Confine_S.thy

(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

(* Title:   Confinement_S
 * Description: confinement proof of the security model
 *)

theory Confine_S
imports System_S
begin

(* These translate Create into all_rights *)
definition
  extra_rights :: "cap \<Rightarrow> cap" where
  "extra_rights c \<equiv>
  if (Create \<in> rights c)
  then c\<lparr>rights := all_rights\<rparr>
  else c"


lemma extra_rights_idem [simp]:
  "(extra_rights (extra_rights c)) = (extra_rights c)"
  apply (clarsimp simp add: extra_rights_def)
  done

lemma extra_rights_image_idem [simp]:
  "(extra_rights ` (extra_rights ` S)) = (extra_rights ` S)"
  by (rule set_eqI) (simp add: image_iff)

lemma extra_rights_empty_rights_ident [simp]:
   "extra_rights \<lparr> target = e, rights = {} \<rparr> = \<lparr> target = e, rights = {} \<rparr>"
  by (simp add: extra_rights_def)

lemma entity_extra_rights [simp]:
  "target (extra_rights c) = target c"
  by (simp add: extra_rights_def)

lemma rights_extra_rights:
  "rights (extra_rights c) =
   (if Create \<in> (rights c)
    then all_rights
    else rights c)"
  by (simp add: extra_rights_def)

(* The following two definitions both translate Create into all_rights *)

(* A cap is in a set, or a cap with more access is. *)
definition
  cap_in_caps :: "cap \<Rightarrow> cap set \<Rightarrow> bool" (infix "\<in>cap" 50) where
  "c \<in>cap C \<equiv> \<exists>c' \<in> C. target c = target c' \<and> rights (extra_rights c) \<subseteq> rights (extra_rights c')"

abbreviation not_cap_in_caps where
  "not_cap_in_caps x A \<equiv> ~ (x \<in>cap A)" \<comment> \<open>non-membership\<close>

notation (input) cap_in_caps (infix ":cap" 50)
notation (latex output)  cap_in_caps (infix "\<in>\<^sub>c\<^sub>a\<^sub>p" 50)

notation
  not_cap_in_caps  ("(\<notin>cap)") and
  not_cap_in_caps  ("(_/ \<notin>cap _)" [51, 51] 50)

notation (latex output)
  not_cap_in_caps  ("(\<notin>\<^sub>c\<^sub>a\<^sub>p)") and
  not_cap_in_caps  (infix "\<notin>\<^sub>c\<^sub>a\<^sub>p" 50)

(* A set of caps "caps" have less (or equal) access to an entity as "cap" does. *)
definition
  caps_dominated_by :: "cap set \<Rightarrow> cap \<Rightarrow> bool" (infix "\<le>cap" 50) where
  "caps \<le>cap cap \<equiv> \<forall>cap' \<in> caps. target cap' = target cap \<longrightarrow> rights (extra_rights cap') \<subseteq> rights (extra_rights cap)"

notation (input) caps_dominated_by (infix "<=cap" 50)
notation (latex output) caps_dominated_by (infix "\<unlhd>\<^sub>c\<^sub>a\<^sub>p" 50)

definition
  shares_caps :: "state \<Rightarrow> entity_id \<Rightarrow> entity_id \<Rightarrow> bool" where
  "shares_caps s e\<^sub>x e\<^sub>y \<equiv> \<exists>e\<^sub>i . (e\<^sub>x, e\<^sub>i) \<in> store_connected s \<and> (e\<^sub>y, e\<^sub>i) \<in> store_connected s"

definition
  leak :: "state \<Rightarrow> entity_id \<Rightarrow> entity_id \<Rightarrow> bool" ("_ \<turnstile> _ \<rightarrow> _") where
  "leak s e\<^sub>x e\<^sub>y \<equiv> take_cap e\<^sub>x \<in>cap caps_of s e\<^sub>y \<or> grant_cap e\<^sub>y \<in>cap caps_of s e\<^sub>x \<or> shares_caps s e\<^sub>x e\<^sub>y"


definition
  directly_tgs_connected :: "state \<Rightarrow> (entity_id \<times> entity_id) set" where
  "directly_tgs_connected s \<equiv> {(e\<^sub>x, e\<^sub>y). leak s e\<^sub>x e\<^sub>y \<or> leak s e\<^sub>y e\<^sub>x}"

lemma directly_tgs_connected_def2:
  "(e\<^sub>x, e\<^sub>y) \<in> directly_tgs_connected s = (leak s e\<^sub>x e\<^sub>y \<or> leak s e\<^sub>y e\<^sub>x)"
  by (simp add: directly_tgs_connected_def)

abbreviation
  in_directly_tgs_connected :: "state \<Rightarrow> entity_id \<Rightarrow> entity_id \<Rightarrow> bool" ("_ \<turnstile> _ \<leftrightarrow> _" [60,0,60] 61)
where
  "s \<turnstile> x \<leftrightarrow> y \<equiv> (x,y) \<in> directly_tgs_connected s"

definition
  tgs_connected :: "state \<Rightarrow> (entity_id \<times> entity_id) set" where
  "tgs_connected s \<equiv> (directly_tgs_connected s)\<^sup>*"

abbreviation
  in_tgs_connected :: "state \<Rightarrow> entity_id \<Rightarrow> entity_id \<Rightarrow> bool" ("_ \<turnstile> _ \<leftrightarrow>* _" [60,0,60] 61)
where
  "s \<turnstile> x \<leftrightarrow>* y == (x,y) \<in> tgs_connected s"

notation (latex output)
  in_tgs_connected ("_ \<turnstile> _ \<leftrightarrow>\<^sup>* _" [60,0,60] 61)

translations
  "\<not> (s \<turnstile> x \<leftrightarrow> y)" <= "(x,y) \<notin> CONST directly_tgs_connected s"
  "\<not> (s \<turnstile> x \<leftrightarrow>* y)" <= "(x,y) \<notin> CONST tgs_connected s"

lemma shares_caps_sym [simp]:
 "shares_caps s y x = shares_caps s x y"
  by (auto simp: shares_caps_def)

lemma directly_tgs_connected_def4:
  "s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y = (take_cap e\<^sub>x \<in>cap caps_of s e\<^sub>y \<or> take_cap e\<^sub>y \<in>cap caps_of s e\<^sub>x \<or>
                  grant_cap e\<^sub>y \<in>cap caps_of s e\<^sub>x \<or> grant_cap e\<^sub>x \<in>cap caps_of s e\<^sub>y \<or>
                  shares_caps s e\<^sub>x e\<^sub>y)"
  by (auto simp: directly_tgs_connected_def leak_def)

