theory Confine_S

lemma revoke_directly_tgs_connected:
  "\<lbrakk>s' \<in> step (SysRevoke n c\<^sub>1) s; (x, y) \<in> directly_tgs_connected s'\<rbrakk>
  \<Longrightarrow> (x, y) \<in>  directly_tgs_connected s" apply (simp add: step_def split: if_split_asm) apply (erule disjE, simp) apply (simp add: directly_tgs_connected_def leak_def) apply (erule disjE) apply(auto simp add: cap_in_caps_def dest!: caps_of_revoke)[1] apply (erule disjE) apply(auto simp add: cap_in_caps_def dest!: caps_of_revoke)[1] apply (erule disjE) apply (drule (1) shares_caps_revoke, simp) apply (erule disjE) apply(auto simp add: cap_in_caps_def dest!: caps_of_revoke)[1] apply (erule disjE) apply(auto simp add: cap_in_caps_def dest!: caps_of_revoke)[1] apply (drule (1) shares_caps_revoke, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step (SysRevoke n c\<^sub>1) s; s' \<turnstile> x \<leftrightarrow> y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<turnstile> x \<leftrightarrow> y; is_entity s n; c\<^sub>1 \<in> caps_of s n; s' = s \<or> s' \<in> revokeOperation n c\<^sub>1 s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<turnstile> x \<leftrightarrow> y; is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_cap x \<in>cap caps_of s' y \<or> grant_cap y \<in>cap caps_of s' x \<or> shares_caps s' x y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> shares_caps s' x y; is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; take_cap x \<in>cap caps_of s' y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y
 2. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; grant_cap y \<in>cap caps_of s' x \<or> shares_caps s' x y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; grant_cap y \<in>cap caps_of s' x \<or> shares_caps s' x y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; grant_cap y \<in>cap caps_of s' x\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y
 2. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; shares_caps s' x y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; shares_caps s' x y \<or> take_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y
 2. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; take_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; take_cap y \<in>cap caps_of s' x \<or> grant_cap x \<in>cap caps_of s' y \<or> shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; take_cap y \<in>cap caps_of s' x\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y
 2. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; grant_cap x \<in>cap caps_of s' y \<or> shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; grant_cap x \<in>cap caps_of s' y \<or> shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; grant_cap x \<in>cap caps_of s' y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y
 2. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_entity s n; c\<^sub>1 \<in> caps_of s n; s' \<in> revokeOperation n c\<^sub>1 s; shares_caps s' x y\<rbrakk> \<Longrightarrow> take_cap x \<in>cap caps_of s y \<or> grant_cap y \<in>cap caps_of s x \<or> shares_caps s x y \<or> take_cap y \<in>cap caps_of s x \<or> grant_cap x \<in>cap caps_of s y \<or> shares_caps s x y proof (prove)
goal:
No subgoals!