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.

Larry Paulson


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.” [1]
> “Structured Programming supports the law of the excluded muddle.” [1]
> [1]: Epigrams on Programming — Alan J. — P. Yale University
> 
> 





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