[isabelle] About undefined

Dear Isabelle experts,

As I have used the keyword "undefined" in my proofs, I am quite curious about its properties. The following lemma is easily proved:

lemma "(undefined::rat) â â  â (undefined::rat) â â" by auto

but I cannot prove either of the following two lemmas:

lemma "(undefined::rat) â â" oops

lemma "(undefined::rat) â â" oops

Is it true that both of the last two propositions are unprovable within Isabelle? If it is, I think it is a fun fact about the non-constructivity in Isabelle.

Any comment is appreciated,

Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge

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