(* Title: CoreC++ Author: Daniel Wasserrab Maintainer: Daniel Wasserrab <wasserra at fmi.uni-passau.de> *) section ‹Definition of Subobjects› theory SubObj imports ClassRel begin subsection ‹General definitions› type_synonym subobj = "cname × path" definition mdc :: "subobj ⇒ cname" where "mdc S = fst S" definition ldc :: "subobj ⇒ cname" where "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) subsection ‹Subobjects according to Rossie-Friedman› fun is_subobj :: "prog ⇒ subobj ⇒ bool" ― ‹legal subobject to class hierarchie› where "is_subobj P (C, []) ⟷ False" | "is_subobj P (C, [D]) ⟷ (is_class P C ∧ C = D) ∨ (∃ X. P ⊢ C ≼⇧^{*}X ∧ P ⊢ X ≺⇩_{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 ⊢ X ≺⇩_{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:if_split_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 ⊢ D ≺⇩_{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 ⊢ D ≺⇩_{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 ⊢ D ≺⇩_{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 ⊢ C ≼⇧^{*}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 ⊢ C ≼⇧^{*}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 ⊢ C ≼⇧^{*}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 ⊢ D ≺⇩_{R}C''" by (rule_tac Cs'="[]" in isSubobjs_subclsR) simp hence rel1:"P ⊢ D ≺⇧^{1}C''" by (rule subclsR_subcls1) from DDs have "D = last (C' # rev Cs'')" by simp with rel1 have lastrel1:"P ⊢ last (C' # rev Cs'') ≺⇧^{1}C''" by simp with rel have "P ⊢ C ≼⇧^{*}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 ⊢ mdc R ≼⇧^{*}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 ⊢ C ≼⇧^{*}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 ⊢ X ≺⇩_{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 ⊢ (last(butlast(D#E#Cs'))) ≺⇩_{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 ⊢ X ≺⇩_{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 ⊢ C ≼⇧^{*}X" by (drule_tac R="(C,Xs@[X])" in mdc_leq_ldc, simp add:mdc_def ldc_def) with classC 2 show ?thesis by fastforce qed text‹Auxiliary lemmas› lemma build_rec_isSubobj_rev: assumes 1:"is_subobj P ((D,D#rev Cs))" and 2:" P ⊢ C ≺⇩_{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 ⊢ X ≺⇩_{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 ⊢ last(D#rev Cs') ≺⇩_{R}C'" by (auto split:if_split_asm) with suboCD show ?case by simp qed lemma build_rec_isSubobj: assumes 1:"is_subobj P ((D,D#Cs))" and 2:" P ⊢ C ≺⇩_{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 moreover have "D # rev Cs' = butlast (D # rev Cs') @ [last (D # rev Cs')]" by (rule append_butlast_last_id [symmetric]) simp ultimately have 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 ⊢ C'' ≺⇩_{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 subsection ‹Subobject handling and lemmas› text‹Subobjects consisting of repeated inheritance relations only:› inductive Subobjs⇩_{R}:: "prog ⇒ cname ⇒ path ⇒ bool" for P :: prog where SubobjsR_Base: "is_class P C ⟹ Subobjs⇩_{R}P C [C]" | SubobjsR_Rep: "⟦P ⊢ C ≺⇩_{R}D; Subobjs⇩_{R}P D Cs⟧ ⟹ Subobjs⇩_{R}P C (C # Cs)" text‹All subobjects:› inductive Subobjs :: "prog ⇒ cname ⇒ path ⇒ bool" for P :: prog where Subobjs_Rep: "Subobjs⇩_{R}P C Cs ⟹ Subobjs P C Cs" | Subobjs_Sh: "⟦P ⊢ C ≼⇧^{*}C'; P ⊢ C' ≺⇩_{S}D; Subobjs⇩_{R}P D Cs⟧ ⟹ Subobjs P C Cs" lemma Subobjs_Base:"is_class P C ⟹ Subobjs P C [C]" by (fastforce intro:Subobjs_Rep SubobjsR_Base) lemma SubobjsR_nonempty: "Subobjs⇩_{R}P C Cs ⟹ Cs ≠ []" by (induct rule: Subobjs⇩_{R}.induct, simp_all) lemma Subobjs_nonempty: "Subobjs P C Cs ⟹ Cs ≠ []" by (erule Subobjs.induct)(erule SubobjsR_nonempty)+ lemma hd_SubobjsR: "Subobjs⇩_{R}P C Cs ⟹ ∃Cs'. Cs = C#Cs'" by(erule Subobjs⇩_{R}.induct,simp+) lemma SubobjsR_subclassRep: "Subobjs⇩_{R}P C Cs ⟹ (C,last Cs) ∈ (subclsR P)⇧^{*}" apply(erule Subobjs⇩_{R}.induct) apply simp apply(simp add: SubobjsR_nonempty) done lemma SubobjsR_subclass: "Subobjs⇩_{R}P C Cs ⟹ P ⊢ C ≼⇧^{*}last Cs" apply(erule Subobjs⇩_{R}.induct) apply simp apply(simp add: SubobjsR_nonempty) apply(blast intro:subclsR_subcls1 rtrancl_trans) done lemma Subobjs_subclass: "Subobjs P C Cs ⟹ P ⊢ C ≼⇧^{*}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; ¬ Subobjs⇩_{R}P C Cs⟧ ⟹ ∃C' D. P ⊢ C ≼⇧^{*}C' ∧ P ⊢ C' ≺⇩_{S}D ∧ Subobjs⇩_{R}P D Cs" apply (induct rule: Subobjs.induct) apply clarsimp apply fastforce done lemma assumes subo:"Subobjs⇩_{R}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,fastforce intro:Subobjs_Rep) next case (Cons D Ds) have subo':"Subobjs⇩_{R}P (hd ((D#Ds) @ C'#Cs')) ((D#Ds) @ C'#Cs')" and IH:"Subobjs⇩_{R}P (hd (Ds @ C'#Cs')) (Ds @ C'#Cs') ⟹ Subobjs P C' (C'#Cs')" by fact+ from subo' have "Subobjs⇩_{R}P (hd (Ds @ C' # Cs')) (Ds @ C' # Cs')" apply - apply (drule Subobjs⇩_{R}.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 (fastforce intro:SubobjsR_Subobjs) apply (fastforce dest:hd_SubobjsR) apply (subgoal_tac "D = hd(Cs @ C' # Cs')") apply (fastforce intro:SubobjsR_Subobjs) apply (fastforce dest:hd_SubobjsR) done lemma SubobjsR_isClass: assumes subo:"Subobjs⇩_{R}P C Cs" shows "is_class P C" using subo proof (induct rule:Subobjs⇩_{R}.induct) case SubobjsR_Base thus ?case by assumption next case SubobjsR_Rep thus ?case by (fastforce 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 ⊢ C ≼⇧^{*}C'" and leqS:"P ⊢ C' ≺⇩_{S}D" by fact+ hence "(C,D) ∈ (subcls1 P)⇧^{+}" by (fastforce intro:rtrancl_into_trancl1 subclsS_subcls1) thus ?case by (induct rule:trancl_induct, fastforce intro:subcls1_class) qed lemma Subobjs_subclsR: assumes subo:"Subobjs P C (Cs@[D,D']@Cs')" shows "P ⊢ D ≺⇩_{R}D'" using subo proof - from subo have "Subobjs P D (D#D'#Cs')" by -(rule Subobjs_Subobjs,simp) then obtain C' where subo':"Subobjs⇩_{R}P C' (D#D'#Cs')" by (induct rule:Subobjs.induct,blast+) hence "C' = D" by -(drule hd_SubobjsR,simp) with subo' have "Subobjs⇩_{R}P D (D#D'#Cs')" by simp thus ?thesis by (fastforce elim:Subobjs⇩_{R}.cases dest:hd_SubobjsR) qed lemma assumes subo:"Subobjs⇩_{R}P (hd Cs) (Cs@[D])" and notempty:"Cs ≠ []" shows butlast_Subobjs_Rep:"Subobjs⇩_{R}P (hd Cs) Cs" using subo notempty proof (induct Cs) case Nil thus ?case by simp next case (Cons C' Cs') have subo:"Subobjs⇩_{R}P (hd(C'#Cs')) ((C'#Cs')@[D])" and IH:"⟦Subobjs⇩_{R}P (hd Cs') (Cs'@[D]); Cs' ≠ []⟧ ⟹ Subobjs⇩_{R}P (hd Cs') Cs'" by fact+ from subo have subo':"Subobjs⇩_{R}P C' (C'#Cs'@[D])" by simp show ?case proof (cases "Cs' = []") case True with subo' have "Subobjs⇩_{R}P C' [C',D]" by simp hence "is_class P C'" by(rule SubobjsR_isClass) hence "Subobjs⇩_{R}P C' [C']" by (rule SubobjsR_Base) with True show ?thesis by simp next case False with subo' obtain D' where subo'':"Subobjs⇩_{R}P D' (Cs'@[D])" and subR:"P ⊢ C' ≺⇩_{R}D'" by (auto elim:Subobjs⇩_{R}.cases) from False subo'' have hd:"D' = hd Cs'" by (induct Cs',auto dest:hd_SubobjsR) with subo'' False IH have "Subobjs⇩_{R}P (hd Cs') Cs'" by simp with subR hd have "Subobjs⇩_{R}P C' (C'#Cs')" by (fastforce 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:"Subobjs⇩_{R}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 "Subobjs⇩_{R}P (hd Cs) Cs" by(fastforce intro:butlast_Subobjs_Rep) with hd show "Subobjs P C Cs" by (fastforce intro:Subobjs_Rep) next fix C' D' assume leq:"P ⊢ C ≼⇧^{*}C'" and subS:"P ⊢ C' ≺⇩_{S}D'" and suboR:"Subobjs⇩_{R}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 "Subobjs⇩_{R}P (hd Cs) Cs" by(fastforce intro:butlast_Subobjs_Rep) with hd leq subS show "Subobjs P C Cs" by(fastforce 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 (fastforce 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: "Subobjs⇩_{R}P C Cs ⟹ is_subobj P ((C,Cs))" by(erule Subobjs⇩_{R}.induct,simp, auto dest:hd_SubobjsR intro:build_rec_isSubobj) lemma leq_SubobjsR_isSubobj: "⟦P ⊢ C ≼⇧^{*}C'; P ⊢ C' ≺⇩_{S}D; Subobjs⇩_{R}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) subsection ‹Paths› subsection ‹Appending paths› text‹Avoided name clash by calling one path Path.› definition path_via :: "prog ⇒ cname ⇒ cname ⇒ path ⇒ bool" ("_ ⊢ Path _ to _ via _ " [51,51,51,51] 50) where "P ⊢ Path C to D via Cs ≡ Subobjs P C Cs ∧ last Cs = D" definition path_unique :: "prog ⇒ cname ⇒ cname ⇒ bool" ("_ ⊢ Path _ to _ unique" [51,51,51] 50) where "P ⊢ Path C to D unique ≡ ∃!Cs. Subobjs P C Cs ∧ last Cs = D" definition appendPath :: "path ⇒ path ⇒ path" (infixr "@⇩_{p}" 65) where "Cs @⇩_{p}Cs' ≡ if (last Cs = hd Cs') then Cs @ (tl Cs') else Cs'" lemma appendPath_last: "Cs ≠ [] ⟹ last Cs = last (Cs'@⇩_{p}Cs)" by(auto simp:appendPath_def last_append)(cases Cs, simp_all)+ inductive casts_to :: "prog ⇒ ty ⇒ val ⇒ val ⇒ bool" ("_ ⊢ _ casts _ to _ " [51,51,51,51] 50) for P :: prog where casts_prim: "∀C. T ≠ Class C ⟹ P ⊢ T casts v to v" | casts_null: "P ⊢ Class C casts Null to Null" | casts_ref: "⟦ P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩_{p}Cs' ⟧ ⟹ P ⊢ Class C casts Ref(a,Cs) to Ref(a,Ds)" inductive Casts_to :: "prog ⇒ ty list ⇒ val list ⇒ val list ⇒ bool" ("_ ⊢ _ Casts _ to _ " [51,51,51,51] 50) for P :: prog where Casts_Nil: "P ⊢ [] Casts [] to []" | Casts_Cons: "⟦ P ⊢ T casts v to v'; P ⊢ Ts Casts vs to vs' ⟧ ⟹ P ⊢ (T#Ts) Casts (v#vs) to (v'#vs')" lemma length_Casts_vs: "P ⊢ Ts Casts vs to vs' ⟹ length Ts = length vs" by (induct rule:Casts_to.induct,simp_all) lemma length_Casts_vs': "P ⊢ 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" ("_,_ ⊢ _ ⊏⇧^{1}_" [71,71,71] 70) for P :: prog and C :: cname where "P,C ⊢ Cs ⊏⇧^{1}Ds ≡ (Cs,Ds) ∈ leq_path1 P C" | leq_pathRep: "⟦ Subobjs P C Cs; Subobjs P C Ds; Cs = butlast Ds⟧ ⟹ P,C ⊢ Cs ⊏⇧^{1}Ds" | leq_pathSh: "⟦ Subobjs P C Cs; P ⊢ last Cs ≺⇩_{S}D ⟧ ⟹ P,C ⊢ Cs ⊏⇧^{1}[D]" abbreviation leq_path :: "prog ⇒ cname ⇒ [path, path] ⇒ bool" ("_,_ ⊢ _ ⊑ _" [71,71,71] 70) where "P,C ⊢ Cs ⊑ Ds ≡ (Cs,Ds) ∈ (leq_path1 P C)⇧^{*}" lemma leq_path_rep: "⟦ Subobjs P C (Cs@[C']); Subobjs P C (Cs@[C',C''])⟧ ⟹ P,C ⊢ (Cs@[C']) ⊏⇧^{1}(Cs@[C',C''])" by(rule leq_pathRep,simp_all add:butlast_tail) lemma leq_path_sh: "⟦ Subobjs P C (Cs@[C']); P ⊢ C' ≺⇩_{S}C''⟧ ⟹ P,C ⊢ (Cs@[C']) ⊏⇧^{1}[C'']" by(erule leq_pathSh)simp subsection‹Member lookups› definition FieldDecls :: "prog ⇒ cname ⇒ vname ⇒ (path × ty) set" where "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)}" definition LeastFieldDecl :: "prog ⇒ cname ⇒ vname ⇒ ty ⇒ path ⇒ bool" ("_ ⊢ _ has least _:_ via _" [51,0,0,0,51] 50) where "P ⊢ C has least F:T via Cs ≡ (Cs,T) ∈ FieldDecls P C F ∧ (∀(Cs',T') ∈ FieldDecls P C F. P,C ⊢ Cs ⊑ Cs')" definition MethodDefs :: "prog ⇒ cname ⇒ mname ⇒ (path × method)set" where "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› definition HasMethodDef :: "prog ⇒ cname ⇒ mname ⇒ method ⇒ path ⇒ bool" ("_ ⊢ _ has _ = _ via _" [51,0,0,0,51] 50) where "P ⊢ C has M = mthd via Cs ≡ (Cs,mthd) ∈ MethodDefs P C M" definition LeastMethodDef :: "prog ⇒ cname ⇒ mname ⇒ method ⇒ path ⇒ bool" ("_ ⊢ _ has least _ = _ via _" [51,0,0,0,51] 50) where "P ⊢ C has least M = mthd via Cs ≡ (Cs,mthd) ∈ MethodDefs P C M ∧ (∀(Cs',mthd') ∈ MethodDefs P C M. P,C ⊢ Cs ⊑ Cs')" definition MinimalMethodDefs :: "prog ⇒ cname ⇒ mname ⇒ (path × method)set" where "MinimalMethodDefs P C M ≡ {(Cs,mthd). (Cs,mthd) ∈ MethodDefs P C M ∧ (∀(Cs',mthd')∈ MethodDefs P C M. P,C ⊢ Cs' ⊑ Cs ⟶ Cs' = Cs)}" definition OverriderMethodDefs :: "prog ⇒ subobj ⇒ mname ⇒ (path × method)set" where "OverriderMethodDefs P R M ≡ {(Cs,mthd). ∃Cs' mthd'. P ⊢ (ldc R) has least M = mthd' via Cs' ∧ (Cs,mthd) ∈ MinimalMethodDefs P (mdc R) M ∧ P,mdc R ⊢ Cs ⊑ (snd R)@⇩_{p}Cs'}" definition FinalOverriderMethodDef :: "prog ⇒ subobj ⇒ mname ⇒ method ⇒ path ⇒ bool" ("_ ⊢ _ has overrider _ = _ via _" [51,0,0,0,51] 50) where "P ⊢ R has overrider M = mthd via Cs ≡ (Cs,mthd) ∈ OverriderMethodDefs P R M ∧ card(OverriderMethodDefs P R M) = 1" (*(∀(Cs',mthd') ∈ OverriderMethodDefs P R M. Cs = Cs' ∧ mthd = mthd')"*) inductive SelectMethodDef :: "prog ⇒ cname ⇒ path ⇒ mname ⇒ method ⇒ path ⇒ bool" ("_ ⊢ '(_,_') selects _ = _ via _" [51,0,0,0,0,51] 50) for P :: prog where dyn_unique: "P ⊢ C has least M = mthd via Cs' ⟹ P ⊢ (C,Cs) selects M = mthd via Cs'" | dyn_ambiguous: "⟦∀mthd Cs'. ¬ P ⊢ C has least M = mthd via Cs'; P ⊢ (C,Cs) has overrider M = mthd via Cs'⟧ ⟹ P ⊢ (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(fastforce simp:FieldDecls_def) lemma sees_field_fun: "⟦P ⊢ C has least F:T via Cs; P ⊢ C has least F:T' via Cs⟧ ⟹ T = T'" by (fastforce simp:LeastFieldDecl_def dest:sees_fields_fun) lemma has_least_method_has_method: "P ⊢ C has least M = mthd via Cs ⟹ P ⊢ 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(fastforce simp:MethodDefs_def) lemma sees_method_fun: "⟦P ⊢ C has least M = mthd via Cs; P ⊢ C has least M = mthd' via Cs⟧ ⟹ mthd = mthd'" by (fastforce simp:LeastMethodDef_def dest:sees_methods_fun) lemma overrider_method_fun: assumes overrider:"P ⊢ (C,Cs) has overrider M = mthd via Cs'" and overrider':"P ⊢ (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(fastforce simp:card_Suc_eq) with omd show ?thesis by fastforce qed end