[STATEMENT]
lemma frame_commute:
  assumes "$y \<sharp> P" "$y\<acute> \<sharp> P" "$x \<sharp> Q" "$x\<acute> \<sharp> Q" "x \<bowtie> y"
  shows "x:[P] ;; y:[Q] = y:[Q] ;; x:[P]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x}:[P] ;; {y}:[Q] = {y}:[Q] ;; {x}:[P]
[PROOF STEP]
apply (insert assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>$y \<sharp> P; $y\<acute> \<sharp> P; $x \<sharp> Q; $x\<acute> \<sharp> Q; x \<bowtie> y\<rbrakk> \<Longrightarrow> {x}:[P] ;; {y}:[Q] = {y}:[Q] ;; {x}:[P]
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ya. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (a, ya); ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya); \<lbrakk>Q\<rbrakk>\<^sub>e (ya, b); b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>Q\<rbrakk>\<^sub>e (a, ya) \<and> ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya) \<and> \<lbrakk>P\<rbrakk>\<^sub>e (ya, b) \<and> b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)
 2. \<And>a b ya. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (a, ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (ya, b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (a, ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (ya, b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
[PROOF STEP]
apply (rename_tac s s' s\<^sub>0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' s\<^sub>0. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (s, s\<^sub>0); s\<^sub>0 = put\<^bsub>x\<^esub> s (get\<^bsub>x\<^esub> s\<^sub>0); \<lbrakk>Q\<rbrakk>\<^sub>e (s\<^sub>0, s'); s' = put\<^bsub>y\<^esub> s\<^sub>0 (get\<^bsub>y\<^esub> s')\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>Q\<rbrakk>\<^sub>e (s, ya) \<and> ya = put\<^bsub>y\<^esub> s (get\<^bsub>y\<^esub> ya) \<and> \<lbrakk>P\<rbrakk>\<^sub>e (ya, s') \<and> s' = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> s')
 2. \<And>a b ya. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (a, ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (ya, b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (a, ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (ya, b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
[PROOF STEP]
apply (subgoal_tac "(s \<oplus>\<^sub>L s' on y) \<oplus>\<^sub>L s\<^sub>0 on x = s\<^sub>0 \<oplus>\<^sub>L s' on y")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s' s\<^sub>0. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (s, s\<^sub>0); s\<^sub>0 = put\<^bsub>x\<^esub> s (get\<^bsub>x\<^esub> s\<^sub>0); \<lbrakk>Q\<rbrakk>\<^sub>e (s\<^sub>0, s'); s' = put\<^bsub>y\<^esub> s\<^sub>0 (get\<^bsub>y\<^esub> s'); s \<triangleleft>\<^bsub>y\<^esub> s' \<triangleleft>\<^bsub>x\<^esub> s\<^sub>0 = s\<^sub>0 \<triangleleft>\<^bsub>y\<^esub> s'\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>Q\<rbrakk>\<^sub>e (s, ya) \<and> ya = put\<^bsub>y\<^esub> s (get\<^bsub>y\<^esub> ya) \<and> \<lbrakk>P\<rbrakk>\<^sub>e (ya, s') \<and> s' = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> s')
 2. \<And>s s' s\<^sub>0. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (s, s\<^sub>0); s\<^sub>0 = put\<^bsub>x\<^esub> s (get\<^bsub>x\<^esub> s\<^sub>0); \<lbrakk>Q\<rbrakk>\<^sub>e (s\<^sub>0, s'); s' = put\<^bsub>y\<^esub> s\<^sub>0 (get\<^bsub>y\<^esub> s')\<rbrakk> \<Longrightarrow> s \<triangleleft>\<^bsub>y\<^esub> s' \<triangleleft>\<^bsub>x\<^esub> s\<^sub>0 = s\<^sub>0 \<triangleleft>\<^bsub>y\<^esub> s'
 3. \<And>a b ya. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (a, ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (ya, b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (a, ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (ya, b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
[PROOF STEP]
apply (metis lens_indep_get lens_indep_sym lens_override_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' s\<^sub>0. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (s, s\<^sub>0); s\<^sub>0 = put\<^bsub>x\<^esub> s (get\<^bsub>x\<^esub> s\<^sub>0); \<lbrakk>Q\<rbrakk>\<^sub>e (s\<^sub>0, s'); s' = put\<^bsub>y\<^esub> s\<^sub>0 (get\<^bsub>y\<^esub> s')\<rbrakk> \<Longrightarrow> s \<triangleleft>\<^bsub>y\<^esub> s' \<triangleleft>\<^bsub>x\<^esub> s\<^sub>0 = s\<^sub>0 \<triangleleft>\<^bsub>y\<^esub> s'
 2. \<And>a b ya. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (a, ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (ya, b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (a, ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (ya, b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
[PROOF STEP]
apply (simp add: lens_indep.lens_put_comm lens_override_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ya. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (a, ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (ya, b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (a, ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (ya, b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
[PROOF STEP]
apply (rename_tac s s' s\<^sub>0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' s\<^sub>0. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (s, s\<^sub>0); s\<^sub>0 = put\<^bsub>y\<^esub> s (get\<^bsub>y\<^esub> s\<^sub>0); \<lbrakk>P\<rbrakk>\<^sub>e (s\<^sub>0, s'); s' = put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (s, ya) \<and> ya = put\<^bsub>x\<^esub> s (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (ya, s') \<and> s' = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> s')
[PROOF STEP]
apply (subgoal_tac "put\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> s (get\<^bsub>x\<^esub> (put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')))) (get\<^bsub>y\<^esub> (put\<^bsub>y\<^esub> s (get\<^bsub>y\<^esub> s\<^sub>0)))
                      = put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' s\<^sub>0. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (s, s\<^sub>0); s\<^sub>0 = put\<^bsub>y\<^esub> s (get\<^bsub>y\<^esub> s\<^sub>0); \<lbrakk>P\<rbrakk>\<^sub>e (s\<^sub>0, s'); s' = put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s'); put\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> s (get\<^bsub>x\<^esub> (put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')))) (get\<^bsub>y\<^esub> (put\<^bsub>y\<^esub> s (get\<^bsub>y\<^esub> s\<^sub>0))) = put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (s, ya) \<and> ya = put\<^bsub>x\<^esub> s (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (ya, s') \<and> s' = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> s')
 2. \<And>s s' s\<^sub>0. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (s, s\<^sub>0); s\<^sub>0 = put\<^bsub>y\<^esub> s (get\<^bsub>y\<^esub> s\<^sub>0); \<lbrakk>P\<rbrakk>\<^sub>e (s\<^sub>0, s'); s' = put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')\<rbrakk> \<Longrightarrow> put\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> s (get\<^bsub>x\<^esub> (put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')))) (get\<^bsub>y\<^esub> (put\<^bsub>y\<^esub> s (get\<^bsub>y\<^esub> s\<^sub>0))) = put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')
[PROOF STEP]
apply (metis lens_indep_get lens_indep_sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s' s\<^sub>0. \<lbrakk>\<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>y\<^esub> a v, b) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>y\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (s, s\<^sub>0); s\<^sub>0 = put\<^bsub>y\<^esub> s (get\<^bsub>y\<^esub> s\<^sub>0); \<lbrakk>P\<rbrakk>\<^sub>e (s\<^sub>0, s'); s' = put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')\<rbrakk> \<Longrightarrow> put\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> s (get\<^bsub>x\<^esub> (put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')))) (get\<^bsub>y\<^esub> (put\<^bsub>y\<^esub> s (get\<^bsub>y\<^esub> s\<^sub>0))) = put\<^bsub>x\<^esub> s\<^sub>0 (get\<^bsub>x\<^esub> s')
[PROOF STEP]
apply (metis lens_indep.lens_put_comm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma frame_miracle [simp]:
  "x:[false] = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x}:[false] = false
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma frame_skip [simp]:
  "vwb_lens x \<Longrightarrow> x:[II] = II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwb_lens x \<Longrightarrow> {x}:[II] = II
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma frame_assign_in [frame]:
  "\<lbrakk> vwb_lens a; x \<subseteq>\<^sub>L a \<rbrakk> \<Longrightarrow> a:[x := v] = x := v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vwb_lens a; x \<subseteq>\<^sub>L a\<rbrakk> \<Longrightarrow> {a}:[x := v] = x := v
[PROOF STEP]
by (rel_auto, simp_all add: lens_get_put_quasi_commute lens_put_of_quotient)


[STATEMENT]
lemma frame_conj_true [frame]:
  "\<lbrakk> {$x,$x\<acute>} \<natural> P; vwb_lens x \<rbrakk> \<Longrightarrow> (P \<and> x:[true]) = x:[P]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{$x, $x\<acute>} \<natural> P; vwb_lens x\<rbrakk> \<Longrightarrow> (P \<and> {x}:[true]) = {x}:[P]
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma frame_is_assign [frame]:
  "vwb_lens x \<Longrightarrow> x:[$x\<acute> =\<^sub>u \<lceil>v\<rceil>\<^sub><] = x := v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwb_lens x \<Longrightarrow> {x}:[$x\<acute> =\<^sub>u \<lceil>v\<rceil>\<^sub><] = x := v
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma frame_seq [frame]:
  "\<lbrakk> vwb_lens x; {$x,$x\<acute>} \<natural> P; {$x,$x\<acute>} \<natural> Q \<rbrakk> \<Longrightarrow> x:[P ;; Q] = x:[P] ;; x:[Q]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vwb_lens x; {$x, $x\<acute>} \<natural> P; {$x, $x\<acute>} \<natural> Q\<rbrakk> \<Longrightarrow> {x}:[P ;; Q] = {x}:[P] ;; {x}:[Q]
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>vwb_lens x; \<forall>a b aa ba. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> aa (get\<^bsub>x\<^esub> a), put\<^bsub>x\<^esub> ba (get\<^bsub>x\<^esub> b)) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b aa ba. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> aa (get\<^bsub>x\<^esub> a), put\<^bsub>x\<^esub> ba (get\<^bsub>x\<^esub> b)) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); b = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> b); \<lbrakk>P\<rbrakk>\<^sub>e (a, y); \<lbrakk>Q\<rbrakk>\<^sub>e (y, b)\<rbrakk> \<Longrightarrow> \<exists>y. \<lbrakk>P\<rbrakk>\<^sub>e (a, y) \<and> y = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> y) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (y, b) \<and> b = put\<^bsub>x\<^esub> y (get\<^bsub>x\<^esub> b)
 2. \<And>a b y. \<lbrakk>vwb_lens x; \<forall>a b aa ba. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> aa (get\<^bsub>x\<^esub> a), put\<^bsub>x\<^esub> ba (get\<^bsub>x\<^esub> b)) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b aa ba. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> aa (get\<^bsub>x\<^esub> a), put\<^bsub>x\<^esub> ba (get\<^bsub>x\<^esub> b)) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<lbrakk>P\<rbrakk>\<^sub>e (a, y); y = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> y); \<lbrakk>Q\<rbrakk>\<^sub>e (y, b); b = put\<^bsub>x\<^esub> y (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> b = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> b)
[PROOF STEP]
apply (metis mwb_lens.put_put vwb_lens_mwb vwb_lens_wb wb_lens_def weak_lens.put_get)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>vwb_lens x; \<forall>a b aa ba. \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> aa (get\<^bsub>x\<^esub> a), put\<^bsub>x\<^esub> ba (get\<^bsub>x\<^esub> b)) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b aa ba. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> aa (get\<^bsub>x\<^esub> a), put\<^bsub>x\<^esub> ba (get\<^bsub>x\<^esub> b)) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<lbrakk>P\<rbrakk>\<^sub>e (a, y); y = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> y); \<lbrakk>Q\<rbrakk>\<^sub>e (y, b); b = put\<^bsub>x\<^esub> y (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> b = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> b)
[PROOF STEP]
apply (metis mwb_lens.put_put vwb_lens_mwb)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma frame_to_antiframe [frame]:
  "\<lbrakk> x \<bowtie> y; x +\<^sub>L y = 1\<^sub>L \<rbrakk> \<Longrightarrow> x:[P] = y:\<lbrakk>P\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<bowtie> y; x +\<^sub>L y = \<Sigma>\<rbrakk> \<Longrightarrow> {x}:[P] = {y}:\<lbrakk>P\<rbrakk>
[PROOF STEP]
by (rel_auto, metis lens_indep_def, metis lens_indep_def surj_pair)


[STATEMENT]
lemma rel_frext_miracle [frame]:
  "a:[false]\<^sup>+ = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a:[false]\<^sup>+ = false
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma rel_frext_skip [frame]:
  "vwb_lens a \<Longrightarrow> a:[II]\<^sup>+ = II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwb_lens a \<Longrightarrow> a:[II]\<^sup>+ = II
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma rel_frext_seq [frame]:
  "vwb_lens a \<Longrightarrow> a:[P ;; Q]\<^sup>+ = (a:[P]\<^sup>+ ;; a:[Q]\<^sup>+)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwb_lens a \<Longrightarrow> a:[P ;; Q]\<^sup>+ = a:[P]\<^sup>+ ;; a:[Q]\<^sup>+
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b y. \<lbrakk>vwb_lens a; b = put\<^bsub>a\<^esub> aa (get\<^bsub>a\<^esub> b); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> aa, y); \<lbrakk>Q\<rbrakk>\<^sub>e (y, get\<^bsub>a\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>y. \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> aa, get\<^bsub>a\<^esub> y) \<and> y = put\<^bsub>a\<^esub> aa (get\<^bsub>a\<^esub> y) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> y, get\<^bsub>a\<^esub> b) \<and> b = put\<^bsub>a\<^esub> y (get\<^bsub>a\<^esub> b)
 2. \<And>aa b y. \<lbrakk>vwb_lens a; \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> aa, get\<^bsub>a\<^esub> y); y = put\<^bsub>a\<^esub> aa (get\<^bsub>a\<^esub> y); \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> y, get\<^bsub>a\<^esub> b); b = put\<^bsub>a\<^esub> y (get\<^bsub>a\<^esub> b)\<rbrakk> \<Longrightarrow> b = put\<^bsub>a\<^esub> aa (get\<^bsub>a\<^esub> b)
[PROOF STEP]
apply (rename_tac s s' s\<^sub>0)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' s\<^sub>0. \<lbrakk>vwb_lens a; s' = put\<^bsub>a\<^esub> s (get\<^bsub>a\<^esub> s'); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> s, s\<^sub>0); \<lbrakk>Q\<rbrakk>\<^sub>e (s\<^sub>0, get\<^bsub>a\<^esub> s')\<rbrakk> \<Longrightarrow> \<exists>y. \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> s, get\<^bsub>a\<^esub> y) \<and> y = put\<^bsub>a\<^esub> s (get\<^bsub>a\<^esub> y) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> y, get\<^bsub>a\<^esub> s') \<and> s' = put\<^bsub>a\<^esub> y (get\<^bsub>a\<^esub> s')
 2. \<And>aa b y. \<lbrakk>vwb_lens a; \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> aa, get\<^bsub>a\<^esub> y); y = put\<^bsub>a\<^esub> aa (get\<^bsub>a\<^esub> y); \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> y, get\<^bsub>a\<^esub> b); b = put\<^bsub>a\<^esub> y (get\<^bsub>a\<^esub> b)\<rbrakk> \<Longrightarrow> b = put\<^bsub>a\<^esub> aa (get\<^bsub>a\<^esub> b)
[PROOF STEP]
apply (rule_tac x="put\<^bsub>a\<^esub> s s\<^sub>0" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s' s\<^sub>0. \<lbrakk>vwb_lens a; s' = put\<^bsub>a\<^esub> s (get\<^bsub>a\<^esub> s'); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> s, s\<^sub>0); \<lbrakk>Q\<rbrakk>\<^sub>e (s\<^sub>0, get\<^bsub>a\<^esub> s')\<rbrakk> \<Longrightarrow> \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> s, get\<^bsub>a\<^esub> (put\<^bsub>a\<^esub> s s\<^sub>0)) \<and> put\<^bsub>a\<^esub> s s\<^sub>0 = put\<^bsub>a\<^esub> s (get\<^bsub>a\<^esub> (put\<^bsub>a\<^esub> s s\<^sub>0)) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> (put\<^bsub>a\<^esub> s s\<^sub>0), get\<^bsub>a\<^esub> s') \<and> s' = put\<^bsub>a\<^esub> (put\<^bsub>a\<^esub> s s\<^sub>0) (get\<^bsub>a\<^esub> s')
 2. \<And>aa b y. \<lbrakk>vwb_lens a; \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> aa, get\<^bsub>a\<^esub> y); y = put\<^bsub>a\<^esub> aa (get\<^bsub>a\<^esub> y); \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> y, get\<^bsub>a\<^esub> b); b = put\<^bsub>a\<^esub> y (get\<^bsub>a\<^esub> b)\<rbrakk> \<Longrightarrow> b = put\<^bsub>a\<^esub> aa (get\<^bsub>a\<^esub> b)
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b y. \<lbrakk>vwb_lens a; \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> aa, get\<^bsub>a\<^esub> y); y = put\<^bsub>a\<^esub> aa (get\<^bsub>a\<^esub> y); \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>a\<^esub> y, get\<^bsub>a\<^esub> b); b = put\<^bsub>a\<^esub> y (get\<^bsub>a\<^esub> b)\<rbrakk> \<Longrightarrow> b = put\<^bsub>a\<^esub> aa (get\<^bsub>a\<^esub> b)
[PROOF STEP]
apply (metis mwb_lens.put_put vwb_lens_mwb)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rel_frext_assigns [frame]:
  "vwb_lens a \<Longrightarrow> a:[\<langle>\<sigma>\<rangle>\<^sub>a]\<^sup>+ = \<langle>\<sigma> \<oplus>\<^sub>s a\<rangle>\<^sub>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwb_lens a \<Longrightarrow> a:[\<langle>\<sigma>\<rangle>\<^sub>a]\<^sup>+ = \<langle>\<sigma> \<oplus>\<^sub>s a\<rangle>\<^sub>a
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma rel_frext_rcond [frame]:
  "a:[P \<triangleleft> b \<triangleright>\<^sub>r Q]\<^sup>+ = (a:[P]\<^sup>+ \<triangleleft> b \<oplus>\<^sub>p a \<triangleright>\<^sub>r a:[Q]\<^sup>+)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a:[P \<triangleleft> b \<triangleright>\<^sub>r Q]\<^sup>+ = a:[P]\<^sup>+ \<triangleleft> b \<oplus>\<^sub>p a \<triangleright>\<^sub>r a:[Q]\<^sup>+
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma rel_frext_commute:
  "x \<bowtie> y \<Longrightarrow> x:[P]\<^sup>+ ;; y:[Q]\<^sup>+ = y:[Q]\<^sup>+ ;; x:[P]\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<bowtie> y \<Longrightarrow> x:[P]\<^sup>+ ;; y:[Q]\<^sup>+ = y:[Q]\<^sup>+ ;; x:[P]\<^sup>+
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ya. \<lbrakk>x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> ya); ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya); \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> ya, get\<^bsub>y\<^esub> b); b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya) \<and> ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya) \<and> \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b) \<and> b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)
 2. \<And>a b ya. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> ya, get\<^bsub>y\<^esub> b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
