Theory VS

(*File: VS.thy*)
(*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*)
theory VS imports VDM begin
section‹Base-line noninterference›

text‹\label{sec:BaseLineNI} We now show how to interprete the type
system of Volpano, Smith and Irvine~\<^cite>‹"VolpanoSmithIrvine:JCS1996"›,
as described in Section 3 of our
paper~\<^cite>‹"BeringerHofmann:CSF2007"›.›

subsection‹Basic definitions›

text‹Muli-level security being treated in Section
\ref{sec:HuntSands}, we restrict our attention in the present section
to the two-point security lattice.›

datatype TP = low | high

text‹A global context assigns a security type to each program
variable.›

consts CONTEXT :: "Var ⇒ TP"

text‹Next, we define when two states are considered (low)
equivalent.›

definition twiddle::"State ⇒ State ⇒ bool" (‹ _ ≈ _ › [100,100] 100)
where "s ≈ ss = (∀ x. CONTEXT x = low ⟶ s x = ss x)"

text‹A command $c$ is \emph{secure} if the low equivalence of any two
initial states entails the equivalence of the corresponding final
states.›

definition secure::"IMP ⇒ bool"
where "secure c = (∀ s t ss tt . s ≈ t ⟶ (s,c ⇓ ss) ⟶ 
                          (t,c ⇓ tt) ⟶ ss ≈ tt)"

text ‹Here is the definition of the assertion transformer
that is called $\mathit{Sec}$ in the paper \ldots›

definition Sec :: "((State × State) ⇒ bool) ⇒ VDMAssn"
where "Sec Φ s t = ((∀ r . s ≈ r ⟶ Φ(t, r)) ∧ (∀ r . Φ(r ,s) ⟶ r ≈ t))"

text‹\ldots and the proofs of two directions of its characteristic
property, Proposition 1.›

lemma Prop1A:"⊨ c : (Sec Φ) ⟹ secure c"
(*<*)
by (simp add: VDM_valid_def secure_def Sec_def)
(*>*)

lemma Prop1B:
  "secure c ⟹ ⊨ c : Sec (λ (r, t) . ∃ s . (s , c ⇓ r) ∧ s ≈ t)"
(*<*)
apply (simp add: VDM_valid_def Sec_def) 
apply clarsimp
apply (unfold secure_def)
apply rule
apply (rule, rule) apply (rule_tac x=s in exI) apply(rule, assumption+)
apply (rule, rule, erule exE, erule conjE) apply fast
done
(*>*)

lemma Prop1BB:"secure c ⟹ ∃ Φ . ⊨ c : Sec Φ"
(*<*)
by (drule Prop1B, fast)
(*>*)

lemma Prop1:
"(secure c) = (⊨ c : Sec (λ (r, t) . ∃ s . (s , c ⇓ r) ∧ s ≈ t))"
(*<*)
apply rule
apply (erule Prop1B)
apply (erule Prop1A)
done
(*>*)

subsection‹Derivation of the LOW rules›

text‹We now derive the interpretation of the LOW rules of Volpano et
al's paper according to the constructions given in the paper. (The
rules themselves are given later, since they are not yet needed).›

lemma CAST[rule_format]:
  "G ⊳ c : twiddle ⟶ G ⊳ c : Sec (λ (s,t) . s ≈ t)"
(*<*)
apply clarsimp
apply (erule VDMConseq)  apply (simp add: twiddle_def Sec_def)
done
(*>*)

lemma SKIP: "G ⊳ Skip : Sec (λ (s,t) . s ≈ t)"
(*<*)
apply (rule VDMConseq, rule VDMSkip)
apply (simp add: Sec_def twiddle_def)
done
(*>*)

lemma ASSIGN: 
  "(∀ s ss. s ≈ ss ⟶ evalE e s = evalE e ss) ⟹
   G ⊳ (Assign x e) 
     : (Sec (λ (s, t) . s ≈ (update t x (evalE e t))))"
(*<*)
 apply (rule VDMConseq) apply(rule VDMAssign)
  apply clarsimp apply (simp add: Sec_def)
  apply clarsimp 
  apply (erule_tac x=s in allE, erule_tac x=r in allE, clarsimp)
  apply (simp add: twiddle_def update_def)
done
(*>*)

