theory Confine_S

lemma caps_of_op:
  "\<lbrakk>s' \<in> step cmd s; c' \<in> caps_of s' x\<rbrakk>
  \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z" apply (simp add: step_def split:if_split_asm) prefer 2 apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights) apply (erule disjE) apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights) apply (case_tac cmd) apply (simp add: caps_of_create) apply (simp add: caps_of_take) apply (simp add: caps_of_grant) apply (simp add: caps_of_copy) apply (clarsimp, drule caps_of_remove) apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights) apply (clarsimp, drule caps_of_removeSet) apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights) apply (clarsimp, drule (1) caps_of_revoke) apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights) apply (clarsimp, drule caps_of_destroy) apply (fastforce simp: cap_in_caps_def tgs_connected_def rights_extra_rights) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step cmd s; c' \<in> caps_of s' x\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' = s \<or> s' \<in> step' cmd s\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<lbrakk>c' \<in> caps_of s x; \<not> legal cmd s; s' = s\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c' \<in> caps_of s x; \<not> legal cmd s; s' = s\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' = s \<or> s' \<in> step' cmd s\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' = s \<or> s' \<in> step' cmd s\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' = s\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysCreate x11 x12 x13\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>x21 x22 x23 x24. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysTake x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 3. \<And>x31 x32 x33 x34. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysGrant x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 4. \<And>x41 x42 x43 x44. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysCopy x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 5. \<And>x51 x52 x53. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemove x51 x52 x53\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 6. \<And>x61 x62 x63. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 7. \<And>x71 x72. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 8. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (7 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysTake x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>x31 x32 x33 x34. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysGrant x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 3. \<And>x41 x42 x43 x44. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysCopy x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 4. \<And>x51 x52 x53. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemove x51 x52 x53\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 5. \<And>x61 x62 x63. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 6. \<And>x71 x72. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 7. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysGrant x31 x32 x33 x34\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>x41 x42 x43 x44. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysCopy x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 3. \<And>x51 x52 x53. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemove x51 x52 x53\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 4. \<And>x61 x62 x63. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 5. \<And>x71 x72. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 6. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 x44. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysCopy x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>x51 x52 x53. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemove x51 x52 x53\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 3. \<And>x61 x62 x63. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 4. \<And>x71 x72. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 5. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemove x51 x52 x53\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>x61 x62 x63. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 3. \<And>x71 x72. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 4. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53. \<lbrakk>s' = removeOperation x51 x52 x53 s; cmd = SysRemove x51 x52 x53; is_entity s x51; x52 \<in> caps_of s x51; c' \<in> caps_of s x\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>x61 x62 x63. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 3. \<And>x71 x72. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 4. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (3 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>x71 x72. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 3. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (3 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>s' = removeSetOperation x61 x62 x63 s; cmd = SysRemoveSet x61 x62 x63; is_entity s x61; x62 \<in> caps_of s x61; c' \<in> caps_of s x\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>x71 x72. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 3. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72. \<lbrakk>c' \<in> caps_of s' x; cmd = SysRevoke x71 x72; is_entity s x71; x72 \<in> caps_of s x71; c' \<in> caps_of s x\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z
 2. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (1 subgoal):
 1. \<And>x81 x82. \<lbrakk>c' \<in> caps_of s' x; legal cmd s; s' \<in> step' cmd s; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal (1 subgoal):
 1. \<And>x81 x82. \<lbrakk>s' = destroyOperation x81 x82 s; cmd = SysDestroy x81 x82; is_entity s x81; x82 \<in> caps_of s x81; {Create} = rights x82; target x82 \<notin> target ` (all_caps_of s - {x82}); c' \<in> caps_of s x\<rbrakk> \<Longrightarrow> \<exists>z. s \<turnstile> x \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z proof (prove)
goal:
No subgoals!