theory Corres_UL_C

lemma ccorres_symb_exec_l2:
  assumes cc: "\<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv) hs (f rv) c"
  and     v1: "\<And>s. G s \<Longrightarrow> exs_valid ((=) s) m (\<lambda>r. (=) s)"
  and     v2: "valid G m Q"
  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 use_exs_valid [OF v1]) apply (rule refl) apply clarsimp apply (frule (1) use_valid [OF _ v2]) apply (drule (1) not_snd_bindD) apply (rule ccorresE [OF cc]) apply assumption apply assumption apply (drule spec, erule mp) apply fastforce apply simp apply assumption apply (fastforce simp: in_monad') 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 (2 subgoals):
 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> s = ?s2 s s' n z
 2. \<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); \<exists>(r, s')\<in>fst (m (?s2 s s' n z)). s = 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); \<exists>(r, s')\<in>fst (m s). s = 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' n z 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)\<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 z 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); Q a 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 (1 subgoal):
 1. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a 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 (6 subgoals):
 1. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> (?s14 s' n z a b, ?s'14 s' n z a b) \<in> sr
 2. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> Q (?rv15 s' n z a b) (?s14 s' n z a b)
 3. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> ?s'14 s' n z a b \<in> Q' (?rv15 s' n z a b)
 4. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<not> snd (f (?rv15 s' n z a b) (?s14 s' n z a b))
 5. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,?s'14 s' n z a b\<rangle> \<Rightarrow> (?n14 s' n z a b, ?x14 s' n z a b)
 6. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b); ?x14 s' n z a b = Normal t'; (ra, t) \<in> fst (f (?rv15 s' n z a b) (?s14 s' n z a b)); (t, t') \<in> sr; unif_rrel (?n14 s' n z a b = length hs) r xf arrel axf ra t'; ?n14 s' n z 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 (5 subgoals):
 1. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> Q (?rv15 s' n z a b) b
 2. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> s' \<in> Q' (?rv15 s' n z a b)
 3. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<not> snd (f (?rv15 s' n z a b) b)
 4. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n14 s' n z a b, ?x14 s' n z a b)
 5. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b); ?x14 s' n z a b = Normal t'; (ra, t) \<in> fst (f (?rv15 s' n z a b) b); (t, t') \<in> sr; unif_rrel (?n14 s' n z a b = length hs) r xf arrel axf ra t'; ?n14 s' n z 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 (4 subgoals):
 1. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> s' \<in> Q' a
 2. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<not> snd (f a b)
 3. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n14 s' n z a b, ?x14 s' n z a b)
 4. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b); ?x14 s' n z a b = Normal t'; (ra, t) \<in> fst (f a b); (t, t') \<in> sr; unif_rrel (?n14 s' n z a b = length hs) r xf arrel axf ra t'; ?n14 s' n z 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 (4 subgoals):
 1. \<And>s' n z a b. \<lbrakk>(b, s') \<in> sr; G b; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<exists>s. (s, s') \<in> sr \<and> Q a s
 2. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<not> snd (f a b)
 3. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n14 s' n z a b, ?x14 s' n z a b)
 4. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b); ?x14 s' n z a b = Normal t'; (ra, t) \<in> fst (f a b); (t, t') \<in> sr; unif_rrel (?n14 s' n z a b = length hs) r xf arrel axf ra t'; ?n14 s' n z 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' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<not> snd (f a b)
 2. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n14 s' n z a b, ?x14 s' n z a b)
 3. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b); ?x14 s' n z a b = Normal t'; (ra, t) \<in> fst (f a b); (t, t') \<in> sr; unif_rrel (?n14 s' n z a b = length hs) r xf arrel axf ra t'; ?n14 s' n z 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' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (?n14 s' n z a b, ?x14 s' n z a b)
 2. \<And>s' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a b); ?x14 s' n z a b = Normal t'; (ra, t) \<in> fst (f a b); (t, t') \<in> sr; unif_rrel (?n14 s' n z a b = length hs) r xf arrel axf ra t'; ?n14 s' n z 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' n z 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); (a, b) \<in> fst (m b); Q a b; \<not> snd (m b) \<and> \<not> snd (f a 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:
No subgoals!