lemma COMP: 
  "⟦ G ⊳ c1 : (Sec Φ); G ⊳ c2 : (Sec Ψ)⟧ ⟹
     G ⊳ (Comp c1 c2) : (Sec (λ (s,t) . ∃ r . Φ(r, t) ∧ 
                           (∀ w . (r ≈ w ⟶ Ψ(s, w)))))"
(*<*)
apply (rule VDMConseq) apply (erule VDMComp) apply assumption
    apply (simp add: Sec_def, clarsimp)
    apply rule
      apply clarsimp apply (erule_tac x=ra in allE, clarsimp)
        apply (rule_tac x=r in exI, clarsimp) 
     apply clarsimp
done
(*>*)

lemma IFF:
  "⟦ (∀ s ss. s ≈ ss ⟶ evalB b s = evalB b ss);
     G ⊳ c1 : (Sec Φ); G ⊳ c2 : (Sec Ψ)⟧ ⟹
     G ⊳ (Iff b c1 c2) : Sec (λ (s, t) . (evalB b t ⟶ Φ(s,t)) ∧ 
                                        ((¬ evalB b t) ⟶ Ψ(s,t)))"
(*<*)
 apply (rule VDMConseq) apply(rule VDMIff) apply assumption+
  apply clarsimp apply (simp add: Sec_def)
  apply clarsimp 
  apply (case_tac "evalB b s")
  apply clarsimp 
  apply clarsimp 
done
(*>*)

text‹We introduce an explicit fixed point construction over the type
$TT$ of the invariants $\Phi$.›

type_synonym TT = "(State × State) ⇒ bool"

text‹We deliberately introduce a new type here since the agreement
with ‹VDMAssn› (modulo currying) is purely coincidental. In
particular, in the generalisation for objects in Section
\ref{sec:Objects} the type of invariants will differ from the
type of program logic assertions.›

definition FIX::"(TT ⇒ TT) ⇒ TT"
where "FIX φ = (λ (s,t). ∀ Φ. (∀ ss tt . φ Φ (ss,tt) ⟶ Φ (ss,tt)) 
         ⟶ Φ (s,t))" 

definition Monotone::"(TT ⇒ TT) ⇒ bool"
where "Monotone φ = (∀ Φ Ψ . (∀ s t . Φ(s,t) ⟶ Ψ(s,t)) ⟶ 
                        (∀ s t . φ Φ (s,t) ⟶ φ Ψ (s,t)))"

(*<*)
lemma Fix2: "⟦Monotone φ; φ (FIX φ) (s, t)⟧ ⟹ FIX φ (s,t)"
apply (simp add: FIX_def) apply clarsimp
apply (subgoal_tac "φ Φ (s,t)", simp)
apply (subgoal_tac "∀ r u . FIX φ (r,u) ⟶ Φ(r,u)")
prefer 2 apply (erule thin_rl) apply (simp add: FIX_def) apply clarsimp
  apply (erule_tac x=Φ in allE, simp)
apply (unfold Monotone_def)
  apply (erule_tac x="FIX φ" in allE, erule_tac x="Φ" in allE)
  apply (erule impE) apply assumption
  apply (simp add: FIX_def)
done

lemma Fix1: "⟦Monotone φ; FIX φ (s,t)⟧ ⟹ φ (FIX φ) (s,t)"
apply (simp add: FIX_def) 
apply (erule_tac x="φ(FIX φ)" in allE) 
apply (erule impE)
prefer 2 apply (simp add: FIX_def)
apply (subgoal_tac "∀ r u .φ(FIX φ) (r,u) ⟶ (FIX φ) (r,u)")
  prefer 2 apply clarsimp apply (erule Fix2) apply assumption
apply (unfold Monotone_def)
  apply (erule_tac x="φ(FIX φ)" in allE, erule_tac x="(FIX φ)" in allE, erule impE) apply assumption
apply simp
done
(*>*)

text‹For monotone invariant transformers $\varphi$, the construction indeed
yields a fixed point.›

lemma Fix_lemma:"Monotone φ ⟹ φ (FIX φ) = FIX φ"
(*<*)
apply (rule ext, rule iffI)
apply clarsimp  apply (erule Fix2) apply assumption
apply clarsimp  apply (erule Fix1) apply assumption
done
(*>*)

