header {* \isaheader{Generic Well-formedness of programs} *}
theory WellForm imports SystemClasses TypeRel WellType begin
text {*\noindent This theory defines global well-formedness conditions
for programs but does not look inside method bodies. Well-typing of
expressions is defined elsewhere (in theory @{text WellType}).
CoreC++ allows covariant return types *}
types wf_mdecl_test = "prog => cname => mdecl => bool"
constdefs
wf_fdecl :: "prog => fdecl => bool"
"wf_fdecl P ≡ λ(F,T). is_type P T"
wf_mdecl :: "wf_mdecl_test => wf_mdecl_test"
"wf_mdecl wf_md P C ≡ λ(M,Ts,T,mb).
(∀T∈set Ts. is_type P T) ∧ is_type P T ∧ T ≠ NT ∧ wf_md P C (M,Ts,T,mb)"
wf_cdecl :: "wf_mdecl_test => prog => cdecl => bool"
"wf_cdecl wf_md P ≡ λ(C,(Bs,fs,ms)).
(∀M mthd Cs. P \<turnstile> C has M = mthd via Cs -->
(∃mthd' Cs'. P \<turnstile> (C,Cs) has overrider M = mthd' via Cs')) ∧
(∀f∈set fs. wf_fdecl P f) ∧ distinct_fst fs ∧
(∀m∈set ms. wf_mdecl wf_md P C m) ∧ distinct_fst ms ∧
(∀D ∈ baseClasses Bs.
is_class P D ∧ ¬ P \<turnstile> D \<preceq>* C ∧
(∀(M,Ts,T,m)∈set ms.
∀Ts' T' m' Cs. P \<turnstile> D has M = (Ts',T',m') via Cs -->
Ts' = Ts ∧ P \<turnstile> T ≤ T'))"
wf_syscls :: "prog => bool"
"wf_syscls P ≡ sys_xcpts ⊆ set(map fst P)"
wf_prog :: "wf_mdecl_test => prog => bool"
"wf_prog wf_md P ≡ wf_syscls P ∧ distinct_fst P ∧
(∀c ∈ set P. wf_cdecl wf_md P c)"
section{* Well-formedness lemmas *}
lemma class_wf:
"[|class P C = Some c; wf_prog wf_md P|] ==> wf_cdecl wf_md P (C,c)"
apply (unfold wf_prog_def class_def)
apply (fast dest: map_of_SomeD)
done
lemma is_class_xcpt:
"[| C ∈ sys_xcpts; wf_prog wf_md P |] ==> is_class P C"
apply (simp add: wf_prog_def wf_syscls_def is_class_def class_def)
apply (fastsimp intro!: map_of_SomeI)
done
lemma is_type_pTs:
assumes "wf_prog wf_md P" and "(C,S,fs,ms) ∈ set P" and "(M,Ts,T,m) ∈ set ms"
shows "set Ts ⊆ types P"
proof
from prems have "wf_mdecl wf_md P C (M,Ts,T,m)"
by (unfold wf_prog_def wf_cdecl_def) auto
hence "∀t ∈ set Ts. is_type P t" by (unfold wf_mdecl_def) auto
moreover fix t assume "t ∈ set Ts"
ultimately have "is_type P t" by blast
thus "t ∈ types P" ..
qed
section{* Well-formedness subclass lemmas *}
lemma subcls1_wfD:
"[| P \<turnstile> C \<prec>1 D; wf_prog wf_md P |] ==> D ≠ C ∧ (D,C) ∉ (subcls1 P)+"
apply( frule r_into_trancl)
apply( drule subcls1D)
apply(clarify)
apply( drule (1) class_wf)
apply( unfold wf_cdecl_def baseClasses_def)
apply(force simp add: reflcl_trancl [THEN sym] simp del: reflcl_trancl)
done
lemma wf_cdecl_supD:
"[|wf_cdecl wf_md P (C,Bs,r); D ∈ baseClasses Bs|] ==> is_class P D"
by (auto simp: wf_cdecl_def baseClasses_def)
lemma subcls_asym:
"[| wf_prog wf_md P; (C,D) ∈ (subcls1 P)+ |] ==> (D,C) ∉ (subcls1 P)+"
apply(erule trancl.cases)
apply(fast dest!: subcls1_wfD )
apply(fast dest!: subcls1_wfD intro: trancl_trans)
done
lemma subcls_irrefl:
"[| wf_prog wf_md P; (C,D) ∈ (subcls1 P)+ |] ==> C ≠ D"
apply (erule trancl_trans_induct)
apply (auto dest: subcls1_wfD subcls_asym)
done
lemma subcls_asym2:
"[| (C,D) ∈ (subcls1 P)*; wf_prog wf_md P; (D,C) ∈ (subcls1 P)* |] ==> C = D"
apply (induct rule:rtrancl.induct)
apply simp
apply (drule rtrancl_into_trancl1)
apply simp
apply (drule subcls_asym)
apply simp
apply(drule rtranclD)
apply simp
done
lemma acyclic_subcls1:
"wf_prog wf_md P ==> acyclic (subcls1 P)"
apply (unfold acyclic_def)
apply (fast dest: subcls_irrefl)
done
lemma wf_subcls1:
"wf_prog wf_md P ==> wf ((subcls1 P)¯)"
apply (rule finite_acyclic_wf_converse)
apply (rule finite_subcls1)
apply (erule acyclic_subcls1)
done
lemma subcls_induct:
"[| wf_prog wf_md P; !!C. ∀D. (C,D) ∈ (subcls1 P)+ --> Q D ==> Q C |] ==> Q C"
(is "?A ==> PROP ?P ==> _")
proof -
assume p: "PROP ?P"
assume ?A thus ?thesis apply -
apply(drule wf_subcls1)
apply(drule wf_trancl)
apply(simp only: trancl_converse)
apply(erule_tac a = C in wf_induct)
apply(rule p)
apply(auto)
done
qed
section{* Well-formedness leq\_path lemmas *}
lemma last_leq_path:
assumes leq:"P,C \<turnstile> Cs \<sqsubset>1 Ds" and wf:"wf_prog wf_md P"
shows "P \<turnstile> last Cs \<prec>1 last Ds"
using leq
proof (induct rule:leq_path1.induct)
fix Cs Ds assume suboCs:"Subobjs P C Cs" and suboDs:"Subobjs P C Ds"
and butlast:"Cs = butlast Ds"
from suboDs have notempty:"Ds ≠ []" by -(drule Subobjs_nonempty)
with butlast have DsCs:"Ds = Cs @ [last Ds]" by simp
from suboCs have notempty:"Cs ≠ []" by -(drule Subobjs_nonempty)
with DsCs have "Ds = ((butlast Cs) @ [last Cs]) @ [last Ds]" by simp
with suboDs have "Subobjs P C ((butlast Cs) @ [last Cs,last Ds])"
by simp
thus "P \<turnstile> last Cs \<prec>1 last Ds" by (fastsimp intro:subclsR_subcls1 Subobjs_subclsR)
next
fix Cs D assume "P \<turnstile> last Cs \<prec>S D"
thus "P \<turnstile> last Cs \<prec>1 last [D]" by (fastsimp intro:subclsS_subcls1)
qed
lemma last_leq_paths:
assumes leq:"(Cs,Ds) ∈ (leq_path1 P C)+" and wf:"wf_prog wf_md P"
shows "(last Cs,last Ds) ∈ (subcls1 P)+"
using leq
proof (induct rule:trancl.induct)
fix Cs Ds assume "P,C \<turnstile> Cs \<sqsubset>1 Ds"
thus "(last Cs, last Ds) ∈ (subcls1 P)+" using wf
by (fastsimp intro:r_into_trancl elim:last_leq_path)
next
fix Cs Cs' Ds assume "(last Cs, last Cs') ∈ (subcls1 P)+"
and "P,C \<turnstile> Cs' \<sqsubset>1 Ds"
thus "(last Cs, last Ds) ∈ (subcls1 P)+" using wf
by (fastsimp dest:last_leq_path)
qed
lemma leq_path1_wfD:
"[| P,C \<turnstile> Cs \<sqsubset>1 Cs'; wf_prog wf_md P |] ==> Cs ≠ Cs' ∧ (Cs',Cs) ∉ (leq_path1 P C)+"
apply (rule conjI)
apply (erule leq_path1.cases)
apply simp
apply (drule_tac Cs="Ds" in Subobjs_nonempty)
apply (rule butlast_noteq) apply assumption
apply clarsimp
apply (drule subclsS_subcls1)
apply (drule subcls1_wfD) apply simp_all
apply clarsimp
apply (frule last_leq_path)
apply simp
apply (drule last_leq_paths)
apply simp
apply (drule_tac r="subcls1 P" in r_into_trancl)
apply (drule subcls_asym)
apply auto
done
lemma leq_path_asym:
"[|(Cs,Cs') ∈ (leq_path1 P C)+; wf_prog wf_md P|] ==> (Cs',Cs) ∉ (leq_path1 P C)+"
apply(erule tranclE)
apply(fast dest!:leq_path1_wfD )
apply(fast dest!:leq_path1_wfD intro: trancl_trans)
done
lemma leq_path_asym2:"[|P,C \<turnstile> Cs \<sqsubseteq> Cs'; P,C \<turnstile> Cs' \<sqsubseteq> Cs; wf_prog wf_md P|] ==> Cs = Cs'"
apply (induct rule:rtrancl.induct)
apply simp
apply (drule rtrancl_into_trancl1)
apply simp
apply (drule leq_path_asym)
apply simp
apply (drule_tac a="c" and b="a" in rtranclD)
apply simp
done
lemma leq_path_Subobjs:
"[|P,C \<turnstile> [C] \<sqsubseteq> Cs; is_class P C; wf_prog wf_md P|] ==> Subobjs P C Cs"
by (induct rule:rtrancl_induct,auto intro:Subobjs_Base elim!:leq_path1.cases,
auto dest!:Subobjs_subclass intro!:Subobjs_Sh SubobjsR_Base dest!:subclsSD
intro:wf_cdecl_supD class_wf ShBaseclass_isBaseclass subclsSI)
section{* Lemmas concerning Subobjs *}
lemma Subobj_last_isClass:"[|wf_prog wf_md P; Subobjs P C Cs|] ==> is_class P (last Cs)"
apply (frule Subobjs_isClass)
apply (drule Subobjs_subclass)
apply (drule rtranclD)
apply (erule disjE)
apply simp
apply clarsimp
apply (erule trancl_induct)
apply (fastsimp dest:subcls1D class_wf elim:wf_cdecl_supD)
apply (fastsimp dest:subcls1D class_wf elim:wf_cdecl_supD)
done
lemma converse_SubobjsR_Rep:
"[|SubobjsR P C Cs; P \<turnstile> last Cs \<prec>R C'; wf_prog wf_md P|]
==> SubobjsR P C (Cs@[C'])"
apply (induct rule:SubobjsR.induct)
apply (frule subclsR_subcls1)
apply (fastsimp dest!:subcls1D class_wf wf_cdecl_supD SubobjsR_Base SubobjsR_Rep)
apply (fastsimp elim:SubobjsR_Rep simp: SubobjsR_nonempty split:split_if_asm)
done
lemma converse_Subobjs_Rep:
"[|Subobjs P C Cs; P \<turnstile> last Cs \<prec>R C'; wf_prog wf_md P|]
==> Subobjs P C (Cs@[C'])"
by (induct rule:Subobjs.induct, fastsimp dest:converse_SubobjsR_Rep Subobjs_Rep,
fastsimp dest:converse_SubobjsR_Rep Subobjs_Sh)
lemma isSubobj_Subobjs_rev:
assumes subo:"is_subobj(P,(C,C'#rev Cs'))" and wf:"wf_prog wf_md P"
shows "Subobjs P C (C'#rev Cs')"
using subo
proof (induct Cs')
case Nil
show ?case
proof (cases "C=C'")
case True
have "is_subobj (P,(C,C'#rev []))" by fact
with True have "is_subobj (P,(C,[C]))" by simp
hence "is_class P C"
by (fastsimp elim:converse_rtranclE dest:subclsS_subcls1 elim:subcls1_class)
with True show ?thesis by (fastsimp intro:Subobjs_Base)
next
case False
have "is_subobj (P,(C,C'#rev []))" by fact
with False obtain D where sup:"P \<turnstile> C \<preceq>* D" and subS:"P \<turnstile> D \<prec>S C'"
by fastsimp
with wf have "is_class P C'"
by (fastsimp dest:subclsS_subcls1 subcls1D class_wf elim:wf_cdecl_supD)
hence "SubobjsR P C' [C']" by (fastsimp elim:SubobjsR_Base)
with sup subS have "Subobjs P C [C']" by -(erule Subobjs_Sh, simp)
thus ?thesis by simp
qed
next
case (Cons C'' Cs'')
have IH:"is_subobj (P,(C,C'#rev Cs'')) ==> Subobjs P C (C'#rev Cs'')"
and subo:"is_subobj (P,(C,C'#rev(C''# Cs'')))" by fact+
obtain Ds' where Ds':"Ds' = rev Cs''" by simp
obtain D Ds where DDs:"D#Ds = Ds'@[C'']" by (cases Ds') auto
with Ds' subo have "is_subobj(P,(C,C'#D#Ds))" by simp
hence subobl:"is_subobj(P,(C,butlast(C'#D#Ds)))"
and subRbl:"P \<turnstile> last(butlast(C'#D#Ds)) \<prec>R last(C'#D#Ds)" by simp+
with DDs Ds' have "is_subobj(P,(C,C'#rev Cs''))" by (simp del:is_subobj.simps)
with IH have suborev:"Subobjs P C (C'#rev Cs'')" by simp
from subRbl DDs Ds' have subR:"P \<turnstile> last(C'#rev Cs'') \<prec>R C''" by simp
with suborev wf show ?case by (fastsimp dest:converse_Subobjs_Rep)
qed
lemma isSubobj_Subobjs:
assumes subo:"is_subobj(P,(C,Cs))" and wf:"wf_prog wf_md P"
shows "Subobjs P C Cs"
using subo
proof (induct Cs)
case Nil
thus ?case by simp
next
case (Cons C' Cs')
have subo:"is_subobj(P,(C,C'#Cs'))" by fact
obtain Cs'' where Cs'':"Cs'' = rev Cs'" by simp
with subo have "is_subobj(P,(C,C'#rev Cs''))" by simp
with wf have "Subobjs P C (C'#rev Cs'')" by - (rule isSubobj_Subobjs_rev)
with Cs'' show ?case by simp
qed
lemma isSubobj_eq_Subobjs:
"wf_prog wf_md P ==> is_subobj(P,(C,Cs)) = (Subobjs P C Cs)"
by(auto elim:isSubobj_Subobjs Subobjs_isSubobj)
lemma subo_trans_subcls:
assumes subo:"Subobjs P C (Cs@ C'#rev Cs')"
shows "∀C'' ∈ set Cs'. (C',C'') ∈ (subcls1 P)+"
using subo
proof (induct Cs')
case Nil
thus ?case by simp
next
case (Cons D Ds)
have IH:"Subobjs P C (Cs @ C' # rev Ds) ==>
∀C''∈set Ds. (C', C'') ∈ (subcls1 P)+"
and "Subobjs P C (Cs @ C' # rev (D # Ds))" by fact+
hence subo':"Subobjs P C (Cs@ C'#rev Ds @ [D])" by simp
hence "Subobjs P C (Cs@ C'#rev Ds)"
by -(rule appendSubobj,simp_all)
with IH have set:"∀C''∈set Ds. (C', C'') ∈ (subcls1 P)+" by simp
hence revset:"∀C''∈set (rev Ds). (C', C'') ∈ (subcls1 P)+" by simp
have "(C',D) ∈ (subcls1 P)+"
proof (cases "Ds = []")
case True
with subo' have "Subobjs P C (Cs@[C',D])" by simp
thus ?thesis
by (fastsimp intro: subclsR_subcls1 Subobjs_subclsR)
next
case False
with revset have hd:"(C',hd Ds) ∈ (subcls1 P)+"
apply -
apply (erule ballE)
apply simp
apply (simp add:in_set_conv_decomp)
apply (erule_tac x="[]" in allE)
apply (erule_tac x="tl Ds" in allE)
apply simp
done
from False subo' have "(hd Ds,D) ∈ (subcls1 P)+"
apply (cases Ds)
apply simp
apply simp
apply (rule r_into_trancl)
apply (rule subclsR_subcls1)
apply (rule_tac Cs="Cs @ C' # rev list" in Subobjs_subclsR)
apply simp
done
with hd show ?thesis by (rule trancl_trans)
qed
with set show ?case by simp
qed
lemma unique1:
assumes subo:"Subobjs P C (Cs@ C'#Cs')" and wf:"wf_prog wf_md P"
shows "C' ∉ set Cs'"
proof -
obtain Ds where Ds:"Ds = rev Cs'" by simp
with subo have "Subobjs P C (Cs@ C'#rev Ds)" by simp
with Ds subo have "∀C'' ∈ set Cs'. (C',C'') ∈ (subcls1 P)+"
by (fastsimp dest:subo_trans_subcls)
with wf have "∀C'' ∈ set Cs'. C' ≠ C''"
by (auto dest:subcls_irrefl)
thus ?thesis by fastsimp
qed
lemma subo_subcls_trans:
assumes subo:"Subobjs P C (Cs@ C'#Cs')"
shows "∀C'' ∈ set Cs. (C'',C') ∈ (subcls1 P)+"
proof -
from wf subo have "!!C''. C'' ∈ set Cs ==> (C'',C') ∈ (subcls1 P)+"
apply (auto simp:in_set_conv_decomp)
apply (case_tac zs)
apply (fastsimp intro: subclsR_subcls1 Subobjs_subclsR)
apply simp
apply (rule_tac b="a" in trancl_rtrancl_trancl)
apply (fastsimp intro: subclsR_subcls1 Subobjs_subclsR)
apply (subgoal_tac "P \<turnstile> a \<preceq>* last (a # list @ [C'])")
apply simp
apply (rule Subobjs_subclass)
apply (rule_tac C="C" and Cs=" ys @[C'']" in Subobjs_Subobjs)
apply (rule_tac Cs'="Cs'" in appendSubobj)
apply simp_all
done
thus ?thesis by fastsimp
qed
lemma unique2:
assumes subo:"Subobjs P C (Cs@ C'#Cs')" and wf:"wf_prog wf_md P"
shows "C' ∉ set Cs"
proof -
from subo wf have "∀C'' ∈ set Cs. (C'',C') ∈ (subcls1 P)+"
by (fastsimp dest:subo_subcls_trans)
with wf have "∀C'' ∈ set Cs. C' ≠ C''"
by (auto dest:subcls_irrefl)
thus ?thesis by fastsimp
qed
lemma mdc_hd_path:
assumes subo:"Subobjs P C Cs" and set:"C ∈ set Cs" and wf:"wf_prog wf_md P"
shows "C = hd Cs"
proof -
from subo set obtain Ds Ds' where Cs:"Cs = Ds@ C#Ds'"
by (auto simp:in_set_conv_decomp)
then obtain Cs' where Cs':"Cs' = rev Ds" by simp
with Cs subo have subo':"Subobjs P C ((rev Cs')@ C#Ds')" by simp
thus ?thesis
proof (cases Cs')
case Nil
with Cs Cs' show ?thesis by simp
next
case (Cons X Xs)
with subo' have suboX:"Subobjs P C ((rev Xs)@[X,C]@Ds')" by simp
hence leq:"P \<turnstile> X \<prec>1 C"
by (fastsimp intro:subclsR_subcls1 Subobjs_subclsR)
from suboX wf have "P \<turnstile> C \<preceq>* last ((rev Xs)@[X])"
by (fastsimp intro:Subobjs_subclass appendSubobj)
with leq have "(C,C) ∈ (subcls1 P)+" by simp
with wf show ?thesis by (fastsimp dest:subcls_irrefl)
qed
qed
lemma mdc_eq_last:
assumes subo:"Subobjs P C Cs" and last:"last Cs = C" and wf:"wf_prog wf_md P"
shows "Cs = [C]"
proof -
from subo have notempty:"Cs ≠ []" by - (drule Subobjs_nonempty)
hence lastset:"last Cs ∈ set Cs"
apply (auto simp add:in_set_conv_decomp)
apply (rule_tac x="butlast Cs" in exI)
apply (rule_tac x="[]" in exI)
apply simp
done
with last have C:"C ∈ set Cs" by simp
with subo wf have hd:"C = hd Cs" by -(rule mdc_hd_path)
then obtain Cs' where Cs':"Cs' = tl Cs" by simp
thus ?thesis
proof (cases Cs')
case Nil
with hd subo Cs' show ?thesis by (fastsimp dest:Subobjs_nonempty hd_Cons_tl)
next
case (Cons D Ds)
with Cs' hd notempty have Cs:"Cs=C#D#Ds" by simp
with subo have "Subobjs P C (C#D#Ds)" by simp
with wf have notset:"C ∉ set (D#Ds)" by -(rule_tac Cs="[]" in unique1,simp_all)
from Cs last have "last Cs = last (D#Ds)" by simp
hence "last Cs ∈ set (D#Ds)"
apply (auto simp add:in_set_conv_decomp)
apply (erule_tac x="butlast Ds" in allE)
apply (erule_tac x="[]" in allE)
apply simp
done
with last have "C ∈ set (D#Ds)" by simp
with notset show ?thesis by simp
qed
qed
lemma assumes leq:"P \<turnstile> C \<preceq>* D" and wf:"wf_prog wf_md P"
shows subcls_leq_path:"∃Cs. P,C \<turnstile> [C] \<sqsubseteq> Cs@[D]"
using leq
proof (induct rule:rtrancl.induct)
fix C show "∃Cs. P,C \<turnstile> [C] \<sqsubseteq> Cs@[C]" by (rule_tac x="[]" in exI,simp)
next
fix C C' D assume leq':"P \<turnstile> C \<preceq>* C'" and IH:"∃Cs. P,C \<turnstile> [C] \<sqsubseteq> Cs@[C']"
and sub:"P \<turnstile> C' \<prec>1 D"
from sub have "is_class P C'" by (rule subcls1_class)
with leq' have "class": "is_class P C" by (rule subcls_is_class)
from IH obtain Cs where steps:"P,C \<turnstile> [C] \<sqsubseteq> Cs@[C']" by auto
hence subo:"Subobjs P C (Cs@[C'])" using "class" wf
by (fastsimp intro:leq_path_Subobjs)
{ assume "P \<turnstile> C' \<prec>R D"
with subo wf have "Subobjs P C (Cs@[C',D])"
by (fastsimp dest:converse_Subobjs_Rep)
with subo have "P,C \<turnstile> (Cs@[C']) \<sqsubset>1 (Cs@[C']@[D])"
by (fastsimp intro:leq_path_rep) }
moreover
{ assume "P \<turnstile> C' \<prec>S D"
with subo have "P,C \<turnstile> (Cs@[C']) \<sqsubset>1 [D]" by (rule leq_path_sh) }
ultimately show "∃Cs. P,C \<turnstile> [C] \<sqsubseteq> Cs@[D]" using sub steps
apply (auto dest!:subcls1_subclsR_or_subclsS)
apply (rule_tac x="Cs@[C']" in exI) apply simp
apply (rule_tac x="[]" in exI) apply simp
done
qed
lemma assumes subo:"Subobjs P C (rev Cs)" and wf:"wf_prog wf_md P"
shows subobjs_rel_rev:"P,C \<turnstile> [C] \<sqsubseteq> (rev Cs)"
using subo
proof (induct Cs)
case Nil
thus ?case by (fastsimp dest:Subobjs_nonempty)
next
case (Cons C' Cs')
have subo':"Subobjs P C (rev (C'#Cs'))"
and IH:"Subobjs P C (rev Cs') ==> P,C \<turnstile> [C] \<sqsubseteq> rev Cs'" by fact+
from subo' have "class": "is_class P C" by(rule Subobjs_isClass)
show ?case
proof (cases "Cs' = []")
case True hence empty:"Cs' = []" .
with subo' have subo'':"Subobjs P C [C']" by simp
thus ?thesis
proof (cases "C = C'")
case True
with empty show ?thesis by simp
next
case False
with subo'' obtain D D' where leq:"P \<turnstile> C \<preceq>* D" and subS:"P \<turnstile> D \<prec>S D'"
and suboR:"SubobjsR P D' [C']"
by (auto elim:Subobjs.cases dest:hd_SubobjsR)
from suboR have C':"C' = D'" by (fastsimp dest:hd_SubobjsR)
from leq wf obtain Ds where steps:"P,C \<turnstile> [C] \<sqsubseteq> Ds@[D]"
by (auto dest:subcls_leq_path)
hence suboSteps:"Subobjs P C (Ds@[D])" using "class" wf
apply (induct rule:rtrancl_induct)
apply (erule Subobjs_Base)
apply (auto elim!:leq_path1.cases)
apply (subgoal_tac "SubobjsR P D [D]")
apply (fastsimp dest:Subobjs_subclass intro:Subobjs_Sh)
apply (fastsimp dest!:subclsSD intro:SubobjsR_Base wf_cdecl_supD
class_wf ShBaseclass_isBaseclass)
done
hence step:"P,C \<turnstile> (Ds@[D]) \<sqsubset>1 [D']" using subS by (rule leq_path_sh)
with steps empty False C' show ?thesis by simp
qed
next
case False
with subo' have subo'':"Subobjs P C (rev Cs')"
by (fastsimp intro:butlast_Subobjs)
with IH have steps:"P,C \<turnstile> [C] \<sqsubseteq> rev Cs'" by simp
from subo' subo'' have "P,C \<turnstile> rev Cs' \<sqsubset>1 rev (C'#Cs')"
by (fastsimp intro:leq_pathRep)
with steps show ?thesis by simp
qed
qed
lemma subobjs_rel:
assumes subo:"Subobjs P C Cs" and wf:"wf_prog wf_md P"
shows "P,C \<turnstile> [C] \<sqsubseteq> Cs"
proof -
obtain Cs' where Cs':"Cs' = rev Cs" by simp
with subo have "Subobjs P C (rev Cs')" by simp
hence "P,C \<turnstile> [C] \<sqsubseteq> rev Cs'" using wf by (rule subobjs_rel_rev)
with Cs' show ?thesis by simp
qed
lemma assumes wf:"wf_prog wf_md P"
shows leq_path_last:"[|P,C \<turnstile> Cs \<sqsubseteq> Cs'; last Cs = last Cs'|] ==> Cs = Cs'"
proof(induct rule:rtrancl_induct)
show "Cs = Cs" by simp
next
fix Cs' Cs''
assume leqs:"P,C \<turnstile> Cs \<sqsubseteq> Cs'" and leq:"P,C \<turnstile> Cs' \<sqsubset>1 Cs''"
and last:"last Cs = last Cs''"
and IH:"last Cs = last Cs' ==> Cs = Cs'"
from leq wf have sup1:"P \<turnstile> last Cs' \<prec>1 last Cs''"
by(rule last_leq_path)
{ assume "Cs = Cs'"
with last have eq:"last Cs'' = last Cs'" by simp
with eq wf sup1 have "Cs = Cs''" by(fastsimp dest:subcls1_wfD) }
moreover
{ assume "(Cs,Cs') ∈ (leq_path1 P C)+"
hence sub:"(last Cs,last Cs') ∈ (subcls1 P)+" using wf
by(rule last_leq_paths)
with sup1 last have "(last Cs'',last Cs'') ∈ (subcls1 P)+" by simp
with wf have "Cs = Cs''" by(fastsimp dest:subcls_irrefl) }
ultimately show "Cs = Cs''" using leqs
by(fastsimp dest:rtranclD)
qed
section{* Well-formedness and appendPath *}
lemma appendPath1:
"[|Subobjs P C Cs; Subobjs P (last Cs) Ds; last Cs ≠ hd Ds|]
==> Subobjs P C Ds"
apply(subgoal_tac "¬ SubobjsR P (last Cs) Ds")
apply (subgoal_tac "∃C' D. P \<turnstile> last Cs \<preceq>* C' ∧ P \<turnstile> C' \<prec>S D ∧ SubobjsR P D Ds")
apply clarsimp
apply (drule Subobjs_subclass)
apply (subgoal_tac "P \<turnstile> C \<preceq>* C'")
apply (erule_tac C'="C'" and D="D" in Subobjs_Sh)
apply simp
apply simp
apply fastsimp
apply (erule Subobjs_notSubobjsR)
apply simp
apply (fastsimp dest:hd_SubobjsR)
done
lemma appendPath2_rev:
assumes subo1:"Subobjs P C Cs" and subo2:"Subobjs P (last Cs) (last Cs#rev Ds)"
and wf:"wf_prog wf_md P"
shows "Subobjs P C (Cs@(tl (last Cs#rev Ds)))"
using subo2
proof (induct Ds)
case Nil
with subo1 show ?case by simp
next
case (Cons D' Ds')
have IH:"Subobjs P (last Cs) (last Cs#rev Ds')
==> Subobjs P C (Cs@tl(last Cs#rev Ds'))"
and subo:"Subobjs P (last Cs) (last Cs#rev (D'#Ds'))" by fact+
from subo have "Subobjs P (last Cs) (last Cs#rev Ds')"
by (fastsimp intro:butlast_Subobjs)
with IH have subo':"Subobjs P C (Cs@tl(last Cs#rev Ds'))"
by simp
have last:"last(last Cs#rev Ds') = last (Cs@tl(last Cs#rev Ds'))"
by (cases Ds')auto
obtain C' Cs' where C':"C' = last(last Cs#rev Ds')" and
"Cs' = butlast(last Cs#rev Ds')" by simp
hence "Cs'@[C'] = last Cs#rev Ds'" by simp
hence "last Cs#rev (D'#Ds') = Cs'@[C',D']" by simp
with subo have "Subobjs P (last Cs) (Cs'@[C',D'])" by (cases Cs') auto
hence "P \<turnstile> C' \<prec>R D'" by - (rule Subobjs_subclsR,simp)
with C' last have "P \<turnstile> last (Cs@tl(last Cs#rev Ds')) \<prec>R D'" by simp
with subo' wf have "Subobjs P C ((Cs@tl(last Cs#rev Ds'))@[D'])"
by (erule_tac Cs="(Cs@tl(last Cs#rev Ds'))" in converse_Subobjs_Rep) simp
thus ?case by simp
qed
lemma appendPath2:
assumes subo1:"Subobjs P C Cs" and subo2:"Subobjs P (last Cs) Ds"
and eq:"last Cs = hd Ds" and wf:"wf_prog wf_md P"
shows "Subobjs P C (Cs@(tl Ds))"
using subo2
proof (cases Ds)
case Nil
with subo1 show ?thesis by simp
next
case (Cons D' Ds')
with subo2 eq have subo:"Subobjs P (last Cs) (last Cs#Ds')" by simp
obtain Ds'' where Ds'':"Ds'' = rev Ds'" by simp
with subo have "Subobjs P (last Cs) (last Cs#rev Ds'')" by simp
with subo1 wf have "Subobjs P C (Cs@(tl (last Cs#rev Ds'')))"
by -(rule appendPath2_rev)
with Ds'' eq Cons show ?thesis by simp
qed
lemma Subobjs_appendPath:
"[|Subobjs P C Cs; Subobjs P (last Cs) Ds;wf_prog wf_md P|]
==> Subobjs P C (Cs@pDs)"
by(fastsimp elim:appendPath2 appendPath1 simp:appendPath_def)
section{* Path and program size *}
lemma assumes subo:"Subobjs P C Cs" and wf:"wf_prog wf_md P"
shows path_contains_classes:"∀C' ∈ set Cs. is_class P C'"
using subo
proof clarsimp
fix C' assume subo:"Subobjs P C Cs" and set:"C' ∈ set Cs"
from set obtain Ds Ds' where Cs:"Cs = Ds@C'#Ds'"
by (fastsimp simp:in_set_conv_decomp)
with Cs show "is_class P C'"
proof (cases "Ds = []")
case True
with Cs subo have subo':"Subobjs P C (C'#Ds')" by simp
thus ?thesis by (rule Subobjs.cases,
auto dest:hd_SubobjsR intro:SubobjsR_isClass)
next
case False
then obtain C'' Cs'' where Cs'':"Cs'' = butlast Ds"
and last:"C'' = last Ds" by auto
with False have Ds:"Ds = Cs''@[C'']" by simp
with Cs subo have subo':"Subobjs P C (Cs''@[C'',C']@Ds')"
by simp
hence "P \<turnstile> C'' \<prec>R C'" by(fastsimp intro:isSubobjs_subclsR Subobjs_isSubobj)
with wf show ?thesis
by (fastsimp dest!:subclsRD
intro:wf_cdecl_supD class_wf RepBaseclass_isBaseclass subclsSI)
qed
qed
lemma path_subset_classes:"[|Subobjs P C Cs; wf_prog wf_md P|]
==> set Cs ⊆ {C. is_class P C}"
by (auto dest:path_contains_classes)
lemma assumes subo:"Subobjs P C (rev Cs)" and wf:"wf_prog wf_md P"
shows rev_path_distinct_classes:"distinct Cs"
using subo
proof (induct Cs)
case Nil thus ?case by(fastsimp dest:Subobjs_nonempty)
next
case (Cons C' Cs')
have subo':"Subobjs P C (rev(C'#Cs'))"
and IH:"Subobjs P C (rev Cs') ==> distinct Cs'" by fact+
show ?case
proof (cases "Cs' = []")
case True thus ?thesis by simp
next
case False
hence rev:"rev Cs' ≠ []" by simp
from subo' have subo'':"Subobjs P C (rev Cs'@[C'])" by simp
hence "Subobjs P C (rev Cs')" using rev wf
by(fastsimp dest:appendSubobj)
with IH have dist:"distinct Cs'" by simp
from subo'' wf have "C' ∉ set (rev Cs')"
by(fastsimp dest:unique2)
with dist show ?thesis by simp
qed
qed
lemma assumes subo:"Subobjs P C Cs" and wf:"wf_prog wf_md P"
shows path_distinct_classes:"distinct Cs"
proof -
obtain Cs' where Cs':"Cs' = rev Cs" by simp
with subo have "Subobjs P C (rev Cs')" by simp
with wf have "distinct Cs'"
by -(rule rev_path_distinct_classes)
with Cs' show ?thesis by simp
qed
lemma assumes wf:"wf_prog wf_md P"
shows prog_length:"length P = card {C. is_class P C}"
proof -
from wf have dist_fst:"distinct_fst P" by (simp add:wf_prog_def)
hence "distinct P" by (simp add:distinct_fst_def,induct P,auto)
hence card_set:"card (set P) = length P" by (rule distinct_card)
from dist_fst have set:"{C. is_class P C} = fst ` (set P)"
by (simp add:is_class_def class_def,auto simp:distinct_fst_def,
auto dest:map_of_eq_Some_iff intro!:image_eqI)
from dist_fst have "card(fst ` (set P)) = card (set P)"
by(auto intro:card_image simp:distinct_map distinct_fst_def)
with card_set set show ?thesis by simp
qed
lemma assumes subo:"Subobjs P C Cs" and wf:"wf_prog wf_md P"
shows path_length:"length Cs ≤ length P"
proof -
from subo wf have "distinct Cs" by (rule path_distinct_classes)
hence card_eq_length:"card (set Cs) = length Cs" by (rule distinct_card)
from subo wf have "card (set Cs) ≤ card {C. is_class P C}"
by (auto dest:path_subset_classes intro:card_mono finite_is_class)
with card_eq_length have "length Cs ≤ card {C. is_class P C}" by simp
with wf show ?thesis by(fastsimp dest:prog_length)
qed
lemma empty_path_empty_set:"{Cs. Subobjs P C Cs ∧ length Cs ≤ 0} = {}"
by (auto dest:Subobjs_nonempty)
lemma split_set_path_length:"{Cs. Subobjs P C Cs ∧ length Cs ≤ Suc(n)} =
{Cs. Subobjs P C Cs ∧ length Cs ≤ n} ∪ {Cs. Subobjs P C Cs ∧ length Cs = Suc(n)}"
by auto
lemma empty_list_set:"{xs. set xs ⊆ F ∧ xs = []} = {[]}"
by auto
lemma suc_n_union_of_union:"{xs. set xs ⊆ F ∧ length xs = Suc n} = (UN x:F. UN xs : {xs. set xs ≤ F ∧ length xs = n}. {x#xs})"
by (auto simp:length_Suc_conv)
lemma max_length_finite_set:"finite F ==> finite{xs. set xs <= F ∧ length xs = n}"
by(induct n,simp add:empty_list_set, simp add:suc_n_union_of_union)
lemma path_length_n_finite_set:
"wf_prog wf_md P ==> finite{Cs. Subobjs P C Cs ∧ length Cs = n}"
by (rule_tac B="{Cs. set Cs <= {C. is_class P C} ∧ length Cs = n}" in finite_subset,
auto dest:path_contains_classes intro:max_length_finite_set simp:finite_is_class)
lemma path_finite_leq:
"wf_prog wf_md P ==> finite{Cs. Subobjs P C Cs ∧ length Cs ≤ length P}"
by (induct "length P",simp only:empty_path_empty_set,
auto intro:path_length_n_finite_set simp:split_set_path_length)
lemma path_finite:"wf_prog wf_md P ==> finite{Cs. Subobjs P C Cs}"
by (subgoal_tac "{Cs. Subobjs P C Cs} =
{Cs. Subobjs P C Cs ∧ length Cs ≤ length P}",
auto intro:path_finite_leq path_length)
section{* Well-formedness and Path *}
lemma path_via_reverse:
assumes path_via:"P \<turnstile> Path C to D via Cs" and wf:"wf_prog wf_md P"
shows "∀Cs'. P \<turnstile> Path D to C via Cs' --> Cs = [C] ∧ Cs' = [C] ∧ C = D"
proof -
from path_via have subo:"Subobjs P C Cs" and last:"last Cs = D"
by(simp add:path_via_def)+
hence leq:"P \<turnstile> C \<preceq>* D" by(fastsimp dest:Subobjs_subclass)
{ fix Cs' assume "P \<turnstile> Path D to C via Cs'"
hence subo':"Subobjs P D Cs'" and last':"last Cs' = C"
by(simp add:path_via_def)+
hence leq':"P \<turnstile> D \<preceq>* C" by(fastsimp dest:Subobjs_subclass)
with leq wf have CeqD:"C = D" by(rule subcls_asym2)
moreover have Cs:"Cs = [C]" using CeqD subo last wf by(fastsimp intro:mdc_eq_last)
moreover have "Cs' = [C]" using CeqD subo' last' wf by(fastsimp intro:mdc_eq_last)
ultimately have "Cs = [C] ∧ Cs' = [C] ∧ C = D" by simp }
thus ?thesis by blast
qed
lemma path_hd_appendPath:
assumes path:"P,C \<turnstile> Cs \<sqsubseteq> Cs'@pCs" and last:"last Cs' = hd Cs"
and notemptyCs:"Cs ≠ []" and notemptyCs':"Cs' ≠ []" and wf:"wf_prog wf_md P"
shows "Cs' = [hd Cs]"
using path
proof -
from path notemptyCs last have path2:"P,C \<turnstile> Cs \<sqsubseteq> Cs'@ tl Cs"
by (simp add:appendPath_def)
thus ?thesis
proof (auto dest!:rtranclD)
assume "Cs = Cs'@ tl Cs"
with notemptyCs show "Cs' = [hd Cs]" by (rule app_hd_tl)
next
assume trancl:"(Cs,Cs'@ tl Cs) ∈ (leq_path1 P C)+"
from notemptyCs' last have butlastLast:"Cs' = butlast Cs' @ [hd Cs]"
by -(drule append_butlast_last_id,simp)
with trancl have trancl':"(Cs, (butlast Cs' @ [hd Cs]) @ tl Cs) ∈ (leq_path1 P C)+"
by simp
from notemptyCs have "(butlast Cs' @ [hd Cs]) @ tl Cs = butlast Cs' @ Cs"
by simp
with trancl' have "(Cs, butlast Cs' @ Cs) ∈ (leq_path1 P C)+" by simp
hence "(last Cs, last (butlast Cs' @ Cs)) ∈ (subcls1 P)+" using wf
by (rule last_leq_paths)
with notemptyCs have "(last Cs, last Cs) ∈ (subcls1 P)+"
by -(drule_tac xs="butlast Cs'" in last_appendR,simp)
with wf show ?thesis by (auto dest:subcls_irrefl)
qed
qed
lemma path_via_C: "[|P \<turnstile> Path C to C via Cs; wf_prog wf_md P|] ==> Cs = [C]"
by (fastsimp intro:mdc_eq_last simp:path_via_def)
lemma assumes wf:"wf_prog wf_md P"
and path_via:"P \<turnstile> Path last Cs to C via Cs'"
and path_via':"P \<turnstile> Path last Cs to C via Cs''"
and appendPath:"Cs = Cs@pCs'"
shows appendPath_path_via:"Cs = Cs@pCs''"
proof -
from path_via have notempty:"Cs' ≠ []"
by(fastsimp intro!:Subobjs_nonempty simp:path_via_def)
{ assume eq:"last Cs = hd Cs'"
and Cs:"Cs = Cs@tl Cs'"
from Cs have "tl Cs' = []" by simp
with eq notempty have "Cs' = [last Cs]"
by -(drule hd_Cons_tl,simp) }
moreover
{ assume "Cs = Cs'"
with wf path_via have "Cs' = [last Cs]"
by(fastsimp intro:mdc_eq_last simp:path_via_def) }
ultimately have eq:"Cs' = [last Cs]" using appendPath
by(simp add:appendPath_def,split split_if_asm,simp_all)
with path_via have "C = last Cs"
by(simp add:path_via_def)
with wf path_via' have "Cs'' = [last Cs]"
by simp(rule path_via_C)
thus ?thesis by (simp add:appendPath_def)
qed
lemma subo_no_path:
assumes subo:"Subobjs P C' (Cs @ C#Cs')" and wf:"wf_prog wf_md P"
and notempty:"Cs' ≠ []"
shows "¬ P \<turnstile> Path last Cs' to C via Ds"
proof
assume "P \<turnstile> Path last Cs' to C via Ds"
hence subo':"Subobjs P (last Cs') Ds" and last:"last Ds = C"
by (auto simp:path_via_def)
hence notemptyDs:"Ds ≠ []" by -(drule Subobjs_nonempty)
then obtain D' Ds' where D'Ds':"Ds = D'#Ds'" by(cases Ds)auto
from subo have suboC:"Subobjs P C (C#Cs')" by (rule Subobjs_Subobjs)
with wf subo' notempty have suboapp:"Subobjs P C ((C#Cs')@pDs)"
by -(rule Subobjs_appendPath,simp_all)
with notemptyDs last have last':"last ((C#Cs')@pDs) = C"
by -(drule_tac Cs'="(C#Cs')" in appendPath_last,simp)
from notemptyDs have "(C#Cs')@pDs ≠ []"
by (simp add:appendPath_def)
with last' have "C ∈ set ((C#Cs')@pDs)"
apply (auto simp add:in_set_conv_decomp)
apply (rule_tac x="butlast((C#Cs')@pDs)" in exI)
apply (rule_tac x="[]" in exI)
apply (drule append_butlast_last_id)
apply simp
done
with suboapp wf have hd:"C = hd ((C#Cs')@pDs)" by -(rule mdc_hd_path)
thus "False"
proof (cases "last (C#Cs') = hd Ds")
case True
hence eq:"(C#Cs')@pDs = (C#Cs')@(tl Ds)" by (simp add:appendPath_def)
show ?thesis
proof (cases Ds')
case Nil
with D'Ds' have Ds:"Ds = [D']" by simp
with last have "C = D'" by simp
with True notempty Ds have "last (C#Cs') = C" by simp
with notempty have "last Cs' = C" by simp
with notempty have Cset:"C ∈ set Cs'"
apply (auto simp add:in_set_conv_decomp)
apply (rule_tac x="butlast Cs'" in exI)
apply (rule_tac x="[]" in exI)
apply (drule append_butlast_last_id)
apply simp
done
from subo wf have "C ∉ set Cs'" by (rule unique1)
with Cset show ?thesis by simp
next
case (Cons X Xs)
with D'Ds' have tlnotempty:"tl Ds ≠ []" by simp
with Cons last D'Ds' have "last (tl Ds) = C" by simp
with tlnotempty have "C ∈ set (tl Ds)"
apply (auto simp add:in_set_conv_decomp)
apply (rule_tac x="butlast (tl Ds)" in exI)
apply (rule_tac x="[]" in exI)
apply (drule append_butlast_last_id)
apply simp
done
hence Cset:"C ∈ set (Cs'@(tl Ds))" by simp
from suboapp eq wf have "C ∉ set (Cs'@(tl Ds))"
by (subgoal_tac "Subobjs P C (C#(Cs'@(tl Ds)))",
rule_tac Cs="[]" in unique1,simp_all)
with Cset show ?thesis by simp
qed
next
case False
with notemptyDs have eq:"(C#Cs')@pDs = Ds" by (simp add:appendPath_def)
with subo' last have lastleq:"P \<turnstile> last Cs' \<preceq>* C"
by (fastsimp dest:Subobjs_subclass)
from notempty obtain X Xs where X:"X = last Cs'" and "Xs = butlast Cs'"
by auto
with notempty have XXs:"Cs' = Xs@[X]" by simp
hence CleqX:"(C,X) ∈ (subcls1 P)+"
proof (cases Xs)
case Nil
with suboC XXs have "Subobjs P C [C,X]" by simp
thus ?thesis
apply -
apply (rule r_into_trancl)
apply (rule subclsR_subcls1)
apply (rule_tac Cs="[]" in Subobjs_subclsR)
apply simp
done
next
case (Cons Y Ys)
with suboC XXs have subo'':"Subobjs P C ([C,Y]@Ys@[X])" by simp
hence plus:"(C,Y) ∈ (subcls1 P)+"
apply -
apply (rule r_into_trancl)
apply (rule subclsR_subcls1)
apply (rule_tac Cs="[]" in Subobjs_subclsR)
apply simp
done
from subo'' have "P \<turnstile> Y \<preceq>* X"
apply -
apply (subgoal_tac "Subobjs P C ([C]@Y#(Ys@[X]))")
apply (drule Subobjs_Subobjs)
apply (drule_tac C="Y" in Subobjs_subclass) apply simp_all
done
with plus show ?thesis by (fastsimp elim:trancl_rtrancl_trancl)
qed
from lastleq X have leq:"P \<turnstile> X \<preceq>* C" by simp
with CleqX have "(C,C) ∈ (subcls1 P)+"
by (rule trancl_rtrancl_trancl)
with wf show ?thesis by (fastsimp dest:subcls_irrefl)
qed
qed
lemma leq_implies_path:
assumes leq:"P \<turnstile> C \<preceq>* D" and "class": "is_class P C"
and wf:"wf_prog wf_md P"
shows "∃Cs. P \<turnstile> Path C to D via Cs"
using leq "class"
proof(induct rule:rtrancl.induct)
fix C assume "is_class P C"
thus "∃Cs. P \<turnstile> Path C to C via Cs"
by (rule_tac x="[C]" in exI,fastsimp intro:Subobjs_Base simp:path_via_def)
next
fix C C' D assume CleqC':"P \<turnstile> C \<preceq>* C'" and C'leqD:"P \<turnstile> C' \<prec>1 D"
and classC:"is_class P C" and IH:"is_class P C ==> ∃Cs. P \<turnstile> Path C to C' via Cs"
from IH[OF classC] obtain Cs where subo:"Subobjs P C Cs" and last:"last Cs = C'"
by (auto simp:path_via_def)
with C'leqD show "∃Cs. P \<turnstile> Path C to D via Cs"
proof (auto dest!:subcls1_subclsR_or_subclsS)
assume "P \<turnstile> last Cs \<prec>R D"
with subo have "Subobjs P C (Cs@[D])" using wf
by (rule converse_Subobjs_Rep)
thus ?thesis by (fastsimp simp:path_via_def)
next
assume subS:"P \<turnstile> last Cs \<prec>S D"
from CleqC' last have Cleqlast:"P \<turnstile> C \<preceq>* last Cs" by simp
from subS have classLast:"is_class P (last Cs)"
by (auto intro:subcls1_class subclsS_subcls1)
then obtain Bs fs ms where "class P (last Cs) = Some(Bs,fs,ms)"
by (fastsimp simp:is_class_def)
hence classD:"is_class P D" using subS wf
by (auto intro:wf_cdecl_supD dest:class_wf dest!:subclsSD
elim:ShBaseclass_isBaseclass)
with Cleqlast subS have "Subobjs P C [D]"
by (fastsimp intro:Subobjs_Sh SubobjsR_Base)
thus ?thesis by (fastsimp simp:path_via_def)
qed
qed
lemma least_method_implies_path_unique:
assumes least:"P \<turnstile> C has least M = (Ts,T,m) via Cs" and wf:"wf_prog wf_md P"
shows "P \<turnstile> Path C to (last Cs) unique"
proof (auto simp add:path_unique_def)
from least have "Subobjs P C Cs"
by (simp add:LeastMethodDef_def MethodDefs_def)
thus "∃Cs'. Subobjs P C Cs' ∧ last Cs' = last Cs"
by fastsimp
next
fix Cs' Cs''
assume suboCs':"Subobjs P C Cs'" and suboCs'':"Subobjs P C Cs''"
and lastCs':"last Cs' = last Cs" and lastCs'':"last Cs'' = last Cs"
from suboCs' have notemptyCs':"Cs' ≠ []" by (rule Subobjs_nonempty)
from suboCs'' have notemptyCs'':"Cs'' ≠ []" by (rule Subobjs_nonempty)
from least have suboCs:"Subobjs P C Cs"
and all:"∀Ds. Subobjs P C Ds ∧
(∃Ts T m Bs ms. (∃fs. class P (last Ds) = Some (Bs, fs, ms)) ∧
map_of ms M = Some(Ts,T,m)) --> P,C \<turnstile> Cs \<sqsubseteq> Ds"
by (auto simp:LeastMethodDef_def MethodDefs_def)
from least obtain Bs fs ms T Ts m where
"class": "class P (last Cs) = Some(Bs, fs, ms)" and map:"map_of ms M = Some(Ts,T,m)"
by (auto simp:LeastMethodDef_def MethodDefs_def intro:that)
from suboCs' lastCs' "class" map all have pathCs':"P,C \<turnstile> Cs \<sqsubseteq> Cs'"
by simp
with wf lastCs' have eq:"Cs = Cs'" by(fastsimp intro:leq_path_last)
from suboCs'' lastCs'' "class" map all have pathCs'':"P,C \<turnstile> Cs \<sqsubseteq> Cs''"
by simp
with wf lastCs'' have "Cs = Cs''" by(fastsimp intro:leq_path_last)
with eq show "Cs' = Cs''" by simp
qed
lemma least_field_implies_path_unique:
assumes least:"P \<turnstile> C has least F:T via Cs" and wf:"wf_prog wf_md P"
shows "P \<turnstile> Path C to (hd Cs) unique"
proof (auto simp add:path_unique_def)
from least have "Subobjs P C Cs"
by (simp add:LeastFieldDecl_def FieldDecls_def)
hence "Subobjs P C ([hd Cs]@tl Cs)"
by - (frule Subobjs_nonempty,simp)
with wf have "Subobjs P C [hd Cs]"
by (fastsimp intro:appendSubobj)
thus "∃Cs'. Subobjs P C Cs' ∧ last Cs' = hd Cs"
by fastsimp
next
fix Cs' Cs''
assume suboCs':"Subobjs P C Cs'" and suboCs'':"Subobjs P C Cs''"
and lastCs':"last Cs' = hd Cs" and lastCs'':"last Cs'' = hd Cs"
from suboCs' have notemptyCs':"Cs' ≠ []" by (rule Subobjs_nonempty)
from suboCs'' have notemptyCs'':"Cs'' ≠ []" by (rule Subobjs_nonempty)
from least have suboCs:"Subobjs P C Cs"
and all:"∀Ds. Subobjs P C Ds ∧
(∃T Bs fs. (∃ms. class P (last Ds) = Some (Bs, fs, ms)) ∧
map_of fs F = Some T) --> P,C \<turnstile> Cs \<sqsubseteq> Ds"
by (auto simp:LeastFieldDecl_def FieldDecls_def)
from least obtain Bs fs ms T where
"class": "class P (last Cs) = Some(Bs, fs, ms)" and map:"map_of fs F = Some T"
by (auto simp:LeastFieldDecl_def FieldDecls_def)
from suboCs have notemptyCs:"Cs ≠ []" by (rule Subobjs_nonempty)
from suboCs notemptyCs have suboHd:"Subobjs P (hd Cs) (hd Cs#tl Cs)"
by -(rule_tac C="C" and Cs="[]" in Subobjs_Subobjs,simp)
with suboCs' notemptyCs lastCs' wf have suboCs'App:"Subobjs P C (Cs'@pCs)"
by -(rule Subobjs_appendPath,simp_all)
from suboHd suboCs'' notemptyCs lastCs'' wf
have suboCs''App:"Subobjs P C (Cs''@pCs)"
by -(rule Subobjs_appendPath,simp_all)
from suboCs'App all "class" map notemptyCs have pathCs':"P,C \<turnstile> Cs \<sqsubseteq> Cs'@pCs"
by -(erule_tac x="Cs'@pCs" in allE,drule_tac Cs'="Cs'" in appendPath_last,simp)
from suboCs''App all "class" map notemptyCs have pathCs'':"P,C \<turnstile> Cs \<sqsubseteq> Cs''@pCs"
by -(erule_tac x="Cs''@pCs" in allE,drule_tac Cs'="Cs''" in appendPath_last,simp)
from pathCs' lastCs' notemptyCs notemptyCs' wf have Cs':"Cs' = [hd Cs]"
by (rule path_hd_appendPath)
from pathCs'' lastCs'' notemptyCs notemptyCs'' wf have "Cs'' = [hd Cs]"
by (rule path_hd_appendPath)
with Cs' show "Cs' = Cs''" by simp
qed
lemma least_field_implies_path_via_hd:
"[|P \<turnstile> C has least F:T via Cs; wf_prog wf_md P|]
==> P \<turnstile> Path C to (hd Cs) via [hd Cs]"
apply (simp add:LeastFieldDecl_def FieldDecls_def)
apply clarsimp
apply (simp add:path_via_def)
apply (frule Subobjs_nonempty)
apply (rule_tac Cs'="tl Cs" in appendSubobj)
apply auto
done
lemma path_C_to_C_unique:
"[|wf_prog wf_md P; is_class P C|] ==> P \<turnstile> Path C to C unique"
apply (unfold path_unique_def)
apply (rule_tac a="[C]" in ex1I)
apply (auto intro:Subobjs_Base mdc_eq_last)
done
lemma leqR_SubobjsR:"[|(C,D) ∈ (subclsR P)*; is_class P C; wf_prog wf_md P|]
==> ∃Cs. SubobjsR P C (Cs@[D])"
apply (induct rule:rtrancl_induct)
apply (drule SubobjsR_Base)
apply (rule_tac x="[]" in exI)
apply simp
apply (auto dest:converse_SubobjsR_Rep)
done
lemma assumes path_unique:"P \<turnstile> Path C to D unique" and leq:"P \<turnstile> C \<preceq>* C'"
and leqR:"(C',D) ∈ (subclsR P)*" and wf:"wf_prog wf_md P"
shows "P \<turnstile> Path C to C' unique"
proof -
from path_unique have "is_class P C"
by (auto intro:Subobjs_isClass simp:path_unique_def)
with leq wf obtain Cs where path_via:"P \<turnstile> Path C to C' via Cs"
by (auto dest:leq_implies_path)
with wf have classC':"is_class P C'"
by (fastsimp intro:Subobj_last_isClass simp:path_via_def)
with leqR wf obtain Cs' where subo:"SubobjsR P C' Cs'" and last:"last Cs' = D"
by (auto dest:leqR_SubobjsR)
hence hd:"hd Cs' = C'"
by (fastsimp dest:hd_SubobjsR)
with path_via subo wf have suboApp:"Subobjs P C (Cs@tl Cs')"
by (auto dest!:Subobjs_Rep dest:Subobjs_appendPath
simp:path_via_def appendPath_def)
hence last':"last (Cs@tl Cs') = D"
proof (cases "tl Cs' = []")
case True
with subo hd last have "C' = D"
by (subgoal_tac "Cs' = [C']",auto dest!:SubobjsR_nonempty hd_Cons_tl)
with path_via have "last Cs = D"
by (auto simp:path_via_def)
with True show ?thesis by simp
next
case False
from subo have Cs':"Cs' = hd Cs'#tl Cs'"
by (auto dest:SubobjsR_nonempty)
from False have "last(hd Cs'#tl Cs') = last (tl Cs')"
by (rule last_ConsR)
with False Cs' last show ?thesis by simp
qed
with path_unique suboApp
have all:"∀Ds. Subobjs P C Ds ∧ last Ds = D --> Ds = Cs@tl Cs'"
by (auto simp add:path_unique_def)
{ fix Cs'' assume path_via2:"P \<turnstile> Path C to C' via Cs''" and noteq:"Cs'' ≠ Cs"
with suboApp have "last (Cs''@tl Cs') = D"
proof (cases "tl Cs' = []")
case True
with subo hd last have "C' = D"
by (subgoal_tac "Cs' = [C']",auto dest!:SubobjsR_nonempty hd_Cons_tl)
with path_via2 have "last Cs'' = D"
by (auto simp:path_via_def)
with True show ?thesis by simp
next
case False
from subo have Cs':"Cs' = hd Cs'#tl Cs'"
by (auto dest:SubobjsR_nonempty)
from False have "last(hd Cs'#tl Cs') = last (tl Cs')"
by (rule last_ConsR)
with False Cs' last show ?thesis by simp
qed
with path_via2 noteq have False using all subo hd wf
apply (auto simp:path_via_def)
apply (drule Subobjs_Rep)
apply (drule Subobjs_appendPath)
apply (auto simp:appendPath_def)
done }
with path_via show ?thesis
by (auto simp:path_via_def path_unique_def)
qed
section{* Well-formedness and member lookup *}
lemma has_path_has:
"[|P \<turnstile> Path D to C via Ds; P \<turnstile> C has M = (Ts,T,m) via Cs; wf_prog wf_md P|]
==> P \<turnstile> D has M = (Ts,T,m) via Ds@pCs"
by (clarsimp simp:HasMethodDef_def MethodDefs_def,frule Subobjs_nonempty,
drule_tac Cs'="Ds" in appendPath_last,
fastsimp intro:Subobjs_appendPath simp:path_via_def)
lemma has_least_wf_mdecl:
"[| wf_prog wf_md P; P \<turnstile> C has least M = m via Cs |]
==> wf_mdecl wf_md P (last Cs) (M,m)"
by(fastsimp dest:visible_methods_exist class_wf map_of_SomeD
simp:LeastMethodDef_def wf_cdecl_def)
lemma has_overrider_wf_mdecl:
"[| wf_prog wf_md P; P \<turnstile> (C,Cs) has overrider M = m via Cs' |]
==> wf_mdecl wf_md P (last Cs') (M,m)"
by(fastsimp dest:visible_methods_exist map_of_SomeD class_wf
simp:FinalOverriderMethodDef_def OverriderMethodDefs_def
MinimalMethodDefs_def wf_cdecl_def)
lemma select_method_wf_mdecl:
"[| wf_prog wf_md P; P \<turnstile> (C,Cs) selects M = m via Cs' |]
==> wf_mdecl wf_md P (last Cs') (M,m)"
by(fastsimp elim:SelectMethodDef.induct
intro:has_least_wf_mdecl has_overrider_wf_mdecl)
lemma wf_sees_method_fun:
"[|P \<turnstile> C has least M = mthd via Cs; P \<turnstile> C has least M = mthd' via Cs';
wf_prog wf_md P|]
==> mthd = mthd' ∧ Cs = Cs'"
apply (auto simp:LeastMethodDef_def)
apply (erule_tac x="(Cs', mthd')" in ballE)
apply (erule_tac x="(Cs, mthd)" in ballE)
apply auto
apply (drule leq_path_asym2) apply simp_all
apply (rule sees_methods_fun) apply simp_all
apply (erule_tac x="(Cs', mthd')" in ballE)
apply (erule_tac x="(Cs, mthd)" in ballE)
apply (auto intro:leq_path_asym2)
done
lemma wf_select_method_fun:
assumes wf:"wf_prog wf_md P"
shows "[|P \<turnstile> (C,Cs) selects M = mthd via Cs'; P \<turnstile> (C,Cs) selects M = mthd' via Cs''|]
==> mthd = mthd' ∧ Cs' = Cs''"
proof(induct rule:SelectMethodDef.induct)
case (dyn_unique C M mthd Cs' Cs)
have "P \<turnstile> (C, Cs) selects M = mthd' via Cs''"
and "P \<turnstile> C has least M = mthd via Cs'" by fact+
thus ?case
proof(induct rule:SelectMethodDef.induct)
case (dyn_unique D M' mthd' Ds' Ds)
have "P \<turnstile> D has least M' = mthd' via Ds'"
and "P \<turnstile> D has least M' = mthd via Cs'" by fact+
with wf show ?case
by -(rule wf_sees_method_fun,simp_all)
next
case (dyn_ambiguous D M' Ds mthd' Ds')
have "∀mthd Cs'. ¬ P \<turnstile> D has least M' = mthd via Cs'"
and "P \<turnstile> D has least M' = mthd via Cs'" by fact+
thus ?case by blast
qed
next
case (dyn_ambiguous C M Cs mthd Cs')
have "P \<turnstile> (C, Cs) selects M = mthd' via Cs''"
and "P \<turnstile> (C, Cs) has overrider M = mthd via Cs'"
and "∀mthd Cs'. ¬ P \<turnstile> C has least M = mthd via Cs'" by fact+
thus ?case
proof(induct rule:SelectMethodDef.induct)
case (dyn_unique D M' mthd' Ds' Ds)
have "P \<turnstile> D has least M' = mthd' via Ds'"
and "∀mthd Cs'. ¬ P \<turnstile> D has least M' = mthd via Cs'" by fact+
thus ?case by blast
next
case (dyn_ambiguous D M' Ds mthd' Ds')
have "P \<turnstile> (D, Ds) has overrider M' = mthd' via Ds'"
and "P \<turnstile> (D, Ds) has overrider M' = mthd via Cs'" by fact+
thus ?case by(fastsimp dest:overrider_method_fun)
qed
qed
lemma least_field_is_type:
assumes field:"P \<turnstile> C has least F:T via Cs" and wf:"wf_prog wf_md P"
shows "is_type P T"
proof -
from field have "(Cs,T) ∈ FieldDecls P C F"
by (simp add:LeastFieldDecl_def)
from this obtain Bs fs ms
where "map_of fs F = Some T"
and "class": "class P (last Cs) = Some (Bs,fs,ms)"
by (auto simp add:FieldDecls_def)
hence "(F,T) ∈ set fs" by (simp add:map_of_SomeD)
with "class" wf show ?thesis
by(fastsimp dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)
qed
lemma least_method_is_type:
assumes method:"P \<turnstile> C has least M = (Ts,T,m) via Cs" and wf:"wf_prog wf_md P"
shows "is_type P T"
proof -
from method have "(Cs,Ts,T,m) ∈ MethodDefs P C M"
by (simp add:LeastMethodDef_def)
from this obtain Bs fs ms
where "map_of ms M = Some(Ts,T,m)"
and "class": "class P (last Cs) = Some (Bs,fs,ms)"
by (auto simp add:MethodDefs_def)
hence "(M,Ts,T,m) ∈ set ms" by (simp add:map_of_SomeD)
with "class" wf show ?thesis
by(fastsimp dest!: class_wf simp: wf_cdecl_def wf_mdecl_def)
qed
lemma least_overrider_is_type:
assumes method:"P \<turnstile> (C,Cs) has overrider M = (Ts,T,m) via Cs'"
and wf:"wf_prog wf_md P"
shows "is_type P T"
proof -
from method have "(Cs',Ts,T,m) ∈ MethodDefs P C M"
by(clarsimp simp:FinalOverriderMethodDef_def OverriderMethodDefs_def
MinimalMethodDefs_def)
from this obtain Bs fs ms
where "map_of ms M = Some(Ts,T,m)"
and "class": "class P (last Cs') = Some (Bs,fs,ms)"
by (auto simp add:MethodDefs_def)
hence "(M,Ts,T,m) ∈ set ms" by (simp add:map_of_SomeD)
with "class" wf show ?thesis
by(fastsimp dest!: class_wf simp: wf_cdecl_def wf_mdecl_def)
qed
lemma select_method_is_type:
"[| P \<turnstile> (C,Cs) selects M = (Ts,T,m) via Cs'; wf_prog wf_md P|] ==> is_type P T"
by(auto elim:SelectMethodDef.cases
intro:least_method_is_type least_overrider_is_type)
lemma base_subtype:
"[|wf_cdecl wf_md P (C,Bs,fs,ms); C' ∈ baseClasses Bs;
P \<turnstile> C' has M = (Ts',T',m') via Cs@p[D]; (M,Ts,T,m)∈set ms|]
==> Ts' = Ts ∧ P \<turnstile> T ≤ T'"
apply (simp add:wf_cdecl_def)
apply clarsimp
apply (rotate_tac -1)
apply (erule_tac x="C'" in ballE)
apply clarsimp
apply (rotate_tac -1)
apply (erule_tac x="(M, Ts, T, m)" in ballE)
apply clarsimp
apply (erule_tac x="Ts'" in allE)
apply (erule_tac x="T'" in allE)
apply (auto simp:HasMethodDef_def)
apply (erule_tac x="fst m'" in allE)
apply (erule_tac x="snd m'" in allE)
apply (erule_tac x="Cs@p[D]" in allE)
apply simp
apply (erule_tac x="fst m'" in allE)
apply (erule_tac x="snd m'" in allE)
apply (erule_tac x="Cs@p[D]" in allE)
apply simp
done
lemma subclsPlus_subtype:
assumes classD:"class P D = Some(Bs',fs',ms')"
and mapMs':"map_of ms' M = Some(Ts',T',m')"
and leq:"(C,D) ∈ (subcls1 P)+" and wf:"wf_prog wf_md P"
shows "∀Bs fs ms Ts T m. class P C = Some(Bs,fs,ms) ∧ map_of ms M = Some(Ts,T,m)
--> Ts' = Ts ∧ P \<turnstile> T ≤ T'"
using leq classD mapMs'
proof (erule_tac a="C" and b="D" in converse_trancl_induct)
fix C
assume CleqD:"P \<turnstile> C \<prec>1 D" and classD1:"class P D = Some(Bs',fs',ms')"
{ fix Bs fs ms Ts T m
assume classC:"class P C = Some(Bs,fs,ms)" and mapMs:"map_of ms M = Some(Ts,T,m)"
from classD1 mapMs' have hasViaD:"P \<turnstile> D has M = (Ts',T',m') via [D]"
by (fastsimp intro:Subobjs_Base simp:HasMethodDef_def MethodDefs_def is_class_def)
from CleqD classC have base:"D ∈ baseClasses Bs"
by (fastsimp dest:subcls1D)
from classC wf have cdecl:"wf_cdecl wf_md P (C,Bs,fs,ms)"
by (rule class_wf)
from classC mapMs have "(M,Ts,T,m)∈set ms"
by -(drule map_of_is_SomeD)
with cdecl base hasViaD have "Ts' = Ts ∧ P \<turnstile> T ≤ T'"
by -(rule_tac Cs="[D]" in base_subtype,auto simp:appendPath_def) }
thus "∀Bs fs ms Ts T m. class P C = Some(Bs, fs, ms) ∧ map_of ms M = Some(Ts,T,m)
--> Ts' = Ts ∧ P \<turnstile> T ≤ T'" by blast
next
fix C C'
assume classD1:"class P D = Some(Bs',fs',ms')" and CleqC':"P \<turnstile> C \<prec>1 C'"
and subcls:"(C',D) ∈ (subcls1 P)+"
and IH:"∀Bs fs ms Ts T m. class P C' = Some(Bs,fs,ms) ∧
map_of ms M = Some(Ts,T,m) -->
Ts' = Ts ∧ P \<turnstile> T ≤ T'"
{ fix Bs fs ms Ts T m
assume classC:"class P C = Some(Bs,fs,ms)" and mapMs:"map_of ms M = Some(Ts,T,m)"
from classD1 mapMs' have hasViaD:"P \<turnstile> D has M = (Ts',T',m') via [D]"
by (fastsimp intro:Subobjs_Base simp:HasMethodDef_def MethodDefs_def is_class_def)
from subcls have C'leqD:"P \<turnstile> C' \<preceq>* D" by simp
from classC wf CleqC' have "is_class P C'"
by (fastsimp intro:wf_cdecl_supD class_wf dest:subcls1D)
with C'leqD wf obtain Cs where "P \<turnstile> Path C' to D via Cs"
by (auto dest!:leq_implies_path simp:is_class_def)
hence hasVia:"P \<turnstile> C' has M = (Ts',T',m') via Cs@p[D]" using hasViaD wf
by (rule has_path_has)
from CleqC' classC have base:"C' ∈ baseClasses Bs"
by (fastsimp dest:subcls1D)
from classC wf have cdecl:"wf_cdecl wf_md P (C,Bs,fs,ms)"
by (rule class_wf)
from classC mapMs have "(M,Ts,T,m)∈set ms"
by -(drule map_of_is_SomeD)
with cdecl base hasVia have "Ts' = Ts ∧ P \<turnstile> T ≤ T'"
by(rule base_subtype) }
thus "∀Bs fs ms Ts T m. class P C = Some(Bs, fs, ms) ∧ map_of ms M = Some(Ts,T,m)
--> Ts' = Ts ∧ P \<turnstile> T ≤ T'" by blast
qed
lemma leq_method_subtypes:
assumes leq:"P \<turnstile> D \<preceq>* C" and least:"P \<turnstile> D has least M = (Ts',T',m') via Ds"
and wf:"wf_prog wf_md P"
shows "∀Ts T m Cs. P \<turnstile> C has M = (Ts,T,m) via Cs -->
Ts = Ts' ∧ P \<turnstile> T' ≤ T"
using prems
proof (induct rule:rtrancl.induct)
fix C
assume Cleast:"P \<turnstile> C has least M = (Ts',T',m') via Ds"
{ fix Ts T m Cs
assume Chas:"P \<turnstile> C has M = (Ts,T,m) via Cs"
with Cleast have path:"P,C \<turnstile> Ds \<sqsubseteq> Cs"
by (fastsimp simp:LeastMethodDef_def HasMethodDef_def)
{ assume "Ds = Cs"
with Cleast Chas have "Ts = Ts' ∧ T' = T"
by (auto simp:LeastMethodDef_def HasMethodDef_def MethodDefs_def)
hence "Ts = Ts' ∧ P \<turnstile> T' ≤ T" by auto }
moreover
{ assume "(Ds,Cs) ∈ (leq_path1 P C)+"
hence subcls:"(last Ds,last Cs) ∈ (subcls1 P)+" using wf
by -(rule last_leq_paths)
from Chas obtain Bs fs ms where "class P (last Cs) = Some(Bs,fs,ms)"
and "map_of ms M = Some(Ts,T,m)"
by (auto simp:HasMethodDef_def MethodDefs_def)
hence ex:"∀Bs' fs' ms' Ts' T' m'. class P (last Ds) = Some(Bs',fs',ms') ∧
map_of ms' M = Some(Ts',T',m') --> Ts = Ts' ∧ P \<turnstile> T' ≤ T"
using subcls wf
by -(rule subclsPlus_subtype,auto)
from Cleast obtain Bs' fs' ms' where "class P (last Ds) = Some(Bs',fs',ms')"
and "map_of ms' M = Some(Ts',T',m')"
by (auto simp:LeastMethodDef_def MethodDefs_def)
with ex have "Ts = Ts'" and "P \<turnstile> T' ≤ T" by auto }
ultimately have "Ts = Ts'" and "P \<turnstile> T' ≤ T" using path
by (auto dest!:rtranclD) }
thus "∀Ts T m Cs. P \<turnstile> C has M = (Ts, T, m) via Cs -->
Ts = Ts' ∧ P \<turnstile> T' ≤ T"
by (simp add:HasMethodDef_def MethodDefs_def)
next
fix D C' C
assume DleqC':"P \<turnstile> D \<preceq>* C'" and C'leqC:"P \<turnstile> C' \<prec>1 C"
and Dleast:"P \<turnstile> D has least M = (Ts',T',m') via Ds"
and IH:"[|P \<turnstile> D has least M = (Ts',T',m') via Ds; wf_prog wf_md P|]
==> ∀Ts T m Cs. P \<turnstile> C' has M = (Ts, T, m) via Cs -->
Ts = Ts' ∧ P \<turnstile> T' ≤ T"
{ fix Ts T m Cs
assume Chas:"P \<turnstile> C has M = (Ts,T,m) via Cs"
from Dleast have classD:"is_class P D"
by (auto intro:Subobjs_isClass simp:LeastMethodDef_def MethodDefs_def)
from DleqC' C'leqC have "P \<turnstile> D \<preceq>* C" by simp
then obtain Cs' where "P \<turnstile> Path D to C via Cs'" using classD wf
by (auto dest:leq_implies_path)
hence Dhas:"P \<turnstile> D has M = (Ts,T,m) via Cs'@pCs" using Chas wf
by (fastsimp intro:has_path_has)
with Dleast have path:"P,D \<turnstile> Ds \<sqsubseteq> Cs'@pCs"
by (auto simp:LeastMethodDef_def HasMethodDef_def)
{ assume "Ds = Cs'@pCs"
with Dleast Dhas have "Ts = Ts' ∧ T' = T"
by (auto simp:LeastMethodDef_def HasMethodDef_def MethodDefs_def)
hence "Ts = Ts' ∧ T' = T" by auto }
moreover
{ assume "(Ds,Cs'@pCs) ∈ (leq_path1 P D)+"
hence subcls:"(last Ds,last (Cs'@pCs)) ∈ (subcls1 P)+" using wf
by -(rule last_leq_paths)
from Dhas obtain Bs fs ms where "class P (last (Cs'@pCs)) = Some(Bs,fs,ms)"
and "map_of ms M = Some(Ts,T,m)"
by (auto simp:HasMethodDef_def MethodDefs_def)
hence ex:"∀Bs' fs' ms' Ts' T' m'. class P (last Ds) = Some(Bs',fs',ms') ∧
map_of ms' M = Some(Ts',T',m') -->
Ts = Ts' ∧ P \<turnstile> T' ≤ T"
using subcls wf
by -(rule subclsPlus_subtype,auto)
from Dleast obtain Bs' fs' ms' where "class P (last Ds) = Some(Bs',fs',ms')"
and "map_of ms' M = Some(Ts',T',m')"
by (auto simp:LeastMethodDef_def MethodDefs_def)
with ex have "Ts = Ts'" and "P \<turnstile> T' ≤ T" by auto }
ultimately have "Ts = Ts'" and "P \<turnstile> T' ≤ T" using path
by (auto dest!:rtranclD) }
thus "∀Ts T m Cs. P \<turnstile> C has M = (Ts, T, m) via Cs -->
Ts = Ts' ∧ P \<turnstile> T' ≤ T"
by simp
qed
lemma leq_methods_subtypes:
assumes leq:"P \<turnstile> D \<preceq>* C" and least:"(Ds,(Ts',T',m')) ∈ MinimalMethodDefs P D M"
and wf:"wf_prog wf_md P"
shows "∀Ts T m Cs Cs'. P \<turnstile> Path D to C via Cs' ∧ P,D \<turnstile> Ds \<sqsubseteq> Cs'@pCs ∧ Cs ≠ [] ∧
P \<turnstile> C has M = (Ts,T,m) via Cs
--> Ts = Ts' ∧ P \<turnstile> T' ≤ T"
using prems
proof (induct rule:rtrancl.induct)
fix C
assume Cleast:"(Ds,(Ts',T',m')) ∈ MinimalMethodDefs P C M"
{ fix Ts T m Cs Cs'
assume path':"P \<turnstile> Path C to C via Cs'"
and leq_path:"P,C \<turnstile> Ds \<sqsubseteq> Cs' @p Cs" and notempty:"Cs ≠ []"
and Chas:"P \<turnstile> C has M = (Ts,T,m) via Cs"
from path' wf have Cs':"Cs' = [C]" by(rule path_via_C)
from leq_path Cs' notempty have leq':"P,C \<turnstile> Ds \<sqsubseteq> Cs"
by(auto simp:appendPath_def split:split_if_asm)
{ assume "Ds = Cs"
with Cleast Chas have "Ts = Ts' ∧ T' = T"
by (auto simp:MinimalMethodDefs_def HasMethodDef_def MethodDefs_def)
hence "Ts = Ts' ∧ P \<turnstile> T' ≤ T" by auto }
moreover
{ assume "(Ds,Cs) ∈ (leq_path1 P C)+"
hence subcls:"(last Ds,last Cs) ∈ (subcls1 P)+" using wf
by -(rule last_leq_paths)
from Chas obtain Bs fs ms where "class P (last Cs) = Some(Bs,fs,ms)"
and "map_of ms M = Some(Ts,T,m)"
by (auto simp:HasMethodDef_def MethodDefs_def)
hence ex:"∀Bs' fs' ms' Ts' T' m'. class P (last Ds) = Some(Bs',fs',ms') ∧
map_of ms' M = Some(Ts',T',m') --> Ts = Ts' ∧ P \<turnstile> T' ≤ T"
using subcls wf
by -(rule subclsPlus_subtype,auto)
from Cleast obtain Bs' fs' ms' where "class P (last Ds) = Some(Bs',fs',ms')"
and "map_of ms' M = Some(Ts',T',m')"
by (auto simp:MinimalMethodDefs_def MethodDefs_def)
with ex have "Ts = Ts'" and "P \<turnstile> T' ≤ T" by auto }
ultimately have "Ts = Ts'" and "P \<turnstile> T' ≤ T" using leq'
by (auto dest!:rtranclD) }
thus "∀Ts T m Cs Cs'. P \<turnstile> Path C to C via Cs' ∧ P,C \<turnstile> Ds \<sqsubseteq> Cs' @p Cs ∧ Cs ≠ [] ∧
P \<turnstile> C has M = (Ts, T, m) via Cs -->
Ts = Ts' ∧ P \<turnstile> T' ≤ T" by blast
next
fix D C' C
assume DleqC':"P \<turnstile> D \<preceq>* C'" and C'leqC:"P \<turnstile> C' \<prec>1 C"
and Dleast:"(Ds, Ts', T', m') ∈ MinimalMethodDefs P D M"
and IH:"[|(Ds,Ts',T',m') ∈ MinimalMethodDefs P D M; wf_prog wf_md P|]
==> ∀Ts T m Cs Cs'. P \<turnstile> Path D to C' via Cs' ∧
P,D \<turnstile> Ds \<sqsubseteq> Cs' @p Cs ∧ Cs ≠ [] ∧ P \<turnstile> C' has M = (Ts, T, m) via Cs -->
Ts = Ts' ∧ P \<turnstile> T' ≤ T"
{ fix Ts T m Cs Cs'
assume path:"P \<turnstile> Path D to C via Cs'"
and leq_path:"P,D \<turnstile> Ds \<sqsubseteq> Cs' @p Cs"
and notempty:"Cs ≠ []"
and Chas:"P \<turnstile> C has M = (Ts,T,m) via Cs"
from Dleast have classD:"is_class P D"
by (auto intro:Subobjs_isClass simp:MinimalMethodDefs_def MethodDefs_def)
from path have Dhas:"P \<turnstile> D has M = (Ts,T,m) via Cs'@pCs" using Chas wf
by (fastsimp intro:has_path_has)
{ assume "Ds = Cs'@pCs"
with Dleast Dhas have "Ts = Ts' ∧ T' = T"
by (auto simp:MinimalMethodDefs_def HasMethodDef_def MethodDefs_def)
hence "Ts = Ts' ∧ T' = T" by auto }
moreover
{ assume "(Ds,Cs'@pCs) ∈ (leq_path1 P D)+"
hence subcls:"(last Ds,last (Cs'@pCs)) ∈ (subcls1 P)+" using wf
by -(rule last_leq_paths)
from Dhas obtain Bs fs ms where "class P (last (Cs'@pCs)) = Some(Bs,fs,ms)"
and "map_of ms M = Some(Ts,T,m)"
by (auto simp:HasMethodDef_def MethodDefs_def)
hence ex:"∀Bs' fs' ms' Ts' T' m'. class P (last Ds) = Some(Bs',fs',ms') ∧
map_of ms' M = Some(Ts',T',m') -->
Ts = Ts' ∧ P \<turnstile> T' ≤ T"
using subcls wf
by -(rule subclsPlus_subtype,auto)
from Dleast obtain Bs' fs' ms' where "class P (last Ds) = Some(Bs',fs',ms')"
and "map_of ms' M = Some(Ts',T',m')"
by (auto simp:MinimalMethodDefs_def MethodDefs_def)
with ex have "Ts = Ts'" and "P \<turnstile> T' ≤ T" by auto }
ultimately have "Ts = Ts'" and "P \<turnstile> T' ≤ T" using leq_path
by (auto dest!:rtranclD) }
thus "∀Ts T m Cs Cs'. P \<turnstile> Path D to C via Cs' ∧ P,D \<turnstile> Ds \<sqsubseteq> Cs' @p Cs ∧ Cs ≠ [] ∧
P \<turnstile> C has M = (Ts, T, m) via Cs -->
Ts = Ts' ∧ P \<turnstile> T' ≤ T"
by blast
qed
lemma select_least_methods_subtypes:
assumes select_method:"P \<turnstile> (C,Cs@pDs) selects M = (Ts,T,pns,body) via Cs'"
and least_method:"P \<turnstile> last Cs has least M = (Ts',T',pns',body') via Ds"
and path:"P \<turnstile> Path C to (last Cs) via Cs"
and wf:"wf_prog wf_md P"
shows "Ts' = Ts ∧ P \<turnstile> T ≤ T'"
using select_method
proof -
from path have sub:"P \<turnstile> C \<preceq>* last Cs"
by(fastsimp intro:Subobjs_subclass simp:path_via_def)
from least_method have has:"P \<turnstile> last Cs has M = (Ts',T',pns',body') via Ds"
by(rule has_least_method_has_method)
from select_method show ?thesis
proof cases
case dyn_unique
hence dyn:"P \<turnstile> C has least M = (Ts,T,pns,body) via Cs'" by simp
with sub has wf show ?thesis
by -(drule leq_method_subtypes,assumption,simp,blast)+
next
case dyn_ambiguous
hence overrider:"P \<turnstile> (C,Cs@pDs) has overrider M = (Ts,T,pns,body) via Cs'"
by simp
from least_method have notempty:"Ds ≠ []"
by(auto intro!:Subobjs_nonempty simp:LeastMethodDef_def MethodDefs_def)
have "last Cs = hd Ds ==> last (Cs @ tl Ds) = last Ds"
proof(cases "tl Ds = []")
case True
assume last:"last Cs = hd Ds"
with True notempty have "Ds = [last Cs]" by (fastsimp dest:hd_Cons_tl)
hence "last Ds = last Cs" by simp
with True show ?thesis by simp
next
case False
assume last:"last Cs = hd Ds"
from notempty False have "last (tl Ds) = last Ds"
by -(drule hd_Cons_tl,drule_tac x="hd Ds" in last_ConsR,simp)
with False show ?thesis by simp
qed
hence eq:"(Cs @p Ds) @p [last Ds] = (Cs @p Ds)"
by(simp add:appendPath_def)
from least_method wf
have "P \<turnstile> last Ds has least M = (Ts',T',pns',body') via [last Ds]"
by(auto dest:Subobj_last_isClass intro:Subobjs_Base subobjs_rel
simp:LeastMethodDef_def MethodDefs_def)
with notempty
have "P \<turnstile> last (Cs@pDs) has least M = (Ts',T',pns',body') via [last Ds]"
by -(drule_tac Cs'="Cs" in appendPath_last,simp)
with overrider wf eq have "(Cs',Ts,T,pns,body) ∈ MinimalMethodDefs P C M"
and "P,C \<turnstile> Cs' \<sqsubseteq> Cs @p Ds"
by -(auto simp:FinalOverriderMethodDef_def OverriderMethodDefs_def,
drule wf_sees_method_fun,auto)
with sub wf path notempty has show ?thesis
by -(drule leq_methods_subtypes,simp_all,blast)+
qed
qed
lemma wf_syscls:
"set SystemClasses ⊆ set P ==> wf_syscls P"
by (simp add: image_def SystemClasses_def wf_syscls_def sys_xcpts_def
NullPointerC_def ClassCastC_def OutOfMemoryC_def,force intro:conjI)
section{* Well formedness and widen *}
lemma Class_widen: "[|P \<turnstile> Class C ≤ T; wf_prog wf_md P; is_class P C|]
==> ∃D. T = Class D ∧ P \<turnstile> Path C to D unique"
apply (ind_cases "P \<turnstile> Class C ≤ T")
apply (auto intro:path_C_to_C_unique)
done
lemma Class_widen_Class [iff]: "[|wf_prog wf_md P; is_class P C|] ==>
(P \<turnstile> Class C ≤ Class D) = (P \<turnstile> Path C to D unique)"
apply (rule iffI)
apply (ind_cases " P \<turnstile> Class C ≤ Class D")
apply (auto elim: widen_subcls intro:path_C_to_C_unique)
done
lemma widen_Class: "[|wf_prog wf_md P; is_class P C|] ==>
(P \<turnstile> T ≤ Class C) =
(T = NT ∨ (∃D. T = Class D ∧ P \<turnstile> Path D to C unique))"
apply(induct T) apply (auto intro:widen_subcls)
apply (ind_cases "P \<turnstile> Class D ≤ Class C" for D) apply (auto intro:path_C_to_C_unique)
done
section{* Well formedness and well typing *}
lemma assumes wf:"wf_prog wf_md P"
shows WT_determ: "P,E \<turnstile> e :: T ==> (!!T'. P,E \<turnstile> e :: T' ==> T = T')"
and WTs_determ: "P,E \<turnstile> es [::] Ts ==> (!!Ts'. P,E \<turnstile> es [::] Ts' ==> Ts = Ts')"
proof(induct rule:WT_WTs_inducts)
case (WTDynCast E e D C)
have "P,E \<turnstile> Cast C e :: T'" by fact
thus ?case by (fastsimp elim:WT.cases)
next
case (WTStaticCast E e D C)
have "P,E \<turnstile> (|C|)),e :: T'" by fact
thus ?case by (fastsimp elim:WT.cases)
next
case (WTBinOp E e1 T1 e2 T2 T bop)
have bop:"case bop of Eq => T1 = T2 ∧ T = Boolean
| Add => T1 = Integer ∧ T2 = Integer ∧ T = Integer"
and wt:"P,E \<turnstile> e1 «bop» e2 :: T'" by fact+
from wt obtain T1' T2' where
bop':"case bop of Eq => T1' = T2' ∧ T' = Boolean
| Add => T1' = Integer ∧ T2' = Integer ∧ T' = Integer"
by auto
from bop show ?case
proof (cases bop)
assume Eq:"bop = Eq"
with bop have "T = Boolean" by auto
with Eq bop' show ?thesis by simp
next
assume Add:"bop = Add"
with bop have "T = Integer"
by auto
with Add bop' show ?thesis by simp
qed
next
case (WTLAss E V T e T' T'')
have "P,E \<turnstile> V:=e :: T''"
and "E V = Some T" by fact+
thus ?case by auto
next
case (WTFAcc E e C F T Cs)
have IH:"!!T'. P,E \<turnstile> e :: T' ==> Class C = T'"
and least:"P \<turnstile> C has least F:T via Cs"
and wt:"P,E \<turnstile> e•F{Cs} :: T'" by fact+
from wt obtain C' where wte':"P,E \<turnstile> e :: Class C'"
and least':"P \<turnstile> C' has least F:T' via Cs" by auto
from IH[OF wte'] have "C = C'" by simp
with least least' show ?case
by (fastsimp simp:sees_field_fun)
next
case (WTFAss E e1 C F T Cs e2 T' T'')
have least:"P \<turnstile> C has least F:T via Cs"
and wt:"P,E \<turnstile> e1•F{Cs} := e2 :: T''"
and IH:"!!S. P,E \<turnstile> e1 :: S ==> Class C = S" by fact+
from wt obtain C' where wte':"P,E \<turnstile> e1 :: Class C'"
and least':"P \<turnstile> C' has least F:T'' via Cs" by auto
from IH[OF wte'] have "C = C'" by simp
with least least' show ?case
by (fastsimp simp:sees_field_fun)
next
case (WTCall E e C M Ts T pns body Cs es Ts')
have IH:"!!T'. P,E \<turnstile> e :: T' ==> Class C = T'"
and least:"P \<turnstile> C has least M = (Ts, T, pns, body) via Cs"
and wt:"P,E \<turnstile> e•M(es) :: T'" by fact+
from wt obtain C' Ts' pns' body' Cs' where wte':"P,E \<turnstile> e :: Class C'"
and least':"P \<turnstile> C' has least M = (Ts',T',pns',body') via Cs'" by auto
from IH[OF wte'] have "C = C'" by simp
with least least' wf show ?case by (auto dest:wf_sees_method_fun)
next
case (WTStaticCall E e C' C M Ts T pns body Cs es Ts')
have IH:"!!T'. P,E \<turnstile> e :: T' ==> Class C' = T'"
and unique:"P \<turnstile> Path C' to C unique"
and least:"P \<turnstile> C has least M = (Ts, T, pns, body) via Cs"
and wt:"P,E \<turnstile> e•(C::)M(es) :: T'" by fact+
from wt obtain Ts' pns' body' Cs'
where "P \<turnstile> C has least M = (Ts',T',pns',body') via Cs'" by auto
with least wf show ?case by (auto dest:wf_sees_method_fun)
next
case WTBlock thus ?case by (clarsimp simp del:fun_upd_apply)
next
case (WTSeq E e1 T1 e2 T2)
have IH:"!!T'. P,E \<turnstile> e2 :: T' ==> T2 = T'"
and wt:"P,E \<turnstile> e1;; e2 :: T'" by fact+
from wt have wt':"P,E \<turnstile> e2 :: T'" by auto
from IH[OF wt'] show ?case .
next
case (WTCond E e e1 T e2)
have IH:"!!S. P,E \<turnstile> e1 :: S ==> T = S"
and wt:"P,E \<turnstile> if (e) e1 else e2 :: T'" by fact+
from wt have "P,E \<turnstile> e1 :: T'" by auto
from IH[OF this] show ?case .
next
case (WTCons E e T es Ts)
have IHe:"!!T'. P,E \<turnstile> e :: T' ==> T = T'"
and IHes:"!!Ts'. P,E \<turnstile> es [::] Ts' ==> Ts = Ts'"
and wt:"P,E \<turnstile> e # es [::] Ts'" by fact+
from wt show ?case
proof (cases Ts')
case Nil with wt show ?thesis by simp
next
case (Cons T'' Ts'')
with wt have wte':"P,E \<turnstile> e :: T''" and wtes':"P,E \<turnstile> es [::] Ts''"
by auto
from IHe[OF wte'] IHes[OF wtes'] Cons show ?thesis by simp
qed
qed clarsimp+
end