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, simp add: mkId1)
  apply (rule, simp add: mkId2)
  apply (rule, simp add: mkId2b Dom_def) apply fast
  apply clarsimp apply rule
  (*l=ll*)
    apply clarsimp apply (drule mkId4b) apply clarsimp 
      apply (simp add: twiddleObj_def) 
        apply (rule, simp add: LowDom_def) apply (rotate_tac -1, erule thin_rl) apply fastforce
        apply clarsimp apply rule
        (*f=fa*)
        apply clarsimp
        (*f≠fa*)
        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
   (*l≠ll*)
     apply clarsimp apply (drule mkId4b) apply clarsimp 
      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 PutHigh2: 
  "⟦ GAMMA f = high; ∀ s . Expr_good e s⟧ ⟹ G ⊳ Put x f e: HighSec"
apply (rule VDMConseq, erule PutHigh) apply simp apply simp
done
(*>*)

(*<*)
lemma twiddle_mkIDs_compose:
  "⟦(a,b) ≡⇩(mkId b) (ab, bb); (ab,bb) ≡⇩(mkId bb) (aa, ba)⟧
  ⟹ (a,b) ≡⇩(mkId b) (aa, ba)"
supply [[simproc del: defined_all]]
apply (simp add: twiddle_def)
  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 prefer 2 apply clarsimp 
                       apply (drule mkId4b, clarsimp) apply (drule mkId4b, clarsimp) 
                       apply (rule twiddleVal_Loc) apply (erule mkId4)
      apply clarsimp 
  apply (simp add: twiddleHeap_def, clarsimp)
    apply (simp add: mkId2 mkId2b)
    apply rule apply fast
    apply clarsimp apply (drule mkId4b, clarsimp)
      apply (erule_tac x=ll in allE, erule_tac x=ll in allE, erule impE, erule mkId4) apply clarsimp
      apply (subgoal_tac "ll:Dom bb") prefer 2 apply fast
      apply (erule_tac x=ll in allE, erule_tac x=ll in allE, erule impE, erule mkId4) apply clarsimp
      apply (subgoal_tac "∃ x y . lookup bb ll = Some(x,y)", clarsimp)
      prefer 2 apply (simp add: Dom_def)
      apply (simp add: twiddleObj_def, clarsimp)
      apply (subgoal_tac "∃ u . lookup bc f = Some u", clarsimp)
      prefer 2 apply (simp add: LowDom_def) 
      apply (subgoal_tac "∃ u . lookup y f = Some u", clarsimp)
      prefer 2 apply (rotate_tac -7, erule thin_rl, erule thin_rl) apply (simp add: LowDom_def) apply fast
      apply (erule_tac x=f in allE, clarsimp)
      apply (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 prefer 2 apply clarsimp 
                       apply (drule mkId4b, clarsimp) apply (drule mkId4b, clarsimp) 
                       apply (rule twiddleVal_Loc) apply (erule mkId4)
      apply clarsimp apply (erule twiddleVal.cases)
                       apply clarsimp apply clarsimp apply clarsimp apply (rule twiddleVal_IVal) apply clarsimp       
done
(*>*)
(*<*)
lemma twiddle_mkIDs_compose':
  "⟦ s ≡⇩(mkId (snd s)) r; r ≡⇩(mkId (snd r)) t⟧ ⟹ s ≡⇩(mkId (snd s)) t"
apply (case_tac s, clarsimp)
apply (case_tac t, clarsimp)
apply (case_tac r, clarsimp)
apply (erule twiddle_mkIDs_compose, assumption)
done
(*>*)

lemma CompHigh:
 "⟦ G ⊳ c: HighSec; G ⊳ d:HighSec⟧ ⟹ G ⊳ Comp c d: HighSec"
(*<*)
apply (rule VDMConseq, erule VDMComp, assumption)
apply (unfold HighSec_def)
apply (rule, rule, rule)
apply (erule thin_rl, erule thin_rl, erule exE)
apply (erule conjE) apply clarsimp
apply (erule impE) prefer 2 apply (erule twiddle_mkIDs_compose, assumption) 
apply (simp add: noLowDPs_def twiddle_def)
done
(*>*)

lemma IfHigh: 
 "⟦ G ⊳ c: HighSec; G ⊳ d:HighSec⟧ ⟹ G ⊳ Iff b c d: HighSec"
(*<*)
apply (rule VDMConseq, rule VDMIff)
apply (assumption, assumption)
apply (erule thin_rl, erule thin_rl)
apply clarsimp
done(*>*)

lemma WhileHigh: "⟦ G ⊳ c: HighSec⟧ ⟹ G ⊳ While b c: HighSec"
(*<*)
apply (rule VDMConseq, erule VDMWhile [of G c HighSec b HighSec])
apply (simp add: HighSec_def) apply clarsimp
(*apply (rule_tac x="mkId ba" in exI)*)
apply (erule twiddle_mkId) 

apply clarsimp
apply (simp add: HighSec_def) apply clarsimp
(*apply (rule_tac x="Pbij_compose β β'" in exI)*)
apply (erule impE) prefer 2 apply (erule twiddle_mkIDs_compose, assumption) 
(*apply (erule twiddle_compose, assumption)*)
apply (simp add: noLowDPs_def twiddle_def)

apply clarsimp
done(*>*)

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

text‹We combine all rules to an inductive derivation system.›

inductive_set Deriv::"(Assn set × OBJ × Assn) set"
where
D_CAST: 
  "(G, c, HighSec):Deriv ⟹
  (G, c, Sec (λ (s, t, β). s ≡⇩β t)):Deriv"

| D_SKIP: "(G, Skip, Sec (λ (s, t, β) . s ≡⇩β t)) : Deriv"

| D_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)):Deriv"

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

