Re: [isabelle] Unable to prove easy existential "directly"



In order to answer Wilmer's original question explicitly: your second lemma can be proved using baby-steps as follows.

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

Observe that you also have to type-constrain the bound variable in "thus", and that (as noted by Christian and Manuel) ".." (or equivalently "apply (rule exI)"), which applies the rule in elim-resolution mode fail due to somewhat inscrutable issues of type resolution.

Of course, you'd typically apply automatic proof methods such as auto or blast that do the job.

Stephan


On Jul 19, 2013, at 2:54 PM, Christian Sternagel <c.sternagel at gmail.com> wrote:

> On 07/19/2013 09:41 PM, Manuel Eberl wrote:
>> But be that as it may, even when one does annotate the bound variable,
>> ".." still does not work, which then brings us back to what I said in my
>> first reply. :)
> 
> Yes. That's what I wanted to say with "combine our two mails". -cheers chris
> 
> For the record: I also find this behavior of ".."/"rule"/... vs. "rule_tac"/"blast"/... strange.
> 
> 





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