theory Confine_S

lemma authority_confinement_helper:
  "s' \<in> execute cmds s \<longrightarrow>
   (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow>
   (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c)" proof (induct cmds arbitrary: s') case Nil show ?case by clarsimp next case (Cons cmd cmds s') show ?case apply clarsimp apply (rule authority_confinement_induct_step, assumption) apply clarsimp apply (rule Cons.hyps[rule_format], simp_all) apply (drule(1) tgs_connected_preserved_step) apply (simp add: tgs_connected_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s' \<in> execute cmds s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c) proof (state)
goal (2 subgoals):
 1. \<And>s'. s' \<in> execute [] s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c)
 2. \<And>a cmds s'. (\<And>s'. s' \<in> execute cmds s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c)) \<Longrightarrow> s' \<in> execute (a # cmds) s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c) proof (state)
this:


goal (2 subgoals):
 1. \<And>s'. s' \<in> execute [] s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c)
 2. \<And>a cmds s'. (\<And>s'. s' \<in> execute cmds s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c)) \<Longrightarrow> s' \<in> execute (a # cmds) s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c) proof (prove)
goal (1 subgoal):
 1. s' \<in> execute [] s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c) proof (state)
this:
s' \<in> execute [] s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c)

goal (1 subgoal):
 1. \<And>a cmds s'. (\<And>s'. s' \<in> execute cmds s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c)) \<Longrightarrow> s' \<in> execute (a # cmds) s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c) proof (state)
goal (1 subgoal):
 1. \<And>a cmds s'. (\<And>s'. s' \<in> execute cmds s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c)) \<Longrightarrow> s' \<in> execute (a # cmds) s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s' e\<^sub>i \<le>cap c) proof (state)
this:
?s' \<in> execute cmds s \<longrightarrow> (\<forall>e\<^sub>i. s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of s e\<^sub>i \<le>cap c) \<longrightarrow> (\<forall>e\<^sub>i. ?s' \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>i \<longrightarrow> caps_of ?s' e\<^sub>i \<le>cap c)

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

goal:
No subgoals!