theory Corres_UL_C

lemma ccorres_liftM_simp [simp]:
  "(ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g)
    = (ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g)" apply rule apply (rule ccorresI') apply (erule (3) ccorresE) apply clarsimp apply assumption apply (clarsimp simp add: liftM_def bind_def return_def) apply (erule bexI [rotated]) apply (simp add: unif_rrel_def) apply (rule ccorresI') apply simp apply (erule (5) ccorresE) apply (simp add: liftM_def Nondet_Monad.bind_def return_def) apply (erule bexI [rotated]) apply (simp add: unif_rrel_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g = ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g proof (prove)
goal (2 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g \<Longrightarrow> ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g
 2. ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g; (s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, ta)\<in>fst (f s). (ta, t') \<in> sr \<and> unif_rrel (n = length hs) (r \<circ> t) xf (arrel \<circ> t) axf ra t')
 2. ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<not> snd (liftM t f s)
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (?n5 s s' n z, ?x5 s s' n z)
 3. \<And>s s' n z t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); ?x5 s s' n z = Normal t'; (ra, ta) \<in> fst (liftM t f s); (ta, t') \<in> sr; unif_rrel (?n5 s s' n z = length hs) r xf arrel axf ra t'; ?n5 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, ta)\<in>fst (f s). (ta, t') \<in> sr \<and> unif_rrel (n = length hs) (r \<circ> t) xf (arrel \<circ> t) axf ra t')
 4. ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (?n5 s s' n z, ?x5 s s' n z)
 2. \<And>s s' n z t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); ?x5 s s' n z = Normal t'; (ra, ta) \<in> fst (liftM t f s); (ta, t') \<in> sr; unif_rrel (?n5 s s' n z = length hs) r xf arrel axf ra t'; ?n5 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, ta)\<in>fst (f s). (ta, t') \<in> sr \<and> unif_rrel (n = length hs) (r \<circ> t) xf (arrel \<circ> t) axf ra t')
 3. ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); z = Normal t'; (ra, ta) \<in> fst (liftM t f s); (ta, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, ta)\<in>fst (f s). (ta, t') \<in> sr \<and> unif_rrel (n = length hs) (r \<circ> t) xf (arrel \<circ> t) axf ra t')
 2. ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g proof (prove)
goal (2 subgoals):
 1. \<And>s s' n t' ta a. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (f s); (ta, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf (t a) t'; n \<le> length hs; (a, ta) \<in> fst (f s)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). case x of (ra, ta) \<Rightarrow> (ta, t') \<in> sr \<and> unif_rrel (n = length hs) (r \<circ> t) xf (arrel \<circ> t) axf ra t'
 2. ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g proof (prove)
goal (2 subgoals):
 1. \<And>s s' n t' ta a. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (f s); (ta, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf (t a) t'; n \<le> length hs\<rbrakk> \<Longrightarrow> case (a, ta) of (ra, ta) \<Rightarrow> (ta, t') \<in> sr \<and> unif_rrel (n = length hs) (r \<circ> t) xf (arrel \<circ> t) axf ra t'
 2. ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs (liftM t f) g proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g; (s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (liftM t f s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (liftM t f s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr \<Gamma> (r \<circ> t) xf (arrel \<circ> t) axf P P' hs f g; (s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (liftM t f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); z = Normal t'; (ra, ta) \<in> fst (f s); (ta, t') \<in> sr; unif_rrel (n = length hs) (r \<circ> t) xf (arrel \<circ> t) axf ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (liftM t f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (f s); z = Normal t'; (ra, ta) \<in> fst (f s); (ta, t') \<in> sr; unif_rrel (n = length hs) (r \<circ> t) xf (arrel \<circ> t) axf ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (f s). \<exists>x\<in>fst (case y of (x, s) \<Rightarrow> ({(t x, s)}, False)). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' ra ta. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (f s); z = Normal t'; (ta, t') \<in> sr; unif_rrel (n = length hs) (r \<circ> t) xf (arrel \<circ> t) axf ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case (ra, ta) of (x, s) \<Rightarrow> ({(t x, s)}, False)). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t' proof (prove)
goal:
No subgoals!