[PROOF STEP]
apply (rename_tac a c b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a c b. \<lbrakk>x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> b); \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> b, get\<^bsub>y\<^esub> c); c = put\<^bsub>y\<^esub> b (get\<^bsub>y\<^esub> c)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya) \<and> ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya) \<and> \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> c) \<and> c = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> c)
 2. \<And>a b ya. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> ya, get\<^bsub>y\<^esub> b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
[PROOF STEP]
apply (subgoal_tac "\<And>b a. get\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> b a) = get\<^bsub>y\<^esub> b")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a c b. \<lbrakk>x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> b); \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> b, get\<^bsub>y\<^esub> c); c = put\<^bsub>y\<^esub> b (get\<^bsub>y\<^esub> c); \<And>b a. get\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> b a) = get\<^bsub>y\<^esub> b\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya) \<and> ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya) \<and> \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> c) \<and> c = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> c)
 2. \<And>a c b ba aa. \<lbrakk>x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> b); \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> b, get\<^bsub>y\<^esub> c); c = put\<^bsub>y\<^esub> b (get\<^bsub>y\<^esub> c)\<rbrakk> \<Longrightarrow> get\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> ba aa) = get\<^bsub>y\<^esub> ba
 3. \<And>a b ya. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> ya, get\<^bsub>y\<^esub> b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
