Theory Sound

(*File: Sound.thy
  Author: L Beringer & M Hofmann, LMU Munich
  Date: 05/12/2008
  Purpose: Interpretation of judgements, and soundness proof,
           of the program logic with  invariants, pre-
           and post-conditions, and local assertions, but no
           exploitation of sucessful bytecode verification.
*)
(*<*)
theory Sound imports Logic MultiStep Reachability begin
(*>*)

section‹Soundness›
text‹This section contains the soundness proof of the program logic.
In the first subsection, we define our notion of validity, thus
formalising our intuitive explanation of the terms preconditions,
specifications, and invariants. The following two subsections contain
the details of the proof and can easily be skipped during a first pass
through the document.›

subsection‹Validity›

text‹A  judgement is valid at the program point ‹C.m.l›
(i.e.~at label ‹l› in method ‹m› of class ‹C›),
written $\mathit{valid}\; C\; m\; l\; A\; B\; I$ or, in symbols, $$\vDash\,
\lbrace A \rbrace\, C,m,l\, \lbrace B \rbrace\, I,$$ if $A$ is a
precondition for $B$ and for all local annotations following $l$ in an
execution of ‹m›, and all reachable states in the current frame
or yet-to-be created subframes satisfy $I$. More precisely,
whenever an execution of the method starting in an initial state $s_0$
reaches the label ‹l› with state ‹s›, the following 
properties are implied by $A(s_0,s)$.
\begin{enumerate}

  \item If the continued execution from ‹s› reaches a final
  state ‹t› (i.e.~the method terminates), then that final state
  ‹t› satisfies $B(s_0,s,t)$.

  \item Any state $s'$ visited in the current frame during the remaining
  program execution whose label carries an annotation ‹Q› will
  satisfy $Q(s_0,s')$, even if the execution of the frame does not
  terminate.

  \item Any state $s'$ visited in the current frame or a subframe of
  the current frame will satisfy $I(s_0,s,\mathit{heap}(s'))$, again even if the
  execution does not terminate.

\end{enumerate}

Formally, this interpretation is expressed as follows.
›

definition valid::"Class ⇒ Method ⇒ Label ⇒ Assn ⇒ Post ⇒ Inv ⇒ bool" where
"valid C m l A B I =
   (∀ M. mbody_is C m M ⟶
   (∀ Mspec Minv Anno . MST↓(C,m) = Some(Mspec,Minv,Anno) ⟶
   (∀ par code l0 . M = (par,code,l0) ⟶
   (∀ s0 s . MS M l0 (mkState s0) l s ⟶ A s0 s ⟶
    ((∀ h v. Opsem M l s h v ⟶ B s0 s (h,v)) ∧
     (∀ ll r . (MS M l s ll r  ⟶ (∀ Q . Anno↓(ll) = Some Q ⟶  Q s0 r)) ∧
               (Reach M l s r ⟶ I s0 s (heap r))))))))"

abbreviation valid_syntax :: "Assn ⇒ Class ⇒ Method ⇒ 
                    Label ⇒ Post ⇒ Inv ⇒ bool" 
       (" ⊨ ⦃ _ ⦄ _ , _ , _ ⦃ _ ⦄ _" [200,200,200,200,200,200] 200)
where "valid_syntax A C m l B I == valid C m l A B I"

text‹This notion of validity extends that of Bannwart-M\"uller by
allowing the post-condition to differ from method specification and to
refer to the initial state, and by including invariants.  In
the logic of Bannwart and M\"uller, the validity of a method
specification is given by a partial correctness (Hoare-style)
interpretation, while the validity of  preconditions of
individual instructions is such that a precondition at $l$ implies the
preconditions of its immediate control flow successors.›

text‹Validity us lifted to contexts and the method specification
table. In the case of the former, we simply require that all entries
be valid.›

definition G_valid::"CTXT ⇒ bool" where
"G_valid G = (∀ C m l A B I. G↓(C,m,l) = Some (A,B,I)⟶
                                ⊨ ⦃A⦄ C, m, l ⦃B⦄ I)"

text‹Regarding the specification table, we require that the initial
label of each method satisfies an assertion that ties the method
precondition to the current state.›

definition MST_valid ::bool where
"MST_valid = (∀ C m par code l0 T MI Anno. 
  mbody_is C m (par,code,l0) ⟶ MST↓(C, m) = Some (T,MI,Anno) ⟶ 
  ⊨ ⦃(λ s0 s. s = mkState s0)⦄ C, m, l0 ⦃(mkPost T)⦄ (mkInv MI))"

definition Prog_valid::bool where
"Prog_valid = (∃ G . G_valid G ∧ MST_valid)"

text‹The remainder of this section contains a proof of soundness,
i.e.~of the property $$‹VP› \Longrightarrow ‹Prog_valid›,$$ and is structured into two parts. The first step
(Section \ref{SoundnessUnderValidContexts}) establishes a soundness
result where the ‹VP› property is replaced by validity
assumptions regarding the method specification table and the
context. In the second step (Section \ref{SectionContextElimination}),
we show that these validity assumptions are satisfied by verified
programs, which implies the overall soundness theorem.›

subsection‹Soundness under valid contexts
\label{SoundnessUnderValidContexts}›

text‹The soundness proof proceeds by induction on the axiomatic
semantics, based on an auxiliary lemma for method invocations that is
proven by induction on the derivation height of the operational
semantics. For the latter induction, relativised notions of validity
are employed that restrict the derivation height of the program
continuations affected by an assertion. The appropriate definitions of
relativised validity for judgements, for the precondition table, and
for the method specification table are as follows.›

definition validn::
  "nat ⇒ Class ⇒ Method ⇒ Label ⇒ Assn ⇒ Post ⇒ Inv ⇒ bool" where
"validn K C m l A B I =
   (∀ M. mbody_is C m M ⟶
   (∀ Mspec Minv Anno . MST↓(C,m) = Some(Mspec,Minv,Anno) ⟶
   (∀ par code l0 . M = (par,code,l0) ⟶
   (∀ s0 s . MS M l0 (mkState s0) l s ⟶ A s0 s ⟶
   (∀ k . k ≤ K ⟶ 
    ((∀ h v. (M,l,s,k,h,v):Exec ⟶ B s0 s (h,v)) ∧
     (∀ ll r . ((M,l,s,k,ll,r):MStep  ⟶
                 (∀ Q . Anno↓(ll) = Some Q ⟶  Q s0 r)) ∧
               ((M,l,s,k,r):Reachable ⟶ I s0 s (heap r)))))))))"

abbreviation validn_syntax :: "nat ⇒ Assn ⇒ Class ⇒ Method ⇒
                     Label ⇒ Post ⇒ Inv ⇒ bool" 
("⊨⇩_ ⦃ _ ⦄ _ , _ , _ ⦃ _ ⦄ _ " [200,200,200,200,200,200,200] 200)
where "validn_syntax K A C m l B I == validn K C m l A B I"

definition G_validn::"nat ⇒ CTXT ⇒ bool" where
"G_validn K G = (∀ C m l A B I. G↓(C,m,l) = Some (A,B,I) ⟶
                                ⊨⇩K ⦃A⦄ C, m, l ⦃B⦄ I)"