(* Note: e\<^sub>0 is unused. *)
definition
  generalOperation ::
  "entity_id \<Rightarrow> entity_id \<Rightarrow> cap \<Rightarrow> right set \<Rightarrow> modify_state" where
  "generalOperation e\<^sub>0 e\<^sub>1 c r s \<equiv>
  s (e\<^sub>1 \<mapsto> Entity ( insert (diminish r (extra_rights c)) (direct_caps_of s e\<^sub>1) ))"

lemma is_entity_general [simp]:
  "is_entity s e\<^sub>1 \<Longrightarrow> is_entity (generalOperation e\<^sub>0 e\<^sub>1 c r s) e' = is_entity s e'"
  by (simp add: is_entity_def generalOperation_def)

definition
  make_entity :: "entity_id \<Rightarrow> modify_state" where
  "make_entity n s \<equiv>
  s (n \<mapsto> null_entity)"

lemma direct_caps_of_store_connected_eq:
  "\<forall> e. direct_caps_of s e = direct_caps_of s' e
  \<Longrightarrow> store_connected s = store_connected s'"
  by (simp add: store_connected_def store_connected_direct_def
                direct_caps_of_def)

lemma direct_caps_of_caps_of_eq:
  "\<forall> e. direct_caps_of s e = direct_caps_of s' e \<Longrightarrow> caps_of s e = caps_of s' e"
  by (simp add: caps_of_def store_connected_def store_connected_direct_def
                direct_caps_of_def)

lemma direct_caps_of_caps_of_eq2:
  "\<lbrakk>\<forall> e. direct_caps_of s e = direct_caps_of s' e; c \<in>cap caps_of s e\<rbrakk> \<Longrightarrow> c \<in>cap caps_of s' e"
  apply (drule direct_caps_of_caps_of_eq)
  apply (simp add: cap_in_caps_def)
  by auto

lemma direct_caps_of_directly_tgs_connected_eq:
  "\<forall> e. direct_caps_of s e = direct_caps_of s' e \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y = s' \<turnstile> x \<leftrightarrow> y"
  apply (simp add: directly_tgs_connected_def4 shares_caps_def)
  apply rule
   apply (erule disjE, drule (1) direct_caps_of_caps_of_eq2, clarsimp)+
   apply (drule direct_caps_of_store_connected_eq, clarsimp)
  apply (erule disjE, drule direct_caps_of_caps_of_eq2 [rotated, where s=s' and s'=s], simp+)+
  apply (drule direct_caps_of_store_connected_eq, simp)
  done

lemma direct_caps_of_make_entity:
  "\<not> is_entity s n \<Longrightarrow> direct_caps_of (make_entity n s) e = direct_caps_of s e"
  by (simp add: direct_caps_of_def make_entity_def is_entity_def
                null_entity_def)

lemma caps_of_make_entity:
  "\<not> is_entity s n \<Longrightarrow> caps_of (make_entity n s) e = caps_of s e"
  apply (rule direct_caps_of_caps_of_eq)
  apply clarsimp
  apply (erule direct_caps_of_make_entity)
  done

lemma caps_of_make_entity2:
  "\<lbrakk>\<not> is_entity s n; c \<in> caps_of (make_entity n s) e\<rbrakk> \<Longrightarrow> c \<in> caps_of s e"
  apply (drule caps_of_make_entity)
  apply fastforce
  done

lemma directly_tgs_connected_make_entity:
 "\<not> is_entity s n \<Longrightarrow> make_entity n s \<turnstile> x \<leftrightarrow> y = s \<turnstile> x \<leftrightarrow> y"
  apply (rule direct_caps_of_directly_tgs_connected_eq)
  apply clarsimp
  apply (drule (1) direct_caps_of_make_entity)
  done

lemma directly_tgs_connected_make_entity2:
 "\<lbrakk>\<not> is_entity s n; make_entity n s \<turnstile> x \<leftrightarrow> y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y"
  apply (drule directly_tgs_connected_make_entity)
  apply fastforce
  done

lemma diminish_extra_rights [simp]:
  "diminish (rights c) (extra_rights c) = c"
  by (simp add: diminish_def all_rights_def rights_extra_rights)

lemma diminish_extra_rights2 [simp]:
  "diminish (r \<inter> rights c) (extra_rights c) = diminish r c"
  apply (simp add: diminish_def extra_rights_def all_rights_def)
  apply (simp add: Int_commute)
  apply (subgoal_tac "rights c \<inter> (r \<inter> rights c) = r \<inter> rights c")
   apply simp
  apply fastforce
  done

lemma create_general_helper:
  "Create \<in> rights c\<^sub>2 \<Longrightarrow>
   \<lparr>target = target c\<^sub>2, rights = UNIV\<rparr> = c\<^sub>2\<lparr>rights := UNIV\<rparr>"
  by auto

lemma extra_rights_full_cap [simp]:
  "extra_rights (full_cap e) = full_cap e"
  by (simp add: extra_rights_def)

lemma create_general_alt:
  "createOperation e c\<^sub>1 c\<^sub>2 s =
   make_entity (target c\<^sub>2)
               (generalOperation  e (target c\<^sub>1) (full_cap (target c\<^sub>2)) (all_rights) s)"
  by (simp add: createOperation_def generalOperation_def make_entity_def)

lemma create_general:
  "Create \<in> rights c\<^sub>2 \<Longrightarrow> createOperation e c\<^sub>1 c\<^sub>2 s =
   make_entity (target c\<^sub>2)
               (generalOperation  e (target c\<^sub>1) c\<^sub>2 (all_rights) s)"
  by (simp add: createOperation_def generalOperation_def make_entity_def
                full_cap_def all_rights_def diminish_def
                extra_rights_def create_general_helper null_entity_def)

lemma take_general:
  "takeOperation e c\<^sub>1 c\<^sub>2 r s =
   generalOperation (target c\<^sub>1) e c\<^sub>2 (r \<inter> rights c\<^sub>2) s"
  by (simp add: takeOperation_def generalOperation_def)

lemma grant_general:
  "grantOperation e c\<^sub>1 c\<^sub>2 r s =
   generalOperation e (target c\<^sub>1) c\<^sub>2 (r \<inter> rights c\<^sub>2) s"
  by (simp add: grantOperation_def generalOperation_def)

lemma copy_general:
  "copyOperation e c\<^sub>1 c\<^sub>2 r s =
   generalOperation e (target c\<^sub>1) c\<^sub>2 (r \<inter> rights c\<^sub>2) s"
  by (simp add: copyOperation_def generalOperation_def)

