Re: [isabelle] Data‑types: How to use discriminators?
On Sun, 08 Dec 2013 15:24:49 +0100, Lawrence Paulson <lp15 at cam.ac.uk>
It’s actually quite rare to need destructor or discriminator functions
What is a destructor? Isn't it pattern matching?
I guess too it may be perhaps quite rare, but it's unavoidable for my
actual practical case. Using pattern matching in propositions is not
always OK, as it can lead to paradoxical cases where its needed to prove a
relation between things which don't exist. That's why I need a predicates
which really says “t is as this” or “t is not as this”.
You should use pattern-matching instead, or the built-in case
expression. With the latter, you can also get the simplifier to perform
rewriting with case-splitting automatically.
I tried with a definition and a function:
definition isα: "isα t ≡ (case t of α a ⇒ True | _ ⇒ False)"
lemma "t = α a ⟹ isα t" sorry -- No way, and unfolding does not help
lemma "isα t ⟹ t = α a" sorry -- No way too
fun isα where "isα t = (case t of α a ⇒ True | _ ⇒ False)"
lemma "t = α a ⟹ isα t" sorry -- OK
lemma "isα t ⟹ t = α a" by simp -- But no way with this one
None seems to work as expectable and even “try” fails to find a solution.
This archive was generated by a fusion of
Pipermail (Mailman edition) and