definition MST_validn::"nat ⇒ bool" where
"MST_validn K = (∀ C m par code l0 T MI Anno. 
   mbody_is C m (par,code,l0) ⟶ MST↓(C, m) = Some (T,MI,Anno) ⟶ 
   ⊨⇩K ⦃(λ s0 s. s = mkState s0)⦄ C, m, l0 ⦃(mkPost T)⦄ (mkInv MI))"

definition Prog_validn::"nat ⇒ bool" where
"Prog_validn K = (∃ G . G_validn K G ∧ MST_validn K)"

text‹The relativised notions are related to each other, and to the
native notions of validity as follows.›

lemma valid_validn: "⊨ ⦃A⦄ C, m, l ⦃B⦄ I ⟹ ⊨⇩K ⦃A⦄ C, m, l ⦃B⦄ I"
(*<*)
apply (simp add: valid_def validn_def Opsem_def MS_def Reach_def)
apply clarsimp
apply (erule_tac x=a in allE)
apply (erule_tac x=aa in allE)
apply (erule_tac x=b in allE, clarsimp)
apply (erule_tac x=ab in allE)
apply (erule_tac x=ba in allE)
apply (erule_tac x=ac in allE)
apply (erule_tac x=ad in allE)
apply (erule_tac x=bb in allE, erule impE) apply fast
apply fastforce
done
(*>*)

lemma validn_valid: "⟦∀ K . ⊨⇩K ⦃A⦄ C, m, l ⦃B⦄ I⟧ ⟹ ⊨ ⦃A⦄ C, m, l ⦃B⦄ I"
(*<*)
apply (unfold valid_def validn_def)(*apply ( Opsem_def MS_def Reach_def)*)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (rule, rule)
apply (rule,rule,rule, rule)    
    apply (unfold Opsem_def, erule exE)
    apply (erule_tac x=n in allE)
    apply (erule_tac x=M in allE, erule impE, assumption) 
    apply (erule_tac x=Mspec in allE, erule_tac x=Minv in allE, erule_tac x=Anno in allE, erule impE, assumption)
    apply (erule_tac x=par in allE, erule_tac x=code in allE)
    apply (erule_tac x=l0 in allE, erule impE, assumption) 
    apply (erule_tac x=s0 in allE, erule_tac x=s in allE)
    apply (erule impE, assumption) 
    apply (erule impE, assumption) 
    apply (erule_tac x=n in allE, erule impE, simp)
    apply fast
apply (rule, rule, rule)
apply (rule, rule, rule)
    apply (unfold MS_def, erule exE, erule exE)
    apply (erule_tac x=ka in allE)
    apply (erule_tac x=M in allE, erule impE, assumption) 
    apply (erule_tac x=Mspec in allE, erule_tac x=Minv in allE, erule_tac x=Anno in allE, erule impE, assumption)
    apply (erule_tac x=par in allE, erule_tac x=code in allE)
    apply (erule_tac x=l0 in allE, erule impE, assumption) 
    apply (erule_tac x=s0 in allE, erule_tac x=s in allE)
    apply (erule impE, fast) 
    apply (erule impE, assumption) 
    apply (erule_tac x=ka in allE, erule impE, simp)
    apply fast
apply rule
    apply (unfold Reach_def, erule exE, erule exE)
    apply (erule_tac x=ka in allE)
    apply (erule_tac x=M in allE, erule impE, assumption) 
    apply (erule_tac x=Mspec in allE, erule_tac x=Minv in allE, erule_tac x=Anno in allE, erule impE, assumption)
    apply (erule_tac x=par in allE, erule_tac x=code in allE)
    apply (erule_tac x=l0 in allE, erule impE, assumption) 
    apply (erule_tac x=s0 in allE, erule_tac x=s in allE)
    apply (erule impE, fast) 
    apply (erule impE, assumption) 
    apply (erule_tac x=ka in allE, erule impE, simp)
    apply fast
done
(*>*)

lemma validn_lower: 
 "⟦⊨⇩K ⦃A⦄ C, m, l ⦃B⦄ I; L ≤ K⟧ ⟹ ⊨⇩L ⦃A⦄ C, m, l ⦃B⦄ I"
(*<*)
apply (unfold validn_def)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply rule
    apply (erule_tac x=M in allE, erule impE, assumption)
    apply (erule_tac x=Mspec in allE, erule_tac x=Minv in allE, erule_tac x=Anno in allE, erule impE, assumption)
    apply (erule_tac x=par in allE)
    apply (erule_tac x=code in allE)
    apply (erule_tac x=l0 in allE, erule impE, assumption)
    apply (erule_tac x=s0 in allE)
    apply (erule_tac x=s in allE, erule impE, assumption, erule impE, assumption)
    apply (erule_tac x=k in allE, erule impE, simp)
apply assumption
done
(*>*)

lemma G_valid_validn: "G_valid G ⟹ G_validn K G"
(*<*)
apply (simp add: G_valid_def G_validn_def, clarsimp)
apply (rule valid_validn) apply fast
done
(*>*)

lemma G_validn_valid:"⟦∀ K . G_validn K G⟧ ⟹ G_valid G"
(*<*)
apply (simp add: G_valid_def G_validn_def, clarsimp)
apply (rule validn_valid) apply clarsimp
done
(*>*)

lemma G_validn_lower: "⟦G_validn K G; L ≤ K⟧ ⟹ G_validn L G"
(*<*)
apply (simp add: G_validn_def, clarsimp)
apply (rule validn_lower) apply fast apply assumption
done
(*>*)

lemma MST_validn_valid:"⟦∀ K. MST_validn K⟧ ⟹ MST_valid"
(*<*)
apply (simp add: MST_validn_def MST_valid_def, clarsimp)
apply (rule validn_valid, clarsimp)
done
(*>*)

lemma MST_valid_validn:"MST_valid ⟹ MST_validn K"
(*<*)
apply (unfold MST_validn_def MST_valid_def)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (rule, rule, rule)
apply rule
apply (rule valid_validn)
apply fast
done
(*>*)

lemma MST_validn_lower: "⟦MST_validn K; L ≤ K⟧ ⟹ MST_validn L"
(*<*)
apply (simp add: MST_validn_def, clarsimp)
apply (erule_tac x=C in allE)
apply (erule_tac x=m in allE)
apply (erule_tac x=par in allE)
apply (erule_tac x=code in allE)
apply (erule_tac x=l0 in allE, erule impE, assumption)
apply (erule_tac x=T in allE)
apply (erule_tac x=MI in allE, clarsimp)
apply (erule validn_lower) apply assumption
done
(*>*)

text‹We define an abbreviation for the side conditions of the rule
for static method invocations\ldots›

definition INVS_SC::
  "Class ⇒ Method ⇒ Label ⇒ Class ⇒ Method ⇒  MethSpec ⇒ MethInv ⇒
   ANNO ⇒ ANNO ⇒ Mbody ⇒ Assn ⇒ Inv ⇒ bool" where
