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

Le Sun, 08 Dec 2013 09:07:41 +0100, Yannick Duchêne (Hibou57) <yannick_duchene at> 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.