kings-crown/FVELER_Isabelle huggingface dataset:
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>c'\<in>caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x. y = target c' \<and> rights (extra_rights (take_cap y)) \<subseteq> rights (extra_rights c'); 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> (\<exists>c'\<in>caps_of s z. y = target c' \<and> rights (extra_rights (take_cap y)) \<subseteq> rights (extra_rights c')) proof (prove)
goal (1 subgoal):
 1. \<And>c'. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; c' \<in> caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> (\<exists>c'a\<in>caps_of s z. target c' = target c'a \<and> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'a)) proof (prove)
goal (1 subgoal):
 1. \<And>c'. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'; \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> (\<exists>c'a\<in>caps_of s z. target c' = target c'a \<and> rights (extra_rights (take_cap (target c'))) \<subseteq> rights (extra_rights c'a)) proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>c'\<in>caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x. y = target c' \<and> rights (extra_rights (grant_cap y)) \<subseteq> rights (extra_rights c'); 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> (\<exists>c'\<in>caps_of s z. y = target c' \<and> rights (extra_rights (grant_cap y)) \<subseteq> rights (extra_rights c')) proof (prove)
goal (1 subgoal):
 1. \<And>c'. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; c' \<in> caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> (\<exists>c'a\<in>caps_of s z. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a)) proof (prove)
goal (1 subgoal):
 1. \<And>c'. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'); y = target c'; \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> (\<exists>c'a\<in>caps_of s z. target c' = target c'a \<and> rights (extra_rights (grant_cap (target c'))) \<subseteq> rights (extra_rights c'a)) proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> take_cap y \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow>* z; take_cap y \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow>* z; take_cap y \<in>cap caps_of s z; s \<turnstile> z \<leftrightarrow> y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<And>z. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow>* z; take_cap y \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> s \<turnstile> z \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow>* z; take_cap y \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> s \<turnstile> z \<leftrightarrow> y proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> grant_cap y \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow>* z; grant_cap y \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow>* z; grant_cap y \<in>cap caps_of s z; s \<turnstile> z \<leftrightarrow> y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<And>z. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow>* z; grant_cap y \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> s \<turnstile> z \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; s \<turnstile> x \<leftrightarrow>* z; grant_cap y \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> s \<turnstile> z \<leftrightarrow> y proof (prove)
goal:
No subgoals!
theory Confine_S

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

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

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. legal (SysTake e c\<^sub>1 c\<^sub>2 r) s \<Longrightarrow> s \<turnstile> target c\<^sub>1 \<leftrightarrow> e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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> target c\<^sub>1 \<leftrightarrow> e proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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> e \<leftrightarrow> target c\<^sub>1 proof (prove)
goal:
No subgoals!
theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. legal (SysGrant e c\<^sub>1 c\<^sub>2 r) s \<Longrightarrow> s \<turnstile> e \<leftrightarrow> target c\<^sub>1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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> e \<leftrightarrow> target c\<^sub>1 proof (prove)
goal:
No subgoals!
theory Confine_S

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

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

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (1 subgoal):
 1. \<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; s \<turnstile> target c\<^sub>1 \<leftrightarrow> e\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c' \<in> caps_of (make_entity (target c\<^sub>2) (generalOperation e (target c\<^sub>1) c\<^sub>2 all_rights s)) x; 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> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z 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; c' \<in> caps_of (generalOperation e (target c\<^sub>1) c\<^sub>2 all_rights s) x\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z 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; \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal:
No subgoals!
theory Confine_S

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

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

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

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

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

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