theory Confine_S

lemma direct_caps_of_directly_tgs_connected_eq:
  "\<forall> e. direct_caps_of s e = direct_caps_of s' e \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y = s' \<turnstile> x \<leftrightarrow> y" apply (simp add: directly_tgs_connected_def4 shares_caps_def) apply rule apply (erule disjE, drule (1) direct_caps_of_caps_of_eq2, clarsimp)+ apply (drule direct_caps_of_store_connected_eq, clarsimp) apply (erule disjE, drule direct_caps_of_caps_of_eq2 [rotated, where s=s' and s'=s], simp+)+ apply (drule direct_caps_of_store_connected_eq, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>e. direct_caps_of s e = direct_caps_of s' e \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y = s' \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<forall>e. direct_caps_of s e = direct_caps_of s' e \<Longrightarrow> (take_cap x \<in>cap caps_of s y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s)) = (take_cap x \<in>cap caps_of s' y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s' \<and> (y, e\<^sub>i) \<in> store_connected s')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>e. direct_caps_of s e = direct_caps_of s' e; take_cap x \<in>cap caps_of s y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s)\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s' y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s' \<and> (y, e\<^sub>i) \<in> store_connected s')
 2. \<lbrakk>\<forall>e. direct_caps_of s e = direct_caps_of s' e; take_cap x \<in>cap caps_of s' y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s' \<and> (y, e\<^sub>i) \<in> store_connected s')\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>e. direct_caps_of s e = direct_caps_of s' e; \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s' y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s' \<and> (y, e\<^sub>i) \<in> store_connected s')
 2. \<lbrakk>\<forall>e. direct_caps_of s e = direct_caps_of s' e; take_cap x \<in>cap caps_of s' y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s' \<and> (y, e\<^sub>i) \<in> store_connected s')\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>e. direct_caps_of s e = direct_caps_of s' e; take_cap x \<in>cap caps_of s' y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s' \<and> (y, e\<^sub>i) \<in> store_connected s')\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>e. direct_caps_of s e = direct_caps_of s' e; \<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s' \<and> (y, e\<^sub>i) \<in> store_connected s'\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> (\<exists>e\<^sub>i. (x, e\<^sub>i) \<in> store_connected s \<and> (y, e\<^sub>i) \<in> store_connected s) proof (prove)
goal:
No subgoals!