Quelle  HuntSands.thy

(*File: HuntSands.thy*)
(*Authors: Lennart Beringer and Martin Hofmann, LMU Munich 2008*)
theory HuntSands imports VDM Lattice begin
section‹Flow-sensitivity a la Hunt and Sands›

text‹\label{sec:HuntSands}\footnote{As the Isabelle theory representing this section is
  only on VDM.thy and Lattice.thy, name conflicts with
  defined in Section \ref{sec:BaseLineNI} are avoided.} The
  cite‹"HuntSands:POPL2006"› by Hunt and Sands presents a
  of the type system of Volpano et al.~to
 -sensitivity. Thus, programs such as $l:=h; l:=5$ are not rejected
  longer by the type system. Following the description in Section 4
  our paper~cite‹"BeringerHofmann:CSF2007"›, we embed Hunt and Sands'
  system into the program logic given in Section \ref{sec:VDM}.›

subsection‹General $A; R \Rightarrow S$-security›
text‹\label{sec:ARSsecurity}Again, we define the type $TT$ of
  formulae $\Phi$, and an assertion operator
 \mathit{Sec}$. The latter is now parametrised not only by the
  formulae but also by the (possibly differing) pre- and
 -relations $R$ and $S$ (both instantiated to $\approx$ in Section
 ref{sec:BaseLineNI}), and by a specification $A$ that directly links
 - and post-states.›

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

definition RSsecure::"(State ==> State ==> bool) ==>
                      (State ==> State ==> bool) ==> IMP ==> bool"
where "RSsecure R S c = (∀ s t ss tt . R s t ⟶ (s,c ⇓ ss) ⟶
                          (t,c ⇓ tt) ⟶ S ss tt)"

definition ARSsecure::"VDMAssn ==> (State ==> State ==> bool) ==>
                      (State ==> State ==> bool) ==> IMP ==> bool"
where "ARSsecure A R S c = ((⊨ c : A) ∧ RSsecure R S c)"

text‹Definition 3 of our paper follows.›

definition Sec :: "VDMAssn ==> (State ==> State ==> bool) ==>
                  (State ==> State ==> bool) ==> TT ==> VDMAssn"
where "Sec A R S Φ s t = (A s t ∧
                   (∀ r . R s r ⟶ Φ(t,r)) ∧ (∀ r . Φ(r,s) ⟶ S r t))"

text‹With these definitions, we can prove Proposition 4 of our
 .›

lemma Prop4A: "⊨ c : Sec A R S Φ ==> ARSsecure A R S c"
(*<*)
by (simp add:  VDM_valid_def Sec_def ARSsecure_def RSsecure_def)
(*>*)

lemma Prop4B : "ARSsecure A R S c ==>
   ⊨ c : Sec A R S (λ (r,t) . ∃ s . (s , c ⇓ r) ∧ R s t)"
(*<*)
apply (simp add: VDM_valid_def Sec_def) 
apply clarsimp
apply (unfold ARSsecure_def RSsecure_def VDM_valid_def)
apply rule apply fastforce
apply rule
apply (rule, rule) apply (rule_tac x=s in exI, rule, assumption+) 
apply (rule, rule, erule exE, erule conjE) apply fast
done
(*>*)

subsection‹Basic definitions›

text‹Contexts map program variables to lattice elements.›

type_synonym "CONTEXT" = "Var ==> L"

definition upd ::"CONTEXT ==> Var ==> L ==> CONTEXT"
where "upd G x p = (λ y . if x=y then p else G y)"

text‹We also define the predicate $\mathit{EQ}$
 (in our paper denoted by the symbol $\ltimes$)
  expresses when two states agree on all
  whose entry in a given context is below a certain security
 .›

definition EQ:: "CONTEXT ==> L ==> State ==> State ==> bool"
where "EQ G p = (λ s t . ∀ x . LEQ (G x) p ⟶ s x = t x)"

lemma EQ_LEQ: "[EQ G p s t; LEQ pp p] ==> EQ G pp s t"
(*<*)
apply (simp add: EQ_def, clarsimp)
apply (erule_tac x=x in allE, erule mp)
apply (erule LAT2, assumption)
done 
(*>*)

text‹The assertion called $\mathcal{Q}$ in our paper:›

definition Q::"L ==> CONTEXT ==> VDMAssn"
where "Q p H = (λ s t . ∀ x . (¬ LEQ p (H x)) ⟶ t x = s x)"

text‹$Q$ expresses the preservation of values in a single execution,
  corresponds to the first clause of Definition 3.2 in
 cite‹"HuntSands:POPL2006"›. In accordance with this, the following
  of security instantiates the $A$ position of $A; R
 Rightarrow S$-security with $Q$, while the context-dependent binary
  relations are plugged in as the $R$ and $S$ components.›

definition secure :: "L ==> CONTEXT ==> IMP ==> CONTEXT ==> bool"
where "secure p G c H = (∀ q . ARSsecure (Q p H) (EQ G q) (EQ H q) c)"

text‹Indeed, one may show that this notion of security amounds to the
  of a unary (i.e.~one-execution-)property and a binary
 i.e.~two-execution-) property, as expressed in Hunt \& Sands'
  3.2.›

definition secure1 :: "L ==> CONTEXT ==> IMP ==> CONTEXT ==> bool"
where "secure1 p G c H = (∀ s t . (s,c ⇓ t) ⟶ Q p H s t)"

definition secure2 :: "L ==> CONTEXT ==> IMP ==> CONTEXT ==> bool"
where "secure2 p G c H = ((∀ s t ss tt . (s,c ⇓ t) ⟶ (ss,c ⇓ tt) ⟶
                                    EQ G p s ss ⟶ EQ H p t tt))"

lemma secureEQUIV: 
  "secure p G c H = (∀ q . secure1 p G c H ∧ secure2 q G c H)"
(*<*)by (simp add: secure1_def secure2_def secure_def ARSsecure_def
              RSsecure_def Q_def VDM_valid_def, auto)
(*>*)

subsection‹Type system›

text‹The type system of Hunt and Sands -- our language formalisation
  a concrete datatype of expressions, so we add the obvious typing
  for expressions and prove the expected evaluation lemmas.›

inductive_set HS_E:: "(CONTEXT × Expr × L) set"
where 
HS_E_var: "(G, varE x, G x) : HS_E"
| HS_E_val: "(G, valE c, bottom) : HS_E"
| HS_E_op: "[(G, e1,p1):HS_E; (G, e2,p2):HS_E; p= LUB p1 p2]
           ==> (G,opE f e1 e2,p) : HS_E"
| HS_E_sup: "[(G,e,p):HS_E; LEQ p q] ==> (G,e,q):HS_E"

lemma HS_E_eval[rule_format]:
"(G, e, t) ∈ HS_E ==>
 ∀ r s q. EQ G q r s ⟶ LEQ t q ⟶ evalE e r = evalE e s"
