kings-crown/FVELER_Isabelle huggingface dataset:
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target (extra_rights c) = target c
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rights (extra_rights c) = (if Create \<in> rights c then all_rights else rights c)
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((e\<^sub>x, e\<^sub>y) \<in> directly_tgs_connected s) = (s \<turnstile> e\<^sub>x \<rightarrow> e\<^sub>y \<or> s \<turnstile> e\<^sub>y \<rightarrow> e\<^sub>x)
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shares_caps s y x = shares_caps s x y
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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)
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>e. direct_caps_of s e = direct_caps_of s' e \<Longrightarrow> store_connected s = store_connected s'
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>e. direct_caps_of s e = direct_caps_of s' e \<Longrightarrow> caps_of s e = caps_of s' e
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in>cap caps_of s e; caps_of s ?e = caps_of s' ?e\<rbrakk> \<Longrightarrow> c \<in>cap caps_of s' e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>c'\<in>caps_of s e. target c = target c' \<and> rights (extra_rights c) \<subseteq> rights (extra_rights c'); caps_of s ?e = caps_of s' ?e\<rbrakk> \<Longrightarrow> \<exists>c'\<in>caps_of s' e. target c = target c' \<and> rights (extra_rights c) \<subseteq> rights (extra_rights c')
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_entity s n \<Longrightarrow> direct_caps_of (make_entity n s) e = direct_caps_of s e
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_entity s n \<Longrightarrow> caps_of (make_entity n s) e = caps_of s e proof (prove)
goal (1 subgoal):
 1. \<not> is_entity s n \<Longrightarrow> \<forall>e. direct_caps_of (make_entity n s) e = direct_caps_of s e proof (prove)
goal (1 subgoal):
 1. \<And>e. \<not> is_entity s n \<Longrightarrow> direct_caps_of (make_entity n s) e = direct_caps_of s e proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_entity s n; c \<in> caps_of (make_entity n s) e\<rbrakk> \<Longrightarrow> c \<in> caps_of s e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of (make_entity n s) e; caps_of (make_entity n s) ?e = caps_of s ?e\<rbrakk> \<Longrightarrow> c \<in> caps_of s e proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_entity s n \<Longrightarrow> make_entity n s \<turnstile> x \<leftrightarrow> y = s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<not> is_entity s n \<Longrightarrow> \<forall>e. direct_caps_of (make_entity n s) e = direct_caps_of s e proof (prove)
goal (1 subgoal):
 1. \<And>e. \<not> is_entity s n \<Longrightarrow> direct_caps_of (make_entity n s) e = direct_caps_of s e proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> is_entity s n; make_entity n s \<turnstile> x \<leftrightarrow> y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>make_entity n s \<turnstile> x \<leftrightarrow> y; make_entity n s \<turnstile> ?x \<leftrightarrow> ?y = s \<turnstile> ?x \<leftrightarrow> ?y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. diminish (rights c) (extra_rights c) = c
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. diminish (r \<inter> rights c) (extra_rights c) = diminish r c proof (prove)
goal (1 subgoal):
 1. (Create \<in> rights c \<longrightarrow> c\<lparr>rights := r \<inter> rights c\<rparr> = c\<lparr>rights := rights c \<inter> r\<rparr>) \<and> (Create \<notin> rights c \<longrightarrow> c\<lparr>rights := rights c \<inter> (r \<inter> rights c)\<rparr> = c\<lparr>rights := rights c \<inter> r\<rparr>) proof (prove)
goal (1 subgoal):
 1. Create \<notin> rights c \<longrightarrow> c\<lparr>rights := rights c \<inter> (r \<inter> rights c)\<rparr> = c\<lparr>rights := r \<inter> rights c\<rparr> proof (prove)
goal (2 subgoals):
 1. rights c \<inter> (r \<inter> rights c) = r \<inter> rights c \<Longrightarrow> Create \<notin> rights c \<longrightarrow> c\<lparr>rights := rights c \<inter> (r \<inter> rights c)\<rparr> = c\<lparr>rights := r \<inter> rights c\<rparr>
 2. rights c \<inter> (r \<inter> rights c) = r \<inter> rights c proof (prove)
goal (1 subgoal):
 1. rights c \<inter> (r \<inter> rights c) = r \<inter> rights c proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Create \<in> rights c\<^sub>2 \<Longrightarrow> \<lparr>target = target c\<^sub>2, rights = UNIV\<rparr> = c\<^sub>2\<lparr>rights := UNIV\<rparr>
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. extra_rights (full_cap e) = full_cap e
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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)
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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)
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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
theory Confine_S