(* Lemmas on the directly_tgs_connected predicate *)
lemma directly_tgs_connected_comm:
  "s \<turnstile> x \<leftrightarrow> y \<Longrightarrow> s \<turnstile> y \<leftrightarrow> x"
  by(auto simp: directly_tgs_connected_def)

lemma tgs_connected_refl [simp]:
  "s \<turnstile> x \<leftrightarrow>* x"
  by (metis tgs_connected_def rtrancl.rtrancl_refl)

lemma tgs_connected_comm:
  "s \<turnstile> x \<leftrightarrow>* y \<Longrightarrow> s \<turnstile> y \<leftrightarrow>* x"
  apply(simp add: tgs_connected_def)
  apply(erule rtrancl_induct, simp)
  apply(case_tac "s \<turnstile> z \<leftrightarrow> y")
   apply(simp add: directly_tgs_connected_comm)
  apply(simp add: directly_tgs_connected_comm)
  done

lemma tgs_connected_comm_eq:
  "s \<turnstile> x \<leftrightarrow>* y = s \<turnstile> y \<leftrightarrow>* x"
  by (metis tgs_connected_comm)

lemmas tgs_connected_trans =
       rtrancl_trans [where r="directly_tgs_connected s"  for s, simplified tgs_connected_def[symmetric]]

lemmas directly_tgs_connected_rtrancl_into_rtrancl =
       rtrancl_into_rtrancl [where r="directly_tgs_connected s" for s, simplified tgs_connected_def[symmetric]]

lemma take_caps_directly_tgs_connected:
  "\<lbrakk>c \<in> caps_of s e; Take \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c"
  by (auto simp: directly_tgs_connected_def leak_def take_cap_def cap_in_caps_def extra_rights_def all_rights_def)

lemma grant_caps_directly_tgs_connected:
  "\<lbrakk>c \<in> caps_of s e; Grant \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c"
  by (auto simp: directly_tgs_connected_def leak_def grant_cap_def cap_in_caps_def extra_rights_def all_rights_def)

lemma create_caps_directly_tgs_connected:
  "\<lbrakk>c \<in> caps_of s e; Create \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c"
  by (auto simp: directly_tgs_connected_def leak_def cap_in_caps_def rights_extra_rights all_rights_def)

lemma store_connected_directly_tgs_connected:
  "(x, y) \<in> store_connected s \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y"
  by (auto simp: directly_tgs_connected_def leak_def shares_caps_def store_connected_def)

(* Lemmas on caps *)

lemma cap_in_caps_insert [simp]:
  "c \<in>cap insert c' S = (target c = target c' \<and>
  rights (extra_rights c) \<subseteq> rights (extra_rights c') \<or> c \<in>cap S)"
  by (simp add: cap_in_caps_def)

lemma cap_in_caps_singleton [simp]:
  "c \<in>cap {c'} = (target c = target c' \<and> rights (extra_rights c) \<subseteq> rights (extra_rights c'))"
  by (simp add: cap_in_caps_def)

lemma not_in [simp]:
  "{} \<le>cap c"
  by(simp add: caps_dominated_by_def)

lemma extra_rights_diminish:
  "x \<in> rights (extra_rights (diminish r c))
   \<Longrightarrow> x \<in> rights (extra_rights c)"
  by (auto simp: rights_extra_rights all_rights_def split:if_split_asm)

(* Lemmas on system operations *)

definition
  in_store_connected :: "state \<Rightarrow> entity_id \<Rightarrow> entity_id \<Rightarrow> bool" where
  "in_store_connected s x y \<equiv> (x, y) \<in> store_connected s"

(* Lemmas about the general operation *)

lemma direct_caps_of_generalOp:
  "direct_caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) e =
  (if e = e\<^sub>1
   then insert (diminish r (extra_rights c)) (direct_caps_of s (e\<^sub>1))
   else direct_caps_of s e)"
  by (clarsimp simp: generalOperation_def direct_caps_of_def split:option.splits)

lemma direct_caps_of_generalOp2:
  "\<lbrakk>c' \<in> direct_caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x\<rbrakk> \<Longrightarrow>
   c' \<in> direct_caps_of s x \<or> (c' \<in>cap {c} \<and> x = e\<^sub>1)"
  apply (clarsimp simp: direct_caps_of_generalOp extra_rights_diminish
           split:if_split_asm)
  apply (drule extra_rights_diminish)
  by simp

lemma store_connected_direct_generalOp:
  "\<lbrakk>(x, y) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s)\<rbrakk> \<Longrightarrow>
   (x, y) \<in> store_connected_direct s \<or>
   (x = e\<^sub>1 \<and> y = target c \<and> Store \<in> rights (extra_rights c))"
  by (auto simp: store_connected_direct_def direct_caps_of_generalOp all_rights_def
          split: if_split_asm)

