kings-crown/FVELER_Isabelle huggingface dataset:
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>createOperation e c\<^sub>1 c\<^sub>2 s \<turnstile> x \<leftrightarrow> y; legal (SysCreate e c\<^sub>1 c\<^sub>2) s; s \<turnstile> target c\<^sub>1 \<leftrightarrow> e\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>make_entity (target c\<^sub>2) (generalOperation e (target c\<^sub>1) c\<^sub>2 all_rights s) \<turnstile> x \<leftrightarrow> y; s \<turnstile> target c\<^sub>1 \<leftrightarrow> e; is_entity s e; is_entity s (target c\<^sub>1); \<not> is_entity s (target c\<^sub>2); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s e; Write \<in> rights c\<^sub>1; Store \<in> rights c\<^sub>1; Create \<in> rights c\<^sub>2\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> target c\<^sub>1 \<leftrightarrow> e; is_entity s e; is_entity s (target c\<^sub>1); \<not> is_entity s (target c\<^sub>2); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s e; Write \<in> rights c\<^sub>1; Store \<in> rights c\<^sub>1; Create \<in> rights c\<^sub>2; generalOperation e (target c\<^sub>1) c\<^sub>2 all_rights s \<turnstile> x \<leftrightarrow> y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<turnstile> target c\<^sub>1 \<leftrightarrow> e; is_entity s e; is_entity s (target c\<^sub>1); \<not> is_entity s (target c\<^sub>2); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s e; Write \<in> rights c\<^sub>1; Store \<in> rights c\<^sub>1; Create \<in> rights c\<^sub>2\<rbrakk> \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c\<^sub>1
 2. \<lbrakk>s \<turnstile> target c\<^sub>1 \<leftrightarrow> e; is_entity s e; is_entity s (target c\<^sub>1); \<not> is_entity s (target c\<^sub>2); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s e; Write \<in> rights c\<^sub>1; Store \<in> rights c\<^sub>1; Create \<in> rights c\<^sub>2; s \<turnstile> x \<leftrightarrow>* y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<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; s \<turnstile> target c\<^sub>1 \<leftrightarrow> e\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>generalOperation (target c\<^sub>1) e c\<^sub>2 (r \<inter> rights c\<^sub>2) s \<turnstile> x \<leftrightarrow> y; s \<turnstile> target c\<^sub>1 \<leftrightarrow> e; is_entity s e; is_entity s (target c\<^sub>1); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s (target c\<^sub>1); Take \<in> rights c\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<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; s \<turnstile> e \<leftrightarrow> target c\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>generalOperation e (target c\<^sub>1) c\<^sub>2 (r \<inter> rights c\<^sub>2) s \<turnstile> x \<leftrightarrow> y; s \<turnstile> e \<leftrightarrow> target c\<^sub>1; is_entity s e; is_entity s (target c\<^sub>1); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s e; Grant \<in> rights c\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<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; s \<turnstile> e \<leftrightarrow> target c\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>generalOperation e (target c\<^sub>1) c\<^sub>2 (r \<inter> rights c\<^sub>2) s \<turnstile> x \<leftrightarrow> y; s \<turnstile> e \<leftrightarrow> target c\<^sub>1; is_entity s e; is_entity s (target c\<^sub>1); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s e; Store \<in> rights c\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leftrightarrow> y; cmd = SysTake e c\<^sub>1 c\<^sub>2 r\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s' \<turnstile> x \<leftrightarrow> y; cmd = SysTake e c\<^sub>1 c\<^sub>2 r; is_entity s e; is_entity s (target c\<^sub>1); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s (target c\<^sub>1); Take \<in> rights c\<^sub>1; s' = s \<or> s' = takeOperation e c\<^sub>1 c\<^sub>2 r s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>s \<turnstile> x \<leftrightarrow> y; cmd = SysTake e c\<^sub>1 c\<^sub>2 r; c\<^sub>2 \<in> caps_of s (target c\<^sub>1) \<longrightarrow> c\<^sub>1 \<in> caps_of s e \<longrightarrow> is_entity s (target c\<^sub>1) \<longrightarrow> is_entity s e \<longrightarrow> Take \<notin> rights c\<^sub>1; s' = s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>takeOperation e c\<^sub>1 c\<^sub>2 r s \<turnstile> x \<leftrightarrow> y; cmd = SysTake e c\<^sub>1 c\<^sub>2 r; is_entity s e; is_entity s (target c\<^sub>1); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s (target c\<^sub>1); Take \<in> rights c\<^sub>1; s' = takeOperation e c\<^sub>1 c\<^sub>2 r s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>s \<turnstile> x \<leftrightarrow> y; cmd = SysTake e c\<^sub>1 c\<^sub>2 r; c\<^sub>2 \<in> caps_of s (target c\<^sub>1) \<longrightarrow> c\<^sub>1 \<in> caps_of s e \<longrightarrow> is_entity s (target c\<^sub>1) \<longrightarrow> is_entity s e \<longrightarrow> Take \<notin> rights c\<^sub>1; s' = s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> x \<leftrightarrow> y; cmd = SysTake e c\<^sub>1 c\<^sub>2 r; c\<^sub>2 \<in> caps_of s (target c\<^sub>1) \<longrightarrow> c\<^sub>1 \<in> caps_of s e \<longrightarrow> is_entity s (target c\<^sub>1) \<longrightarrow> is_entity s e \<longrightarrow> Take \<notin> rights c\<^sub>1; s' = s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leftrightarrow> y; cmd = SysCopy e c\<^sub>1 c\<^sub>2 r\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s' \<turnstile> x \<leftrightarrow> y; cmd = SysCopy e c\<^sub>1 c\<^sub>2 r; is_entity s e; is_entity s (target c\<^sub>1); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s e; Store \<in> rights c\<^sub>1; s' = s \<or> s' = copyOperation e c\<^sub>1 c\<^sub>2 r s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>s \<turnstile> x \<leftrightarrow> y; cmd = SysCopy e c\<^sub>1 c\<^sub>2 r; c\<^sub>2 \<in> caps_of s e \<longrightarrow> c\<^sub>1 \<in> caps_of s e \<longrightarrow> is_entity s (target c\<^sub>1) \<longrightarrow> is_entity s e \<longrightarrow> Store \<notin> rights c\<^sub>1; s' = s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>copyOperation e c\<^sub>1 c\<^sub>2 r s \<turnstile> x \<leftrightarrow> y; cmd = SysCopy e c\<^sub>1 c\<^sub>2 r; is_entity s e; is_entity s (target c\<^sub>1); c\<^sub>1 \<in> caps_of s e; c\<^sub>2 \<in> caps_of s e; Store \<in> rights c\<^sub>1; s' = copyOperation e c\<^sub>1 c\<^sub>2 r s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>s \<turnstile> x \<leftrightarrow> y; cmd = SysCopy e c\<^sub>1 c\<^sub>2 r; c\<^sub>2 \<in> caps_of s e \<longrightarrow> c\<^sub>1 \<in> caps_of s e \<longrightarrow> is_entity s (target c\<^sub>1) \<longrightarrow> is_entity s e \<longrightarrow> Store \<notin> rights c\<^sub>1; s' = s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> x \<leftrightarrow> y; cmd = SysCopy e c\<^sub>1 c\<^sub>2 r; c\<^sub>2 \<in> caps_of s e \<longrightarrow> c\<^sub>1 \<in> caps_of s e \<longrightarrow> is_entity s (target c\<^sub>1) \<longrightarrow> is_entity s e \<longrightarrow> Store \<notin> rights c\<^sub>1; s' = s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in> direct_caps_of (s(e := None)) x \<Longrightarrow> c \<in> direct_caps_of s x
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> store_connected (s(e := None)) \<Longrightarrow> (x, y) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> (store_connected_direct (s(e := None)))\<^sup>* \<Longrightarrow> (x, y) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. (x, x) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (s(e := None)))\<^sup>*; (y, z) \<in> store_connected_direct (s(e := None)); (x, y) \<in> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (s(e := None)))\<^sup>*; (y, z) \<in> store_connected_direct (s(e := None)); (x, y) \<in> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (s(e := None)); (y, z) \<in> store_connected_direct (s(e := None)); (x, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> (x, z) \<in> store_connected s proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (s(e := None)); (y, z) \<in> store_connected_direct (s(e := None)); (x, y) \<in> store_connected s; (y, z) \<in> store_connected_direct s\<rbrakk> \<Longrightarrow> (x, z) \<in> store_connected s
 2. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (s(e := None)); (y, z) \<in> store_connected_direct (s(e := None)); (x, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (s(e := None)); (y, z) \<in> store_connected_direct (s(e := None)); (x, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> store_connected (s(e := None)); \<exists>cap. cap \<in> direct_caps_of (s(e := None)) y \<and> Store \<in> rights cap \<and> target cap = z; (x, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> \<exists>cap. cap \<in> direct_caps_of s y \<and> Store \<in> rights cap \<and> target cap = z proof (prove)
goal (1 subgoal):
 1. \<And>y cap. \<lbrakk>(x, y) \<in> store_connected (s(e := None)); (x, y) \<in> store_connected s; cap \<in> direct_caps_of (s(e := None)) y; Store \<in> rights cap\<rbrakk> \<Longrightarrow> \<exists>capa. capa \<in> direct_caps_of s y \<and> Store \<in> rights capa \<and> target capa = target cap
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. shares_caps (destroyOperation e c s) x y \<Longrightarrow> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>(x, e\<^sub>i) \<in> store_connected (s(target c := None)); (y, e\<^sub>i) \<in> store_connected (s(target c := None))\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>(x, e\<^sub>i) \<in> store_connected (s(target c := None)); (y, e\<^sub>i) \<in> store_connected (s(target c := None)); (x, e\<^sub>i) \<in> store_connected s\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>(x, e\<^sub>i) \<in> store_connected (s(target c := None)); (x, e\<^sub>i) \<in> store_connected s; (y, e\<^sub>i) \<in> store_connected s\<rbrakk> \<Longrightarrow> \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in> caps_of (destroyOperation e' c' s) e \<Longrightarrow> c \<in> caps_of s e proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(e, x) \<in> store_connected (s(target c' := None)); c \<in> direct_caps_of (s(target c' := None)) x\<rbrakk> \<Longrightarrow> \<exists>x. (e, x) \<in> store_connected s \<and> c \<in> direct_caps_of s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(e, x) \<in> store_connected (s(target c' := None)); c \<in> direct_caps_of (s(target c' := None)) x\<rbrakk> \<Longrightarrow> (e, x) \<in> store_connected s \<and> c \<in> direct_caps_of s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(e, x) \<in> store_connected (s(target c' := None)); c \<in> direct_caps_of s x\<rbrakk> \<Longrightarrow> (e, x) \<in> store_connected s \<and> c \<in> direct_caps_of s x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(e, x) \<in> store_connected (s(target c' := None)); c \<in> direct_caps_of s x\<rbrakk> \<Longrightarrow> (e, x) \<in> store_connected s proof (prove)
goal:
No subgoals!
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leftrightarrow> y; cmd = SysDestroy e c\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y
theory Confine_S

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)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in> direct_caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x \<Longrightarrow> c \<in> direct_caps_of s x
theory Confine_S

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)

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

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<in> caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x \<Longrightarrow> c \<in> caps_of s x proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(x, xa) \<in> store_connected (removeOperation e c\<^sub>1 c\<^sub>2 s); c \<in> direct_caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) xa\<rbrakk> \<Longrightarrow> \<exists>xa. (x, xa) \<in> store_connected s \<and> c \<in> direct_caps_of s xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(x, xa) \<in> store_connected (removeOperation e c\<^sub>1 c\<^sub>2 s); c \<in> direct_caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) xa\<rbrakk> \<Longrightarrow> (x, xa) \<in> store_connected s \<and> c \<in> direct_caps_of s xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>(x, xa) \<in> store_connected (removeOperation e c\<^sub>1 c\<^sub>2 s); c \<in> direct_caps_of s xa\<rbrakk> \<Longrightarrow> (x, xa) \<in> store_connected s \<and> c \<in> direct_caps_of s xa proof (prove)
goal (1 subgoal):
 1. \<And>xa x2 xaa. \<lbrakk>c \<in> direct_caps_of s xa; s (target c\<^sub>1) = Some (Entity xaa); x2 = Entity xaa; (x, xa) \<in> store_connected (s(target c\<^sub>1 \<mapsto> Entity (xaa - {c\<^sub>2})))\<rbrakk> \<Longrightarrow> (x, xa) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. \<And>x x2 xa. \<lbrakk>c \<in> direct_caps_of s x; s (target c\<^sub>1) = Some (Entity xa); x2 = Entity xa\<rbrakk> \<Longrightarrow> xa - {c\<^sub>2} \<subseteq> xa proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of (removeOperation e c\<^sub>1 c\<^sub>2 s) x \<subseteq> caps_of s x proof (prove)
