theory CCorresLemmas

lemma ccorres_rel_imp_guard:
  fixes Q' :: "'a set"
  assumes x: "ccorres_underlying sr \<Gamma> r' xf' arrel axf P P' hs f g"
  and     y: "\<And>x s s'. \<lbrakk> (s, s') \<in> sr; R x s; s' \<in> R'; r' x (xf' s') \<rbrakk> \<Longrightarrow> r x (xf s')"
  and valid:  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>"
  and valid': "\<Gamma> \<turnstile> Q' g R', R'"
  and wfh:   "\<And>t t' n. \<Gamma>\<turnstile>\<^sub>h \<langle>hs,t\<rangle> \<Rightarrow> (n, Normal t') \<Longrightarrow> t = t'"
  shows      "ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs f g" using x apply - apply (rule ccorresI') apply clarsimp apply (erule (5) ccorresE) apply (frule (1) use_valid [OF _ valid]) apply simp apply (clarsimp elim!: bexI [rotated] simp: unif_rrel_def) apply (erule y, simp_all) apply (frule exec_handlers_Hoare_NormalD[rotated 2]) apply simp apply (rule exec_handlers_Hoare_from_vcg_might_fail[OF valid' order_refl]) apply assumption+ done

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

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs f g proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r' xf' arrel axf P P' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and Q) (P' \<inter> Q') hs f g proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr \<Gamma> r' xf' arrel axf P P' hs f g; (s, s') \<in> sr; (P and Q) s; s' \<in> P' \<inter> Q'; \<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 P P' hs f g; (s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (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 t' ra t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); P s; Q s; s' \<in> P'; 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>x\<in>fst (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 t' ra t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); P s; Q s; s' \<in> P'; 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; R ra t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (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 t' ra t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; 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; R ra t\<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 arrel axf ra t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' t' ra t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; (t, t') \<in> sr; r' ra (xf' t'); R ra t\<rbrakk> \<Longrightarrow> r ra (xf t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' t' r t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; r' r (xf' t'); R r t\<rbrakk> \<Longrightarrow> t' \<in> R' proof (prove)
goal (4 subgoals):
 1. \<And>s s' t' r t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; r' r (xf' t'); R r t\<rbrakk> \<Longrightarrow> length hs = length (g # hs) - 1
 2. \<And>s s' t' r t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; r' r (xf' t'); R r t\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> (?P29 s s' t' r t) (g # hs) (?Q29 s s' t' r t) (?A29 s s' t' r t)
 3. \<And>s s' t' r t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; r' r (xf' t'); R r t\<rbrakk> \<Longrightarrow> s' \<in> ?P29 s s' t' r t
 4. \<And>s s' t' r t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; r' r (xf' t'); R r t; t' \<in> ?Q29 s s' t' r t\<rbrakk> \<Longrightarrow> t' \<in> R' proof (prove)
goal (3 subgoals):
 1. \<And>s s' t' r t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; r' r (xf' t'); R r t\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> (?P29 s s' t' r t) (g # hs) (?Q29 s s' t' r t) (?A29 s s' t' r t)
 2. \<And>s s' t' r t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; r' r (xf' t'); R r t\<rbrakk> \<Longrightarrow> s' \<in> ?P29 s s' t' r t
 3. \<And>s s' t' r t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; r' r (xf' t'); R r t; t' \<in> ?Q29 s s' t' r t\<rbrakk> \<Longrightarrow> t' \<in> R' proof (prove)
goal (2 subgoals):
 1. \<And>s s' t' r t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; r' r (xf' t'); R r t\<rbrakk> \<Longrightarrow> s' \<in> Q'
 2. \<And>s s' t' r t. \<lbrakk>(s, s') \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (length hs, Normal t'); \<not> snd (f s); P s; Q s; s' \<in> P'; s' \<in> Q'; r' r (xf' t'); R r t; t' \<in> R'\<rbrakk> \<Longrightarrow> t' \<in> R' proof (prove)
goal:
No subgoals!