Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails



Just for fun some further vacuous 'obtain' proofs:

notepad
begin
  obtain x where "x = (0 :: nat)" by (rule that) (rule refl)
next
  obtain x where "x == (0 :: nat)" by (rule that) (rule reflexive)
next
  obtain x where "x == (0 :: nat)" ..
end

The last form works, because "that" is declared as Pure.intro, and Pure "reflexive" implicit (like assumption).


The better form is this:

  def x == "0 :: nat"

Here the system does the reflexicity step for you, and it bypasses the full "may-assume-that-holds" mechanism of 'obtain', that involves the restriction on variable occurrences (as seen in the exE rule).


	Makarius





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