header {* \isaheader{Definition of Subobjects} *}
theory SubObj imports ClassRel begin
section {* General definitions *}
types
subobj = "cname × path"
consts
mdc :: "subobj => cname"
ldc :: "subobj => cname"
defs mdc_def:
"mdc S == fst S"
defs ldc_def:
"ldc S == last (snd S)"
lemma mdc_tuple [simp]: "mdc (C,Cs) = C"
by(simp add:mdc_def)
lemma ldc_tuple [simp]: "ldc (C,Cs) = last Cs"
by(simp add:ldc_def)
section {* Subobjects according to Rossie-Friedman *}
consts
is_subobj :: "prog × subobj => bool" -- "legal subobject to class hierarchie"
recdef is_subobj "measure (λ (P,(C,Xs)).length Xs)"
"is_subobj (P,(C,[])) = False"
"is_subobj (P,(C,[D])) = ((is_class P C ∧ C = D)
∨ (∃ X. P \<turnstile> C \<preceq>* X ∧ P \<turnstile> X \<prec>S D))"
"is_subobj (P, (C,D#E#Xs)) = (let Ys=butlast(D#E#Xs);
Y=last (D#E#Xs);
X=last Ys
in is_subobj (P, (C,Ys)) ∧ P \<turnstile> X \<prec>R Y)"
lemma subobj_aux_rev:
assumes 1:"is_subobj(P,(C,C'#rev Cs@[C'']))"
shows "is_subobj(P,(C,C'#rev Cs))"
proof -
obtain Cs' where Cs':"Cs' = rev Cs" by simp
hence rev:"Cs'@[C''] = rev Cs@[C'']" by simp
from this obtain D Ds where DDs:"Cs'@[C''] = D#Ds" by (cases Cs') auto
with 1 rev have subo:"is_subobj(P,(C,C'#D#Ds))" by simp
from DDs have "butlast (C'#D#Ds) = C'#Cs'" by (cases Cs') auto
with subo have "is_subobj(P,(C,C'#Cs'))" by simp
with Cs' show ?thesis by simp
qed
lemma subobj_aux:
assumes 1:"is_subobj(P,(C,C'#Cs@[C'']))"
shows "is_subobj(P,(C,C'#Cs))"
proof -
from 1 obtain Cs' where Cs':"Cs' = rev Cs" by simp
with 1 have "is_subobj (P,(C,C'#rev Cs'@[C'']))" by simp
hence "is_subobj (P,(C,C'#rev Cs'))" by (rule subobj_aux_rev)
with Cs' show ?thesis by simp
qed
lemma isSubobj_isClass:
assumes 1:"is_subobj (P,R)"
shows "is_class P (mdc R)"
proof -
obtain C' Cs' where R:"R = (C',Cs')" by(cases R) auto
with 1 have ne:"Cs' ≠ []" by (cases Cs') auto
from this obtain C'' Cs'' where C''Cs'':"Cs' = C''#Cs''" by (cases Cs') auto
from this obtain Ds where "Ds = rev Cs''" by simp
with 1 R C''Cs'' have subo1:"is_subobj(P,(C',C''#rev Ds))" by simp
with R show ?thesis
by (induct Ds,auto simp:mdc_def split:split_if_asm dest:subobj_aux,
auto elim:converse_rtranclE dest!:subclsS_subcls1 elim:subcls1_class)
qed
lemma isSubobjs_subclsR_rev:
assumes 1:"is_subobj (P,(C,Cs@[D,D']@(rev Cs')))"
shows "P \<turnstile> D \<prec>R D'"
using 1
proof (induct Cs')
case Nil
from this obtain Cs' X Y Xs where Cs'1:"Cs' = Cs@[D,D']"
and "X = hd(Cs@[D,D'])" and "Y = hd(tl(Cs@[D,D']))"
and "Xs = tl(tl(Cs@[D,D']))" by simp
hence Cs'2:"Cs' = X#Y#Xs" by (cases Cs) auto
from Cs'1 have last:"last Cs' = D'" by simp
from Cs'1 have butlast:"last(butlast Cs') = D" by (simp add:butlast_tail)
from Nil Cs'1 Cs'2 have "is_subobj (P,(C,X#Y#Xs))" by simp
with last butlast Cs'2 show ?case by simp
next
case (Cons C'' Cs'')
have IH:"is_subobj (P, C, Cs @ [D, D'] @ rev Cs'') ==> P \<turnstile> D \<prec>R D'" by fact
from Cons obtain Cs' X Y Xs where Cs'1:"Cs' = Cs@[D,D']@(rev (C''#Cs''))"
and "X = hd(Cs@[D,D']@(rev (C''#Cs'')))"
and "Y = hd(tl(Cs@[D,D']@(rev (C''#Cs''))))"
and "Xs = tl(tl(Cs@[D,D']@(rev (C''#Cs''))))" by simp
hence Cs'2:"Cs' = X#Y#Xs" by (cases Cs) auto
from Cons Cs'1 Cs'2 have "is_subobj (P,(C,X#Y#Xs))" by simp
hence sub:"is_subobj (P,(C,butlast (X#Y#Xs)))" by simp
from Cs'1 obtain E Es where Cs'3:"Cs' = Es@[E]" by (cases Cs') auto
with Cs'1 have butlast:"Es = Cs@[D,D']@(rev Cs'')" by simp
from Cs'3 have "butlast Cs' = Es" by simp
with butlast have "butlast Cs' = Cs@[D,D']@(rev Cs'')" by simp
with Cs'2 sub have "is_subobj (P,(C,Cs@[D,D']@(rev Cs'')))"
by simp
with IH show ?case by simp
qed
lemma isSubobjs_subclsR:
assumes 1:"is_subobj (P,(C,Cs@[D,D']@Cs'))"
shows "P \<turnstile> D \<prec>R D'"
proof -
from 1 obtain Cs'' where "Cs'' = rev Cs'" by simp
with 1 have "is_subobj (P,(C,Cs@[D,D']@(rev Cs'')))" by simp
thus ?thesis by (rule isSubobjs_subclsR_rev)
qed
lemma mdc_leq_ldc_aux:
assumes 1:"is_subobj(P,(C,C'#rev Cs'))"
shows "P \<turnstile> C \<preceq>* last (C'#rev Cs')"
using 1
proof (induct Cs')
case Nil
from 1 have "is_class P C"
by (drule_tac R="(C,C'#rev Cs')" in isSubobj_isClass, simp add:mdc_def)
with Nil show ?case
proof (cases "C=C'")
case True
thus ?thesis by simp
next
case False
with Nil show ?thesis
by (auto dest!:subclsS_subcls1)
qed
next
case (Cons C'' Cs'')
have IH:"is_subobj (P, C, C' # rev Cs'') ==> P \<turnstile> C \<preceq>* last (C' # rev Cs'')"
and subo:"is_subobj (P, C, C' # rev (C'' # Cs''))" by fact+
hence "is_subobj (P, C, C' # rev Cs'')" by (simp add:subobj_aux_rev)
with IH have rel:"P \<turnstile> C \<preceq>* last (C' # rev Cs'')" by simp
from subo obtain D Ds where DDs:"C' # rev Cs'' = Ds@[D]"
by (cases Cs'') auto
hence " C' # rev (C'' # Cs'') = Ds@[D,C'']" by simp
with subo have "is_subobj(P,(C,Ds@[D,C'']))" by (cases Ds) auto
hence "P \<turnstile> D \<prec>R C''" by (rule_tac Cs'="[]" in isSubobjs_subclsR) simp
hence rel1:"P \<turnstile> D \<prec>1 C''" by (rule subclsR_subcls1)
from DDs have "D = last (C' # rev Cs'')" by simp
with rel1 have lastrel1:"P \<turnstile> last (C' # rev Cs'') \<prec>1 C''" by simp
with rel have "P \<turnstile> C \<preceq>* C''"
by(rule_tac b="last (C' # rev Cs'')" in rtrancl_into_rtrancl) simp
thus ?case by simp
qed
lemma mdc_leq_ldc:
assumes 1:"is_subobj(P,R)"
shows "P \<turnstile> mdc R \<preceq>* ldc R"
proof -
from 1 obtain C Cs where R:"R = (C,Cs)" by (cases R) auto
with 1 have ne:"Cs ≠ []" by (cases Cs) auto
from this obtain C' Cs' where Cs:"Cs = C'#Cs'" by (cases Cs) auto
from this obtain Cs'' where Cs':"Cs'' = rev Cs'" by simp
with R Cs 1 have "is_subobj(P,(C,C'#rev Cs''))" by simp
hence rel:"P \<turnstile> C \<preceq>* last (C'#rev Cs'')" by (rule mdc_leq_ldc_aux)
from R Cs Cs' have ldc:"last (C'#rev Cs'') = ldc R" by(simp add:ldc_def)
from R have "mdc R = C" by(simp add:mdc_def)
with ldc rel show ?thesis by simp
qed
text{* Next three lemmas show subobject property as presented in literature *}
lemma class_isSubobj:
"is_class P C ==> is_subobj (P,(C,[C]))"
by simp
lemma repSubobj_isSubobj:
assumes 1:"is_subobj (P,(C,Xs@[X]))" and 2:"P \<turnstile> X \<prec>R Y"
shows "is_subobj (P,(C,Xs@[X,Y]))"
using 1
proof -
obtain Cs D E Cs' where Cs1:"Cs = Xs@[X,Y]" and "D = hd(Xs@[X,Y])"
and "E = hd(tl(Xs@[X,Y]))" and "Cs' = tl(tl(Xs@[X,Y]))"by simp
hence Cs2:"Cs = D#E#Cs'" by (cases Xs) auto
with 1 Cs1 have subobj_butlast:"is_subobj (P,(C,butlast(D#E#Cs')))"
by (simp add:butlast_tail)
with 2 Cs1 Cs2 have "P \<turnstile> (last(butlast(D#E#Cs'))) \<prec>R last(D#E#Cs')"
by (simp add:butlast_tail)
with subobj_butlast have "is_subobj (P,(C,(D#E#Cs')))" by simp
with Cs1 Cs2 show ?thesis by simp
qed
lemma shSubobj_isSubobj:
assumes 1: "is_subobj (P,(C,Xs@[X]))" and 2:"P \<turnstile> X \<prec>S Y"
shows "is_subobj (P,(C,[Y]))"
using 1
proof -
from 1 have classC:"is_class P C"
by (drule_tac R="(C,Xs@[X])" in isSubobj_isClass, simp add:mdc_def)
from 1 have "P \<turnstile> C \<preceq>* X"
by (drule_tac R="(C,Xs@[X])" in mdc_leq_ldc, simp add:mdc_def ldc_def)
with classC 2 show ?thesis by fastsimp
qed
text{* Auxiliary lemmas *}
lemma build_rec_isSubobj_rev:
assumes 1:"is_subobj (P,(D,D#rev Cs))" and 2:" P \<turnstile> C \<prec>R D"
shows "is_subobj (P,(C,C#D#rev Cs))"
using 1
proof (induct Cs)
case Nil
from 2 have "is_class P C" by (auto dest:subclsRD simp add:is_class_def)
with 1 2 show ?case by simp
next
case (Cons C' Cs')
have suboD:"is_subobj (P,(D,D#rev (C'#Cs')))"
and IH:"is_subobj (P,(D,D#rev Cs')) ==> is_subobj (P,(C,C#D#rev Cs'))" by fact+
obtain E Es where E:"E = hd (rev (C'#Cs'))" and Es:"Es = tl (rev (C'#Cs'))"
by simp
with E have E_Es:"rev (C'#Cs') = E#Es" by simp
with E Es have butlast:"butlast (D#E#Es) = D#rev Cs'" by simp
from E_Es suboD have suboDE:"is_subobj (P,(D,D#E#Es))" by simp
hence "is_subobj (P,(D,butlast (D#E#Es)))" by simp
with butlast have "is_subobj (P,(D,D#rev Cs'))" by simp
with IH have suboCD:"is_subobj (P, C, C#D#rev Cs')" by simp
from suboDE obtain Xs X Y Xs' where Xs':"Xs' = D#E#Es"
and bb:"Xs = butlast (butlast (D#E#Es))"
and lb:"X = last(butlast (D#E#Es))" and l:"Y = last (D#E#Es)" by simp
from this obtain Xs'' where Xs'':"Xs'' = Xs@[X]" by simp
with bb lb have "Xs'' = butlast (D#E#Es)" by simp
with l have "D#E#Es = Xs''@[Y]" by simp
with Xs'' have "D#E#Es = Xs@[X]@[Y]" by simp
with suboDE have "is_subobj (P,(D,Xs@[X,Y]))" by simp
hence subR:"P \<turnstile> X \<prec>R Y" by(rule_tac Cs="Xs" and Cs'="[]" in isSubobjs_subclsR) simp
from E_Es Es have "last (D#E#Es) = C'" by simp
with subR lb l butlast have "P \<turnstile> last(D#rev Cs') \<prec>R C'"
by (auto split:split_if_asm)
with suboCD show ?case by simp
qed
lemma build_rec_isSubobj:
assumes 1:"is_subobj (P,(D,D#Cs))" and 2:" P \<turnstile> C \<prec>R D"
shows "is_subobj (P,(C,C#D#Cs))"
proof -
obtain Cs' where Cs':"Cs' = rev Cs" by simp
with 1 have "is_subobj (P,(D,D#rev Cs'))" by simp
with 2 have "is_subobj (P,(C,C#D#rev Cs'))"
by - (rule build_rec_isSubobj_rev)
with Cs' show ?thesis by simp
qed
lemma isSubobj_isSubobj_isSubobj_rev:
assumes 1:"is_subobj(P,(C,[D]))" and 2:"is_subobj(P,(D,D#(rev Cs)))"
shows "is_subobj(P,(C,D#(rev Cs)))"
using 2
proof (induct Cs)
case Nil
with 1 show ?case by simp
next
case (Cons C' Cs')
have IH:"is_subobj (P,(D,D#rev Cs')) ==> is_subobj (P,(C,D#rev Cs'))"
and "is_subobj (P,(D,D#rev (C'#Cs')))" by fact+
hence suboD:"is_subobj (P,(D,D#rev Cs'@[C']))" by simp
hence "is_subobj (P,(D,D#rev Cs'))" by (rule subobj_aux_rev)
with IH have suboC:"is_subobj (P,(C,D#rev Cs'))" by simp
obtain C'' where C'':"C'' = last(D#rev Cs')" by simp
hence butlast:"D#rev Cs' = butlast(D#rev Cs')@[C'']" by simp
hence butlast2:"D#rev Cs'@[C'] = butlast(D#rev Cs')@[C'']@[C']" by simp
with suboD have "is_subobj (P,(D,butlast(D#rev Cs')@[C'']@[C']))"
by simp
with C'' have subR:"P \<turnstile> C'' \<prec>R C'"
by (rule_tac Cs="butlast(D#rev Cs')" and Cs'="[]" in isSubobjs_subclsR)simp
with C'' suboC butlast have "is_subobj (P,(C,butlast(D#rev Cs')@[C'']@[C']))"
by (auto intro:repSubobj_isSubobj simp del:butlast.simps)
with butlast2 have "is_subobj (P,(C,D#rev Cs'@[C']))"
by (cases Cs')auto
thus ?case by simp
qed
lemma isSubobj_isSubobj_isSubobj:
assumes 1:"is_subobj(P,(C,[D]))" and 2:"is_subobj(P,(D,D#Cs))"
shows "is_subobj(P,(C,D#Cs))"
proof -
obtain Cs' where Cs':"Cs' = rev Cs" by simp
with 2 have "is_subobj(P,(D,D#rev Cs'))" by simp
with 1 have "is_subobj(P,(C,D#rev Cs'))"
by - (rule isSubobj_isSubobj_isSubobj_rev)
with Cs' show ?thesis by simp
qed
section {* Subobject handling and lemmas *}
text{* Subobjects consisting of repeated inheritance relations only: *}
inductive SubobjsR :: "prog => cname => path => bool" for P :: prog
where
SubobjsR_Base: "is_class P C ==> SubobjsR P C [C]"
| SubobjsR_Rep: "[|P \<turnstile> C \<prec>R D; SubobjsR P D Cs|] ==> SubobjsR P C (C # Cs)"
text{* All subobjects: *}
inductive Subobjs :: "prog => cname => path => bool" for P :: prog
where
Subobjs_Rep: "SubobjsR P C Cs ==> Subobjs P C Cs"
| Subobjs_Sh: "[|P \<turnstile> C \<preceq>* C'; P \<turnstile> C' \<prec>S D; SubobjsR P D Cs|]
==> Subobjs P C Cs"
lemma Subobjs_Base:"is_class P C ==> Subobjs P C [C]"
by (fastsimp intro:Subobjs_Rep SubobjsR_Base)
lemma SubobjsR_nonempty: "SubobjsR P C Cs ==> Cs ≠ []"
by (induct rule: SubobjsR.induct, simp_all)
lemma Subobjs_nonempty: "Subobjs P C Cs ==> Cs ≠ []"
by (erule Subobjs.induct)(erule SubobjsR_nonempty)+
lemma hd_SubobjsR:
"SubobjsR P C Cs ==> ∃Cs'. Cs = C#Cs'"
by(erule SubobjsR.induct,simp+)
lemma SubobjsR_subclassRep:
"SubobjsR P C Cs ==> (C,last Cs) ∈ (subclsR P)*"
apply(erule SubobjsR.induct)
apply simp
apply(simp add: SubobjsR_nonempty)
done
lemma SubobjsR_subclass: "SubobjsR P C Cs ==> P \<turnstile> C \<preceq>* last Cs"
apply(erule SubobjsR.induct)
apply simp
apply(simp add: SubobjsR_nonempty)
apply(blast intro:subclsR_subcls1 rtrancl_trans)
done
lemma Subobjs_subclass: "Subobjs P C Cs ==> P \<turnstile> C \<preceq>* last Cs"
apply(erule Subobjs.induct)
apply(erule SubobjsR_subclass)
apply(erule rtrancl_trans)
apply(blast intro:subclsS_subcls1 SubobjsR_subclass rtrancl_trans)
done
lemma Subobjs_notSubobjsR:
"[|Subobjs P C Cs; ¬ SubobjsR P C Cs|]
==> ∃C' D. P \<turnstile> C \<preceq>* C' ∧ P \<turnstile> C' \<prec>S D ∧ SubobjsR P D Cs"
apply (induct rule: Subobjs.induct)
apply clarsimp
apply fastsimp
done
lemma assumes subo:"SubobjsR P (hd (Cs@ C'#Cs')) (Cs@ C'#Cs')"
shows SubobjsR_Subobjs:"Subobjs P C' (C'#Cs')"
using subo
proof (induct Cs)
case Nil
thus ?case by -(frule hd_SubobjsR,fastsimp intro:Subobjs_Rep)
next
case (Cons D Ds)
have subo':"SubobjsR P (hd ((D#Ds) @ C'#Cs')) ((D#Ds) @ C'#Cs')"
and IH:"SubobjsR P (hd (Ds @ C'#Cs')) (Ds @ C'#Cs') ==> Subobjs P C' (C'#Cs')" by fact+
from subo' have "SubobjsR P (hd (Ds @ C' # Cs')) (Ds @ C' # Cs')"
apply -
apply (drule SubobjsR.cases)
apply auto
apply (rename_tac D')
apply (subgoal_tac "D' = hd (Ds @ C' # Cs')")
apply (auto dest:hd_SubobjsR)
done
with IH show ?case by simp
qed
lemma Subobjs_Subobjs:"Subobjs P C (Cs@ C'#Cs') ==> Subobjs P C' (C'#Cs')"
apply -
apply (drule Subobjs.cases)
apply auto
apply (subgoal_tac "C = hd(Cs @ C' # Cs')")
apply (fastsimp intro:SubobjsR_Subobjs)
apply (fastsimp dest:hd_SubobjsR)
apply (subgoal_tac "D = hd(Cs @ C' # Cs')")
apply (fastsimp intro:SubobjsR_Subobjs)
apply (fastsimp dest:hd_SubobjsR)
done
lemma SubobjsR_isClass:
assumes subo:"SubobjsR P C Cs"
shows "is_class P C"
using subo
proof (induct rule:SubobjsR.induct)
case SubobjsR_Base thus ?case by assumption
next
case SubobjsR_Rep thus ?case by (fastsimp intro:subclsR_subcls1 subcls1_class)
qed
lemma Subobjs_isClass:
assumes subo:"Subobjs P C Cs"
shows "is_class P C"
using subo
proof (induct rule:Subobjs.induct)
case Subobjs_Rep thus ?case by (rule SubobjsR_isClass)
next
case (Subobjs_Sh C C' D Cs)
have leq:"P \<turnstile> C \<preceq>* C'" and leqS:"P \<turnstile> C' \<prec>S D" by fact+
hence "(C,D) ∈ (subcls1 P)+" by (fastsimp intro:rtrancl_into_trancl1 subclsS_subcls1)
thus ?case by (induct rule:trancl_induct, fastsimp intro:subcls1_class)
qed
lemma Subobjs_subclsR:
assumes subo:"Subobjs P C (Cs@[D,D']@Cs')"
shows "P \<turnstile> D \<prec>R D'"
using subo
proof -
from subo have "Subobjs P D (D#D'#Cs')" by -(rule Subobjs_Subobjs,simp)
then obtain C' where subo':"SubobjsR P C' (D#D'#Cs')"
by (induct rule:Subobjs.induct,blast+)
hence "C' = D" by -(drule hd_SubobjsR,simp)
with subo' have "SubobjsR P D (D#D'#Cs')" by simp
thus ?thesis by (fastsimp elim:SubobjsR.cases dest:hd_SubobjsR)
qed
lemma assumes subo:"SubobjsR P (hd Cs) (Cs@[D])" and notempty:"Cs ≠ []"
shows butlast_Subobjs_Rep:"SubobjsR P (hd Cs) Cs"
using subo notempty
proof (induct Cs)
case Nil thus ?case by simp
next
case (Cons C' Cs')
have subo:"SubobjsR P (hd(C'#Cs')) ((C'#Cs')@[D])"
and IH:"[|SubobjsR P (hd Cs') (Cs'@[D]); Cs' ≠ []|] ==> SubobjsR P (hd Cs') Cs'" by fact+
from subo have subo':"SubobjsR P C' (C'#Cs'@[D])" by simp
show ?case
proof (cases "Cs' = []")
case True
with subo' have "SubobjsR P C' [C',D]" by simp
hence "is_class P C'" by(rule SubobjsR_isClass)
hence "SubobjsR P C' [C']" by (rule SubobjsR_Base)
with True show ?thesis by simp
next
case False
with subo' obtain D' where subo'':"SubobjsR P D' (Cs'@[D])"
and subR:"P \<turnstile> C' \<prec>R D'"
by (auto elim:SubobjsR.cases)
from False subo'' have hd:"D' = hd Cs'"
by (induct Cs',auto dest:hd_SubobjsR)
with subo'' False IH have "SubobjsR P (hd Cs') Cs'" by simp
with subR hd have "SubobjsR P C' (C'#Cs')" by (fastsimp intro:SubobjsR_Rep)
thus ?thesis by simp
qed
qed
lemma assumes subo:"Subobjs P C (Cs@[D])" and notempty:"Cs ≠ []"
shows butlast_Subobjs:"Subobjs P C Cs"
using subo
proof (rule Subobjs.cases,auto)
assume suboR:"SubobjsR P C (Cs@[D])" and "Subobjs P C (Cs@[D])"
from suboR notempty have hd:"C = hd Cs"
by (induct Cs,auto dest:hd_SubobjsR)
with suboR notempty have "SubobjsR P (hd Cs) Cs"
by(fastsimp intro:butlast_Subobjs_Rep)
with hd show "Subobjs P C Cs" by (fastsimp intro:Subobjs_Rep)
next
fix C' D' assume leq:"P \<turnstile> C \<preceq>* C'" and subS:"P \<turnstile> C' \<prec>S D'"
and suboR:"SubobjsR P D' (Cs@[D])" and "Subobjs P C (Cs@[D])"
from suboR notempty have hd:"D' = hd Cs"
by (induct Cs,auto dest:hd_SubobjsR)
with suboR notempty have "SubobjsR P (hd Cs) Cs"
by(fastsimp intro:butlast_Subobjs_Rep)
with hd leq subS show "Subobjs P C Cs"
by(fastsimp intro:Subobjs_Sh)
qed
lemma assumes subo:"Subobjs P C (Cs@(rev Cs'))" and notempty:"Cs ≠ []"
shows rev_appendSubobj:"Subobjs P C Cs"
using subo
proof(induct Cs')
case Nil thus ?case by simp
next
case (Cons D Ds)
have subo':"Subobjs P C (Cs@rev(D#Ds))"
and IH:"Subobjs P C (Cs@rev Ds) ==> Subobjs P C Cs" by fact+
from notempty subo' have "Subobjs P C (Cs@rev Ds)"
by (fastsimp intro:butlast_Subobjs)
with IH show ?case by simp
qed
lemma appendSubobj:
assumes subo:"Subobjs P C (Cs@Cs')" and notempty:"Cs ≠ []"
shows "Subobjs P C Cs"
proof -
obtain Cs'' where Cs'':"Cs'' = rev Cs'" by simp
with subo have "Subobjs P C (Cs@(rev Cs''))" by simp
with notempty show ?thesis by - (rule rev_appendSubobj)
qed
lemma SubobjsR_isSubobj:
"SubobjsR P C Cs ==> is_subobj(P,(C,Cs))"
by(erule SubobjsR.induct,simp,
auto dest:hd_SubobjsR intro:build_rec_isSubobj)
lemma leq_SubobjsR_isSubobj:
"[|P \<turnstile> C \<preceq>* C'; P \<turnstile> C' \<prec>S D; SubobjsR P D Cs|]
==> is_subobj (P,(C,Cs))"
apply (subgoal_tac "is_subobj(P,(C,[D]))")
apply (frule hd_SubobjsR)
apply (drule SubobjsR_isSubobj)
apply (erule exE)
apply (simp del:is_subobj.simps)
apply (erule isSubobj_isSubobj_isSubobj)
apply simp
apply auto
done
lemma Subobjs_isSubobj:
"Subobjs P C Cs ==> is_subobj(P,(C,Cs))"
by (auto elim:Subobjs.induct SubobjsR_isSubobj
simp add:leq_SubobjsR_isSubobj)
section {* Paths *}
subsection {* Appending paths *}
text{* Avoided name clash by calling one path Path. *}
constdefs
path_via :: "prog => cname => cname => path => bool"
("_ \<turnstile> Path _ to _ via _ " [51,51,51,51] 50)
"P \<turnstile> Path C to D via Cs ≡ Subobjs P C Cs ∧ last Cs = D"
path_unique :: "prog => cname => cname => bool"
("_ \<turnstile> Path _ to _ unique" [51,51,51] 50)
"P \<turnstile> Path C to D unique ≡ ∃!Cs. Subobjs P C Cs ∧ last Cs = D"
appendPath :: "path => path => path" (infixr "@p" 65)
"Cs @p Cs' ≡ if (last Cs = hd Cs') then Cs @ (tl Cs') else Cs'"
lemma appendPath_last: "Cs ≠ [] ==> last Cs = last (Cs'@pCs)"
by(auto simp:appendPath_def last_append)(cases Cs, simp_all)+
inductive
casts_to :: "prog => ty => val => val => bool"
("_ \<turnstile> _ casts _ to _ " [51,51,51,51] 50)
for P :: prog
where
casts_prim: "∀C. T ≠ Class C ==> P \<turnstile> T casts v to v"
| casts_null: "P \<turnstile> Class C casts Null to Null"
| casts_ref: "[| P \<turnstile> Path last Cs to C via Cs'; Ds = Cs@pCs' |]
==> P \<turnstile> Class C casts Ref(a,Cs) to Ref(a,Ds)"
inductive
Casts_to :: "prog => ty list => val list => val list => bool"
("_ \<turnstile> _ Casts _ to _ " [51,51,51,51] 50)
for P :: prog
where
Casts_Nil: "P \<turnstile> [] Casts [] to []"
| Casts_Cons: "[| P \<turnstile> T casts v to v'; P \<turnstile> Ts Casts vs to vs' |]
==> P \<turnstile> (T#Ts) Casts (v#vs) to (v'#vs')"
lemma length_Casts_vs:
"P \<turnstile> Ts Casts vs to vs' ==> length Ts = length vs"
by (induct rule:Casts_to.induct,simp_all)
lemma length_Casts_vs':
"P \<turnstile> Ts Casts vs to vs' ==> length Ts = length vs'"
by (induct rule:Casts_to.induct,simp_all)
subsection {* The relation on paths *}
inductive_set
leq_path1 :: "prog => cname => (path × path) set"
and leq_path1' :: "prog => cname => [path, path] => bool" ("_,_ \<turnstile> _ \<sqsubset>1 _" [71,71,71] 70)
for P :: prog and C :: cname
where
"P,C \<turnstile> Cs \<sqsubset>1 Ds ≡ (Cs,Ds) ∈ leq_path1 P C"
| leq_pathRep: "[| Subobjs P C Cs; Subobjs P C Ds; Cs = butlast Ds|]
==> P,C \<turnstile> Cs \<sqsubset>1 Ds"
| leq_pathSh: "[| Subobjs P C Cs; P \<turnstile> last Cs \<prec>S D |]
==> P,C \<turnstile> Cs \<sqsubset>1 [D]"
abbreviation
leq_path :: "prog => cname => [path, path] => bool" ("_,_ \<turnstile> _ \<sqsubseteq> _" [71,71,71] 70) where
"P,C \<turnstile> Cs \<sqsubseteq> Ds ≡ (Cs,Ds) ∈ (leq_path1 P C)*"
lemma leq_path_rep:
"[| Subobjs P C (Cs@[C']); Subobjs P C (Cs@[C',C''])|]
==> P,C \<turnstile> (Cs@[C']) \<sqsubset>1 (Cs@[C',C''])"
by(rule leq_pathRep,simp_all add:butlast_tail)
lemma leq_path_sh:
"[| Subobjs P C (Cs@[C']); P \<turnstile> C' \<prec>S C''|]
==> P,C \<turnstile> (Cs@[C']) \<sqsubset>1 [C'']"
by(erule leq_pathSh)simp
section{* Member lookups *}
constdefs
FieldDecls :: "prog => cname => vname => (path × ty) set"
"FieldDecls P C F ≡
{(Cs,T). Subobjs P C Cs ∧ (∃Bs fs ms. class P (last Cs) = Some(Bs,fs,ms)
∧ map_of fs F = Some T)}"
LeastFieldDecl :: "prog => cname => vname => ty => path => bool"
("_ \<turnstile> _ has least _:_ via _" [51,0,0,0,51] 50)
"P \<turnstile> C has least F:T via Cs ≡
(Cs,T) ∈ FieldDecls P C F ∧
(∀(Cs',T') ∈ FieldDecls P C F. P,C \<turnstile> Cs \<sqsubseteq> Cs')"
MethodDefs :: "prog => cname => mname => (path × method)set"
"MethodDefs P C M ≡
{(Cs,mthd). Subobjs P C Cs ∧ (∃Bs fs ms. class P (last Cs) = Some(Bs,fs,ms)
∧ map_of ms M = Some mthd)}"
-- "needed for well formed criterion"
HasMethodDef :: "prog => cname => mname => method => path => bool"
("_ \<turnstile> _ has _ = _ via _" [51,0,0,0,51] 50)
"P \<turnstile> C has M = mthd via Cs ≡ (Cs,mthd) ∈ MethodDefs P C M"
LeastMethodDef :: "prog => cname => mname => method => path => bool"
("_ \<turnstile> _ has least _ = _ via _" [51,0,0,0,51] 50)
"P \<turnstile> C has least M = mthd via Cs ≡
(Cs,mthd) ∈ MethodDefs P C M ∧
(∀(Cs',mthd') ∈ MethodDefs P C M. P,C \<turnstile> Cs \<sqsubseteq> Cs')"
MinimalMethodDefs :: "prog => cname => mname => (path × method)set"
"MinimalMethodDefs P C M ≡
{(Cs,mthd). (Cs,mthd) ∈ MethodDefs P C M ∧
(∀(Cs',mthd')∈ MethodDefs P C M. P,C \<turnstile> Cs' \<sqsubseteq> Cs --> Cs' = Cs)}"
OverriderMethodDefs :: "prog => subobj => mname => (path × method)set"
"OverriderMethodDefs P R M ≡
{(Cs,mthd). ∃Cs' mthd'. P \<turnstile> (ldc R) has least M = mthd' via Cs' ∧
(Cs,mthd) ∈ MinimalMethodDefs P (mdc R) M ∧
P,mdc R \<turnstile> Cs \<sqsubseteq> (snd R)@pCs'}"
FinalOverriderMethodDef :: "prog => subobj => mname => method => path => bool"
("_ \<turnstile> _ has overrider _ = _ via _" [51,0,0,0,51] 50)
"P \<turnstile> R has overrider M = mthd via Cs ≡
(Cs,mthd) ∈ OverriderMethodDefs P R M ∧
card(OverriderMethodDefs P R M) = 1"
inductive
SelectMethodDef :: "prog => cname => path => mname => method => path => bool"
("_ \<turnstile> '(_,_') selects _ = _ via _" [51,0,0,0,0,51] 50)
for P :: prog
where
dyn_unique:
"P \<turnstile> C has least M = mthd via Cs' ==> P \<turnstile> (C,Cs) selects M = mthd via Cs'"
| dyn_ambiguous:
"[|∀mthd Cs'. ¬ P \<turnstile> C has least M = mthd via Cs';
P \<turnstile> (C,Cs) has overrider M = mthd via Cs'|]
==> P \<turnstile> (C,Cs) selects M = mthd via Cs'"
lemma sees_fields_fun:
"(Cs,T) ∈ FieldDecls P C F ==> (Cs,T') ∈ FieldDecls P C F ==> T = T'"
by(fastsimp simp:FieldDecls_def)
lemma sees_field_fun:
"[|P \<turnstile> C has least F:T via Cs; P \<turnstile> C has least F:T' via Cs|]
==> T = T'"
by (fastsimp simp:LeastFieldDecl_def dest:sees_fields_fun)
lemma has_least_method_has_method:
"P \<turnstile> C has least M = mthd via Cs ==> P \<turnstile> C has M = mthd via Cs"
by (simp add:LeastMethodDef_def HasMethodDef_def)
lemma visible_methods_exist:
"(Cs,mthd) ∈ MethodDefs P C M ==>
(∃Bs fs ms. class P (last Cs) = Some(Bs,fs,ms) ∧ map_of ms M = Some mthd)"
by(auto simp:MethodDefs_def)
lemma sees_methods_fun:
"(Cs,mthd) ∈ MethodDefs P C M ==> (Cs,mthd') ∈ MethodDefs P C M ==> mthd = mthd'"
by(fastsimp simp:MethodDefs_def)
lemma sees_method_fun:
"[|P \<turnstile> C has least M = mthd via Cs; P \<turnstile> C has least M = mthd' via Cs|]
==> mthd = mthd'"
by (fastsimp simp:LeastMethodDef_def dest:sees_methods_fun)
lemma overrider_method_fun:
assumes overrider:"P \<turnstile> (C,Cs) has overrider M = mthd via Cs'"
and overrider':"P \<turnstile> (C,Cs) has overrider M = mthd' via Cs''"
shows "mthd = mthd' ∧ Cs' = Cs''"
proof -
from overrider' have omd:"(Cs'',mthd') ∈ OverriderMethodDefs P (C,Cs) M"
by(simp_all add:FinalOverriderMethodDef_def)
from overrider have "(Cs',mthd) ∈ OverriderMethodDefs P (C,Cs) M"
and "card(OverriderMethodDefs P (C,Cs) M) = 1"
by(simp_all add:FinalOverriderMethodDef_def)
hence "∀(Ds,mthd'') ∈ OverriderMethodDefs P (C,Cs) M. (Cs',mthd) = (Ds,mthd'')"
by(fastsimp simp:card_Suc_eq)
with omd show ?thesis by fastsimp
qed
end