theory CCorresLemmas

lemma ccorres_rel_imp2:
  "\<lbrakk> ccorres_underlying sr \<Gamma> r' xf' arrel' axf' P P' hs a b;
        \<And>rv s. \<lbrakk> r' rv (xf' s) \<rbrakk> \<Longrightarrow> r rv (xf s);
        \<And>rv s. \<lbrakk> arrel' rv (axf' s); hs \<noteq> [] \<rbrakk> \<Longrightarrow> arrel rv (axf s) \<rbrakk>
     \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a b" apply (rule ccorresI', erule(5) ccorresE) apply simp apply (erule rev_bexI) apply (simp add: unif_rrel_def split: if_split_asm) apply (cases "hs = []", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying sr \<Gamma> r' xf' arrel' axf' P P' hs a b; \<And>rv s. r' rv (xf' s) \<Longrightarrow> r rv (xf s); \<And>rv s. \<lbrakk>arrel' rv (axf' s); hs \<noteq> []\<rbrakk> \<Longrightarrow> arrel rv (axf s)\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a b proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' ra t. \<lbrakk>\<And>rv s. r' rv (xf' s) \<Longrightarrow> r rv (xf s); \<And>rv s. \<lbrakk>arrel' rv (axf' s); hs \<noteq> []\<rbrakk> \<Longrightarrow> arrel rv (axf s); (s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); z = Normal t'; (ra, t) \<in> fst (a 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 (a 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>\<And>rv s. r' rv (xf' s) \<Longrightarrow> r rv (xf s); \<And>rv s. \<lbrakk>arrel' rv (axf' s); hs \<noteq> []\<rbrakk> \<Longrightarrow> arrel rv (axf s); (s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s); z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (n = length hs) r' xf' arrel' axf' ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a 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>\<And>rv s. r' rv (xf' s) \<Longrightarrow> r rv (xf s); \<And>rv s. \<lbrakk>arrel' rv (axf' s); hs \<noteq> []\<rbrakk> \<Longrightarrow> arrel rv (axf s); (s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s); z = Normal t'; (t, t') \<in> sr; unif_rrel (n = length hs) r' xf' arrel' axf' 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 arrel axf ra t' proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' ra t. \<lbrakk>n \<le> length hs; \<And>rv s. r' rv (xf' s) \<Longrightarrow> r rv (xf s); \<And>rv s. \<lbrakk>arrel' rv (axf' s); hs \<noteq> []\<rbrakk> \<Longrightarrow> arrel rv (axf s); (s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>b # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s); z = Normal t'; (t, t') \<in> sr; n \<noteq> length hs; arrel' ra (axf' t')\<rbrakk> \<Longrightarrow> arrel ra (axf t') proof (prove)
goal:
No subgoals!