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 help
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”).

--
Yannick Duchêne




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