(*<*)
apply (erule HS_E.induct)
apply clarsimp  apply (simp add: EQ_def)
apply clarsimp
apply clarsimp
  apply (erule_tac x=r in allE, erule_tac x=r in allE)
  apply (erule_tac x=s in allE, erule_tac x=s in allE)
  apply (erule_tac x=q in allE, erule_tac x=q in allE, clarsimp)
  apply (erule impE) apply (rule LAT2) prefer 2 apply assumption
    apply (simp add: LAT3)
  apply (erule impE) apply (rule LAT2) prefer 2 apply assumption
    apply (subgoal_tac "LEQ p2 (LUB p2 p1)")
      apply (simp add: LAT4)
    apply (simp add: LAT3)
  apply clarsimp
apply clarsimp
  apply (erule_tac x=r in allE, erule_tac x=s in allE, erule_tac x=qa in allE, erule impE)
    apply clarsimp
  apply (erule mp) apply (erule LAT2, assumption)
done
(*>*)

text‹Likewise for boolean expressions:›

inductive_set HS_B:: "(CONTEXT × BExpr × L) set"
where
HS_B_compB: "[(G, e1,p1):HS_E; (G, e2,p2):HS_E; p= LUB p1 p2]
             ==> (G,compB f e1 e2,p) : HS_B"
| HS_B_sup: "[(G,b,p):HS_B; LEQ p q] ==> (G,b,q):HS_B"

lemma HS_B_eval[rule_format]:
"(G, b, t) ∈ HS_B ==>
 ∀ r s pp . EQ G pp r s ⟶ LEQ t pp ⟶ evalB b r = evalB b s"
(*<*)
apply (erule HS_B.induct)
apply clarsimp
  apply (subgoal_tac "evalE e1 r = evalE e1 s", clarsimp) 
  prefer 2 apply (erule HS_E_eval) apply assumption 
           apply (rule LAT2) prefer 2 apply assumption apply (simp add: LAT3)
  apply (subgoal_tac "evalE e2 r = evalE e2 s", clarsimp) 
    apply (erule HS_E_eval) apply assumption
           apply (rule LAT2) prefer 2 apply assumption 
           apply (subgoal_tac "LEQ p2 (LUB p2 p1)", simp add: LAT4)
           apply (simp add: LAT3)
apply clarsimp
  apply (erule_tac x=r in allE, erule_tac x=s in allE, erule_tac x=pp in allE, erule impE)
    apply clarsimp
  apply (erule mp) apply (erule LAT2, assumption)
done
(*>*)

text‹The typing rules for commands follow.›

inductive_set HS::"(L × CONTEXT × IMP × CONTEXT) set"
where
HS_Skip:   "(p,G,Skip,G):HS"

| HS_Assign:
  "(G,e,t):HS_E ==> (p,G,Assign x e,upd G x (LUB p t)):HS"

| HS_Seq:
  "[(p,G,c,K):HS; (p,K,d,H):HS] ==> (p,G, Comp c d,H):HS"

| HS_If:
  "[(G,b,t):HS_B; (LUB p t,G,c,H):HS; (LUB p t,G,d,H):HS] ==>
   (p,G,Iff b c d,H):HS"

| HS_If_alg:
  "[(G,b,p):HS_B; (p,G,c,H):HS; (p,G,d,H):HS] ==>
   (p,G,Iff b c d,H):HS"

| HS_While:
  "[(G,b,t):HS_B; (LUB p t,G,c,H):HS;H=G] ==>
   (p,G,While b c,H):HS"

| HS_Sub:
  "[ (pp,GG,c,HH):HS; LEQ p pp; ∀ x . LEQ (G x) (GG x);
       ∀ x . LEQ (HH x) (H x)] ==>
   (p,G,c,H):HS"

text ‹Using ‹HS_Sub›, rules ‹If› and ‹If_alg› are
 -derivable.›

lemma IF_derivable_from_If_alg:
  "[(G,b,t):HS_B; (LUB p t,G,c1,H):HS; (LUB p t,G,c2,H):HS]
   ==> (p,G,Iff b c1 c2,H):HS"
apply (subgoal_tac "(LUB p t,G,Iff b c1 c2,H):HS")
  apply (erule HS_Sub) apply (rule LAT3)
    apply (clarsimp, rule LAT6) apply (clarsimp, rule LAT6) 
apply (rule HS_If_alg) apply (erule HS_B_sup) 
  apply (subgoal_tac "LEQ t (LUB t p)", simp add: LAT4) 
  apply (rule LAT3) apply assumption+
done

lemma IF_alg_derivable_from_If:
  "[(G,b,p):HS_B; (p,G,c1,H):HS; (p,G,c2,H):HS]
  ==> (p,G,Iff b c1 c2,H):HS"
apply (erule HS_If) apply (subgoal_tac "LUB p p = p", clarsimp) 
  apply (subgoal_tac "p = LUB p p", fastforce) apply (rule LAT7)
apply (subgoal_tac "LUB p p = p", clarsimp) 
  apply (subgoal_tac "p = LUB p p", fastforce) apply (rule LAT7)
done

text‹An easy induction on typing derivations shows the following property.›

lemma HS_Aux1: 
 "(p,G,c,H):HS ==> ∀ x. LEQ (G x) (H x) ∨ LEQ p (H x)"
(*<*)
apply (erule HS.induct)
(*Skip*)
apply (simp add: LAT6)
(*Assign*)
apply (simp add: upd_def) apply clarsimp apply rule
  apply clarsimp apply (simp add: LAT3)
  apply clarsimp apply (simp add: LAT6)
(*Seq*)
apply clarsimp
   apply (erule_tac x=x in allE, erule disjE)
   apply (erule_tac x=x in allE, erule disjE)
     apply (erule LAT2) apply assumption apply fast
   apply (erule_tac x=x in allE, erule disjE)
     apply(subgoal_tac "LEQ p (H x)", fast)
     apply (erule LAT2) apply assumption apply fast
(*If*)
apply clarsimp
   apply (erule_tac x=x in allE, erule disjE) apply assumption
     apply(subgoal_tac "LEQ p (H x)", fast)
     apply (subgoal_tac "LEQ p (LUB p t)", rotate_tac -1)
     apply (erule LAT2) apply assumption 
     apply (rule LAT3)
(*If2*)
apply clarsimp
(*While*)
apply clarsimp
   apply (simp add: LAT6)
(*Sub*)
apply clarsimp
   apply (erule_tac x=x in allE, erule disjE) 
   apply (erule_tac x=x in allE) 
   apply (erule_tac x=x in allE)
     apply (erule LAT2)
     apply (erule LAT2) apply assumption
   apply (erule_tac x=x in allE)
     apply (erule LAT2)
   apply (erule_tac x=x in allE)
     apply (subgoal_tac "LEQ p (H x)", fast)
     apply (erule LAT2)
     apply (erule LAT2) apply assumption
done
(*>*)

subsection‹Derived proof rules›

text‹In order to show the derivability of the properties given in
  3.3 of Hunt and Sands' paper, we give the following derived
  rules. By including the $Q$ property in the $A$ position of
 Sec$, we prove both parts of theorem in one proof, and can exploit
  first property ($Q$) in the proof of the second.›

lemma SKIP:
 "X ⊳ Skip : Sec (Q p H) (EQ G q) (EQ G q)
                  (λ (s,t) . EQ G q s t)"
