theory MonadicRewrite_C

lemma monadic_rewrite_ccorres_assemble:
  assumes cc: "ccorres_underlying sr G r xf ar axf P P' hs f c"
  assumes mr: "monadic_rewrite F E Q g f"
  shows       "ccorres_underlying sr G r xf ar axf (P and Q) P' hs g c" proof - have snd: "\<And>s. \<lbrakk> Q s; \<not> snd (g s) \<rbrakk> \<Longrightarrow> \<not> snd (f s)" using mr by (fastforce simp: monadic_rewrite_def) have fst: "\<And>s v. \<lbrakk> Q s; \<not> snd (g s); v \<in> fst (f s) \<rbrakk> \<Longrightarrow> v \<in> fst (g s)" using mr by (auto simp add: monadic_rewrite_def) show ?thesis apply (rule ccorresI') apply (erule ccorresE[OF cc], (simp add: snd)+) apply clarsimp apply (rule rev_bexI[OF fst], assumption+) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr G r xf ar axf (P and Q) P' hs g c proof (state)
goal (1 subgoal):
 1. ccorres_underlying sr G r xf ar axf (P and Q) P' hs g c proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Q s; \<not> snd (g s)\<rbrakk> \<Longrightarrow> \<not> snd (f s) proof (prove)
using this:
monadic_rewrite F E Q g f

goal (1 subgoal):
 1. \<And>s. \<lbrakk>Q s; \<not> snd (g s)\<rbrakk> \<Longrightarrow> \<not> snd (f s) proof (state)
this:
\<lbrakk>Q ?s; \<not> snd (g ?s)\<rbrakk> \<Longrightarrow> \<not> snd (f ?s)

goal (1 subgoal):
 1. ccorres_underlying sr G r xf ar axf (P and Q) P' hs g c proof (prove)
goal (1 subgoal):
 1. \<And>s v. \<lbrakk>Q s; \<not> snd (g s); v \<in> fst (f s)\<rbrakk> \<Longrightarrow> v \<in> fst (g s) proof (prove)
using this:
monadic_rewrite F E Q g f

goal (1 subgoal):
 1. \<And>s v. \<lbrakk>Q s; \<not> snd (g s); v \<in> fst (f s)\<rbrakk> \<Longrightarrow> v \<in> fst (g s) proof (state)
this:
\<lbrakk>Q ?s; \<not> snd (g ?s); ?v \<in> fst (f ?s)\<rbrakk> \<Longrightarrow> ?v \<in> fst (g ?s)

goal (1 subgoal):
 1. ccorres_underlying sr G r xf ar axf (P and Q) P' hs g c proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr G r xf ar axf (P and Q) P' hs g c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (P and Q) s; s' \<in> P'; G\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (g s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (g s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf ar axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' ra t. \<lbrakk>P s \<and> Q s; s' \<in> P'; G\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (g s); z = Normal t'; (ra, t) \<in> fst (f s); (t, t') \<in> sr; unif_rrel (n = length hs) r xf ar axf ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf ar axf ra t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' n t' ra t. \<lbrakk>s' \<in> P'; G\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (g s); (ra, t) \<in> fst (f s); (t, t') \<in> sr; unif_rrel (n = length hs) r xf ar axf ra t'; n \<le> length hs; P s; Q s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf ar axf ra t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' n t' ra t. \<lbrakk>s' \<in> P'; G\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (g s); (ra, t) \<in> fst (f s); (t, t') \<in> sr; unif_rrel (n = length hs) r xf ar axf ra t'; n \<le> length hs; P s; Q s\<rbrakk> \<Longrightarrow> case (ra, t) of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf ar axf ra t' proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres_underlying sr G r xf ar axf (P and Q) P' hs g c

goal:
No subgoals!