Quelle  VDM.thy

(*File: VDM.thy*)
(*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*)
theory VDM imports IMP begin
section‹Program logic›

text‹\label{sec:VDM} The program logic is a partial correctness logic
  (precondition-less) VDM style. This means that assertions are
  predicates over states and relate the initial and final
  of a terminating execution.›

subsection ‹Assertions and their semantic validity›

text‹Assertions are binary predicates over states, i.e.~are of type›

type_synonym "VDMAssn" = "State ==> State ==> bool"

text‹Command $c$ satisfies assertion $A$ if all (terminating)
  behaviours are covered by the assertion.›

definition VDM_valid :: "IMP ==> VDMAssn ==> bool"
                       (‹ ⊨ _ : _ › [100,100] 100)
where "⊨ c : A = (∀ s t . (s,c ⇓ t) ⟶ A s t)"

text‹A variation of this property for the height-indexed operational
 ,\ldots›

definition VDM_validn :: "nat ==> IMP ==> VDMAssn ==> bool"
                        (‹ ⊨_{_} _ : _ › [100,100,100] 100)
where "⊨_n c : A = (∀ m . m ≤ n --> (∀ s t . (s,c →_m t) --> A s t))"

text‹\ldots plus the obvious relationships.›
lemma VDM_valid_validn: "⊨ c:A ==> ⊨_n c:A"
(*<*)
by (simp add: VDM_valid_def VDM_validn_def Sem_def, fastforce)
(*>*)

lemma VDM_validn_valid: "(∀ n . ⊨_n c:A) ==> ⊨ c:A"
(*<*)
by (simp add: VDM_valid_def VDM_validn_def Sem_def, fastforce)
(*>*)

lemma VDM_lowerm: "[ ⊨_n c:A; m ≤ n ] ==> ⊨_m c:A"
(*<*)
apply (simp add: VDM_validn_def, clarsimp)
apply (erule_tac x="ma" in allE, simp)
done
(*>*)

text‹Proof contexts are simply sets of assertions -- each entry
  an assumption for the unnamed procedure. In particular, a
  is valid if each entry is satisfied by the method call
 .›

definition Ctxt_valid :: "VDMAssn set ==> bool" (‹ ⊨ _ › [100] 100)
where "⊨ G = (∀ A . A ∈ G ⟶ (⊨ Call : A))"

text‹Again, a relativised sibling \ldots›

definition Ctxt_validn :: "nat ==> (VDMAssn set) ==> bool"
                         (‹ ⊨_{_} _ › [100,100] 100)
where "⊨_n G = (∀ m . m ≤ n ⟶ (∀ A. A ∈ G ⟶ ( ⊨_m Call : A)))"

text‹satisfies the obvious properties.›

lemma Ctxt_valid_validn: "⊨ G ==> ⊨_n G"
(*<*)
apply (simp add: Ctxt_valid_def Ctxt_validn_def, clarsimp)
apply (rule VDM_valid_validn) apply fast
done
(*>*)

lemma Ctxt_validn_valid: "(∀ n . ⊨_n G) ==> ⊨ G"
(*<*)
apply (simp add: Ctxt_valid_def Ctxt_validn_def, clarsimp)
apply (rule VDM_validn_valid) apply fast
done
(*>*)

lemma Ctxt_lowerm: "[ ⊨_n G; m < n ] ==> ⊨_m G"
(*<*)
by (simp add: Ctxt_validn_def)
(*>*)

text‹A judgement is valid if the validity of the context implies that
  the commmand-assertion pair.›

definition valid :: "(VDMAssn set) ==> IMP ==> VDMAssn ==> bool"
                    (‹_ ⊨ _ : _ › [100,100,100] 100)
where "G ⊨ c : A = (⊨ G ⟶ ⊨ c : A)"

text‹And, again, a relatived notion of judgement validity.›

definition validn :: 
 "(VDMAssn set) ==> nat ==> IMP ==> VDMAssn ==> bool"
  (‹_ ⊨_{_} _ : _› [100,100,100,100] 100)