(*<*)
apply (rule VDMConseq, rule VDMSkip)
  apply (simp add: Sec_def EQ_def Q_def)
done
(*>*)

lemma ASSIGN: 
  "[H = upd G x (LUB p t);
    ∀ s ss . EQ G t s ss ⟶ evalE e s = evalE e ss]
  ==> X ⊳ Assign x e : Sec (Q p H) (EQ G q) (EQ H q)
            (λ (s,t) . ∃ r . s = update r x (evalE e r) ∧ EQ G q r t)"
(*<*)
  apply (rule VDMConseq, rule VDMAssign) apply clarsimp
  apply (simp add: Sec_def EQ_def Q_def)
  apply (rule, clarsimp) apply (simp add: update_def upd_def)
    apply (case_tac "x=xa", clarsimp) apply (simp add: LAT3)
    apply clarsimp
  apply (rule, clarsimp) apply (rule_tac x=s in exI, simp)
  apply clarsimp
    apply (case_tac "x=xa", clarsimp, hypsubst_thin)
      apply (simp add: update_def upd_def)
        apply (erule_tac x=ra in allE, erule_tac x=s in allE, erule mp, clarsimp)
        apply (erule_tac x=x in allE, erule mp)
        apply (erule LAT2, rule LAT2) prefer 2 apply assumption
        apply (subgoal_tac "LEQ t (LUB t p)", simp add: LAT4)  apply (rule LAT3)
      apply (simp add: update_def upd_def) 
done
(*>*)

lemma COMP: 
  "[ X ⊳ c1 : Sec (Q p K) (EQ G q) (EQ K q) Φ;
     X ⊳ c2 : Sec (Q p H) (EQ K q) (EQ H q) Ψ;
    ∀ x . LEQ (G x) (K x) ∨ LEQ p (K x);
    ∀ x . LEQ (K x) (H x) ∨ LEQ p (H x)]
   ==> X ⊳ Comp c1 c2 : Sec (Q p H) (EQ G q) (EQ H q)
        (λ (x, y) . ∃ z . Φ (z, y) ∧
                          (∀ w . EQ K q z w ⟶ Ψ (x, w)))"
(*<*)
  apply (rule VDMConseq, rule VDMComp, assumption, assumption, clarsimp)
    apply (erule thin_rl, erule thin_rl)
  apply (simp add: Sec_def, rule, clarsimp)
    apply (simp add: Q_def, clarsimp)
    apply (rotate_tac 3, erule_tac x=x in allE, erule impE, assumption)
    apply (erule_tac x=x in allE, clarsimp)
    apply (erule_tac x=x in allE, clarsimp)
    apply (subgoal_tac "LEQ p (H x)", fast)
    apply (erule LAT2) apply assumption
  apply (rule, clarsimp)
    apply (rule_tac x=r in exI, simp) 
  apply clarsimp
done
(*>*)

text‹We distinguish, for any given $q$, \emph{parallel} conditionals
  \emph{diagonal} ones. Speaking operationally (i.e.~in terms of
  executions), conditionals of the former kind evaluate the branch
  identically in both executions. The following rule
  this condition explicitly, in the first side condition. The
  inside the $\mathit{Sec}$-operator of the conclusion resembles
  conclusion of the VDM rule for conditionals in that the formula
  depends on the outcome of the branch.›

lemma IF_PARALLEL:
  "[ ∀ s ss . EQ G p s ss ⟶ evalB b s = evalB b ss;
     ∀ x. LEQ (G x) (H x) ∨ LEQ p (H x);
     ∃ x . LEQ p (H x) ∧ LEQ (H x) q;
     X ⊳ c1 : Sec (Q p H) (EQ G q) (EQ H q) Φ;
     X ⊳ c2 : Sec (Q p H) (EQ G q) (EQ H q) Ψ]
  ==> X ⊳ Iff b c1 c2 : Sec (Q p H) (EQ G q) (EQ H q)
                       (λ (r, u) . (evalB b u ⟶ Φ (r, u)) ∧
                                   ( (¬ evalB b u) ⟶ Ψ (r, u)))"
(*<*)
    apply (rule VDMConseq, rule VDMIff) apply (assumption, assumption) apply clarsimp
    apply (simp add: Sec_def Q_def)
    apply (subgoal_tac "(∀x. ¬ LEQ p (H x) ⟶ t x = s x)", simp)
    prefer 2 apply (case_tac "evalB b s", clarsimp,clarsimp) 
    apply (rule, clarsimp)
    (*left component of Sec*)
      apply (subgoal_tac "evalB b s = evalB b r")
      prefer 2 apply (erule_tac x=s in allE, rotate_tac -1, erule_tac x=r in allE, erule mp)
        apply (erule EQ_LEQ) apply (erule LAT2, assumption)
      apply (case_tac "evalB b s")
              apply clarsimp 
              apply clarsimp 
    (*right component of Sec*)
      apply clarsimp
      apply (case_tac "evalB b s")
        apply clarsimp  
        apply clarsimp 
done
(*>*)

text‹An alternative formulation replaces the first side condition
  a typing hypothesis on the branch condition, thus exploiting
  HS\_B\_eval.›

lemma IF_PARALLEL_tp:
  "[ (G, b, p) ∈ HS_B; (p , G, c1, H) ∈ HS; (p, G, c2, H) ∈ HS;
     ∃ x . LEQ p (H x) ∧ LEQ (H x) q;
     X ⊳ c1 : Sec (Q p H) (EQ G q) (EQ H q) Φ;
     X ⊳ c2 : Sec (Q p H) (EQ G q) (EQ H q) Ψ]
  ==> X ⊳ Iff b c1 c2 : Sec (Q p H) (EQ G q) (EQ H q)
                       (λ (r, u) . (evalB b u ⟶ Φ (r, u)) ∧
                                   ( (¬ evalB b u) ⟶ Ψ (r, u)))"
(*<*)
  apply (rule IF_PARALLEL)
    apply (clarsimp, erule HS_B_eval) apply assumption apply (rule LAT6)
    apply (erule HS_Aux1)
    apply assumption+
done
(*>*)

text‹Diagonal conditionals, in contrast, capture cases where (from
  perspective of an observer at level $q$) the two executions may
  the branch condition differently. In this case, the formula
  the $\mathit{Sec}$-operator in the conclusion cannot depend
  the branch outcome, so the least common denominator of the two
  must be taken, which is given by the equality condition
 .r.t.~the post-context $H$. A side condition (the first one given in
  rule) ensures that indeed no information leaks during the
  of either branch, by relating $G$ and $H$.›

lemma IF_DIAGONAL:
  "[ ∀x. LEQ (G x) (H x) ∨ LEQ p (H x);
      ¬ (∃x. LEQ p (H x) ∧ LEQ (H x) q);
      X ⊳ c1 : Sec (Q p H) (EQ G q) (EQ H q) Φ;
      X ⊳ c2 : Sec (Q p H) (EQ G q) (EQ H q) Ψ]
   ==> X ⊳ Iff b c1 c2 : Sec (Q p H) (EQ G q) (EQ H q)
                             (λ (s,t). EQ H q s t)"
