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



On 09/12/13 12:05, Yannick wrote:
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
This is what you get with the function package. In that case, isα.simps is what you need. With definition, the theorem is usually names <constant name>_def. In your example above, however, you renamed the definition theorem to isα, so apply(simp add: isα) should work.

Best,
Andreas




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