where "G ⊨_n c : A = (⊨_n G ⟶ ⊨_n c : A)"

lemma validn_valid: "(∀ n . G ⊨_n c : A) ==> G ⊨ c : A"
(*<*)
apply (simp add: valid_def validn_def, clarsimp)
apply (rule VDM_validn_valid, clarsimp) 
apply (erule_tac x=n in allE, erule mp)
apply (erule Ctxt_valid_validn)
done
(*>*)

lemma ctxt_consn: "[ ⊨_n G; ⊨_n Call:A ] ==> ⊨_n ({A} ∪ G)"
(*<*)
apply (simp add: Ctxt_validn_def)  apply clarsimp 
apply (erule_tac x=m in allE, clarsimp) 
apply (erule VDM_lowerm) apply assumption
done
(*>*)

subsection‹Proof system›

inductive_set
  VDM_proof :: "(VDMAssn set × IMP × VDMAssn) set"
where

VDMSkip:   "(G, Skip, λ s t . t=s) : VDM_proof"

| VDMAssign:
  "(G, Assign x e, λ s t . t = (update s x (evalE e s))) : VDM_proof"

| VDMComp:
  "[ (G, c1, A1) : VDM_proof; (G, c2, A2) : VDM_proof] ==>
   (G, Comp c1 c2, λ s t . ∃ r . A1 s r ∧ A2 r t) : VDM_proof"

| VDMIff:
  "[ (G, c1, A):VDM_proof; (G, c2, B):VDM_proof] ==>
   (G, Iff b c1 c2, λ s t . (((evalB b s) ⟶ A s t) ∧
                                    ((¬ (evalB b s)) ⟶ B s t))) : VDM_proof"

(*VDMWhile:  "\<lbrakk>\<rhd> C : (\<lambda> s t . (evalB b s \<longrightarrow> I s t)); Trans I; Refl I\<rbrakk>
            \<Longrightarrow> \<rhd> (While b C) : (\<lambda> s t . I s t \<and> \<not> (evalB b t))"*)
| VDMWhile:
  "[ (G, c, B):VDM_proof; ∀ s . (¬ evalB b s) ⟶ A s s;
             ∀ s r t. evalB b s ⟶ B s r ⟶ A r t ⟶ A s t ] ==>
   (G, While b c, λ s t . A s t ∧ ¬ (evalB b t)) : VDM_proof"

| VDMCall:
  "({A} ∪ G, body, A):VDM_proof ==> (G, Call, A):VDM_proof"

| VDMAx: "A ∈ G ==> (G, Call, A):VDM_proof"

| VDMConseq:
  "[ (G, c, A):VDM_proof; ∀ s t. A s t ⟶ B s t] ==>
   (G, c, B):VDM_proof"
(*
VDMSkip:   "G \<rhd> Skip : (\<lambda> s t . t=s)"
VDMAssign: "G \<rhd> (Assign x e) : (\<lambda> s t . t = (update s x (evalE e s)))"
VDMComp:   "\<lbrakk> G \<rhd> c1:A1; G \<rhd> c2:A2\<rbrakk> 
           \<Longrightarrow> G \<rhd> (Comp c1 c2) : (\<lambda> s t . \<exists> r . A1 s r \<and> A2 r t)"
VDMIff:    "\<lbrakk> G \<rhd> c1 : A; G \<rhd> c2 :B\<rbrakk>
            \<Longrightarrow> G \<rhd> (Iff b c1 c2) : (\<lambda> s t . (((evalB b s) \<longrightarrow> A s t) \<and> 
                                             ((\<not> (evalB b s)) \<longrightarrow> B s t)))"
(*VDMWhile:  "\<lbrakk>\<rhd> C : (\<lambda> s t . (evalB b s \<longrightarrow> I s t)); Trans I; Refl I\<rbrakk>
            \<Longrightarrow> \<rhd> (While b C) : (\<lambda> s t . I s t \<and> \<not> (evalB b t))"*)
VDMWhile:  "[ G ⊳ c : B;
              ∀ s . (¬ evalB b s) ⟶ A s s;
              ∀ s r t. evalB b s ⟶ B s r ⟶ A r t ⟶ A s t ]
            ==> G ⊳ (While b c) : (λ s t . A s t ∧ ¬ (evalB b t))"
VDMCall: "({A} ∪ G) ⊳ body : A ==> G ⊳ Call : A"
VDMAx: "A ∈ G ==> G ⊳ Call : A"
VDMConseq: "[ G ⊳ c : A; ∀ s t. A s t ⟶ B s t] ==> G ⊳ c : B"
*)

