Quelle  VS.thy

(*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
  of Volpano, Smith and Irvine~cite‹"VolpanoSmithIrvine:JCS1996"›,
  described in Section 3 of our
 ~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
  the two-point security lattice.›

datatype TP = low | high

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

consts CONTEXT :: "Var ==> TP"

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

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
  states entails the equivalence of the corresponding final
 .›

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
  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
 , 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
 's paper according to the constructions given in the paper. (The
  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
  ‹VDMAssn› (modulo currying) is purely coincidental. In
 , in the generalisation for objects in Section
 ref{sec:Objects} the type of invariants will differ from the
  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
  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
 .›

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
  in the conclusion of the rule is itself monotone - this is
  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
  formulation of a variant that replaces the fixed point
 . 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
  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
  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
  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
  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
  into the system of derived rules. First, type systems for
  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)
  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
  one: HIGH commands require initial and final state be low
  (i.e.~the low variables in the final state can't depend on
  high variables of the initial state), while LOW commands must
  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
  the program logic and the definition of validity yields the
  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
  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
  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