How to replace ⋀ and ⟹ with ∀ and ⟶ in assumption

Question

I'm an Isabelle newbie, and I'm a little (actually, a lot) confused about the relationship between ⋀ and ∀, and between ⟹ and ⟶.

I have the following goal (which is a highly simplified version of something that I've ended up with in a real proof):

⟦⋀x. P x ⟹ P z; P y⟧ ⟹ P z

which I want to prove by specialising x with y to get ⟦P y ⟹ P z; P y⟧ ⟹ P z, and then using modus ponens. This works for proving the very similar-looking:

⟦∀x. P x ⟶ P z; P y⟧ ⟹ P z

but I can't get it to work for the goal above.

Is there a way of converting the former goal into the latter? If not, is this because they are logically different statements, in which case can someone help me understand the difference?

Answer 1

That the two premises !!x. P x ==> P y and ALL x. P x --> P y are logically equivalent can be shown by the following proof

lemma
  "(⋀x. P x ⟹ P y) ≡ (Trueprop (∀x. P x ⟶ P y))"
  by (simp add: atomize_imp atomize_all)

When I tried the same kind of reasoning for your example proof I ran into a problem however. I intended to do the following proof

lemma
  "⟦⋀x. P x ⟹ P z; P y⟧ ⟹ P z"
apply (subst (asm) atomize_imp)
apply (unfold atomize_all)
apply (drule spec [of _ y])
apply (erule rev_mp)
apply assumption
done

but at unfold atomize_all I get

Failed to apply proof method:

When trying to explicitly instantiate the lemma I get a more clear error message, i.e.,

apply (unfold atomize_all [of "λx. P x ⟶ P z"])

yields

Type unification failed: Variable 'a::{} not of sort type

This I find strange, since as far as I know every type variable should be of sort type. We can solve this issue by adding an explicit sort constraint:

lemma
  "⟦⋀x::_::type. P x ⟹ P z; P y⟧ ⟹ P z"

Then the proof works as shown above.

Cutting a long story short. I usually work with Isar structured proofs instead of apply scripts. Then such issues are often avoided. For your statement I would actually do

lemma
  "⟦⋀x. P x ⟹ P z; P y⟧ ⟹ P z"
proof -
  assume *: "⋀x. P x ⟹ P z"
    and **: "P y"
  from * [OF **] show ?thesis .
qed

Or maybe more idiomatic

lemma
  assumes *: "⋀x. P x ⟹ P z"
    and **: "P y"
  shows "P z"
  using * [OF **] .