Theory VDM

(*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
in (precondition-less) VDM style. This means that assertions are
binary predicates over states and relate the initial and final
states 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)
operational 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
semantics,\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
represents an assumption for the unnamed procedure. In particular, a
context is valid if each entry is satisfied by the method call
instruction.›

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
of 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:  "⟦⊳ C : (λ s t . (evalB b s ⟶ I s t)); Trans I; Refl I⟧
            ⟹ ⊳ (While b C) : (λ s t . I s t ∧ ¬ (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 ⊳ Skip : (λ s t . t=s)"
VDMAssign: "G ⊳ (Assign x e) : (λ s t . t = (update s x (evalE e s)))"
VDMComp:   "⟦ G ⊳ c1:A1; G ⊳ c2:A2⟧ 
           ⟹ G ⊳ (Comp c1 c2) : (λ s t . ∃ r . A1 s r ∧ A2 r t)"
VDMIff:    "⟦ G ⊳ c1 : A; G ⊳ c2 :B⟧
            ⟹ G ⊳ (Iff b c1 c2) : (λ s t . (((evalB b s) ⟶ A s t) ∧ 
                                             ((¬ (evalB b s)) ⟶ B s t)))"
(*VDMWhile:  "⟦⊳ C : (λ s t . (evalB b s ⟶ I s t)); Trans I; Refl I⟧
            ⟹ ⊳ (While b C) : (λ s t . I s t ∧ ¬ (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
proof 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,
the 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
proven 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
contexts.›

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
derivations 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}) ⊳ 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}) ⊳  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}) ⊳  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)
contexts. 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
finite 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
behaviour.›

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
their 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
specification of the procedure.›

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

text‹By construction, the strongest specification of the procedure's
body 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
show that arbitrary commands satisfy their strongest specification
with 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