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:
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 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 :)
This archive was generated by a fusion of
Pipermail (Mailman edition) and