Theory VDM_OBJ

(*File: VDM_OBJ.thy*)
(*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*)
theory VDM_OBJ imports OBJ begin

subsection‹Program logic› 

text‹\label{sec:ObjLogic}Apart from the addition of proof rules for the three new
instructions, this section is essentially identical to Section
\ref{sec:VDM}.›

subsubsection ‹Assertions and their semantic validity›

text‹Assertions are binary state predicates, as before.›

type_synonym "Assn" = "State ⇒ State ⇒ bool"

definition VDM_validn :: "nat ⇒ OBJ ⇒ Assn ⇒ bool" 
                         (‹ ⊨⇩_ _ : _ › 50)
where "(⊨⇩n c : A) = (∀ m . m ≤ n ⟶ (∀ s t . (s,c →⇩m t) ⟶ A s t))"

definition VDM_valid :: "OBJ ⇒ Assn ⇒ bool"
                         (‹ ⊨ _ : _ › 50)
where "(⊨ c : A) = (∀ s t . (s,c ⇓ t) ⟶ A s t)"

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
(*>*)

definition Ctxt_validn :: "nat ⇒ (Assn set) ⇒ bool"
                       (‹ ⊨⇩_ _  › 50)
where "(⊨⇩n G) = (∀ m . m ≤ n ⟶ (∀ A. A ∈ G ⟶ ⊨⇩n Call : A))"

definition Ctxt_valid :: "Assn set ⇒ bool" (‹ ⊨ _ › 50)
where "(⊨ G) = (∀ A . A ∈ G ⟶ ⊨ Call : A)"

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"
(*<*)
apply (simp add: Ctxt_validn_def, clarsimp)
apply (rule VDM_lowerm) prefer 2 apply assumption apply fast
done
(*>*)

definition valid :: "(Assn set) ⇒ OBJ ⇒ Assn ⇒ bool"
                      (‹_ ⊨ _ : _ › 50)
where "(G ⊨ c : A) = (Ctxt_valid G ⟶ VDM_valid c A)"

definition validn :: "(Assn set) ⇒ nat ⇒ OBJ ⇒ Assn ⇒ bool"
                     (‹_ ⊨⇩_ _ : _› 50)
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"
(*<*)
by (simp add: Ctxt_validn_def) 
(*>*)

subsubsection‹Proof system›

inductive_set VDM_proof :: "(Assn set × OBJ × Assn) set"
where
VDMSkip: "(G, Skip, λ s t . t=s):VDM_proof"

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

| VDMNew:
  "(G, New x C,
       λ s t . ∃ l . l ∉ Dom (snd s) ∧ 
                         t = (update (fst s) x (RVal (Loc l)),
                              (l,(C,[])) # (snd s))):VDM_proof"

| VDMGet:
  "(G, Get x y F,
       λ s t . ∃ l C Flds v. (fst s) y = RVal(Loc l) ∧ 
                         lookup (snd s) l = Some(C,Flds) ∧ 
                         lookup Flds F = Some v ∧ 
                         t = (update (fst s) x v, snd s)):VDM_proof"