[PROOF STEP]
apply (metis (no_types, opaque_lifting) lens_indep_comm lens_indep_get)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a c b ba aa. \<lbrakk>x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> b); \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> b, get\<^bsub>y\<^esub> c); c = put\<^bsub>y\<^esub> b (get\<^bsub>y\<^esub> c)\<rbrakk> \<Longrightarrow> get\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> ba aa) = get\<^bsub>y\<^esub> ba
 2. \<And>a b ya. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> ya, get\<^bsub>y\<^esub> b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
[PROOF STEP]
apply (simp add: lens_indep.lens_put_irr2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b ya. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> ya, get\<^bsub>y\<^esub> b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
[PROOF STEP]
apply (subgoal_tac "\<And>b c. get\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> b c) = get\<^bsub>x\<^esub> b")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ya. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b); \<And>b c. get\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> b c) = get\<^bsub>x\<^esub> b\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> ya, get\<^bsub>y\<^esub> b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
 2. \<And>a b ya ba c. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> get\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> ba c) = get\<^bsub>x\<^esub> ba
[PROOF STEP]
apply (subgoal_tac "\<And>b a. get\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> b a) = get\<^bsub>y\<^esub> b")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a b ya. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b); \<And>b c. get\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> b c) = get\<^bsub>x\<^esub> b; \<And>b a. get\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> b a) = get\<^bsub>y\<^esub> b\<rbrakk> \<Longrightarrow> \<exists>ya. \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> a, get\<^bsub>x\<^esub> ya) \<and> ya = put\<^bsub>x\<^esub> a (get\<^bsub>x\<^esub> ya) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> ya, get\<^bsub>y\<^esub> b) \<and> b = put\<^bsub>y\<^esub> ya (get\<^bsub>y\<^esub> b)
 2. \<And>a b ya ba aa. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b); \<And>b c. get\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> b c) = get\<^bsub>x\<^esub> b\<rbrakk> \<Longrightarrow> get\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> ba aa) = get\<^bsub>y\<^esub> ba
 3. \<And>a b ya ba c. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> get\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> ba c) = get\<^bsub>x\<^esub> ba
[PROOF STEP]
apply (metis (mono_tags, lifting) lens_indep_comm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b ya ba aa. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b); \<And>b c. get\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> b c) = get\<^bsub>x\<^esub> b\<rbrakk> \<Longrightarrow> get\<^bsub>y\<^esub> (put\<^bsub>x\<^esub> ba aa) = get\<^bsub>y\<^esub> ba
 2. \<And>a b ya ba c. \<lbrakk>x \<bowtie> y; \<lbrakk>Q\<rbrakk>\<^sub>e (get\<^bsub>y\<^esub> a, get\<^bsub>y\<^esub> ya); ya = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> ya); \<lbrakk>P\<rbrakk>\<^sub>e (get\<^bsub>x\<^esub> ya, get\<^bsub>x\<^esub> b); b = put\<^bsub>x\<^esub> ya (get\<^bsub>x\<^esub> b)\<rbrakk> \<Longrightarrow> get\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> ba c) = get\<^bsub>x\<^esub> ba
[PROOF STEP]
apply (simp_all add: lens_indep.lens_put_irr2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma antiframe_disj [frame]: "(x:\<lbrakk>P\<rbrakk> \<or> x:\<lbrakk>Q\<rbrakk>) = x:\<lbrakk>P \<or> Q\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({x}:\<lbrakk>P\<rbrakk> \<or> {x}:\<lbrakk>Q\<rbrakk>) = {x}:\<lbrakk>P \<or> Q\<rbrakk>
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma antiframe_seq [frame]:
  "\<lbrakk> vwb_lens x; $x\<acute> \<sharp> P; $x \<sharp> Q \<rbrakk>  \<Longrightarrow> (x:\<lbrakk>P\<rbrakk> ;; x:\<lbrakk>Q\<rbrakk>) = x:\<lbrakk>P ;; Q\<rbrakk>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vwb_lens x; $x\<acute> \<sharp> P; $x \<sharp> Q\<rbrakk> \<Longrightarrow> {x}:\<lbrakk>P\<rbrakk> ;; {x}:\<lbrakk>Q\<rbrakk> = {x}:\<lbrakk>P ;; Q\<rbrakk>
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b y. \<lbrakk>vwb_lens x; \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<lbrakk>P\<rbrakk>\<^sub>e (a, y); y = put\<^bsub>x\<^esub> y (get\<^bsub>x\<^esub> a); \<lbrakk>Q\<rbrakk>\<^sub>e (y, b); b = put\<^bsub>x\<^esub> b (get\<^bsub>x\<^esub> y)\<rbrakk> \<Longrightarrow> b = put\<^bsub>x\<^esub> b (get\<^bsub>x\<^esub> a)
 2. \<And>a b y. \<lbrakk>vwb_lens x; \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); b = put\<^bsub>x\<^esub> b (get\<^bsub>x\<^esub> a); \<lbrakk>P\<rbrakk>\<^sub>e (a, y); \<lbrakk>Q\<rbrakk>\<^sub>e (y, b)\<rbrakk> \<Longrightarrow> \<exists>y. \<lbrakk>P\<rbrakk>\<^sub>e (a, y) \<and> y = put\<^bsub>x\<^esub> y (get\<^bsub>x\<^esub> a) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (y, b) \<and> b = put\<^bsub>x\<^esub> b (get\<^bsub>x\<^esub> y)
