Re: [isabelle] proving that a value is outside of an inductively defined set
On Sunday 22 January 2006 01:07, Patrice Chalin wrote:
> theory IndX = Main:
> datatype X = a | b
> consts I :: "X set"
> inductive I
> aintro: "a : I"
> How would one prove that b is not in I:
> lemma "b ~: I"
> so that eventually one can prove that x : I ==> x = a.
when you define the set I, an elimination rule is proved automatically (see
"thm I.elims"). Your latter lemma, "x : I ==> x = a", can be proved e.g.
apply (erule I.elims)
This archive was generated by a fusion of
Pipermail (Mailman edition) and