theory CCorresLemmas

lemma ccorres_guard_from_wp_bind:
  "\<lbrakk> \<lbrace>\<lambda>s. \<not> P s \<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; empty_fail a; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c \<rbrakk> \<Longrightarrow>
  ccorres_underlying sr Gamm rvr xf arrel axf (\<lambda>s. P s \<longrightarrow> G s) G' hs (a >>= b) c" apply (rule ccorresI') apply (simp add: empty_fail_def) apply (drule_tac x = s in spec) apply (case_tac "P s") apply simp apply (erule (5) ccorresE) apply fastforce apply (drule not_snd_bindI1) apply (clarsimp simp: not_empty_eq) apply (drule (2) use_valid) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; empty_fail a; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c\<rbrakk> \<Longrightarrow> ccorres_underlying sr Gamm rvr xf arrel axf (\<lambda>s. P s \<longrightarrow> G s) G' hs (a >>= b) c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; empty_fail a; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; P s \<longrightarrow> G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst ((a >>= b) s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; \<forall>s. fst (a s) = {} \<longrightarrow> snd (a s); ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; P s \<longrightarrow> G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; P s \<longrightarrow> G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s); fst (a s) = {} \<longrightarrow> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; P s \<longrightarrow> G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s); fst (a s) = {} \<longrightarrow> snd (a s); P s\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t')
 2. \<And>s s' n z. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; P s \<longrightarrow> G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s); fst (a s) = {} \<longrightarrow> snd (a s); \<not> P s\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s); fst (a s) = {} \<longrightarrow> snd (a s); P s\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t')
 2. \<And>s s' n z. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; P s \<longrightarrow> G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s); fst (a s) = {} \<longrightarrow> snd (a s); \<not> P s\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z t' r t. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; (s, s') \<in> sr; G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s); fst (a s) = {} \<longrightarrow> snd (a s); P s; z = Normal t'; (r, t) \<in> fst ((a >>= b) s); (t, t') \<in> sr; unif_rrel (n = length hs) rvr xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t')
 2. \<And>s s' n z. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; P s \<longrightarrow> G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s); fst (a s) = {} \<longrightarrow> snd (a s); \<not> P s\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; P s \<longrightarrow> G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd ((a >>= b) s); fst (a s) = {} \<longrightarrow> snd (a s); \<not> P s\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; P s \<longrightarrow> G s; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); fst (a s) = {} \<longrightarrow> snd (a s); \<not> P s; \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z aa ba. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> P s; \<not> snd (a s); (aa, ba) \<in> fst (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z aa ba. \<lbrakk>\<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>\<lambda>_ _. False\<rbrace>; ccorres_underlying sr Gamm rvr xf arrel axf G G' hs (a >>= b) c; (s, s') \<in> sr; s' \<in> G'; Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> P s; \<not> snd (a s); False\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst ((a >>= b) s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr xf arrel axf r t') proof (prove)
goal:
No subgoals!