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



Hi Yannik,

What is a destructor? Isn't it pattern matching?
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.

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 and selectors.

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,
Andreas




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