text‹In order to derive the while rule we define the following
transfomer.›

definition PhiWhileOp::"BExpr ⇒ TT ⇒ TT ⇒ TT"
where "PhiWhileOp b Φ =
     (λ Ψ . (λ(s, t).
             (evalB b t ⟶ (∃r. Φ (r, t) ∧ 
                                 (∀w. r ≈ w ⟶ Ψ (s, w)))) ∧ 
             (¬ evalB b t ⟶ s ≈ t)))"

text‹Since this operator is monotone, \ldots›

lemma PhiWhileOp_Monotone: "Monotone (PhiWhileOp b Φ)"
(*<*)
apply (simp add: PhiWhileOp_def Monotone_def) apply clarsimp
  apply (rule_tac x=r in exI, simp)
done
(*>*)

text‹we may define its fixed point,›

definition PhiWhile::"BExpr ⇒ TT ⇒ TT"
where "PhiWhile b Φ = FIX (PhiWhileOp b Φ)"

text‹which we can use to derive the following rule.›

lemma WHILE:  
  "⟦ (∀ s t. s ≈ t ⟶ evalB b s = evalB b t); G ⊳ c : (Sec Φ)⟧ ⟹
   G ⊳ (While b c) : (Sec (PhiWhile b Φ))"
(*<*)
apply (rule VDMConseq)
apply (rule VDMWhile) 
prefer 4 apply (subgoal_tac "∀s t. (Sec (PhiWhileOp b Φ (PhiWhile b Φ))) s t ∧ ¬ evalB b t ⟶ Sec (PhiWhile b Φ) s t") apply assumption
  apply clarsimp apply (subgoal_tac "PhiWhileOp b Φ (PhiWhile b Φ)= PhiWhile b Φ", clarsimp)
                 apply (simp add: PhiWhile_def) apply (rule Fix_lemma) apply (rule PhiWhileOp_Monotone)
apply assumption
apply clarsimp apply (simp add: Sec_def) 
  apply (rule, clarsimp) apply (simp add: PhiWhileOp_def)
  apply clarsimp apply (simp add: PhiWhileOp_def)
apply clarsimp apply (simp add: Sec_def)
  apply rule
  prefer 2 apply clarsimp
    apply (subgoal_tac "∃r. Φ (r, s) ∧ (∀w. r ≈ w ⟶ (PhiWhile b Φ) (ra, w))")
    prefer 2 apply (simp add: PhiWhileOp_def) 
    apply clarsimp apply (rotate_tac -3, erule thin_rl)
    apply (rotate_tac -1, erule_tac x=ra in allE, erule mp)
    apply (rotate_tac 1, erule_tac x=r in allE, erule impE) apply fast
    apply (subgoal_tac "PhiWhileOp b Φ (PhiWhile b Φ) = PhiWhile b Φ", clarsimp)
    apply (simp add: PhiWhile_def)
    apply (rule Fix_lemma) apply (rule PhiWhileOp_Monotone)
  apply clarsimp
    apply (simp (no_asm_simp) add: PhiWhileOp_def)
    apply (rule_tac x=r in exI, rule) apply simp
    apply clarsimp
    apply (rotate_tac 5, erule_tac x=w in allE, clarsimp)
    apply (subgoal_tac "PhiWhileOp b Φ (PhiWhile b Φ) = PhiWhile b Φ", clarsimp)
    apply (simp add: PhiWhile_def)
    apply (rule Fix_lemma) apply (rule PhiWhileOp_Monotone)
done
(*>*)

text‹The operator that given $\Phi$ returns the invariant
occurring in the conclusion of the rule is itself monotone - this is
the property required for the rule for procedure invocations.›

