Re: [isabelle] Data‑types: How to use discriminators?
It’s actually quite rare to need destructor or discriminator functions in datatypes. 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.
On 8 Dec 2013, at 14:13, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote:
> Le Sun, 08 Dec 2013 09:07:41 +0100, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> a écrit:
>> I was seeking for something like constructor predicates, I mean something which says whether or not an instance of that data‑type is from a particular constructor of a that data‑type.
>> In “datatypes.pdf”, in “2.3 Generated Constants” there is the mention of discriminators of the form “t.is_Cn” where “Cn” is the name of a constructor of the type “t”.
>> I could not find anything like this in the theory context, […]
> I fell back to this:
> datatype "term" =
> Any ("ε")
> | Atom atom ("α")
> | Variable variable ("υ")
> | Compound "term list" ("ω")
> primrec isυ :: "term ⇒ bool" where
> "isυ ε = False"
> | "isυ (α _) = False"
> | "isυ (υ _) = True"
> | "isυ (ω _) = False"
> (* And so on for the other three constructors… *)
> “isυ” is what is supposed to be “term.is_Variable” after “datatypes.pdf”, but which does not seems to be there.
> The simplifier seems to be able to deal with this in proof.
> I noticed something I don't understand. Isabelle/jEdit tells me in the output pan and about the primrec: “No function definition for datatype "List.list"”.
> “Syntactic sugar causes cancer of the semi-colons.” 
> “Structured Programming supports the law of the excluded muddle.” 
> : Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and