Theory VS_OBJ

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

subsection‹Non-interference›
text‹\label{sec:ObjNI}›
subsubsection‹Indistinguishability relations›

text‹We have the usual two security types.›

datatype TP = low | high

text‹Global contexts assigns security types to program
variables and field names.›

consts CONTEXT :: "Var  TP"
consts GAMMA :: "Field  TP"

text‹Indistinguishability of values depends on a partial bijection
$\beta$.›

inductive_set twiddleVal::"(PBij × Val × Val) set"
where
twiddleVal_Null: "(β, RVal Nullref, RVal Nullref) : twiddleVal"

| twiddleVal_Loc: "(l1,l2) : β 
                 (β, RVal (Loc l1), RVal (Loc l2)) : twiddleVal"
| twiddleVal_IVal: "i1 = i2  (β, IVal i1, IVal i2) : twiddleVal"

text‹For stores, indistinguishability is as follows.›

definition twiddleStore::"PBij  Store  Store  bool"
where "twiddleStore β s1 s2 =
  ( x. CONTEXT x = low  (β, s1 x, s2 x) : twiddleVal)"

abbreviation twiddleStore_syntax  ("_  ≈⇩_ _" [100,100] 50)
  where "s ≈⇩β t == twiddleStore β s t"

text‹On objects, we require the values in low fields to be related,
and the sets of defined low fields to be equal.›

definition LowDom::"((Field × Val) list)  Field set"
where "LowDom F = {f .  v . lookup F f = Some v  GAMMA f = low}"

definition twiddleObj::"PBij  Object  Object  bool"
where "twiddleObj β o1 o2 = ((fst o1 = fst o2)  
                          LowDom (snd o1) = LowDom (snd o2) 
                         ( f v w . lookup (snd o1) f = Some v 
                                     lookup (snd o2) f = Some w 
                                     GAMMA f = low 
                                     (β, v, w) : twiddleVal))"

text‹On heaps, we require locations related by $\beta$ to contain
indistinguishable objects. Domain and codomain of the bijection
should be subsets of the domains of the heaps, of course.›

definition twiddleHeap::"PBij  Heap  Heap  bool"
where "twiddleHeap β h1 h2 = (β:Pbij 
                          Pbij_Dom β  Dom h1  
                          Pbij_Rng β  Dom h2 
                          ( l ll v w . (l,ll):β 
                                        lookup h1 l = Some v 
                                        lookup h2 ll = Some w 
                                        twiddleObj β v w))"

text‹We also define a predicate which expresses when a state does not
contain dangling pointers.›

(*The notion used in our paper:
definition noDPs::"State ⇒ bool"
where "noDPs S = (case S of (s,h) ⇒  ((∀ x l . s x = RVal(Loc l) ⟶ l:Dom h) ∧
                (∀ ll c F f l . lookup h ll = Some(c,F) ⟶
                               lookup F f = Some(RVal(Loc l))
                                 ⟶ l:Dom h)))"
*)

definition noLowDPs::"State  bool"
where "noLowDPs S = (case S of (s,h)  
   (( x l . CONTEXT x = low  s x = RVal(Loc l)  l:Dom h) 
    ( ll c F f l . lookup h ll = Some(c,F)  GAMMA f = low 
                    lookup F f = Some(RVal(Loc l))  l:Dom h)))"

text‹The motivation for introducing this notion stems from the
intended interpretation of the proof rule for skip, where the initial
and final states should be low equivalent. However, in the presence of
dangling pointers, indistinguishability does not hold as such a
dangling pointer is not in the expected bijection mkId›. In
contrast, for the notion of indistinguishability we use (see the
following definition), reflexivity indeed holds, as proven in lemma
twiddle_mkId› below. As a small improvement in comparison to
our paper, we now allow dangling pointers in high variables and high
fields since these are harmless.›

definition twiddle::"PBij  State  State  bool"
where "twiddle β s t = (noLowDPs s  noLowDPs t  
                 (fst s) ≈⇩β (fst t)  twiddleHeap β (snd s) (snd t))"

abbreviation twiddle_syntax  ("_ ≡⇩_ _" [100,100] 50)
  where "s ≡⇩β t == twiddle β s t"

text‹The following properties are easily proven by unfolding the
definitions.›

lemma twiddleHeap_isPbij:"twiddleHeap β h hh  β:Pbij"
(*<*)
by (simp add:twiddleHeap_def)
(*>*)

lemma isPBij:"s ≡⇩β t  β:Pbij"
(*<*)
apply (simp add: twiddle_def, clarsimp)
by (erule twiddleHeap_isPbij) 
(*>*)

lemma twiddleVal_inverse:
  "(β, w, v)  twiddleVal  (Pbij_inverse β, v, w)  twiddleVal"
(*<*)
apply (erule twiddleVal.cases) 
  apply clarsimp apply (rule twiddleVal_Null)
  apply clarsimp apply (rule twiddleVal_Loc) 
    apply (erule Pbij_inverseI) 
  apply clarsimp apply (rule twiddleVal_IVal) apply simp
done
(*>*)

lemma twiddleStore_inverse: "s ≈⇩β t  t ≈⇩(Pbij_inverse β) s"
(*<*)
apply (simp add: twiddleStore_def, clarsimp)
apply (rule twiddleVal_inverse) apply fast
done
(*>*)

lemma twiddleHeap_inverse:
  "twiddleHeap β s t  twiddleHeap (Pbij_inverse β) t s"
(*<*)
apply (simp add: twiddleHeap_def, clarsimp)
apply (rule, erule Pbij_inverse_Pbij)
apply (rule, simp add:  Pbij_inverse_Rng) 
apply (rule, simp add: Pbij_inverse_Dom)
apply clarsimp
  apply (erule_tac x=ll in allE, erule_tac x=l in allE, erule impE, erule Pbij_inverseD) 
  apply clarsimp
  apply (simp add: twiddleObj_def, clarsimp)
  apply (erule_tac x=f in allE, clarsimp)
  apply (erule twiddleVal_inverse)
done
(*>*)

lemma Pbij_inverse_twiddle: "s ≡⇩β t  t ≡⇩(Pbij_inverse β) s"
(*<*)
apply (simp add: twiddle_def, clarsimp)
apply (rule, erule twiddleStore_inverse)
apply (erule twiddleHeap_inverse)
done
(*>*)

lemma twiddleVal_betaExtend[rule_format]:
  "(β,v,w):twiddleVal   γ. Pbij_extends γ β  (γ,v,w):twiddleVal"
(*<*)
apply (erule twiddleVal.induct)
apply clarsimp apply (rule twiddleVal_Null)
apply clarsimp apply (rule twiddleVal_Loc) apply (simp add: Pbij_extends_def) apply fast
apply clarsimp apply (rule twiddleVal_IVal) apply simp
done
(*>*)

lemma twiddleObj_betaExtend[rule_format]:
  "twiddleObj β o1 o2; Pbij_extends γ β  twiddleObj γ o1 o2"
(*<*)
apply (simp add: twiddleObj_def, clarsimp)
apply (erule_tac x=f in allE, erule_tac x=v in allE, clarsimp)
apply (erule twiddleVal_betaExtend) apply assumption 
done
(*>*)

lemma twiddleVal_compose:
  "(β, v, u)  twiddleVal; (γ, u, w)  twiddleVal 
    (Pbij_compose β γ, v, w)  twiddleVal"
(*<*)
apply (erule twiddleVal.cases)
  apply clarsimp
    apply (erule twiddleVal.cases)
    apply clarsimp apply (rule twiddleVal_Null)
    apply clarsimp 
    apply clarsimp
  apply clarsimp
    apply (erule twiddleVal.cases)
    apply clarsimp 
    apply clarsimp apply (rule twiddleVal_Loc) apply (erule Pbij_composeI, assumption)
    apply clarsimp 
  apply clarsimp
    apply (erule twiddleVal.cases)
    apply clarsimp 
    apply clarsimp 
    apply clarsimp apply (rule twiddleVal_IVal) apply simp
done
(*>*)

