Re: [isabelle] Data‑types: How to use discriminators?
On 09/12/13 12:05, Yannick wrote:
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.
On Mon, 09 Dec 2013 10:44:27 +0100, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
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 archive was generated by a fusion of
Pipermail (Mailman edition) and