theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y \<or> grant_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x \<or> shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y \<or> take_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x \<or> grant_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y \<or> 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 (6 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; take_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; grant_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 3. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 4. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; take_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 5. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; grant_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 6. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (6 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; take_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y\<rbrakk> \<Longrightarrow> s \<turnstile> y \<leftrightarrow>* x
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; grant_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 3. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 4. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; take_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 5. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; grant_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 6. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (5 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; grant_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 3. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; take_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 4. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; grant_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 5. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (4 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; take_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 3. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; grant_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 4. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (3 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; take_cap y \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) x\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; grant_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 3. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; grant_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; grant_cap x \<in>cap caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) y\<rbrakk> \<Longrightarrow> s \<turnstile> y \<leftrightarrow>* x
 2. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<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; shares_caps (generalOperation e\<^sub>0 e\<^sub>1 c r s) x y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* y proof (prove)
goal:
No subgoals!