Re: [isabelle] Data‑types: How to use discriminators?
On Mon, 09 Dec 2013 10:44:27 +0100, Andreas Lochbihler
<andreas.lochbihler at inf.ethz.ch> wrote:
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
Have you tried apply(simp add: isα_def)? It should do the job.
I forget to comment on this: “thm isα_def” just says “isα ≡ isα_sumC”, and
“isα_sumC” is just a constant of type “t => bool”, so it was not usable
(HOL-BNF has a really usable “is_Atom_def”).
This archive was generated by a fusion of
Pipermail (Mailman edition) and