lemma directly_tgs_connected_comm:
  "s \<turnstile> x \<leftrightarrow> y \<Longrightarrow> s \<turnstile> y \<leftrightarrow> x" by(auto simp: directly_tgs_connected_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> x \<leftrightarrow> y \<Longrightarrow> s \<turnstile> y \<leftrightarrow> x
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> x \<leftrightarrow>* x
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> x \<leftrightarrow>* y \<Longrightarrow> s \<turnstile> y \<leftrightarrow>* x proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> (directly_tgs_connected s)\<^sup>* \<Longrightarrow> (y, x) \<in> (directly_tgs_connected s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (directly_tgs_connected s)\<^sup>*; s \<turnstile> y \<leftrightarrow> z; (y, x) \<in> (directly_tgs_connected s)\<^sup>*\<rbrakk> \<Longrightarrow> (z, x) \<in> (directly_tgs_connected s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (directly_tgs_connected s)\<^sup>*; s \<turnstile> y \<leftrightarrow> z; (y, x) \<in> (directly_tgs_connected s)\<^sup>*; s \<turnstile> z \<leftrightarrow> y\<rbrakk> \<Longrightarrow> (z, x) \<in> (directly_tgs_connected s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> (directly_tgs_connected s)\<^sup>*; s \<turnstile> y \<leftrightarrow> z; (y, x) \<in> (directly_tgs_connected s)\<^sup>*; \<not> s \<turnstile> z \<leftrightarrow> y\<rbrakk> \<Longrightarrow> (z, x) \<in> (directly_tgs_connected s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (directly_tgs_connected s)\<^sup>*; s \<turnstile> y \<leftrightarrow> z; (y, x) \<in> (directly_tgs_connected s)\<^sup>*; \<not> s \<turnstile> z \<leftrightarrow> y\<rbrakk> \<Longrightarrow> (z, x) \<in> (directly_tgs_connected s)\<^sup>* proof (prove)
goal:
No subgoals!
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e; Take \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e; Create \<in> rights c\<rbrakk> \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> store_connected s \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (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)
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (c \<in>cap {c'}) = (target c = target c' \<and> rights (extra_rights c) \<subseteq> rights (extra_rights c'))
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {} \<le>cap c
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> rights (extra_rights (diminish r c)) \<Longrightarrow> x \<in> rights (extra_rights c)
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 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)
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c' \<in> direct_caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x \<Longrightarrow> c' \<in> direct_caps_of s x \<or> c' \<in>cap {c} \<and> x = e\<^sub>1 proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x = e\<^sub>1; diminish r (extra_rights c) \<notin> direct_caps_of s e\<^sub>1; diminish r (extra_rights c) \<notin>cap {}; c' = diminish r (extra_rights c); xa \<in> rights (extra_rights (diminish r (extra_rights c)))\<rbrakk> \<Longrightarrow> xa \<in> rights (extra_rights c) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x = e\<^sub>1; diminish r (extra_rights c) \<notin> direct_caps_of s e\<^sub>1; diminish r (extra_rights c) \<notin>cap {}; c' = diminish r (extra_rights c); xa \<in> rights (extra_rights (extra_rights c))\<rbrakk> \<Longrightarrow> xa \<in> rights (extra_rights c)
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> store_connected_direct (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<Longrightarrow> (x, y) \<in> store_connected_direct s \<or> x = e\<^sub>1 \<and> y = target c \<and> Store \<in> rights (extra_rights c)
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; (e\<^sub>1, target c) \<in> store_connected_direct s \<or> e\<^sub>1 = e\<^sub>1 \<and> target c = target c \<and> Store \<in> rights (extra_rights c)\<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 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; Create \<notin> rights c; (e\<^sub>0, target c) \<notin> store_connected s; Store \<in> rights c\<rbrakk> \<Longrightarrow> (e\<^sub>1, target c) \<in> store_connected_direct s proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, e\<^sub>i) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, e\<^sub>i) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s)\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, e\<^sub>i) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); (y, e\<^sub>i) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* e\<^sub>i\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, e\<^sub>i) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> y \<leftrightarrow>* e\<^sub>i\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, e\<^sub>i) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> e\<^sub>i \<leftrightarrow>* y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!