# Re: [isabelle] proving that a value is outside of an inductivelydefined set

To prove the first lemma you need to induct on the cases you get from the intro rules, like this:
lemma bNotInI : "b ~: I"
apply clarify;
by (ind_cases "b : I");
You need to use clarify first to change the not in into an in, then ind_cases finishes it off.
The next lemma you mentioned is then fairly straight-forward:
lemma "x : I ==> x = a"
apply (case_tac x);
apply auto;
by (simp add:bNotInI);
Mark
-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk on behalf of Patrice Chalin
Sent: Sat 1/21/2006 6:07 PM
To: isabelle-users at cl.cam.ac.uk
Subject: [isabelle] proving that a value is outside of an inductivelydefined set
Hi,
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.
Thanks,
Patrice
--
Patrice Chalin, Assistant Professor - http://www.cs.concordia.ca/~chalin
Dependable Software Research Group, CSE Department, Concordia University

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