[isabelle] Data‑types: How to use discriminators?
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, so searched the
web for “Isabelle HOL is_Cons is_Nil” with the hope this could pop up some
examples on the topic. I could just find this, which did not help to
For the practical issue, I encountered a case where I needed but failed to
prove this: “a ≠ ω b ⟹ a ≠ ω (c # d)”. I can't prove it, as “a” is not
produced by “ω” there is no “b” and no way to compare the latter to “(c #
d)”. The case seemed a bit paradoxical to me, when I started to think I
finally need something to say “a” is not produced by the constructor “ω”.
Also I noticed “datatypes.pdf” talks about “datatype_new” and some others,
which seems not to be recognized. Is this an error or something old or
something new to come?
“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