(*<*)
  apply clarsimp
  apply (rule VDMConseq, rule VDMIff) apply (assumption, assumption) apply clarsimp
  apply (simp add: Sec_def Q_def)
  apply (subgoal_tac "(∀x. ¬ LEQ p (H x) ⟶ t x = s x)", simp)
  prefer 2 apply (case_tac "evalB b s")
           apply clarsimp
           apply clarsimp
  apply (rule, clarsimp)
  (*Left component*)
    apply (simp (no_asm) add: EQ_def, clarsimp)
    apply (case_tac "LEQ p (H x)") apply clarsimp
    apply (rotate_tac -4, erule_tac x=x in allE, clarsimp)
    apply (simp add: EQ_def)
    apply (erule_tac x=x in allE, erule mp)
    apply (rotate_tac -4, erule_tac x=x in allE, clarsimp)
    apply (erule LAT2, assumption)
  (*right component*)
    apply clarsimp
    apply (simp add: EQ_def, clarsimp)
    apply (case_tac "LEQ p (H x)")
    apply clarsimp
    apply clarsimp
done
(*>*)

text‹Again, the first side condition of the rule may be replaced by a
  condition, but now this condition is on the commands (instead
  the branch condition) -- in fact, a derivation for either branch
 .›

lemma IF_DIAGONAL_tp:
  "[ (p, G, c1, H) ∈ HS ∨ (p, G, c2, H) ∈ HS;
      ¬ (∃x. LEQ p (H x) ∧ LEQ (H x) q);
      X ⊳ c1 : Sec (Q p H) (EQ G q) (EQ H q) Φ;
      X ⊳ c2 : Sec (Q p H) (EQ G q) (EQ H q) Ψ]
   ==> X ⊳ Iff b c1 c2 : Sec (Q p H) (EQ G q) (EQ H q)
                             (λ (s,t). EQ H q s t)"
(*<*)
  apply (rule IF_DIAGONAL)
    apply (erule disjE) apply (erule HS_Aux1) apply (erule HS_Aux1)
    apply assumption+
done
(*>*)

text‹Obviously, given $q$, any conditional is either parallel or
  as the second side conditions of the diagonal rules and the
  rules are exclusive.›

lemma if_algorithmic:
  "[∃ x . LEQ p (H x) ∧ LEQ (H x) q;
    ¬ (∃x. LEQ p (H x) ∧ LEQ (H x) q)]
   ==> False"
(*<*) by simp (*>*)


text‹As in Section \ref{sec:BaseLineNI} we define a fixed point
 , useful for the (parallel) while rule.›

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

text‹For monotone invariant transformers, the construction indeed
  a fixed point.›

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
(*>*)
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‹Next, the definition of a while-operator.›

definition PhiWhilePOp::
          "VDMAssn ==> BExpr ==> TT ==> TT ==> TT"
where "PhiWhilePOp A b Φ =
  (λ Ψ . (λ(r, u). (evalB b u ⟶ (∃z. Φ (z, u) ∧
                                        (∀w. A z w ⟶ Ψ (r, w)))) ∧
                     ((¬ evalB b u) ⟶ A r u)))"

text‹This operator is monotone in $\Phi$.›

lemma PhiWhilePOp_Monotone:"Monotone (PhiWhilePOp A b Φ)"
(*<*)
apply (simp add: PhiWhilePOp_def Monotone_def) apply clarsimp
  apply (rule_tac x=z in exI, simp)
done
(*>*)

text‹Therefore, we can define the following fixed point.›

definition PhiWhileP::"VDMAssn ==> BExpr ==> TT ==> TT"
where "PhiWhileP A b Φ = FIX (PhiWhilePOp A b Φ)"

text‹As as a function on $\phi$, this PhiWhileP is itself monotone
  $\phi$:›

lemma PhiWhilePMonotone: "Monotone (λ Φ . PhiWhileP A b Φ)"
(*<*)
apply (simp add: Monotone_def) apply clarsimp
apply (simp add: PhiWhileP_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: PhiWhilePOp_def) apply clarsimp
apply (rule_tac x=z in exI, simp)
done
(*>*)

text‹Now the rule for parallel while loops, i.e.~loops where the
  condition evaluates identically in both executions.›

lemma WHILE_PARALLEL:
 "[ X ⊳ c : Sec (Q p G) (EQ G q) (EQ G q) Φ;
    ∀ s ss . EQ G p s ss ⟶ evalB b s = evalB b ss; LEQ p q]
 ==> X ⊳ While b c : Sec (Q p G) (EQ G q) (EQ G q)
                         (PhiWhileP (EQ G q) b Φ)"
(*<*)
apply (rule VDMConseq)
apply (rule VDMWhile)
prefer 4 apply (subgoal_tac "∀s t. Sec (Q p G) (EQ G q) (EQ G q) (PhiWhilePOp (EQ G q) b Φ (PhiWhileP (EQ G q) b Φ)) s t ∧ ¬ evalB b t ⟶ Sec (Q p G) (EQ G q) (EQ G q) (PhiWhileP (EQ G q) b Φ) s t") apply assumption
  apply clarsimp apply (subgoal_tac "PhiWhilePOp (EQ G q) b Φ (PhiWhileP (EQ G q) b Φ) = PhiWhileP (EQ G q) b Φ", clarsimp)
                 apply (simp add: PhiWhileP_def) apply (rule Fix_lemma) apply (rule PhiWhilePOp_Monotone)
apply assumption
apply clarsimp apply (simp add: Sec_def) 
  apply rule apply (simp add: Q_def)
  apply (rule, clarsimp) apply (simp add: PhiWhilePOp_def) apply clarsimp
      apply (erule_tac x=s in allE, erule_tac x=r in allE, erule impE) apply (erule EQ_LEQ) apply assumption apply clarsimp
  apply clarsimp apply (simp add: PhiWhilePOp_def)
apply clarsimp apply (simp add: Sec_def)
  apply rule apply clarsimp apply (simp add: Q_def)
  apply rule
  prefer 2 apply clarsimp
    apply (subgoal_tac "∃r. Φ (r, s) ∧ (∀w. EQ G q r w ⟶ (PhiWhileP (EQ G q) b Φ) (ra, w))")
    prefer 2 apply (simp add: PhiWhilePOp_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 "PhiWhilePOp (EQ G q) b Φ (PhiWhileP (EQ G q) b Φ) = PhiWhileP (EQ G q) b Φ", clarsimp)
    apply (simp add: PhiWhileP_def)
    apply (rule Fix_lemma) apply (rule PhiWhilePOp_Monotone)
  apply clarsimp
    apply (simp (no_asm_simp) add: PhiWhilePOp_def) 
    apply rule
    prefer 2  apply clarsimp
              apply (erule_tac x=s in allE, rotate_tac -1, erule_tac x=ra in allE, erule impE)
               apply (erule EQ_LEQ) apply assumption apply clarsimp 
    apply clarsimp
    apply (rotate_tac 2, erule_tac x=ra in allE, clarsimp)
    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 "PhiWhilePOp (EQ G q) b Φ (PhiWhileP (EQ G q) b Φ) = PhiWhileP (EQ G q) b Φ", clarsimp)
    apply (simp add: PhiWhileP_def)
    apply (rule Fix_lemma) apply (rule PhiWhilePOp_Monotone)
