theory Confine_S

lemma destroy_directly_tgs_connected:
  "\<lbrakk>s' \<in> step (SysDestroy e c) s; (x, y) \<in> directly_tgs_connected s'\<rbrakk> \<Longrightarrow>
  (x, y) \<in> directly_tgs_connected s" apply(clarsimp simp: step_def split: if_split_asm) apply(erule disjE, simp) apply(simp add: directly_tgs_connected_def leak_def) apply (erule disjE) apply(fastforce simp add: cap_in_caps_def dest!: caps_of_destroy) apply (erule disjE) apply(fastforce simp add: cap_in_caps_def dest!: caps_of_destroy) apply (erule disjE) apply (drule shares_caps_destroy, simp) apply (erule disjE) apply(fastforce simp add: cap_in_caps_def dest!: caps_of_destroy) apply (erule disjE) apply(fastforce simp add: cap_in_caps_def dest!: caps_of_destroy) apply (drule shares_caps_destroy, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step (SysDestroy e c) 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = s \<or> s' = destroyOperation e c s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<turnstile> x \<leftrightarrow> y; is_entity s e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow> y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>take_cap x \<in>cap caps_of (destroyOperation e c s) y \<or> grant_cap y \<in>cap caps_of (destroyOperation e c s) x \<or> shares_caps (destroyOperation e c s) x y \<or> take_cap y \<in>cap caps_of (destroyOperation e c s) x \<or> grant_cap x \<in>cap caps_of (destroyOperation e c s) y \<or> shares_caps (destroyOperation e c s) x y; is_entity s e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; take_cap x \<in>cap caps_of (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; grant_cap y \<in>cap caps_of (destroyOperation e c s) x \<or> shares_caps (destroyOperation e c s) x y \<or> take_cap y \<in>cap caps_of (destroyOperation e c s) x \<or> grant_cap x \<in>cap caps_of (destroyOperation e c s) y \<or> shares_caps (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; grant_cap y \<in>cap caps_of (destroyOperation e c s) x \<or> shares_caps (destroyOperation e c s) x y \<or> take_cap y \<in>cap caps_of (destroyOperation e c s) x \<or> grant_cap x \<in>cap caps_of (destroyOperation e c s) y \<or> shares_caps (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; grant_cap y \<in>cap caps_of (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; shares_caps (destroyOperation e c s) x y \<or> take_cap y \<in>cap caps_of (destroyOperation e c s) x \<or> grant_cap x \<in>cap caps_of (destroyOperation e c s) y \<or> shares_caps (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; shares_caps (destroyOperation e c s) x y \<or> take_cap y \<in>cap caps_of (destroyOperation e c s) x \<or> grant_cap x \<in>cap caps_of (destroyOperation e c s) y \<or> shares_caps (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; shares_caps (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; take_cap y \<in>cap caps_of (destroyOperation e c s) x \<or> grant_cap x \<in>cap caps_of (destroyOperation e c s) y \<or> shares_caps (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; take_cap y \<in>cap caps_of (destroyOperation e c s) x \<or> grant_cap x \<in>cap caps_of (destroyOperation e c s) y \<or> shares_caps (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; take_cap y \<in>cap caps_of (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; grant_cap x \<in>cap caps_of (destroyOperation e c s) y \<or> shares_caps (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; grant_cap x \<in>cap caps_of (destroyOperation e c s) y \<or> shares_caps (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; grant_cap x \<in>cap caps_of (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; shares_caps (destroyOperation e c 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 e; c \<in> caps_of s e; {Create} = rights c; target c \<notin> target ` (all_caps_of s - {c}); s' = destroyOperation e c s; shares_caps (destroyOperation e c 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!