Re: [isabelle] Data‑types: How to use discriminators?
A destructor (or more precisely, a selector) is a function that returns one of the
arguments of a constructor. For example, hd and tl are the selectors for list, they return
the arguments of a Cons.
What is a destructor? Isn't it pattern matching?
The new datatype package (keyword datatype_new) generates such discriminators and
selectors, the old one (keyword datatype) does not. In Isabelle2013-1, the datatypes in
HOL are generated by the old datatype package. To use the new datatype package, you must
import ~~/src/HOL/BNF/BNF. But of course, you can always define your own discriminators
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
Have you tried apply(simp add: isα_def)? It should do the job.
lemma "isα t ⟹ t = α a" sorry -- No way too
This is not provable, you probably want to have "isα t ⟹ EX a. t = α a".
Try by(cases t)(auto simp add: isα_def)
Hope this helps,
This archive was generated by a fusion of
Pipermail (Mailman edition) and