[isabelle] Unable to prove easy existential "directly"



Hi all,

as a beginner in the use of Isabelle/Isar, I have every day numerous clashes with the Isar way of proving theorems. The strangest one to date is related to proving an existentially quantified formula when you have the same formula with an explicit witness as a hypothesis. That is to say, something similar to this lemma:

  lemma fie : "P a ⟶ (∃b.(P b))"
  proof
    assume ha : "P a"
    thus "∃b.(P b)"..
  qed

Unsurprisingly, this proof doesn't pose any challenge at all. However I can slightly complicate the formula by means of a definition, and this obvious proof technique won't work any more. Specifically, I define

  definition bijection :: "('a ⇒ 'b) ⇒ bool" where
    "bijection f = (∀y::'b.∃!x::'a. y = f x)"

and then the same proof as before, with bijection in place of a generic P, fails:

  lemma foo : "bijection (g::'a ⇒ 'b) ⟶ (∃ f.(bijection (f::'a ⇒ 'b)))"
  proof
    assume hg : "bijection (g::'a ⇒ 'b)"
    thus "∃f.(bijection f)"..
  qed

replacing the implicit ".." with an explicit "proof (rule exI)" fails similarly, leaving me quite puzzled.
(Un)Interestingly, since "foo" is an instance of "fie", we can easily prove it using "by (rule fie)" and nothing else. However this feels more like a trick to make things work than a solution.

What am I doing wrong?

Best,
--
Wilmer Ricciotti




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.