lemma store_connected_generalOp:
  "\<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s)\<rbrakk> \<Longrightarrow>
   (x, y) \<in> store_connected s \<or>
   ((x, e\<^sub>1) \<in> store_connected s \<and>
   (e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<and>
   (target c, y) \<in> store_connected s)"
  apply (unfold store_connected_def)
  apply (erule rtrancl_induct)
   apply clarsimp
  apply (clarsimp)
  apply (fold store_connected_def)
  apply (subgoal_tac "(y, z) \<in> store_connected_direct s")
   apply (clarsimp simp: store_connected_def)
   apply (erule disjE)
    apply fastforce
   apply clarsimp
   apply (erule notE)
   apply fastforce
  apply (frule store_connected_direct_generalOp)
  apply (clarsimp simp: store_connected_def)
  done


lemma store_connected_generalOp_not_new:
  "\<lbrakk>(e\<^sub>1, target c) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s);
   c \<in> caps_of s e\<^sub>0\<rbrakk> \<Longrightarrow>
   (e\<^sub>1, target c) \<in> store_connected_direct s \<or>
   (e\<^sub>0, target c) \<in> store_connected s \<or>
   Create \<in> rights c"
  apply (drule store_connected_direct_generalOp)
  apply (clarsimp simp: rights_extra_rights split:if_split_asm)
   apply (drule (1) store_caps_store_connected, simp)
  done

lemma store_connected_generalOp2:
  "\<lbrakk>(x, y) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s);
   c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1\<rbrakk> \<Longrightarrow>
   s \<turnstile> x \<leftrightarrow>* y"
  apply (drule store_connected_generalOp)
  apply (erule disjE)
   apply (simp add: tgs_connected_def)
   apply (drule store_connected_directly_tgs_connected, simp)
  apply clarsimp
  apply (drule store_connected_directly_tgs_connected [where x=x and y=e\<^sub>1])
  apply (drule store_connected_directly_tgs_connected [where x="target c" and y=y])
  apply (drule (1) store_connected_generalOp_not_new)
  apply (erule disjE)
   apply (drule store_connected_direct_in_store_connected)
   apply (drule store_connected_directly_tgs_connected [where x=e\<^sub>1 and y="target c"])
   apply (simp add: tgs_connected_def)
  apply (drule directly_tgs_connected_comm [where x="e\<^sub>0" and y="e\<^sub>1"])
  apply (erule disjE)
   apply (drule store_connected_directly_tgs_connected [where x=e\<^sub>0 and y="target c"])
   apply (simp add: tgs_connected_def)
  apply (drule (1) create_caps_directly_tgs_connected)
  apply (simp add: tgs_connected_def)
  done

lemma shares_caps_of_generalOp:
  "\<lbrakk>shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y;
   c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1\<rbrakk>
  \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y"
  apply (clarsimp simp: shares_caps_def)
  apply (frule (2) store_connected_generalOp2 [where x=x])
  apply (drule (2) store_connected_generalOp2 [where x=y])
  apply (drule tgs_connected_comm [where x=y])
  apply (simp add: tgs_connected_def)
  done

lemma caps_of_generalOp:
  "\<lbrakk>c' \<in> caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x;
   c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1\<rbrakk>
  \<Longrightarrow> \<exists>z. (x,z) \<in> tgs_connected s \<and> c' \<in>cap caps_of s z"
  apply (simp add: caps_of_def[where e=x])
  apply clarsimp
  apply (frule (2) store_connected_generalOp2)
  apply (drule direct_caps_of_generalOp2)
  apply (erule disjE)
   apply (drule direct_cap_in_cap)
   apply (fastforce simp: cap_in_caps_def)
  apply (subgoal_tac "s \<turnstile> x \<leftrightarrow>* e\<^sub>0")
   apply (subgoal_tac "c' \<in>cap caps_of s e\<^sub>0")
    apply fastforce
   apply (fastforce simp: cap_in_caps_def)
  apply clarsimp
  apply (drule directly_tgs_connected_comm [where x="e\<^sub>0" and y="e\<^sub>1"])
  apply (simp add: tgs_connected_def)
  done

lemma take_cap_generalOp:
  "\<lbrakk>take_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x;
   c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1\<rbrakk>
  \<Longrightarrow> \<exists>z.  s \<turnstile> x \<leftrightarrow>* z \<and> take_cap y \<in>cap caps_of s z"
  apply (simp add: cap_in_caps_def)
  apply clarsimp
  apply (drule (2) caps_of_generalOp)
  apply (fastforce simp: cap_in_caps_def)
  done

lemma grant_cap_generalOp:
  "\<lbrakk>grant_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x;
   c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1\<rbrakk>
  \<Longrightarrow> \<exists>z.  s \<turnstile> x \<leftrightarrow>* z \<and> grant_cap y \<in>cap caps_of s z"
  apply (simp add: cap_in_caps_def)
  apply clarsimp
  apply (drule (2) caps_of_generalOp)
  apply (fastforce simp: cap_in_caps_def)
  done

lemma take_cap_generalOp2:
  "\<lbrakk>take_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x;
   c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1\<rbrakk>
  \<Longrightarrow> (x, y) \<in> tgs_connected s"
  apply (drule (2) take_cap_generalOp)
  apply clarsimp
  apply (subgoal_tac "s \<turnstile> z \<leftrightarrow> y")
   apply (simp add: tgs_connected_def)
  apply (simp add: directly_tgs_connected_def leak_def)
  done

lemma grant_cap_generalOp2:
  "\<lbrakk>grant_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x;
   c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1\<rbrakk>
  \<Longrightarrow> (x, y) \<in> tgs_connected s"
  apply (drule (2) grant_cap_generalOp)
  apply clarsimp
  apply (subgoal_tac "s \<turnstile> z \<leftrightarrow> y")
   apply (simp add: tgs_connected_def)
  apply (simp add: directly_tgs_connected_def leak_def)
  done

lemma generalOp_directly_tgs_connected:
 "\<lbrakk>generalOperation e\<^sub>0 e\<^sub>1 c r s \<turnstile> x \<leftrightarrow> y;
   c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1\<rbrakk>
  \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y"
  apply (simp add: directly_tgs_connected_def [where s="generalOperation e\<^sub>0 e\<^sub>1 c r s"] leak_def)
  apply safe
       apply (rule tgs_connected_comm)
       apply (drule (3) take_cap_generalOp2)
      apply (drule (3) grant_cap_generalOp2)
     apply (erule (2) shares_caps_of_generalOp)
    apply (drule (3) take_cap_generalOp2)
   apply (rule tgs_connected_comm)
   apply (drule (3) grant_cap_generalOp2)
  apply (erule (2) shares_caps_of_generalOp)
  done



(* results from general operation *)

lemma create_legal_directly_tgs_connected:
  "legal (SysCreate e c\<^sub>1 c\<^sub>2) s \<Longrightarrow> s  \<turnstile> target c\<^sub>1 \<leftrightarrow> e"
  apply clarsimp
  apply (rule directly_tgs_connected_comm)
  apply (drule (1) create_caps_directly_tgs_connected)
  apply (drule (1) store_caps_store_connected)
  apply (drule (1) store_connected_directly_tgs_connected)
  done

lemma take_legal_directly_tgs_connected:
  "legal (SysTake e c\<^sub>1 c\<^sub>2 r) s \<Longrightarrow> s  \<turnstile> target c\<^sub>1 \<leftrightarrow> e"
  apply clarsimp
  apply (rule directly_tgs_connected_comm)
  apply (drule (2) take_caps_directly_tgs_connected)
  done

lemma grant_legal_directly_tgs_connected:
  "legal (SysGrant e c\<^sub>1 c\<^sub>2 r) s \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c\<^sub>1"
  apply clarsimp
  apply (drule (2) grant_caps_directly_tgs_connected)
  done

lemma copy_legal_directly_tgs_connected:
  "legal (SysCopy e c\<^sub>1 c\<^sub>2 r) s \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c\<^sub>1"
  apply clarsimp
  apply (drule (1) store_caps_store_connected)
  apply (drule (1) store_connected_directly_tgs_connected)
  done

lemma caps_of_create:
  "\<lbrakk>c' \<in> caps_of (createOperation e c\<^sub>1 c\<^sub>2 s) x; legal (SysCreate e c\<^sub>1 c\<^sub>2) s\<rbrakk>
  \<Longrightarrow> \<exists>z. (x,z) \<in> tgs_connected s \<and> c' \<in>cap caps_of s z"
  apply (frule create_legal_directly_tgs_connected)
  apply (clarsimp simp: create_general)
  apply (drule caps_of_make_entity2 [rotated], clarsimp)
  apply (drule (1) caps_of_generalOp)
   apply (drule (2) directly_tgs_connected_comm)
  done

lemma caps_of_take:
  "\<lbrakk>c' \<in> caps_of (takeOperation e c\<^sub>1 c\<^sub>2 r s) x; legal (SysTake e c\<^sub>1 c\<^sub>2 r) s\<rbrakk>
  \<Longrightarrow> \<exists>z. (x,z) \<in> tgs_connected s \<and> c' \<in>cap caps_of s z"
  apply (frule take_legal_directly_tgs_connected)
  apply (clarsimp simp: take_general)
  apply (drule (2) caps_of_generalOp)
   apply (drule (1) directly_tgs_connected_comm)
  done

lemma caps_of_grant:
  "\<lbrakk>c' \<in> caps_of (grantOperation e c\<^sub>1 c\<^sub>2 r s) x; legal (SysGrant e c\<^sub>1 c\<^sub>2 r) s\<rbrakk>
  \<Longrightarrow> \<exists>z. (x,z) \<in> tgs_connected s \<and> c' \<in>cap caps_of s z"
  apply (frule grant_legal_directly_tgs_connected)
  apply (clarsimp simp: grant_general)
  apply (drule (2) caps_of_generalOp)
   apply (drule (1) directly_tgs_connected_comm)
  done

lemma caps_of_copy:
  "\<lbrakk>c' \<in> caps_of (copyOperation e c\<^sub>1 c\<^sub>2 r s) x; legal (SysCopy e c\<^sub>1 c\<^sub>2 r) s\<rbrakk>
  \<Longrightarrow> \<exists>z. (x,z) \<in> tgs_connected s \<and> c' \<in>cap caps_of s z"
  apply (frule copy_legal_directly_tgs_connected)
  apply (clarsimp simp: copy_general)
  apply (drule (2) caps_of_generalOp)
   apply (drule (1) directly_tgs_connected_comm)
  done

lemma create_directly_tgs_connected:
 "\<lbrakk>createOperation e c\<^sub>1 c\<^sub>2 s \<turnstile> x \<leftrightarrow> y; legal (SysCreate e c\<^sub>1 c\<^sub>2) s\<rbrakk>
  \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y"
  apply (frule create_legal_directly_tgs_connected)
  apply (clarsimp simp: create_general)
  apply (drule directly_tgs_connected_make_entity2 [rotated], clarsimp)
  apply (drule (1) generalOp_directly_tgs_connected)
   apply (drule (2) directly_tgs_connected_comm)
  done

lemma take_directly_tgs_connected:
 "\<lbrakk>takeOperation e c\<^sub>1 c\<^sub>2 r s \<turnstile> x \<leftrightarrow> y; legal (SysTake e c\<^sub>1 c\<^sub>2 r) s\<rbrakk>
  \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y"
  apply (frule take_legal_directly_tgs_connected)
  apply (clarsimp simp: take_general)
  apply (drule (3) generalOp_directly_tgs_connected)
  done

lemma grant_directly_tgs_connected:
 "\<lbrakk>grantOperation e c\<^sub>1 c\<^sub>2 r s \<turnstile> x \<leftrightarrow> y; legal (SysGrant e c\<^sub>1 c\<^sub>2 r) s\<rbrakk>
  \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y"
  apply (frule grant_legal_directly_tgs_connected)
  apply (clarsimp simp: grant_general)
  apply (drule (3) generalOp_directly_tgs_connected)
  done

lemma copy_directly_tgs_connected:
 "\<lbrakk>copyOperation e c\<^sub>1 c\<^sub>2 r s \<turnstile> x \<leftrightarrow> y; legal (SysCopy e c\<^sub>1 c\<^sub>2 r) s\<rbrakk>
  \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y"
  apply (frule copy_legal_directly_tgs_connected)
  apply (clarsimp simp: copy_general)
  apply (drule (3) generalOp_directly_tgs_connected)
  done



lemma create_conTrans:
  "\<lbrakk>s' \<in> step cmd s; (x, y) \<in> directly_tgs_connected s'; cmd = (SysCreate e c\<^sub>1 c\<^sub>2)\<rbrakk>
  \<Longrightarrow> (x, y) \<in> tgs_connected s"
  apply(clarsimp simp: step_def split: if_split_asm)
   apply (erule disjE, fastforce simp: tgs_connected_def, clarsimp)
   apply (drule create_directly_tgs_connected, clarsimp, assumption)
  apply (simp add: tgs_connected_def)
  done

lemma take_conTrans:
  "\<lbrakk>s' \<in> step cmd s; (x, y) \<in> directly_tgs_connected s'; cmd = (SysTake e c\<^sub>1 c\<^sub>2 r)\<rbrakk>
  \<Longrightarrow> (x, y) \<in> tgs_connected s"
  apply(clarsimp simp: step_def split: if_split_asm)
   apply (erule disjE, fastforce simp: tgs_connected_def, clarsimp)
   apply (drule take_directly_tgs_connected, clarsimp, assumption)
  apply (simp add: tgs_connected_def)
  done

lemma grant_conTrans:
  "\<lbrakk>s' \<in> step cmd s; (x, y) \<in> directly_tgs_connected s'; cmd = (SysGrant e c\<^sub>1 c\<^sub>2 r)\<rbrakk>
  \<Longrightarrow> (x, y) \<in> tgs_connected s"
  apply(clarsimp simp: step_def split: if_split_asm)
   apply (erule disjE, fastforce simp: tgs_connected_def, clarsimp)
   apply (drule grant_directly_tgs_connected, clarsimp, assumption)
  apply (simp add: tgs_connected_def)
  done

lemma copy_conTrans:
  "\<lbrakk>s' \<in> step cmd s; (x, y) \<in> directly_tgs_connected s'; cmd = (SysCopy e c\<^sub>1 c\<^sub>2 r)\<rbrakk>
  \<Longrightarrow> (x, y) \<in> tgs_connected s"
  apply(clarsimp simp: step_def split: if_split_asm)
   apply (erule disjE, fastforce simp: tgs_connected_def, clarsimp)
   apply (drule copy_directly_tgs_connected, clarsimp, assumption)
  apply (simp add: tgs_connected_def)
  done

(* Lemmas about destroy *)

lemma direct_caps_of_destroy:
  "c \<in> direct_caps_of (s(e := None)) x \<Longrightarrow> c \<in> direct_caps_of s x"
  by (simp add: direct_caps_of_def split: option.splits split: if_split_asm)

lemma store_connected_destroy:
 "(x, y) \<in> store_connected (s(e := None)) \<Longrightarrow> (x, y) \<in> store_connected s"
  apply (simp add: store_connected_def)
  apply (erule rtrancl_induct)
   apply simp
  apply (fold store_connected_def)
  apply (subgoal_tac "(y,z) \<in> store_connected_direct s")
   apply (fastforce simp: store_connected_def)
  apply (simp add: store_connected_direct_def)
  apply clarsimp
  by (metis direct_caps_of_destroy)

lemma shares_caps_destroy:
  "shares_caps (destroyOperation e c s) x y
  \<Longrightarrow> shares_caps s x y"
  apply (clarsimp simp: shares_caps_def destroyOperation_def)
  apply (frule store_connected_destroy [where x=x])
  apply (drule store_connected_destroy [where x=y])
  by auto

lemma caps_of_destroy:
  "c \<in> caps_of (destroyOperation e' c' s) e \<Longrightarrow>
  c \<in> caps_of s e"
  apply (clarsimp simp add: destroyOperation_def caps_of_def)
  apply (rule_tac x=x in exI)
  apply (drule direct_caps_of_destroy)
  apply simp
  apply (erule store_connected_destroy)
  done

lemma destroy_directly_tgs_connected:
  "\<lbrakk>s' \<in> step (SysDestroy e c) s; (x, y) \<in> directly_tgs_connected s'\<rbrakk> \<Longrightarrow>
  (x, y) \<in> directly_tgs_connected s"
  apply(clarsimp simp: step_def split: if_split_asm)
  apply(erule disjE, simp)
  apply(simp add: directly_tgs_connected_def leak_def)
  apply (erule disjE)
   apply(fastforce simp add: cap_in_caps_def dest!: caps_of_destroy)
  apply (erule disjE)
   apply(fastforce simp add: cap_in_caps_def dest!: caps_of_destroy)
  apply (erule disjE)
   apply (drule shares_caps_destroy, simp)
  apply (erule disjE)
   apply(fastforce simp add: cap_in_caps_def dest!: caps_of_destroy)
  apply (erule disjE)
   apply(fastforce simp add: cap_in_caps_def dest!: caps_of_destroy)
  apply (drule shares_caps_destroy, simp)
  done

lemma destroy_conTrans:
  "\<lbrakk>s' \<in> step cmd s; (x, y) \<in> directly_tgs_connected s'; cmd = (SysDestroy e c)\<rbrakk>
  \<Longrightarrow> (x, y) \<in>  directly_tgs_connected s"
  by(auto dest!: destroy_directly_tgs_connected)


(* lemmas about remove *)

lemma direct_caps_of_remove:
  "c \<in> direct_caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x \<Longrightarrow>
  c \<in> direct_caps_of s x"
  by (clarsimp simp: removeOperation_simpler direct_caps_of_def
              split: option.splits if_split_asm)

lemma direct_caps_of_remove_eq:
  "direct_caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x =
  ( if   is_entity s (target c\<^sub>1) \<and> x = target c\<^sub>1
   then  direct_caps_of s (target c\<^sub>1) - {c\<^sub>2}
   else  direct_caps_of s x )"
  by(simp add: direct_caps_of_def is_entity_def removeOperation_def)

lemma store_connected_remove [rule_format]:
  "(x, y) \<in> store_connected (s(e \<mapsto> Entity C')) \<Longrightarrow>
  s e = Some (Entity C) \<longrightarrow> C' \<subseteq> C \<longrightarrow> (x, y) \<in> store_connected s"
  apply (unfold store_connected_def)
  apply (erule rtrancl_induct)
   apply simp
  apply clarsimp
  apply (subgoal_tac "(y,z) \<in> store_connected_direct s")
   apply (erule rtrancl_trans)
   apply fastforce
  apply (fold store_connected_def)
  apply (clarsimp simp add: store_connected_direct_def)
  apply (fastforce simp: direct_caps_of_def
                  split: option.splits if_split_asm)
  done

lemma caps_of_remove:
  "c \<in> caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x \<Longrightarrow>
  c \<in> caps_of s x"
  apply (clarsimp simp: caps_of_def)
  apply (rule_tac x=xa in exI)
  apply (drule direct_caps_of_remove)
  apply (simp add: removeOperation_simpler
            split: option.splits)
  apply (erule (1) store_connected_remove)
  apply blast
  done

(* Might equal either  "caps s (target c\<^sub>1) - {c\<^sub>2}" or "caps s x" depending if the caps are duplicated.*)
lemma caps_of_remove2:
  "caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x \<subseteq> caps_of s x"
  apply(simp add: caps_of_def is_entity_def removeOperation_def direct_caps_of_def)
  apply (clarsimp split: if_split_asm)
   apply (auto dest!: store_connected_remove)
  done

lemma shares_caps_remove:
  "shares_caps (removeOperation e c\<^sub>1 c\<^sub>2 s) x y
  \<Longrightarrow> shares_caps s x y"
  apply (clarsimp simp: shares_caps_def removeOperation_simpler
                 split:option.splits)
  apply (frule (1) store_connected_remove [where x=x], clarsimp)
  apply (drule (1) store_connected_remove [where x=y], clarsimp)
  by auto

lemma remove_directly_tgs_connected:
  "\<lbrakk>s' \<in> step (SysRemove e c\<^sub>1 c\<^sub>2) s; (x, y) \<in> directly_tgs_connected s'\<rbrakk> \<Longrightarrow>
  (x, y) \<in> directly_tgs_connected s"
  apply(simp add: step_def split: if_split_asm)
  apply(erule disjE, simp)
  apply(simp add: directly_tgs_connected_def leak_def)
  apply(simp add: cap_in_caps_def)
  apply(clarsimp)
  apply safe
     prefer 3
     apply (drule shares_caps_remove, simp)
    prefer 5
    apply (drule shares_caps_remove, simp)
   apply(auto dest!: caps_of_remove)
  done

lemma remove_conTrans:
  "\<lbrakk>s' \<in> step cmd s; (x, y) \<in> directly_tgs_connected s'; cmd = (SysRemove e c\<^sub>1 c\<^sub>2)\<rbrakk>
  \<Longrightarrow> (x, y) \<in>  directly_tgs_connected s"
  by(auto dest!: remove_directly_tgs_connected)

lemma direct_caps_of_removeSet:
  "c' \<in> direct_caps_of (removeSetOperation e c C s) x \<Longrightarrow>
  c' \<in> direct_caps_of s x"
  by (clarsimp simp: removeSetOperation_simpler direct_caps_of_def
              split: option.splits if_split_asm)

lemma caps_of_removeSet:
  "c' \<in> caps_of (removeSetOperation e c C s) x \<Longrightarrow>
  c' \<in> caps_of s x"
  apply (clarsimp simp: caps_of_def)
  apply (rule_tac x=xa in exI)
  apply (drule direct_caps_of_removeSet)
  apply (simp add: removeSetOperation_simpler split: option.splits)
  apply (erule (1) store_connected_remove)
  apply blast
  done

lemma shares_caps_removeSet:
  "shares_caps (removeSetOperation e c C s) x y
  \<Longrightarrow> shares_caps s x y"
  apply (clarsimp simp: shares_caps_def removeSetOperation_simpler split:option.splits)
  apply (frule (1) store_connected_remove [where x=x], clarsimp)
  apply (drule (1) store_connected_remove [where x=y], clarsimp)
  by auto

lemma removeSet_connected:
  " \<lbrakk>s' \<in> step (SysRemoveSet e c C) s; s' \<turnstile> x \<leftrightarrow> y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y"
  apply(simp add: step_def split: if_split_asm)
  apply(erule disjE, simp)
  apply(simp add: directly_tgs_connected_def leak_def)
  apply(simp add: cap_in_caps_def)
  apply(clarsimp)
  apply safe
     prefer 3
     apply (drule shares_caps_removeSet, simp)
    prefer 5
    apply (drule shares_caps_removeSet, simp)
   apply (auto dest!: caps_of_removeSet)
  done

lemma removeSet_conTrans:
  "\<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leftrightarrow> y; cmd = (SysRemoveSet n c C)\<rbrakk>
  \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y"
  by(auto dest!: removeSet_connected)

(* lemmas about revoke *)
lemma direct_caps_of_removeSetOfCaps:
  "c' \<in> direct_caps_of (removeSetOfCaps cap_map s) x \<Longrightarrow>
  c' \<in> direct_caps_of s x"
  by (clarsimp simp: removeSetOfCaps_def direct_caps_of_def
              split: option.splits if_split_asm)
thm store_connected_remove

lemma store_connected_removeSetOfCaps:
  "(x, y) \<in> store_connected (\<lambda>e. if is_entity s e
                                 then Some (Entity (direct_caps_of s e - cap_map e))
                                 else None) \<Longrightarrow>
    (x, y) \<in> store_connected s"
  apply (unfold store_connected_def)
  apply (erule rtrancl_induct)
   apply simp
  apply (subgoal_tac "(y,z) \<in> store_connected_direct s")
   apply (erule rtrancl_trans)
   apply fastforce
  apply (fold store_connected_def)
  apply (clarsimp simp add: store_connected_direct_def)
  apply (fastforce simp: direct_caps_of_def
                  split: option.splits if_split_asm)
  done