lemma PhiWhileMonotone: "Monotone (λ Φ . PhiWhile b Φ)"
(*<*)
apply (simp add: Monotone_def) apply clarsimp
apply (simp add: PhiWhile_def)
apply (simp add: FIX_def) apply clarsimp
apply (erule_tac x=Φ' in allE, erule mp)
apply (clarsimp) apply (erule_tac x=ss in allE, erule_tac x=tt in allE, erule mp)
apply (simp add: PhiWhileOp_def) apply clarsimp
apply (rule_tac x=r in exI, simp)
done
(*>*)

text‹We now derive an alternative while rule that employs an
inductive formulation of a variant that replaces the fixed point
construction. This version is given in the paper.›

text‹First, the inductive definition of the $\mathit{var}$ relation.›

inductive_set var::"(BExpr × TT × State × State) set"
where
varFalse: "⟦¬ evalB b t; s ≈ t⟧ ⟹ (b,Φ,s,t):var"
| varTrue:"⟦evalB b t; Φ(r,t); ∀ w . r ≈ w ⟶ (b,Φ,s,w): var⟧
           ⟹ (b,Φ,s,t):var"

text‹It is easy to prove the equivalence of $\mathit{var}$ and the
fixed point:›

(*<*)
lemma varFIX: "(b,Φ,s,t):var ⟹ PhiWhile b Φ (s,t)"
apply (erule var.induct)
apply (simp add: PhiWhile_def)
  apply (subgoal_tac "PhiWhileOp b Φ (FIX (PhiWhileOp b Φ)) (s,t)")
  apply (subgoal_tac "PhiWhileOp b Φ (FIX (PhiWhileOp b Φ)) = FIX (PhiWhileOp b Φ)", clarsimp)
  apply (rule Fix_lemma) apply (rule PhiWhileOp_Monotone)
  apply (simp add: PhiWhileOp_def)
apply (simp (no_asm_simp) add: PhiWhile_def)
apply (subgoal_tac "PhiWhileOp b Φ (FIX (PhiWhileOp b Φ)) (s,t)")
  apply (subgoal_tac "PhiWhileOp b Φ (FIX (PhiWhileOp b Φ)) = FIX (PhiWhileOp b Φ)", clarsimp)
  apply (rule Fix_lemma) apply (rule PhiWhileOp_Monotone)
  apply (simp add: PhiWhileOp_def)
  apply (rule_tac x=r in exI, simp)
  apply clarsimp
  apply (erule_tac x=w in allE, clarsimp)
  apply (simp add: PhiWhile_def)
  apply (simp add: PhiWhileOp_def)
done

lemma FIXvar: "PhiWhile b Φ (s,t) ⟹ (b,Φ,s,t):var"
apply (simp add: PhiWhile_def)
apply (subgoal_tac "PhiWhileOp b Φ (FIX (PhiWhileOp b Φ)) (s, t)")
prefer 2 
  apply (subgoal_tac "PhiWhileOp b Φ (FIX (PhiWhileOp b Φ)) = FIX (PhiWhileOp b Φ)", clarsimp)
  apply (rule Fix_lemma) apply (rule PhiWhileOp_Monotone)
apply (erule thin_rl, simp add: PhiWhileOp_def) apply clarsimp
  apply (case_tac "evalB b t")
  prefer 2 apply clarsimp apply (rule varFalse) apply assumption+
  apply clarsimp apply (rule varTrue) apply assumption apply assumption 
    apply clarsimp apply (erule_tac x=w in allE, clarsimp)
    apply (unfold FIX_def) apply clarify
    apply (erule_tac x="λ (x,y) . (b,Φ,x,y):var" in allE, erule impE) prefer 2 apply simp
    apply clarsimp
    apply (case_tac "evalB b tt")
    prefer 2 apply clarsimp apply (rule varFalse) apply assumption+
    apply clarsimp apply (rule varTrue) apply assumption+
done

lemma varFIXvar: "(PhiWhile b Φ (s,t)) = ((b,Φ,s,t):var)"
apply rule
apply (erule FIXvar)
apply (erule varFIX)
done

lemma FIXvarFIX': "(PhiWhile b Φ) = (λ (s,t) . (b,Φ,s,t):var)"
apply (rule ext, rule iffI)
apply (case_tac x, clarsimp) apply (erule FIXvar)
apply (case_tac x, clarsimp) apply (simp add: varFIXvar)
done
(*>*)

lemma FIXvarFIX: "(PhiWhile b) = (λ Φ . (λ (s,t) . (b,Φ,s,t):var))"
(*<*)
by (rule, rule FIXvarFIX')
(*>*)

text‹From this rule and the rule WHILE above, one may derive the
while rule we gave in the paper.› 

lemma WHILE_IND:
  "⟦ (∀ s t. s ≈ t ⟶ evalB b s = evalB b t); G ⊳ c : (Sec Φ)⟧ ⟹
   G ⊳ (While b c) : (Sec (λ (s,t) . (b,Φ,s,t):var))"
(*<*)
apply (rule VDMConseq)
apply (rule WHILE [of b G c Φ]) apply assumption+
apply (simp add: FIXvarFIX)
done
(*>*)

text‹Not suprisingly, the construction $\mathit{var}$ can be shown to
be monotone in $\Phi$.›
(*<*)
lemma varMonotoneAux[rule_format]:
  "(b, Φ, s, t) ∈ var ⟹ 
   (∀s t. Φ (s, t) ⟶ Ψ (s, t)) ⟶ (b, Ψ, s, t) ∈ var"
apply (erule var.induct)
apply clarsimp apply (erule varFalse, simp)
apply clarsimp apply (erule varTrue) apply fast apply simp
done
(*>*)

lemma var_Monotone: "Monotone (λ Φ . (λ (s,t) .(b,Φ,s,t):var))"
(*<*)
apply (simp add: Monotone_def)
apply clarsimp
apply (rule varMonotoneAux) apply assumption apply simp
done
(*>*)

(*<*)
lemma varMonotone_byFIX: "Monotone (λ Φ . (λ (s,t) .(b,Φ,s,t):var))"
apply (subgoal_tac "Monotone (λ Φ . PhiWhile b Φ)")
apply (simp add: FIXvarFIX)
apply (rule PhiWhileMonotone)
done  
(*>*)

text‹The call rule is formulated for an arbitrary fixed point of
a monotone transformer.›

lemma CALL: 
  "⟦ ({Sec(FIX Φ)} ∪ G) ⊳ body : Sec(Φ (FIX Φ)); Monotone Φ⟧ ⟹
   G ⊳ Call : Sec(FIX Φ)"
(*<*)
apply (rule VDMCall)
apply (subgoal_tac "Φ (FIX Φ) = FIX Φ", clarsimp)
apply (erule Fix_lemma)
done
(*>*)

subsection‹Derivation of the HIGH rules›

text‹The HIGH rules are easy.›

lemma HIGH_SKIP: "G ⊳ Skip : twiddle"
(*<*)
apply (rule VDMConseq, rule VDMSkip) 
apply (simp add: twiddle_def)
done
(*>*)

lemma HIGH_ASSIGN:
  "CONTEXT x = high ⟹ G ⊳ (Assign x e) : twiddle"
(*<*)
apply (rule VDMConseq, rule VDMAssign) 
apply (simp add: update_def twiddle_def)
done
(*>*)

lemma HIGH_COMP: 
  "⟦ G ⊳ c1 : twiddle; G ⊳ c2 : twiddle⟧ 
  ⟹ G ⊳ (Comp c1 c2): twiddle"
(*<*)
apply (rule VDMConseq, rule VDMComp) apply assumption+
apply (simp add: twiddle_def)
apply clarsimp
done
(*>*)

lemma HIGH_IFF:
  "⟦ G ⊳ c1 : twiddle; G ⊳ c2 : twiddle ⟧ 
  ⟹ G ⊳ (Iff b c1 c2) : twiddle"
(*<*)
apply (rule VDMConseq, rule VDMIff) apply assumption+
apply (simp add: twiddle_def)
done
(*>*)

lemma HIGH_WHILE:
  "⟦ G ⊳ c  : twiddle⟧ ⟹ G ⊳ (While b c)  : twiddle"
(*<*)
apply (rule VDMConseq)
  apply (rule VDMWhile) 
  apply (subgoal_tac "G ⊳ c : (λs t. evalB b s ⟶ s ≈ t)", erule thin_rl, assumption)
  apply (erule VDMConseq) apply simp
  prefer 3 apply (subgoal_tac "∀s t. s ≈ t ∧ ¬ evalB b t ⟶ s ≈ t", assumption) apply simp
  apply (simp add: twiddle_def)
  apply (simp add: twiddle_def)
done
(*>*)

lemma HIGH_CALL:
  "({twiddle} ∪ G) ⊳ body : twiddle ⟹ G ⊳ Call : twiddle"
(*<*)
by (erule VDMCall)
(*>*)

subsection‹The type system of Volpano, Smith and Irvine›

text‹We now give the type system of Volpano et al.~and then prove its
embedding into the system of derived rules. First, type systems for
expressions and boolean expressions.›

inductive_set VS_expr :: "(Expr × TP) set"
where
VS_exprVar: "CONTEXT x = t ⟹ (varE x, t) : VS_expr"
| VS_exprVal: "(valE v, low) : VS_expr"
| VS_exprOp: "⟦(e1,t) : VS_expr; (e2,t):VS_expr⟧
             ⟹ (opE f e1 e2,t) : VS_expr"
| VS_exprHigh: "(e, high) : VS_expr"

inductive_set VS_Bexpr :: "(BExpr × TP) set"
where
VS_BexprOp: "⟦(e1,t) : VS_expr; (e2,t):VS_expr⟧
             ⟹ (compB f e1 e2,t) : VS_Bexpr"
| VS_BexprHigh: "(e,high) : VS_Bexpr"

text‹Next, the core of the type system, the rules for commands.›

inductive_set VS_com :: "(TP × IMP) set"
where

VS_comSkip: "(pc,Skip) : VS_com"

| VS_comAssHigh:
  "CONTEXT x = high ⟹ (pc,Assign x e) : VS_com"

| VS_comAssLow:
  "⟦CONTEXT x = low; pc = low; (e,low):VS_expr⟧ ⟹
   (pc,Assign x e) : VS_com"

| VS_comComp:
  "⟦ (pc,c1):VS_com; (pc,c2):VS_com⟧ ⟹
   (pc,Comp c1 c2) : VS_com"

| VS_comIf:
  "⟦ (b,pc):VS_Bexpr; (pc,c1):VS_com; (pc,c2):VS_com⟧ ⟹
   (pc,Iff b c1 c2):VS_com"

| VS_comWhile:
  "⟦(b,pc):VS_Bexpr; (pc,c):VS_com⟧ ⟹ (pc,While b c):VS_com"

| VS_comSub: "(high,c) : VS_com ⟹ (low,c):VS_com"

text‹We define the interpretation of expression typings\ldots›

primrec SemExpr::"Expr ⇒ TP ⇒ bool"
where
"SemExpr e low = (∀ s ss. s ≈ ss ⟶ evalE e s = evalE e ss)" |
"SemExpr e high = True"

text‹\ldots and show the soundness of the typing rules.›

lemma ExprSound: "(e,tp):VS_expr ⟹ SemExpr e tp"
(*<*)
apply (erule VS_expr.induct)
apply (case_tac t,simp_all)
  apply (simp add: twiddle_def)
apply (case_tac t, simp_all)
done
(*>*)

text‹Likewise for the boolean expressions.›

primrec SemBExpr::"BExpr ⇒ TP ⇒ bool"
where
"SemBExpr b low = (∀ s ss. s ≈ ss ⟶ evalB b s = evalB b ss)" |
"SemBExpr b high = True"

lemma BExprSound: "(e,tp):VS_Bexpr ⟹ SemBExpr e tp"
(*<*)
apply (erule VS_Bexpr.induct, simp_all)
apply (drule ExprSound) 
apply (drule ExprSound) 
apply (case_tac t, simp_all) 
done
(*>*)

text‹The proof of the main theorem (called Theorem 2 in our paper)
proceeds by induction on $(t,c):VS\_com$.›

theorem VS_com_VDM[rule_format]:
"(t,c):VS_com ⟹ (t=high ⟶ G ⊳ c : twiddle) ∧
                  (t=low ⟶ (∃ A . G ⊳ c : Sec A))"
(*<*)
apply (erule VS_com.induct)
apply rule
  apply clarsimp
  apply (rule HIGH_SKIP)
  apply clarsimp
  apply (rule, rule SKIP)
apply rule
  apply clarsimp
  apply (erule HIGH_ASSIGN)
  apply clarsimp
  apply (subgoal_tac "∃ t. (e,t):VS_expr", clarsimp) prefer 2 apply (rule, rule VS_exprHigh)
  apply (drule ExprSound)
  apply (case_tac t)
    apply clarsimp apply (rule, erule ASSIGN) 
    apply clarsimp apply (rule_tac x="λ (s,t).  s ≈ t" in exI, rule VDMConseq) 
         apply (erule HIGH_ASSIGN) apply (simp add: Sec_def twiddle_def)
apply rule
  apply clarsimp
  apply (drule ExprSound)
    apply clarsimp apply (rule, erule ASSIGN) 
apply rule
  apply clarsimp
  apply (rule HIGH_COMP) apply (assumption, assumption)
  apply clarsimp
  apply (rule, rule COMP) apply (assumption, assumption)
apply rule
  apply clarsimp
  apply (rule HIGH_IFF) apply (assumption, assumption)
  apply clarsimp
  apply (drule BExprSound)
  apply clarsimp
  apply (rule, erule IFF)  apply (assumption, assumption)
apply rule
  apply clarsimp
  apply (erule HIGH_WHILE) 
  apply clarsimp
  apply (drule BExprSound)
  apply clarsimp
  apply (rule, erule WHILE) apply assumption
apply clarsimp
  apply (rule, erule CAST)
done
(*>*)

text‹The semantic of typing judgements for commands is now the
expected one: HIGH commands require initial and final state be low
equivalent (i.e.~the low variables in the final state can't depend on
the high variables of the initial state), while LOW commands must
respect the above mentioned security property.›

primrec SemCom::"TP ⇒ IMP ⇒ bool"
where
"SemCom low c = (∀ s ss t tt. s ≈ ss ⟶ (s,c ⇓ t) ⟶
                               (ss,c ⇓ tt) ⟶ t ≈ tt)" |
"SemCom high c = (∀ s t . (s,c ⇓ t) ⟶ s ≈ t)"

text‹Combining theorem ‹VS_com_VDM› with the soundness result
of the program logic and the definition of validity yields the
soundness of Volpano et al.'s type system.›

theorem VS_SOUND: "(t,c):VS_com ⟹ SemCom t c"
(*<*)
apply (subgoal_tac "(t=high ⟶ {} ⊳ c : twiddle) ∧ (t=low ⟶ (∃ A . {} ⊳ c : Sec A))")
prefer 2 apply (erule VS_com_VDM)
apply (case_tac t)
apply clarsimp apply (drule VDM_Sound) apply (simp add: valid_def VDM_valid_def Ctxt_valid_def Sec_def)
apply clarsimp apply (drule VDM_Sound) apply (simp add: valid_def VDM_valid_def Ctxt_valid_def) 
done
(*>*)

text‹As a further minor result, we prove that all judgements
interpreting the low rules indeed yield assertions $A$ of the form $A
= Sec(\Phi(FIX \Phi))$ for some monotone $\Phi$.›

inductive_set Deriv ::"(VDMAssn set × IMP × VDMAssn) set"
where
D_CAST: 
  "(G,c,twiddle):Deriv ⟹ (G, c, Sec (λ (s,t) . s ≈ t)) : Deriv"

| D_SKIP: "(G, Skip, Sec (λ (s,t) . s ≈ t)) : Deriv"

| D_ASSIGN:
  "(∀ s ss. s ≈ ss ⟶ evalE e s = evalE e ss) ⟹
   (G, Assign x e, Sec (λ (s, t) . s ≈ (update t x (evalE e t)))):Deriv"

| D_COMP: 
  "⟦ (G, c1, Sec Φ):Deriv; (G, c2, Sec Ψ):Deriv⟧ ⟹
   (G, Comp c1 c2, Sec (λ (s,t) . ∃ r . Φ(r, t) ∧ 
                           (∀ w . (r ≈ w ⟶ Ψ(s, w))))):Deriv"

| C_IFF:
  "⟦ (∀ s ss. s ≈ ss ⟶ evalB b s = evalB b ss);
     (G, c1, Sec Φ):Deriv; (G,c2, Sec Ψ):Deriv⟧ ⟹
   (G, Iff b c1 c2, Sec (λ (s, t) . (evalB b t ⟶ Φ(s,t)) ∧ 
                                            ((¬ evalB b t) ⟶ Ψ(s,t)))):Deriv"

| D_WHILE:  
  "⟦ (∀ s ss. s ≈ ss ⟶ evalB b s = evalB b ss); 
     (G, c, Sec Φ):Deriv⟧ ⟹
   (G, While b c, Sec (PhiWhile b Φ)):Deriv"

| D_CALL:
  "⟦ ({Sec(FIX Φ)} ∪ G, body, Sec(Φ(FIX Φ))):Deriv;
      Monotone Φ⟧ ⟹
   (G, Call, Sec(FIX Φ)):Deriv"

| D_HighSKIP:"(G, Skip, twiddle):Deriv"

| D_HighASSIGN:
  "CONTEXT x = high ⟹ (G,Assign x e, twiddle):Deriv"

| D_HighCOMP:
  "⟦ (G,c1,twiddle):Deriv; (G,c2,twiddle):Deriv⟧ ⟹
   (G, Comp c1 c2, twiddle):Deriv"

| D_HighIFF:
  "⟦ (G,c1,twiddle):Deriv; (G,c2,twiddle):Deriv⟧ ⟹
   (G, Iff b c1 c2, twiddle):Deriv"

| D_HighWHILE:
  "(G, c, twiddle):Deriv ⟹ (G, While b c, twiddle):Deriv"

| D_HighCALL:
  "({twiddle} ∪ G, body, twiddle):Deriv ⟹ (G, Call, twiddle):Deriv"

(*<*)
definition DProp :: "VDMAssn ⇒ bool"
where "DProp A = (∃ φ . A =  Sec (φ (FIX φ)) ∧ Monotone φ)"

lemma DerivProp_Aux: "(X,c,A):Deriv ⟹ DProp A"
apply (erule Deriv.induct)
apply (simp_all add: DProp_def)
  apply clarsimp
  apply (rule, rule) apply simp apply (simp add: Monotone_def)
  apply clarsimp?
  apply (rule, rule) apply simp apply (simp add: Monotone_def)
  apply clarsimp?
  apply (rule, rule) apply simp apply (simp add: Monotone_def)
  apply clarsimp?
  apply (rule, rule) apply simp apply (simp add: Monotone_def)
  apply clarsimp?
  apply (rule, rule) apply simp apply (simp add: Monotone_def)
  apply clarsimp?
  apply (rule, rule) apply simp apply (simp add: Monotone_def)
  apply clarsimp ?
  apply (rule, rule) apply simp apply (simp add: Monotone_def)
  apply clarsimp?
    apply (rule_tac x="λ Φ. λ (s,t) . s ≈ t" in exI)
    apply (subgoal_tac "Monotone (λ Φ. λ (s,t) . s ≈ t)", simp) 
      apply (drule Fix_lemma) apply (erule thin_rl)
      apply (rule ext, rule ext, rule iffI)
      apply (simp add: twiddle_def Sec_def)
      apply (simp add: Sec_def) apply (simp only: twiddle_def) apply fast
    apply (simp add: Monotone_def)
  apply clarsimp?
    apply (rule_tac x="λ Φ. λ (s,t) . s ≈ t" in exI)
    apply (subgoal_tac "Monotone (λ Φ. λ (s,t) . s ≈ t)", simp) 
      apply (drule Fix_lemma) apply (erule thin_rl)
      apply (rule ext, rule ext, rule iffI)
      apply (simp add: twiddle_def Sec_def)
      apply (simp add: Sec_def) apply (simp only: twiddle_def) apply fast
    apply (simp add: Monotone_def)
done
(*>*)

lemma DerivMono: 
 "(X,c,A):Deriv ⟹ ∃ Φ . A =  Sec (Φ (FIX Φ)) ∧ Monotone Φ"
(*<*)
by (drule DerivProp_Aux, simp add: DProp_def)
(*>*)

text‹Also, all rules in the ‹Deriv› relation are indeed
derivable in the program logic.›

lemma Deriv_derivable: "(G,c,A):Deriv ⟹ G ⊳ c: A"
(*<*)
apply (erule Deriv.induct)
apply (erule CAST)
apply (rule SKIP)
apply (erule ASSIGN)
apply (erule COMP) apply assumption
apply (erule IFF) apply assumption apply assumption
apply (erule WHILE) apply assumption 
apply (erule CALL) apply assumption
apply (rule HIGH_SKIP)
apply (erule HIGH_ASSIGN)
apply (erule HIGH_COMP) apply assumption
apply (erule HIGH_IFF) apply assumption 
apply (erule HIGH_WHILE) 
apply (erule HIGH_CALL) 
done
(*>*)
text‹End of theory VS›
end