[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 understand:
http://isabelle.in.tum.de/repos/isabelle/file/3d520eec2746/src/HOL/Codatatype/Tools/bnf_wrap.ML

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.” [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.