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

isabelle

Solution

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 **] .

Problem

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?

Original source