| D_IFF:
 "⟦ BExpr_low b; (G, c1, Sec Φ):Deriv; (G, c2, Sec Ψ):Deriv⟧ ⟹
 (G, Iff b c1 c2, Sec (λ (s,t,β) .
                       (evalB b (fst t) ⟶ Φ(s,t,β)) ∧ 
                       ((¬ evalB b (fst t)) ⟶ Ψ(s,t,β)))):Deriv"

| D_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)))):Deriv"

| D_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))):Deriv"

| D_PUT: 
  "⟦ CONTEXT x = low; GAMMA f = low; Expr_low e⟧ ⟹
  (G, Put x f e, Sec (λ (s,t,β) .
         ∃ r l C F h. (fst r) x = RVal(Loc l) ∧ r ≡⇩β t ∧
                       lookup (snd r) l = Some(C,F) ∧ 
                       h = (l,(C,(f,evalE e (fst r)) # F)) # (snd r) ∧
                       s = (fst r, h))):Deriv"

| D_WHILE:  
 "⟦ BExpr_low b; (G, c, Sec Φ):Deriv⟧ 
  ⟹ (G, While b c, Sec (PhiWhile b Φ)):Deriv"

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

| D_SKIP_H: "(G, Skip, HighSec):Deriv"

| D_ASSIGN_H:
 "⟦ CONTEXT x = high; ∀ s . noLowDPs s ⟶ Expr_good e s⟧
  ⟹ (G, Assign x e, HighSec):Deriv"

| D_NEW_H: "CONTEXT x = high ⟹ (G, New x C, HighSec):Deriv"

| D_GET_H: "CONTEXT x = high ⟹ (G, Get x y f, HighSec):Deriv"

| D_PUT_H: 
 "⟦ GAMMA f = high; ∀ s . noLowDPs s ⟶ Expr_good e s⟧
  ⟹ (G, Put x f e, HighSec):Deriv"  

| D_COMP_H:
 "⟦ (G, c, HighSec):Deriv; (G, d, HighSec):Deriv⟧ 
 ⟹ (G, Comp c d, HighSec):Deriv"

| D_IFF_H:
 "⟦ (G, c, HighSec):Deriv; (G, d, HighSec):Deriv⟧
  ⟹ (G, Iff b c d, HighSec):Deriv"

| D_WHILE_H:
 "⟦ (G, c, HighSec):Deriv⟧ ⟹ (G, While b c, HighSec):Deriv"

| D_CALL_H:
 "({HighSec} ∪ G, body, HighSec):Deriv ⟹ (G, Call, HighSec):Deriv"

text‹By construction, all derivations represent legal derivations in
the program logic. Here's an explicit lemma to this effect.›

lemma Deriv_derivable: "(G,c,A):Deriv ⟹ G ⊳ c: A"
(*<*)
apply (erule Deriv.induct)
apply (erule CAST)
apply (rule SKIP)
apply (erule ASSIGN)
apply (erule COMP) apply assumption
apply (erule IFF) apply assumption apply assumption
apply (erule NEW)
apply (erule GET) apply assumption 
apply (drule_tac G=G in PUT) apply assumption apply assumption apply simp
apply (erule WHILE) apply assumption 
apply (erule CALL) apply assumption
apply (rule SkipHigh)
apply (erule AssignHigh) apply assumption
apply (erule NewHigh)
apply (erule GetHigh)
apply (erule PutHigh) apply assumption
apply (erule CompHigh) apply assumption
apply (erule IfHigh) apply assumption
apply (erule WhileHigh) 
apply (erule CallHigh)
done
(*>*)

subsection‹Type system›
text‹\label{sec:ObjTypeSystem}›

text‹We now give a type system in the style of Volpano et al.~and
then prove its embedding into the system of derived rules. First, type
systems for expressions and boolean expressions. These are similar to
the ones in Section \ref{sec:BaseLineNI} but require some side
conditions regarding the (semantically modelled) operators.›

definition opEGood::"(Val ⇒ Val ⇒ Val) ⇒ bool"
where "opEGood f = (∀ β v v' w w' . (β, v, v') ∈ twiddleVal⟶
        (β, w, w') ∈ twiddleVal ⟶ (β, f v w, f v' w') ∈ twiddleVal)"

definition compBGood::"(Val ⇒ Val ⇒ bool) ⇒ bool"
where "compBGood f = (∀ β v v' w w' . (β, v, v') ∈ twiddleVal⟶
        (β, w, w') ∈ twiddleVal ⟶ f v w = f v' w')"

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

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

text‹Next, the core of the type system, the rules for commands. The
second side conditions of rules ‹VS_comAssH› and ‹VS_comPutH› could be strengthened to $\forall\; s .\;
\mathit{Epxr\_good}\; e\; s$.›

inductive_set VS_com:: "(TP × OBJ) set"
where
VS_comGetL: 
  "⟦ CONTEXT y = low; GAMMA f = low⟧ 
  ⟹ (low, Get x y f):VS_com"

| VS_comGetH: "CONTEXT x = high ⟹ (high, Get x y f):VS_com"

| VS_comPutL:
  "⟦ CONTEXT x = low; GAMMA f = low; (e, low) : VS_expr⟧
  ⟹ (low,Put x f e):VS_com"

| VS_comPutH:
  "⟦ GAMMA f = high; ∀ s . noLowDPs s ⟶ Expr_good e s⟧
  ⟹ (high,Put x f e):VS_com"

| VS_comNewL:
  "CONTEXT x = low ⟹ (low, New x c) : VS_com"

| VS_comNewH:
  "CONTEXT x = high ⟹ (high, New x C):VS_com"

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

| VS_comAssH:
  "⟦CONTEXT x = high; ∀ s . noLowDPs s ⟶ Expr_good e s⟧ 
  ⟹ (high,Assign x e) : VS_com"

| VS_comSkip: "(pc,Skip) : VS_com"

| VS_comComp:
  "⟦ (pc,c):VS_com; (pc,d):VS_com⟧  ⟹ (pc,Comp c d) : VS_com"

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

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

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

text‹In order to prove the type system sound, we first define the
interpretation of expression typings\ldots›

primrec SemExpr::"Expr ⇒ TP ⇒ bool"
where
"SemExpr e low = Expr_low e" |
"SemExpr e high = True"

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

lemma ExprSound: "(e,tp):VS_expr ⟹ SemExpr e tp"
(*<*)
apply (erule VS_expr.induct)
apply clarsimp
  apply (case_tac "CONTEXT x", clarsimp) apply (simp add: Expr_low_def twiddleStore_def)
  apply clarsimp
apply (simp add: Expr_low_def)
  apply (erule disjE) apply clarsimp apply (rule twiddleVal_Null)
    apply clarsimp apply (rule twiddleVal_IVal) apply simp
apply (case_tac t, clarsimp)
  apply (simp add: Expr_low_def, clarsimp)
    apply (erule_tac x=s in allE, erule_tac x=t in allE, erule_tac x=β in allE, erule impE, assumption)
    apply (erule_tac x=s in allE, erule_tac x=t in allE, erule_tac x=β in allE, erule impE, assumption)
    apply (simp add: opEGood_def)
  apply simp
apply clarsimp
done
(*>*)

text‹Likewise for the boolean expressions.›

primrec SemBExpr::"BExpr ⇒ TP ⇒ bool"
where
"SemBExpr b low = BExpr_low b" |
"SemBExpr b high = True"

lemma BExprSound: "(e,tp):VS_Bexpr ⟹ SemBExpr e tp"
(*<*)
apply (erule VS_Bexpr.induct, simp_all)
apply (drule ExprSound) 
apply (drule ExprSound) 
apply (case_tac t, simp_all add: BExpr_low_def Expr_low_def) apply clarsimp
  apply (erule_tac x=s in allE, erule_tac x=ta in allE, erule_tac x=β in allE, erule impE, assumption)
  apply (erule_tac x=s in allE, erule_tac x=ta in allE, erule_tac x=β in allE, erule impE, assumption)
  apply (simp add: compBGood_def)
done
(*>*)

text‹Using these auxiliary lemmas we can prove the embedding of the
type system for commands into the system of derived proof rules, by
induction on the typing rules.›

theorem VS_com_Deriv[rule_format]:
"(t,c):VS_com ⟹ (t=high ⟶ (G, c, HighSec):Deriv) ∧
                  (t=low ⟶ (∃ Φ . (G, c, Sec Φ):Deriv))"
(*<*)
apply (erule VS_com.induct)
apply clarsimp
  apply (rule, erule D_GET) apply assumption
apply clarsimp apply (erule D_GET_H) 
apply clarsimp
  apply (rule, erule D_PUT) apply assumption apply (drule ExprSound) apply simp
apply clarsimp apply (erule D_PUT_H) apply simp 
apply clarsimp apply (rule, erule D_NEW) 
apply clarsimp apply (erule D_NEW_H) 
apply clarsimp apply (rule, rule D_ASSIGN) apply (drule ExprSound) apply simp 
apply clarsimp apply (erule D_ASSIGN_H) apply simp
apply rule
  apply clarsimp apply (rule D_SKIP_H)
  apply clarsimp apply (rule, rule D_SKIP) 
apply (erule conjE)+ apply rule 
  apply rule apply (erule impE, assumption) apply (erule impE, assumption) 
             apply (erule D_COMP_H) apply assumption
  apply rule apply (erule impE, assumption, erule exE) apply (erule impE, assumption, erule exE) 
             apply (rule, erule D_COMP) apply assumption
apply (erule conjE)+ apply rule 
  apply rule apply (erule impE, assumption) apply (erule impE, assumption) 
             apply (erule D_IFF_H) apply assumption
  apply rule apply (erule impE, assumption, erule exE) apply (erule impE, assumption, erule exE) 
             apply (rule, rule D_IFF) prefer 2 apply assumption prefer 2 apply assumption
             apply (drule BExprSound) apply simp
apply (erule conjE)+ apply rule 
  apply (rule, erule impE, assumption) 
             apply (erule D_WHILE_H) 
  apply (rule, erule impE, assumption, erule exE) 
             apply (rule, rule D_WHILE) prefer 2 apply assumption 
             apply (drule BExprSound) apply simp
apply simp apply (rule, erule D_CAST)
done
(*>*)

text‹Combining this result with the derivability of the derived proof
system and the soundness theorem of the program logic yields non-interference
of programs that are low typeable.›

theorem VS_SOUND: "(low,c):VS_com ⟹ secure c"
(*<*)
apply (drule_tac G="{}" in VS_com_Deriv, simp)
apply (erule exE)
apply (drule  Deriv_derivable)
apply (drule VDM_Sound_emptyCtxt)
apply (erule Prop1A)
done
(*>*)

text‹End of theory ‹VS_OBJ››
end