lemma twiddleHeap_compose: 
  " twiddleHeap β h1 h2; twiddleHeap γ h2 h3; β  Pbij; γ  Pbij
    twiddleHeap (Pbij_compose β γ) h1 h3"
(*<*)
apply (simp add: twiddleHeap_def)
apply rule apply (erule Pbij_compose_Pbij) apply assumption
apply rule apply (subgoal_tac "Pbij_Dom (Pbij_compose β γ)  Pbij_Dom β", fast) apply (rule Pbij_compose_Dom)
apply rule apply (subgoal_tac "Pbij_Rng (Pbij_compose β γ)  Pbij_Rng γ", fast) apply (rule Pbij_compose_Rng)
apply (erule conjE)+
apply (rule, rule, rule)
apply (subgoal_tac " l1 . (l,l1) : β  (l1,ll):γ", erule exE, erule conjE)
prefer 2 apply (simp add: Pbij_compose_def)
apply (subgoal_tac " x y . lookup h2 l1 = Some(x,y)", (erule exE)+)
prefer 2 apply (subgoal_tac "l1 : Dom h2", simp add: Dom_def)
         apply (simp add:Pbij_compose_def Pbij_Dom_def) apply clarsimp apply fast
apply (rule, rule, rule)
apply (rule, rule, rule)
apply (erule_tac x=l in allE, erule_tac x=l1 in allE, erule impE, assumption)
apply (erule_tac x=l1 in allE, erule_tac x=ll in allE, erule impE, assumption)
apply (erule_tac x=a in allE, erule_tac x=b in allE, erule impE, assumption)
apply (erule_tac x=x in allE, erule_tac x=y in allE, erule impE, assumption)
apply (erule_tac x=aa in allE, erule_tac x=ba in allE, erule impE, assumption)
apply (erule_tac x=x in allE, erule_tac x=y in allE, erule impE, assumption)
apply (simp add: twiddleObj_def)
apply clarsimp
  apply (subgoal_tac " u . lookup y f = Some u", erule exE)
  prefer 2 apply (simp add: LowDom_def) apply (rotate_tac -6) apply (erule thin_rl, erule thin_rl) apply (erule thin_rl) apply fast
  apply (erule_tac x=f in allE, erule_tac x=u in allE, clarsimp)
  apply (erule_tac x=f in allE, erule_tac x=v in allE, clarsimp)
  apply (erule twiddleVal_compose) apply assumption
done
(*>*)

lemma twiddleStore_compose:
  "s ≈⇩β r; r≈⇩γ t  s ≈⇩(Pbij_compose β γ) t"
(*<*)
apply (simp add:twiddleStore_def)
  apply clarsimp apply (erule_tac x=x in allE, clarsimp)+
  apply (erule twiddleVal_compose) apply assumption 
done
(*>*)

lemma twiddle_compose:
  "s ≡⇩β r; r ≡⇩γ t  s ≡⇩(Pbij_compose β γ) t"
(*<*)
apply (simp add: twiddle_def)
apply (erule conjE)+
apply rule apply (erule twiddleStore_compose) apply assumption
apply (rule twiddleHeap_compose) apply assumption+
apply (simp add: twiddleHeap_def)
apply (simp add: twiddleHeap_def)
done
(*>*)

lemma twiddle_mkId: "noLowDPs (s,h)  (s,h) ≡⇩(mkId h) (s,h)"
(*<*)
apply (simp add: twiddle_def)
apply rule
  apply (simp add: twiddleStore_def)
    apply (rule, rule) 
    apply (case_tac "s x")
    apply (rename_tac Var Ref)
    apply clarsimp apply (case_tac Ref) 
      apply clarsimp apply (rule twiddleVal_Null) 
      apply clarsimp apply (rule twiddleVal_Loc) apply (rule mkId4) apply (simp add: noLowDPs_def)
      apply clarsimp apply (simp add: twiddleVal_IVal)
(*twiddleHeap*)
  apply (simp add: twiddleHeap_def) 
  apply (rule, rule mkId1)
  apply (rule, simp add: mkId2) 
  apply (rule, simp add: mkId2b Dom_def) 
  apply clarsimp 
      apply (simp add: twiddleObj_def) apply (drule mkId4b) apply clarsimp
        apply (case_tac v, clarsimp)
        apply (rename_tac Ref)
        apply (case_tac Ref, clarsimp)
        apply (rule twiddleVal_Null)
        apply clarsimp apply (rule twiddleVal_Loc) apply (rule mkId4) apply (simp add: noLowDPs_def) 
        apply clarsimp apply (rule twiddleVal_IVal) apply simp
done(*>*)


text‹We call expressions (semantically) low if the following
predicate is satisfied. In particular, this means that if $e$
evaluates in $s$ (respecitvely, $t$) to some location $l$, then $l
\in Pbij\_dom(\beta)$ ($l \in Pbij\_cod(\beta)$) holds.›

definition Expr_low::"Expr  bool"
where "Expr_low e = ( s t β. s ≈⇩β t  (β, evalE e s, evalE e t):twiddleVal)"

text‹A similar notion is defined for boolean expressions, but the
fact that these evaluate to (meta-logical) boolean values allows us to
replace indistinguishability by equality.›

definition BExpr_low::"BExpr  bool"
where "BExpr_low b = ( s t β . s ≈⇩β t  evalB b s = evalB b t)"

subsubsection‹Definition and characterisation of security›

text‹Now, the notion of security, as defined in the paper. Banerjee
and Naumann's paper~cite"DBLP:journals/jfp/BanerjeeN05" and the
Mobius Deliverable 2.3~cite"MobiusDeliverable2.3" contain similar
notions.›

definition secure::"OBJ  bool"
where "secure c = ( s ss t tt β . 
               s ≡⇩β ss  (s,c  t)  (ss,c  tt) 
               ( γ . t ≡⇩γ tt  Pbij_extends γ β))"

(*<*)
lemma Skip1: "secure Skip"
apply (simp only: secure_def Sem_def twiddle_def)
apply (rule, rule, rule, rule, rule, rule)
apply (rule, rule, erule exE, erule exE)
apply (erule Sem_eval_cases)
apply (erule Sem_eval_cases)
apply (rule_tac x=β in exI)
apply simp
apply (rule Pbij_extends_reflexive)
done

lemma AssignAux:
  " Expr_low e; s ≡⇩β t 
   (update (fst s) x (evalE e (fst s)), snd s) ≡⇩β
      (update (fst t) x (evalE e (fst t)), snd t)"
apply (simp only: twiddle_def Expr_low_def)
apply rule apply (simp add: noLowDPs_def) 
  apply (case_tac s, clarsimp, hypsubst_thin) apply (rename_tac s h y t k l)
  apply (case_tac "x=y", clarsimp) apply (simp add: update_def) 
    apply (erule_tac x=s in allE)
    apply (erule_tac x=t in allE, clarsimp)
    apply (erule_tac x=β in allE, erule impE, assumption)
    apply (erule twiddleVal.cases, clarsimp) prefer 2 apply clarsimp apply clarsimp
    apply (simp add: twiddleHeap_def) apply (simp add: Pbij_Dom_def) apply fast
  apply (simp add: update_def)
apply rule apply (simp add: noLowDPs_def)
  apply (case_tac s, clarsimp, hypsubst_thin) apply (rename_tac s h t k y l) 
  apply (case_tac "x=y", clarsimp) apply (simp add: update_def) 
    apply (erule_tac x=s in allE)
    apply (erule_tac x=t in allE)
    apply (erule_tac x=β in allE, clarsimp)
    apply (erule twiddleVal.cases, clarsimp) prefer 2 apply clarsimp apply clarsimp
    apply (simp add: twiddleHeap_def) apply (simp add: Pbij_Rng_def) apply fast
  apply (simp add: update_def)
apply rule
prefer 2 apply simp
apply (unfold twiddleStore_def)
  apply (rule, rule)
  apply (case_tac "x=xa", clarsimp)
    apply (erule_tac x="fst s" in allE)
    apply (erule_tac x="fst t" in allE)
    apply (erule_tac x=β in allE, clarsimp)
    apply (simp add: update_def)
  apply (simp add: update_def)