done
(*>*)

text‹The side condition regarding the evalution of the branch
  may be replaced by a typing hypothesis, thanks to lemma
 ‹HS_B_eval›.›

lemma WHILE_PARALLEL_tp:
 "[ X ⊳ c : Sec (Q p G) (EQ G q) (EQ G q) Φ;
    (G, b, p) ∈ HS_B; LEQ p q]
 ==> X ⊳ While b c : Sec (Q p G) (EQ G q) (EQ G q)
                         (PhiWhileP (EQ G q) b Φ)"
(*<*)
apply (erule WHILE_PARALLEL)
apply clarsimp 
  apply (erule HS_B_eval) apply assumption apply (rule LAT6)
apply assumption
done
(*>*)

text‹One may also give an inductive formulation of FIX:›

inductive_set var::"(BExpr × VDMAssn × TT × State × State) set"
where
varFalse:
   "[¬ evalB b t; A s t] ==> (b,A,Φ,s,t):var"
| varTrue:
   "[evalB b t; Φ(r,t); (∀ w . A r w ⟶
    (b,A,Φ,s,w): var) ] ==> (b,A,Φ,s,t):var"

(*<*)
lemma varFIX: "(b,A,Φ,s,t):var ==> PhiWhileP A b Φ (s,t)"
apply (erule var.induct)
apply (simp add: PhiWhileP_def)
  apply (subgoal_tac "PhiWhilePOp A b Φ (FIX (PhiWhilePOp A b Φ)) (s,t)")
  apply (subgoal_tac "PhiWhilePOp A b Φ (FIX (PhiWhilePOp A b Φ)) = FIX (PhiWhilePOp A b Φ)", clarsimp)
  apply (rule Fix_lemma) apply (rule PhiWhilePOp_Monotone)
  apply (simp add: PhiWhilePOp_def)
apply (simp (no_asm_simp) add: PhiWhileP_def)
apply (subgoal_tac "PhiWhilePOp A b Φ (FIX (PhiWhilePOp A b Φ)) (s,t)")
  apply (subgoal_tac "PhiWhilePOp A b Φ (FIX (PhiWhilePOp A b Φ)) = FIX (PhiWhilePOp A b Φ)", clarsimp)
  apply (rule Fix_lemma) apply (rule PhiWhilePOp_Monotone)
  apply (simp add: PhiWhilePOp_def)
  apply (rule_tac x=r in exI, simp)
  apply clarsimp
  apply (erule_tac x=w in allE, clarsimp)
  apply (simp add: PhiWhileP_def)
  apply (simp add: PhiWhilePOp_def)
done

lemma FIXvar: "PhiWhileP A b Φ (s,t) ==> (b,A,Φ,s,t):var"
apply (simp add: PhiWhileP_def)
apply (subgoal_tac "PhiWhilePOp A b Φ (FIX (PhiWhilePOp A b Φ)) (s, t)")
prefer 2 
  apply (subgoal_tac "PhiWhilePOp A b Φ (FIX (PhiWhilePOp A b Φ)) = FIX (PhiWhilePOp A b Φ)", clarsimp)
  apply (rule Fix_lemma) apply (rule PhiWhilePOp_Monotone)
apply (erule thin_rl, simp add: PhiWhilePOp_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,A,Φ,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
(*>*)

text‹The inductive formulation and the fixed point formulation are
 .›
(*<*)
lemma varFIXvar: "(PhiWhileP A b Φ (s,t)) = ((b,A,Φ,s,t):var)"
apply rule
apply (erule FIXvar)
apply (erule varFIX)
done
(*>*)
(*<*)
lemma FIXvarFIX': "(PhiWhileP A b Φ) = (λ (s,t) . (b,A,Φ,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: 
"PhiWhileP A b = (λ Φ . (λ (s,t) . (b,A,Φ,s,t):var))"
(*<*)
by (rule, rule FIXvarFIX')
(*>*)

text‹Thus, the above while rule may also be written using the
  formulation.›

lemma WHILE_PARALLEL_IND:
 "[ X ⊳ c : Sec (Q p G) (EQ G q) (EQ G q) Φ;
    ∀ s ss . EQ G p s ss ⟶ evalB b s = evalB b ss; LEQ p q] ==>
   X ⊳ While b c : (Sec (Q p G) (EQ G q) (EQ G q)
                    (λ (s,t) . (b,EQ G q,Φ,s,t):var))"
(*<*)
apply (rule VDMConseq)
apply (rule WHILE_PARALLEL) apply assumption+
apply clarsimp
apply (simp add: FIXvarFIX)
done
(*>*)

text‹Again, we may replace the side condition regarding the branch
  by a typing hypothesis.›

lemma WHILE_PARALLEL_IND_tp:
 "[ X ⊳ c : Sec (Q p G) (EQ G q) (EQ G q) Φ;
    (G, b, p) ∈ HS_B; LEQ p q ] ==>
 X ⊳ (While b c) :
  (Sec (Q p G) (EQ G q) (EQ G q) (λ (s,t) . (b,EQ G q,Φ,s,t):var))"
(*<*)
apply (erule WHILE_PARALLEL_IND)
apply clarsimp 
  apply (erule HS_B_eval) apply assumption apply (rule LAT6)
apply assumption
done
(*>*)
(*<*)
lemma varMonotoneAux[rule_format]:
 "(b, A, Φ, s, t) ∈ var ==>
  (∀s t. Φ (s, t) ⟶ Ψ (s, t)) ⟶
  (b, A, Ψ, s, t) ∈ var"
apply (erule var.induct)
apply clarsimp apply (erule varFalse, simp)
apply clarsimp apply (erule varTrue) apply fast apply simp
done
(*>*)
text‹Of course, the inductive formulation is also monotone:›

lemma var_MonotoneInPhi:
  "Monotone (λ Φ . (λ (s,t) .(b,A, Φ,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,A, Φ,s,t):var))"
apply (subgoal_tac "Monotone (λ Φ . PhiWhileP A b Φ)")
apply (simp add: FIXvarFIX)
apply (rule PhiWhilePMonotone)
done  
(*>*)

text‹In order to derive a diagonal while rule, we directly define an
  relation that calculates the transitive closure of relation
 A$, such that all but the last state evaluate $b$ to
 \mathit{True}$.›

inductive_set varD::"(BExpr × VDMAssn × State × State) set"
where
varDFalse: "[¬ evalB b s; A s t] ==> (b,A,s,t):varD"
| varDTrue: "[evalB b s; A s w; (b,A,w,t): varD ] ==> (b,A,s,t):varD"

text‹Here is the obvious definition of transitivity for assertions.›

definition transitive::"VDMAssn ==> bool"
where "transitive P = (∀ x y z . P x y ⟶ P y z ⟶ P x z)"

text‹The inductive relation satisfies the following property.›

lemma varD_transitive[rule_format]: 
 "(b,A,s,t):varD ==> transitive A ⟶ A s t"
(*<*)
apply (erule varD.induct)
apply clarsimp
apply clarsimp 
  apply (unfold transitive_def) apply (erule_tac x=s in allE, erule_tac x=w in allE, erule_tac x=t in allE, simp)
