# Theory AxCompl

theory AxCompl
imports AxSem
(*  Title:      HOL/Bali/AxCompl.thy
Author:     David von Oheimb and Norbert Schirmer
*)

subsection ‹
Completeness proof for Axiomatic semantics of Java expressions and statements
›

theory AxCompl imports AxSem begin

text ‹
design issues:
\begin{itemize}
\item proof structured by Most General Formulas (-> Thomas Kleymann)
\end{itemize}
›

subsubsection "set of not yet initialzed classes"

definition
nyinitcls :: "prog ⇒ state ⇒ qtname set"
where "nyinitcls G s = {C. is_class G C ∧ ¬ initd C s}"

lemma nyinitcls_subset_class: "nyinitcls G s ⊆ {C. is_class G C}"
apply (unfold nyinitcls_def)
apply fast
done

lemmas finite_nyinitcls [simp] =
finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset]]

lemma card_nyinitcls_bound: "card (nyinitcls G s) ≤ card {C. is_class G C}"
apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]])
done

lemma nyinitcls_set_locals_cong [simp]:
"nyinitcls G (x,set_locals l s) = nyinitcls G (x,s)"

lemma nyinitcls_abrupt_cong [simp]: "nyinitcls G (f x, y) = nyinitcls G (x, y)"

lemma nyinitcls_abupd_cong [simp]: "nyinitcls G (abupd f s) = nyinitcls G s"

lemma card_nyinitcls_abrupt_congE [elim!]:
"card (nyinitcls G (x, s)) ≤ n ⟹ card (nyinitcls G (y, s)) ≤ n"
unfolding nyinitcls_def by auto

lemma nyinitcls_new_xcpt_var [simp]:
"nyinitcls G (new_xcpt_var vn s) = nyinitcls G s"
by (induct s) (simp_all add: nyinitcls_def)

lemma nyinitcls_init_lvars [simp]:
"nyinitcls G ((init_lvars G C sig mode a' pvs) s) = nyinitcls G s"
by (induct s) (simp add: init_lvars_def2 split: if_split)

lemma nyinitcls_emptyD: "⟦nyinitcls G s = {}; is_class G C⟧ ⟹ initd C s"
unfolding nyinitcls_def by fast

lemma card_Suc_lemma:
"⟦card (insert a A) ≤ Suc n; a∉A; finite A⟧ ⟹ card A ≤ n"
by auto

lemma nyinitcls_le_SucD:
"⟦card (nyinitcls G (x,s)) ≤ Suc n; ¬inited C (globs s); class G C=Some y⟧ ⟹
card (nyinitcls G (x,init_class_obj G C s)) ≤ n"
apply (subgoal_tac
"nyinitcls G (x,s) = insert C (nyinitcls G (x,init_class_obj G C s))")
apply  clarsimp
apply  (erule_tac V="nyinitcls G (x, s) = rhs" for rhs in thin_rl)
apply  (rule card_Suc_lemma [OF _ _ finite_nyinitcls])
apply   (auto dest!: not_initedD elim!:
simp add: nyinitcls_def inited_def split: if_split_asm)
done

