theory Isolation_S

lemma flow_connected_step:
  "\<lbrakk>s' \<turnstile> x \<leadsto>* y; s' \<in> step cmd s\<rbrakk> \<Longrightarrow>
    s \<turnstile> x \<leadsto>* y" apply (erule rtrancl_induct [where r="flow s'",
                              simplified flow_trans_def[symmetric]]) apply simp apply (subgoal_tac "s \<turnstile> y \<leadsto> z") apply (fastforce simp: flow_trans_def rtrancl.rtrancl_into_rtrancl) apply (clarsimp simp: flow_def island_def set_flow_def) apply (frule_tac x=y in tgs_connected_preserved_step, simp) apply (frule_tac x=z in tgs_connected_preserved_step, simp) apply (clarsimp simp: cap_in_caps_def) apply (erule disjE) apply clarsimp apply (drule (1) caps_of_op) apply (clarsimp simp: cap_in_caps_def) apply (metis (no_types) tgs_connected_trans subsetD) apply clarsimp apply (drule (1) caps_of_op) apply (clarsimp simp: cap_in_caps_def) apply (metis (no_types) tgs_connected_trans subsetD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<turnstile> x \<leadsto>* y; s' \<in> step cmd s\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leadsto>* y proof (prove)
goal (2 subgoals):
 1. s' \<in> step cmd s \<Longrightarrow> s \<turnstile> x \<leadsto>* x
 2. \<And>y z. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leadsto> z; s \<turnstile> x \<leadsto>* y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leadsto>* z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leadsto> z; s \<turnstile> x \<leadsto>* y\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leadsto>* z proof (prove)
goal (2 subgoals):
 1. \<And>y z. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leadsto> z; s \<turnstile> x \<leadsto>* y; s \<turnstile> y \<leadsto> z\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leadsto>* z
 2. \<And>y z. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leadsto> z; s \<turnstile> x \<leadsto>* y\<rbrakk> \<Longrightarrow> s \<turnstile> y \<leadsto> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leadsto> z; s \<turnstile> x \<leadsto>* y\<rbrakk> \<Longrightarrow> s \<turnstile> y \<leadsto> z proof (prove)
goal (1 subgoal):
 1. \<And>y z xa ya. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* ya; read_cap xa \<in>cap caps_of s' ya \<or> write_cap ya \<in>cap caps_of s' xa\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> (read_cap x \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s x)) proof (prove)
goal (1 subgoal):
 1. \<And>y z xa ya. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* ya; read_cap xa \<in>cap caps_of s' ya \<or> write_cap ya \<in>cap caps_of s' xa; s \<turnstile> y \<leftrightarrow>* xa\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> (read_cap x \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s x)) proof (prove)
goal (1 subgoal):
 1. \<And>y z xa ya. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* ya; read_cap xa \<in>cap caps_of s' ya \<or> write_cap ya \<in>cap caps_of s' xa; s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* ya\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> (read_cap x \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s x)) proof (prove)
goal (1 subgoal):
 1. \<And>y z xa ya. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* ya; (\<exists>c'\<in>caps_of s' ya. xa = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s' xa. ya = target c' \<and> Write \<in> rights (extra_rights c')); s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* ya\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c')))) proof (prove)
goal (2 subgoals):
 1. \<And>y z xa ya. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* ya; s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* ya; \<exists>c'\<in>caps_of s' ya. xa = target c' \<and> Read \<in> rights (extra_rights c')\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c'))))
 2. \<And>y z xa ya. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* ya; s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* ya; \<exists>c'\<in>caps_of s' xa. ya = target c' \<and> Write \<in> rights (extra_rights c')\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c')))) proof (prove)
goal (2 subgoals):
 1. \<And>y z ya c'. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* target c'; s' \<turnstile> z \<leftrightarrow>* ya; s \<turnstile> y \<leftrightarrow>* target c'; s \<turnstile> z \<leftrightarrow>* ya; c' \<in> caps_of s' ya; Read \<in> rights (extra_rights c')\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c'))))
 2. \<And>y z xa ya. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* ya; s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* ya; \<exists>c'\<in>caps_of s' xa. ya = target c' \<and> Write \<in> rights (extra_rights c')\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c')))) proof (prove)
goal (2 subgoals):
 1. \<And>y z ya c'. \<lbrakk>s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* target c'; s' \<turnstile> z \<leftrightarrow>* ya; s \<turnstile> y \<leftrightarrow>* target c'; s \<turnstile> z \<leftrightarrow>* ya; c' \<in> caps_of s' ya; Read \<in> rights (extra_rights c'); \<exists>z. s \<turnstile> ya \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c'))))
 2. \<And>y z xa ya. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* ya; s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* ya; \<exists>c'\<in>caps_of s' xa. ya = target c' \<and> Write \<in> rights (extra_rights c')\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c')))) proof (prove)
goal (2 subgoals):
 1. \<And>y z ya c' za c'a. \<lbrakk>s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* target c'a; s' \<turnstile> z \<leftrightarrow>* ya; s \<turnstile> y \<leftrightarrow>* target c'a; s \<turnstile> z \<leftrightarrow>* ya; c' \<in> caps_of s' ya; Read \<in> rights (extra_rights c'); s \<turnstile> ya \<leftrightarrow>* za; c'a \<in> caps_of s za; target c' = target c'a; rights (extra_rights c') \<subseteq> rights (extra_rights c'a)\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c'))))
 2. \<And>y z xa ya. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* ya; s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* ya; \<exists>c'\<in>caps_of s' xa. ya = target c' \<and> Write \<in> rights (extra_rights c')\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c')))) proof (prove)
goal (1 subgoal):
 1. \<And>y z xa ya. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* ya; s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* ya; \<exists>c'\<in>caps_of s' xa. ya = target c' \<and> Write \<in> rights (extra_rights c')\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c')))) proof (prove)
goal (1 subgoal):
 1. \<And>y z xa c'. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* target c'; s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* target c'; c' \<in> caps_of s' xa; Write \<in> rights (extra_rights c')\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c')))) proof (prove)
goal (1 subgoal):
 1. \<And>y z xa c'. \<lbrakk>s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* target c'; s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* target c'; c' \<in> caps_of s' xa; Write \<in> rights (extra_rights c'); \<exists>z. s \<turnstile> xa \<leftrightarrow>* z \<and> c' \<in>cap caps_of s z\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c')))) proof (prove)
goal (1 subgoal):
 1. \<And>y z xa c' za c'a. \<lbrakk>s' \<turnstile> x \<leadsto>* y; s \<turnstile> x \<leadsto>* y; s' \<turnstile> y \<leftrightarrow>* xa; s' \<turnstile> z \<leftrightarrow>* target c'a; s \<turnstile> y \<leftrightarrow>* xa; s \<turnstile> z \<leftrightarrow>* target c'a; c' \<in> caps_of s' xa; Write \<in> rights (extra_rights c'); s \<turnstile> xa \<leftrightarrow>* za; c'a \<in> caps_of s za; target c' = target c'a; rights (extra_rights c') \<subseteq> rights (extra_rights c'a)\<rbrakk> \<Longrightarrow> \<exists>x. s \<turnstile> y \<leftrightarrow>* x \<and> (\<exists>y. s \<turnstile> z \<leftrightarrow>* y \<and> ((\<exists>c'\<in>caps_of s y. x = target c' \<and> Read \<in> rights (extra_rights c')) \<or> (\<exists>c'\<in>caps_of s x. y = target c' \<and> Write \<in> rights (extra_rights c')))) proof (prove)
goal:
No subgoals!