theory Islands_S

lemma authority_confinement_islands:
  "\<lbrakk>s' \<in> execute cmds s;
    island_caps s x \<le>cap c\<rbrakk>
  \<Longrightarrow> island_caps s' x \<le>cap c" apply (simp add: island_caps_dom) apply clarsimp apply (frule (1) tgs_connected_preserved) apply (subst (asm) tgs_connected_comm_eq) apply (erule authority_confinement) apply clarsimp apply (erule_tac x=e\<^sub>i' in allE) apply (erule impE) apply (metis (opaque_lifting, no_types) tgs_connected_comm_eq tgs_connected_def rtrancl_trans) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> execute cmds s; island_caps s x \<le>cap c\<rbrakk> \<Longrightarrow> island_caps s' x \<le>cap c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> execute cmds s; \<forall>e\<^sub>i. s \<turnstile> x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c\<rbrakk> \<Longrightarrow> \<forall>e\<^sub>i. s' \<turnstile> x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>s' \<in> execute cmds s; \<forall>e\<^sub>i. s \<turnstile> x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c; s' \<turnstile> x \<leftrightarrow>* e\<^sub>i\<rbrakk> \<Longrightarrow> caps_of s' e\<^sub>i \<le>cap c proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>s' \<in> execute cmds s; \<forall>e\<^sub>i. s \<turnstile> x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c; s' \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> x \<leftrightarrow>* e\<^sub>i\<rbrakk> \<Longrightarrow> caps_of s' e\<^sub>i \<le>cap c proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>s' \<in> execute cmds s; \<forall>e\<^sub>i. s \<turnstile> e\<^sub>i \<leftrightarrow>* x \<longrightarrow> caps_of s e\<^sub>i \<le>cap c; s' \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> x \<leftrightarrow>* e\<^sub>i\<rbrakk> \<Longrightarrow> caps_of s' e\<^sub>i \<le>cap c proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i. \<lbrakk>\<forall>e\<^sub>i. s \<turnstile> e\<^sub>i \<leftrightarrow>* x \<longrightarrow> caps_of s e\<^sub>i \<le>cap c; s' \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> x \<leftrightarrow>* e\<^sub>i\<rbrakk> \<Longrightarrow> \<forall>e\<^sub>i'. s \<turnstile> e\<^sub>i \<leftrightarrow>* e\<^sub>i' \<longrightarrow> caps_of s e\<^sub>i' \<le>cap c proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i e\<^sub>i'. \<lbrakk>\<forall>e\<^sub>i. s \<turnstile> e\<^sub>i \<leftrightarrow>* x \<longrightarrow> caps_of s e\<^sub>i \<le>cap c; s' \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> e\<^sub>i \<leftrightarrow>* e\<^sub>i'\<rbrakk> \<Longrightarrow> caps_of s e\<^sub>i' \<le>cap c proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i e\<^sub>i'. \<lbrakk>s' \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> e\<^sub>i \<leftrightarrow>* e\<^sub>i'; s \<turnstile> e\<^sub>i' \<leftrightarrow>* x \<longrightarrow> caps_of s e\<^sub>i' \<le>cap c\<rbrakk> \<Longrightarrow> caps_of s e\<^sub>i' \<le>cap c proof (prove)
goal (2 subgoals):
 1. \<And>e\<^sub>i e\<^sub>i'. \<lbrakk>s' \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> e\<^sub>i \<leftrightarrow>* e\<^sub>i'\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>i' \<leftrightarrow>* x
 2. \<And>e\<^sub>i e\<^sub>i'. \<lbrakk>s' \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> e\<^sub>i \<leftrightarrow>* e\<^sub>i'; caps_of s e\<^sub>i' \<le>cap c\<rbrakk> \<Longrightarrow> caps_of s e\<^sub>i' \<le>cap c proof (prove)
goal (1 subgoal):
 1. \<And>e\<^sub>i e\<^sub>i'. \<lbrakk>s' \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> x \<leftrightarrow>* e\<^sub>i; s \<turnstile> e\<^sub>i \<leftrightarrow>* e\<^sub>i'; caps_of s e\<^sub>i' \<le>cap c\<rbrakk> \<Longrightarrow> caps_of s e\<^sub>i' \<le>cap c proof (prove)
goal:
No subgoals!