"INVS_SC C m l D m' T MI Anno Anno2 M' A I = (∃ M par code l0 T1 MI1.
    mbody_is C m M ∧ get_ins M l = Some (invokeS D m') ∧ 
    MST↓(C,m) = Some (T1,MI1,Anno) ∧ 
    MST↓(D,m') = Some (T,MI,Anno2) ∧  
    mbody_is D m' M' ∧ M'=(par,code,l0) ∧  
    (∀ Q . Anno↓(l) = Some Q ⟶ (∀ s0 s . A s0 s ⟶ Q s0 s)) ∧ 
    (∀ s0 s . A s0 s ⟶ I s0 s (heap s)) ∧ 
    (∀ s0 ops1 ops2 S R h t . (ops1,par,R,ops2) : Frame ⟶
          A s0 (ops1,S,h) ⟶ MI (R,h) t ⟶ I s0 (ops1,S,h) t))"

text‹\ldots and another abbreviation for the soundness property of
the same rule.›

definition INVS_soundK::
  "nat ⇒ CTXT ⇒ Class ⇒ Method ⇒ Label ⇒ Class ⇒ Method ⇒ 
   MethSpec ⇒ MethInv ⇒ ANNO ⇒ ANNO ⇒ Mbody ⇒ Assn ⇒ 
   Post ⇒ Inv ⇒ bool" where
"INVS_soundK K G C m l D m' T MI Anno Anno2 M' A B I =
  (INVS_SC C m l D m' T MI Anno Anno2 M' A I ⟶ 
    G_validn K G ⟶ MST_validn K ⟶
    ⊨⇩K ⦃(SINV_pre (fst M') T A)⦄ C,m,(l+1)
        ⦃(SINV_post (fst M') T B)⦄ (SINV_inv (fst M') T I)
   ⟶ ⊨⇩(K+1) ⦃ A ⦄ C,m,l ⦃ B ⦄ I)"

text‹The proof that this property holds for all $K$ proceeds by
induction on $K$.›

lemma INVS_soundK_all:
  "INVS_soundK K G C m l D m' T MI Anno Anno2 M' A B I"
(*<*)
supply [[simproc del: defined_all]]
apply (induct K)
(*K=0*)
apply (simp add: INVS_soundK_def , clarsimp)
  apply (unfold validn_def)
  apply (rule, rule) apply (erule_tac x=M in allE, erule impE, assumption)
  apply (rule, rule, rule, rule)
  apply (erule_tac x=Mspec in allE, erule_tac x=Minv in allE, erule_tac x=Annoa in allE, erule impE, assumption)
  apply (rule, rule, rule, rule)
  apply (erule_tac x=par in allE, erule_tac x=code in allE, erule_tac x=l0 in allE, erule impE, assumption)
  apply (rule, rule, rule)
  apply (rule, rule, rule)
  apply rule  
    apply (rule, rule, rule) apply (case_tac k, clarsimp)  apply (drule no_zero_height_Exec_derivs, simp) apply clarsimp
       apply (erule eval_cases) apply (simp add: INVS_SC_def mbody_is_def,clarsimp) apply clarsimp
       apply (drule no_zero_height_Exec_derivs, simp)
   apply (rule, rule, rule, rule)
     apply clarsimp 
           apply (case_tac k, clarsimp) apply (drule ZeroHeightMultiElim, clarsimp) 
             apply (simp add: INVS_SC_def mbody_is_def,clarsimp)
           apply clarsimp
               apply (drule MultiSplit, simp, clarsimp) apply (drule no_zero_height_Step_derivs, simp)
   apply rule apply (case_tac k, clarsimp) apply (drule ZeroHeightReachableElim, clarsimp)
          apply (simp add: INVS_SC_def mbody_is_def,clarsimp) 
         apply clarsimp apply (drule ReachableSplit, simp, clarsimp)
        apply (erule disjE)
         apply clarsimp  apply (drule no_zero_height_Step_derivs, simp)
         apply clarsimp  apply (drule ZeroHeightReachableElim, clarsimp)
         apply (rotate_tac 5, erule thin_rl)
          apply (simp add: INVS_SC_def mbody_is_def,clarsimp)  
             apply (simp add: MST_validn_def)
             apply (erule_tac x=D in allE, rotate_tac -1)
             apply (erule_tac x=m' in allE, rotate_tac -1)
             apply (erule_tac x=para in allE, rotate_tac -1)
             apply (erule_tac x=codea in allE, rotate_tac -1)
             apply (erule_tac x=l0a in allE, rotate_tac -1,erule impE) apply (simp add: mbody_is_def)
             apply (rotate_tac -1, erule_tac x=T in allE)
             apply (rotate_tac -1, erule_tac x=MI in allE, clarsimp)
             apply (simp add: validn_def)
             apply (simp add: mbody_is_def)
             apply (simp add: heap_def)
(*k>0*)
apply (simp add: INVS_soundK_def , clarsimp)
apply (rotate_tac -1, erule thin_rl)
apply (unfold validn_def)
apply (rule, rule) apply (erule_tac x=M in allE, erule impE, assumption)
apply (rule, rule) apply (rule, rule) apply (rule, rule) apply (rule, rule) apply (rule, rule) 
  apply (erule_tac x=Mspec in allE, erule_tac x=Minv in allE, erule_tac x=Annoa in allE, erule impE, assumption)
  apply (erule_tac x=par in allE, erule_tac x=code in allE)
  apply (erule_tac x=l0 in allE, erule impE, assumption)
apply (rule, rule) 
apply (rule, rule)
apply (erule_tac x=s0 in allE)
apply rule
(*Exec*)
  apply (rule, rule, rule)
   apply (erule eval_cases) apply clarsimp apply (simp add: INVS_SC_def mbody_is_def) apply clarsimp
   apply (erule_tac x=t in allE, erule impE)
     apply (frule InvokeElim)  apply (simp add: INVS_SC_def mbody_is_def) apply clarsimp apply fastforce
     apply (simp add: MS_def, erule exE, rule) apply clarsimp apply (erule MultiApp) apply assumption
   apply (erule impE, drule InvokeElim, simp add: INVS_SC_def mbody_is_def) apply clarsimp apply fastforce
     apply clarsimp apply (simp add: INVS_SC_def mbody_is_def SINV_pre_def) apply clarsimp apply (rule, rule)
        apply (rule, rule, rule, assumption) apply (rule, rule) prefer 2 apply (rule, assumption) apply simp
        apply (simp add: MST_validn_def) apply (erule_tac x=D in allE, erule_tac x=m' in allE)
          apply (erule_tac x=parb in allE, erule_tac x=codeb in allE) 
          apply (erule_tac x=l0b in allE, simp add: mbody_is_def) 
          apply (simp add: validn_def) 
          apply (erule_tac x=parb in allE, erule_tac x=codeb in allE) 
          apply (erule_tac x=l0b in allE, simp add: mbody_is_def) 
          apply (rotate_tac -1, erule_tac x=R in allE, erule_tac x=bb in allE)
          apply (rotate_tac -1, erule_tac x="[]" in allE, rotate_tac -1, erule_tac x=R in allE, erule_tac x=bb in allE)
          apply (simp add: mkState_def)
          apply (erule impE) apply (simp add: MS_def, rule) apply (rule MS_zero) apply simp apply simp apply simp
          apply (erule_tac x=ka in allE, erule impE, simp) 
          apply (simp add: mkPost_def, erule conjE)
          apply (erule_tac x=hh in allE, erule_tac x=va in allE, simp add: mkState_def)
        apply (erule_tac x=ma in allE, erule impE) apply (simp add: max_def) apply (case_tac "n ≤ ma") apply clarsimp apply clarsimp
         apply (erule conjE) apply (erule_tac x=h in allE, erule_tac x=v in allE, erule impE)
         apply (drule InvokeElim) apply (simp add: INVS_SC_def mbody_is_def) apply clarsimp apply fastforce
           apply clarsimp 
         apply (simp add: SINV_post_def) apply (simp add: INVS_SC_def mbody_is_def, clarsimp)
           apply (drule InvokeElim, clarsimp) apply fastforce apply clarsimp
           apply (simp add: mbody_is_def, clarsimp)
           apply (erule_tac x=ac in allE, erule_tac x=ops in allE, rotate_tac -1)
           apply (erule_tac x=ad in allE, erule_tac x=R in allE, rotate_tac -1, erule impE, assumption) 
           apply (erule_tac x=bb in allE, simp, erule mp)
           apply (simp add: MST_validn_def)
           apply (erule_tac x=D in allE, erule_tac x=m' in allE, rotate_tac -1)
           apply (erule_tac x=par in allE, erule_tac x=code in allE,  erule_tac x=l0 in allE, simp add: mbody_is_def)
           apply (simp add: validn_def)
           apply (rotate_tac -1) apply (erule thin_rl) apply (rotate_tac -1) 
           apply (simp add: mbody_is_def) 
           apply (erule_tac x=R in allE, rotate_tac -1, erule_tac x=bb in allE, rotate_tac -1)
           apply (erule_tac x="[]" in allE, rotate_tac -1, erule_tac x=R in allE, rotate_tac -1)
           apply (erule_tac x=bb in allE, erule impE)
             apply (simp add: MS_def, rule, rule MS_zero) apply (simp, simp add: mkState_def, simp)
           apply (simp add: mkState_def)
           apply (erule_tac x=k in allE, clarsimp)
           apply (erule_tac x=bc in allE, erule_tac x=va in allE, simp add: mkPost_def mkState_def)
(*MStep*)
apply (rule, rule)           
apply (rule, rule)
apply (rule, rule)
   apply (case_tac k, clarsimp) apply (drule ZeroHeightMultiElim, clarsimp) apply (simp add: INVS_SC_def) apply clarsimp
   apply clarsimp
   apply (frule MultiSplit) apply clarsimp apply clarsimp 
     apply (frule InvokeElim)  apply (simp add: INVS_SC_def mbody_is_def) apply clarsimp apply fastforce
     apply clarsimp
     apply (erule_tac x="v # ops" in allE, erule_tac x=ad in allE, erule_tac x=b in allE, erule impE)
     apply (simp add: MS_def, erule exE, rule)  apply (erule MultiApp) apply assumption
       apply (erule impE, simp add: SINV_pre_def INVS_SC_def mbody_is_def) apply clarsimp 
        apply (rule, rule, rule, rule, rule, assumption) apply (rule, rule) 
          prefer 2 apply (rule, assumption) apply simp
        apply (simp add: MST_validn_def) apply (erule_tac x=D in allE, erule_tac x=m' in allE)
          apply (erule_tac x=parb in allE, erule_tac x=codeb in allE) 
          apply (erule_tac x=l0b in allE, simp add: mbody_is_def) 
          apply (simp add: validn_def) 
          apply (erule_tac x=parb in allE, erule_tac x=codeb in allE) 
          apply (erule_tac x=l0b in allE, simp add: mbody_is_def) 
          apply (rotate_tac -1, erule_tac x=R in allE, erule_tac x=bb in allE)
          apply (rotate_tac -1, erule_tac x="[]" in allE, rotate_tac -1, erule_tac x=R in allE, erule_tac x=bb in allE)
          apply (simp add: mkState_def)
          apply (erule impE) apply (simp add: MS_def, rule) apply (rule MS_zero) apply simp apply simp apply simp
          apply (erule_tac x=k in allE, erule impE, simp) 
          apply (simp add: mkPost_def, erule conjE)
          apply (erule_tac x=hh in allE, erule_tac x=va in allE, simp add: mkState_def)
        apply (erule_tac x=ma in allE, erule impE) apply simp 
         apply (erule conjE) apply (erule_tac x=ll in allE, erule_tac x=ae in allE)
           apply (erule_tac x=af in allE, rotate_tac -1, erule_tac x=bc in allE, clarsimp)
(*Reach*)
apply rule
  apply (case_tac k, clarsimp) apply (drule ZeroHeightReachableElim, clarsimp)
       apply (simp add: INVS_SC_def mbody_is_def, clarsimp)
  apply clarsimp
  apply (drule ReachableSplit) apply simp apply clarsimp
  apply (erule disjE)
    apply clarsimp 
         apply (frule InvokeElim) apply (simp add: INVS_SC_def mbody_is_def) apply clarsimp apply fastforce
           apply clarsimp 
           apply (erule_tac x="v#ops" in allE, erule_tac x=ad in allE, erule_tac x=b in allE, erule impE)
           apply (simp add: MS_def, clarsimp, rule) apply (erule MultiApp) apply assumption
         apply (erule impE) apply (simp add: SINV_pre_def) apply (simp add: INVS_SC_def mbody_is_def, clarsimp)
            apply (rule, rule, rule, rule, rule) apply assumption 
            apply (rule, rule) prefer 2 apply (rule, assumption, simp)
           apply (simp add: MST_validn_def)
           apply (erule_tac x=D in allE, erule_tac x=m' in allE, rotate_tac -1)
           apply (erule_tac x=parb in allE, erule_tac x=codeb in allE,  erule_tac x=l0b in allE, simp add: mbody_is_def)
           apply (simp add: validn_def)
           apply (simp add: mbody_is_def) apply (rotate_tac -1)
           apply (erule_tac x=R in allE, rotate_tac -1, erule_tac x=bb in allE, rotate_tac -1)
           apply (erule_tac x="[]" in allE, rotate_tac -1, erule_tac x=R in allE, rotate_tac -1)
           apply (erule_tac x=bb in allE, erule impE)
             apply (simp add: MS_def, rule, rule MS_zero) apply (simp, simp add: mkState_def, simp)
           apply (simp add: mkState_def)
           apply (erule_tac x=k in allE, clarsimp)
           apply (erule_tac x=b in allE, erule_tac x=v in allE, simp add: mkPost_def mkState_def)
        apply (erule_tac x=ma in allE, clarsimp)
        apply (rotate_tac -1)
        apply (simp add: SINV_inv_def)
        apply (erule_tac x="l+1" in allE, erule_tac x=ae in allE)
        apply (erule_tac x=af in allE, rotate_tac -1, erule_tac x=bc in allE, clarsimp)
        apply (rotate_tac -2, erule thin_rl)
        apply (simp add: SINV_inv_def INVS_SC_def mbody_is_def) apply clarsimp 
        apply (rotate_tac -1, erule_tac x=ac in allE)
        apply (rotate_tac -1, erule_tac x=ops in allE)
        apply (rotate_tac -1, erule_tac x=ad in allE)
        apply (rotate_tac -1, erule_tac x=R in allE, clarsimp)
        apply (rotate_tac -1, erule_tac x=bb in allE, erule mp)
        apply (erule thin_rl)
           apply (simp add: MST_validn_def)
           apply (erule_tac x=D in allE, erule_tac x=m' in allE, rotate_tac -1)
           apply (erule_tac x=parb in allE, erule_tac x=codeb in allE,  erule_tac x=l0b in allE, simp add: mbody_is_def)
           apply (simp add: validn_def)
           apply (simp add: mbody_is_def) apply (rotate_tac -1)
           apply (erule_tac x=R in allE, rotate_tac -1, erule_tac x=bb in allE, rotate_tac -1)
           apply (erule_tac x="[]" in allE, rotate_tac -1, erule_tac x=R in allE, rotate_tac -1)
           apply (erule_tac x=bb in allE, erule impE)
             apply (simp add: MS_def, rule, rule MS_zero) apply (simp, simp add: mkState_def, simp)
           apply (simp add: mkState_def)
           apply (erule_tac x=k in allE, clarsimp)
           apply (erule_tac x=b in allE, erule_tac x=v in allE, simp add: mkPost_def mkState_def)
  apply clarsimp
  apply (simp add: INVS_SC_def mbody_is_def, clarsimp) 
  apply (rotate_tac -1, erule_tac x=ab in allE)
  apply (rotate_tac -1, erule_tac x=ba in allE)
  apply (rotate_tac -1, erule_tac x=ac in allE)
  apply (rotate_tac -1, erule_tac x=ops1 in allE)
  apply (rotate_tac -1, erule_tac x=ad in allE)
  apply (rotate_tac -1, erule_tac x=R in allE, clarsimp)
  apply (rotate_tac -1, erule_tac x=bb in allE, clarsimp)
  apply (rotate_tac -1, erule_tac x="heap (ae,af,bc)" in allE, erule mp)
  apply (rotate_tac 6) apply (erule thin_rl)
  apply (simp add: MST_validn_def)
  apply (erule_tac x=D in allE, erule_tac x=m' in allE)
  apply (simp add: mbody_is_def)
  apply (simp add: validn_def)
  apply (simp add: mbody_is_def mkInv_def)
  apply (rotate_tac -1)
  apply (erule_tac x=R in allE, erule_tac x=bb in allE)
  apply (rotate_tac -1) apply (erule_tac x="[]" in allE)
  apply (rotate_tac -1)
  apply (erule_tac x=R in allE, erule_tac x=bb in allE, simp add: mkState_def, erule impE)
  apply (simp add: MS_def, rule, rule MS_zero) apply (simp, simp, simp)
  apply (erule_tac x=nat in allE, simp)
done
(*>*)


text‹The heart of the soundness proof - the induction on the
axiomatic semantics.›

lemma SOUND_Aux[rule_format]: 
"(b,G,C,m,l,A,B,I):SP_Judgement ⟹ G_validn K G ⟶ MST_validn K ⟶ 
  ((b ⟶ ⊨⇩K ⦃A⦄ C, m, l ⦃B⦄ I) ∧ 
   ((¬ b) ⟶ ⊨⇩(Suc K) ⦃A⦄ C, m, l ⦃B⦄ I))"
(*<*)
supply [[simproc del: defined_all]]
apply (erule SP_Judgement.induct)
(*INSTR*)
apply clarsimp
apply (rotate_tac -4) apply (erule thin_rl)
apply (simp add: mbody_is_def validn_def Opsem_def MS_def Reach_def, clarsimp)
apply rule
  apply clarsimp apply (erule eval_cases) apply simp
    apply clarsimp apply (frule InstrElimNext, simp, assumption, clarsimp)
    apply (erule_tac x=ad in allE)
    apply (erule_tac x=bb in allE)
    apply (erule_tac x=a in allE, rotate_tac -1)
    apply (erule_tac x=aa in allE)
    apply (erule_tac x=b in allE, erule impE)
      apply rule
        apply (erule MultiApp)
        apply assumption
      apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule, assumption)
         apply (rule, rule,assumption) 
      apply (erule_tac x=ma in allE, clarsimp)
      apply (erule_tac x=h in allE, erule_tac x=v in allE, clarsimp)
      apply (simp add: SP_post_def) 
       apply (rotate_tac -1)
       apply (erule_tac x=ae in allE, rotate_tac -1)
       apply (erule_tac x=af in allE, rotate_tac -1)
       apply (erule_tac x=bc in allE, erule mp)
         apply (rule, rule, assumption)
apply clarsimp
apply rule
  apply clarsimp 
    apply (case_tac ka) apply clarsimp apply (drule ZeroHeightMultiElim) apply clarsimp
    apply clarsimp
    apply (rotate_tac -2, drule MultiSplit) apply simp apply clarsimp
      apply (frule InstrElimNext, simp, assumption, clarsimp)
      apply (erule_tac x=ad in allE)
      apply (erule_tac x=bb in allE)
      apply (erule_tac x=ag in allE, rotate_tac -1)
      apply (erule_tac x=ah in allE)
      apply (erule_tac x=bd in allE, erule impE)
        apply rule
          apply (erule MultiApp)
          apply assumption
       apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule, assumption)
         apply (rule, rule, assumption) 
      apply (erule_tac x=ma in allE, clarsimp)
      apply (erule_tac x=ll in allE, rotate_tac -1)
      apply (erule_tac x=a in allE, rotate_tac -1)
      apply (erule_tac x=aa in allE, rotate_tac -1)
      apply (erule_tac x=b in allE, clarsimp)
  apply clarsimp 
    apply (case_tac ka) apply clarsimp apply (drule ZeroHeightReachableElim) apply clarsimp
    apply clarsimp
    apply (rotate_tac -2, drule ReachableSplit) apply simp apply clarsimp
    apply (rotate_tac -1, erule disjE)
      apply clarsimp
      apply (frule InstrElimNext, simp, assumption, clarsimp)
      apply (erule_tac x=ad in allE)
      apply (erule_tac x=bb in allE)
      apply (erule_tac x=ag in allE, rotate_tac -1)
      apply (erule_tac x=ah in allE)
      apply (erule_tac x=bd in allE, erule impE)
        apply rule
          apply (erule MultiApp)
          apply assumption
       apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule, assumption)
         apply (rule, rule, assumption) 
       apply (erule_tac x=ma in allE, clarsimp)
         apply (rotate_tac -1, erule_tac x=ll in allE)
         apply (rotate_tac -1, erule_tac x=a in allE)
         apply (rotate_tac -1, erule_tac x=aa in allE)
         apply (rotate_tac -1, erule_tac x=b in allE, clarsimp)
         apply (simp add: SP_inv_def) 
(*         apply (rotate_tac -1, erule_tac x="l+1" in allE)*)
         apply (rotate_tac -1, erule_tac x=ae in allE)
         apply (rotate_tac -1, erule_tac x=af in allE)
         apply (rotate_tac -1, erule_tac x=bc in allE, erule mp) apply (rule, rule, assumption)
    apply clarsimp
(*GOTO*)
apply clarsimp
apply (rotate_tac 5) apply (erule thin_rl)
apply (simp add: mbody_is_def validn_def Opsem_def MS_def Reach_def, clarsimp)
apply rule
  apply clarsimp apply (erule eval_cases) apply simp
    apply clarsimp apply (drule GotoElim1) apply (simp, clarsimp)
    apply (erule_tac x=ad in allE)
    apply (erule_tac x=bb in allE)
    apply (erule_tac x=ae in allE, rotate_tac- 1)
    apply (erule_tac x=af in allE)
    apply (erule_tac x=bc in allE, erule impE)
      apply rule
        apply (erule MultiApp)
          apply (erule Goto) 
    apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule, assumption)
         apply (rule, rule, erule Goto) 
         apply (erule_tac x=ma in allE, clarsimp) 
         apply (erule_tac x=h in allE, erule_tac x=v in allE, clarsimp)
         apply(simp add: SP_post_def, rotate_tac -1) 
         apply (erule_tac x=ae in allE, rotate_tac -1)
         apply (erule_tac x=af in allE, rotate_tac -1)
         apply (erule_tac x=bc in allE, erule mp)
           apply (rule, rule, erule Goto) 
apply clarsimp
apply rule
  apply clarsimp 
    apply (case_tac ka) apply clarsimp apply (drule ZeroHeightMultiElim) apply clarsimp 
    apply clarsimp
    apply (rotate_tac -2, drule MultiSplit) apply simp apply clarsimp
      apply (drule GotoElim1) apply simp apply clarsimp 
      apply (erule_tac x=ad in allE)
      apply (erule_tac x=bb in allE)
      apply (erule_tac x=ae in allE,rotate_tac -1)
      apply (erule_tac x=af in allE)
      apply (erule_tac x=bc in allE, erule impE)
        apply rule
          apply (erule MultiApp)
            apply (erule Goto) 
       apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule, assumption)
         apply (rule, rule, erule Goto) 
      apply (erule_tac x=ma in allE, clarsimp)
      apply (erule_tac x=ll in allE, rotate_tac -1)
      apply (erule_tac x=a in allE, rotate_tac -1)
      apply (erule_tac x=aa in allE)
      apply (erule_tac x=b in allE, clarsimp)
  apply clarsimp 
    apply (case_tac ka) apply clarsimp apply (drule ZeroHeightReachableElim) apply clarsimp 
    apply clarsimp
    apply (rotate_tac -2, drule ReachableSplit) apply simp apply clarsimp
      apply (drule GotoElim1) apply simp apply clarsimp 
      apply (erule_tac x=ad in allE)
      apply (erule_tac x=bb in allE)
      apply (erule_tac x=ae in allE,rotate_tac -1)
      apply (erule_tac x=af in allE)
      apply (erule_tac x=bc in allE, erule impE)
        apply rule
          apply (erule MultiApp)
            apply (erule Goto) 
       apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule, assumption)
         apply (rule, rule, erule Goto) 
      apply (erule_tac x=ma in allE, clarsimp)
         apply (rotate_tac -1, erule_tac x=ll in allE)
         apply (rotate_tac -1, erule_tac x=a in allE)
         apply (rotate_tac -1, erule_tac x=aa in allE)
         apply (rotate_tac -1, erule_tac x=b in allE, clarsimp)
         apply (simp add: SP_inv_def) 
(*         apply (rotate_tac -1, erule_tac x=pc in allE)*)
         apply (rotate_tac -1, erule_tac x=ae in allE)
         apply (rotate_tac -1, erule_tac x=af in allE)
         apply (rotate_tac -1, erule_tac x=bc in allE, erule mp)
         apply (rule, rule) 
            apply (erule Goto) 
(*If*) 
apply clarsimp
apply (rotate_tac 5) apply (erule thin_rl,erule thin_rl)
apply (simp add: mbody_is_def validn_def Opsem_def MS_def Reach_def, clarsimp)
apply rule
  apply clarsimp apply (erule eval_cases) apply simp
    apply clarsimp apply (drule IfElim1) apply (simp, clarsimp)
    apply (erule disjE)
    apply clarsimp
      apply (rotate_tac 3) apply (erule thin_rl)
      apply (rotate_tac -1)
      apply (erule_tac x=ad in allE)
      apply (erule_tac x=bb in allE)
      apply (erule_tac x=a in allE, rotate_tac -1)
      apply (erule_tac x=af in allE)
      apply (erule_tac x=bc in allE, erule impE)
        apply rule
          apply (erule MultiApp)
            apply (erule IfT, simp) 
      apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule) prefer 2 
            apply (rule, rule, erule IfT, simp) apply fastforce
         apply (erule_tac x=ma in allE, clarsimp)
           apply (erule_tac x=h in allE, erule_tac x=v in allE, clarsimp)
           apply (simp add: SP_post_def)
           apply (rotate_tac -1)
           apply (erule_tac x="TRUE # a" in allE, erule_tac x=af in allE, erule_tac x=bc in allE, erule impE)
             apply (rule, rule, rule IfT, simp,simp)
           apply clarsimp
    apply clarsimp
      apply (rotate_tac 2) apply (erule thin_rl)
      apply (erule_tac x=ad in allE)
      apply (erule_tac x=bb in allE)
      apply (erule_tac x=a in allE, rotate_tac -1)
      apply (erule_tac x=af in allE)
      apply (erule_tac x=bc in allE, erule impE)
        apply rule
          apply (erule MultiApp)
            apply (rule IfF) apply (simp, assumption, simp) apply simp
      apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule) prefer 2 
            apply (rule, rule, rule IfF) apply (simp, assumption) apply fastforce
            apply simp
            apply clarsimp
         apply (erule_tac x=ma in allE, clarsimp)
           apply (erule_tac x=h in allE, erule_tac x=v in allE, clarsimp)
           apply (simp add: SP_post_def)
           apply (rotate_tac -1)
           apply (erule_tac x="va # a" in allE, erule_tac x=af in allE, erule_tac x=bc in allE, erule impE)
             apply (rule, rule, rule IfF) apply (simp, assumption) apply fastforce apply simp
           apply clarsimp
apply clarsimp
apply rule
  apply clarsimp 
    apply (case_tac ka) apply clarsimp apply (drule ZeroHeightMultiElim) apply clarsimp 
    apply clarsimp
    apply (rotate_tac -2, drule MultiSplit) apply simp apply clarsimp
      apply (drule IfElim1) apply simp apply clarsimp 
      apply (erule disjE)
      apply clarsimp
        apply (rotate_tac 4) apply (erule thin_rl)
        apply (rotate_tac -1)
        apply (erule_tac x=ad in allE)
        apply (erule_tac x=bb in allE)
        apply (erule_tac x=ag in allE, rotate_tac -1)
        apply (erule_tac x=af in allE)
        apply (erule_tac x=bc in allE, erule impE)
          apply rule
            apply (erule MultiApp)
              apply (rule IfT) apply (simp, fastforce) 
        apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule,rule) prefer 2 
           apply (rule, rule, rule IfT) apply simp apply fastforce
           apply clarsimp
        apply (erule_tac x=ma in allE, clarsimp)
        apply (erule_tac x=ll in allE, rotate_tac -1)
        apply (erule_tac x=a in allE, rotate_tac -1)
        apply (erule_tac x=aa in allE, rotate_tac -1)
        apply (erule_tac x=b in allE, rotate_tac -1, clarsimp)
      apply clarsimp
        apply (rotate_tac 3) apply (erule thin_rl)
        apply (erule_tac x=ad in allE)
        apply (erule_tac x=bb in allE)
        apply (erule_tac x=ag in allE, rotate_tac -1)
        apply (erule_tac x=af in allE)
        apply (erule_tac x=bc in allE, erule impE)
          apply rule
            apply (erule MultiApp)
              apply (rule IfF) apply (simp, assumption, simp) apply simp
        apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule) prefer 2 
           apply (rule, rule, rule IfF) apply (simp, assumption) apply fastforce apply simp 
           apply clarsimp
        apply (erule_tac x=ma in allE, clarsimp)
        apply (erule_tac x=ll in allE, rotate_tac -1)
        apply (erule_tac x=a in allE, rotate_tac -1)
        apply (erule_tac x=aa in allE, rotate_tac -1)
        apply (erule_tac x=b in allE, rotate_tac -1, clarsimp)
  apply clarsimp 
    apply (case_tac ka) apply clarsimp apply (drule ZeroHeightReachableElim) apply clarsimp 
    apply clarsimp
    apply (rotate_tac -2, drule ReachableSplit) apply simp apply clarsimp
      apply (drule IfElim1) apply simp apply clarsimp 
      apply (erule disjE)
      apply clarsimp
        apply (rotate_tac 4) apply (erule thin_rl)
        apply (rotate_tac -1)
        apply (erule_tac x=ad in allE)
        apply (erule_tac x=bb in allE)
        apply (erule_tac x=ag in allE, rotate_tac -1)
        apply (erule_tac x=af in allE)
        apply (erule_tac x=bc in allE, erule impE)
          apply rule
            apply (erule MultiApp)
              apply (rule IfT) apply (simp, fastforce) 
        apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule) prefer 2 
           apply (rule, rule, rule IfT) apply simp apply fastforce
           apply clarsimp
        apply (erule_tac x=ma in allE, clarsimp)
         apply (rotate_tac -1, erule_tac x=ll in allE)
         apply (rotate_tac -1, erule_tac x=a in allE)
         apply (rotate_tac -1, erule_tac x=aa in allE)
         apply (rotate_tac -1, erule_tac x=b in allE, clarsimp)
         apply (simp add: SP_inv_def) 
