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

On Sun, 08 Dec 2013 15:24:49 +0100, Lawrence Paulson <lp15 at>

It’s actually quite rare to need destructor or discriminator functions in datatypes.

What is a destructor? Isn't it pattern matching?

I guess too it may be perhaps quite rare, but it's unavoidable for my actual practical case. Using pattern matching in propositions is not always OK, as it can lead to paradoxical cases where its needed to prove a relation between things which don't exist. That's why I need a predicates which really says “t is as this” or “t is not as this”.

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.

I tried with a definition and a function:

    definition isα: "isα t ≡ (case t of α a ⇒ True | _ ⇒ False)"

    lemma "t = α a ⟹ isα t" sorry -- No way, and unfolding does not help
    lemma "isα t ⟹ t = α a" sorry -- No way too


    fun isα where "isα t = (case t of α a ⇒ True | _ ⇒ False)"

    lemma "t = α a ⟹ isα t" sorry -- OK
    lemma "isα t ⟹ t = α a" by simp -- But no way with this one

None seems to work as expectable and even “try” fails to find a solution.

Yannick Duchêne

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