Re: [isabelle] Data‑types: How to use discriminators?
Yes, fresh variables in theorem statements are implicitly fixed. You can also specify
variables that you can instantiate later, as in
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?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and