*To*: cl-isabelle-users at lists.cam.ac.uk, Patrice Chalin <chalin at cs.concordia.ca>*Subject*: Re: [isabelle] proving that a value is outside of an inductively defined set*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Mon, 23 Jan 2006 01:54:26 +0100*In-reply-to*: <43D2CCBE.7070409@cs.concordia.ca>*References*: <43D2CCBE.7070409@cs.concordia.ca>*User-agent*: KMail/1.8

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

**References**:**[isabelle] proving that a value is outside of an inductively defined set***From:*Patrice Chalin

- Previous by Date: Re: [isabelle] simple proof over inductively defined relation (operational semantics)
- Next by Date: Re: [isabelle] simple proof over inductively defined relation (operational semantics)
- Previous by Thread: Re: [isabelle] proving that a value is outside of an inductivelydefined set
- Next by Thread: [isabelle] FLoC'06 - Call for Papers
- Cl-isabelle-users January 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list