theory Corres_D

lemma corres_throw_skip_r:
  assumes c: "corres_underlying R False z (dc \<oplus> r) P P' (f \<sqinter> Monads_D.throw) g'"
  assumes eq: "\<And>s. \<lbrace>(=) s\<rbrace> f' \<lbrace>\<lambda>_. (=) s\<rbrace>"
  assumes nf: "z \<longrightarrow> no_fail P' f'"
  shows "corres_underlying R nf z (dc \<oplus> r) P P' (f \<sqinter> Monads_D.throw) (f' >>=E (\<lambda>_. g'))" using c apply (clarsimp simp: corres_underlying_def alternative_def bindE_def) apply (drule (1) bspec) apply (rule conjI) apply (clarsimp simp: in_bind) apply (frule use_valid, rule eq, rule refl) apply clarsimp apply (clarsimp simp: lift_def in_throwError split: sum.splits) apply (simp add: throwError_def return_def) apply (drule (1) bspec, clarsimp) apply clarsimp apply (clarsimp simp: bind_def) apply (erule disjE) prefer 2 apply (insert nf)[1] apply (clarsimp simp: no_fail_def) apply (clarsimp simp: lift_def throwError_def return_def split: sum.splits) apply (frule use_valid, rule eq, rule refl) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying R nf z (dc \<oplus> r) P P' (f \<sqinter> throw) (doE _ <- f';
g'
odE) proof (prove)
using this:
corres_underlying R False z (dc \<oplus> r) P P' (f \<sqinter> throw) g'

goal (1 subgoal):
 1. corres_underlying R nf z (dc \<oplus> r) P P' (f \<sqinter> throw) (doE _ <- f';
g'
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s) \<union> fst (throw s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' s')); (a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((f' >>= lift (\<lambda>_. g')) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd ((f' >>= lift (\<lambda>_. g')) b)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); case (a, b) of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s) \<union> fst (throw s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' s'))\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((f' >>= lift (\<lambda>_. g')) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd ((f' >>= lift (\<lambda>_. g')) b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); case (a, b) of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s) \<union> fst (throw s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' s'))\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((f' >>= lift (\<lambda>_. g')) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); case (a, b) of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s) \<union> fst (throw s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' s'))\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift (\<lambda>_. g')) b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' x. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z \<longrightarrow> \<not> snd (g' b); (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift (\<lambda>_. g') x s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); case (a, b) of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s) \<union> fst (throw s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' s'))\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift (\<lambda>_. g')) b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' x. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z \<longrightarrow> \<not> snd (g' b); (x, s'') \<in> fst (f' b); (aa, ba) \<in> fst (lift (\<lambda>_. g') x s''); b = s''\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); case (a, b) of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s) \<union> fst (throw s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' s'))\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift (\<lambda>_. g')) b) proof (prove)
goal (2 subgoals):
 1. \<And>a aa ba s'' x. \<lbrakk>(a, s'') \<in> R; P a; P' s''; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' s''). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z \<longrightarrow> \<not> snd (g' s''); (x, s'') \<in> fst (f' s''); (aa, ba) \<in> fst (lift (\<lambda>_. g') x s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); case (a, b) of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s) \<union> fst (throw s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' s'))\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift (\<lambda>_. g')) b) proof (prove)
goal (3 subgoals):
 1. \<And>a ba x1. \<lbrakk>(a, ba) \<in> R; P a; P' ba; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z \<longrightarrow> \<not> snd (g' ba); (Inl x1, ba) \<in> fst (f' ba)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (r, t) \<Rightarrow> (t, ba) \<in> R \<and> (\<exists>x'. r = Inl x')
 2. \<And>a aa ba s'' x2. \<lbrakk>(a, s'') \<in> R; P a; P' s''; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' s''). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z \<longrightarrow> \<not> snd (g' s''); (Inr x2, s'') \<in> fst (f' s''); (aa, ba) \<in> fst (g' s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa
 3. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); case (a, b) of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s) \<union> fst (throw s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' s'))\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift (\<lambda>_. g')) b) proof (prove)
goal (2 subgoals):
 1. \<And>a aa ba s'' x2. \<lbrakk>(a, s'') \<in> R; P a; P' s''; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' s''). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z \<longrightarrow> \<not> snd (g' s''); (Inr x2, s'') \<in> fst (f' s''); (aa, ba) \<in> fst (g' s'')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); case (a, b) of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s) \<union> fst (throw s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' s'))\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift (\<lambda>_. g')) b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); case (a, b) of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (g' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s) \<union> fst (throw s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (z \<longrightarrow> \<not> snd (g' s'))\<rbrakk> \<Longrightarrow> z \<longrightarrow> \<not> snd ((f' >>= lift (\<lambda>_. g')) b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z; snd ((f' >>= lift (\<lambda>_. g')) b); \<not> snd (g' b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z; (\<exists>x\<in>fst (f' b). snd (case x of (x, xa) \<Rightarrow> lift (\<lambda>_. g') x xa)) \<or> snd (f' b); \<not> snd (g' b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z; \<not> snd (g' b); \<exists>x\<in>fst (f' b). snd (case x of (x, xa) \<Rightarrow> lift (\<lambda>_. g') x xa)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z; \<not> snd (g' b); snd (f' b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z; \<not> snd (g' b); snd (f' b)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z; \<not> snd (g' b); \<exists>x\<in>fst (f' b). snd (case x of (x, xa) \<Rightarrow> lift (\<lambda>_. g') x xa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z; \<not> snd (g' b); snd (f' b); z \<longrightarrow> no_fail P' f'\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z; \<not> snd (g' b); \<exists>x\<in>fst (f' b). snd (case x of (x, xa) \<Rightarrow> lift (\<lambda>_. g') x xa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a) \<and> \<not> snd (throw a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a) \<union> fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; z; \<not> snd (g' b); \<exists>x\<in>fst (f' b). snd (case x of (x, xa) \<Rightarrow> lift (\<lambda>_. g') x xa)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b ba x2. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> (a, t') \<in> R \<and> (\<exists>y'. r' = Inl y') \<or> (\<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'); z; \<not> snd (g' b); (Inr x2, ba) \<in> fst (f' b); snd (g' ba)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b ba x2. \<lbrakk>(a, b) \<in> R; P a; P' b; nf \<longrightarrow> \<not> snd (f a); \<forall>x\<in>fst (g' b). case x of (r', t') \<Rightarrow> (a, t') \<in> R \<and> (\<exists>y'. r' = Inl y') \<or> (\<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'); z; \<not> snd (g' b); (Inr x2, ba) \<in> fst (f' b); snd (g' ba); b = ba\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!