(*         apply (rotate_tac -1, erule_tac x=pc in allE)*)
         apply (rotate_tac -1, erule_tac x="TRUE#ag" in allE)
         apply (rotate_tac -1, erule_tac x=af in allE)
         apply (rotate_tac -1, erule_tac x=bc in allE)
         apply (rotate_tac -1, erule impE)
            apply (rule, rule, erule IfT) apply simp
         apply clarsimp
      apply clarsimp
        apply (rotate_tac 3) apply (erule thin_rl)
        apply (erule_tac x=ad in allE)
        apply (erule_tac x=bb in allE)
        apply (erule_tac x=ag in allE, rotate_tac -1)
        apply (erule_tac x=af in allE)
        apply (erule_tac x=bc in allE, erule impE)
          apply rule
            apply (erule MultiApp)
              apply (erule IfF) apply (assumption, simp, simp) 
        apply (erule impE, simp add: SP_pre_def) apply (rule, rule, rule, rule) prefer 2 
           apply (rule, rule, erule IfF) apply (assumption, fastforce,simp) 
           apply clarsimp
        apply (erule_tac x=ma in allE, clarsimp)
         apply (rotate_tac -1, erule_tac x=ll in allE)
         apply (rotate_tac -1, erule_tac x=a in allE)
         apply (rotate_tac -1, erule_tac x=aa in allE)
         apply (rotate_tac -1, erule_tac x=b in allE, clarsimp)
         apply (simp add: SP_inv_def) 
