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



On Mon, 09 Dec 2013 10:44:27 +0100, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch> wrote:

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.

So I will try this one.

     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)

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? If so, I didn't suspected it, and will be aware of it since now.

Thanks for the precious comments :)

--
Yannick Duchêne




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