Re: [isabelle] Inductively Defined Predicate



Gary Gao wrote:
> My question is that how can I prove :
> 
> lemma "[|cIC ~= OBJECT; cB ~= OBJECT|] ==> ~ subcls cIC cB";

You can prove an auxiliary lemma by induction on subcls, from
which your lemma follows trivially:

lemma aux:
  assumes "subcls cIC cB"
  shows "cIC ~= OBJECT" "cB = OBJECT"
  using assms
  by induct (simp_all add: clp_def split add: split_if_asm)

lemma "[|cIC ~= OBJECT; cB ~= OBJECT|] ==> ~ subcls cIC cB"
  by (blast dest: aux)

Greetings,
Stefan

-- 
Dr. Stefan Berghofer               E-Mail: berghofe at in.tum.de
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY            http://www.in.tum.de/~berghofe





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