| VDMPut:
  "(G, Put x F e,
       λ s t . ∃ l C Flds. (fst s) x = RVal(Loc l) ∧
                         lookup (snd s) l = Some(C,Flds) ∧ 
                         t = (fst s, 
                              (l,(C,(F,evalE e (fst s)) # Flds))
                                           # (snd s))):VDM_proof"

| VDMComp:
  "⟦ (G, c, A):VDM_proof; (G, d, B):VDM_proof⟧ ⟹
  (G, Comp c d, λ s t . ∃ r . A s r ∧ B r t):VDM_proof"

| VDMIff:
  "⟦ (G, c, A):VDM_proof; (G, d, B):VDM_proof⟧ ⟹ 
  (G, Iff b c d,
     λ s t . (((evalB b (fst s)) ⟶ A s t) ∧ 
                      ((¬ (evalB b (fst 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 (fst s)) ⟶ A s s;
        ∀ s r t. evalB b (fst s) ⟶ B s r ⟶ A r t ⟶ A s t ⟧
 ⟹ (G, While b c, λ s t . A s t ∧ ¬ (evalB b (fst 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"

abbreviation VDM_deriv :: "[Assn set, OBJ, Assn] ⇒ bool" 
                   (‹_ ⊳ _ : _› [100,100] 50)
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 t . ∀ r . evalB b (fst s) ⟶ I s r ⟶ I t r) ⟹
  G ⊳ While b c : (λ s t. ∀ r . I s r ⟶ (I t r ∧ ¬ evalB b (fst t)))"
apply (subgoal_tac "G ⊳ (While b c) : 
           (λ s t . (λ s t . ∀r. I s r ⟶ I t r) s t ∧ ¬ (evalB b (fst 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 (fst s)) ⟶ A s s;
     ∀ s r t. evalB b (fst s) ⟶ B s r ⟶ A r t ⟶ A s t ⟧
  ⟹ G ⊳ (While b c) : (λ s t . A s t ∧ ¬ (evalB b (fst 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

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

text‹The following auxiliary lemma for loops is proven by induction
on $n$.›

lemma SoundWhile[rule_format]:
 "(∀n. G ⊨⇩n c : B) 
    ⟶ (∀s. (¬ evalB b (fst s)) ⟶ A s s)
    ⟶ (∀s. evalB b (fst s)
              ⟶ (∀r. B s r ⟶ (∀t. A r t ⟶ A s t)))
    ⟶ G ⊨⇩n (While b c) : (λs t. A s t ∧ ¬ evalB b (fst t))"
(*<*)
apply (induct n)
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 
(*>*)

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
(*>*)

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, 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, 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=ab in exI, rule_tac x=bb 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 (case_tac s, clarsimp)
    apply (case_tac s, 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 fast
apply (simp add: validn_def VDM_validn_def) 
done
(*>*)

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

text‹A simple corollary is soundness w.r.t.~an empty context.›

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
(*>*)

subsubsection‹Derived rules›

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 VDMNew)
apply (rule, rule) apply (rule VDMGet) 
apply (rule, rule) apply (rule VDMPut)
apply (rule, rule) apply (rule VDMComp) apply (erule_tac x=H in allE, simp) apply (erule_tac x=H in allE, simp) 
apply (rule,rule) apply (rule VDMIff)  apply (erule_tac x=H in allE, simp) apply (erule_tac x=H in allE, simp)  
apply (rule,rule) apply (rule VDMWhile) apply (erule_tac x=H in allE, simp)  apply (assumption) apply simp
apply (rule,rule) apply (rule VDMCall) apply (erule_tac x="({A} ∪ H)" in allE, simp) apply fast
apply (rule,rule) apply (rule VDMAx) apply fast
apply (rule,rule) apply (rule VDMConseq) apply (erule_tac x=H in allE, clarsimp) apply assumption apply assumption
done
(*>*)

lemma CutAux: 
 "(H ⊳ c : A) ⟹
  (∀ G P D . (H = (insert P D) ⟶ G ⊳ Call :P ⟶ (G ⊆ D) 
             ⟶ D ⊳ c:A))"
(*<*)
apply (erule VDM_proof.induct)
apply clarify
apply (fast intro: VDMSkip)
apply (fast intro: VDMAssign)
apply (rule, rule, rule)
  apply (rule, rule, rule)
  apply (rule VDMNew) 
apply (rule, rule, rule)
  apply (rule, rule, rule)
  apply (rule VDMGet) 
apply (rule, rule, rule)
  apply (rule, rule, rule)
  apply (rule VDMPut)
apply (rule, rule, rule)
  apply (rule, rule, rule)
  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, erule impE, assumption) 
  apply (erule_tac x=D in allE, erule impE, assumption)
  apply (rule VDMComp) apply simp apply simp 
apply (rule, rule, rule)
  apply (rule, rule, rule)
  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, erule impE, assumption) 
  apply (erule_tac x=D in allE, erule impE, assumption)
  apply (rule VDMIff) apply simp apply simp 
apply (rule, rule, rule)
  apply (rule, rule, rule)
  apply (erule_tac x=Ga in allE) 
  apply (erule_tac x=P in allE) 
  apply (erule_tac x=D in allE, erule impE, assumption) 
  apply (rule VDMWhile) apply simp apply simp
  apply simp
apply (rule, rule, rule)
  apply (rule, rule, rule)
  apply (erule_tac x=Ga in allE) 
  apply (erule_tac x=P in allE) 
  apply (erule_tac x="insert A D" in allE, erule impE, 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 simp
  apply simp
done
(*>*)

lemma Cut:"⟦ G ⊳ Call : P ; (insert P G) ⊳ c : A ⟧ ⟹ G ⊳ c : A"
(*<*)by (drule CutAux , simp)(*>*)

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

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
(*>*)

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

subsubsection‹Completeness›
definition SSpec::"OBJ ⇒ Assn"
where "SSpec c s t = (s,c ⇓ t)"

lemma SSpec_valid: "⊨ c : (SSpec c)"
(*<*)by (simp add: VDM_valid_def SSpec_def)(*>*)

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

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, rule) apply (rule SemSkip) apply simp
  apply (rule VDMConseq)
  apply (rule VDMAssign) apply (simp add: SSpec_def Sem_def, rule, rule, rule) apply (rule SemAssign) apply simp
  apply (rule VDMConseq)
  apply (rule VDMNew) apply (simp only: SSpec_def Sem_def, rule, rule, rule, rule)
    apply (erule exE, erule conjE)
    apply (rule SemNew) apply assumption apply assumption
  apply (rule VDMConseq)
  apply (rule VDMGet) apply (simp only: SSpec_def Sem_def, rule, rule, rule, rule)
    apply (erule exE)+
    apply (erule conjE)+
    apply (rule SemGet) apply assumption apply assumption apply assumption apply assumption
  apply (rule VDMConseq)
  apply (rule VDMPut) apply (simp only: SSpec_def Sem_def, rule, rule, rule, rule)
    apply (erule exE)+
    apply (erule conjE)+
    apply (rule SemPut) apply assumption apply assumption apply assumption
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 (rule VDMConseq)
  apply (erule VDMWhile) 
    prefer 3
    apply (rename_tac BExpr c)
    apply (subgoal_tac "∀s t. SSpec (While BExpr c) s t ∧ ¬ evalB BExpr (fst t) ⟶ SSpec (While BExpr c) s t", assumption)
    apply simp
    apply (simp only: SSpec_def Sem_def) apply (rule, rule, rule) apply (erule SemWhileF) apply simp
    apply (simp only: SSpec_def Sem_def) apply (rule, rule, rule) 
      apply (rule, rule, rule) apply (erule exE)+ apply (rule, erule SemWhileT) apply assumption+ apply simp
apply clarsimp
apply (rule VDMConseq)
  apply (rule VDMIff) apply assumption+ apply (simp only: SSpec_def Sem_def)
  apply (erule thin_rl, erule thin_rl) 
  apply (rule, rule, rule)
  apply (erule conjE)
  apply (rename_tac BExpr c1 c2 s t)
  apply (case_tac "evalB BExpr (fst s)")
  apply (erule impE, assumption) apply (erule exE) apply (rule, rule SemTrue) apply assumption+ 
  apply (rotate_tac 2, erule impE, assumption) apply (erule exE) apply (rule, rule SemFalse) apply assumption+ 
done
(*>*)

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

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
(*>*)

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
(*>*)

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
(*>*)

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

(*<*)

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 only: VDM_valid_def Sem_def)
apply (rule, rule, rule)
apply (erule exE)
apply (erule_tac x=s in allE, erule_tac x=t in allE, erule mp)
apply (rule, erule SemCall)
done
(*>*)

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 (rule Mutrec, assumption) 
  apply (insert card_def) apply fast
  apply assumption 
  apply assumption 
done
(*>*)

text‹End of theory VDM_Obj›
end