lemma caps_of_removeSetOfCaps:
  "c' \<in> caps_of (removeSetOfCaps cap_map s) x \<Longrightarrow>
  c' \<in> caps_of s x"
  apply (clarsimp simp: caps_of_def)
  apply (rule_tac x=xa in exI)
  apply (drule direct_caps_of_removeSetOfCaps)
  apply (simp add: removeSetOfCaps_def split: option.splits)
  apply (erule store_connected_removeSetOfCaps)
  done

lemma caps_of_revoke:
  "\<lbrakk>s' \<in> revokeOperation sub c\<^sub>1 s ;  c \<in> caps_of s' e \<rbrakk>
  \<Longrightarrow> c \<in> caps_of s e"
  apply (clarsimp simp: revokeOperation_def
                 split: if_split_asm)
  apply (drule (1) caps_of_removeSetOfCaps)
  done

lemma direct_caps_of_revoke:
  "\<lbrakk>s' \<in> revokeOperation e c s; c' \<in> direct_caps_of s' x\<rbrakk>
   \<Longrightarrow> c' \<in> direct_caps_of s x"
  apply (clarsimp simp: revokeOperation_def
                 split: if_split_asm)
  apply (drule (1) direct_caps_of_removeSetOfCaps)
  done

lemma store_connected_revoke:
 "\<lbrakk>(x, y) \<in> store_connected s'; s' \<in> revokeOperation e c s\<rbrakk>
  \<Longrightarrow> (x, y) \<in> store_connected s"
  apply (simp add: store_connected_def)
  apply (erule rtrancl_induct)
   apply simp
  apply (fold store_connected_def)
  apply (subgoal_tac "(y,z) \<in> store_connected_direct s")
   apply (fastforce simp: store_connected_def)
  apply (clarsimp simp: store_connected_direct_def)
  apply (metis direct_caps_of_revoke)
  done

