Re: [isabelle] Data‑types: How to use discriminators?



Hi Yannik,

Yes, that was the intent. I though this was the same as to say there exist an “a” such
that “t = α a”. Or else, this just mean nothing, unless “a” is fixed and in which case
this is indeed not provable. Is “a” implicitly fixed in the proposition I tested?
Yes, fresh variables in theorem statements are implicitly fixed. You can also specify variables that you can instantiate later, as in

schematic_lemma "isα t ==> t = α ?a"

but this does not work well with Isar proofs, parallelisation of proof checking, and (in this case) proof automation. So it's better to explicitly use an existential quantifier here.

Best,
Andreas




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