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"
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);
by (simp add:bNotInI);
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
theory IndX = Main:
datatype X = a | b
consts I :: "X set"
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.
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