[isabelle] proving that a value is outside of an inductively defined 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.