theory Corres_UL_C

lemma ccorres_symb_exec_l:
  assumes cc: "\<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv) hs (f rv) c"
  and   pres: "\<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>"
  and    val: "\<lbrace>G\<rbrace> m \<lbrace>Q\<rbrace>"
  and     ef: "empty_fail m"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf G {s'. \<forall>rv s. (s, s') \<in> sr \<and> Q rv s \<longrightarrow> s' \<in> Q' rv} hs (m >>= (\<lambda>rv. f rv)) c" apply (rule ccorresI') apply (frule not_snd_bindI1) apply (erule empty_fail_not_snd [OF _ ef, THEN exE]) apply (case_tac x) apply simp apply (frule (1) use_valid [OF _  val]) apply (frule use_valid [OF _ pres]) apply (rule refl) apply simp apply (rule ccorresE [OF cc], assumption+) apply fastforce apply (erule (1) not_snd_bindI2) apply assumption apply (clarsimp simp: bind_def split: prod.splits) apply (erule (1) my_BallE) apply (erule bexI [rotated]) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G {s'. \<forall>rv s. (s, s') \<in> sr \<and> Q rv s \<longrightarrow> s' \<in> Q' rv} hs (m >>= f) c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> Q rv s \<longrightarrow> s' \<in> Q' rv}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((m >>= 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>(s, s') \<in> sr; G s; s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> Q rv s \<longrightarrow> s' \<in> Q' rv}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) s); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((m >>= 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 x. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> Q rv s \<longrightarrow> s' \<in> Q' rv}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) s); x \<in> fst (m s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((m >>= 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 x a b. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> Q rv s \<longrightarrow> s' \<in> Q' rv}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) s); x \<in> fst (m s); x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst ((m >>= 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 x a b. \<lbrakk>(s, s') \<in> sr; G s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) s); (a, b) \<in> fst (m s); x = (a, b)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((m >>= 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 x a b. \<lbrakk>(s, s') \<in> sr; G s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) s); (a, b) \<in> fst (m s); x = (a, b); Q a b\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((m >>= 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 (2 subgoals):
 1. \<And>s s' n z x a b. \<lbrakk>(s, s') \<in> sr; G s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) s); (a, b) \<in> fst (m s); x = (a, b); Q a b\<rbrakk> \<Longrightarrow> ?sa12 s s' n z x a b = s
 2. \<And>s s' n z x a b. \<lbrakk>(s, s') \<in> sr; G s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) s); (a, b) \<in> fst (m s); x = (a, b); Q a b; ?sa12 s s' n z x a b = b\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((m >>= 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 x a b. \<lbrakk>(s, s') \<in> sr; G s; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) s); (a, b) \<in> fst (m s); x = (a, b); Q a b; s = b\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((m >>= 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 x a b. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((m >>= f) b). 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 (4 subgoals):
 1. \<And>s s' n z x a b. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b\<rbrakk> \<Longrightarrow> s' \<in> Q' a
 2. \<And>s s' n z x a b. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b\<rbrakk> \<Longrightarrow> \<not> snd (f a b)
 3. \<And>s s' n z x a b. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n16 s s' n z x a b, ?x16 s s' n z x a b)
 4. \<And>s s' n z x a b t' ra t. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b; ?x16 s s' n z x a b = Normal t'; (ra, t) \<in> fst (f a b); (t, t') \<in> sr; unif_rrel (?n16 s s' n z x a b = length hs) r xf arrel axf ra t'; ?n16 s s' n z x a b \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((m >>= f) b). 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 (3 subgoals):
 1. \<And>s s' n z x a b. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b\<rbrakk> \<Longrightarrow> \<not> snd (f a b)
 2. \<And>s s' n z x a b. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n16 s s' n z x a b, ?x16 s s' n z x a b)
 3. \<And>s s' n z x a b t' ra t. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b; ?x16 s s' n z x a b = Normal t'; (ra, t) \<in> fst (f a b); (t, t') \<in> sr; unif_rrel (?n16 s s' n z x a b = length hs) r xf arrel axf ra t'; ?n16 s s' n z x a b \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((m >>= f) b). 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 (2 subgoals):
 1. \<And>s s' n z x a b. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n16 s s' n z x a b, ?x16 s s' n z x a b)
 2. \<And>s s' n z x a b t' ra t. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b; ?x16 s s' n z x a b = Normal t'; (ra, t) \<in> fst (f a b); (t, t') \<in> sr; unif_rrel (?n16 s s' n z x a b = length hs) r xf arrel axf ra t'; ?n16 s s' n z x a b \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((m >>= f) b). 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 x a b t' ra t. \<lbrakk>(b, s') \<in> sr; G b; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((m >>= f) b); (a, b) \<in> fst (m b); x = (a, b); Q a b; s = b; z = Normal t'; (ra, t) \<in> fst (f a b); (t, 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>x\<in>fst ((m >>= f) b). 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' n aa ba t' ra t. \<lbrakk>(aa, ba) \<in> fst (m ba); Q aa ba; (ra, t) \<in> fst (f aa ba); (t, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'; n \<le> length hs; (ba, s') \<in> sr; G ba; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<forall>x\<in>fst (m ba). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> \<not> snd (f x1 x2); \<not> snd (m ba)\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (m ba). \<forall>x1 x2. y = (x1, x2) \<longrightarrow> (\<exists>x\<in>fst (f x1 x2). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> (x2, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf x1 t') proof (prove)
goal (1 subgoal):
 1. \<And>s' n aa ba t' ra t. \<lbrakk>(aa, ba) \<in> fst (m ba); Q aa ba; (ra, t) \<in> fst (f aa ba); (t, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'; n \<le> length hs; (ba, s') \<in> sr; G ba; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (m ba); \<forall>x1 x2. (aa, ba) = (x1, x2) \<longrightarrow> \<not> snd (f x1 x2)\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (m ba). \<forall>x1 x2. y = (x1, x2) \<longrightarrow> (\<exists>x\<in>fst (f x1 x2). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> (x2, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf x1 t') proof (prove)
goal (1 subgoal):
 1. \<And>s' n aa ba t' ra t. \<lbrakk>Q aa ba; (ra, t) \<in> fst (f aa ba); (t, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'; n \<le> length hs; (ba, s') \<in> sr; G ba; \<forall>rv. (\<exists>s. (s, s') \<in> sr \<and> Q rv s) \<longrightarrow> s' \<in> Q' rv; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (m ba); \<forall>x1 x2. (aa, ba) = (x1, x2) \<longrightarrow> \<not> snd (f x1 x2)\<rbrakk> \<Longrightarrow> \<forall>x1 x2. (aa, ba) = (x1, x2) \<longrightarrow> (\<exists>x\<in>fst (f x1 x2). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> (x2, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf x1 t') proof (prove)
goal:
No subgoals!