done
(*>*)

text‹On the other hand, the assertion $\mathit{Q}$ defined above is transitive,›

lemma Q_transitive:"transitive (Q q G)"
(*<*)
by (simp add: Q_def transitive_def) 
(*>*)

text‹and is hence respected by the inductive closure:›

lemma varDQ:"(b,Q q G,s,t):varD ==> Q q G s t"
(*<*)by (erule varD_transitive,rule Q_transitive)(*>*)

text‹The diagonal while rule has a conclusion that is independent of
 \phi$.›

lemma WHILE_DIAGONAL:
 "[X ⊳ c : Sec (Q p G) (EQ G q) (EQ G q) Φ; ¬ LEQ p q]
       ==> X ⊳ While b c : Sec (Q p G) (EQ G q) (EQ G q)
                               (λ (s,t). EQ G q s t)"
(*<*)
apply (subgoal_tac "∀x. LEQ p (G x) ⟶ ¬ LEQ (G x) q")
prefer 2 apply (case_tac "∀x. LEQ p (G x) ⟶ ¬ LEQ (G x) q", assumption) apply clarsimp
  apply (subgoal_tac "LEQ p q", fast)
  apply (erule LAT2, assumption)
apply (rule VDMConseq)
apply (insert VDMWhile)
  apply (erule VDMWhile [of X c "Sec (Q p G) (EQ G q) (EQ G q) Φ" b "(λ s t . (b,Q p G,s,t):varD)"])
    apply clarsimp apply (erule varDFalse) apply (simp add: Q_def) 
    apply clarsimp apply (simp add: Sec_def) apply clarsimp
      apply (rule varDTrue) apply assumption prefer 2 apply assumption 
        apply (erule_tac x=s in allE, erule impE, simp add: EQ_def) apply assumption 
apply clarsimp 
apply (simp add: Sec_def)
apply rule apply (erule varDQ) 
apply (rule, clarsimp) 
  apply (drule varDQ)  apply (simp add: Q_def EQ_def, clarsimp) 
  apply (case_tac "LEQ p (G x)") prefer 2 apply simp 
  apply (rotate_tac -1, drule LAT2) apply assumption apply fast 
apply (drule varDQ)  apply (simp add: Q_def EQ_def, clarsimp) 
  apply (case_tac "LEQ p (G x)") prefer 2 apply simp 
  apply (rotate_tac -1, drule LAT2) apply assumption apply fast 
done
(*>*)

text‹$\mathit{varD}$ is monotone in the assertion position.›

lemma varDMonotoneInAssertion[rule_format]:
  "(b, A, s, t) ∈ varD ==>
   (∀s t. A s t ⟶ B s t) ⟶ (b, B, s, t) ∈ varD"
(*<*)
apply (erule varD.induct) 
apply clarsimp apply (erule varDFalse) apply simp
apply clarsimp apply (erule varDTrue) prefer 2 apply assumption apply simp
done
(*>*)

(*<*)
text‹As $\mathit{varD}$ does not depend on $\Phi$, the monotonicity
  in this position is trivially fulfilled.›

lemma varDMonotoneInPhi[rule_format]:
  "[(b, A, s, t) ∈ varD; ∀s t. Φ(s, t) ⟶ Ψ(s, t)]
  ==> (b, A, s, t) ∈ varD"
by simp
(*>*)

text‹Finally, the subsumption rule.›

lemma SUB:
  "[ LEQ p pp; ∀x. LEQ (G x) (GG x); ∀x. LEQ (HH x) (H x);
     X ⊳ c : Sec (Q pp HH) (EQ GG q) (EQ HH q) Φ]
   ==> X ⊳ c : Sec (Q p H) (EQ G q) (EQ H q) Φ"
(*<*)
apply (erule VDMConseq)
  apply (simp add: Sec_def EQ_def, clarsimp)
  apply (rule, simp add: Q_def, clarsimp)
    apply (erule_tac x=x in allE, erule mp, clarsimp)
    apply (subgoal_tac "LEQ p (H x)", fast)
    apply (rotate_tac 2, erule_tac x=x in allE)
    apply (erule LAT2)
    apply (erule LAT2, assumption)
  apply (rule, clarsimp)
    apply (erule_tac x=r in allE, erule mp, clarsimp)
    apply (erule_tac x=x in allE, erule mp)
    apply (erule_tac x=x in allE, erule LAT2,assumption) 
  apply clarsimp
    apply (erule_tac x=r in allE, erule impE, assumption)
    apply (erule_tac x=x in allE, erule mp)
    apply (erule_tac x=x in allE, erule LAT2, assumption) 
done
(*>*)

subsection‹Soundness results›

(*<*)
definition Theorem3derivProp::"VDMAssn set ==> L ==> CONTEXT ==> IMP ==> CONTEXT ==> L ==> bool"
where "Theorem3derivProp X p G c H q = (∃ Φ . X ⊳ c : (Sec (Q p H) (EQ G q) (EQ H q) Φ))"

lemma Theorem3_derivAux[rule_format]: 
"(p,G,c,H):HS ==> Theorem3derivProp X p G c H q"
apply (erule HS.induct)
apply (simp_all add: Theorem3derivProp_def)
(*Skip*)
  apply (rule, rule SKIP) 
(*Assign*)
  apply (rule, rule ASSIGN[simplified]) apply simp 
  apply (clarsimp, erule HS_E_eval) apply assumption apply (rule LAT6)
(*COMP*)
apply clarsimp
  apply (rule, rule COMP) apply (assumption, assumption) apply (erule HS_Aux1) 
  apply (erule HS_Aux1)
(*IFF*) 
  apply clarsimp
  apply (subgoal_tac "(G, b, LUB p t) ∈ HS_B", erule thin_rl)
  prefer 2 apply (erule HS_B_sup) apply (subgoal_tac "LEQ t (LUB t p)", simp add: LAT4) apply (rule LAT3)
  apply (subgoal_tac "∃ psi. X ⊳ Iff b c d : Sec (Q (LUB p t) H) (EQ G q) (EQ H q) psi", clarsimp)
  apply (rule_tac x=psi in exI, erule VDMConseq, clarsimp)
    apply (simp add: Sec_def, clarsimp)
    apply (simp add: Q_def, clarsimp)
    apply (erule_tac x=x in allE, erule mp, clarsimp)
    apply (subgoal_tac "LEQ p (LUB p t)")
    prefer 2 apply (rule LAT3)
    apply (rotate_tac -1, drule LAT2) apply assumption apply simp
  apply (case_tac "∃ x . LEQ (LUB p t) (H x) ∧ LEQ (H x) q")
    apply (rule, erule IF_PARALLEL_tp) apply assumption+
    apply (rule, rule IF_DIAGONAL) apply (erule HS_Aux1) apply assumption+
(*If2*)
  apply clarsimp
  apply (case_tac "∃ x . LEQ p (H x) ∧ LEQ (H x) q")
    apply (rule, erule IF_PARALLEL_tp) apply assumption+
    apply (rule, rule IF_DIAGONAL) apply (erule HS_Aux1) apply assumption+