[PROOF STEP]
apply (metis vwb_lens_wb wb_lens_def weak_lens.put_get)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>vwb_lens x; \<forall>a b v. \<lbrakk>P\<rbrakk>\<^sub>e (a, put\<^bsub>x\<^esub> b v) = \<lbrakk>P\<rbrakk>\<^sub>e (a, b); \<forall>a b v. \<lbrakk>Q\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, b) = \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); b = put\<^bsub>x\<^esub> b (get\<^bsub>x\<^esub> a); \<lbrakk>P\<rbrakk>\<^sub>e (a, y); \<lbrakk>Q\<rbrakk>\<^sub>e (y, b)\<rbrakk> \<Longrightarrow> \<exists>y. \<lbrakk>P\<rbrakk>\<^sub>e (a, y) \<and> y = put\<^bsub>x\<^esub> y (get\<^bsub>x\<^esub> a) \<and> \<lbrakk>Q\<rbrakk>\<^sub>e (y, b) \<and> b = put\<^bsub>x\<^esub> b (get\<^bsub>x\<^esub> y)
[PROOF STEP]
apply (metis vwb_lens_wb wb_lens.put_twice wb_lens_def weak_lens.put_get)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nameset_skip: "vwb_lens x \<Longrightarrow> (ns x \<bullet> II) = II\<^bsub>x\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwb_lens x \<Longrightarrow> ns x \<bullet> II = II\<^bsub>x\<^esub>
[PROOF STEP]
by (rel_auto, meson vwb_lens_wb wb_lens.get_put)


[STATEMENT]
lemma nameset_skip_ra: "vwb_lens x \<Longrightarrow> (ns x \<bullet> II\<^bsub>x\<^esub>) = II\<^bsub>x\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwb_lens x \<Longrightarrow> ns x \<bullet> II\<^bsub>x\<^esub> = II\<^bsub>x\<^esub>
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem while_unfold:
  "while b do P od = ((P ;; while b do P od) \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
have m:"mono (\<lambda>X. (P ;; X) \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Monotonic (\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
by (auto intro: monoI seqr_mono cond_mono)
[PROOF STATE]
proof (state)
this:
Monotonic (\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
have "(while b do P od) = (\<nu> X \<bullet> (P ;; X) \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
by (simp add: while_top_def)
[PROOF STATE]
proof (state)
this:
while\<^sup>\<top> b do P od = (\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
while\<^sup>\<top> b do P od = (\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
have "... = ((P ;; (\<nu> X \<bullet> (P ;; X) \<triangleleft> b \<triangleright>\<^sub>r II)) \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) = P ;; (\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
by (subst lfp_unfold, simp_all add: m)
[PROOF STATE]
proof (state)
this:
(\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) = P ;; (\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) \<triangleleft> b \<triangleright>\<^sub>r II

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) = P ;; (\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) \<triangleleft> b \<triangleright>\<^sub>r II

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
have "... = ((P ;; while b do P od) \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; (\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) \<triangleleft> b \<triangleright>\<^sub>r II = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
by (simp add: while_top_def)
[PROOF STATE]
proof (state)
this:
P ;; (\<nu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) \<triangleleft> b \<triangleright>\<^sub>r II = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
while\<^sup>\<top> b do P od = P ;; while\<^sup>\<top> b do P od \<triangleleft> b \<triangleright>\<^sub>r II

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem while_false: "while false do P od = II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while\<^sup>\<top> false do P od = II
[PROOF STEP]
by (subst while_unfold, rel_auto)


[STATEMENT]
theorem while_true: "while true do P od = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while\<^sup>\<top> true do P od = false
[PROOF STEP]
apply (simp add: while_top_def alpha)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> ((;;) P) = false
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. false \<sqsubseteq> \<nu> ((;;) P)
 2. \<nu> ((;;) P) \<sqsubseteq> false
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. false \<sqsubseteq> \<nu> ((;;) P)
[PROOF STEP]
apply (rule lfp_lowerbound)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. false \<sqsubseteq> P ;; false
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
theorem while_bot_unfold:
  "while\<^sub>\<bottom> b do P od = ((P ;; while\<^sub>\<bottom> b do P od) \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
have m:"mono (\<lambda>X. (P ;; X) \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Monotonic (\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
by (auto intro: monoI seqr_mono cond_mono)
[PROOF STATE]
proof (state)
this:
Monotonic (\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)

goal (1 subgoal):
 1. while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
have "(while\<^sub>\<bottom> b do P od) = (\<mu> X \<bullet> (P ;; X) \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while\<^sub>\<bottom> b do P od = (\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
by (simp add: while_bot_def)
[PROOF STATE]
proof (state)
this:
while\<^sub>\<bottom> b do P od = (\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)

goal (1 subgoal):
 1. while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
while\<^sub>\<bottom> b do P od = (\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)

goal (1 subgoal):
 1. while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
have "... = ((P ;; (\<mu> X \<bullet> (P ;; X) \<triangleleft> b \<triangleright>\<^sub>r II)) \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) = P ;; (\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
by (subst gfp_unfold, simp_all add: m)
[PROOF STATE]
proof (state)
this:
(\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) = P ;; (\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) \<triangleleft> b \<triangleright>\<^sub>r II

goal (1 subgoal):
 1. while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) = P ;; (\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) \<triangleleft> b \<triangleright>\<^sub>r II

goal (1 subgoal):
 1. while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
have "... = ((P ;; while\<^sub>\<bottom> b do P od) \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; (\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) \<triangleleft> b \<triangleright>\<^sub>r II = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
by (simp add: while_bot_def)
[PROOF STATE]
proof (state)
this:
P ;; (\<mu> X \<bullet> P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) \<triangleleft> b \<triangleright>\<^sub>r II = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II

goal (1 subgoal):
 1. while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II

goal (1 subgoal):
 1. while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
while\<^sub>\<bottom> b do P od = P ;; while\<^sub>\<bottom> b do P od \<triangleleft> b \<triangleright>\<^sub>r II

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem while_bot_false: "while\<^sub>\<bottom> false do P od = II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while\<^sub>\<bottom> false do P od = II
[PROOF STEP]
by (simp add: while_bot_def mu_const alpha)


[STATEMENT]
theorem while_bot_true: "while\<^sub>\<bottom> true do P od = (\<mu> X \<bullet> P ;; X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while\<^sub>\<bottom> true do P od = \<mu> ((;;) P)
[PROOF STEP]
by (simp add: while_bot_def alpha)


[STATEMENT]
lemma upower_rep_eq:
  "\<lbrakk>P \<^bold>^ i\<rbrakk>\<^sub>e = (\<lambda> b. b \<in> ({p. \<lbrakk>P\<rbrakk>\<^sub>e p} ^^ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>power.power II (;;) P i\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> {p. \<lbrakk>P\<rbrakk>\<^sub>e p} ^^ i)
[PROOF STEP]
proof (induct i arbitrary: P)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>power.power II (;;) P 0\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ 0)
 2. \<And>i P. (\<And>P. \<lbrakk>power.power II (;;) P i\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ i)) \<Longrightarrow> \<lbrakk>power.power II (;;) P (Suc i)\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ Suc i)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>P. \<lbrakk>power.power II (;;) P 0\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ 0)
 2. \<And>i P. (\<And>P. \<lbrakk>power.power II (;;) P i\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ i)) \<Longrightarrow> \<lbrakk>power.power II (;;) P (Suc i)\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>power.power II (;;) P 0\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> {a. \<lbrakk>P\<rbrakk>\<^sub>e a} ^^ 0)
[PROOF STEP]
by (auto, rel_auto)
[PROOF STATE]
proof (state)
this:
\<lbrakk>power.power II (;;) P 0\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> {a. \<lbrakk>P\<rbrakk>\<^sub>e a} ^^ 0)

