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

On Fri, 19 Jul 2013, Brian Huffman wrote:

lemma "bijection (g::'a ⇒ 'b) ⟶ (∃f::'a ⇒ 'b. bijection f)"
proof
assume "bijection g"
then show "∃f::'a ⇒ 'b. bijection f" by (rule exI [of _ g])
qed

lemma "bijection (g::'a ⇒ 'b) ⟶ (∃f::'a ⇒ 'b. bijection f)"
proof
assume "bijection g"
then show "∃f::'a ⇒ 'b. bijection f" by - (rule exI)
qed
The "-" method serves to turn "bijection g" from a chained fact into
an ordinary assumption in the proof goal; this then affects how the
"rule" method does unification. (Writing "by - rule" will also work.)

`For practical purposes, the "by - rule" form is indeed better. My more
``ugly variant above stays formally within structured rule application of
``Isar, but its need of instantiation is not nice.
`

`BTW, the 'by' command has these two slots: initial method and terminal
``method. There is a difference in handling of chained facts, so
`
by method1 method2
is conceptionally (and operationally) different from
by (method1, method2) -- improper
Normally one should only show the good examples to imitate, but

`"by (cases, auto)" is seen a bit too often in examples, where "by cases auto"
``was meant by the writer of the text.
`

The same trick used to be necessary for proving things of the form
"∃A::'a set. P A", during the period when "'a set" was an abbreviation
for "'a => bool".

`Gladly that episode is history. It was known beforehand that such issues
``would follow from that experiment, because Larry or Tobias had introduced
``the explicit 'a set type exactly to prevent HO unification problems,
``although it was before recorded history.
`
Makarius

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