(*         apply (rotate_tac -1, erule_tac x="Suc l" in allE)*)
         apply (rotate_tac -1, erule_tac x="v#ag" in allE)
         apply (rotate_tac -1, erule_tac x=af in allE)
         apply (rotate_tac -1, erule_tac x=bc in allE)
         apply (rotate_tac -1, erule impE)
         apply (rule, rule) 
            apply (erule IfF) apply (assumption, simp, simp) 
         apply clarsimp
(*RET*)
apply clarsimp
apply (simp add: mbody_is_def validn_def Opsem_def MS_def Reach_def, clarsimp)
apply rule
  apply clarsimp apply (erule eval_cases) apply clarsimp
    apply (drule RetElim1) apply simp apply simp
apply clarsimp
apply rule
  apply clarsimp 
    apply (case_tac ka) apply clarsimp apply (drule ZeroHeightMultiElim) apply clarsimp 
    apply clarsimp
    apply (rotate_tac -2, drule MultiSplit) apply simp apply clarsimp
      apply (drule RetElim1, clarsimp) apply simp  
apply clarsimp 
    apply (case_tac ka) apply clarsimp apply (drule ZeroHeightReachableElim) apply clarsimp 
    apply clarsimp
    apply (rotate_tac -2, drule ReachableSplit) apply simp apply clarsimp
      apply (drule RetElim1, clarsimp) apply simp  