lemma shares_caps_revoke:
  "\<lbrakk>shares_caps s' x y; s' \<in> revokeOperation e c s\<rbrakk>
  \<Longrightarrow> shares_caps s x y"
  apply (clarsimp simp: shares_caps_def)
  apply (frule (1) store_connected_revoke [where x=x])
  apply (drule (1) store_connected_revoke [where x=y])
  by auto

lemma removeOperation_entity_ids [simp]:
  "is_entity (removeOperation e c c' s) e' = is_entity s e'"
  by (simp add: is_entity_def removeOperation_def)

lemma removeSetOfCaps_entity_ids [simp]:
  "is_entity (removeSetOfCaps cap_map s) e' = is_entity s e'"
  by (simp add: is_entity_def removeSetOfCaps_def)

lemma revoke_entities:
  "s' \<in> revokeOperation sub c\<^sub>1 s \<Longrightarrow> is_entity s' e = is_entity s e"
  by (clarsimp simp: revokeOperation_def split: if_split_asm)

lemma revoke_directly_tgs_connected:
  "\<lbrakk>s' \<in> step (SysRevoke n c\<^sub>1) s; (x, y) \<in> directly_tgs_connected s'\<rbrakk>
  \<Longrightarrow> (x, y) \<in>  directly_tgs_connected s"
  apply (simp add: step_def split: if_split_asm)
  apply (erule disjE, simp)
  apply (simp add: directly_tgs_connected_def leak_def)
  apply (erule disjE)
   apply(auto simp add: cap_in_caps_def dest!: caps_of_revoke)[1]
  apply (erule disjE)
   apply(auto simp add: cap_in_caps_def dest!: caps_of_revoke)[1]
  apply (erule disjE)
   apply (drule (1) shares_caps_revoke, simp)
  apply (erule disjE)
   apply(auto simp add: cap_in_caps_def dest!: caps_of_revoke)[1]
  apply (erule disjE)
   apply(auto simp add: cap_in_caps_def dest!: caps_of_revoke)[1]
  apply (drule (1) shares_caps_revoke, simp)
  done

