Re: [isabelle] proving existentially quantified statements using 'obtain'ed witness fails
Just for fun some further vacuous 'obtain' proofs:
obtain x where "x = (0 :: nat)" by (rule that) (rule refl)
obtain x where "x == (0 :: nat)" by (rule that) (rule reflexive)
obtain x where "x == (0 :: nat)" ..
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).
This archive was generated by a fusion of
Pipermail (Mailman edition) and