[isabelle] Inductively Defined Predicate



Hi,

I defined a subclass predicate inductively as:

datatype cname = 
     CNAME name (*User defined class name*)
  |  OBJECT (*Super class of all classes*);

consts
cIC :: cname
cB :: cname;

constdefs 
clp :: "cname ~=> cname"
"clp == [cIC |-> OBJECT, cB |-> OBJECT]";

inductive
subcls :: "cname => cname => bool"
where
     base [intro!, simp]: "(cn ~= OBJECT) & (clp cn) ~= None ==> subcls cn (the (clp cn))"
  |  step: "(subcls cn cn') & (subcls cn' cn'') ==> subcls cn cn''";

My question is that how can I prove :

lemma "[|cIC ~= OBJECT; cB ~= OBJECT|] ==> ~ subcls cIC cB";

I know that I can prove "subcls cIC cB" is true using inductive case if constant "clp" is defined as "[cIC |-> cB, cB |-> OBJECT]".

Thanks in advance,

Gary
_________________________________________________________________






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