(*While*)
  apply clarsimp
  apply (subgoal_tac "(G, b, LUB p t) ∈ HS_B", erule thin_rl)
  prefer 2 apply (erule HS_B_sup) apply (subgoal_tac "LEQ t (LUB t p)", simp add: LAT4) apply (rule LAT3)
  apply (subgoal_tac "∃ psi. X ⊳ While b c : Sec (Q (LUB p t) G) (EQ G q) (EQ G q) psi", clarsimp)
  apply (rule_tac x=psi in exI, erule VDMConseq, clarsimp)
    apply (simp add: Sec_def, clarsimp)
    apply (simp add: Q_def, clarsimp)
    apply (erule_tac x=x in allE, erule mp, clarsimp)
    apply (subgoal_tac "LEQ p (LUB p t)")
    prefer 2 apply (rule LAT3)
    apply (rotate_tac -1, drule LAT2) apply assumption apply simp
  apply (case_tac "LEQ (LUB p t) q")
    apply (rule, rule WHILE_PARALLEL) apply assumption
      apply clarsimp apply (erule HS_B_eval)  apply assumption apply (rule LAT6) apply assumption
  (*OTHER CASE*)
  apply (rule, erule WHILE_DIAGONAL) apply assumption
(*Sub*)
  apply clarsimp
  apply (rule, erule SUB, assumption+)
done
(*>*)

text‹An induction on the typing rules now proves the main theorem
  was called Theorem 4 in~cite‹"BeringerHofmann:CSF2007"›.›

theorem Theorem4[rule_format]: 
  "(p,G,c,H):HS ==>
  (∃ Φ . X ⊳ c : (Sec (Q p H) (EQ G q) (EQ H q) Φ))"
(*<*)
by (drule Theorem3_derivAux, simp add: Theorem3derivProp_def)
(*>*)

text‹By the construction of the operator $\mathit{Sec}$ (lemmas
 ‹Prop4A› and ‹Prop4A› in Section \ref{sec:ARSsecurity}) we
  the soundness property with respect to the oprational
 , i.e.~the result stated as Theorem 3.3 in
 cite‹"HuntSands:POPL2006"›.›

theorem HuntSands33: "(p,G,c,H):HS ==> secure p G c H"
(*<*)
apply (simp add: secure_def, clarsimp)
apply (drule Theorem4, clarsimp) 
apply (rule Prop4A)
apply (rule VDM_Sound_emptyCtxt)  apply fast
done
(*>*)

text ‹Both parts of this theorem may also be shown
 . We factor both proofs by the program logic.›

lemma Sec1_deriv: "(p,G,c,H):HS ==> X ⊳ c : (Q p H)"
(*<*)
apply (drule Theorem4, clarsimp)
apply (erule VDMConseq)
apply (simp add: Sec_def) apply clarsimp
done
(*>*)

(*<*)
lemma 
 "(p,G,c,H):HS ==>
  X ⊳ c : (λ s t . ∀ x . ¬ LEQ p (H x) ⟶ s x = t x)"
apply (drule Sec1_deriv) apply (erule VDMConseq) apply (simp add: Q_def)
done
(*>*)

theorem HuntSands33_1:"(p,G,c,H):HS ==> secure1 p G c H"
(*<*)
apply (subgoal_tac "{} ⊳ c : Q p H")
apply (drule VDM_Sound) 
  apply (simp add: Q_def secure1_def valid_def VDM_valid_def Ctxt_valid_def)
apply (erule Sec1_deriv)
done(*>*)

lemma Sec2_deriv: 
  "(p,G,c,H):HS ==>
  (∃ A . X ⊳ c : (Sec (Q p H) (EQ G q) (EQ H q) A))"
(*<*)
by (drule Theorem4 [of p G c H "X" q], clarsimp)
(*>*)

(*<*)
lemma Sec2:
  "(p,G,c,H):HS ==>
   (∃ Φ . ⊨ c : (Sec (Q p H) (EQ G q) (EQ H q) Φ))"
apply (drule Theorem4 [of p G c H "{}" q], clarsimp)
apply (rule_tac x=Φ in exI, erule VDM_Sound_emptyCtxt)
done
(*>*)

theorem HuntSands33_2: "(p,G,c,H):HS ==> secure2 q G c H"
(*<*)
apply (subgoal_tac "∀ q . ARSsecure (Q p H) (EQ G q) (EQ H q) c")
prefer 2 apply clarsimp
         apply (drule Sec2_deriv[of p G c H "{}"], erule exE)
         apply (rule Prop4A) apply (erule VDM_Sound_emptyCtxt)
apply (insert secureEQUIV [of p G c H]) apply (simp add: secure_def)
done
(*>*)

text‹Again, the call rule is formulated for an arbitrary fixed point
  a monotone transformer.›

lemma CALL: 
  "[ ({B} ∪ X) ⊳ body : Sec A R S (φ(FIX φ));
      Monotone φ; B = Sec A R S (FIX φ) ]
   ==> X ⊳ Call : B"
(*<*)
apply (rule VDMCall)
apply (subgoal_tac "φ (FIX φ) = FIX φ", clarsimp)
apply (erule Fix_lemma)
done
(*>*)

(*<*)
text‹Monotonicity lemmas for the operators occurring in the derived proof rules.›
lemma SkipMonotone:"Monotone (λ T (s,t). EQ G p s t)"
by (simp add: Monotone_def)

lemma AssignMonotone:"Monotone (λ T (s,t). ∃r. s = update r x (evalE e r) ∧ EQ G p r t)"
by (simp add: Monotone_def)

lemma CompMonotone: "Monotone (λ T (s,t). ∃ r. A r t ∧ (∀w. EQ K q r w ⟶ B s w))"
by (simp add: Monotone_def)

lemma IfPMonotone1: "Monotone (λ T (s,t). (evalB b t ⟶ T(s,t)) ∧ (¬ evalB b t ⟶ B (s,t)))"
by (simp add: Monotone_def)

lemma IfPMonotone2: "Monotone (λ T (s,t). (evalB b t ⟶ A(s,t)) ∧ (¬ evalB b t ⟶ T (s,t)))"
by (simp add: Monotone_def)

lemma IfDMonotone:"Monotone (λ T (s,t). EQ G p s t)"
by (simp add: Monotone_def)


lemma WhileDMonotone: "Monotone (λ T (s,t). EQ G q s t)"
by (simp add: Monotone_def)

lemma SubMonotone: "Monotone (λT. T)"
by (simp add: Monotone_def)
(*>*)

text‹As in Section \ref{sec:BaseLineNI}, we define a formal derivation system
  all derived rules and show that all derivable judgements
  of the for $\mathit{Sec}(\Phi)$ for some monotone $\Phi$.›

inductive_set Deriv:: "(VDMAssn set × IMP × VDMAssn) set"
where
D_SKIP: 
  "Ω = (λ (s,t). EQ G q s t)
 ==> (X, Skip, Sec (Q p H) (EQ G q) (EQ G q) Ω) : Deriv"

