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.