goal (1 subgoal):
 1. \<And>i P. (\<And>P. \<lbrakk>power.power II (;;) P i\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ i)) \<Longrightarrow> \<lbrakk>power.power II (;;) P (Suc i)\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i P. (\<And>P. \<lbrakk>power.power II (;;) P i\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ i)) \<Longrightarrow> \<lbrakk>power.power II (;;) P (Suc i)\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ Suc i)
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
\<lbrakk>power.power II (;;) ?P i\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> {a. \<lbrakk>?P\<rbrakk>\<^sub>e a} ^^ i)

goal (1 subgoal):
 1. \<And>i P. (\<And>P. \<lbrakk>power.power II (;;) P i\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ i)) \<Longrightarrow> \<lbrakk>power.power II (;;) P (Suc i)\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> Collect \<lbrakk>P\<rbrakk>\<^sub>e ^^ Suc i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>power.power II (;;) P (Suc i)\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> {a. \<lbrakk>P\<rbrakk>\<^sub>e a} ^^ Suc i)
[PROOF STEP]
by (simp add: Suc seqr.rep_eq relpow_commute upred_semiring.power_Suc)
[PROOF STATE]
proof (state)
this:
\<lbrakk>power.power II (;;) P (Suc i)\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> {a. \<lbrakk>P\<rbrakk>\<^sub>e a} ^^ Suc i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upower_rep_eq_alt:
  "\<lbrakk>power.power \<langle>id\<rangle>\<^sub>a (;;) P i\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> ({p. \<lbrakk>P\<rbrakk>\<^sub>e p} ^^ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>power.power \<langle>id\<rangle>\<^sub>a (;;) P i\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> {p. \<lbrakk>P\<rbrakk>\<^sub>e p} ^^ i)
[PROOF STEP]
by (metis skip_r_def upower_rep_eq)


[STATEMENT]
lemma Sup_power_expand:
  fixes P :: "nat \<Rightarrow> 'a::complete_lattice"
  shows "P(0) \<sqinter> (\<Sqinter>i. P(i+1)) = (\<Sqinter>i. P(i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P
[PROOF STEP]
have "UNIV = insert (0::nat) {1..}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = insert 0 {1..}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
UNIV = insert 0 {1..}

goal (1 subgoal):
 1. P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
UNIV = insert 0 {1..}

goal (1 subgoal):
 1. P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P
[PROOF STEP]
have "(\<Sqinter>i. P(i)) = \<Sqinter> (P ` UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter>range P = \<Sqinter>range P
[PROOF STEP]
by (blast)
[PROOF STATE]
proof (state)
this:
\<Sqinter>range P = \<Sqinter>range P

goal (1 subgoal):
 1. P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Sqinter>range P = \<Sqinter>range P

goal (1 subgoal):
 1. P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P
[PROOF STEP]
have "\<Sqinter> (P ` insert 0 {1..}) = P(0) \<sqinter> \<Sqinter> (P ` {1..})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter>(P ` insert 0 {1..}) = P 0 \<sqinter> \<Sqinter>(P ` {1..})
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
\<Sqinter>(P ` insert 0 {1..}) = P 0 \<sqinter> \<Sqinter>(P ` {1..})

goal (1 subgoal):
 1. P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Sqinter>(P ` insert 0 {1..}) = P 0 \<sqinter> \<Sqinter>(P ` {1..})

goal (1 subgoal):
 1. P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P