| D_ASSIGN: 
  "[H = upd G x (LUB p t);
    ∀ s ss . EQ G t s ss ⟶ evalE e s = evalE e ss;
    Ω = (λ (s, t) . ∃ r . s = update r x (evalE e r) ∧ EQ G q r t)]
\<Longrightarrow> (X, Assign x e, Sec (Q p H) (EQ G q) (EQ H q) Ω) : Deriv"

| D_COMP: 
  "[ (X, c, Sec (Q p K) (EQ G q) (EQ K q) Φ) : Deriv;
     (X, d, Sec (Q p H) (EQ K q) (EQ H q) Ψ) : Deriv;
    ∀ x . LEQ (G x) (K x) ∨ LEQ p (K x);
    ∀ x . LEQ (K x) (H x) ∨ LEQ p (H x);
    Ω = (λ (x, y) . ∃ z . Φ(z,y) ∧ (∀ w . EQ K q z w ⟶ Ψ(x,w)))]
 ==> (X, Comp c d, Sec (Q p H) (EQ G q) (EQ H q) Ω) : Deriv"

| D_IF_PARALLEL:
  "[ ∀ s ss . EQ G p s ss ⟶ evalB b s = evalB b ss;
     ∀ x. LEQ (G x) (H x) ∨ LEQ p (H x);
     ∃ x . LEQ p (H x) ∧ LEQ (H x) q;
     (X, c, Sec (Q p H) (EQ G q) (EQ H q) Φ) : Deriv;
     (X, d, Sec (Q p H) (EQ G q) (EQ H q) Ψ) : Deriv;
     Ω = (λ (r, u) . (evalB b u ⟶ Φ(r,u)) ∧
                      ( (¬ evalB b u) ⟶ Ψ(r,u)))]
  ==> (X, Iff b c d, Sec (Q p H) (EQ G q) (EQ H q) Ω) : Deriv"

| D_IF_DIAGONAL:
  "[ ∀x. LEQ (G x) (H x) ∨ LEQ p (H x);
     ¬ (∃x. LEQ p (H x) ∧ LEQ (H x) q);
     (X, c, Sec (Q p H) (EQ G q) (EQ H q) Φ) : Deriv;
     (X, d, Sec (Q p H) (EQ G q) (EQ H q) Ψ) : Deriv;
     Ω = (λ (s,t) . EQ H q s t)]
   ==> (X, Iff b c d, Sec (Q p H) (EQ G q) (EQ H q) Ω) : Deriv"

| D_WHILE_PARALLEL:
 "[ (X, c, Sec (Q p G) (EQ G q) (EQ G q) Φ):Deriv;
    ∀ s ss . EQ G p s ss ⟶ evalB b s = evalB b ss; LEQ p q;
    Ω = (λ (s,t) . (b,EQ G q,Φ,s,t):var)]
   ==> (X, While b c, Sec (Q p G) (EQ G q) (EQ G q) Ω):Deriv"

| D_WHILE_DIAGONAL:
 "[(X, c, Sec (Q p G) (EQ G q) (EQ G q) Φ) : Deriv; ¬ LEQ p q;
   Ω = (λ (s,t) . EQ G q s t)]
 ==> (X, While b c, Sec (Q p G) (EQ G q) (EQ G q) Ω) : Deriv"

| D_SUB:
  "[ LEQ p pp; ∀x. LEQ (G x) (GG x); ∀x. LEQ (HH x) (H x);
     (X, c, Sec (Q pp HH) (EQ GG q) (EQ HH q) Φ) : Deriv]
   ==> (X, c, Sec (Q p H) (EQ G q) (EQ H q) Φ) :Deriv"

| D_CALL:
  "({A} ∪ X,body,A): Deriv ==> (X,Call,A) : Deriv"

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

lemma DerivProp_Aux: "(X,c,A):Deriv ==> DProp A"
apply (erule Deriv.induct)
apply (simp_all add: DProp_def)
apply (rule_tac x="Q p H" in exI,
       rule_tac x="EQ G q" in exI,
       rule_tac x="EQ G q" in exI)
       apply rule apply rule 
       apply simp
       apply (simp add: Monotone_def)
apply (rule_tac x="(Q p (upd G x (LUB p t)))" in exI,
       rule_tac x="EQ G q" in exI,
       rule_tac x="(EQ (upd G x (LUB p t)) q)" in exI)
       apply rule apply rule
       apply simp
       apply (simp add: Monotone_def)
apply clarsimp
apply (rule_tac x="Q p H" in exI,
       rule_tac x="EQ G q" in exI,
       rule_tac x="EQ H q" in exI)
       apply rule apply rule
       apply simp
       apply (simp add: Monotone_def)
apply clarsimp 
apply (rule_tac x="Q p H" in exI,
       rule_tac x="EQ G q" in exI,
       rule_tac x="EQ H q" in exI)
       apply rule apply rule apply simp 
       apply (simp add: Monotone_def)
apply clarsimp
apply (rule_tac x="Q p H" in exI,
       rule_tac x="EQ G q" in exI,
       rule_tac x="EQ H q" in exI)
       apply rule apply rule
       apply simp
       apply (simp add: Monotone_def)
apply clarsimp
apply (rule_tac x="Q p G" in exI,
       rule_tac x="EQ G q" in exI,
       rule_tac x="EQ G q" in exI)
       apply rule apply rule 
       apply simp
       apply (simp add: Monotone_def)
apply clarsimp
apply (rule_tac x="Q p G" in exI,
       rule_tac x="EQ G q" in exI,
       rule_tac x="EQ G q" in exI)
       apply rule apply rule 
       apply simp
       apply (simp add: Monotone_def)
apply clarsimp
apply (rule_tac x="Q p H" in exI,
       rule_tac x="EQ G q" in exI,
       rule_tac x="EQ H q" in exI)
       apply rule apply rule apply simp
       apply (simp add: Monotone_def)
done
(*>*)

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

text‹Also, the ‹Deriv› is indeed a subsystem of the program
 .›

theorem Deriv_derivable: "(X,c,A):Deriv ==> X ⊳ c :A"
(*<*)
apply (erule Deriv.induct)
apply clarify apply (rule SKIP)
apply clarify apply (rule_tac t=t in ASSIGN) apply simp apply assumption
apply clarify apply (rule COMP) apply assumption apply assumption apply assumption apply assumption
apply clarify apply (rule IF_PARALLEL) apply assumption apply assumption apply (rule_tac x=x in exI, simp) apply assumption apply assumption 
apply clarify apply (rule IF_DIAGONAL) apply assumption apply assumption apply assumption apply assumption 
apply clarify apply (rule WHILE_PARALLEL_IND) apply assumption apply assumption apply assumption 
apply clarify apply (rule WHILE_DIAGONAL) apply assumption apply assumption 
apply (rule SUB) apply assumption apply assumption apply assumption apply assumption 
apply (frule DerivMono) apply (erule exE)+ apply clarsimp
  apply (subgoal_tac "X ⊳ Call : Sec Aa R S (FIX φ)")
  prefer 2 apply (rule CALL)
    prefer 2 apply assumption
    apply (simp add: Fix_lemma)
    apply simp
  apply (simp add: Fix_lemma)
done
(*>*)
text‹End of theory HuntSands›
end