kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_UL_C

lemma exec_handlers_assoc:
  "E \<turnstile>\<^sub>h \<langle>(c1;; (c2 ;; c3)) # hs, s\<rangle> \<Rightarrow> (n, t) = E \<turnstile>\<^sub>h \<langle>(c1;;c2;;c3) # hs,s\<rangle> \<Rightarrow> (n, t)" apply (rule exec_handlers_semantic_equiv) apply (rule semantic_equivI) apply (rule exec_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. E\<turnstile>\<^sub>h \<langle>(c1;;
(c2;;
c3)) # hs,s\<rangle> \<Rightarrow> (n, t) = E\<turnstile>\<^sub>h \<langle>(c1;;
c2;;
c3) # hs,s\<rangle> \<Rightarrow> (n, t) proof (prove)
goal (1 subgoal):
 1. \<And>s'. semantic_equiv E s s' (c1;;
(c2;;
c3)) (c1;;
c2;;
c3) proof (prove)
goal (1 subgoal):
 1. \<And>s'. E\<turnstile> \<langle>c1;;
(c2;;
c3),Normal s\<rangle> \<Rightarrow> s' = E\<turnstile> \<langle>c1;;
c2;;
c3,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_rhs_assoc:
  assumes cc: "ccorres_underlying sr E r xf arrel axf G G' hs a (c ;; (d ;; e))"
  shows "ccorres_underlying sr E r xf arrel axf G G' hs a (c ;; d ;; e)" using cc apply (rule ccorres_semantic_equivD1) apply (rule semantic_equivI) apply (rule exec_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr E r xf arrel axf G G' hs a (c;;
d;;
e) proof (prove)
using this:
ccorres_underlying sr E r xf arrel axf G G' hs a (c;;
(d;;
e))

goal (1 subgoal):
 1. ccorres_underlying sr E r xf arrel axf G G' hs a (c;;
d;;
e) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv E s s' (c;;
(d;;
e)) (c;;
d;;
e) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> E\<turnstile> \<langle>c;;
(d;;
e),Normal s\<rangle> \<Rightarrow> s' = E\<turnstile> \<langle>c;;
d;;
e,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_rhs_assoc2:
  "ccorres_underlying sr E r xf arrel axf G G' hs a ((c ;; c') ;; c'')
  \<Longrightarrow> ccorres_underlying sr E r xf arrel axf G G' hs a (c ;; (c' ;; c''))" apply (erule iffD2 [OF ccorres_semantic_equiv, rotated]) apply (rule semantic_equivI) apply (rule exec_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr E r xf arrel axf G G' hs a (c;;
