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.