lemma inited_gext': "⟦s≤|s';inited C (globs s)⟧ ⟹ inited C (globs s')"
by (rule inited_gext)

lemma nyinitcls_gext: "snd s≤|snd s' ⟹ nyinitcls G s' ⊆ nyinitcls G s"
unfolding nyinitcls_def by (force dest!: inited_gext')

lemma card_nyinitcls_gext:
"⟦snd s≤|snd s'; card (nyinitcls G s) ≤ n⟧⟹ card (nyinitcls G s') ≤ n"
apply (rule le_trans)
apply  (rule card_mono)
apply   (rule finite_nyinitcls)
apply  (erule nyinitcls_gext)
apply assumption
done

subsubsection "init-le"

definition
init_le :: "prog ⇒ nat ⇒ state ⇒ bool" ("_⊢init≤_"  [51,51] 50)
where "G⊢init≤n = (λs. card (nyinitcls G s) ≤ n)"

lemma init_le_def2 [simp]: "(G⊢init≤n) s = (card (nyinitcls G s)≤n)"
apply (unfold init_le_def)
apply auto
done

lemma All_init_leD:
"∀n::nat. G,(A::'a triple set)⊢{P ∧. G⊢init≤n} t≻ {Q::'a assn}
⟹ G,A⊢{P} t≻ {Q}"
apply (drule spec)
apply (erule conseq1)
apply clarsimp
apply (rule card_nyinitcls_bound)
done

subsubsection "Most General Triples and Formulas"

definition
remember_init_state :: "state assn" ("≐")
where "≐ ≡ λY s Z. s = Z"

lemma remember_init_state_def2 [simp]: "≐ Y = (=)"
apply (unfold remember_init_state_def)
apply (simp (no_asm))
done

definition
MGF ::"[state assn, term, prog] ⇒ state triple"   ("{_} _≻ {_→}"[3,65,3]62)
where "{P} t≻ {G→} = {P} t≻ {λY s' s. G⊢s ─t≻→ (Y,s')}"

definition
MGFn :: "[nat, term, prog] ⇒ state triple" ("{=:_} _≻ {_→}"[3,65,3]62)
where "{=:n} t≻ {G→} = {≐ ∧. G⊢init≤n} t≻ {G→}"

(* unused *)
lemma MGF_valid: "wf_prog G ⟹ G,{}⊨{≐} t≻ {G→}"
apply (unfold MGF_def)
apply (auto elim: evaln_eval)
done

lemma MGF_res_eq_lemma [simp]:
"(∀Y' Y s. Y = Y' ∧ P s ⟶ Q s) = (∀s. P s ⟶ Q s)"
by auto

lemma MGFn_def2:
"G,A⊢{=:n} t≻ {G→} = G,A⊢{≐ ∧. G⊢init≤n}
t≻ {λY s' s. G⊢s ─t≻→ (Y,s')}"
unfolding MGFn_def MGF_def by fast

lemma MGF_MGFn_iff:
"G,(A::state triple set)⊢{≐} t≻ {G→} = (∀n. G,A⊢{=:n} t≻ {G→})"
apply safe
apply  (erule_tac [2] All_init_leD)
apply (erule conseq1)
apply clarsimp
done

lemma MGFnD:
"G,(A::state triple set)⊢{=:n} t≻ {G→} ⟹
G,A⊢{(λY' s' s. s' = s           ∧ P s) ∧. G⊢init≤n}
t≻  {(λY' s' s. G⊢s─t≻→(Y',s') ∧ P s) ∧. G⊢init≤n}"
apply (unfold init_le_def)
apply (erule conseq12)
apply clarsimp
apply (erule (1) eval_gext [THEN card_nyinitcls_gext])
done
lemmas MGFnD' = MGFnD [of _ _ _ _ "λx. True"]

text ‹To derive the most general formula, we can always assume a normal
state in the precondition, since abrupt cases can be handled uniformally by
the abrupt rule.
›
lemma MGFNormalI: "G,A⊢{Normal ≐} t≻ {G→} ⟹
G,(A::state triple set)⊢{≐::state assn} t≻ {G→}"
apply (unfold MGF_def)
apply (rule ax_Normal_cases)
apply  (erule conseq1)
apply  clarsimp
apply (rule ax_derivs.Abrupt [THEN conseq1])
done

lemma MGFNormalD:
"G,(A::state triple set)⊢{≐} t≻ {G→} ⟹ G,A⊢{Normal ≐} t≻ {G→}"
apply (unfold MGF_def)
apply (erule conseq1)
apply clarsimp
done

text ‹Additionally to ‹MGFNormalI›, we also expand the definition of
the most general formula here›
lemma MGFn_NormalI:
"G,(A::state triple set)⊢{Normal((λY' s' s. s'=s ∧ normal s) ∧. G⊢init≤n)}t≻
{λY s' s. G⊢s ─t≻→ (Y,s')} ⟹ G,A⊢{=:n}t≻{G→}"
apply (rule ax_Normal_cases)
apply  (erule conseq1)
apply  clarsimp
apply (rule ax_derivs.Abrupt [THEN conseq1])
done

text ‹To derive the most general formula, we can restrict ourselves to
welltyped terms, since all others can be uniformally handled by the hazard
rule.›
lemma MGFn_free_wt:
"(∃T L C. ⦇prg=G,cls=C,lcl=L⦈⊢t∷T)
⟶ G,(A::state triple set)⊢{=:n} t≻ {G→}
⟹ G,A⊢{=:n} t≻ {G→}"
apply (rule MGFn_NormalI)
apply (rule ax_free_wt)
apply (auto elim: conseq12 simp add: MGFn_def MGF_def)
done

text ‹To derive the most general formula, we can restrict ourselves to
welltyped terms and assume that the state in the precondition conforms to the
environment. All type violations can be uniformally handled by the hazard
rule.›
lemma MGFn_free_wt_NormalConformI:
"(∀ T L C . ⦇prg=G,cls=C,lcl=L⦈⊢t∷T
⟶ G,(A::state triple set)
⊢{Normal((λY' s' s. s'=s ∧ normal s) ∧. G⊢init≤n) ∧. (λ s. s∷≼(G, L))}
t≻
{λY s' s. G⊢s ─t≻→ (Y,s')})
⟹ G,A⊢{=:n}t≻{G→}"
apply (rule MGFn_NormalI)
apply (rule ax_no_hazard)
apply (rule ax_escape)
apply (intro strip)
apply (simp only: type_ok_def peek_and_def)
apply (erule conjE)+
apply (erule exE,erule exE, erule exE, erule exE,erule conjE,drule (1) mp,
erule conjE)
apply (drule spec,drule spec, drule spec, drule (1) mp)
apply (erule conseq12)
apply blast
done

text ‹To derive the most general formula, we can restrict ourselves to
welltyped terms and assume that the state in the precondition conforms to the
environment and that the term is definetly assigned with respect to this state.
All type violations can be uniformally handled by the hazard rule.›
lemma MGFn_free_wt_da_NormalConformI:
"(∀ T L C B. ⦇prg=G,cls=C,lcl=L⦈⊢t∷T
⟶ G,(A::state triple set)
⊢{Normal((λY' s' s. s'=s ∧ normal s) ∧. G⊢init≤n) ∧. (λ s. s∷≼(G, L))
∧. (λ s. ⦇prg=G,cls=C,lcl=L⦈⊢dom (locals (store s))»t»B)}
t≻
{λY s' s. G⊢s ─t≻→ (Y,s')})
⟹ G,A⊢{=:n}t≻{G→}"
apply (rule MGFn_NormalI)
apply (rule ax_no_hazard)
apply (rule ax_escape)
apply (intro strip)
apply (simp only: type_ok_def peek_and_def)
apply (erule conjE)+
apply (erule exE,erule exE, erule exE, erule exE,erule conjE,drule (1) mp,
erule conjE)
apply (drule spec,drule spec, drule spec,drule spec, drule (1) mp)
apply (erule conseq12)
apply blast
done

subsubsection "main lemmas"

lemma MGFn_Init:
assumes mgf_hyp: "∀m. Suc m≤n ⟶ (∀t. G,A⊢{=:m} t≻ {G→})"
shows "G,(A::state triple set)⊢{=:n} ⟨Init C⟩⇩s≻ {G→}"
proof (rule MGFn_free_wt [rule_format],elim exE,rule MGFn_NormalI)
fix T L accC
assume "⦇prg=G, cls=accC, lcl= L⦈⊢⟨Init C⟩⇩s∷T"
hence is_cls: "is_class G C"
by cases simp
show "G,A⊢{Normal ((λY' s' s. s' = s ∧ normal s) ∧. G⊢init≤n)}
.Init C.
{λY s' s. G⊢s ─⟨Init C⟩⇩s≻→ (Y, s')}"
(is "G,A⊢{Normal ?P} .Init C. {?R}")
proof (rule ax_cases [where ?C="initd C"])
show "G,A⊢{Normal ?P  ∧. initd C} .Init C. {?R}"
by (rule ax_derivs.Done [THEN conseq1]) (fastforce intro: init_done)
next
have "G,A⊢{Normal (?P  ∧. Not ∘ initd C)} .Init C. {?R}"
proof (cases n)
case 0
with is_cls
show ?thesis
by - (rule ax_impossible [THEN conseq1],fastforce dest: nyinitcls_emptyD)
next
case (Suc m)
with mgf_hyp have mgf_hyp': "⋀ t. G,A⊢{=:m} t≻ {G→}"
by simp
from is_cls obtain c where c: "the (class G C) = c"
by auto
let ?Q= "(λY s' (x,s) .
G⊢ (x,init_class_obj G C s)
─ (if C=Object then Skip else Init (super (the (class G C))))→ s'
∧ x=None ∧ ¬inited C (globs s)) ∧. G⊢init≤m"
from c
show ?thesis
proof (rule ax_derivs.Init [where ?Q="?Q"])
let ?P' = "Normal ((λY s' s. s' = supd (init_class_obj G C) s
∧ normal s ∧ ¬ initd C s) ∧. G⊢init≤m)"
show "G,A⊢{Normal (?P ∧. Not ∘ initd C ;. supd (init_class_obj G C))}
.(if C = Object then Skip else Init (super c)).
{?Q}"
proof (rule conseq1 [where ?P'="?P'"])
show "G,A⊢{?P'} .(if C = Object then Skip else Init (super c)). {?Q}"
proof (cases "C=Object")
case True
have "G,A⊢{?P'} .Skip. {?Q}"
by (rule ax_derivs.Skip [THEN conseq1])
(auto simp add: True intro: eval.Skip)
with True show ?thesis
by simp
next
case False
from mgf_hyp'
have "G,A⊢{?P'} .Init (super c). {?Q}"
by (rule MGFnD' [THEN conseq12]) (fastforce simp add: False c)
with False show ?thesis
by simp
qed
next
from Suc is_cls
show "Normal (?P ∧. Not ∘ initd C ;. supd (init_class_obj G C))
⇒ ?P'"
by (fastforce elim: nyinitcls_le_SucD)
qed
next
from mgf_hyp'
show "∀l. G,A⊢{?Q ∧. (λs. l = locals (snd s)) ;. set_lvars Map.empty}
.init c.
{set_lvars l .; ?R}"
apply (rule MGFnD' [THEN conseq12, THEN allI])
apply (rule eval.Init [OF c])
apply (insert c)
apply auto
done
qed
qed
thus "G,A⊢{Normal ?P  ∧. Not ∘ initd C} .Init C. {?R}"
by clarsimp
qed
qed
lemmas MGFn_InitD = MGFn_Init [THEN MGFnD, THEN ax_NormalD]

lemma MGFn_Call:
assumes mgf_methds:
"∀C sig. G,(A::state triple set)⊢{=:n} ⟨(Methd C sig)⟩⇩e≻ {G→}"
and mgf_e: "G,A⊢{=:n} ⟨e⟩⇩e≻ {G→}"
and mgf_ps: "G,A⊢{=:n} ⟨ps⟩⇩l≻ {G→}"
and wf: "wf_prog G"
shows "G,A⊢{=:n} ⟨{accC,statT,mode}e⋅mn({pTs'}ps)⟩⇩e≻ {G→}"
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
note inj_term_simps [simp]
fix T L accC' E
assume wt: "⦇prg=G,cls=accC',lcl = L⦈⊢⟨({accC,statT,mode}e⋅mn( {pTs'}ps))⟩⇩e∷T"
then obtain pTs statDeclT statM where
wt_e: "⦇prg=G,cls=accC,lcl=L⦈⊢e∷-RefT statT" and
wt_args: "⦇prg=G,cls=accC,lcl=L⦈⊢ps∷≐pTs" and
statM: "max_spec G accC statT ⦇name=mn,parTs=pTs⦈
= {((statDeclT,statM),pTs')}" and
mode: "mode = invmode statM e" and
T: "T =Inl (resTy statM)" and
eq_accC_accC': "accC=accC'"
by cases fastforce+
let ?Q="(λY s1 (x,s) . x = None ∧
(∃a. G⊢Norm s ─e-≻a→ s1 ∧
(normal s1 ⟶ G, store s1⊢a∷≼RefT statT)
∧ Y = In1 a) ∧
(∃ P. normal s1
⟶ ⦇prg=G,cls=accC',lcl=L⦈⊢dom (locals (store s1))»⟨ps⟩⇩l»P))
∧. G⊢init≤n ∧. (λ s. s∷≼(G, L))::state assn"
let ?R="λa. ((λY (x2,s2) (x,s) . x = None ∧
(∃s1 pvs. G⊢Norm s ─e-≻a→ s1 ∧
(normal s1 ⟶ G, store s1⊢a∷≼RefT statT)∧
Y = ⌊pvs⌋⇩l ∧ G⊢s1 ─ps≐≻pvs→ (x2,s2)))
∧. G⊢init≤n ∧. (λ s. s∷≼(G, L)))::state assn"

show "G,A⊢{Normal ((λY' s' s. s' = s ∧ abrupt s = None) ∧. G⊢init≤n ∧.
(λs. s∷≼(G, L)) ∧.
(λs. ⦇prg=G, cls=accC',lcl=L⦈ ⊢ dom (locals (store s))
» ⟨{accC,statT,mode}e⋅mn( {pTs'}ps)⟩⇩e» E))}
{accC,statT,mode}e⋅mn( {pTs'}ps)-≻
{λY s' s. ∃v. Y = ⌊v⌋⇩e ∧
G⊢s ─{accC,statT,mode}e⋅mn( {pTs'}ps)-≻v→ s'}"
(is "G,A⊢{Normal ?P} {accC,statT,mode}e⋅mn( {pTs'}ps)-≻ {?S}")
proof (rule ax_derivs.Call [where ?Q="?Q" and ?R="?R"])
from mgf_e
show "G,A⊢{Normal ?P} e-≻ {?Q}"
proof (rule MGFnD' [THEN conseq12],clarsimp)
fix s0 s1 a
assume conf_s0: "Norm s0∷≼(G, L)"
assume da: "⦇prg=G,cls=accC',lcl=L⦈⊢
dom (locals s0) »⟨{accC,statT,mode}e⋅mn( {pTs'}ps)⟩⇩e» E"
assume eval_e: "G⊢Norm s0 ─e-≻a→ s1"
show "(abrupt s1 = None ⟶ G,store s1⊢a∷≼RefT statT) ∧
(abrupt s1 = None ⟶
(∃P. ⦇prg=G,cls=accC',lcl=L⦈⊢ dom (locals (store s1)) »⟨ps⟩⇩l» P))
∧ s1∷≼(G, L)"
proof -
from da obtain C where
da_e:  "⦇prg=G,cls=accC,lcl=L⦈⊢
dom (locals (store ((Norm s0)::state)))»⟨e⟩⇩e» C" and
da_ps: "⦇prg=G,cls=accC,lcl=L⦈⊢ nrm C »⟨ps⟩⇩l» E"
from eval_e conf_s0 wt_e da_e wf
obtain "(abrupt s1 = None ⟶ G,store s1⊢a∷≼RefT statT)"
and  "s1∷≼(G, L)"
by (rule eval_type_soundE) simp
moreover
{
assume normal_s1: "normal s1"
have "∃P. ⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »⟨ps⟩⇩l» P"
proof -
from eval_e wt_e da_e wf normal_s1
have "nrm C ⊆  dom (locals (store s1))"
by (cases rule: da_good_approxE') iprover
with da_ps show ?thesis
by (rule da_weakenE) iprover
qed
}
ultimately show ?thesis
using eq_accC_accC' by simp
qed
qed
next
show "∀a. G,A⊢{?Q←In1 a} ps≐≻ {?R a}" (is "∀ a. ?PS a")
proof
fix a
show "?PS a"
proof (rule MGFnD' [OF mgf_ps, THEN conseq12],
fix s0 s1 s2 vs
assume conf_s1: "s1∷≼(G, L)"
assume eval_e: "G⊢Norm s0 ─e-≻a→ s1"
assume conf_a: "abrupt s1 = None ⟶ G,store s1⊢a∷≼RefT statT"
assume eval_ps: "G⊢s1 ─ps≐≻vs→ s2"
assume da_ps: "abrupt s1 = None ⟶
(∃P. ⦇prg=G,cls=accC,lcl=L⦈⊢
dom (locals (store s1)) »⟨ps⟩⇩l» P)"
show "(∃s1. G⊢Norm s0 ─e-≻a→ s1 ∧
(abrupt s1 = None ⟶ G,store s1⊢a∷≼RefT statT) ∧
G⊢s1 ─ps≐≻vs→ s2) ∧
s2∷≼(G, L)"
proof (cases "normal s1")
case True
with da_ps obtain P where
"⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals (store s1)) »⟨ps⟩⇩l» P"
by auto
from eval_ps conf_s1 wt_args this wf
have "s2∷≼(G, L)"
by (rule eval_type_soundE)
with eval_e conf_a eval_ps
show ?thesis
by auto
next
case False
with eval_ps have "s2=s1" by auto
with eval_e conf_a eval_ps conf_s1
show ?thesis
by auto
qed
qed
qed
next
show "∀a vs invC declC l.
G,A⊢{?R a←⌊vs⌋⇩l ∧.
(λs. declC =
invocation_declclass G mode (store s) a statT
⦇name=mn, parTs=pTs'⦈ ∧
invC = invocation_class mode (store s) a statT ∧
l = locals (store s)) ;.
init_lvars G declC ⦇name=mn, parTs=pTs'⦈ mode a vs ∧.
(λs. normal s ⟶ G⊢mode→invC≼statT)}
Methd declC ⦇name=mn,parTs=pTs'⦈-≻
{set_lvars l .; ?S}"
(is "∀ a vs invC declC l. ?METHD a vs invC declC l")
proof (intro allI)
fix a vs invC declC l
from mgf_methds [rule_format]
show "?METHD a vs invC declC l"
proof (rule MGFnD' [THEN conseq12],clarsimp)
fix s4 s2 s1::state
fix s0 v
let ?D= "invocation_declclass G mode (store s2) a statT
⦇name=mn,parTs=pTs'⦈"
let ?s3= "init_lvars G ?D ⦇name=mn, parTs=pTs'⦈ mode a vs s2"
assume inv_prop: "abrupt ?s3=None
⟶ G⊢mode→invocation_class mode (store s2) a statT≼statT"
assume conf_s2: "s2∷≼(G, L)"
assume conf_a: "abrupt s1 = None ⟶ G,store s1⊢a∷≼RefT statT"
assume eval_e: "G⊢Norm s0 ─e-≻a→ s1"
assume eval_ps: "G⊢s1 ─ps≐≻vs→ s2"
assume eval_mthd: "G⊢?s3 ─Methd ?D ⦇name=mn,parTs=pTs'⦈-≻v→ s4"
show "G⊢Norm s0 ─{accC,statT,mode}e⋅mn( {pTs'}ps)-≻v
→ (set_lvars (locals (store s2))) s4"
proof -
obtain D where D: "D=?D" by simp
obtain s3 where s3: "s3=?s3" by simp
obtain s3' where
s3': "s3' = check_method_access G accC statT mode
⦇name=mn,parTs=pTs'⦈ a s3"
by simp
have eq_s3'_s3: "s3'=s3"
proof -
from inv_prop s3 mode
have "normal s3 ⟹
G⊢invmode statM e→invocation_class mode (store s2) a statT≼statT"
by auto
with eval_ps wt_e statM conf_s2 conf_a [rule_format]
have "check_method_access G accC statT (invmode statM e)
⦇name=mn,parTs=pTs'⦈ a s3 = s3"
by (rule error_free_call_access) (auto simp add: s3 mode wf)
thus ?thesis
qed
with eval_mthd D s3
have "G⊢s3' ─Methd D ⦇name=mn,parTs=pTs'⦈-≻v→ s4"
by simp
with eval_e eval_ps D _ s3'
show ?thesis
by (rule eval_Call) (auto simp add: s3 mode D)
qed
qed
qed
qed
qed

lemma eval_expression_no_jump':
assumes eval: "G⊢s0 ─e-≻v→ s1"
and   no_jmp: "abrupt s0 ≠ Some (Jump j)"
and      wt: "⦇prg=G, cls=C,lcl=L⦈⊢e∷-T"
and      wf: "wf_prog G"
shows "abrupt s1 ≠ Some (Jump j)"
using eval no_jmp wt wf
by - (rule eval_expression_no_jump
[where ?Env="⦇prg=G, cls=C,lcl=L⦈",simplified],auto)

text ‹To derive the most general formula for the loop statement, we need to
come up with a proper loop invariant, which intuitively states that we are
currently inside the evaluation of the loop. To define such an invariant, we
unroll the loop in iterated evaluations of the expression and evaluations of
the loop body.›

definition
unroll :: "prog ⇒ label ⇒ expr ⇒ stmt ⇒ (state ×  state) set" where
"unroll G l e c = {(s,t). ∃ v s1 s2.
G⊢s ─e-≻v→ s1 ∧ the_Bool v ∧ normal s1 ∧
G⊢s1 ─c→ s2 ∧ t=(abupd (absorb (Cont l)) s2)}"

lemma unroll_while:
assumes unroll: "(s, t) ∈ (unroll G l e c)⇧*"
and     eval_e: "G⊢t ─e-≻v→ s'"
and     normal_termination: "normal s'  ⟶ ¬ the_Bool v"
and     wt: "⦇prg=G,cls=C,lcl=L⦈⊢e∷-T"
and     wf: "wf_prog G"
shows "G⊢s ─l∙ While(e) c→ s'"
using unroll (* normal_s *)
proof (induct rule: converse_rtrancl_induct)
show "G⊢t ─l∙ While(e) c→ s'"
proof (cases "normal t")
case False
with eval_e have "s'=t" by auto
with False show ?thesis by auto
next
case True
note normal_t = this
show ?thesis
proof (cases "normal s'")
case True
with normal_t eval_e normal_termination
show ?thesis
by (auto intro: eval.Loop)
next
case False
note abrupt_s' = this
from eval_e _ wt wf
have no_cont: "abrupt s' ≠ Some (Jump (Cont l))"
by (rule eval_expression_no_jump') (insert normal_t,simp)
have
"if the_Bool v
then (G⊢s' ─c→ s' ∧
G⊢(abupd (absorb (Cont l)) s') ─l∙ While(e) c→ s')
else s' = s'"
proof (cases "the_Bool v")
case False thus ?thesis by simp
next
case True
with abrupt_s' have "G⊢s' ─c→ s'" by auto
moreover from abrupt_s' no_cont
have no_absorb: "(abupd (absorb (Cont l)) s')=s'"
by (cases s') (simp add: absorb_def split: if_split)
moreover
from no_absorb abrupt_s'
have "G⊢(abupd (absorb (Cont l)) s') ─l∙ While(e) c→ s'"
by auto
ultimately show ?thesis
using True by simp
qed
with eval_e
show ?thesis
using normal_t by (auto intro: eval.Loop)
qed
qed
next
fix s s3
assume unroll: "(s,s3) ∈ unroll G l e c"
assume while: "G⊢s3 ─l∙ While(e) c→ s'"
show "G⊢s ─l∙ While(e) c→ s'"
proof -
from unroll obtain v s1 s2 where
normal_s1: "normal s1" and
eval_e: "G⊢s ─e-≻v→ s1" and
continue: "the_Bool v" and
eval_c: "G⊢s1 ─c→ s2" and
s3: "s3=(abupd (absorb (Cont l)) s2)"
by  (unfold unroll_def) fast
from eval_e normal_s1 have
"normal s"
by (rule eval_no_abrupt_lemma [rule_format])
with while eval_e continue eval_c s3 show ?thesis
by (auto intro!: eval.Loop)
qed
qed

lemma MGFn_Loop:
assumes mfg_e: "G,(A::state triple set)⊢{=:n} ⟨e⟩⇩e≻ {G→}"
and     mfg_c: "G,A⊢{=:n} ⟨c⟩⇩s≻ {G→}"
and     wf: "wf_prog G"
shows "G,A⊢{=:n} ⟨l∙ While(e) c⟩⇩s≻ {G→}"
proof (rule MGFn_free_wt [rule_format],elim exE)
fix T L C
assume wt: "⦇prg = G, cls = C, lcl = L⦈⊢⟨l∙ While(e) c⟩⇩s∷T"
then obtain eT where
wt_e: "⦇prg = G, cls = C, lcl = L⦈⊢e∷-eT"
by cases simp
show ?thesis
proof (rule MGFn_NormalI)
show "G,A⊢{Normal ((λY' s' s. s' = s ∧ normal s) ∧. G⊢init≤n)}
.l∙ While(e) c.
{λY s' s. G⊢s ─In1r (l∙ While(e) c)≻→ (Y, s')}"
proof (rule conseq12
[where ?P'="(λ Y s' s. (s,s') ∈ (unroll G l e c)⇧* ) ∧. G⊢init≤n"
and  ?Q'="((λ Y s' s. (∃ t b. (s,t) ∈ (unroll G l e c)⇧* ∧
Y=⌊b⌋⇩e ∧ G⊢t ─e-≻b→ s'))
∧. G⊢init≤n)←=False↓=♢"])
show  "G,A⊢{(λY s' s. (s, s') ∈ (unroll G l e c)⇧*) ∧. G⊢init≤n}
.l∙ While(e) c.
{((λY s' s. (∃t b. (s, t) ∈ (unroll G l e c)⇧* ∧
Y = In1 b ∧ G⊢t ─e-≻b→ s'))
∧. G⊢init≤n)←=False↓=♢}"
proof (rule ax_derivs.Loop)
from mfg_e
show "G,A⊢{(λY s' s. (s, s') ∈ (unroll G l e c)⇧*) ∧. G⊢init≤n}
e-≻
{(λY s' s. (∃t b. (s, t) ∈ (unroll G l e c)⇧* ∧
Y = In1 b ∧ G⊢t ─e-≻b→ s'))
∧. G⊢init≤n}"
proof (rule MGFnD' [THEN conseq12],clarsimp)
fix s Z s' v
assume "(Z, s) ∈ (unroll G l e c)⇧*"
moreover
assume "G⊢s ─e-≻v→ s'"
ultimately
show "∃t. (Z, t) ∈ (unroll G l e c)⇧* ∧ G⊢t ─e-≻v→ s'"
by blast
qed
next
from mfg_c
show "G,A⊢{Normal (((λY s' s. ∃t b. (s, t) ∈ (unroll G l e c)⇧* ∧
Y = ⌊b⌋⇩e ∧ G⊢t ─e-≻b→ s')
∧. G⊢init≤n)←=True)}
.c.
{abupd (absorb (Cont l)) .;
((λY s' s. (s, s') ∈ (unroll G l e c)⇧*) ∧. G⊢init≤n)}"
proof (rule MGFnD' [THEN conseq12],clarsimp)
fix Z s' s v t
assume unroll: "(Z, t) ∈ (unroll G l e c)⇧*"
assume eval_e: "G⊢t ─e-≻v→ Norm s"
assume true: "the_Bool v"
assume eval_c: "G⊢Norm s ─c→ s'"
show "(Z, abupd (absorb (Cont l)) s') ∈ (unroll G l e c)⇧*"
proof -
note unroll
also
from eval_e true eval_c
have "(t,abupd (absorb (Cont l)) s') ∈ unroll G l e c"
by (unfold unroll_def) force
ultimately show ?thesis ..
qed
qed
qed
next
show
"∀Y s Z.
(Normal ((λY' s' s. s' = s ∧ normal s) ∧. G⊢init≤n)) Y s Z
⟶ (∀Y' s'.
(∀Y Z'.
((λY s' s. (s, s') ∈ (unroll G l e c)⇧*) ∧. G⊢init≤n) Y s Z'
⟶ (((λY s' s. ∃t b. (s,t) ∈ (unroll G l e c)⇧*
∧ Y=⌊b⌋⇩e ∧ G⊢t ─e-≻b→ s')
∧. G⊢init≤n)←=False↓=♢) Y' s' Z')
⟶ G⊢Z ─⟨l∙ While(e) c⟩⇩s≻→ (Y', s'))"
proof (clarsimp)
fix Y' s' s
assume asm:
"∀Z'. (Z', Norm s) ∈ (unroll G l e c)⇧*
⟶ card (nyinitcls G s') ≤ n ∧
(∃v. (∃t. (Z', t) ∈ (unroll G l e c)⇧* ∧ G⊢t ─e-≻v→ s') ∧
(fst s' = None ⟶ ¬ the_Bool v)) ∧ Y' = ♢"
show "Y' = ♢ ∧ G⊢Norm s ─l∙ While(e) c→ s'"
proof -
from asm obtain v t where
― ‹@{term "Z'"} gets instantiated with @{term "Norm s"}›
unroll: "(Norm s, t) ∈ (unroll G l e c)⇧*" and
eval_e: "G⊢t ─e-≻v→ s'" and
normal_termination: "normal s' ⟶ ¬ the_Bool v" and
Y': "Y' = ♢"
by auto
from unroll eval_e normal_termination wt_e wf
have "G⊢Norm s ─l∙ While(e) c→ s'"
by (rule unroll_while)
with Y'
show ?thesis
by simp
qed
qed
qed
qed
qed

lemma MGFn_FVar:
fixes A :: "state triple set"
assumes mgf_init: "G,A⊢{=:n} ⟨Init statDeclC⟩⇩s≻ {G→}"
and    mgf_e: "G,A⊢{=:n} ⟨e⟩⇩e≻ {G→}"
and    wf: "wf_prog G"
shows "G,A⊢{=:n} ⟨{accC,statDeclC,stat}e..fn⟩⇩v≻ {G→}"
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
note inj_term_simps [simp]
fix T L accC' V
assume wt: "⦇prg = G, cls = accC', lcl = L⦈⊢⟨{accC,statDeclC,stat}e..fn⟩⇩v∷T"
then obtain statC f where
wt_e: "⦇prg=G, cls=accC', lcl=L⦈⊢e∷-Class statC" and
accfield: "accfield G accC' statC fn = Some (statDeclC,f )" and
eq_accC: "accC=accC'" and
stat: "stat=is_static  f"
by (cases) (auto simp add: member_is_static_simp)
let ?Q="(λY s1 (x,s) . x = None ∧
(G⊢Norm s ─Init statDeclC→ s1) ∧
(∃ E. ⦇prg=G,cls=accC',lcl=L⦈⊢dom (locals (store s1)) »⟨e⟩⇩e» E))
∧. G⊢init≤n ∧. (λ s. s∷≼(G, L))"
show "G,A⊢{Normal
((λY' s' s. s' = s ∧ abrupt s = None) ∧. G⊢init≤n ∧.
(λs. s∷≼(G, L)) ∧.
(λs. ⦇prg=G,cls=accC',lcl=L⦈
⊢ dom (locals (store s)) » ⟨{accC,statDeclC,stat}e..fn⟩⇩v» V))
} {accC,statDeclC,stat}e..fn=≻
{λY s' s. ∃vf. Y = ⌊vf⌋⇩v ∧
G⊢s ─{accC,statDeclC,stat}e..fn=≻vf→ s'}"
(is "G,A⊢{Normal ?P} {accC,statDeclC,stat}e..fn=≻ {?R}")
proof (rule ax_derivs.FVar [where ?Q="?Q" ])
from mgf_init
show "G,A⊢{Normal ?P} .Init statDeclC. {?Q}"
proof (rule MGFnD' [THEN conseq12],clarsimp)
fix s s'
assume conf_s: "Norm s∷≼(G, L)"
assume da: "⦇prg=G,cls=accC',lcl=L⦈
⊢ dom (locals s) »⟨{accC,statDeclC,stat}e..fn⟩⇩v» V"
assume eval_init: "G⊢Norm s ─Init statDeclC→ s'"
show "(∃E. ⦇prg=G, cls=accC', lcl=L⦈⊢ dom (locals (store s')) »⟨e⟩⇩e» E) ∧
s'∷≼(G, L)"
proof -
from da
obtain E where
"⦇prg=G, cls=accC', lcl=L⦈⊢ dom (locals s) »⟨e⟩⇩e» E"
by cases simp
moreover
from eval_init
have "dom (locals s) ⊆ dom (locals (store s'))"
by (rule dom_locals_eval_mono [elim_format]) simp
ultimately obtain E' where
"⦇prg=G, cls=accC', lcl=L⦈⊢ dom (locals (store s')) »⟨e⟩⇩e» E'"
by (rule da_weakenE)
moreover
have "s'∷≼(G, L)"
proof -
have wt_init: "⦇prg=G, cls=accC, lcl=L⦈⊢(Init statDeclC)∷√"
proof -
from wf wt_e
have iscls_statC: "is_class G statC"
by (auto dest: ty_expr_is_type type_is_class)
with wf accfield
have iscls_statDeclC: "is_class G statDeclC"
by (auto dest!: accfield_fields dest: fields_declC)
thus ?thesis by simp
qed
obtain I where
da_init: "⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store ((Norm s)::state))) »⟨Init statDeclC⟩⇩s» I"
by (auto intro: da_Init [simplified] assigned.select_convs)
from eval_init conf_s wt_init da_init  wf
show ?thesis
by (rule eval_type_soundE)
qed
ultimately show ?thesis by iprover
qed
qed
next
from mgf_e
show "G,A⊢{?Q} e-≻ {λVal:a:. fvar statDeclC stat fn a ..; ?R}"
proof (rule MGFnD' [THEN conseq12],clarsimp)
fix s0 s1 s2 E a
let ?fvar = "fvar statDeclC stat fn a s2"
assume eval_init: "G⊢Norm s0 ─Init statDeclC→ s1"
assume eval_e: "G⊢s1 ─e-≻a→ s2"
assume conf_s1: "s1∷≼(G, L)"
assume da_e: "⦇prg=G,cls=accC',lcl=L⦈⊢ dom (locals (store s1)) »⟨e⟩⇩e» E"
show "G⊢Norm s0 ─{accC,statDeclC,stat}e..fn=≻fst ?fvar→ snd ?fvar"
proof -
obtain v s2' where
v: "v=fst ?fvar" and s2': "s2'=snd ?fvar"
by simp
obtain s3 where
s3: "s3= check_field_access G accC' statDeclC fn stat a s2'"
by simp
have eq_s3_s2': "s3=s2'"
proof -
from eval_e conf_s1 wt_e da_e wf obtain
conf_s2: "s2∷≼(G, L)"  and
conf_a: "normal s2 ⟹ G,store s2⊢a∷≼Class statC"
by (rule eval_type_soundE) simp
from accfield wt_e eval_init eval_e conf_s2 conf_a _ wf
show ?thesis
by (rule  error_free_field_access
[where ?v=v and ?s2'=s2',elim_format])
(simp add: s3 v s2' stat)+
qed
from eval_init eval_e
show ?thesis
apply (rule eval.FVar [where ?s2'=s2'])
apply  (simp add: s3 [symmetric]   eq_s3_s2' eq_accC s2' [symmetric])
done
qed
qed
qed
qed

lemma MGFn_Fin:
assumes wf: "wf_prog G"
and     mgf_c1: "G,A⊢{=:n} ⟨c1⟩⇩s≻ {G→}"
and     mgf_c2: "G,A⊢{=:n} ⟨c2⟩⇩s≻ {G→}"
shows "G,(A::state triple set)⊢{=:n} ⟨c1 Finally c2⟩⇩s≻ {G→}"
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
fix T L accC C
assume wt: "⦇prg=G,cls=accC,lcl=L⦈⊢In1r (c1 Finally c2)∷T"
then obtain
wt_c1: "⦇prg=G,cls=accC,lcl=L⦈⊢c1∷√" and
wt_c2: "⦇prg=G,cls=accC,lcl=L⦈⊢c2∷√"
by cases simp
let  ?Q = "(λY' s' s. normal s ∧ G⊢s ─c1→ s' ∧
(∃ C1. ⦇prg=G,cls=accC,lcl=L⦈⊢dom (locals (store s)) »⟨c1⟩⇩s» C1)
∧ s∷≼(G, L))
∧. G⊢init≤n"
show "G,A⊢{Normal
((λY' s' s. s' = s ∧ abrupt s = None) ∧. G⊢init≤n ∧.
(λs. s∷≼(G, L)) ∧.
(λs. ⦇prg=G,cls=accC,lcl =L⦈
⊢dom (locals (store s)) »⟨c1 Finally c2⟩⇩s» C))}
.c1 Finally c2.
{λY s' s. Y = ♢ ∧ G⊢s ─c1 Finally c2→ s'}"
(is "G,A⊢{Normal ?P} .c1 Finally c2. {?R}")
proof (rule ax_derivs.Fin [where ?Q="?Q"])
from mgf_c1
show "G,A⊢{Normal ?P} .c1. {?Q}"
proof (rule MGFnD' [THEN conseq12],clarsimp)
fix s0
assume "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals s0) »⟨c1 Finally c2⟩⇩s» C"
thus "∃C1. ⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals s0) »⟨c1⟩⇩s» C1"
by cases (auto simp add: inj_term_simps)
qed
next
from mgf_c2
show "∀abr. G,A⊢{?Q ∧. (λs. abr = abrupt s) ;. abupd (λabr. None)} .c2.
{abupd (abrupt_if (abr ≠ None) abr) .; ?R}"
proof (rule MGFnD' [THEN conseq12, THEN allI],clarsimp)
fix s0 s1 s2 C1
assume da_c1:"⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals s0) »⟨c1⟩⇩s» C1"
assume conf_s0: "Norm s0∷≼(G, L)"
assume eval_c1: "G⊢Norm s0 ─c1→ s1"
assume eval_c2: "G⊢abupd (λabr. None) s1 ─c2→ s2"
show "G⊢Norm s0 ─c1 Finally c2
→ abupd (abrupt_if (∃y. abrupt s1 = Some y) (abrupt s1)) s2"
proof -
obtain abr1 str1 where s1: "s1=(abr1,str1)"
by (cases s1)
with eval_c1 eval_c2 obtain
eval_c1': "G⊢Norm s0 ─c1→ (abr1,str1)" and
eval_c2': "G⊢Norm str1 ─c2→ s2"
by simp
obtain s3 where
s3: "s3 = (if ∃err. abr1 = Some (Error err)
then (abr1, str1)
else abupd (abrupt_if (abr1 ≠ None) abr1) s2)"
by simp
from eval_c1' conf_s0 wt_c1 _ wf
have "error_free (abr1,str1)"
by (rule eval_type_soundE) (insert da_c1,auto)
with s3 have eq_s3: "s3=abupd (abrupt_if (abr1 ≠ None) abr1) s2"
from eval_c1' eval_c2' s3
show ?thesis
by (rule eval.Fin [elim_format]) (simp add: s1 eq_s3)
qed
qed
qed
qed

lemma Body_no_break:
assumes eval_init: "G⊢Norm s0 ─Init D→ s1"
and      eval_c: "G⊢s1 ─c→ s2"
and       jmpOk: "jumpNestingOkS {Ret} c"
and        wt_c: "⦇prg=G, cls=C, lcl=L⦈⊢c∷√"
and        clsD: "class G D=Some d"
and          wf: "wf_prog G"
shows "∀ l. abrupt s2 ≠ Some (Jump (Break l)) ∧
abrupt s2 ≠ Some (Jump (Cont l))"
proof
fix l show "abrupt s2 ≠ Some (Jump (Break l)) ∧
abrupt s2 ≠ Some (Jump (Cont l))"
proof -
fix accC from clsD have wt_init: "⦇prg=G, cls=accC, lcl=L⦈⊢(Init D)∷√"
by auto
from eval_init wf
have s1_no_jmp: "⋀ j. abrupt s1 ≠ Some (Jump j)"
by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
from eval_c _ wt_c wf
show ?thesis
apply (rule jumpNestingOk_eval [THEN conjE, elim_format])
using jmpOk s1_no_jmp
apply auto
done
qed
qed

lemma MGFn_Body:
assumes wf: "wf_prog G"
and     mgf_init: "G,A⊢{=:n} ⟨Init D⟩⇩s≻ {G→}"
and     mgf_c: "G,A⊢{=:n} ⟨c⟩⇩s≻ {G→}"
shows  "G,(A::state triple set)⊢{=:n} ⟨Body D c⟩⇩e≻ {G→}"
proof (rule MGFn_free_wt_da_NormalConformI [rule_format],clarsimp)
fix T L accC E
assume wt: "⦇prg=G, cls=accC,lcl=L⦈⊢⟨Body D c⟩⇩e∷T"
let ?Q="(λY' s' s. normal s ∧ G⊢s ─Init D→ s' ∧ jumpNestingOkS {Ret} c)
∧. G⊢init≤n"
show "G,A⊢{Normal
((λY' s' s. s' = s ∧ fst s = None) ∧. G⊢init≤n ∧.
(λs. s∷≼(G, L)) ∧.
(λs. ⦇prg=G,cls=accC,lcl=L⦈
⊢ dom (locals (store s)) »⟨Body D c⟩⇩e» E))}
Body D c-≻
{λY s' s. ∃v. Y = In1 v ∧ G⊢s ─Body D c-≻v→ s'}"
(is "G,A⊢{Normal ?P} Body D c-≻ {?R}")
proof (rule ax_derivs.Body [where ?Q="?Q"])
from mgf_init
show "G,A⊢{Normal ?P} .Init D. {?Q}"
proof (rule MGFnD' [THEN conseq12],clarsimp)
fix s0
assume da: "⦇prg=G,cls=accC,lcl=L⦈⊢ dom (locals s0) »⟨Body D c⟩⇩e» E"
thus "jumpNestingOkS {Ret} c"
by cases simp
qed
next
from mgf_c
show "G,A⊢{?Q}.c.{λs.. abupd (absorb Ret) .; ?R←⌊the (locals s Result)⌋⇩e}"
proof (rule MGFnD' [THEN conseq12],clarsimp)
fix s0 s1 s2
assume eval_init: "G⊢Norm s0 ─Init D→ s1"
assume eval_c: "G⊢s1 ─c→ s2"
assume nestingOk: "jumpNestingOkS {Ret} c"
show "G⊢Norm s0 ─Body D c-≻the (locals (store s2) Result)
→ abupd (absorb Ret) s2"
proof -
from wt obtain d where
d: "class G D=Some d" and
wt_c: "⦇prg = G, cls = accC, lcl = L⦈⊢c∷√"
by cases auto
obtain s3 where
s3: "s3= (if ∃l. fst s2 = Some (Jump (Break l)) ∨
fst s2 = Some (Jump (Cont l))
then abupd (λx. Some (Error CrossMethodJump)) s2
else s2)"
by simp
from eval_init eval_c nestingOk wt_c d wf
have eq_s3_s2: "s3=s2"
by (rule Body_no_break [elim_format]) (simp add: s3)
from eval_init eval_c s3
show ?thesis
by (rule eval.Body [elim_format]) (simp add: eq_s3_s2)
qed
qed
qed
qed

lemma MGFn_lemma:
assumes mgf_methds:
"⋀ n. ∀ C sig. G,(A::state triple set)⊢{=:n} ⟨Methd C sig⟩⇩e≻ {G→}"
and wf: "wf_prog G"
shows "⋀ t. G,A⊢{=:n} t≻ {G→}"
proof (induct rule: full_nat_induct)
fix n t
assume hyp: "∀ m. Suc m ≤ n ⟶ (∀ t. G,A⊢{=:m} t≻ {G→})"
show "G,A⊢{=:n} t≻ {G→}"
proof -
{
fix v e c es
have "G,A⊢{=:n} ⟨v⟩⇩v≻ {G→}" and
"G,A⊢{=:n} ⟨e⟩⇩e≻ {G→}" and
"G,A⊢{=:n} ⟨c⟩⇩s≻ {G→}" and
"G,A⊢{=:n} ⟨es⟩⇩l≻ {G→}"
proof (induct rule: compat_var.induct compat_expr.induct compat_stmt.induct compat_expr_list.induct)
case (LVar v)
show "G,A⊢{=:n} ⟨LVar v⟩⇩v≻ {G→}"
apply (rule MGFn_NormalI)
apply (rule ax_derivs.LVar [THEN conseq1])
apply (clarsimp)
apply (rule eval.LVar)
done
next
case (FVar accC statDeclC stat e fn)
from MGFn_Init [OF hyp] and ‹G,A⊢{=:n} ⟨e⟩⇩e≻ {G→}› and wf
show ?case
by (rule MGFn_FVar)
next
case (AVar e1 e2)
note mgf_e1 = ‹G,A⊢{=:n} ⟨e1⟩⇩e≻ {G→}›
note mgf_e2 = ‹G,A⊢{=:n} ⟨e2⟩⇩e≻ {G→}›
show "G,A⊢{=:n} ⟨e1.[e2]⟩⇩v≻ {G→}"
apply (rule MGFn_NormalI)
apply (rule ax_derivs.AVar)
apply  (rule MGFnD [OF mgf_e1, THEN ax_NormalD])
apply (rule allI)
apply (rule MGFnD' [OF mgf_e2, THEN conseq12])
apply (fastforce intro: eval.AVar)
done
next
case (InsInitV c v)
show ?case
by (rule MGFn_NormalI) (rule ax_derivs.InsInitV)
next
case (NewC C)
show ?case
apply (rule MGFn_NormalI)
apply (rule ax_derivs.NewC)
apply (rule MGFn_InitD [OF hyp, THEN conseq2])
apply (fastforce intro: eval.NewC)
done
next
case (NewA T e)
thus ?case
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.NewA
[where ?Q = "(λY' s' s. normal s ∧ G⊢s ─In1r (init_comp_ty T)
≻→ (Y',s')) ∧. G⊢init≤n"])
apply  (simp add: init_comp_ty_def split: if_split)
apply  (rule conjI, clarsimp)
apply   (rule MGFn_InitD [OF hyp, THEN conseq2])
apply   (clarsimp intro: eval.Init)
apply  clarsimp
apply  (rule ax_derivs.Skip [THEN conseq1])
apply  (clarsimp intro: eval.Skip)
apply (erule MGFnD' [THEN conseq12])
apply (fastforce intro: eval.NewA)
done
next
case (Cast C e)
thus ?case
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Cast])
apply (fastforce intro: eval.Cast)
done
next
case (Inst e C)
thus ?case
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Inst])
apply (fastforce intro: eval.Inst)
done
next
case (Lit v)
show ?case
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Lit [THEN conseq1])
apply (fastforce intro: eval.Lit)
done
next
case (UnOp unop e)
thus ?case
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.UnOp)
apply (erule MGFnD' [THEN conseq12])
apply (fastforce intro: eval.UnOp)
done
next
case (BinOp binop e1 e2)
thus ?case
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.BinOp)
apply  (erule MGFnD [THEN ax_NormalD])
apply (rule allI)
apply (case_tac "need_second_arg binop v1")
apply  simp
apply  (erule MGFnD' [THEN conseq12])
apply  (fastforce intro: eval.BinOp)
apply simp
apply (rule ax_Normal_cases)
apply  (rule ax_derivs.Skip [THEN conseq1])
apply  clarsimp
apply  (rule eval_BinOp_arg2_indepI)
apply   simp
apply  simp
apply (rule ax_derivs.Abrupt [THEN conseq1], clarsimp simp add: Let_def)
apply (fastforce intro: eval.BinOp)
done
next
case Super
show ?case
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Super [THEN conseq1])
apply (fastforce intro: eval.Super)
done
next
case (Acc v)
thus ?case
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Acc])
apply (fastforce intro: eval.Acc simp add: split_paired_all)
done
next
case (Ass v e)
thus "G,A⊢{=:n} ⟨v:=e⟩⇩e≻ {G→}"
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Ass)
apply  (erule MGFnD [THEN ax_NormalD])
apply (rule allI)
apply (erule MGFnD'[THEN conseq12])
apply (fastforce intro: eval.Ass simp add: split_paired_all)
done
next
case (Cond e1 e2 e3)
thus "G,A⊢{=:n} ⟨e1 ? e2 : e3⟩⇩e≻ {G→}"
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Cond)
apply  (erule MGFnD [THEN ax_NormalD])
apply (rule allI)
apply (rule ax_Normal_cases)
prefer 2
apply  (rule ax_derivs.Abrupt [THEN conseq1],clarsimp simp add: Let_def)
apply  (fastforce intro: eval.Cond)
apply (case_tac "b")
apply  simp
apply  (erule MGFnD'[THEN conseq12])
apply  (fastforce intro: eval.Cond)
apply simp
apply (erule MGFnD'[THEN conseq12])
apply (fastforce intro: eval.Cond)
done
next
case (Call accC statT mode e mn pTs' ps)
note mgf_e = ‹G,A⊢{=:n} ⟨e⟩⇩e≻ {G→}›
note mgf_ps = ‹G,A⊢{=:n} ⟨ps⟩⇩l≻ {G→}›
from mgf_methds mgf_e mgf_ps wf
show "G,A⊢{=:n} ⟨{accC,statT,mode}e⋅mn({pTs'}ps)⟩⇩e≻ {G→}"
by (rule MGFn_Call)
next
case (Methd D mn)
from mgf_methds
show "G,A⊢{=:n} ⟨Methd D mn⟩⇩e≻ {G→}"
by simp
next
case (Body D c)
note mgf_c = ‹G,A⊢{=:n} ⟨c⟩⇩s≻ {G→}›
from wf MGFn_Init [OF hyp] mgf_c
show "G,A⊢{=:n} ⟨Body D c⟩⇩e≻ {G→}"
by (rule MGFn_Body)
next
case (InsInitE c e)
show ?case
by (rule MGFn_NormalI) (rule ax_derivs.InsInitE)
next
case (Callee l e)
show ?case
by (rule MGFn_NormalI) (rule ax_derivs.Callee)
next
case Skip
show ?case
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Skip [THEN conseq1])
apply (fastforce intro: eval.Skip)
done
next
case (Expr e)
thus ?case
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD'[THEN conseq12,THEN ax_derivs.Expr])
apply (fastforce intro: eval.Expr)
done
next
case (Lab l c)
thus "G,A⊢{=:n} ⟨l∙ c⟩⇩s≻ {G→}"
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Lab])
apply (fastforce intro: eval.Lab)
done
next
case (Comp c1 c2)
thus "G,A⊢{=:n} ⟨c1;; c2⟩⇩s≻ {G→}"
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Comp)
apply  (erule MGFnD [THEN ax_NormalD])
apply (erule MGFnD' [THEN conseq12])
apply (fastforce intro: eval.Comp)
done
next
case (If' e c1 c2)
thus "G,A⊢{=:n} ⟨If(e) c1 Else c2⟩⇩s≻ {G→}"
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.If)
apply  (erule MGFnD [THEN ax_NormalD])
apply (rule allI)
apply (rule ax_Normal_cases)
prefer 2
apply  (rule ax_derivs.Abrupt [THEN conseq1],clarsimp simp add: Let_def)
apply  (fastforce intro: eval.If)
apply (case_tac "b")
apply  simp
apply  (erule MGFnD' [THEN conseq12])
apply  (fastforce intro: eval.If)
apply simp
apply (erule MGFnD' [THEN conseq12])
apply (fastforce intro: eval.If)
done
next
case (Loop l e c)
note mgf_e = ‹G,A⊢{=:n} ⟨e⟩⇩e≻ {G→}›
note mgf_c = ‹G,A⊢{=:n} ⟨c⟩⇩s≻ {G→}›
from mgf_e mgf_c wf
show "G,A⊢{=:n} ⟨l∙ While(e) c⟩⇩s≻ {G→}"
by (rule MGFn_Loop)
next
case (Jmp j)
thus ?case
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Jmp [THEN conseq1])
apply (auto intro: eval.Jmp)
done
next
case (Throw e)
thus ?case
apply -
apply (rule MGFn_NormalI)
apply (erule MGFnD' [THEN conseq12, THEN ax_derivs.Throw])
apply (fastforce intro: eval.Throw)
done
next
case (TryC c1 C vn c2)
thus "G,A⊢{=:n} ⟨Try c1 Catch(C vn) c2⟩⇩s≻ {G→}"
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Try [where
?Q = " (λY' s' s. normal s ∧ (∃s''. G⊢s ─⟨c1⟩⇩s≻→ (Y',s'') ∧
G⊢s'' ─sxalloc→ s')) ∧. G⊢init≤n"])
apply   (erule MGFnD [THEN ax_NormalD, THEN conseq2])
apply   (fastforce elim: sxalloc_gext [THEN card_nyinitcls_gext])
apply  (erule MGFnD'[THEN conseq12])
apply  (fastforce intro: eval.Try)
apply (fastforce intro: eval.Try)
done
next
case (Fin c1 c2)
note mgf_c1 = ‹G,A⊢{=:n} ⟨c1⟩⇩s≻ {G→}›
note mgf_c2 = ‹G,A⊢{=:n} ⟨c2⟩⇩s≻ {G→}›
from wf mgf_c1 mgf_c2
show "G,A⊢{=:n} ⟨c1 Finally c2⟩⇩s≻ {G→}"
by (rule MGFn_Fin)
next
case (FinA abr c)
show ?case
by (rule MGFn_NormalI) (rule ax_derivs.FinA)
next
case (Init C)
from hyp
show "G,A⊢{=:n} ⟨Init C⟩⇩s≻ {G→}"
by (rule MGFn_Init)
next
case Nil_expr
show "G,A⊢{=:n} ⟨[]⟩⇩l≻ {G→}"
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Nil [THEN conseq1])
apply (fastforce intro: eval.Nil)
done
next
case (Cons_expr e es)
thus "G,A⊢{=:n} ⟨e# es⟩⇩l≻ {G→}"
apply -
apply (rule MGFn_NormalI)
apply (rule ax_derivs.Cons)
apply  (erule MGFnD [THEN ax_NormalD])
apply (rule allI)
apply (erule MGFnD'[THEN conseq12])
apply (fastforce intro: eval.Cons)
done
qed
}
thus ?thesis
by (cases rule: term_cases) auto
qed
qed

lemma MGF_asm:
"⟦∀C sig. is_methd G C sig ⟶ G,A⊢{≐} In1l (Methd C sig)≻ {G→}; wf_prog G⟧
⟹ G,(A::state triple set)⊢{≐} t≻ {G→}"
apply (rule allI)
apply (rule MGFn_lemma)
apply (intro strip)
apply (rule MGFn_free_wt)
apply (force dest: wt_Methd_is_methd)
apply assumption (* wf_prog G *)
done

subsubsection "nested version"

lemma nesting_lemma' [rule_format (no_asm)]:
assumes ax_derivs_asm: "⋀A ts. ts ⊆ A ⟹ P A ts"
and MGF_nested_Methd: "⋀A pn. ∀b∈bdy pn. P (insert (mgf_call pn) A) {mgf b}
⟹ P A {mgf_call pn}"
and MGF_asm: "⋀A t. ∀pn∈U. P A {mgf_call pn} ⟹ P A {mgf t}"
and finU: "finite U"
and uA: "uA = mgf_callU"
shows "∀A. A ⊆ uA ⟶ n ≤ card uA ⟶ card A = card uA - n
⟶ (∀t. P A {mgf t})"
using finU uA
apply -
apply (induct_tac "n")
apply  (tactic "ALLGOALS (clarsimp_tac @{context})")
apply  (tactic ‹dresolve_tac @{context} [Thm.permute_prems 0 1 @{thm card_seteq}] 1›)
apply    simp
apply   (erule finite_imageI)
apply (rule MGF_asm)
apply (rule ballI)
apply (case_tac "mgf_call pn ∈ A")
apply  (fast intro: ax_derivs_asm)
apply (rule MGF_nested_Methd)
apply (rule ballI)
apply (drule spec, erule impE, erule_tac [2] impE, erule_tac [3] spec)
apply hypsubst_thin
apply   fast
apply (drule finite_subset)
apply (erule finite_imageI)
apply auto
done

lemma nesting_lemma [rule_format (no_asm)]:
assumes ax_derivs_asm: "⋀A ts. ts ⊆ A ⟹ P A ts"
and MGF_nested_Methd: "⋀A pn. ∀b∈bdy pn. P (insert (mgf (f pn)) A) {mgf b}
⟹ P A {mgf (f pn)}"
and MGF_asm: "⋀A t. ∀pn∈U. P A {mgf (f pn)} ⟹ P A {mgf t}"
and finU: "finite U"
shows "P {} {mgf t}"
using ax_derivs_asm MGF_nested_Methd MGF_asm finU
by (rule nesting_lemma') (auto intro!: le_refl)

lemma MGF_nested_Methd: "⟦
G,insert ({Normal ≐} ⟨Methd  C sig⟩⇩e ≻{G→}) A
⊢{Normal ≐} ⟨body G C sig⟩⇩e ≻{G→}
⟧ ⟹  G,A⊢{Normal ≐}  ⟨Methd  C sig⟩⇩e ≻{G→}"
apply (unfold MGF_def)
apply (rule ax_MethdN)
apply (erule conseq2)
apply clarsimp
apply (erule MethdI)
done

lemma MGF_deriv: "wf_prog G ⟹ G,({}::state triple set)⊢{≐} t≻ {G→}"
apply (rule MGFNormalI)
apply (rule_tac mgf = "λt. {Normal ≐} t≻ {G→}" and
bdy = "λ (C,sig) .{⟨body G C sig⟩⇩e }" and
f = "λ (C,sig) . ⟨Methd C sig⟩⇩e " in nesting_lemma)
apply    (erule ax_derivs.asm)
apply   (erule MGF_nested_Methd)
apply  (erule_tac [2] finite_is_methd [OF wf_ws_prog])
apply (rule MGF_asm [THEN MGFNormalD])
apply (auto intro: MGFNormalI)
done

subsubsection "simultaneous version"

lemma MGF_simult_Methd_lemma: "finite ms ⟹
G,A ∪ (λ(C,sig). {Normal ≐} ⟨Methd  C sig⟩⇩e≻ {G→})  ms
|⊢(λ(C,sig). {Normal ≐} ⟨body G C sig⟩⇩e≻ {G→})  ms ⟹
G,A|⊢(λ(C,sig). {Normal ≐} ⟨Methd  C sig⟩⇩e≻ {G→})  ms"
apply (unfold MGF_def)
apply (rule ax_derivs.Methd [unfolded mtriples_def])
apply (erule ax_finite_pointwise)
prefer 2
apply  (rule ax_derivs.asm)
apply  fast
apply clarsimp
apply (rule conseq2)
apply  (erule (1) ax_methods_spec)
apply clarsimp
apply (erule eval_Methd)
done

lemma MGF_simult_Methd: "wf_prog G ⟹
G,({}::state triple set)|⊢(λ(C,sig). {Normal ≐} ⟨Methd C sig⟩⇩e≻ {G→})
Collect (case_prod (is_methd G)) "
apply (frule finite_is_methd [OF wf_ws_prog])
apply (rule MGF_simult_Methd_lemma)
apply  assumption
apply (erule ax_finite_pointwise)
prefer 2
apply  (rule ax_derivs.asm)
apply  blast
apply clarsimp
apply (rule MGF_asm [THEN MGFNormalD])
apply   (auto intro: MGFNormalI)
done

subsubsection "corollaries"

lemma eval_to_evaln: "⟦G⊢s ─t≻→ (Y', s');type_ok G t s; wf_prog G⟧
⟹   ∃n. G⊢s ─t≻─n→ (Y', s')"
apply (cases "normal s")
apply   (force simp add: type_ok_def intro: eval_evaln)
apply   (force intro: evaln.Abrupt)
done

lemma MGF_complete:
assumes valid: "G,{}⊨{P} t≻ {Q}"
and     mgf: "G,({}::state triple set)⊢{≐} t≻ {G→}"
and      wf: "wf_prog G"
shows "G,({}::state triple set)⊢{P::state assn} t≻ {Q}"
proof (rule ax_no_hazard)
from mgf
have "G,({}::state triple set)⊢{≐} t≻ {λY s' s. G⊢s ─t≻→ (Y, s')}"
by  (unfold MGF_def)
thus "G,({}::state triple set)⊢{P ∧. type_ok G t} t≻ {Q}"
proof (rule conseq12,clarsimp)
fix Y s Z Y' s'
assume P: "P Y s Z"
assume type_ok: "type_ok G t s"
assume eval_t: "G⊢s ─t≻→ (Y', s')"
show "Q Y' s' Z"
proof -
from eval_t type_ok wf
obtain n where evaln: "G⊢s ─t≻─n→ (Y', s')"
by (rule eval_to_evaln [elim_format]) iprover
from valid have
valid_expanded:
"∀n Y s Z. P Y s Z ⟶ type_ok G t s
⟶ (∀Y' s'. G⊢s ─t≻─n→ (Y', s') ⟶ Q Y' s' Z)"
from P type_ok evaln
show "Q Y' s' Z"
by (rule valid_expanded [rule_format])
qed
qed
qed

theorem ax_complete:
assumes wf: "wf_prog G"
and valid: "G,{}⊨{P::state assn} t≻ {Q}"
shows "G,({}::state triple set)⊢{P} t≻ {Q}"
proof -
from wf have "G,({}::state triple set)⊢{≐} t≻ {G→}"
by (rule MGF_deriv)
from valid this wf
show ?thesis
by (rule MGF_complete)
qed

end
`