theory Trace_RG

lemma rg_liftP_ext:
  assumes "\<And>P x. m \<lbrace>R\<rbrace>,\<lbrace>G\<rbrace>,\<lbrace>\<lambda>s0 s. P s0 (f s x)\<rbrace>"
  shows "m \<lbrace>R\<rbrace>,\<lbrace>G\<rbrace>,\<lbrace>\<lambda>s0 s. P s0 (f s)\<rbrace>" unfolding validI_def apply (rule conjI, rule validI_prefix_closed[OF assms]) apply clarsimp apply (rule conjI, clarsimp simp: rely_def, erule (2) validI_GD[OF assms]) apply clarsimp apply (erule subst2[rotated 2, where P=P]) apply (drule use_validI, rule assms, rule refl) apply simp apply (rule ext) apply (drule use_validI, rule assms, rule refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. P s0 (f s)\<rbrace>, \<lbrace>R\<rbrace> m \<lbrace>G\<rbrace>, \<lbrace>\<lambda>_ s0 s. P s0 (f s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. prefix_closed m \<and> (\<forall>s0 s tr res. P s0 (f s) \<and> (tr, res) \<in> rely m R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> P (last_st_tr tr s0) (f s'))) proof (prove)
goal (1 subgoal):
 1. \<forall>s0 s tr res. P s0 (f s) \<and> (tr, res) \<in> rely m R s0 s \<longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> P (last_st_tr tr s0) (f s')) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>P s0 (f s); (tr, res) \<in> rely m R s0 s\<rbrakk> \<Longrightarrow> guar_cond G s0 tr \<and> (\<forall>rv s'. res = Result (rv, s') \<longrightarrow> P (last_st_tr tr s0) (f s')) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr res. \<lbrakk>P s0 (f s); (tr, res) \<in> rely m R s0 s\<rbrakk> \<Longrightarrow> \<forall>rv s'. res = Result (rv, s') \<longrightarrow> P (last_st_tr tr s0) (f s') proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. \<lbrakk>P s0 (f s); (tr, Result (rv, s')) \<in> rely m R s0 s\<rbrakk> \<Longrightarrow> P (last_st_tr tr s0) (f s') proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely m R s0 s \<Longrightarrow> s0 = last_st_tr tr s0
 2. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely m R s0 s \<Longrightarrow> f s = f s' proof (prove)
goal (2 subgoals):
 1. \<And>s0 s tr rv s'. ?t40 s0 (last_st_tr tr s0) s tr rv s' (f s' (?x34 s0 s tr rv s')) = ?t39 s0 (last_st_tr tr s0) s tr rv s' (f s' (?x34 s0 s tr rv s')) \<Longrightarrow> s0 = last_st_tr tr s0
 2. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely m R s0 s \<Longrightarrow> f s = f s'
flex-flex pairs:
\<lambda>s0 s tr rv s'. ?t39 s0 s0 s tr rv s' (f s (?x34 s0 s tr rv s')) \<equiv>\<^sup>? \<lambda>s0 s tr rv s'. ?t40 s0 s0 s tr rv s' (f s (?x34 s0 s tr rv s')) proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s'. (tr, Result (rv, s')) \<in> rely m R s0 s \<Longrightarrow> f s = f s' proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s' x. (tr, Result (rv, s')) \<in> rely m R s0 s \<Longrightarrow> f s x = f s' x proof (prove)
goal (1 subgoal):
 1. \<And>s0 s tr rv s' x. ?t53 s0 (last_st_tr tr s0) s tr rv s' x (f s' (?x47 s0 s tr rv s' x)) = ?t52 s0 (last_st_tr tr s0) s tr rv s' x (f s' (?x47 s0 s tr rv s' x)) \<Longrightarrow> f s x = f s' x
flex-flex pairs:
\<lambda>s0 s tr rv s' x. ?t52 s0 s0 s tr rv s' x (f s (?x47 s0 s tr rv s' x)) \<equiv>\<^sup>? \<lambda>s0 s tr rv s' x. ?t53 s0 s0 s tr rv s' x (f s (?x47 s0 s tr rv s' x)) proof (prove)
goal:
No subgoals!