lemma revoke_conTrans:
  "\<lbrakk>s' \<in> step cmd s; (x, y) \<in> directly_tgs_connected s'; cmd = (SysRevoke n c\<^sub>1)\<rbrakk>
  \<Longrightarrow> (x, y) \<in>  directly_tgs_connected s"
  by(auto dest!: revoke_directly_tgs_connected)



(* lemmas about grant *)

lemma is_entity_grant [simp]:
  "is_entity s (target c\<^sub>1) \<Longrightarrow>
  is_entity (grantOperation e c\<^sub>1 c\<^sub>2 r s) e' = is_entity s e'"
  by (simp add: is_entity_def grantOperation_def)

lemma is_entity_destroy:
  "is_entity (destroyOperation e' c s) e \<Longrightarrow> is_entity s e"
  by (simp add: destroyOperation_def is_entity_def split: if_split_asm)


(********************************************
 ********************************************
 ***** Connected transitively preserved *****
 ********************************************
 ********************************************)

lemma connected_tgs_connected:
  "\<lbrakk>s' \<in> step cmd s; (e\<^sub>x, e\<^sub>y) \<in> directly_tgs_connected s'\<rbrakk> \<Longrightarrow>
  (e\<^sub>x, e\<^sub>y) \<in> tgs_connected s"
  apply(case_tac "(e\<^sub>x, e\<^sub>y) \<in> directly_tgs_connected s")
   apply(simp add: tgs_connected_def)
   apply(case_tac cmd)
         apply(rule create_conTrans, fastforce+)
        apply(rule take_conTrans, fastforce+)
       apply(rule grant_conTrans, fastforce+)
      apply(frule copy_conTrans, fastforce+)
     apply(frule remove_conTrans, fastforce+)
    apply(frule removeSet_conTrans, fastforce+)
   apply(frule revoke_conTrans, fastforce+)
  apply(frule destroy_conTrans, fastforce+)
  done

