theory Delete_C

lemma ccorres_drop_cutMon_bindE:
  "ccorres_underlying sr Gamm r xf arrel axf P P' hs (f >>=E f') g
    \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' hs (cutMon Q f >>=E f') g" apply (clarsimp simp: ccorres_underlying_def
                        cutMon_def fail_def bind_def bindE_def lift_def
                 split: if_split_asm) apply (subst if_P, simp)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamm r xf arrel axf P P' hs (f >>=E f') g \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' hs (cutMon Q f >>=E f') g proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>\<not> snd (f a); Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> (\<forall>x\<in>fst (f s). \<not> snd (case x of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa)) \<and> \<not> snd (f 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 (\<Union>a\<in>fst (f s). fst (case a of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa), (\<exists>x\<in>fst (f s). snd (case x of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa)) \<or> snd (f s)). (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'; Q a; \<forall>x\<in>fst (f a). \<not> snd (case x of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (\<Union>a\<in>fst (if Q a then f a else fail a). fst (case a of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa), (\<exists>x\<in>fst (if Q a then f a else fail a). snd (case x of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa)) \<or> snd (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>\<not> snd (f a); Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> (\<forall>x\<in>fst (f s). \<not> snd (case x of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa)) \<and> \<not> snd (f 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 (\<Union>a\<in>fst (f s). fst (case a of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa), (\<exists>x\<in>fst (f s). snd (case x of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa)) \<or> snd (f s)). (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'; Q a; \<forall>x\<in>fst (f a). \<not> snd (case x of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (\<Union>a\<in>fst (f a). fst (case a of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa), (\<exists>x\<in>fst (f a). snd (case x of (x, xa) \<Rightarrow> Nondet_Monad.lift f' x xa)) \<or> snd (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!