Re: [isabelle] proving that a value is outside of an inductively defined set



Patrice,

On Sunday 22 January 2006 01:07, Patrice Chalin wrote:
> Given
>
>     theory IndX = Main:
>
>     datatype X = a | b
>
>     consts I :: "X set"
>     inductive I
>     intros
>       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.
by

    apply (erule I.elims)
    apply assumption
  done

Best regards,
Tjark





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