goal (1 subgoal):
 1. (\<exists>y. s (target c\<^sub>1) = Some y) \<longrightarrow> (\<Union>x\<in>{e'. (x, e') \<in> store_connected (s(target c\<^sub>1 \<mapsto> Entity ((case s (target c\<^sub>1) of None \<Rightarrow> {} | Some (Entity e) \<Rightarrow> e) - {c\<^sub>2})))}. case if x = target c\<^sub>1 then Some (Entity ((case s (target c\<^sub>1) of None \<Rightarrow> {} | Some (Entity e) \<Rightarrow> e) - {c\<^sub>2})) else s x of None \<Rightarrow> {} | Some (Entity e) \<Rightarrow> e) \<subseteq> (\<Union>x\<in>{e'. (x, e') \<in> store_connected s}. case s x of None \<Rightarrow> {} | Some (Entity e) \<Rightarrow> e) proof (prove)
goal (2 subgoals):
 1. \<And>xa xb. \<lbrakk>s (target c\<^sub>1) = Some (Entity xb); (x, target c\<^sub>1) \<in> store_connected (s(target c\<^sub>1 \<mapsto> Entity (xb - {c\<^sub>2}))); xa \<in> xb; xa \<noteq> c\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>xb. (x, xb) \<in> store_connected s \<and> xa \<in> (case s xb of None \<Rightarrow> {} | Some (Entity e) \<Rightarrow> e)
 2. \<And>xa xaa y xb. \<lbrakk>s (target c\<^sub>1) = Some (Entity xb); y = Entity xb; (x, xaa) \<in> store_connected (s(target c\<^sub>1 \<mapsto> Entity (xb - {c\<^sub>2}))); xaa \<noteq> target c\<^sub>1; xa \<in> (case s xaa of None \<Rightarrow> {} | Some (Entity e) \<Rightarrow> e)\<rbrakk> \<Longrightarrow> \<exists>xb. (x, xb) \<in> store_connected s \<and> xa \<in> (case s xb of None \<Rightarrow> {} | Some (Entity e) \<Rightarrow> e) proof (prove)
goal:
No subgoals!