(*INVS*)
apply clarsimp
  apply (subgoal_tac "INVS_soundK K G C m l D m' T MI Anno Anno2 (par,code,l0) A B I")
  apply (simp add: INVS_soundK_def) 
  apply (erule impE) apply (simp add: INVS_SC_def) apply (rule, rule, rule, rule) apply assumption apply (rule, assumption)
     apply assumption
  apply assumption
  apply (rule INVS_soundK_all)
(*CONSEQ*)
apply clarsimp 
apply rule
  apply clarsimp
  apply (simp add: validn_def,clarsimp)
  apply (erule thin_rl)
  apply (rotate_tac 5, erule thin_rl)
  apply (erule_tac x=a in allE, rotate_tac -1)
  apply (erule_tac x=aa in allE, rotate_tac -1)
  apply (erule_tac x=ba in allE, clarsimp, rotate_tac -1)
  apply (erule_tac x=ab in allE)
  apply (erule_tac x=bb in allE) 
  apply (rotate_tac -1)
  apply (erule_tac x=ac in allE, rotate_tac -1)
  apply (erule_tac x=ad in allE, rotate_tac -1)
  apply (erule_tac x=bc in allE, clarsimp)
  apply (erule_tac x=k in allE, clarsimp)
  apply (rotate_tac -1)
    apply (erule_tac x=ll in allE, rotate_tac -1)
    apply (erule_tac x=ae in allE, rotate_tac -1)
    apply (erule_tac x=af in allE)
    apply (erule_tac x=bd in allE, clarsimp)
  apply clarsimp
  apply (simp add: validn_def,clarsimp)
  apply (erule thin_rl)
  apply (rotate_tac 5, erule thin_rl)
  apply (erule_tac x=a in allE, rotate_tac -1)
  apply (erule_tac x=aa in allE, rotate_tac -1)
  apply (erule_tac x=ba in allE, clarsimp, rotate_tac -1)
  apply (erule_tac x=ab in allE)
  apply (erule_tac x=bb in allE) 
  apply (rotate_tac -1)
  apply (erule_tac x=ac in allE, rotate_tac -1)
  apply (erule_tac x=ad in allE, rotate_tac -1)
  apply (erule_tac x=bc in allE, clarsimp)
  apply (erule_tac x=k in allE, clarsimp)
  apply (rotate_tac -1)
    apply (erule_tac x=ll in allE, rotate_tac -1)
    apply (erule_tac x=ae in allE, rotate_tac -1)
    apply (erule_tac x=af in allE)
    apply (erule_tac x=bd in allE, clarsimp)
