theory Delete_C

lemma ccorres_cutMon:
  "(\<And>s. Q s \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' hs (cutMon ((=) s) f) g)
        \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' hs (cutMon Q f) g" apply (clarsimp simp: ccorres_underlying_def
                        cutMon_def fail_def bind_def
                 split: if_split_asm) apply (erule meta_allE, drule(1) meta_mp) apply (drule(1) bspec) apply (clarsimp simp: fail_def
                 split: if_split_asm) apply (subst if_P, assumption)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. Q s \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' hs (cutMon ((=) s) f) g) \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' hs (cutMon Q f) g proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>\<And>s. Q s \<Longrightarrow> \<forall>x\<in>sr. case x of (sa, s') \<Rightarrow> P sa \<and> s' \<in> P' \<and> \<not> snd (if s = sa then f sa else fail sa) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (if s = sa then f sa else fail sa). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False)); (a, b) \<in> sr; P a; b \<in> P'; Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t); Q a; \<not> snd (f a)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (if Q a then f a else fail a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> sr; P a; b \<in> P'; Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t); Q a; \<not> snd (f a); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (if a = s then f s else fail s) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (if a = s then f s else fail s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False))\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (if Q a then f a else fail a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> sr; P a; b \<in> P'; Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t); Q a; \<not> snd (f a); case (a, b) of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (if a = s then f s else fail s) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (if a = s then f s else fail s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False))\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (if Q a then f a else fail a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> sr; P a; b \<in> P'; Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t); Q a; \<not> snd (f a); \<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (f a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (if Q a then f a else fail a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> sr; P a; b \<in> P'; Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t); Q a; \<not> snd (f a); \<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (f a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (f a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!