abbreviation
  VDM_deriv :: "[VDMAssn set, IMP, VDMAssn] ==> bool"
                (‹_ ⊳ _ : _› [100,100,100] 100)
where "G ⊳ c : A == (G,c,A) ∈ VDM_proof"

text‹The while-rule is in fact inter-derivable with the following rule.›

lemma Hoare_While: 
   "G ⊳ c : (λ s s' . ∀ r . evalB b s ⟶ I s r ⟶ I s' r) ==>
    G ⊳ While b c : (λ s s'. ∀ r . I s r ⟶ (I s' r ∧ ¬ evalB b s'))"
apply (subgoal_tac "G ⊳ (While b c) :
           (λ s t . (λ s t . ∀r. I s r ⟶ I t r) s t ∧ ¬ (evalB b t))")
apply (erule VDMConseq)
apply simp
apply (rule VDMWhile) apply assumption apply simp apply simp
done

text‹Here's the proof in the opposite direction.›

lemma VDMWhile_derivable:
  "[ G ⊳ c : B; ∀ s . (¬ evalB b s) ⟶ A s s;
     ∀ s r t. evalB b s ⟶ B s r ⟶ A r t ⟶ A s t ]
  ==> G ⊳ (While b c) : (λ s t . A s t ∧ ¬ (evalB b t))"
apply (rule VDMConseq)
apply (rule Hoare_While [of G c b "λ s r . ∀ t . A s t ⟶ A r t"])
apply (erule VDMConseq) apply clarsimp
apply fast
done

subsection‹Soundness›
(*<*)
lemma MAX:"Suc (max k m) ≤ n ==> k ≤ n ∧ m ≤ n"
by (simp add: max_def, case_tac "k ≤ m", simp+)
(*>*)

(*<*)
definition SoundWhileProp::"nat ==> (VDMAssn set) ==> IMP ==> VDMAssn ==> BExpr ==> VDMAssn ==> bool"
where "SoundWhileProp n G c B b A =
   ((∀m. G ⊨_m c : B) ⟶ (∀s. (¬ evalB b s) ⟶ A s s) ⟶
    (∀s. evalB b s ⟶ (∀r. B s r ⟶ (∀t. A r t ⟶ A s t))) ⟶
   G ⊨_n (While b c) : (λs t. A s t ∧ ¬ evalB b t))"

lemma SoundWhileAux[rule_format]: "SoundWhileProp n G c B b A"
apply (induct n)
apply (simp_all add: SoundWhileProp_def)
apply clarsimp apply (simp add: validn_def VDM_validn_def, clarsimp) 
  apply (drule Sem_no_zero_height_derivs) apply simp 
apply clarsimp apply (simp add: validn_def VDM_validn_def, clarsimp)  
  apply (erule Sem_eval_cases)
  prefer 2 apply clarsimp 
  apply clarsimp 
   apply (erule_tac x=n in allE, erule impE) apply (erule Ctxt_lowerm) apply simp
   apply (rotate_tac -1)
   apply (erule_tac x=ma in allE, clarsimp) 
   apply(erule impE) apply (erule Ctxt_lowerm) apply simp 
   apply (erule_tac x=na in allE, clarsimp) apply fast
done
(*>*)

text‹An auxiliary lemma stating the soundness of the while rule. Its
  is by induction on $n$.›

lemma SoundWhile[rule_format]:
  "(∀m. G ⊨_m c : B) ⟶ (∀s. (¬ evalB b s) ⟶ A s s) ⟶
    (∀s. evalB b s ⟶ (∀r. B s r ⟶ (∀t. A r t ⟶ A s t))) ⟶
   G ⊨_n (While b c) : (λs t. A s t ∧ ¬ evalB b t)"
(*<*)
apply (subgoal_tac "SoundWhileProp n G c B b A")
  apply (simp add: SoundWhileProp_def)
apply (rule SoundWhileAux)
done 
(*>*)

text‹Similarly, an auxiliary lemma for procedure invocations. Again,
  proof proceeds by induction on $n$.›

lemma SoundCall[rule_format]:
"[∀n. ⊨_n ({A} ∪ G) ⟶ ⊨_n body : A] ==> ⊨_n G ⟶ ⊨_n Call : A"
(*<*)
apply (induct_tac n)
apply (simp add: VDM_validn_def, clarsimp) 
  apply (drule Sem_no_zero_height_derivs) apply simp 
apply clarsimp
  apply (drule Ctxt_lowerm) apply (subgoal_tac "n < Suc n", assumption) apply simp apply clarsimp
  apply (drule ctxt_consn) apply assumption
  apply (simp add: VDM_validn_def, clarsimp)
  apply (erule Sem_eval_cases, clarsimp) 
done
(*>*)

text‹The heart of the soundness proof is the following lemma which is
  by induction on the judgement $G \rhd c :A$.›

lemma VDM_Sound_n: "G ⊳ c: A ==> (∀ n . G ⊨_n c:A)"
(*<*)
apply (erule VDM_proof.induct)
apply (simp add: validn_def VDM_validn_def)
  apply(clarsimp, erule Sem_eval_cases, simp)
apply (simp add: validn_def VDM_validn_def)
  apply(clarsimp, erule Sem_eval_cases, simp)
apply (simp add: validn_def VDM_validn_def)
  apply(clarsimp, erule Sem_eval_cases, clarsimp)
  apply (drule MAX, clarsimp)
  apply (erule_tac x=n in allE, clarsimp, rotate_tac -1, erule_tac x=na in allE, clarsimp)
  apply (erule_tac x=n in allE, clarsimp, rotate_tac -1, erule_tac x=ma in allE, clarsimp)
  apply (rule_tac x=r in exI, fast)
apply (simp add: validn_def VDM_validn_def)
  apply(clarsimp, erule Sem_eval_cases, clarsimp)
   apply (erule thin_rl, rotate_tac 1, erule thin_rl, erule thin_rl)
     apply (erule_tac x=n in allE, clarsimp, erule_tac x=na in allE, clarsimp)
   apply (erule thin_rl, erule thin_rl)
     apply (erule_tac x=n in allE, clarsimp, erule_tac x=na in allE, clarsimp)
apply clarsimp
  apply (rule SoundWhile) apply fast apply simp apply simp apply clarsimp
apply (simp add: validn_def, clarsimp)
  apply (rule SoundCall) prefer 2 apply assumption apply fastforce
apply (simp add: Ctxt_validn_def validn_def) 
apply (simp add: validn_def VDM_validn_def) 
done
(*>*)

text‹Combining this result with lemma ‹validn_valid›, we obtain soundness in contexts,\ldots›

theorem VDM_Sound: "G ⊳ c: A ==> G ⊨ c:A"
(*<*)
by (drule VDM_Sound_n, erule validn_valid) 
(*>*)

text‹\ldots and consequently soundness w.r.t.~empty
 .›

lemma VDM_Sound_emptyCtxt:"{} ⊳ c : A ==> ⊨ c : A"
(*<*)
apply (drule VDM_Sound)
apply (simp add: valid_def, erule mp) 
apply (simp add: Ctxt_valid_def)
done
(*>*)

subsection‹Admissible rules›

text‹A weakening rule and some cut rules are easily derived.›

lemma WEAK[rule_format]: 
  "G ⊳ c : A ==> (∀ H . G ⊆ H ⟶ H ⊳ c :A)"
(*<*)
apply (erule VDM_proof.induct)
apply clarsimp apply (rule VDMSkip)
apply clarsimp apply (rule VDMAssign)
apply clarsimp apply (rule VDMComp) apply (erule_tac x=H in allE, simp) apply (erule_tac x=H in allE, simp) 
apply clarsimp apply (rule VDMIff)  apply (erule_tac x=H in allE, simp) apply (erule_tac x=H in allE, simp)  
apply clarsimp apply (rule VDMWhile) apply (erule_tac x=H in allE, simp)  apply (assumption) apply simp
apply clarsimp apply (rule VDMCall) apply (erule_tac x="({A} ∪ H)" in allE, simp) apply fast
apply clarsimp apply (rule VDMAx) apply fast
apply clarsimp apply (rule VDMConseq) apply (erule_tac x=H in allE, clarsimp) apply assumption apply assumption
done
(*>*)

(*<*)
definition CutAuxProp::"VDMAssn set ==> IMP ==> VDMAssn ==> bool"
where "CutAuxProp H c A =
  (∀ G P D . (H = (insert P D) ⟶ G ⊳ Call :P ⟶ (G ⊆ D) ⟶ D ⊳ c:A))"

lemma CutAux1:"(H ⊳ c : A) ==> CutAuxProp H c A"
apply (erule VDM_proof.induct)
apply (simp_all add: add: CutAuxProp_def)
apply clarify
apply (fast intro: VDMSkip)
apply (fast intro: VDMAssign)
apply clarsimp 
  apply (erule_tac x=Ga in allE) apply (erule_tac x=Ga in allE)
  apply (erule_tac x=P in allE) apply (erule_tac x=P in allE)
  apply (erule_tac x=D in allE, simp) apply (erule_tac x=D in allE, simp)
  apply (rule VDMComp) apply assumption+
apply clarsimp 
  apply (erule_tac x=Ga in allE) apply (erule_tac x=Ga in allE)
  apply (erule_tac x=P in allE) apply (erule_tac x=P in allE)
  apply (erule_tac x=D in allE, simp) apply (erule_tac x=D in allE, simp)
  apply (rule VDMIff) apply assumption+
apply clarsimp 
  apply (erule_tac x=Ga in allE) 
  apply (erule_tac x=P in allE) 
  apply (erule_tac x=D in allE, simp) 
  apply (rule VDMWhile) apply assumption+
  apply simp
apply clarsimp 
  apply (erule_tac x=Ga in allE) 
  apply (erule_tac x=P in allE) 
  apply (erule_tac x="insert A D" in allE, simp) 
  apply (rule VDMCall) apply fastforce
apply clarsimp
  apply (erule disjE)
  apply clarsimp apply (erule WEAK) apply assumption
  apply (erule VDMAx)
apply clarsimp
apply (subgoal_tac "D ⊳ c : A") 
apply (erule VDMConseq) apply assumption  
  apply simp
done
(*>*)

lemma CutAux: 
  "[H ⊳ c : A; H = insert P D; G ⊳ Call :P; G ⊆ D] ==> D ⊳ c:A"
(*<*)
by (drule CutAux1, simp add: CutAuxProp_def)
(*>*)

lemma Cut:"[ G ⊳ Call : P ; (insert P G) ⊳ c : A ] ==> G ⊳ c : A"
(*<*)
apply (rotate_tac -1, drule CutAux)
apply (fastforce, assumption)
apply (simp, assumption)
done
(*>*)

text‹We call context $G$ verified if all entries are justified by
  for the procedure body.›

definition verified::"VDMAssn set ==> bool"
where "verified G = (∀ A . A:G ⟶ G ⊳ body : A)"

text‹The property is preserved by sub-contexts›

lemma verified_preserved: "[verified G; A:G] ==> verified (G - {A})"
(*<*)
apply (simp add: verified_def, (rule allI)+, rule)
apply (subgoal_tac "(G - {A}) ⊳ Call:A")
(*now use the subgoal (G - {A}) \<rhd> Call:A to prove the goal*)
apply (subgoal_tac "G = insert A (G - {A})") prefer 2 apply fast
apply (erule_tac x=Aa in allE) 
apply (erule impE, simp)
apply (erule Cut)  apply simp
(* now prove the subgoal (G - {A}) \<rhd>  Call : A *)
  apply (erule_tac x=A in allE, clarsimp)
  apply (rule VDMCall) apply simp apply (erule WEAK) apply fast
done
(*>*)

(*<*)
lemma SetNonSingleton:
  "[G ≠ {A}; A ∈ G] ==> ∃B. B ≠ A ∧ B ∈ G"
by auto

lemma MutrecAux[rule_format]: 
"∀ G . ((finite G ∧ card G = n ∧ verified G ∧ A : G) ⟶ {} ⊳ Call:A)"
apply (induct n)
(*case n=0*)
apply clarsimp
(*Case n>0*)
apply clarsimp
apply (case_tac "G = {A}")
apply clarsimp
apply (erule_tac x="{A}" in allE)
apply (clarsimp, simp add:verified_def)
apply (rule VDMCall, clarsimp)
(*Case G has more entries than A*)
apply (drule SetNonSingleton, assumption) 
(* use the fact that there is another entry B:G*)
apply clarsimp
apply (subgoal_tac "(G - {B}) ⊳ Call : B")
apply (erule_tac x="G - {B}" in allE)
apply (erule impE) apply (simp add: verified_preserved)
apply (erule impE) apply (simp add: card_Diff_singleton)
apply simp
(*the proof for (G - {B}) \<rhd>  Call : B *)
apply (simp add: verified_def)
apply (rotate_tac 3) apply (erule_tac x=B in allE, simp)
apply (rule VDMCall) apply simp apply (erule WEAK) apply fast
done
(*>*)

text‹The ‹Mutrec› rule allows us to eliminate verified (finite)
 . Its proof proceeds by induction on $n$.›

theorem Mutrec:
"[ finite G; card G = n; verified G; A : G ] ==> {} ⊳ Call:A"
(*<*) 
by (rule MutrecAux, fast)
(*>*)

text‹In particular, ‹Mutrec› may be used to show that verified
  contexts are valid.›

lemma Ctxt_verified_valid: "[verified G; finite G] ==> ⊨ G"
(*<*)
apply (subgoal_tac "(∀ A . A:G ⟶ G ⊳ body : A)")
prefer 2 apply (simp add: verified_def)
apply (simp add: Ctxt_valid_def, clarsimp)
apply (erule_tac x=A in allE, simp)
apply (rule VDM_Sound_emptyCtxt)
apply (subgoal_tac "card G = card G")
apply (rule Mutrec, assumption)  apply assumption+ apply simp
(*  apply (simp add: card_def)*)
done
(*>*)

subsection‹Completeness›

text‹Strongest specifications, given precisely by the operational
 .›

definition SSpec::"IMP ==> VDMAssn"
where "SSpec c s t = s,c ⇓ t"

text‹Strongest specifications are valid \ldots›
lemma SSpec_valid: "⊨ c : (SSpec c)"
(*<*)by (simp add: VDM_valid_def SSpec_def)(*>*)

text‹and imply any other valid assertion for the same program (hence
  name).›

lemma SSpec_strong: "⊨ c :A ==> ∀ s t . SSpec c s t ⟶ A s t"
(*<*)by (simp add: VDM_valid_def SSpec_def)(*>*)

text‹By induction on $c$ we show the following.›

lemma SSpec_derivable:"G ⊳ Call : SSpec Call ==> G ⊳ c : SSpec c"
(*<*)
apply (induct c)
  apply (rule VDMConseq)
  apply (rule VDMSkip) apply (simp add: SSpec_def Sem_def, rule, rule) apply (rule SemSkip)
  apply (rule VDMConseq)
  apply (rule VDMAssign) apply (simp add: SSpec_def Sem_def, rule, rule) apply (rule SemAssign) apply simp
apply clarsimp
  apply (rule VDMConseq)
  apply (rule VDMComp) apply assumption+ apply (simp add: SSpec_def Sem_def, clarsimp) 
  apply rule apply (rule SemComp) apply assumption+ apply simp
apply clarsimp
apply (rename_tac BExpr c)
apply (rule VDMConseq)
  apply (erule VDMWhile) 
    prefer 3 apply (subgoal_tac "∀s t. SSpec (While BExpr c) s t ∧ ¬ evalB BExpr t ⟶ SSpec (While BExpr c) s t", assumption)
    apply simp
    apply (simp add: SSpec_def Sem_def, clarsimp) apply (rule, erule SemWhileF) apply simp
    apply (simp add: SSpec_def Sem_def, clarsimp) apply (rule, erule SemWhileT) apply assumption+ apply simp
apply clarsimp
apply (rule VDMConseq)
  apply (rule VDMIff) apply assumption+ apply (simp add: SSpec_def Sem_def, clarsimp)
  apply (erule thin_rl, erule thin_rl)
  apply (rename_tac BExpr c1 c2 s t)
  apply (case_tac "evalB BExpr s")
  apply clarsimp apply (rule, rule SemTrue) apply assumption+ 
  apply clarsimp apply (rule, rule SemFalse) apply (assumption, assumption)
apply assumption 
done
(*>*)

text‹The (singleton) strong context contains the strongest
  of the procedure.›

definition StrongG :: "VDMAssn set"
where "StrongG = {SSpec Call}"

text‹By construction, the strongest specification of the procedure's
  can be verified with respect to this context.›

lemma StrongG_Body: "StrongG ⊳ body : SSpec Call"
(*<*)
apply (subgoal_tac "StrongG ⊳ body : SSpec body")
  apply (erule VDMConseq) apply (simp add: SSpec_def Sem_def, clarsimp)
  apply (rule, erule SemCall)
apply (rule SSpec_derivable) apply (rule VDMAx) apply (simp add: StrongG_def)
done
(*>*)

text‹Thus, the strong context is verified.›

lemma StrongG_verified: "verified StrongG"
(*<*)
apply (simp add: verified_def)
apply (rule allI)+
apply rule
apply (subgoal_tac "StrongG ⊳ body : SSpec Call")
apply (simp add: StrongG_def)
apply (rule StrongG_Body)
done
(*>*)

text‹Using this result and the rules ‹Cut› and ‹Mutrec›, we
  that arbitrary commands satisfy their strongest specification
  respect to the empty context.›

lemma SSpec_derivable_empty:"{} ⊳ c : SSpec c"
(*<*)
apply (rule Cut)
apply (rule Mutrec) apply (subgoal_tac "finite StrongG", assumption)
  apply (simp add: StrongG_def)
  apply (simp add: StrongG_def)
  apply (rule StrongG_verified)
  apply (simp add: StrongG_def)
  apply (rule SSpec_derivable) apply (rule VDMAx) apply simp
done
(*>*)

text‹From this, we easily obtain (relative) completeness.›

theorem VDM_Complete: "⊨ c : A ==> {} ⊳ c : A"
(*<*)
apply (rule VDMConseq)
apply (rule SSpec_derivable_empty)
apply (erule SSpec_strong)
done
(*>*)

text‹Finally, it is easy to show that valid contexts are verified.›

lemma Ctxt_valid_verified: "⊨ G ==> verified G"
(*<*)
apply (simp add: Ctxt_valid_def verified_def, clarsimp)
apply (erule_tac x=A in allE, simp)
apply (subgoal_tac "⊨ body : A")
apply (rotate_tac 1, erule thin_rl, drule VDM_Complete) apply (erule WEAK) apply fast
apply (simp add: VDM_valid_def Sem_def, clarsimp)
apply (erule_tac x=s in allE, erule_tac x=t in allE, erule mp)
apply (rule, erule SemCall)
done
(*>*)
text‹End of theory VDM›
end