(*INJECT*)
apply clarsimp apply (rule validn_lower) apply fast apply simp
(*AX*)
apply clarsimp apply (simp add: G_validn_def) 
done
(*>*)

text‹The statement of this lemma gives a semantic interpretation of
the two judgement forms, as ‹SP_Assum›-judgements enjoy validity
up to execution height $K$, while ‹SP_Deriv›-judgements are
valid up to level $K+1$.›

(*<*)
lemma SOUND_K: 
  "⟦ G ⊳ ⦃A⦄ C,m,l ⦃B⦄ I; G_validn K G ; MST_validn K⟧  
  ⟹ ⊨⇩(Suc K) ⦃A⦄ C, m, l ⦃B⦄ I"
apply (drule SOUND_Aux)  apply assumption+ apply simp
done
(*>*)

text‹From this, we obtain a soundness result that still involves
context validity.›

theorem SOUND_in_CTXT: 
 "⟦G ⊳ ⦃A⦄ C,m,l ⦃B⦄ I; G_valid G; MST_valid⟧ ⟹ ⊨ ⦃A⦄ C, m, l ⦃B⦄ I"
(*<*)
apply (rule validn_valid)
apply clarsimp
apply (rule validn_lower)
apply (erule SOUND_K)
prefer 3 apply (subgoal_tac "K ≤ Suc K", assumption) apply simp
apply (erule G_valid_validn)
apply (erule MST_valid_validn)
done
(*>*)