[PROOF STEP]
have "\<Sqinter> (P ` {1..}) = (\<Sqinter>i. P(i+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter>(P ` {1..}) = (\<Sqinter>i. P (i + 1))
[PROOF STEP]
by (simp add: atLeast_Suc_greaterThan greaterThan_0)
[PROOF STATE]
proof (state)
this:
\<Sqinter>(P ` {1..}) = (\<Sqinter>i. P (i + 1))

goal (1 subgoal):
 1. P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
UNIV = insert 0 {1..}
\<Sqinter>range P = \<Sqinter>range P
\<Sqinter>(P ` insert 0 {1..}) = P 0 \<sqinter> \<Sqinter>(P ` {1..})
\<Sqinter>(P ` {1..}) = (\<Sqinter>i. P (i + 1))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
UNIV = insert 0 {1..}
\<Sqinter>range P = \<Sqinter>range P
\<Sqinter>(P ` insert 0 {1..}) = P 0 \<sqinter> \<Sqinter>(P ` {1..})
\<Sqinter>(P ` {1..}) = (\<Sqinter>i. P (i + 1))

goal (1 subgoal):
 1. P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P
[PROOF STEP]
by (simp only:)
[PROOF STATE]
proof (state)
this:
P 0 \<sqinter> (\<Sqinter>i. P (i + 1)) = \<Sqinter>range P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Sup_upto_Suc: "(\<Sqinter>i\<in>{0..Suc n}. P \<^bold>^ i) = (\<Sqinter>i\<in>{0..n}. P \<^bold>^ i) \<sqinter> P \<^bold>^ Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Or>(power.power II (;;) P ` {0..Suc n}) = \<Or>(power.power II (;;) P ` {0..n}) \<sqinter> power.power II (;;) P (Suc n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Or>(power.power II (;;) P ` {0..Suc n}) = \<Or>(power.power II (;;) P ` {0..n}) \<sqinter> power.power II (;;) P (Suc n)
[PROOF STEP]
have "(\<Sqinter>i\<in>{0..Suc n}. P \<^bold>^ i) = (\<Sqinter>i\<in>insert (Suc n) {0..n}. P \<^bold>^ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Or>(power.power II (;;) P ` {0..Suc n}) = \<Or>(power.power II (;;) P ` insert (Suc n) {0..n})
[PROOF STEP]
by (simp add: atLeast0_atMost_Suc)
[PROOF STATE]
proof (state)
this:
\<Or>(power.power II (;;) P ` {0..Suc n}) = \<Or>(power.power II (;;) P ` insert (Suc n) {0..n})

goal (1 subgoal):
 1. \<Or>(power.power II (;;) P ` {0..Suc n}) = \<Or>(power.power II (;;) P ` {0..n}) \<sqinter> power.power II (;;) P (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Or>(power.power II (;;) P ` {0..Suc n}) = \<Or>(power.power II (;;) P ` insert (Suc n) {0..n})

goal (1 subgoal):
 1. \<Or>(power.power II (;;) P ` {0..Suc n}) = \<Or>(power.power II (;;) P ` {0..n}) \<sqinter> power.power II (;;) P (Suc n)
[PROOF STEP]
have "... = P \<^bold>^ Suc n \<sqinter> (\<Sqinter>i\<in>{0..n}. P \<^bold>^ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Or>(power.power II (;;) P ` insert (Suc n) {0..n}) = power.power II (;;) P (Suc n) \<sqinter> \<Or>(power.power II (;;) P ` {0..n})
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
\<Or>(power.power II (;;) P ` insert (Suc n) {0..n}) = power.power II (;;) P (Suc n) \<sqinter> \<Or>(power.power II (;;) P ` {0..n})

goal (1 subgoal):
 1. \<Or>(power.power II (;;) P ` {0..Suc n}) = \<Or>(power.power II (;;) P ` {0..n}) \<sqinter> power.power II (;;) P (Suc n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Or>(power.power II (;;) P ` {0..Suc n}) = power.power II (;;) P (Suc n) \<sqinter> \<Or>(power.power II (;;) P ` {0..n})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Or>(power.power II (;;) P ` {0..Suc n}) = power.power II (;;) P (Suc n) \<sqinter> \<Or>(power.power II (;;) P ` {0..n})

goal (1 subgoal):
 1. \<Or>(power.power II (;;) P ` {0..Suc n}) = \<Or>(power.power II (;;) P ` {0..n}) \<sqinter> power.power II (;;) P (Suc n)
[PROOF STEP]
by (simp add: Lattices.sup_commute)
[PROOF STATE]
proof (state)
this:
\<Or>(power.power II (;;) P ` {0..Suc n}) = \<Or>(power.power II (;;) P ` {0..n}) \<sqinter> power.power II (;;) P (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upower_inductl: "Q \<sqsubseteq> ((P ;; Q) \<sqinter> R) \<Longrightarrow> Q \<sqsubseteq> P \<^bold>^ n ;; R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P n ;; R
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P 0 ;; R
 2. \<And>n. \<lbrakk>Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P n ;; R; Q \<sqsubseteq> (P ;; Q) \<sqinter> R\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P (Suc n) ;; R
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> (P ;; Q) \<sqinter> R

goal (2 subgoals):
 1. Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P 0 ;; R
 2. \<And>n. \<lbrakk>Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P n ;; R; Q \<sqsubseteq> (P ;; Q) \<sqinter> R\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P (Suc n) ;; R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Q \<sqsubseteq> (P ;; Q) \<sqinter> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Q \<sqsubseteq> (P ;; Q) \<sqinter> R

goal (1 subgoal):
 1. Q \<sqsubseteq> power.power II (;;) P 0 ;; R
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> power.power II (;;) P 0 ;; R

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P n ;; R; Q \<sqsubseteq> (P ;; Q) \<sqinter> R\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P (Suc n) ;; R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P n ;; R; Q \<sqsubseteq> (P ;; Q) \<sqinter> R\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P (Suc n) ;; R
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P n ;; R
Q \<sqsubseteq> (P ;; Q) \<sqinter> R

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P n ;; R; Q \<sqsubseteq> (P ;; Q) \<sqinter> R\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P (Suc n) ;; R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P n ;; R
Q \<sqsubseteq> (P ;; Q) \<sqinter> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Q \<sqsubseteq> (P ;; Q) \<sqinter> R \<Longrightarrow> Q \<sqsubseteq> power.power II (;;) P n ;; R
Q \<sqsubseteq> (P ;; Q) \<sqinter> R

goal (1 subgoal):
 1. Q \<sqsubseteq> power.power II (;;) P (Suc n) ;; R
[PROOF STEP]
by (auto simp add: upred_semiring.power_Suc, metis (no_types, opaque_lifting) dual_order.trans order_refl seqr_assoc seqr_mono)
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> power.power II (;;) P (Suc n) ;; R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upower_inductr:
  assumes "Q \<sqsubseteq> R \<sqinter> (Q ;; P)"
  shows "Q \<sqsubseteq> R ;; (P \<^bold>^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<sqsubseteq> R ;; power.power II (;;) P n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Q \<sqsubseteq> R \<sqinter> (Q ;; P)

goal (1 subgoal):
 1. Q \<sqsubseteq> R ;; power.power II (;;) P n
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P 0
 2. \<And>n. \<lbrakk>Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n; Q \<sqsubseteq> R \<sqinter> (Q ;; P)\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> R \<sqinter> (Q ;; P)

goal (2 subgoals):
 1. Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P 0
 2. \<And>n. \<lbrakk>Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n; Q \<sqsubseteq> R \<sqinter> (Q ;; P)\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Q \<sqsubseteq> R \<sqinter> (Q ;; P)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Q \<sqsubseteq> R \<sqinter> (Q ;; P)

goal (1 subgoal):
 1. Q \<sqsubseteq> R ;; power.power II (;;) P 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> R ;; power.power II (;;) P 0

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n; Q \<sqsubseteq> R \<sqinter> (Q ;; P)\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n; Q \<sqsubseteq> R \<sqinter> (Q ;; P)\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n
Q \<sqsubseteq> R \<sqinter> (Q ;; P)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n; Q \<sqsubseteq> R \<sqinter> (Q ;; P)\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
have "R ;; P \<^bold>^ Suc n = (R ;; P \<^bold>^ n) ;; P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R ;; power.power II (;;) P (Suc n) = (R ;; power.power II (;;) P n) ;; P
[PROOF STEP]
by (metis seqr_assoc upred_semiring.power_Suc2)
[PROOF STATE]
proof (state)
this:
R ;; power.power II (;;) P (Suc n) = (R ;; power.power II (;;) P n) ;; P

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n; Q \<sqsubseteq> R \<sqinter> (Q ;; P)\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R ;; power.power II (;;) P (Suc n) = (R ;; power.power II (;;) P n) ;; P

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n; Q \<sqsubseteq> R \<sqinter> (Q ;; P)\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
have "Q ;; P \<sqsubseteq> ..."
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q ;; P \<sqsubseteq> (R ;; power.power II (;;) P n) ;; P
[PROOF STEP]
by (meson Suc.hyps assms eq_iff seqr_mono)
[PROOF STATE]
proof (state)
this:
Q ;; P \<sqsubseteq> (R ;; power.power II (;;) P n) ;; P

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n; Q \<sqsubseteq> R \<sqinter> (Q ;; P)\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Q ;; P \<sqsubseteq> (R ;; power.power II (;;) P n) ;; P

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n; Q \<sqsubseteq> R \<sqinter> (Q ;; P)\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
have "Q \<sqsubseteq> ..."
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<sqsubseteq> Q ;; P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Q \<sqsubseteq> R \<sqinter> (Q ;; P)

goal (1 subgoal):
 1. Q \<sqsubseteq> Q ;; P
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> Q ;; P

goal (1 subgoal):
 1. \<And>n. \<lbrakk>Q \<sqsubseteq> R \<sqinter> (Q ;; P) \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P n; Q \<sqsubseteq> R \<sqinter> (Q ;; P)\<rbrakk> \<Longrightarrow> Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)

goal (1 subgoal):
 1. Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> R ;; power.power II (;;) P (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SUP_atLeastAtMost_first:
  fixes P :: "nat \<Rightarrow> 'a::complete_lattice"
  assumes "m \<le> n"
  shows "(\<Sqinter>i\<in>{m..n}. P(i)) = P(m) \<sqinter> (\<Sqinter>i\<in>{Suc m..n}. P(i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter>(P ` {m..n}) = P m \<sqinter> \<Sqinter>(P ` {Suc m..n})
[PROOF STEP]
by (metis SUP_insert assms atLeastAtMost_insertL)


[STATEMENT]
lemma upower_seqr_iter: "P \<^bold>^ n = (;; Q : replicate n P \<bullet> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. power.power II (;;) P n = (;; Q : replicate n P \<bullet> Q)
[PROOF STEP]
by (induct n, simp_all add: upred_semiring.power_Suc)


[STATEMENT]
lemma assigns_power: "\<langle>f\<rangle>\<^sub>a \<^bold>^ n = \<langle>f ^^ n\<rangle>\<^sub>a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. power.power II (;;) \<langle>f\<rangle>\<^sub>a n = \<langle>f ^^ n\<rangle>\<^sub>a
[PROOF STEP]
by (induct n, rel_auto+)


[STATEMENT]
lemma ustar_rep_eq:
  "\<lbrakk>P\<^sup>\<star>\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> ({p. \<lbrakk>P\<rbrakk>\<^sub>e p}\<^sup>*))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P\<^sup>\<star>\<rbrakk>\<^sub>e = (\<lambda>b. b \<in> {p. \<lbrakk>P\<rbrakk>\<^sub>e p}\<^sup>*)
[PROOF STEP]
by (simp add: ustar_def, rel_auto, simp_all add: relpow_imp_rtrancl rtrancl_imp_relpow)


[STATEMENT]
lemma uplus_power_def: "P\<^sup>+ = (\<Sqinter> i \<bullet> P \<^bold>^ (Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>+ = (\<Sqinter> i \<bullet> power.power II (;;) P (Suc i))
[PROOF STEP]
by (simp add: uplus_def ustar_def seq_UINF_distl' UINF_atLeast_Suc upred_semiring.power_Suc)


[STATEMENT]
theorem RA1: "(P ;; (Q ;; R)) = ((P ;; Q) ;; R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; Q ;; R = (P ;; Q) ;; R
[PROOF STEP]
by (simp add: seqr_assoc)


[STATEMENT]
theorem RA2: "(P ;; II) = P" "(II ;; P) = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; II = P &&& II ;; P = P
[PROOF STEP]
by simp_all


[STATEMENT]
theorem RA3: "P\<^sup>-\<^sup>- = P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>-\<^sup>- = P
[PROOF STEP]
by simp


[STATEMENT]
theorem RA4: "(P ;; Q)\<^sup>- = (Q\<^sup>- ;; P\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P ;; Q)\<^sup>- = Q\<^sup>- ;; P\<^sup>-
[PROOF STEP]
by simp


[STATEMENT]
theorem RA5: "(P \<or> Q)\<^sup>- = (P\<^sup>- \<or> Q\<^sup>-)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<or> Q)\<^sup>- = (P\<^sup>- \<or> Q\<^sup>-)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
theorem RA6: "((P \<or> Q) ;; R) = (P;;R \<or> Q;;R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<or> Q) ;; R = (P ;; R \<or> Q ;; R)
[PROOF STEP]
using seqr_or_distl
[PROOF STATE]
proof (prove)
using this:
(?P \<or> ?Q) ;; ?R = (?P ;; ?R \<or> ?Q ;; ?R)

goal (1 subgoal):
 1. (P \<or> Q) ;; R = (P ;; R \<or> Q ;; R)
[PROOF STEP]
by blast


[STATEMENT]
lemma ustar_alt_def: "P\<^sup>\<star> = (\<Sqinter> i \<bullet> P \<^bold>^ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>\<star> = (\<Sqinter> i \<bullet> (power.power II (;;) P) i)
[PROOF STEP]
by (simp add: ustar_def)


[STATEMENT]
theorem ustar_sub_unfoldl: "P\<^sup>\<star> \<sqsubseteq> II \<sqinter> (P;;P\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>\<star> \<sqsubseteq> II \<sqinter> (P ;; P\<^sup>\<star>)
[PROOF STEP]
by (rel_simp, simp add: rtrancl_into_trancl2 trancl_into_rtrancl)


[STATEMENT]
theorem ustar_inductl:
  assumes "Q \<sqsubseteq> R" "Q \<sqsubseteq> P ;; Q"
  shows "Q \<sqsubseteq> P\<^sup>\<star> ;; R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<sqsubseteq> P\<^sup>\<star> ;; R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q \<sqsubseteq> P\<^sup>\<star> ;; R
[PROOF STEP]
have "P\<^sup>\<star> ;; R = (\<Sqinter> i. P \<^bold>^ i ;; R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>\<star> ;; R = \<Or>range (\<lambda>i. power.power II (;;) P i ;; R)
[PROOF STEP]
by (simp add: ustar_def UINF_as_Sup_collect' seq_SUP_distr)
[PROOF STATE]
proof (state)
this:
P\<^sup>\<star> ;; R = \<Or>range (\<lambda>i. power.power II (;;) P i ;; R)

goal (1 subgoal):
 1. Q \<sqsubseteq> P\<^sup>\<star> ;; R
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P\<^sup>\<star> ;; R = \<Or>range (\<lambda>i. power.power II (;;) P i ;; R)

goal (1 subgoal):
 1. Q \<sqsubseteq> P\<^sup>\<star> ;; R
[PROOF STEP]
have "Q \<sqsubseteq> ..."
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<sqsubseteq> \<Or>range (\<lambda>i. power.power II (;;) P i ;; R)
[PROOF STEP]
by (simp add: SUP_least assms upower_inductl)
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> \<Or>range (\<lambda>i. power.power II (;;) P i ;; R)

goal (1 subgoal):
 1. Q \<sqsubseteq> P\<^sup>\<star> ;; R
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Q \<sqsubseteq> P\<^sup>\<star> ;; R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Q \<sqsubseteq> P\<^sup>\<star> ;; R

goal (1 subgoal):
 1. Q \<sqsubseteq> P\<^sup>\<star> ;; R
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> P\<^sup>\<star> ;; R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ustar_inductr:
  assumes "Q \<sqsubseteq> R" "Q \<sqsubseteq> Q ;; P"
  shows "Q \<sqsubseteq> R ;; P\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<sqsubseteq> R ;; P\<^sup>\<star>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q \<sqsubseteq> R ;; P\<^sup>\<star>
[PROOF STEP]
have "R ;; P\<^sup>\<star> = (\<Sqinter> i. R ;; P \<^bold>^ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R ;; P\<^sup>\<star> = \<Or>range (\<lambda>i. R ;; power.power II (;;) P i)
[PROOF STEP]
by (simp add: ustar_def UINF_as_Sup_collect' seq_SUP_distl)
[PROOF STATE]
proof (state)
this:
R ;; P\<^sup>\<star> = \<Or>range (\<lambda>i. R ;; power.power II (;;) P i)

goal (1 subgoal):
 1. Q \<sqsubseteq> R ;; P\<^sup>\<star>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R ;; P\<^sup>\<star> = \<Or>range (\<lambda>i. R ;; power.power II (;;) P i)

goal (1 subgoal):
 1. Q \<sqsubseteq> R ;; P\<^sup>\<star>
[PROOF STEP]
have "Q \<sqsubseteq> ..."
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<sqsubseteq> \<Or>range (\<lambda>i. R ;; power.power II (;;) P i)
[PROOF STEP]
by (simp add: SUP_least assms upower_inductr)
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> \<Or>range (\<lambda>i. R ;; power.power II (;;) P i)

goal (1 subgoal):
 1. Q \<sqsubseteq> R ;; P\<^sup>\<star>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Q \<sqsubseteq> R ;; P\<^sup>\<star>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Q \<sqsubseteq> R ;; P\<^sup>\<star>

goal (1 subgoal):
 1. Q \<sqsubseteq> R ;; P\<^sup>\<star>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Q \<sqsubseteq> R ;; P\<^sup>\<star>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ustar_refines_nu: "(\<nu> X \<bullet> (P ;; X) \<sqinter> II) \<sqsubseteq> P\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> X \<bullet> (P ;; X) \<sqinter> II) \<sqsubseteq> P\<^sup>\<star>
[PROOF STEP]
by (metis (no_types, lifting) lfp_greatest semilattice_sup_class.le_sup_iff
      semilattice_sup_class.sup_idem upred_semiring.mult_2_right
      upred_semiring.one_add_one ustar_inductl)


[STATEMENT]
lemma ustar_as_nu: "P\<^sup>\<star> = (\<nu> X \<bullet> (P ;; X) \<sqinter> II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>\<star> = (\<nu> X \<bullet> (P ;; X) \<sqinter> II)
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<nu> X \<bullet> (P ;; X) \<sqinter> II) \<sqsubseteq> P\<^sup>\<star>
 2. P\<^sup>\<star> \<sqsubseteq> (\<nu> X \<bullet> (P ;; X) \<sqinter> II)
[PROOF STEP]
show "(\<nu> X \<bullet> (P ;; X) \<sqinter> II) \<sqsubseteq> P\<^sup>\<star>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> X \<bullet> (P ;; X) \<sqinter> II) \<sqsubseteq> P\<^sup>\<star>
[PROOF STEP]
by (simp add: ustar_refines_nu)
[PROOF STATE]
proof (state)
this:
(\<nu> X \<bullet> (P ;; X) \<sqinter> II) \<sqsubseteq> P\<^sup>\<star>

goal (1 subgoal):
 1. P\<^sup>\<star> \<sqsubseteq> (\<nu> X \<bullet> (P ;; X) \<sqinter> II)
[PROOF STEP]
show "P\<^sup>\<star> \<sqsubseteq> (\<nu> X \<bullet> (P ;; X) \<sqinter> II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>\<star> \<sqsubseteq> (\<nu> X \<bullet> (P ;; X) \<sqinter> II)
[PROOF STEP]
by (metis lfp_lowerbound upred_semiring.add_commute ustar_sub_unfoldl)
[PROOF STATE]
proof (state)
this:
P\<^sup>\<star> \<sqsubseteq> (\<nu> X \<bullet> (P ;; X) \<sqinter> II)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ustar_unfoldl: "P\<^sup>\<star> = II \<sqinter> (P ;; P\<^sup>\<star>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>\<star> = II \<sqinter> (P ;; P\<^sup>\<star>)
[PROOF STEP]
apply (simp add: ustar_as_nu)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nu> X \<bullet> (P ;; X) \<sqinter> II) = II \<sqinter> (P ;; (\<nu> X \<bullet> (P ;; X) \<sqinter> II))
[PROOF STEP]
apply (subst lfp_unfold)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Monotonic (\<lambda>X. (P ;; X) \<sqinter> II)
 2. (P ;; (\<nu> X \<bullet> (P ;; X) \<sqinter> II)) \<sqinter> II = II \<sqinter> (P ;; (\<nu> X \<bullet> (P ;; X) \<sqinter> II))
[PROOF STEP]
apply (rule monoI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. y \<sqsubseteq> x \<Longrightarrow> (P ;; y) \<sqinter> II \<sqsubseteq> (P ;; x) \<sqinter> II
 2. (P ;; (\<nu> X \<bullet> (P ;; X) \<sqinter> II)) \<sqinter> II = II \<sqinter> (P ;; (\<nu> X \<bullet> (P ;; X) \<sqinter> II))
[PROOF STEP]
apply (rel_auto)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma while_star_form:
  "while b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; [(\<not>b)]\<^sup>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
have 1: "Continuous (\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Continuous (\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
by (rel_auto)
[PROOF STATE]
proof (state)
this:
Continuous (\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II)

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
have "while b do P od = (\<Sqinter>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false)
[PROOF STEP]
by (simp add: "1" false_upred_def sup_continuous_Continuous sup_continuous_lfp while_top_def)
[PROOF STATE]
proof (state)
this:
while\<^sup>\<top> b do P od = \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false)

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
while\<^sup>\<top> b do P od = \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false)

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
have "... = ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<sqinter> (\<Sqinter>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i+1)) false)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false) = ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<sqinter> \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false)
[PROOF STEP]
by (subst Sup_power_expand, simp)
[PROOF STATE]
proof (state)
this:
\<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false) = ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<sqinter> \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false)

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false) = ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<sqinter> \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false)

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
have "... = (\<Sqinter>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i+1)) false)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<sqinter> \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false) = \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false)
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<sqinter> \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false) = \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false)

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<sqinter> \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false) = \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false)

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
have "... = (\<Sqinter>i. (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^bold>^i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false) = \<Or>range (\<lambda>i. power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II))
[PROOF STEP]
proof (rule SUP_cong, simp_all)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ x) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) x ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ x) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) x ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
show "P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = (P \<triangleleft> b \<triangleright>\<^sub>r II) \<^bold>^ i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
proof (induct i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) 0 ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
 2. \<And>i. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II) \<Longrightarrow> P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ Suc i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) (Suc i) ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) 0 ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
 2. \<And>i. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II) \<Longrightarrow> P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ Suc i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) (Suc i) ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) 0 ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ 0) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) 0 ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)

goal (1 subgoal):
 1. \<And>i. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II) \<Longrightarrow> P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ Suc i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) (Suc i) ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II) \<Longrightarrow> P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ Suc i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) (Suc i) ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)

goal (1 subgoal):
 1. \<And>i. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II) \<Longrightarrow> P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ Suc i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) (Suc i) ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)

goal (1 subgoal):
 1. P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ Suc i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) (Suc i) ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)
[PROOF STEP]
by (simp add: upred_semiring.power_Suc)
           (metis (no_types, lifting) RA1 comp_cond_left_distr cond_L6 upred_semiring.mult.left_neutral)
[PROOF STATE]
proof (state)
this:
P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ Suc i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) (Suc i) ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P ;; ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ i) false \<triangleleft> b \<triangleright>\<^sub>r II = power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false) = \<Or>range (\<lambda>i. power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II))

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Or>range (\<lambda>i. ((\<lambda>X. P ;; X \<triangleleft> b \<triangleright>\<^sub>r II) ^^ (i + 1)) false) = \<Or>range (\<lambda>i. power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II))

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
have "... = (\<Sqinter>i\<in>{0..} \<bullet> (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^bold>^i ;; [(\<not>b)]\<^sup>\<top>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Or>range (\<lambda>i. power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)) = (\<Sqinter> i \<in> {0..} \<bullet> power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; ?[\<not> b])
[PROOF STEP]
by (rel_auto)
[PROOF STATE]
proof (state)
this:
\<Or>range (\<lambda>i. power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)) = (\<Sqinter> i \<in> {0..} \<bullet> power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; ?[\<not> b])

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Or>range (\<lambda>i. power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; (false \<triangleleft> b \<triangleright>\<^sub>r II)) = (\<Sqinter> i \<in> {0..} \<bullet> power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; ?[\<not> b])

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
have "... = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; [(\<not>b)]\<^sup>\<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter> i \<in> {0..} \<bullet> power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; ?[\<not> b]) = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
by (metis seq_UINF_distr ustar_def)
[PROOF STATE]
proof (state)
this:
(\<Sqinter> i \<in> {0..} \<bullet> power.power II (;;) (P \<triangleleft> b \<triangleright>\<^sub>r II) i ;; ?[\<not> b]) = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]

goal (1 subgoal):
 1. while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
while\<^sup>\<top> b do P od = (P \<triangleleft> b \<triangleright>\<^sub>r II)\<^sup>\<star> ;; ?[\<not> b]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uomega_induct:
  "P ;; P\<^sup>\<omega> \<sqsubseteq> P\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P ;; P\<^sup>\<omega> \<sqsubseteq> P\<^sup>\<omega>
[PROOF STEP]
by (simp add: uomega_def, metis eq_refl gfp_unfold monoI seqr_mono)


[STATEMENT]
lemma skip_r_refine:
  "(p \<Rightarrow> p) \<sqsubseteq> II"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p \<Rightarrow> p) \<sqsubseteq> II
[PROOF STEP]
by pred_blast


[STATEMENT]
lemma conj_refine_left:
  "(Q \<Rightarrow> P) \<sqsubseteq> R \<Longrightarrow> P \<sqsubseteq> (Q \<and> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Q \<Rightarrow> P) \<sqsubseteq> R \<Longrightarrow> P \<sqsubseteq> (Q \<and> R)
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma pre_weak_rel:
  assumes "`Pre \<Rightarrow> I`"
  and     "(I \<Rightarrow> Post) \<sqsubseteq> P"
  shows "(Pre \<Rightarrow> Post) \<sqsubseteq> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
`Pre \<Rightarrow> I`
(I \<Rightarrow> Post) \<sqsubseteq> P

goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> P
[PROOF STEP]
by(rel_auto)


[STATEMENT]
lemma cond_refine_rel:
  assumes "S \<sqsubseteq> (\<lceil>b\<rceil>\<^sub>< \<and> P)" "S \<sqsubseteq> (\<lceil>\<not>b\<rceil>\<^sub>< \<and> Q)"
  shows "S \<sqsubseteq> P \<triangleleft> b \<triangleright>\<^sub>r Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<sqsubseteq> P \<triangleleft> b \<triangleright>\<^sub>r Q
[PROOF STEP]
by (metis aext_not assms(1) assms(2) cond_def lift_rcond_def utp_pred_laws.le_sup_iff)


[STATEMENT]
lemma seq_refine_pred:
  assumes "(\<lceil>b\<rceil>\<^sub>< \<Rightarrow> \<lceil>s\<rceil>\<^sub>>) \<sqsubseteq> P" and "(\<lceil>s\<rceil>\<^sub>< \<Rightarrow> \<lceil>c\<rceil>\<^sub>>) \<sqsubseteq> Q"
  shows "(\<lceil>b\<rceil>\<^sub>< \<Rightarrow> \<lceil>c\<rceil>\<^sub>>) \<sqsubseteq> (P ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lceil>b\<rceil>\<^sub>< \<Rightarrow> \<lceil>c\<rceil>\<^sub>>) \<sqsubseteq> P ;; Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<lceil>b\<rceil>\<^sub>< \<Rightarrow> \<lceil>s\<rceil>\<^sub>>) \<sqsubseteq> P
(\<lceil>s\<rceil>\<^sub>< \<Rightarrow> \<lceil>c\<rceil>\<^sub>>) \<sqsubseteq> Q

goal (1 subgoal):
 1. (\<lceil>b\<rceil>\<^sub>< \<Rightarrow> \<lceil>c\<rceil>\<^sub>>) \<sqsubseteq> P ;; Q
[PROOF STEP]
by rel_auto


[STATEMENT]
lemma seq_refine_unrest:
  assumes "out\<alpha> \<sharp> b" "in\<alpha> \<sharp> c"
  assumes "(b \<Rightarrow> \<lceil>s\<rceil>\<^sub>>) \<sqsubseteq> P" and "(\<lceil>s\<rceil>\<^sub>< \<Rightarrow> c) \<sqsubseteq> Q"
  shows "(b \<Rightarrow> c) \<sqsubseteq> (P ;; Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<Rightarrow> c) \<sqsubseteq> P ;; Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
out\<alpha> \<sharp> b
in\<alpha> \<sharp> c
(b \<Rightarrow> \<lceil>s\<rceil>\<^sub>>) \<sqsubseteq> P
(\<lceil>s\<rceil>\<^sub>< \<Rightarrow> c) \<sqsubseteq> Q

goal (1 subgoal):
 1. (b \<Rightarrow> c) \<sqsubseteq> P ;; Q
[PROOF STEP]
by rel_blast


[STATEMENT]
lemma Dom_conv_Ran:
  "Dom(P\<^sup>-) = Ran(P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom (P\<^sup>-) = Ran P
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma Ran_conv_Dom:
  "Ran(P\<^sup>-) = Dom(P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ran (P\<^sup>-) = Dom P
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma Dom_skip:
  "Dom(II) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom II = true
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma Dom_assigns:
  "Dom(\<langle>\<sigma>\<rangle>\<^sub>a) = true"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom \<langle>\<sigma>\<rangle>\<^sub>a = true
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma Dom_miracle:
  "Dom(false) = false"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Dom false = false
[PROOF STEP]
by (rel_auto)