theory Confine_S

lemma store_connected_remove [rule_format]:
  "(x, y) \<in> store_connected (s(e \<mapsto> Entity C')) \<Longrightarrow>
  s e = Some (Entity C) \<longrightarrow> C' \<subseteq> C \<longrightarrow> (x, y) \<in> store_connected s" apply (unfold store_connected_def) apply (erule rtrancl_induct) apply simp apply clarsimp apply (subgoal_tac "(y,z) \<in> store_connected_direct s") apply (erule rtrancl_trans) apply fastforce apply (fold store_connected_def) apply (clarsimp simp add: store_connected_direct_def) apply (fastforce simp: direct_caps_of_def
                  split: option.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> store_connected (s(e \<mapsto> Entity C')) \<Longrightarrow> s e = Some (Entity C) \<longrightarrow> C' \<subseteq> C \<longrightarrow> (x, y) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> (store_connected_direct (s(e \<mapsto> Entity C')))\<^sup>* \<Longrightarrow> s e = Some (Entity C) \<longrightarrow> C' \<subseteq> C \<longrightarrow> (x, y) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. s e = Some (Entity C) \<longrightarrow> C' \<subseteq> C \<longrightarrow> (x, x) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (s(e \<mapsto> Entity C')))\<^sup>*; (y, z) \<in> store_connected_direct (s(e \<mapsto> Entity C')); s e = Some (Entity C) \<longrightarrow> C' \<subseteq> C \<longrightarrow> (x, y) \<in> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> s e = Some (Entity C) \<longrightarrow> C' \<subseteq> C \<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 \<mapsto> Entity C')))\<^sup>*; (y, z) \<in> store_connected_direct (s(e \<mapsto> Entity C')); s e = Some (Entity C) \<longrightarrow> C' \<subseteq> C \<longrightarrow> (x, y) \<in> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> s e = Some (Entity C) \<longrightarrow> C' \<subseteq> C \<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 \<mapsto> Entity C')))\<^sup>*; (y, z) \<in> store_connected_direct (s(e \<mapsto> Entity C')); s e = Some (Entity C); C' \<subseteq> C; (x, y) \<in> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>* proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (s(e \<mapsto> Entity C')))\<^sup>*; (y, z) \<in> store_connected_direct (s(e \<mapsto> Entity C')); s e = Some (Entity C); C' \<subseteq> C; (x, y) \<in> (store_connected_direct s)\<^sup>*; (y, z) \<in> store_connected_direct s\<rbrakk> \<Longrightarrow> (x, z) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (s(e \<mapsto> Entity C')))\<^sup>*; (y, z) \<in> store_connected_direct (s(e \<mapsto> Entity C')); s e = Some (Entity C); C' \<subseteq> C; (x, y) \<in> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (s(e \<mapsto> Entity C')))\<^sup>*; (y, z) \<in> store_connected_direct (s(e \<mapsto> Entity C')); s e = Some (Entity C); C' \<subseteq> C; (y, z) \<in> store_connected_direct s\<rbrakk> \<Longrightarrow> (y, z) \<in> (store_connected_direct s)\<^sup>*
 2. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (s(e \<mapsto> Entity C')))\<^sup>*; (y, z) \<in> store_connected_direct (s(e \<mapsto> Entity C')); s e = Some (Entity C); C' \<subseteq> C; (x, y) \<in> (store_connected_direct s)\<^sup>*\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(x, y) \<in> (store_connected_direct (s(e \<mapsto> Entity C')))\<^sup>*; (y, z) \<in> store_connected_direct (s(e \<mapsto> Entity C')); s e = Some (Entity C); C' \<subseteq> C; (x, y) \<in> (store_connected_direct s)\<^sup>*\<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 \<mapsto> Entity C')); (y, z) \<in> store_connected_direct (s(e \<mapsto> Entity C')); s e = Some (Entity C); C' \<subseteq> C; (x, y) \<in> store_connected s\<rbrakk> \<Longrightarrow> (y, z) \<in> store_connected_direct s proof (prove)
goal (1 subgoal):
 1. \<And>y cap. \<lbrakk>(x, y) \<in> store_connected (s(e \<mapsto> Entity C')); s e = Some (Entity C); C' \<subseteq> C; (x, y) \<in> store_connected s; cap \<in> direct_caps_of (s(e \<mapsto> Entity C')) 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 proof (prove)
goal:
No subgoals!