Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Inductively Defined Predicate

Email Gateway (Aug 18 2022 at 12:25):

From: Gary Gao <gary_gao2000@hotmail.com>
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

Email Gateway (Aug 18 2022 at 12:26):

From: Stefan Berghofer <berghofe@in.tum.de>
Gary Gao wrote:
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

Last updated: May 03 2024 at 08:18 UTC