text‹We will now show that the two semantic assumptions can be replaced by
the verified-program property.›

subsection‹Soundness of verified programs \label{SectionContextElimination}› 

text‹In order to obtain a soundness result that does not require
validity assumptions of the context or the specification table,
we show that the ‹VP› property implies context validity.
First, the elimination of contexts. By induction on
‹k› we prove›

lemma VPG_MSTn_Gn[rule_format]:
"VP_G G ⟶ MST_validn k ⟶ G_validn k G"
(*<*)
apply (induct k)
(*k=0*)
  apply clarsimp
    apply (simp add: VP_G_def, clarsimp) 
    apply (simp add: G_validn_def, clarsimp)
    apply (simp add: validn_def) apply clarsimp 
        apply rule 
          apply clarsimp apply (drule no_zero_height_Exec_derivs) apply simp
        apply clarsimp
        apply rule
          apply clarsimp apply (drule ZeroHeightMultiElim) apply clarsimp
            apply (rotate_tac 2)
            apply (erule_tac x=C in allE, erule_tac x=m in allE)
            apply (erule_tac x=a in allE, erule_tac x=aa in allE, erule_tac x=b in allE, clarsimp)
            apply (erule_tac x=C in allE, erule_tac x=m in allE)
            apply (erule_tac x=l in allE, erule_tac x=A in allE, erule_tac x=B in allE, clarsimp)
            apply (rule AssertionsImplyAnnoInvariants)
             prefer 3 apply assumption
             apply assumption+
          apply clarsimp apply (drule ZeroHeightReachableElim) apply clarsimp
            apply (rotate_tac 2)
            apply (erule_tac x=C in allE, erule_tac x=m in allE)
            apply (erule_tac x=a in allE, erule_tac x=aa in allE, erule_tac x=b in allE, clarsimp)
            apply (erule_tac x=C in allE, erule_tac x=m in allE, 
                   erule_tac x=l in allE, erule_tac x=A in allE, erule_tac x=B in allE, clarsimp)
            apply (erule AssertionsImplyMethInvariants, assumption+)
(*k>0*)
 apply clarsimp apply (simp add: VP_G_def)
   apply (simp (no_asm) add: G_validn_def, clarsimp)
   apply (subgoal_tac "MST_validn k", clarsimp)
   apply (rule SOUND_K) apply fast 
   apply assumption
   apply assumption
   apply (erule MST_validn_lower) apply simp 
done
(*>*)

text‹which implies›

lemma VPG_MST_G: "⟦VP_G G; MST_valid⟧ ⟹ G_valid G"
(*<*)
apply (rule G_validn_valid, clarsimp)
apply (erule VPG_MSTn_Gn)
apply (erule MST_valid_validn)
done
(*>*)

text‹Next, the elimination of ‹MST_valid›. Again by induction on
‹k›, we prove›

lemma VPG_MSTn[rule_format]: "VP_G G ⟶ MST_validn k"
(*<*)
apply (induct k)
apply (simp add: MST_validn_def, clarsimp)
  apply (simp add: validn_def, clarsimp)
  apply rule
    apply clarsimp apply (drule no_zero_height_Exec_derivs) apply simp 
  apply clarsimp
  apply rule
    apply clarsimp apply (drule ZeroHeightMultiElim) apply clarsimp 
    apply (simp add: VP_G_def, clarsimp, rotate_tac -1)
    apply (erule_tac x=C in allE, erule_tac x=m in allE)
    apply (erule_tac x=par in allE, erule_tac x=code in allE, erule_tac x=l0 in allE, clarsimp)
    apply (rule AssertionsImplyAnnoInvariants) apply fast apply assumption+ apply simp
  apply clarsimp apply (drule ZeroHeightReachableElim) apply clarsimp
    apply (simp add: VP_G_def, clarsimp, rotate_tac -1)
    apply (erule_tac x=C in allE, erule_tac x=m in allE)
    apply (erule_tac x=par in allE, erule_tac x=code in allE, erule_tac x=l0 in allE, clarsimp)
    apply (frule AssertionsImplyMethInvariants) apply assumption apply (simp add: mkState_def) 
apply clarsimp
  apply (frule VPG_MSTn_Gn, assumption)
  apply (simp add: VP_G_def)
  apply (simp (no_asm) add: MST_validn_def, clarsimp)
  apply (rule SOUND_K)
   apply (rotate_tac 3) 
   apply (erule_tac x=C in allE, erule_tac x=m in allE)
   apply (erule_tac x=par in allE, erule_tac x=code in allE, erule_tac x=l0 in allE, clarsimp) apply assumption
  apply assumption
  apply assumption
done
(*>*)

text‹which yields›

lemma VPG_MST:"VP_G G ⟹ MST_valid"
(*<*)
apply (rule MST_validn_valid, clarsimp)
apply (erule VPG_MSTn)
done
(*>*)

text‹Combining these two results, and unfolding the definition of
program validity yields the final soundness result.›

theorem VP_VALID: "VP ⟹ Prog_valid"
(*<*)
apply (simp add: VP_def Prog_valid_def, clarsimp)
apply (frule VPG_MST, simp)
apply (drule VPG_MST_G, assumption) apply fast
done
(*>*)

(*<*)

text ‹In particular, the $\mathit{VP}$ property implies that all
method specifications are honoured by their respective method
implementations.›

theorem "VP ⟹ MST_valid"
(*<*)
by (drule VP_VALID, simp add: Prog_valid_def)
(*>*)

end
(*>*)