lemma tgs_connected_preserved_step:
  "\<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leftrightarrow>* z\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* z"
  thm rtrancl_induct [where r="directly_tgs_connected s'" and a=x and b=z and P="\<lambda>z. (x, z) \<in> (directly_tgs_connected s)\<^sup>*", simplified,
                      simplified tgs_connected_def [symmetric]]
  apply(erule rtrancl_induct [where r="directly_tgs_connected s'",
                              simplified tgs_connected_def [symmetric]], simp)
  apply(case_tac "s \<turnstile> y \<leftrightarrow>* z")
   apply (erule (1) tgs_connected_trans)
  apply (simp add: connected_tgs_connected)
  done

lemma leakImplyConnected:
  "leak s\<^sub>i e\<^sub>x e\<^sub>i \<Longrightarrow> (e\<^sub>x, e\<^sub>i) \<in> directly_tgs_connected s\<^sub>i"
 by(simp add: directly_tgs_connected_def)

lemma leakImplyConnectedTrans:
  "leak s\<^sub>i e\<^sub>x e\<^sub>i \<Longrightarrow> (e\<^sub>x, e\<^sub>i) \<in> tgs_connected s\<^sub>i"
  by(simp add: tgs_connected_def, frule leakImplyConnected, auto)


lemma tgs_connected_preserved [rule_format]:
  "\<forall>s'. s' \<in> execute cmds s \<longrightarrow>
    s' \<turnstile> x \<leftrightarrow>* y \<longrightarrow>
    s \<turnstile> x \<leftrightarrow>* y"
  apply(induct_tac cmds, simp)
  apply clarsimp
  apply(rename_tac cmd cmds s'' s')
  apply(erule_tac x=s' in allE)
  apply(simp add: tgs_connected_preserved_step)
  done

lemma leak_conTrans [rule_format]:
  "\<lbrakk>s \<in> execute cmds s\<^sub>0; leak s x y\<rbrakk>
  \<Longrightarrow> (x, y) \<in> tgs_connected s\<^sub>0"
  by (auto intro: leakImplyConnectedTrans tgs_connected_preserved)

lemma leakage_rule:
  "\<lbrakk>s' \<in> execute cmds s; \<not> s \<turnstile> x \<leftrightarrow>* y\<rbrakk> \<Longrightarrow> \<not> (s' \<turnstile> x \<rightarrow> y)"
  by(auto simp add: leak_conTrans)




(*******************************************
 *******************************************
 *****      Authority confinement     *****
 *******************************************
 *******************************************)

lemma caps_of_op:
  "\<lbrakk>s' \<in> step cmd s; c' \<in> caps_of s' x\<rbrakk>
  \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z"
  apply (simp add: step_def split:if_split_asm)
   prefer 2
   apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights)
  apply (erule disjE)
   apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights)
  apply (case_tac cmd)
         apply (simp add: caps_of_create)
        apply (simp add: caps_of_take)
       apply (simp add: caps_of_grant)
      apply (simp add: caps_of_copy)
     apply (clarsimp, drule caps_of_remove)
     apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights)
    apply (clarsimp, drule caps_of_removeSet)
    apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights)
   apply (clarsimp, drule (1) caps_of_revoke)
   apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights)
  apply (clarsimp, drule caps_of_destroy)
  apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights)
  done

lemma authority_confinement_induct_step:
  "\<lbrakk>s' \<in> step cmd s;
    \<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c\<rbrakk>
  \<Longrightarrow> caps_of s' e\<^sub>x \<le>cap c"
  apply (clarsimp simp: caps_dominated_by_def)
  apply (drule (1) caps_of_op)
  apply (fastforce simp: cap_in_caps_def)
  done

lemma authority_confinement_helper:
  "s' \<in> execute cmds s \<longrightarrow>
   (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow>
   (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c)"
proof (induct cmds arbitrary: s')
case Nil
  show ?case by clarsimp
next
case (Cons cmd cmds s')
show ?case
  apply clarsimp
  apply (rule authority_confinement_induct_step, assumption)
  apply clarsimp
  apply (rule Cons.hyps[rule_format], simp_all)
  apply (drule(1) tgs_connected_preserved_step)
  apply (simp add: tgs_connected_def)
  done
qed

lemma authority_confinement:
  "\<lbrakk>s' \<in> execute cmds s;
    \<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c\<rbrakk>
  \<Longrightarrow> caps_of s' e\<^sub>x \<le>cap c"
  by (erule authority_confinement_helper [rule_format, where e\<^sub>x=e\<^sub>x], simp_all)

end