c';;
c'') \<Longrightarrow> ccorres_underlying sr E r xf arrel axf G G' hs a (c;;
(c';;
c'')) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv E s s' (c;;
(c';;
c'')) (c;;
c';;
c'') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> E\<turnstile> \<langle>c;;
(c';;
c''),Normal s\<rangle> \<Rightarrow> s' = E\<turnstile> \<langle>c;;
c';;
c'',Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_rel_imp:
  assumes x: "ccorres_underlying sr \<Gamma> r' xf' r' xf' P P' hs f g"
  assumes y: "\<And>x y. r' x (xf' y) \<Longrightarrow> r x (xf y)"
  shows      "ccorres_underlying sr \<Gamma> r xf r xf P P' hs f g" using x apply - apply (rule ccorresI') apply (erule (5) ccorresE) apply clarsimp apply (erule bexI [rotated]) apply (simp add: y unif_rrel_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG sr \<Gamma> r xf P P' hs f g proof (prove)
using this:
ccorresG sr \<Gamma> r' xf' P P' hs f g

goal (1 subgoal):
 1. ccorresG sr \<Gamma> r xf P P' hs f g proof (prove)
goal (1 subgoal):
 1. ccorresG sr \<Gamma> r' xf' P P' hs f g \<Longrightarrow> ccorresG sr \<Gamma> r xf P P' hs f g proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorresG sr \<Gamma> r' xf' P P' hs f g; (s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (f s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); z = Normal t'; (ra, t) \<in> fst (f s); (t, t') \<in> sr; unif_rrel (n = length hs) r' xf' r' xf' ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (f s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n t' ra t. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (f s); (ra, t) \<in> fst (f s); (t, t') \<in> sr; unif_rrel (n = length hs) r' xf' r' xf' ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' n t' ra t. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (f s); (t, t') \<in> sr; unif_rrel (n = length hs) r' xf' r' xf' ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> case (ra, t) of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf r xf ra t' proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_cond_empty:
  assumes c2: "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a c'"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a (Cond {} c c')" apply (rule ccorres_guard_imp) apply (rule ccorres_cond_weak [OF _ c2]) apply (rule ccorres_empty) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a (Cond {} c c') proof (prove)
goal (3 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs a (Cond {} c c')
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> P' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Pt4 ?Rt4 hs a c
 2. \<And>s. P s \<Longrightarrow> (?Pt4 and P) s
 3. \<And>s. s \<in> P' \<Longrightarrow> s \<in> ?Rt4 \<inter> {} \<union> P' \<inter> - {} proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> (?Pt4 and P) s
 2. \<And>s. s \<in> P' \<Longrightarrow> s \<in> {} \<inter> {} \<union> P' \<inter> - {} proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> P' \<Longrightarrow> s \<in> {} \<inter> {} \<union> P' \<inter> - {} proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_cond_univ:
  assumes c1: "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a c"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a (Cond UNIV c c')" apply (rule ccorres_guard_imp) apply (rule ccorres_cond_weak [OF c1]) apply (rule ccorres_empty) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a (Cond UNIV c c') proof (prove)
goal (3 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs a (Cond UNIV c c')
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> P' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Pf4 ?Rf4 hs a c'
 2. \<And>s. P s \<Longrightarrow> (P and ?Pf4) s
 3. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' \<inter> UNIV \<union> ?Rf4 \<inter> - UNIV proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> (P and ?Pf4) s
 2. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' \<inter> UNIV \<union> {} \<inter> - UNIV proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> P' \<Longrightarrow> s \<in> P' \<inter> UNIV \<union> {} \<inter> - UNIV proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_Guard_Seq:
  assumes cc: "ccorres_underlying sr \<Gamma> r xf arrel axf A C' hs a (c ;; d)"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf A (C' \<inter> S) hs a (Guard F S c ;; d)" apply (rule ccorres_semantic_equivD2 [OF _ Guard_Seq_semantic_equiv]) apply (rule ccorres_Guard [OF cc]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf A (C' \<inter> S) hs a (Guard F S c;;
d) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf A (C' \<inter> S) hs a (Guard F S (c;;
d)) proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_symb_exec_l':
  assumes cc: "\<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) G' hs (f rv) c"
  and     v1: "\<And>s. valid ((=) s) m (\<lambda>r. (=) s)"
  and     v2: "valid G m Q"
  and     ef: "empty_fail m"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs (m >>= (\<lambda>rv. f rv)) c" apply (rule ccorres_guard_imp) apply (rule ccorres_symb_exec_l [OF cc v1 v2 ef]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs (m >>= f) c proof (prove)
goal (3 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs (m >>= f) c
 2. \<And>s. G s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> G' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (2 subgoals):
 1. \<And>s. G s \<Longrightarrow> G s
 2. \<And>s. s \<in> G' \<Longrightarrow> s \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> Q rv s \<longrightarrow> s' \<in> G'} proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_gen_asm:
  assumes rl: "P \<Longrightarrow> ccorres_underlying \<Gamma> sr r xf arrel axf G G' hs a c"
  shows   "ccorres_underlying \<Gamma> sr r xf arrel axf (G and (\<lambda>_. P)) G' hs a c" apply (rule ccorres_req) prefer 2 apply (rule ccorres_guard_imp) apply (erule rl) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying \<Gamma> sr r xf arrel axf (G and (\<lambda>_. P)) G' hs a c proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> \<Gamma>; (G and (\<lambda>_. P)) s; s' \<in> G'\<rbrakk> \<Longrightarrow> ?F
 2. ?F \<Longrightarrow> ccorres_underlying \<Gamma> sr r xf arrel axf (G and (\<lambda>_. P)) G' hs a c proof (prove)
goal (2 subgoals):
 1. ?F \<Longrightarrow> ccorres_underlying \<Gamma> sr r xf arrel axf (G and (\<lambda>_. P)) G' hs a c
 2. \<And>s s'. \<lbrakk>(s, s') \<in> \<Gamma>; (G and (\<lambda>_. P)) s; s' \<in> G'\<rbrakk> \<Longrightarrow> ?F proof (prove)
goal (4 subgoals):
 1. ?F \<Longrightarrow> ccorres_underlying \<Gamma> sr r xf arrel axf ?Q3 ?Q'3 hs a c
 2. \<And>s. \<lbrakk>?F; (G and (\<lambda>_. P)) s\<rbrakk> \<Longrightarrow> ?Q3 s
 3. \<And>s. \<lbrakk>?F; s \<in> G'\<rbrakk> \<Longrightarrow> s \<in> ?Q'3
 4. \<And>s s'. \<lbrakk>(s, s') \<in> \<Gamma>; (G and (\<lambda>_. P)) s; s' \<in> G'\<rbrakk> \<Longrightarrow> ?F proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>P; (G and (\<lambda>_. P)) s\<rbrakk> \<Longrightarrow> G s
 2. \<And>s. \<lbrakk>P; s \<in> G'\<rbrakk> \<Longrightarrow> s \<in> G'
 3. \<And>s s'. \<lbrakk>(s, s') \<in> \<Gamma>; (G and (\<lambda>_. P)) s; s' \<in> G'\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_gen_asm2:
  assumes rl: "P \<Longrightarrow> ccorres_underlying \<Gamma> sr r xf arrel axf G G' hs a c"
  shows   "ccorres_underlying \<Gamma> sr r xf arrel axf G (G' \<inter> {_. P}) hs a c" apply (rule ccorres_req) prefer 2 apply (rule ccorres_guard_imp) apply (erule rl) apply (simp split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying \<Gamma> sr r xf arrel axf G (G' \<inter> \<lbrace>P\<rbrace>) hs a c proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> \<Gamma>; G s; s' \<in> G' \<inter> \<lbrace>P\<rbrace>\<rbrakk> \<Longrightarrow> ?F
 2. ?F \<Longrightarrow> ccorres_underlying \<Gamma> sr r xf arrel axf G (G' \<inter> \<lbrace>P\<rbrace>) hs a c proof (prove)
goal (2 subgoals):
 1. ?F \<Longrightarrow> ccorres_underlying \<Gamma> sr r xf arrel axf G (G' \<inter> \<lbrace>P\<rbrace>) hs a c
 2. \<And>s s'. \<lbrakk>(s, s') \<in> \<Gamma>; G s; s' \<in> G' \<inter> \<lbrace>P\<rbrace>\<rbrakk> \<Longrightarrow> ?F proof (prove)
goal (4 subgoals):
 1. ?F \<Longrightarrow> ccorres_underlying \<Gamma> sr r xf arrel axf ?Q3 ?Q'3 hs a c
 2. \<And>s. \<lbrakk>?F; G s\<rbrakk> \<Longrightarrow> ?Q3 s
 3. \<And>s. \<lbrakk>?F; s \<in> G' \<inter> \<lbrace>P\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> ?Q'3
 4. \<And>s s'. \<lbrakk>(s, s') \<in> \<Gamma>; G s; s' \<in> G' \<inter> \<lbrace>P\<rbrace>\<rbrakk> \<Longrightarrow> ?F proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>P; G s\<rbrakk> \<Longrightarrow> G s
 2. \<And>s. \<lbrakk>P; s \<in> G' \<inter> \<lbrace>P\<rbrace>\<rbrakk> \<Longrightarrow> s \<in> G'
 3. \<And>s s'. \<lbrakk>(s, s') \<in> \<Gamma>; G s; s' \<in> G' \<inter> \<lbrace>P\<rbrace>\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_guard_imp2:
  assumes cc: "ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g"
  and     rl: "\<And>s s'. \<lbrakk> (s, s') \<in> sr; A s; s' \<in> A' \<rbrakk> \<Longrightarrow> Q s \<and> s' \<in> Q'"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf A A' hs f g" using cc apply - apply (rule ccorresI') apply (frule (2) rl) apply (erule conjE) apply (erule (5) ccorresE) apply (fastforce elim: bexI [rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf A A' hs f g proof (prove)
using this:
ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf A A' hs f g proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A A' hs f g proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g; (s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (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>ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g; (s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); Q s \<and> s' \<in> Q'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (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>ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g; (s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); Q s; s' \<in> Q'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (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 t' ra t. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); Q s; s' \<in> Q'; z = Normal t'; (ra, t) \<in> fst (f s); (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>(ra, t)\<in>fst (f s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma ccorres_move_Guard:
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> P s \<and> P' s' \<longrightarrow> G' s'"
  and      cc: "ccorres_underlying sr \<Gamma> r xf arrel axf A C' hs a c"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf (A and P) (C' \<inter> Collect P') hs a (Guard F (Collect G') c)" apply (rule ccorres_guard_imp2) apply (rule ccorres_Guard [OF cc]) apply simp apply (rule abs [rule_format]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (A and P) (C' \<inter> Collect P') hs a (Guard F (Collect G') c) proof (prove)
goal (2 subgoals):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf ?Q ?Q' hs a (Guard F (Collect G') c)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> sr; (A and P) s; s' \<in> C' \<inter> Collect P'\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; (A and P) s; s' \<in> C' \<inter> Collect P'\<rbrakk> \<Longrightarrow> A s \<and> s' \<in> C' \<inter> Collect G' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; A s \<and> P s; s' \<in> C' \<and> P' s'\<rbrakk> \<Longrightarrow> G' s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; A s \<and> P s; s' \<in> C' \<and> P' s'\<rbrakk> \<Longrightarrow> (?s4 s s', s') \<in> sr \<and> P (?s4 s s') \<and> P' s' proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma exec_handlers_Hoare_UNIV:
  "guard_is_UNIV r xf Q \<Longrightarrow>
   exec_handlers_Hoare \<Gamma> UNIV cs (ccHoarePost r xf Q) UNIV" by (clarsimp simp: exec_handlers_Hoare_def ccHoarePost_def
                     guard_is_UNIV_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. guard_is_UNIV r xf Q \<Longrightarrow> exec_handlers_Hoare \<Gamma> UNIV cs (ccHoarePost r xf Q) UNIV
theory Corres_UL_C

lemma ccorres_split_nothrow_novcg:
  fixes R' :: "'a set"
  assumes ac: "ccorres_underlying sr \<Gamma> r' xf' r' xf' P P' [] a c"
  and   ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  and     bd: "\<And>rv rv'. r' rv rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv')"
  and  valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>"
  and  novcg: "guard_is_UNIV r' xf' Q'"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>= (\<lambda>rv. b rv)) (c ;; d)" apply (rule ccorres_master_split_nohs_UNIV) apply (rule ac) apply (rule ccorres_abstract[OF ceqv]) apply (rule ccorres_gen_asm2) apply (erule bd) apply (simp add: valid) apply (cut_tac novcg, simp add: guard_is_UNIV_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) P' hs (a >>= b) (c;;
d) proof (prove)
goal (4 subgoals):
 1. ccorres_underlying sr \<Gamma> ?r' ?xf' ?arrel' ?axf' P P' [] a c
 2. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?R' rv) hs (b rv) d
 3. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 4. guard_is_UNIV ?r' ?xf' (\<lambda>a b. ?R' a) proof (prove)
goal (3 subgoals):
 1. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?R' rv) hs (b rv) d
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. guard_is_UNIV r' xf' (\<lambda>a b. ?R' a) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?G'5 rv rv') hs (b rv) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. guard_is_UNIV r' xf' (\<lambda>a b. {s. s \<in> ?G'5 a (xf' s)}) proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. ?P8 rv rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (?R rv) (?G'8 rv rv') hs (b rv) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>?R\<rbrace>
 3. guard_is_UNIV r' xf' (\<lambda>a b. {s. s \<in> ?G'8 a (xf' s) \<inter> \<lbrace>?P8 a (xf' s)\<rbrace>}) proof (prove)
goal (2 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>
 2. guard_is_UNIV r' xf' (\<lambda>a b. {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>}) proof (prove)
goal (1 subgoal):
 1. guard_is_UNIV r' xf' (\<lambda>a b. {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>r' a (xf' s)\<rbrace>}) proof (prove)
goal:
No subgoals!
theory Corres_UL_C

lemma inl_inr_rrel_simps[simp]:
  "inl_rrel rrel' (Inl e) = rrel' (Inl e)"
  "inr_rrel rrel (Inr rv) = rrel rv"
  "inl_rrel rrel' (Inr rv) = \<bottom>"
  "inr_rrel rrel (Inl rv) = \<bottom>" by (simp add: inl_rrel_def inr_rrel_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (inl_rrel rrel' (Inl e) = rrel' (Inl e) &&& inr_rrel rrel (Inr rv) = rrel rv) &&& inl_rrel rrel' (Inr rv) = (\<lambda>_. False) &&& inr_rrel rrel (Inl rv) = (\<lambda>_. False)
theory Corres_UL_C

lemma inl_inrE:
  "\<lbrakk> inl_rrel rrel' v ex; \<And>e. \<lbrakk> v = Inl e; rrel' (Inl e) ex \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
  "\<lbrakk> inr_rrel rrel v rv; \<And>r. \<lbrakk> v = Inr r; rrel r rv \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by (simp add: inl_rrel_def inr_rrel_def split: sum.split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>inl_rrel rrel' v ex; \<And>e. \<lbrakk>v = Inl e; rrel' (Inl e) ex\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R) &&& (\<lbrakk>inr_rrel rrel v rv; \<And>r. \<lbrakk>v = Inr r; rrel r rv\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R)
theory Corres_UL_C

lemma ccorres_symb_exec_r_known_rv:
  "\<lbrakk>  \<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. xf' s = val});
        \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv');
        ccorres_underlying sr \<Gamma> r xf arrel axf P Q hs a (y' val);
        \<Gamma> \<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. (xf' s) = val \<longrightarrow> s \<in> Q} \<rbrakk>
       \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs a (c;;y)" by (rule_tac F="\<lambda>rv'. rv' = val" and xf'=xf'
          in ccorres_symb_exec_r_rv_abstract,
       simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) c ({s'. (s, s') \<in> sr} \<inter> {s. xf' s = val}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); ccorres_underlying sr \<Gamma> r xf arrel axf P Q hs a (y' val); \<Gamma>\<turnstile>\<^bsub>/Ft\<^esub> P' c {s. \<forall>rv. xf' s = val \<longrightarrow> s \<in> Q}\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs a (c;;
y)
theory Corres_UL_C

lemma ccorres_symb_exec_r_known_rv_UNIV:
  "\<lbrakk>  \<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. xf' s = val});
        \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv');
        ccorres_underlying sr \<Gamma> r xf arrel axf P Q hs a (y' val); guard_is_UNIV (\<lambda>rv rv'. rv' = val) xf' (\<lambda>rv rv'. Q) \<rbrakk>
       \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) R' hs a (m;;y)" by (rule_tac F="\<lambda>rv'. rv' = val" and xf'=xf'
          in ccorres_symb_exec_r_abstract_UNIV,
       simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<Gamma>\<turnstile> (R' \<inter> {s'. R s \<and> (s, s') \<in> sr}) m ({s'. (s, s') \<in> sr} \<inter> {s. xf' s = val}); \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' y (y' rv'); ccorres_underlying sr \<Gamma> r xf arrel axf P Q hs a (y' val); guard_is_UNIV (\<lambda>rv rv'. rv' = val) xf' (\<lambda>rv rv'. Q)\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) R' hs a (m;;
y)