theory Confine_S

lemma store_connected_removeSetOfCaps:
  "(x, y) \<in> store_connected (\<lambda>e. if is_entity s e
                                 then Some (Entity (direct_caps_of s e - cap_map e))
                                 else None) \<Longrightarrow>
    (x, y) \<in> store_connected s" apply (unfold store_connected_def) apply (erule rtrancl_induct) apply simp 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 (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None) \<Longrightarrow> (x, y) \<in> store_connected s proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> (store_connected_direct (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else 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 (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None))\<^sup>*; (y, z) \<in> store_connected_direct (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else 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 (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None))\<^sup>*; (y, z) \<in> store_connected_direct (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None); (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 (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None))\<^sup>*; (y, z) \<in> store_connected_direct (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None); (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 (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None))\<^sup>*; (y, z) \<in> store_connected_direct (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None); (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 (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None))\<^sup>*; (y, z) \<in> store_connected_direct (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None); (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 (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None))\<^sup>*; (y, z) \<in> store_connected_direct (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None); (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 (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None))\<^sup>*; (y, z) \<in> store_connected_direct (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None); (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 (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None); (y, z) \<in> store_connected_direct (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None); (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 (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else None); (x, y) \<in> store_connected s; cap \<in> direct_caps_of (\<lambda>e. if is_entity s e then Some (Entity (direct_caps_of s e - cap_map e)) else 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 proof (prove)
goal:
No subgoals!