done

lemma Assign1: 
  "Expr_low e  secure (Assign x e)"
apply (simp only: secure_def Sem_def)
apply (rule, rule, rule, rule, rule, rule)
apply (rule, rule, erule exE, erule exE)
apply (erule Sem_eval_cases)
apply (erule Sem_eval_cases)
apply (rule_tac x=β in exI)
apply simp
apply rule
apply (rule AssignAux) apply fastforce apply assumption
apply (rule Pbij_extends_reflexive)
done

lemma Comp1: "secure c1; secure c2  secure (Comp c1 c2)"
apply (simp only: secure_def Sem_def)
apply (rule, rule, rule, rule, rule, rule)
apply (rule, rule)
apply (erule exE, erule exE)
apply (erule Sem_eval_cases, erule Sem_eval_cases)
apply (erule_tac x=s in allE, rotate_tac -1)
apply (erule_tac x=ss in allE, rotate_tac -1)
apply (erule_tac x=r in allE, rotate_tac -1)
apply (erule_tac x=ra in allE, rotate_tac -1)
apply (erule_tac x=β in allE, rotate_tac -1)
apply (erule impE, assumption)
apply (erule impE, rule, assumption)
apply (erule impE, rule, assumption)
apply (erule exE, erule conjE)
apply (erule_tac x=r in allE, rotate_tac -1)
apply (erule_tac x=ra in allE, rotate_tac -1)
apply (erule_tac x=t in allE, rotate_tac -1)
apply (erule_tac x=tt in allE, rotate_tac -1)
apply (erule_tac x=γ in allE, rotate_tac -1)
apply (erule impE, assumption)
apply (erule impE, rule, assumption)
apply (erule impE, rule, assumption)
apply (erule exE, erule conjE)
apply (rule_tac x=γ' in exI, simp)
apply (rule Pbij_extends_transitive)
apply (assumption, assumption)
done

lemma Iff1:
  "BExpr_low b; secure c1; secure c2  secure (Iff b c1 c2)"
apply (simp only: secure_def Sem_def BExpr_low_def)
apply (rule, rule, rule, rule, rule, rule)
apply (rule, rule)
apply (erule exE, erule exE)
apply (erule Sem_eval_cases, erule Sem_eval_cases)
apply (rotate_tac 2, erule thin_rl)
apply (erule_tac x=s in allE, rotate_tac -1)
apply (erule_tac x=ss in allE, rotate_tac -1)
apply (erule_tac x=t in allE, rotate_tac -1)
apply (erule_tac x=tt in allE, rotate_tac -1)
apply (erule_tac x=β in allE, clarsimp)
apply (erule impE, rule, assumption)
apply (erule impE, rule, assumption)
apply assumption
apply (erule_tac x="fst s" in allE, erule thin_rl, erule thin_rl)
apply (erule_tac x="fst ss" in allE)
apply (erule_tac x=β in allE, erule impE, simp add: twiddle_def)
apply simp
apply (erule Sem_eval_cases)
apply (erule_tac x="fst s" in allE, erule thin_rl, erule thin_rl)
apply (erule_tac x="fst ss" in allE)
apply (erule_tac x=β in allE, erule impE, simp add: twiddle_def)
apply simp
apply (erule thin_rl, erule thin_rl)
apply (erule_tac x=s in allE, rotate_tac -1)
apply (erule_tac x=ss in allE, rotate_tac -1)
apply (erule_tac x=t in allE, rotate_tac -1)
apply (erule_tac x=tt in allE, rotate_tac -1)
apply (erule_tac x=β in allE, rotate_tac -1)
apply (erule impE, assumption)
apply (erule impE, rule, assumption)
apply (erule impE, rule, assumption)
apply assumption
done
(*>*)

text‹The type of invariants $\Phi$ includes a component that holds a
partial bijection.›

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

text‹The operator constructing an assertion from an invariant.›

definition Sec :: "TT  Assn"
where "Sec Φ s t =
   (( r β. s ≡⇩β r  Φ(t,r,β)) 
    ( r β . Φ (r,s,β)  ( γ . r ≡⇩γ t  Pbij_extends γ β)))"

text‹The lemmas proving that the operator ensures security, and that
secure programs satisfy an assertion formed by the operator, are
proven in a similar way as in Section \ref{sec:BaseLineNI}.›

lemma Prop1A:" c : Sec Φ  secure c"
(*<*)
apply (simp only: VDM_valid_def secure_def Sec_def) 
apply (rule, rule, rule, rule)
apply (rule, rule, rule, rule)
apply (subgoal_tac "(r β. s ≡⇩β r  Φ(t, r, β)) 
              (r β. Φ(r, s, β)  (γ. r ≡⇩γ t  Pbij_extends γ β))")
prefer 2 apply fast
apply (erule_tac x=ss in allE, erule_tac x=tt in allE, erule impE, assumption)
apply clarsimp
done
(*>*)

lemma Prop1B:
 "secure c   c : Sec (λ (r, t, β).  s. s , c  r  s ≡⇩β t)"
(*<*)
apply (simp only: VDM_valid_def Sec_def)
apply (rule, rule) apply (rule, rule)
apply (rule, rule, rule)
  apply simp
  apply (case_tac s, clarsimp)
  apply (rule_tac x=ac in exI, rule_tac x=bc in exI, simp)
apply (rule, rule)
  apply (rule)
  apply simp
  apply ((erule exE)+, (erule conjE)+) 
  apply (unfold secure_def)
  apply (erule_tac x="(a,b)" in allE, erule_tac x=s in allE)
  apply (erule_tac x=r in allE, erule_tac x=t in allE)
  apply (erule_tac x=β in allE)
  apply (erule impE, assumption)+
  apply (erule exE, erule conjE)
  apply (rule_tac x=γ in exI, simp)
(*  apply (rule Pbij_extends_RCompl)*)
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 proof rules›
text‹\label{sec:ObjDerivedRules}›
subsubsection‹Low proof rules›
(*<*)
lemma SkipSem: " Skip : Sec (λ (s, t, β) . s ≡⇩β t)"
apply (simp only: VDM_valid_def Sec_def Sem_def)
apply (rule, rule, rule)
apply (erule exE)
apply (erule Sem_eval_cases)
apply rule
  apply simp
apply (rule, rule, rule)
  apply (rule_tac x=β in exI, simp)
  apply (rule Pbij_extends_reflexive)
done
(*>*)

lemma SKIP: "G  Skip : Sec (λ (s, t, β) . s ≡⇩β t)"
(*<*)
apply (rule VDMConseq, rule VDMSkip)
apply (simp only: Sec_def)
apply (rule, rule, rule)
apply rule
  apply simp
apply (rule, rule, rule)
  apply (rule_tac x=β in exI,simp)
  apply (rule Pbij_extends_reflexive)
done
(*>*)

lemma ASSIGN:
  "Expr_low e
   G  Assign x e : Sec (λ (s, t, β) .
           r . s = (update (fst r) x (evalE e (fst r)), snd r)
                 r ≡⇩β t)"
(*<*)
apply (rule VDMConseq, rule VDMAssign)
apply (simp only: Sec_def Expr_low_def)
apply (rule, rule, rule)
apply rule
apply (rule, rule, rule)
  apply simp
  apply (erule_tac x="fst s" in allE, erule_tac x="fst r" in allE, erule_tac x=β in allE, erule impE)
    apply (simp add: twiddle_def)
  apply (simp add: twiddle_def)
  apply (simp add: twiddleStore_def)
  apply (erule conjE)
  apply (rule_tac x="fst s" in exI, simp)
apply (rule, rule, rule)
  apply simp
  apply (erule exE)+
  apply (erule conjE)+
  apply (rule_tac x=β in exI)
  apply rule prefer 2 apply (rule Pbij_extends_reflexive)
  apply clarsimp
    apply (simp add: twiddle_def)
    apply (simp add: twiddleStore_def)
    apply clarsimp
    apply (case_tac "xa=x")
      apply (simp add: update_def noLowDPs_def) 
      apply (rule, clarsimp) apply (erule_tac x=ac in allE, erule_tac x=a in allE, erule_tac x=β in allE, erule impE, assumption)
        apply (erule twiddleVal.cases, clarsimp) 
          apply (simp add: twiddleHeap_def  Pbij_Dom_def, clarsimp) apply fast
        apply clarsimp
      apply clarsimp  apply (erule_tac x=ac in allE, erule_tac x=a in allE, erule_tac x=β in allE, erule impE, assumption)
        apply (erule twiddleVal.cases, clarsimp) 
          apply (simp add: twiddleHeap_def  Pbij_Rng_def, clarsimp) apply fast
        apply clarsimp
    apply (simp add: update_def noLowDPs_def) 
      apply (rule, clarsimp) apply (erule_tac x=ac in allE, erule_tac x=a in allE, erule_tac x=β in allE, erule impE, assumption)
        apply (erule twiddleVal.cases, clarsimp) 
          apply (simp add: twiddleHeap_def  Pbij_Dom_def, clarsimp) apply fast
        apply clarsimp
      apply clarsimp  apply (erule_tac x=ac in allE, erule_tac x=a in allE, erule_tac x=β in allE, erule impE, assumption)
        apply (erule twiddleVal.cases, clarsimp) 
          apply (simp add: twiddleHeap_def  Pbij_Rng_def, clarsimp) apply fast
        apply clarsimp
done
(*>*)

(*<*)
lemma CompSem: 
  "  c1 : Sec Φ;  c2 : Sec Ψ 
    (Comp c1 c2) : Sec (λ (s, t, β) .  r . Φ(r, t, β)  
                                      ( w γ. r ≡⇩γ w  Ψ(s, w, γ)))"
apply (simp only: VDM_valid_def Sec_def Sem_def)
apply (rule, rule, rule)
apply (erule exE)
apply (erule Sem_eval_cases)
apply (erule_tac x=s in allE, rotate_tac -1)
apply (erule_tac x=r in allE, rotate_tac -1)
apply (erule impE, rule, assumption)
apply (erule_tac x=r in allE, rotate_tac -1)
apply (erule_tac x=t in allE, rotate_tac -1)
apply (erule impE, rule, assumption)
apply (erule thin_rl, erule thin_rl)
apply (erule conjE)+
apply rule
  apply (rule, rule, rule)
  apply (erule_tac x=ra in allE, rotate_tac -1)
  apply (erule_tac x=β in allE, rotate_tac -1)
  apply (erule impE, assumption)
  apply simp
  apply (case_tac r, clarsimp)
  apply (rule_tac x=ad in exI, rule_tac x=bd in exI, simp)
apply (rule, rule, rule)
  apply simp
  apply (erule exE)+ apply (erule conjE)+
  apply (rotate_tac 2, erule_tac x=a in allE)
  apply (rotate_tac -1, erule_tac x=b in allE)
  apply (rotate_tac -1, erule_tac x=β in allE)
  apply (rotate_tac -1, erule impE, assumption)
  apply (erule exE, erule conjE)
  apply (case_tac r, clarsimp)
  apply (rotate_tac 3, erule_tac x=aaa in allE)
  apply (rotate_tac -1, erule_tac x=baa in allE)
  apply (rotate_tac -1, erule_tac x=γ in allE)
  apply (erule impE, assumption)
  apply (rotate_tac 5, erule_tac x=ac in allE)
  apply (rotate_tac -1, erule_tac x=bc in allE)
  apply (rotate_tac -1, erule_tac x=γ in allE)
  apply (erule impE, assumption)
  apply (erule exE)
  apply (erule conjE)
  apply (rule_tac x=γ' in exI, rule, assumption)
apply (erule Pbij_extends_transitive) apply assumption
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, rule VDMComp)
apply (assumption, assumption)
apply (simp only: Sec_def)
apply (rule, rule, rule)
apply (erule exE)
apply (erule conjE)+
apply (erule thin_rl, erule thin_rl)
apply rule
  apply (rule, rule, rule)
  apply simp
  apply (case_tac ra, clarsimp)
  apply (erule_tac x=ad in allE, rotate_tac -1)
  apply (erule_tac x=bd in allE, rotate_tac -1)
  apply (erule_tac x=β in allE, rotate_tac -1)
  apply (erule impE, assumption)
  apply (rule_tac x=ab in exI, rule_tac x=bb in exI, simp)
apply (rule, rule, rule)
  apply simp
  apply (erule exE)+ apply (erule conjE)+
  apply (rotate_tac 1, erule_tac x=a in allE)
  apply (rotate_tac -1, erule_tac x=b in allE)
  apply (rotate_tac -1, erule_tac x=β in allE)
  apply (rotate_tac -1, erule impE, assumption)
  apply (erule exE, erule conjE)
  apply (case_tac r, clarsimp)
  apply (rotate_tac 3, erule_tac x=aaa in allE)
  apply (rotate_tac -1, erule_tac x=baa in allE)
  apply (rotate_tac -1, erule_tac x=γ in allE)
  apply (erule impE, assumption)
  apply (rotate_tac 4, erule_tac x=ac in allE)
  apply (rotate_tac -1, erule_tac x=bc in allE)
  apply (rotate_tac -1, erule_tac x=γ in allE)
  apply (erule impE, assumption)
  apply (erule exE)
  apply (erule conjE)
  apply (rule_tac x=γ' in exI, rule, assumption)
apply (erule Pbij_extends_transitive) apply assumption
done(*>*)

(*<*)
lemma IffSem: 
  " BExpr_low b;  c1 : Sec Φ;  c2 : Sec Ψ 
    (Iff b c1 c2) : (Sec (λ (s, t, β) .
                       (evalB b (fst t)  Φ(s,t, β))  
                       ((¬ evalB b (fst t))  Ψ(s,t,β))))"
apply (simp only: VDM_valid_def Sec_def Sem_def BExpr_low_def)
apply (rule, rule, rule)
apply (erule exE)
apply (erule Sem_eval_cases)
apply rule
  apply (rule, rule, rule)
  apply simp
  apply (erule_tac x="fst s" in allE, rotate_tac -1)
  apply (erule_tac x="fst r" in allE, rotate_tac -1)
  apply (erule impE, rule_tac x=β in exI, simp add: twiddle_def)
  apply (case_tac s, clarsimp)
  apply (erule_tac x=ac in allE, rotate_tac -1)
  apply (erule_tac x=bc in allE, rotate_tac -1)
  apply (erule_tac x=aa in allE, rotate_tac -1)
  apply (erule_tac x=ba in allE, rotate_tac -1)
  apply (erule impE, rule, assumption)
(*  apply (simp add: twiddle_def)*)
  apply clarsimp
  apply (rule, rule, rule)
  apply simp
  apply (case_tac s, clarsimp)
  apply (rotate_tac 1)
  apply (erule_tac x=ac in allE, rotate_tac -1)
  apply (erule_tac x=bc in allE, rotate_tac -1)
  apply (erule_tac x=aa in allE, rotate_tac -1)
  apply (erule_tac x=ba in allE, rotate_tac -1)
  apply (erule impE, rule, assumption)
  apply clarsimp
apply rule
  apply (rule, rule, rule, rule)
  apply simp
  apply (case_tac s, clarsimp)
  apply (erule_tac x=ac in allE, rotate_tac -1)
  apply (erule_tac x=ab in allE, rotate_tac -1)
  apply (erule impE) apply(rule_tac x=β in exI, simp add: twiddle_def)
  apply clarsimp apply (erule thin_rl, erule_tac x=ac in allE)
                 apply (erule_tac x=bc in allE, erule_tac x=aa in allE, erule_tac x=ba in allE, erule impE)
                   apply (rule, assumption)
                apply clarsimp
  apply clarsimp apply (erule thin_rl, erule thin_rl, erule_tac x=a in allE)
                 apply (erule_tac x=ba in allE, erule_tac x=aa in allE, erule_tac x=baa in allE, erule impE)
                   apply (rule, assumption)
                apply clarsimp
done
(*>*)

lemma IFF:
  " BExpr_low b; G  c1 : Sec Φ; G  c2 : Sec Ψ 
  G  (Iff b c1 c2) : Sec (λ (s,t,β) .
                         (evalB b (fst t)  Φ(s,t,β))  
                         ((¬ evalB b (fst t))  Ψ(s,t,β)))"
(*<*)
apply (rule VDMConseq, rule VDMIff) 
apply (assumption, assumption)
apply (simp only: Sec_def BExpr_low_def)
apply (rule, rule, rule)
apply (rule, rule, rule, rule)
  apply (erule_tac x="fst s" in allE, rotate_tac -1)
  apply (erule_tac x="fst r" in allE, rotate_tac -1)
  apply (erule_tac x=β in allE, rotate_tac -1)
  apply (simp add: twiddle_def)
  apply clarsimp
apply (rule, rule, rule)
  apply (case_tac "evalB b (fst s)")
  apply clarsimp
  apply clarsimp
done
(*>*)

(*<*)
lemma noLowDPs_NEW:
  "noLowDPs (s,h)  noLowDPs (update s x (RVal (Loc l)), (l, C, []) # h)"
apply (simp add: noLowDPs_def update_def, clarsimp)
apply (rule, clarsimp)
  apply (rule, clarsimp) apply (simp add: Dom_def)
  apply clarsimp apply (simp add: Dom_def)
apply clarsimp apply (erule_tac x=ll in allE, clarsimp) apply (simp add: Dom_def)
done
(*>*)

lemma NEW:
  "CONTEXT x = low
   G  (New x C) : Sec (λ (s,t,β) . 
                  l r . l  Dom (snd r)  r ≡⇩β t  
                         s = (update (fst r) x (RVal (Loc l)), 
                                 (l,(C,[])) # (snd r)))"
(*<*)
apply (rule VDMConseq, rule VDMNew)
apply (simp only: Sec_def)
apply (rule, rule, rule)
apply (erule exE, (erule conjE)+)
apply rule
(*First part of Sec*)
apply (rule, rule, rule)
  apply simp
  apply (rule, rule, assumption)
  apply (rule_tac x="fst s" in exI, simp)
(*Second part of Sec*)
apply (rule, rule, rule)
  apply simp
  apply (erule exE)+
  apply (erule conjE)+
  apply (rule_tac x="insert (la,l) β" in exI)

  apply rule 
  (*Show twiddle*)
    apply (frule isPBij)
    apply (simp add: twiddle_def, clarsimp)
    apply rule apply (erule noLowDPs_NEW)
    apply rule apply (erule noLowDPs_NEW) 
    (*twiddleStore*)
    apply (simp add: twiddleStore_def)
      apply (rule, rule)
        apply (case_tac "x=xa")
        apply (simp add: update_def) apply clarsimp 
          apply (rule twiddleVal_Loc) apply simp
        apply (simp add: update_def) apply clarsimp
         apply (erule_tac x=xa in allE, clarsimp)
         apply (rule twiddleVal_betaExtend, assumption) apply (simp add: Pbij_extends_def) apply fast
    (*twiddleHeap*)     
    apply (simp add: twiddleHeap_def) apply clarsimp
      apply rule apply (erule Pbij_insert) apply fast apply fast 
      apply (rule, simp add: Pbij_Dom_def Dom_def) apply fast 
      apply (rule, simp add: Pbij_Rng_def Dom_def) apply fast
      apply (rule, rule)
        apply clarsimp
        apply (rule, clarsimp)
          apply (rule, clarsimp) apply (simp add: twiddleObj_def)
          apply clarsimp apply (simp add: twiddleObj_def)
        apply clarsimp apply (simp add: Pbij_Dom_def) apply fast 
      apply clarsimp
        apply (rule, clarsimp) apply (simp add: Pbij_Rng_def) apply fast 
      apply clarsimp
          apply (erule_tac x=lb in allE, erule_tac x=ll in allE, clarsimp)
          apply (rule twiddleObj_betaExtend) apply assumption+ apply (simp add: Pbij_extends_def) apply fast
  (*Pbij_extends*)
    apply (simp add: Pbij_extends_def) apply fast 
done
(*>*)

lemma GET: 
  " CONTEXT y = low; GAMMA f = low
   G  Get x y f : Sec (λ (s,t,β) .
                r l C Flds v. (fst r) y = RVal(Loc l)  
                               lookup (snd r) l = Some(C,Flds)  
                               lookup Flds f = Some v  r ≡⇩β t  
                               s = (update (fst r) x v, snd r))"
(*<*)
apply (rule VDMConseq, rule VDMGet)
apply (simp only: Sec_def)
apply (rule, rule, rule)
apply (erule exE)+
apply (erule conjE)+
apply rule
  apply (rule, rule, rule)
  apply simp
  apply (rule, rule, rule)
  apply (rule, assumption)
  apply (rule, rule, rule, assumption)
  apply (rule, rule, assumption)
  apply simp
apply (rule, rule, rule)
  apply simp
  apply (erule exE)+
  apply (erule conjE)+
  apply (erule exE)+
  apply (erule conjE)+
  apply (erule exE)+
  apply (erule conjE)+
  apply (rule_tac x=β in exI, rule)
  prefer 2 apply (rule Pbij_extends_reflexive)
  apply (simp add: twiddle_def, (erule conjE)+)
    apply (rule, simp add: noLowDPs_def update_def, clarsimp)
    apply (rule, simp add: noLowDPs_def update_def)
    apply (simp add: twiddleStore_def) apply clarsimp
    apply (case_tac "x=xa", clarsimp) prefer 2  apply (simp add: update_def)
    apply (simp add:update_def) apply (simp add: twiddleHeap_def) apply clarsimp
    apply (erule_tac x=y in allE, clarsimp)
    apply (erule twiddleVal.cases)
    apply clarsimp
    prefer 2 apply clarsimp
    apply clarsimp
      apply (erule_tac x=l1 in allE) 
      apply (erule_tac x=l2 in allE, clarsimp) 
      apply (simp add: twiddleObj_def)
done
(*>*)

lemma PUT: 
  " CONTEXT x = low; GAMMA f = low; Expr_low e
   G  Put x f e: Sec (λ (s,t,β) .
            r l C Flds. (fst r) x = RVal(Loc l)  r ≡⇩β t 
                         lookup (snd r) l = Some(C,Flds)  
                         s = (fst r, 
                              (l,(C,(f,evalE e (fst r)) # Flds)) # (snd r)))"
(*<*)
apply (rule VDMConseq, rule VDMPut)
apply (simp only: Sec_def Expr_low_def)
apply (rule, rule, rule)
apply (erule exE)+
apply (erule conjE)+
apply rule
  apply (rule, rule, rule)
  apply simp
apply (rule, rule, rule)
  apply simp
  apply (erule exE)+
  apply (erule conjE)+
  apply (erule exE)+
  apply (erule conjE)+
  apply (rule_tac x=β in exI, rule)
  prefer 2 apply (rule Pbij_extends_reflexive)
  apply (simp add: twiddle_def)
  apply (simp add: twiddleStore_def)
  apply (simp add: twiddleHeap_def)
  apply clarsimp
  apply (rule, rotate_tac -1, erule thin_rl, simp add: noLowDPs_def) 
    apply (rule, clarsimp) apply (subgoal_tac "lb : Dom bc", simp add: Dom_def) 
      apply (erule_tac x=xa in allE, erule impE, assumption,
             erule_tac x=lb in allE, erule mp, assumption) 
    apply clarsimp apply (rule, clarsimp)
                     apply (rule, clarsimp) 
                       apply (erule_tac x=ac in allE, erule_tac x=a in allE, erule_tac x=β in allE, erule impE, assumption) 
                       apply (erule twiddleVal.cases, clarsimp) 
                         apply clarsimp apply (subgoal_tac "la : Dom bc", simp add: Dom_def) 
                                        apply (simp add: Pbij_Dom_def) apply fast
                         apply clarsimp
                     apply clarsimp apply (erule_tac x=ll in allE, clarsimp)
                                    apply (erule_tac x=fa in allE, clarsimp) apply (simp add: Dom_def)
                   apply clarsimp apply (erule_tac x=ll in allE, clarsimp)
                                    apply (erule_tac x=fa in allE, clarsimp) apply (simp add: Dom_def)
  apply (rule, rotate_tac -1, erule thin_rl, simp add: noLowDPs_def) 
    apply (rule, clarsimp) apply (subgoal_tac "lb : Dom b", simp add: Dom_def) 
      apply (erule_tac x=xa in allE, erule impE, assumption,
             erule_tac x=lb in allE, erule mp, assumption) 
    apply clarsimp apply (rule, clarsimp)
                     apply (rule, clarsimp) 
                       apply (erule_tac x=ac in allE, erule_tac x=a in allE, erule_tac x=β in allE, erule impE, assumption) 
                       apply (erule twiddleVal.cases, clarsimp) 
                         apply clarsimp apply (subgoal_tac "l : Dom b", simp add: Dom_def) 
                                        apply (simp add: Pbij_Rng_def) apply fast
                         apply clarsimp
                     apply clarsimp apply (erule_tac x=ll in allE, clarsimp)
                                    apply (erule_tac x=fa in allE, clarsimp) apply (simp add: Dom_def)
                   apply clarsimp apply (erule_tac x=ll in allE, clarsimp)
                                    apply (erule_tac x=fa in allE, clarsimp) apply (simp add: Dom_def)
  apply (rule, rotate_tac -1, erule thin_rl, simp add: Dom_def) apply fast
  apply (rule, rotate_tac -1, erule thin_rl, simp add: Dom_def) apply fast
  apply clarsimp
  apply (rule, rule, rule)
  apply rule apply clarsimp
             apply (erule_tac x=lb in allE, rotate_tac -1)
             apply (erule_tac x=ll in allE, rotate_tac -1, clarsimp)
             apply (erule_tac x=ac in allE, erule_tac x=a in allE, erule_tac x=β in allE, erule impE, assumption)
             apply (simp add: twiddleObj_def, clarsimp)
             apply (simp add: LowDom_def) apply (rotate_tac -1, erule thin_rl) 
             apply rule apply (rule, clarsimp) apply fast
               apply (rule, clarsimp) apply fast
             apply clarsimp apply (erule_tac x=x in allE, clarsimp)
               apply (erule twiddleVal.cases)
               apply clarsimp 
               apply clarsimp apply (simp add: Pbij_def) apply fast
               apply clarsimp
  apply clarsimp apply (erule_tac x=x in allE, clarsimp)
               apply (erule twiddleVal.cases)
               apply clarsimp 
               apply clarsimp apply (simp add: Pbij_def) 
               apply clarsimp
done
(*>*)

text‹Again, we define a fixed point operator over invariants.›

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 (unfold FIX_def)
apply (rule, rule)
apply (rule, rule) 
apply (subgoal_tac "φ Φ (s,t,β)") apply fast 
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 (unfold FIX_def) apply fast 
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 transformers, 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‹The operator used in the while rule is defined by›

definition PhiWhileOp::"BExpr  TT  TT  TT"
where "PhiWhileOp b Φ = (λ Ψ . (λ (s, t, β).
  (evalB b (fst t) 
      ( r. Φ (r, t, β)  ( w γ. r ≡⇩γ w  Ψ(s, w, γ)))) 
  (¬ evalB b (fst t)  s≡⇩β t)))"

text‹and is monotone:›

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

text‹Hence, we can define its fixed point:›

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

text‹The while rule may now be given as follows:›

lemma WHILE:  
  " BExpr_low b; 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 (fst t)  Sec (PhiWhile b Φ) s t", assumption)
prefer 2 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 clarsimp apply (simp add: Sec_def) 
  apply (rule, clarsimp) apply (simp add: PhiWhileOp_def  BExpr_low_def) 
    apply clarsimp apply (simp add: twiddle_def) apply (erule_tac x=a in allE, erule_tac x=aa in allE, clarsimp) 
  apply clarsimp apply (simp add: PhiWhileOp_def)
    apply (rule_tac x=β in exI, simp) apply (rule Pbij_extends_reflexive)

apply clarsimp apply (simp add: Sec_def)
  apply rule
  prefer 2 apply clarsimp
    apply (subgoal_tac " r1 r2 γ . Φ ((r1,r2), (a,ba),γ)  Pbij_extends γ β 
                                  ( w1 w2 γ . (r1,r2) ≡⇩γ (w1,w2)  
                                                   (PhiWhile b Φ) ((ac,bc), (w1,w2),γ))")
    prefer 2 apply (simp add: PhiWhileOp_def) 
      apply (erule exE)+ apply (erule conjE)+ apply (rule_tac x=ad in exI, rule_tac x=bd in exI, rule)
      apply (rule, assumption)
      apply (rule, rule Pbij_extends_reflexive)
      apply assumption
    apply (erule exE)+ apply (erule conjE)+
    apply (rotate_tac 4, erule_tac x=r1 in allE, 
           rotate_tac -1, erule_tac x=r2 in allE, 
           rotate_tac -1, erule_tac x=γ in allE, erule impE, assumption)
    apply (erule exE, erule conjE)
    apply (rotate_tac 4, erule_tac x=aa in allE, 
           rotate_tac -1, erule_tac x=baa in allE, 
           rotate_tac -1, erule_tac x=γ' in allE, erule impE, assumption)
    apply (rotate_tac 8, erule_tac x=ac in allE,
           rotate_tac -1, erule_tac x=bc in allE, 
           rotate_tac -1, erule_tac x=γ' in allE, erule impE)
      apply (subgoal_tac "PhiWhileOp b Φ (PhiWhile b Φ) = (PhiWhile b Φ)", clarsimp)
      apply (simp add: PhiWhile_def)
      apply (rule Fix_lemma) apply (rule PhiWhileOp_Monotone)
    apply (erule exE, erule conjE)
    apply (rule, rule, assumption) apply (erule Pbij_extends_transitive) 
        apply (erule Pbij_extends_transitive) apply assumption

  apply clarsimp
    apply (simp only:  BExpr_low_def)
    apply (erule_tac x=a in allE, rotate_tac -1)
    apply (erule_tac x=ac in allE, rotate_tac -1)
    apply (erule_tac x=β in allE, rotate_tac -1)
    apply (erule impE, simp add: twiddle_def)
    apply (simp (no_asm_simp) add: PhiWhileOp_def)
    apply clarsimp
    apply (erule thin_rl)
    apply (erule_tac x=ac in allE, rotate_tac -1)
    apply (erule_tac x=bc in allE, rotate_tac -1)
    apply (erule_tac x=β in allE, rotate_tac -1)
    apply (erule impE, assumption)
    apply (rule_tac x=aa in exI, rule_tac x=baa in exI, rule, assumption) 
    apply clarsimp
    apply (rotate_tac 2)
    apply (erule_tac x=ad in allE, rotate_tac -1)
    apply (erule_tac x=bd in allE, rotate_tac -1)
    apply (erule_tac x=γ in allE, rotate_tac -1)
    apply (erule impE, assumption)
    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‹Operator $\mathit{PhiWhile}$ is itself monotone in $\Phi$:›

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=a in allE, erule_tac x=ba in allE,
                        erule_tac x=aa in allE, erule_tac x=baa in allE,
                        erule_tac x=γ in allE, erule mp)
apply (simp add: PhiWhileOp_def) apply clarsimp
apply (rule_tac x=ab in exI, rule_tac x=bb in exI, simp)
done
(*>*)

text‹We now give an alternative formulation using an inductive
relation equivalent to FIX. First, the definition of the variant.›

inductive_set var::"(BExpr × TT × PBij × State × State) set"
where
varFalse: "¬ evalB b (fst t); s ≡⇩β t  (b,Φ,β,s,t):var"

| varTrue:
  " evalB b (fst t); Φ(r,t,β);  w γ. r ≡⇩γ w  (b,Φ,γ,s,w): var
   (b,Φ,β,s,t):var"

text‹The equivalence of the invariant with the fixed point
construction.›
(*<*)
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 (case_tac r, clarsimp)
  apply (rule_tac x=ac in exI, rule_tac x=baa in exI, rule) apply assumption
  apply clarsimp
  apply (erule_tac x=aa in allE)
  apply (erule_tac x=bb in allE)
  apply (erule_tac x=γ 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 (fst t)")
  prefer 2 apply clarsimp apply (rule varFalse) apply assumption+
  apply clarsimp apply (rule varTrue) apply assumption apply assumption
    apply (rule, rule, rule) 
    apply (case_tac w, clarsimp) 
    apply (erule_tac x=aaa in allE, erule_tac x=baa in allE, erule_tac x=γ 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 ab")
    prefer 2 apply clarsimp apply (rule varFalse) apply simp apply assumption
    apply clarsimp apply (rule varTrue) apply simp apply assumption apply simp
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))"
apply rule apply (rule FIXvarFIX')
done
(*>*)

text‹Using this equivalence we can derive the while rule given in our
paper from WHILE›.›

lemma WHILE_IND:
  " BExpr_low b; G  c : (Sec Φ)
   G  While b c: (Sec (λ(s,t,γ). (b,Φ,γ,s,t):var))"
(*<*)
apply (rule VDMConseq)
apply (erule WHILE) apply assumption
apply clarsimp
apply (simp add: FIXvarFIX')
done
(*>*)

text‹We can also show the following property.›

(*<*)
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 (rule varFalse) apply simp apply assumption
apply clarsimp apply (rule varTrue) apply simp apply fast apply clarsimp  
done
(*>*)

lemma var_Monotone:
  "Monotone (λ Φ . (λ (s,t,β) .(b,Φ,β,s,t):var))"
(*<*)
apply (simp add: Monotone_def)
apply clarsimp
apply (rule varMonotoneAux) apply assumption apply clarsimp
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 φ)}  X)  body : Sec (φ (FIX φ)); Monotone φ
   X  Call : Sec (FIX φ)"
(*<*)
apply (rule VDMCall)
apply (subgoal_tac "φ (FIX φ) = FIX φ", clarsimp)
apply (erule Fix_lemma)
done
(*>*)

subsubsection‹High proof rules›

definition HighSec::Assn
where "HighSec = (λ s t . noLowDPs s  s ≡⇩(mkId (snd s)) t)"

lemma CAST[rule_format]:
  "G  c : HighSec  G  c : Sec (λ (s, t, β) . s ≡⇩β t)"
(*<*)
apply (erule VDMConseq)  apply (simp add:Sec_def) apply clarsimp
 apply (rule, clarsimp)
     apply (simp add: HighSec_def)
     apply (simp add: twiddle_def, clarsimp) 
     apply (rule, simp add: twiddleStore_def, clarsimp) 
       apply (erule_tac x=x in allE, clarsimp)
       apply (erule_tac x=x in allE, clarsimp)
       apply (erule twiddleVal.cases)
         apply clarsimp
         apply clarsimp apply (erule twiddleVal.cases)
                          apply clarsimp
                          apply clarsimp apply (drule mkId4b, clarsimp) apply (erule twiddleVal_Loc)
                          apply clarsimp
         apply clarsimp
     apply (simp add: twiddleHeap_def, clarsimp)
       apply (rule, simp add:  mkId2 mkId2b)
       apply (simp add:  mkId2 mkId2b, clarsimp)
         apply (subgoal_tac "l:Dom b")
         prefer 2 apply (simp add: Pbij_Dom_def) apply fast
         apply (erule_tac x=l in allE, erule_tac x=ll in allE, erule impE, assumption)
         apply (erule_tac x=l in allE, erule_tac x=l in allE, erule impE, erule mkId4) 
         apply (subgoal_tac " x y . lookup b l = Some (x,y)", clarsimp)
         prefer  2 apply (simp add: Dom_def)
         apply (simp add: twiddleObj_def, clarsimp)
         apply (subgoal_tac " u . lookup y f = Some u", clarsimp)
         prefer 2 apply (rotate_tac -6, erule thin_rl, erule thin_rl, erule thin_rl)
                  apply (simp add: LowDom_def) apply fastforce
         apply (erule_tac x=f in allE, erule_tac x=f in allE, clarsimp)
       apply (erule twiddleVal.cases)
         apply clarsimp apply (erule twiddleVal.cases)
                          apply clarsimp apply (rule twiddleVal_Null)
                          apply clarsimp 
                          apply clarsimp 
         apply clarsimp apply (erule twiddleVal.cases)
                          apply clarsimp 
                          apply clarsimp apply (drule mkId4b, clarsimp) 
                                         apply (erule twiddleVal_Loc)
                          apply clarsimp 
         apply clarsimp apply (erule twiddleVal.cases)
                          apply clarsimp 
                          apply clarsimp 
                          apply clarsimp apply (rule twiddleVal_IVal) apply simp
 apply (simp add: HighSec_def)
     apply (simp add: twiddle_def, clarsimp) 
     apply (rule_tac x=β in exI)
     apply (rule, simp add: twiddleStore_def, clarsimp) 
       apply (erule_tac x=x in allE, clarsimp)
       apply (erule_tac x=x in allE, clarsimp)
       apply (erule twiddleVal.cases)
         apply clarsimp apply (erule twiddleVal.cases)
                          apply clarsimp apply (rule twiddleVal_Null)
                          apply clarsimp 
                          apply clarsimp 
         apply clarsimp apply (erule twiddleVal.cases)
                          apply clarsimp 
                          apply clarsimp apply (drule mkId4b, clarsimp) 
                                         apply (erule twiddleVal_Loc)
                          apply clarsimp 
         apply clarsimp apply (erule twiddleVal.cases)
                          apply clarsimp 
                          apply clarsimp 
                          apply clarsimp apply (rule twiddleVal_IVal) apply simp
     apply (rule, simp add: twiddleHeap_def, clarsimp)
       apply (rule, simp add:  mkId2 mkId2b)
       apply (simp add:  mkId2 mkId2b, clarsimp)
         apply (subgoal_tac "ll:Dom b")
         prefer 2 apply (simp add: Pbij_Rng_def) apply fast
         apply (erule_tac x=l in allE, erule_tac x=ll in allE, erule impE, assumption)
         apply (erule_tac x=ll in allE, erule_tac x=ll in allE, erule impE, erule mkId4) 
         apply (subgoal_tac " x y . lookup b ll = Some (x,y)", clarsimp)
         prefer  2 apply (simp add: Dom_def)
         apply (simp add: twiddleObj_def, clarsimp)
         apply (subgoal_tac " u . lookup y f = Some u", clarsimp)
         prefer 2 apply (rotate_tac -8, erule thin_rl, erule thin_rl, erule thin_rl)
                  apply (simp add: LowDom_def) apply fastforce
         apply (erule_tac x=f in allE, erule_tac x=f in allE, clarsimp)
       apply (erule twiddleVal.cases)
         apply clarsimp apply (erule twiddleVal.cases)
                          apply clarsimp apply (rule twiddleVal_Null)
                          apply clarsimp 
                          apply clarsimp 
         apply clarsimp apply (erule twiddleVal.cases)
                          apply clarsimp 
                          apply clarsimp apply (drule mkId4b, clarsimp) 
                                         apply (erule twiddleVal_Loc)
                          apply clarsimp 
         apply clarsimp apply (erule twiddleVal.cases)
                          apply clarsimp 
                          apply clarsimp 
                          apply clarsimp apply (rule twiddleVal_IVal) apply simp
  apply (rule Pbij_extends_reflexive)
done
(*>*)

lemma SkipHigh: "G  Skip: HighSec"
(*<*)
apply (rule VDMConseq, rule VDMSkip)
apply (simp add: HighSec_def) apply clarsimp
(*apply (rule_tac x="mkId b" in exI)*)
apply (erule twiddle_mkId) 
done
(*>*)

text‹We define a predicate expressing when locations obtained by
evaluating an expression are non-dangling.›

definition Expr_good::"Expr  State  bool"
where "Expr_good e s =
  ( l . evalE e (fst s) = RVal(Loc l)  l : Dom (snd s))"

lemma AssignHigh: 
  " CONTEXT x = high;  s . noLowDPs s  Expr_good e s 
   G  Assign x e: HighSec"
(*<*)
apply (rule VDMConseq, rule VDMAssign, unfold HighSec_def)
apply (rule, rule, rule, rule)
apply (simp add: twiddle_def)
apply rule
  (*noLowDPs t*)
  apply (simp add: noLowDPs_def update_def) apply clarsimp 
apply rule
  (*twiddleStore*)
    apply (simp add: twiddleStore_def update_def)
    apply (rule, rule) 
      apply clarsimp 
    apply clarsimp
    apply (case_tac "a xa")
    apply (rename_tac Ref)
    apply clarsimp apply (case_tac Ref) 
      apply clarsimp apply (rule twiddleVal_Null) 
      apply clarsimp apply (rule twiddleVal_Loc) apply (rule mkId4) apply (simp add: noLowDPs_def)
      apply clarsimp apply (simp add: twiddleVal_IVal)
(*twiddleHeap*)
  apply (simp add: twiddleHeap_def update_def) apply clarsimp
  apply (rule, rule mkId1)
  apply (rule, simp add: mkId2)
  apply (rule, simp add: mkId2b) 
  apply clarsimp apply (drule mkId4b) apply clarsimp
  (*l=ll*)
      apply (simp add: twiddleObj_def) 
        apply clarsimp 
        apply (case_tac v, clarsimp)
        apply (rename_tac Ref)
        apply (case_tac Ref, clarsimp)
        apply (rule twiddleVal_Null)
        apply clarsimp apply (rule twiddleVal_Loc) apply (rule mkId4) apply (simp add: noLowDPs_def)
        apply clarsimp apply (rule twiddleVal_IVal) apply simp
done
(*>*)

lemma NewHigh:
  "CONTEXT x = high  G  New x C : HighSec"
(*<*)
apply (rule VDMConseq, rule VDMNew, unfold HighSec_def)
apply (rule, rule, rule)
apply (erule exE, (erule conjE)+)
apply (rule, simp add: twiddle_def, rule)
(*noLowDPs t*)
  apply (simp add: noLowDPs_def, clarsimp) apply (rename_tac l s h) apply rule 
  (*store content*)
    apply clarsimp apply (simp add: update_def)
    apply (case_tac "x=xa", clarsimp) apply (simp add: Dom_def)
    (*apply clarsimp apply (erule_tac x=xa in allE, erule_tac x=la in allE, clarsimp)
      apply (simp add: Dom_def)*)
  (*Field content*)
    apply clarsimp apply (simp add: Dom_def)
(*apply (rule_tac x="mkId (snd s)" in exI)*)
apply rule
(*twiddleStore*)
    apply (simp add: twiddleStore_def)
    apply (rule, rule) apply (simp add: update_def) apply clarsimp
    apply (rename_tac s h l xa)
    apply (case_tac "x=xa", clarsimp) apply clarsimp
    apply (case_tac "s xa")
    apply (rename_tac Ref)
    apply clarsimp apply (case_tac Ref) 
      apply clarsimp apply (rule twiddleVal_Null) 
      apply clarsimp apply (rule twiddleVal_Loc) apply (rule mkId4) apply (simp add: noLowDPs_def)
      apply clarsimp apply (simp add: twiddleVal_IVal)
(*twiddleHeap*)
  apply (simp add: twiddleHeap_def) apply clarsimp
  apply (rename_tac s h l)
  apply (rule, rule mkId1)
  apply (rule, simp add: mkId2) 
  apply (rule, simp add: mkId2b Dom_def) apply fastforce
  apply clarsimp 
  apply rule
    apply clarsimp apply (drule mkId4b) apply clarsimp
    apply clarsimp apply (drule mkId4b) apply clarsimp
      apply (rename_tac C F)
      apply (simp add: twiddleObj_def) apply clarsimp
        apply (case_tac v, clarsimp)
        apply (rename_tac Ref)
        apply (case_tac Ref, clarsimp)
        apply (rule twiddleVal_Null)
        apply clarsimp apply (rule twiddleVal_Loc) apply (rule mkId4) apply (simp add: noLowDPs_def)
        apply clarsimp apply (rule twiddleVal_IVal) apply simp
done
(*>*)

lemma GetHigh: 
" CONTEXT x = high   G  Get x y f : HighSec"
(*<*)
apply (rule VDMConseq, rule VDMGet, unfold HighSec_def)
apply (rule, rule, rule)
apply (erule exE)+
apply (erule conjE)+
apply (rule, simp add: twiddle_def, rule)
(*noLowDPs t*)
  apply (simp add: noLowDPs_def, clarsimp)
  (*store content*)
    apply (rename_tac s h xa la)
    apply (simp add: update_def)
    apply (case_tac "x=xa", clarsimp) apply (simp add: Dom_def)
  (*Field content already discharged*)
(*apply (rule_tac x="mkId (snd s)" in exI)*)
apply rule
(*twiddleStore*)
    apply (simp add: twiddleStore_def)
    apply (rule, rule) apply (simp add: update_def) apply clarsimp
    apply (rename_tac s h l C Flds v xa)
    apply (case_tac "x=xa", clarsimp) apply clarsimp
    apply (case_tac "s xa")
    apply (rename_tac Ref)
    apply clarsimp apply (case_tac Ref) 
      apply clarsimp apply (rule twiddleVal_Null) 
      apply clarsimp apply (rule twiddleVal_Loc) apply (rule mkId4) apply (simp add: noLowDPs_def)
      apply clarsimp apply (simp add: twiddleVal_IVal)
(*twiddleHeap*)
  apply (simp add: twiddleHeap_def) apply clarsimp
  apply (rename_tac s h l C Flds v)
  apply (rule, rule mkId1)
  apply (rule, simp add: mkId2)
  apply (rule, simp add: mkId2b)
  apply clarsimp apply (drule mkId4b) apply clarsimp
    apply (rename_tac D F)
      apply (simp add: twiddleObj_def) apply clarsimp
        apply (case_tac va, clarsimp)
        apply (rename_tac Ref)
        apply (case_tac Ref, clarsimp)
        apply (rule twiddleVal_Null)
        apply clarsimp apply (rule twiddleVal_Loc) apply (rule mkId4) apply (simp add: noLowDPs_def)
        apply clarsimp apply (rule twiddleVal_IVal) apply simp
done
(*>*)

lemma PutHigh: 
" GAMMA f = high;  s . noLowDPs s  Expr_good e s
   G  Put x f e: HighSec"
(*<*)
apply (rule VDMConseq, rule VDMPut, unfold HighSec_def)
apply (rule, rule, rule)
apply (erule exE)+
apply (erule conjE)+
apply (rule, simp add: twiddle_def, rule)
(*noLowDPs t*)
  apply (simp add: noLowDPs_def, clarsimp)
  apply (rename_tac s h)
  apply rule
  (*store content*)
    apply clarsimp apply (erule_tac x=xa in allE, erule_tac x=la in allE, clarsimp) 
      apply (simp add: Dom_def)
  (*Field content*)
    apply clarsimp apply rule
    (*l=ll*)
      apply clarsimp apply rule
      (*f=fa*)
        apply clarsimp 
      (*f≠fa*)
        apply clarsimp apply (simp add: Dom_def)
    (*l≠ll*)
     apply clarsimp apply (simp add: Dom_def)
apply rule
(*twiddleStore*)
    apply (simp add: twiddleStore_def)
    apply (rule, rule) 
    apply (case_tac "fst s xa")
    apply (rename_tac Ref)
    apply clarsimp apply (case_tac Ref) 
      apply clarsimp apply (rule twiddleVal_Null) 
      apply clarsimp apply (rule twiddleVal_Loc) apply (rule mkId4) apply (simp add: noLowDPs_def)
      apply clarsimp apply (simp add: twiddleVal_IVal)
(*twiddleHeap*)
  apply (simp add: twiddleHeap_def) apply clarsimp
  apply (rule