theory Trace_More_RG

lemma handy_prop_divs_rg:
  assumes x: "\<And>P. \<lbrace>\<lambda>s0 s. P (Q s0 s) \<and> S s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. P (Q' rv s0 s)\<rbrace>"
             "\<And>P. \<lbrace>\<lambda>s0 s. P (R s0 s) \<and> S s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. P (R' rv s0 s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s0 s. P (Q s0 s \<and> R s0 s) \<and> S s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. P (Q' rv s0 s \<and> R' rv s0 s)\<rbrace>"
             "\<lbrace>\<lambda>s0 s. P (Q s0 s \<or> R s0 s) \<and> S s0 s\<rbrace>,\<lbrace>R\<rbrace> f -,\<lbrace>\<lambda>rv s0 s. P (Q' rv s0 s \<or> R' rv s0 s)\<rbrace>" apply (clarsimp simp: validI_def validI_prefix_closed[OF x(1)]
                  elim!: subst[rotated, where P=P]) apply (rule use_validI [OF _ x(1)], assumption) apply (rule use_validI [OF _ x(2)], assumption) apply simp apply (clarsimp simp: validI_def validI_prefix_closed[OF x(1)]
                 elim!: subst[rotated, where P=P]) apply (rule use_validI [OF _ x(1)], assumption) apply (rule use_validI [OF _ x(2)], assumption) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P (Q s0 s \<and> R s0 s) \<and> S s0 s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. P (Q' rv s0 s \<and> R' rv s0 s)\<rbrace> &&& \<lbrace>\<lambda>s0 s. P (Q s0 s \<or> R s0 s) \<and> S s0 s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. P (Q' rv s0 s \<or> R' rv s0 s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s'. \<lbrakk>S s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> (Q s0 s \<and> R s0 s) = (Q' rv (last_st_tr tr s0) s' \<and> R' rv (last_st_tr tr s0) s')
 2. \<lbrace>\<lambda>s0 s. P (Q s0 s \<or> R s0 s) \<and> S s0 s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. P (Q' rv s0 s \<or> R' rv s0 s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s'. \<lbrakk>S s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> (Q s0 s \<and> R s0 s) = (Q s0 s \<and> R' rv (last_st_tr tr s0) s') \<and> S s0 s
 2. \<lbrace>\<lambda>s0 s. P (Q s0 s \<or> R s0 s) \<and> S s0 s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. P (Q' rv s0 s \<or> R' rv s0 s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s'. \<lbrakk>S s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> ((Q s0 s \<and> R s0 s) = (Q s0 s \<and> R s0 s) \<and> S s0 s) \<and> S s0 s
 2. \<lbrace>\<lambda>s0 s. P (Q s0 s \<or> R s0 s) \<and> S s0 s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. P (Q' rv s0 s \<or> R' rv s0 s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P (Q s0 s \<or> R s0 s) \<and> S s0 s\<rbrace>, \<lbrace>R\<rbrace> f -, \<lbrace>\<lambda>rv s0 s. P (Q' rv s0 s \<or> R' rv s0 s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>S s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> (Q s0 s \<or> R s0 s) = (Q' rv (last_st_tr tr s0) s' \<or> R' rv (last_st_tr tr s0) s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>S s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> (Q s0 s \<or> R s0 s) = (Q s0 s \<or> R' rv (last_st_tr tr s0) s') \<and> S s0 s proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>S s0 s; (tr, Result (rv, s')) \<in> rely f R s0 s\<rbrakk> \<Longrightarrow> ((Q s0 s \<or> R s0 s) = (Q s0 s \<or> R s0 s) \<and> S s0 s) \<and> S s0 s proof (prove)
goal:
No subgoals!