theory Confine_S

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>xa. (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s) \<and> c' \<in> direct_caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) xa; 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> c' \<in>cap caps_of s z proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); c' \<in> direct_caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) xa\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); c' \<in> direct_caps_of (generalOperation e\<^sub>0 e\<^sub>1 c r s) xa; s \<turnstile> x \<leftrightarrow>* xa\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in> direct_caps_of s xa \<or> c' \<in>cap {c} \<and> xa = e\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in> direct_caps_of s xa\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in> caps_of s xa\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^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. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^sub>1\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^sub>1; s \<turnstile> x \<leftrightarrow>* e\<^sub>0\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* e\<^sub>0 proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^sub>1; s \<turnstile> x \<leftrightarrow>* e\<^sub>0; c' \<in>cap caps_of s e\<^sub>0\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^sub>1; s \<turnstile> x \<leftrightarrow>* e\<^sub>0\<rbrakk> \<Longrightarrow> c' \<in>cap caps_of s e\<^sub>0
 3. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* e\<^sub>0 proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^sub>1; s \<turnstile> x \<leftrightarrow>* e\<^sub>0\<rbrakk> \<Longrightarrow> c' \<in>cap caps_of s e\<^sub>0
 2. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* e\<^sub>0 proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, xa) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* xa; c' \<in>cap {c} \<and> xa = e\<^sub>1\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* e\<^sub>0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; s \<turnstile> e\<^sub>0 \<leftrightarrow> e\<^sub>1; (x, e\<^sub>1) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* e\<^sub>1; target c' = target c \<and> rights (extra_rights c') \<subseteq> rights (extra_rights c) \<or> c' \<in>cap {}\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* e\<^sub>0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> caps_of s e\<^sub>0; (x, e\<^sub>1) \<in> store_connected (generalOperation e\<^sub>0 e\<^sub>1 c r s); s \<turnstile> x \<leftrightarrow>* e\<^sub>1; target c' = target c \<and> rights (extra_rights c') \<subseteq> rights (extra_rights c) \<or> c' \<in>cap {}; s \<turnstile> e\<^sub>1 \<leftrightarrow> e\<^sub>0\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* e\<^sub>0 proof (prove)
goal:
No subgoals!