# Theory WellForm

(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Based on the Jinja theory Common/WellForm.thy by Tobias Nipkow
*)

section ‹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 ‹WellType›).

CoreC++ allows covariant return types›

type_synonym wf_mdecl_test = "prog ⇒ cname ⇒ mdecl ⇒ bool"

definition wf_fdecl :: "prog ⇒ fdecl ⇒ bool" where
"wf_fdecl P ≡ λ(F,T). is_type P T"

definition wf_mdecl :: "wf_mdecl_test ⇒ wf_mdecl_test" where
"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)"

definition wf_cdecl :: "wf_mdecl_test ⇒ prog ⇒ cdecl ⇒ bool" where
"wf_cdecl wf_md P  ≡  λ(C,(Bs,fs,ms)).
(∀M mthd Cs. P ⊢ C has M = mthd via Cs ⟶
(∃mthd' Cs'. P ⊢ (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 ⊢ D ≼⇧* C ∧
(∀(M,Ts,T,m)∈set ms.
∀Ts' T' m' Cs. P ⊢ D has M = (Ts',T',m') via Cs ⟶
Ts' = Ts ∧ P ⊢ T ≤ T'))"

definition wf_syscls :: "prog ⇒ bool" where
"wf_syscls P  ≡  sys_xcpts ⊆ set(map fst P)"

definition wf_prog :: "wf_mdecl_test ⇒ prog ⇒ bool" where
"wf_prog wf_md P ≡ wf_syscls P ∧ distinct_fst P ∧
(∀c ∈ set P. wf_cdecl wf_md P c)"

subsection‹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 (fastforce 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 assms 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

subsection‹Well-formedness subclass lemmas›

lemma subcls1_wfD:
"⟦ P ⊢ C ≺⇧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

subsection‹Well-formedness leq\_path lemmas›

lemma last_leq_path:
assumes leq:"P,C ⊢ Cs ⊏⇧1 Ds" and wf:"wf_prog wf_md P"
shows "P ⊢ last Cs ≺⇧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 ⊢ last Cs ≺⇧1 last Ds" by (fastforce intro:subclsR_subcls1 Subobjs_subclsR)
next
fix Cs D assume "P ⊢ last Cs ≺⇩S D"
thus "P ⊢ last Cs ≺⇧1 last [D]" by (fastforce 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 ⊢ Cs ⊏⇧1 Ds"
thus "(last Cs, last Ds) ∈ (subcls1 P)⇧+" using wf
by (fastforce intro:r_into_trancl elim:last_leq_path)
next
fix Cs Cs' Ds assume "(last Cs, last Cs') ∈ (subcls1 P)⇧+"
and "P,C ⊢ Cs' ⊏⇧1 Ds"
thus "(last Cs, last Ds) ∈ (subcls1 P)⇧+" using wf
by (fastforce dest:last_leq_path)
qed

lemma leq_path1_wfD:
"⟦ P,C ⊢ Cs ⊏⇧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 ⊢ Cs ⊑ Cs'; P,C ⊢ Cs' ⊑ 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 ⊢ [C] ⊑ 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)

subsection‹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 (fastforce dest:subcls1D class_wf elim:wf_cdecl_supD)
apply (fastforce dest:subcls1D class_wf elim:wf_cdecl_supD)
done

lemma converse_SubobjsR_Rep:
"⟦Subobjs⇩R P C Cs; P ⊢ last Cs ≺⇩R C'; wf_prog wf_md P⟧
⟹ Subobjs⇩R P C (Cs@[C'])"

apply (induct rule:Subobjs⇩R.induct)
apply (frule subclsR_subcls1)
apply (fastforce dest!:subcls1D class_wf wf_cdecl_supD SubobjsR_Base SubobjsR_Rep)
apply (fastforce elim:SubobjsR_Rep simp: SubobjsR_nonempty split:if_split_asm)
done

lemma converse_Subobjs_Rep:
"⟦Subobjs P C Cs; P ⊢ last Cs ≺⇩R C';  wf_prog wf_md P⟧
⟹ Subobjs P C (Cs@[C'])"
by (induct rule:Subobjs.induct, fastforce dest:converse_SubobjsR_Rep Subobjs_Rep,
fastforce 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 (fastforce elim:converse_rtranclE dest:subclsS_subcls1 elim:subcls1_class)
with True show ?thesis by (fastforce intro:Subobjs_Base)
next
case False
have "is_subobj P ((C,C'#rev []))" by fact
with False obtain D where sup:"P ⊢ C ≼⇧* D" and subS:"P ⊢ D ≺⇩S C'"
by fastforce
with wf have "is_class P C'"
by (fastforce dest:subclsS_subcls1 subcls1D class_wf elim:wf_cdecl_supD)
hence "Subobjs⇩R P C' [C']" by (fastforce 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 ⊢ last(butlast(C'#D#Ds)) ≺⇩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 ⊢ last(C'#rev Cs'') ≺⇩R C''" by simp
with suborev wf show ?case by (fastforce 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 (fastforce intro: subclsR_subcls1 Subobjs_subclsR)
next
case False
with revset have hd:"(C',hd Ds) ∈ (subcls1 P)⇧+"
apply -
apply (erule ballE)
apply simp
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 (fastforce dest:subo_trans_subcls)
with wf have "∀C'' ∈ set Cs'. C' ≠ C''"
by (auto dest:subcls_irrefl)
thus ?thesis by fastforce
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 (fastforce intro: subclsR_subcls1 Subobjs_subclsR)
apply simp
apply (rule_tac b="a" in trancl_rtrancl_trancl)
apply (fastforce intro: subclsR_subcls1 Subobjs_subclsR)
apply (subgoal_tac "P ⊢ a ≼⇧* 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 fastforce
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 (fastforce dest:subo_subcls_trans)
with wf have "∀C'' ∈ set Cs. C' ≠ C''"
by (auto dest:subcls_irrefl)
thus ?thesis by fastforce
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 ⊢ X ≺⇧1 C"
by (fastforce intro:subclsR_subcls1 Subobjs_subclsR)
from suboX wf have "P ⊢ C ≼⇧* last ((rev Xs)@[X])"
by (fastforce intro:Subobjs_subclass appendSubobj)
with leq have "(C,C) ∈ (subcls1 P)⇧+" by simp
with wf show ?thesis by (fastforce 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 (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 (fastforce 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 (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 ⊢ C ≼⇧* D" and wf:"wf_prog wf_md P"
shows subcls_leq_path:"∃Cs. P,C ⊢ [C] ⊑ Cs@[D]"

using leq
proof (induct rule:rtrancl.induct)
fix C show "∃Cs. P,C ⊢ [C] ⊑ Cs@[C]" by (rule_tac x="[]" in exI,simp)
next
fix C C' D assume leq':"P ⊢ C ≼⇧* C'" and IH:"∃Cs. P,C ⊢ [C] ⊑ Cs@[C']"
and sub:"P ⊢ C' ≺⇧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 ⊢ [C] ⊑ Cs@[C']" by auto
hence subo:"Subobjs P C (Cs@[C'])" using "class" wf
by (fastforce intro:leq_path_Subobjs)
{ assume "P ⊢ C' ≺⇩R D"
with subo wf have "Subobjs P C (Cs@[C',D])"
by (fastforce dest:converse_Subobjs_Rep)
with subo have "P,C ⊢ (Cs@[C']) ⊏⇧1 (Cs@[C']@[D])"
by (fastforce intro:leq_path_rep) }
moreover
{ assume "P ⊢ C' ≺⇩S D"
with subo have "P,C ⊢ (Cs@[C']) ⊏⇧1 [D]" by (rule leq_path_sh) }
ultimately show "∃Cs. P,C ⊢ [C] ⊑ 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 ⊢ [C] ⊑ (rev Cs)"
using subo
proof (induct Cs)
case Nil
thus ?case by (fastforce 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 ⊢ [C] ⊑ 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 ⊢ C ≼⇧* D" and subS:"P ⊢ D ≺⇩S D'"
and suboR:"Subobjs⇩R P D' [C']"
by (auto elim:Subobjs.cases dest:hd_SubobjsR)
from suboR have C':"C' = D'" by (fastforce dest:hd_SubobjsR)
from leq wf obtain Ds where steps:"P,C ⊢ [C] ⊑ 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 "Subobjs⇩R P D [D]")
apply (fastforce dest:Subobjs_subclass intro:Subobjs_Sh)
apply (fastforce dest!:subclsSD intro:SubobjsR_Base wf_cdecl_supD
class_wf ShBaseclass_isBaseclass)
done
hence step:"P,C ⊢ (Ds@[D]) ⊏⇧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 (fastforce intro:butlast_Subobjs)
with IH have steps:"P,C ⊢ [C] ⊑ rev Cs'" by simp
from subo' subo'' have "P,C ⊢ rev Cs' ⊏⇧1 rev (C'#Cs')"
by (fastforce 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 ⊢ [C] ⊑ Cs"

proof -
obtain Cs' where Cs':"Cs' = rev Cs" by simp
with subo have "Subobjs P C (rev Cs')" by simp
hence "P,C ⊢ [C] ⊑ 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 ⊢ Cs ⊑ 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 ⊢ Cs ⊑ Cs'" and leq:"P,C ⊢ Cs' ⊏⇧1 Cs''"
and last:"last Cs = last Cs''"
and IH:"last Cs = last Cs' ⟹ Cs = Cs'"
from leq wf have sup1:"P ⊢ last Cs' ≺⇧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(fastforce 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(fastforce dest:subcls_irrefl) }
ultimately show "Cs = Cs''" using leqs
by(fastforce dest:rtranclD)
qed

subsection‹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 "¬ Subobjs⇩R P (last Cs) Ds")
apply (subgoal_tac "∃C' D. P ⊢ last Cs ≼⇧* C' ∧ P ⊢ C' ≺⇩S D ∧ Subobjs⇩R P D Ds")
apply clarsimp
apply (drule Subobjs_subclass)
apply (subgoal_tac "P ⊢ C ≼⇧* C'")
apply (erule_tac C'="C'" and D="D" in Subobjs_Sh)
apply simp
apply simp
apply fastforce
apply (erule Subobjs_notSubobjsR)
apply simp
apply (fastforce 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 (fastforce 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
then have "Cs' @ [C'] = last Cs # rev Ds'"
using append_butlast_last_id by blast
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 ⊢ C' ≺⇩R D'" by - (rule Subobjs_subclsR,simp)
with C' last have "P ⊢ last (Cs@tl(last Cs#rev Ds')) ≺⇩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(fastforce elim:appendPath2 appendPath1 simp:appendPath_def)

subsection‹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 (fastforce 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 ⊢ C'' ≺⇩R C'" by(fastforce intro:isSubobjs_subclsR Subobjs_isSubobj)
with wf show ?thesis
by (fastforce 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(fastforce 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(fastforce dest:appendSubobj)
with IH have dist:"distinct Cs'" by simp
from subo'' wf have "C' ∉ set (rev Cs')"
by(fastforce 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)"
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(fastforce 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}"

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)

subsection‹Well-formedness and Path›

lemma path_via_reverse:
assumes path_via:"P ⊢ Path C to D via Cs" and wf:"wf_prog wf_md P"
shows "∀Cs'. P ⊢ 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"
hence leq:"P ⊢ C ≼⇧* D" by(fastforce dest:Subobjs_subclass)
{ fix Cs' assume "P ⊢ Path D to C via Cs'"
hence subo':"Subobjs P D Cs'" and last':"last Cs' = C"
hence leq':"P ⊢ D ≼⇧* C" by(fastforce 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(fastforce intro:mdc_eq_last)
moreover have "Cs' = [C]" using CeqD subo' last' wf by(fastforce 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 ⊢ Cs ⊑ 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 ⊢ Cs ⊑ Cs'@ tl Cs"
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 ⊢ Path C to C via Cs; wf_prog wf_md P⟧ ⟹ Cs = [C]"
by (fastforce intro:mdc_eq_last simp:path_via_def)

lemma assumes wf:"wf_prog wf_md P"
and path_via:"P ⊢ Path last Cs to C via Cs'"
and path_via':"P ⊢ 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(fastforce 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(fastforce intro:mdc_eq_last simp:path_via_def) }
ultimately have eq:"Cs' = [last Cs]" using appendPath
with path_via have "C = last Cs"
with wf path_via' have "Cs'' = [last Cs]"
by simp(rule path_via_C)
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 ⊢ Path last Cs' to C via Ds"

proof
assume "P ⊢ 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 ≠ []"
with last' have "C ∈ set ((C#Cs')@⇩pDs)"
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 (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 (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 ⊢ last Cs' ≼⇧* C"
by (fastforce 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 ⊢ Y ≼⇧* 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 (fastforce elim:trancl_rtrancl_trancl)
qed
from lastleq X have leq:"P ⊢ X ≼⇧* C" by simp
with CleqX have "(C,C) ∈ (subcls1 P)⇧+"
by (rule trancl_rtrancl_trancl)
with wf show ?thesis by (fastforce dest:subcls_irrefl)
qed
qed

lemma leq_implies_path:
assumes leq:"P ⊢ C ≼⇧* D" and "class": "is_class P C"
and wf:"wf_prog wf_md P"
shows "∃Cs. P ⊢ Path C to D via Cs"

using leq "class"
proof(induct rule:rtrancl.induct)
fix C assume "is_class P C"
thus "∃Cs. P ⊢ Path C to C via Cs"
by (rule_tac x="[C]" in exI,fastforce intro:Subobjs_Base simp:path_via_def)
next
fix C C' D assume CleqC':"P ⊢ C ≼⇧* C'" and C'leqD:"P ⊢ C' ≺⇧1 D"
and classC:"is_class P C" and IH:"is_class P C ⟹ ∃Cs. P ⊢ 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 ⊢ Path C to D via Cs"
proof (auto dest!:subcls1_subclsR_or_subclsS)
assume "P ⊢ last Cs ≺⇩R D"
with subo have "Subobjs P C (Cs@[D])" using wf
by (rule converse_Subobjs_Rep)
thus ?thesis by (fastforce simp:path_via_def)
next
assume subS:"P ⊢ last Cs ≺⇩S D"
from CleqC' last have Cleqlast:"P ⊢ C ≼⇧* 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 (fastforce 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 (fastforce intro:Subobjs_Sh SubobjsR_Base)
thus ?thesis by (fastforce simp:path_via_def)
qed
qed

lemma least_method_implies_path_unique:
assumes least:"P ⊢ C has least M = (Ts,T,m) via Cs" and wf:"wf_prog wf_md P"
shows "P ⊢ Path C to (last Cs) unique"

(* Existence *)
from least have "Subobjs P C Cs"
thus "∃Cs'. Subobjs P C Cs' ∧ last Cs' = last Cs"
by fastforce
next
(* Uniqueness *)
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 ⊢ Cs ⊑ 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 ⊢ Cs ⊑ Cs'"
by simp
with wf lastCs' have eq:"Cs = Cs'" by(fastforce intro:leq_path_last)
from suboCs'' lastCs'' "class" map all have pathCs'':"P,C ⊢ Cs ⊑ Cs''"
by simp
with wf lastCs'' have "Cs = Cs''" by(fastforce intro:leq_path_last)
with eq show "Cs' = Cs''" by simp
qed

lemma least_field_implies_path_unique:
assumes least:"P ⊢ C has least F:T via Cs" and wf:"wf_prog wf_md P"
shows "P ⊢ Path C to (hd Cs) unique"

(* Existence *)
from least have "Subobjs P C Cs"
hence "Subobjs P C ([hd Cs]@tl Cs)"
by - (frule Subobjs_nonempty,simp)
with wf have "Subobjs P C [hd Cs]"
by (fastforce intro:appendSubobj)
thus "∃Cs'. Subobjs P C Cs' ∧ last Cs' = hd Cs"
by fastforce
next
(* Uniqueness *)
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 ⊢ Cs ⊑ 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 ⊢ Cs ⊑ 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 ⊢ Cs ⊑ 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 ⊢ C has least F:T via Cs; wf_prog wf_md P⟧
⟹ P ⊢ Path C to (hd Cs) via [hd Cs]"

apply clarsimp
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 ⊢ 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. Subobjs⇩R 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 ⊢ Path C to D unique" and leq:"P ⊢ C ≼⇧* C'"
and leqR:"(C',D) ∈ (subclsR P)⇧*" and wf:"wf_prog wf_md P"
shows "P ⊢ 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 ⊢ Path C to C' via Cs"
by (auto dest:leq_implies_path)
with wf have classC':"is_class P C'"
by (fastforce intro:Subobj_last_isClass simp:path_via_def)
with leqR wf obtain Cs' where subo:"Subobjs⇩R P C' Cs'" and last:"last Cs' = D"
by (auto dest:leqR_SubobjsR)
hence hd:"hd Cs' = C'"
by (fastforce 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'"
{ fix Cs'' assume path_via2:"P ⊢ 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

subsection‹Well-formedness and member lookup›

lemma has_path_has:
"⟦P ⊢ Path D to C via Ds; P ⊢ C has M = (Ts,T,m) via Cs; wf_prog wf_md P⟧
⟹ P ⊢ 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,
fastforce intro:Subobjs_appendPath simp:path_via_def)

lemma has_least_wf_mdecl:
"⟦ wf_prog wf_md P; P ⊢ C has least M = m via Cs ⟧
⟹ wf_mdecl wf_md P (last Cs) (M,m)"
by(fastforce 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 ⊢ (C,Cs) has overrider M = m via Cs' ⟧
⟹ wf_mdecl wf_md P (last Cs') (M,m)"
by(fastforce 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 ⊢ (C,Cs) selects M = m via Cs' ⟧
⟹ wf_mdecl wf_md P (last Cs') (M,m)"
by(fastforce elim:SelectMethodDef.induct
intro:has_least_wf_mdecl has_overrider_wf_mdecl)

lemma wf_sees_method_fun:
"⟦P ⊢ C has least M = mthd via Cs; P ⊢ 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 ⊢ (C,Cs) selects M = mthd via Cs'; P ⊢ (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 ⊢ (C, Cs) selects M = mthd' via Cs''"
and "P ⊢ 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 ⊢ D has least M' = mthd' via Ds'"
and "P ⊢ 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 ⊢ D has least M' = mthd via Cs'"
and "P ⊢ 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 ⊢ (C, Cs) selects M = mthd' via Cs''"
and "P ⊢ (C, Cs) has overrider M = mthd via Cs'"
and "∀mthd Cs'. ¬ P ⊢ 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 ⊢ D has least M' = mthd' via Ds'"
and "∀mthd Cs'. ¬ P ⊢ D has least M' = mthd via Cs'" by fact+
thus ?case by blast
next
case (dyn_ambiguous D M' Ds mthd' Ds')
have "P ⊢ (D, Ds) has overrider M' = mthd' via Ds'"
and "P ⊢ (D, Ds) has overrider M' = mthd via Cs'" by fact+
thus ?case by(fastforce dest:overrider_method_fun)
qed
qed

lemma least_field_is_type:
assumes field:"P ⊢ 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"
from this obtain Bs fs ms
where "map_of fs F = Some T"
and "class": "class P (last Cs) = Some (Bs,fs,ms)"
hence "(F,T) ∈ set fs" by (simp add:map_of_SomeD)
with "class" wf show ?thesis
by(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)
qed

lemma least_method_is_type:
assumes "method":"P ⊢ 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"
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)"
hence "(M,Ts,T,m) ∈ set ms" by (simp add:map_of_SomeD)
with "class" wf show ?thesis
by(fastforce dest!: class_wf simp: wf_cdecl_def wf_mdecl_def)
qed

lemma least_overrider_is_type:
assumes "method":"P ⊢ (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)"
hence "(M,Ts,T,m) ∈ set ms" by (simp add:map_of_SomeD)
with "class" wf show ?thesis
by(fastforce dest!: class_wf simp: wf_cdecl_def wf_mdecl_def)
qed

lemma select_method_is_type:
"⟦ P ⊢ (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 ⊢ C' has M = (Ts',T',m') via Cs@⇩p[D]; (M,Ts,T,m)∈set ms⟧
⟹ Ts' = Ts ∧ P ⊢ T ≤ T'"

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 ⊢ T ≤ T'"

using leq classD mapMs'
proof (erule_tac a="C" and b="D" in converse_trancl_induct)
fix C
assume CleqD:"P ⊢ C ≺⇧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 ⊢ D has M = (Ts',T',m') via [D]"
by (fastforce intro:Subobjs_Base simp:HasMethodDef_def MethodDefs_def is_class_def)
from CleqD classC have base:"D ∈ baseClasses Bs"
by (fastforce 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_SomeD)
with cdecl base hasViaD have "Ts' = Ts ∧ P ⊢ 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 ⊢ T ≤ T'" by blast
next
fix C C'
assume  classD1:"class P D = Some(Bs',fs',ms')" and CleqC':"P ⊢ C ≺⇧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 ⊢ 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 ⊢ D has M = (Ts',T',m') via [D]"
by (fastforce intro:Subobjs_Base simp:HasMethodDef_def MethodDefs_def is_class_def)
from subcls have C'leqD:"P ⊢ C' ≼⇧* D" by simp
from classC wf CleqC' have "is_class P C'"
by (fastforce intro:wf_cdecl_supD class_wf dest:subcls1D)
with C'leqD wf obtain Cs where "P ⊢ Path C' to D via Cs"
by (auto dest!:leq_implies_path simp:is_class_def)
hence hasVia:"P ⊢ 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 (fastforce 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_SomeD)
with cdecl base hasVia have "Ts' = Ts ∧ P ⊢ 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 ⊢ T ≤ T'" by blast
qed

lemma leq_method_subtypes:
assumes leq:"P ⊢ D ≼⇧* C" and least:"P ⊢ D has least M = (Ts',T',m') via Ds"
and wf:"wf_prog wf_md P"
shows "∀Ts T m Cs. P ⊢ C has M = (Ts,T,m) via Cs ⟶
Ts = Ts' ∧ P ⊢ T' ≤ T"
using assms
proof (induct rule:rtrancl.induct)
fix C
assume Cleast:"P ⊢ C has least M = (Ts',T',m') via Ds"
{ fix Ts T m Cs
assume Chas:"P ⊢ C has M = (Ts,T,m) via Cs"
with Cleast have path:"P,C ⊢ Ds ⊑ Cs"
by (fastforce 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 ⊢ 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 ⊢ 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 ⊢ T' ≤ T" by auto }
ultimately have "Ts = Ts'" and "P ⊢ T' ≤ T" using path
by (auto dest!:rtranclD) }
thus "∀Ts T m Cs. P ⊢ C has M = (Ts, T, m) via Cs ⟶
Ts = Ts' ∧ P ⊢ T' ≤ T"
next
fix D C' C
assume DleqC':"P ⊢ D ≼⇧* C'" and C'leqC:"P ⊢ C' ≺⇧1 C"
and Dleast:"P ⊢ D has least M = (Ts',T',m') via Ds"
and IH:"⟦P ⊢ D has least M = (Ts',T',m') via Ds; wf_prog wf_md P⟧
⟹ ∀Ts T m Cs. P ⊢ C' has M = (Ts, T, m) via Cs ⟶
Ts = Ts' ∧ P ⊢ T' ≤ T"
{ fix Ts T m Cs
assume Chas:"P ⊢ 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 ⊢ D ≼⇧* C" by simp
then obtain Cs' where "P ⊢ Path D to C via Cs'" using classD wf
by (auto dest:leq_implies_path)
hence Dhas:"P ⊢ D has M = (Ts,T,m) via Cs'@⇩pCs" using Chas wf
by (fastforce intro:has_path_has)
with Dleast have path:"P,D ⊢ Ds ⊑ 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 ⊢ 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 ⊢ T' ≤ T" by auto }
ultimately have "Ts = Ts'" and "P ⊢ T' ≤ T" using path
by (auto dest!:rtranclD) }
thus "∀Ts T m Cs. P ⊢ C has M = (Ts, T, m) via Cs ⟶
Ts = Ts' ∧ P ⊢ T' ≤ T"
by simp
qed

lemma leq_methods_subtypes:
assumes leq:"P ⊢ D ≼⇧* 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 ⊢ Path D to C via Cs' ∧ P,D ⊢ Ds ⊑ Cs'@⇩pCs ∧ Cs ≠ [] ∧
P ⊢ C has M = (Ts,T,m) via Cs
⟶  Ts = Ts' ∧ P ⊢ T' ≤ T"
using assms
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 ⊢ Path C to C via Cs'"
and leq_path:"P,C ⊢ Ds ⊑ Cs' @⇩p Cs" and notempty:"Cs ≠ []"
and Chas:"P ⊢ 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 ⊢ Ds ⊑ Cs"
by(auto simp:appendPath_def split:if_split_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 ⊢ 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 ⊢ 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 ⊢ T' ≤ T" by auto }
ultimately have "Ts = Ts'" and "P ⊢ T' ≤ T" using leq'
by (auto dest!:rtranclD) }
thus "∀Ts T m Cs Cs'. P ⊢ Path C to C via Cs' ∧ P,C ⊢ Ds ⊑ Cs' @⇩p Cs ∧ Cs ≠ [] ∧
P ⊢ C has M = (Ts, T, m) via Cs ⟶
Ts = Ts' ∧ P ⊢ T' ≤ T" by blast
next
fix D C' C
assume DleqC':"P ⊢ D ≼⇧* C'" and C'leqC:"P ⊢ C' ≺⇧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 ⊢ Path D to C' via Cs' ∧
P,D ⊢ Ds ⊑ Cs' @⇩p Cs ∧ Cs ≠ [] ∧ P ⊢ C' has M = (Ts, T, m) via Cs ⟶
Ts = Ts' ∧ P ⊢ T' ≤ T"
{ fix Ts T m Cs Cs'
assume path:"P ⊢ Path D to C via Cs'"
and leq_path:"P,D ⊢ Ds ⊑ Cs' @⇩p Cs"
and notempty:"Cs ≠ []"
and Chas:"P ⊢ 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 ⊢ D has M = (Ts,T,m) via Cs'@⇩pCs" using Chas wf
by (fastforce 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 ⊢ 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 ⊢ T' ≤ T" by auto }
ultimately have "Ts = Ts'" and "P ⊢ T' ≤ T" using leq_path
by (auto dest!:rtranclD) }
thus "∀Ts T m Cs Cs'. P ⊢ Path D to C via Cs' ∧ P,D ⊢ Ds ⊑ Cs' @⇩p Cs ∧ Cs ≠ [] ∧
P ⊢ C has M = (Ts, T, m) via Cs ⟶
Ts = Ts' ∧ P ⊢ T' ≤ T"
by blast
qed

lemma select_least_methods_subtypes:
assumes select_method:"P ⊢ (C,Cs@⇩pDs) selects M = (Ts,T,pns,body) via Cs'"
and least_method:"P ⊢ last Cs has least M = (Ts',T',pns',body') via Ds"
and path:"P ⊢ Path C to (last Cs) via Cs"
and wf:"wf_prog wf_md P"
shows "Ts' = Ts ∧ P ⊢ T ≤ T'"
using select_method
proof -
from path have sub:"P ⊢ C ≼⇧* last Cs"
by(fastforce intro:Subobjs_subclass simp:path_via_def)
from least_method have has:"P ⊢ 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 ⊢ 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 ⊢ (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 (fastforce 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)"
from least_method wf
have "P ⊢ 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 ⊢ 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 ⊢ Cs' ⊑ 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)

subsection‹Well formedness and widen›

lemma Class_widen: "⟦P ⊢ Class C ≤ T; wf_prog wf_md P; is_class P C⟧
⟹  ∃D. T = Class D ∧ P ⊢ Path C to D unique"

apply (ind_cases "P ⊢ 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 ⊢ Class C ≤ Class D) = (P ⊢ Path C to D unique)"

apply (rule iffI)
apply (ind_cases " P ⊢ 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 ⊢ T ≤ Class C) =
(T = NT ∨ (∃D. T = Class D ∧ P ⊢ Path D to C unique))"

apply(induct T) apply (auto intro:widen_subcls)
apply (ind_cases "P ⊢ Class D ≤ Class C" for D) apply (auto intro:path_C_to_C_unique)
done

subsection‹Well formedness and well typing›

lemma assumes wf:"wf_prog wf_md P"
shows WT_determ: "P,E ⊢ e :: T ⟹ (⋀T'. P,E ⊢ e :: T' ⟹ T = T')"
and WTs_determ: "P,E ⊢ es [::] Ts ⟹ (⋀Ts'. P,E ⊢ es [::] Ts' ⟹ Ts = Ts')"

proof(induct rule:WT_WTs_inducts)
case (WTDynCast E e D C)
have "P,E ⊢ Cast C e :: T'" by fact
thus ?case by (fastforce elim:WT.cases)
next
case (WTStaticCast E e D C)
have "P,E ⊢ ⦇C⦈e :: T'" by fact
thus ?case by (fastforce elim:WT.cases)
next
case (WTBinOp E e⇩1 T⇩1 e⇩2 T⇩2 bop T)
have bop:"case bop of Eq ⇒ T⇩1 = T⇩2 ∧ T = Boolean
| Add ⇒ T⇩1 = Integer ∧ T⇩2 = Integer ∧ T = Integer"
and wt:"P,E ⊢ e⇩1 «bop» e⇩2 :: 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
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 ⊢ 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 ⊢ e :: T' ⟹ Class C = T'"
and least:"P ⊢ C has least F:T via Cs"
and wt:"P,E ⊢ e∙F{Cs} :: T'" by fact+
from wt obtain C' where wte':"P,E ⊢ e :: Class C'"
and least':"P ⊢ C' has least F:T' via Cs" by auto
from IH[OF wte'] have "C = C'" by simp
with least least' show ?case
by (fastforce simp:sees_field_fun)
next
case (WTFAss E e⇩1 C F T Cs e⇩2 T' T'')
have least:"P ⊢ C has least F:T via Cs"
and wt:"P,E ⊢ e⇩1∙F{Cs} := e⇩2 :: T''"
and IH:"⋀S. P,E ⊢ e⇩1 :: S ⟹ Class C = S" by fact+
from wt obtain C' where wte':"P,E ⊢ e⇩1 :: Class C'"
and least':"P ⊢ C' has least F:T'' via Cs" by auto
from IH[OF wte'] have "C = C'" by simp
with least least' show ?case
by (fastforce simp:sees_field_fun)
next
case (WTCall E e C M Ts T pns body Cs es Ts')
have IH:"⋀T'. P,E ⊢ e :: T' ⟹ Class C = T'"
and least:"P ⊢ C has least M = (Ts, T, pns, body) via Cs"
and wt:"P,E ⊢ e∙M(es) :: T'" by fact+
from wt obtain C' Ts' pns' body' Cs' where wte':"P,E ⊢ e :: Class C'"
and least':"P ⊢ 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 ⊢ e :: T' ⟹ Class C' = T'"
and unique:"P ⊢ Path C' to C unique"
and least:"P ⊢ C has least M = (Ts, T, pns, body) via Cs"
and wt:"P,E ⊢ e∙(C::)M(es) :: T'" by fact+
from wt obtain Ts' pns' body' Cs'
where "P ⊢ 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 e⇩1 T⇩1 e⇩2 T⇩2)
have IH:"⋀T'. P,E ⊢ e⇩2 :: T' ⟹ T⇩2 = T'"
and wt:"P,E ⊢ e⇩1;; e⇩2 :: T'" by fact+
from wt have wt':"P,E ⊢ e⇩2 :: T'" by auto
from IH[OF wt'] show ?case .
next
case (WTCond E e e⇩1 T e⇩2)
have IH:"⋀S. P,E ⊢ e⇩1 :: S ⟹ T = S"
and wt:"P,E ⊢ if (e) e⇩1 else e⇩2 :: T'" by fact+
from wt have "P,E ⊢ e⇩1 :: T'" by auto
from IH[OF this] show ?case .
next
case (WTCons E e T es Ts)
have IHe:"⋀T'. P,E ⊢ e :: T' ⟹ T = T'"
and IHes:"⋀Ts'. P,E ⊢ es [::] Ts' ⟹ Ts = Ts'"
and wt:"P,E ⊢ 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 ⊢ e :: T''" and wtes':"P,E ⊢ es [::] Ts''"
by auto
from IHe[OF wte'] IHes[OF wtes'] Cons show ?thesis by simp
qed
qed clarsimp+

end