*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] proving that a value is outside of an inductively defined set*From*: Patrice Chalin <chalin at cs.concordia.ca>*Date*: Sat, 21 Jan 2006 19:07:26 -0500*User-agent*: Thunderbird 1.4 (Windows/20050908)

Hi, Given How would one prove that b is not in I:theory IndX = Main: datatype X = a | b consts I :: "X set" inductive I intros aintro: "a : I" so that eventually one can prove that x : I ==> x = a.lemma "b ~: I" Thanks, Patrice -- Patrice Chalin, Assistant Professor - http://www.cs.concordia.ca/~chalin Dependable Software Research Group, CSE Department, Concordia University |

**Follow-Ups**:**Re: [isabelle] proving that a value is outside of an inductivelydefined set***From:*Mark A Hills

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

- Previous by Date: Re: [isabelle] simple proof over inductively defined relation (operational semantics)
- Next by Date: Re: [isabelle] proving that a value is outside of an inductivelydefined set
- Previous by Thread: Re: [isabelle] subst_tac?
- Next by Thread: Re: [isabelle] proving that a value is outside of an inductivelydefined set
- 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