theory AutoCorres_C

lemma ccorres_to_corres_no_termination:
  assumes rf_sr_def: "rf_sr \<equiv> {(s,s'). cstate_relation s (globals s')}"
  assumes ac_def: "ac_f \<equiv> AC_call_L1 G globals ret_xf (L1_call_simpl False \<Gamma> f_'proc)"
  assumes ccorres: "ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)"
  assumes pre: "\<And>s'. G s' \<Longrightarrow> ccorres_to_corres_pre Q \<top> Q' s'"
  assumes ret: "\<And>r s'. R r (ret_xf s') \<longleftrightarrow> R' r (ret_xf' s')"
  shows "corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f ac_f" using ccorres ret pre unfolding ac_def ccorres_to_corres_pre_def rf_sr_def apply (clarsimp simp: ac_def corres_underlying_def ccorres_underlying_def) apply (rule conjI) apply (fastforce simp: unif_rrel_def intro: EHOther dest: in_AC_call_simpl) apply (clarsimp simp: AC_call_L1_def L2_call_L1_def L1_call_simpl_def) apply (clarsimp simp: select_f_def select_def snd_bind snd_assert get_def
                 split: sum.splits prod.splits) apply (monad_eq split: xstate.splits sum.splits) apply (drule EHOther, fastforce) apply blast apply (drule EHOther, fastforce) apply blast apply (monad_eq split: xstate.splits) apply (fastforce dest: EHAbrupt[OF _ EHEmpty]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f ac_f proof (prove)
using this:
ccorresG rf_sr \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)
R ?r (ret_xf ?s') = R' ?r (ret_xf' ?s')
G ?s' \<Longrightarrow> ccorres_to_corres_pre Q (\<lambda>_. True) Q' ?s'

goal (1 subgoal):
 1. corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f ac_f proof (prove)
using this:
ccorresG {(s, s'). cstate_relation s (globals s')} \<Gamma> R' ret_xf' P Q' [] dspec_f (Call f_'proc)
R ?r (ret_xf ?s') = R' ?r (ret_xf' ?s')
G ?s' \<Longrightarrow> Q (globals ?s') \<longrightarrow> True \<and> ?s' \<in> Q'

goal (1 subgoal):
 1. corres_underlying {(s, s'). cstate_relation s s'} True True R P Q dspec_f (AC_call_L1 G globals ret_xf (L1_call_simpl False \<Gamma> f_'proc)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a b; P a; Q b; \<not> snd (dspec_f a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (AC_call_L1 G globals ret_xf (L1_call_simpl False \<Gamma> f_'proc) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (dspec_f a). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r') \<and> \<not> snd (AC_call_L1 G globals ret_xf (L1_call_simpl False \<Gamma> f_'proc) b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a b; P a; Q b; \<not> snd (dspec_f a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (AC_call_L1 G globals ret_xf (L1_call_simpl False \<Gamma> f_'proc) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (dspec_f a). case x of (r, t) \<Rightarrow> cstate_relation t t' \<and> R r r'
 2. \<And>a b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a b; P a; Q b; \<not> snd (dspec_f a)\<rbrakk> \<Longrightarrow> \<not> snd (AC_call_L1 G globals ret_xf (L1_call_simpl False \<Gamma> f_'proc) b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a b; P a; Q b; \<not> snd (dspec_f a)\<rbrakk> \<Longrightarrow> \<not> snd (AC_call_L1 G globals ret_xf (L1_call_simpl False \<Gamma> f_'proc) b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a b; P a; Q b; \<not> snd (dspec_f a); snd ((do cur_gs <- get;
s <- select {s. globals s = cur_gs \<and> G s};
(rv, s') <- select_f ((do s <- get;
select (Collect (exec \<Gamma> (Call f_'proc) (Normal s))) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) s);
y <- put (globals s');
case rv of Inl x \<Rightarrow> fail | Inr x \<Rightarrow> return (Inr (ret_xf s'))
od) b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a x xa. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> xa; snd ((case xa of Normal s \<Rightarrow> liftE (put s) | Abrupt s \<Rightarrow> put s >>= throwError | _ \<Rightarrow> fail) x)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a x x3. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Fault x3\<rbrakk> \<Longrightarrow> False
 2. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a x x3. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; \<Gamma>\<turnstile>\<^sub>h \<langle>Call f_'proc # ?hs197 a x x3,x\<rangle> \<Rightarrow> (length (?hs197 a x x3), Fault x3)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False
 3. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Stuck\<rbrakk> \<Longrightarrow> False
 2. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a x. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; \<Gamma>\<turnstile>\<^sub>h \<langle>Call f_'proc # ?hs248 a x,x\<rangle> \<Rightarrow> (length (?hs248 a x), Stuck)\<rbrakk> \<Longrightarrow> False
 2. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a x aa b. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (dspec_f a). (t, s'') \<in> {(s, s'). cstate_relation s (globals s')} \<and> unif_rrel (n = length []) R' ret_xf' R' ret_xf' r s'' | _ \<Rightarrow> False)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; (aa, b) \<in> fst ((do s <- \<lambda>s. ({(s, s)}, False);
(\<lambda>sa. (Collect (exec \<Gamma> (Call f_'proc) (Normal s)) \<times> {sa}, False)) >>= case_xstate (\<lambda>s. liftE (put s)) (\<lambda>s. put s >>= throwError) (\<lambda>ft. fail) fail
od) x); \<forall>x1 x2. (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inr () \<or> snd (put (globals x2) (globals x)) \<or> (\<exists>b. ((), b) \<in> fst (put (globals x2) (globals x)))) \<and> (aa = x1 \<and> b = x2 \<longrightarrow> x1 = Inl () \<or> snd (put (globals x2) (globals x)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a x x2. \<lbrakk>\<forall>a b. cstate_relation a (globals b) \<longrightarrow> P a \<and> b \<in> Q' \<and> \<not> snd (dspec_f a) \<longrightarrow> (\<forall>n t. (\<Gamma>\<turnstile>\<^sub>h \<langle>[Call f_'proc],b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> (\<exists>aa b. cstate_relation b (globals x1) \<and> (aa, b) \<in> fst (dspec_f a) \<and> unif_rrel (n = 0) R' ret_xf' R' ret_xf' aa x1))) \<and> ((\<forall>x2. t \<noteq> Abrupt x2) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> ((\<forall>x3. t \<noteq> Fault x3) \<or> (b, [Call f_'proc], n, t) \<notin> exec_handlers \<Gamma>) \<and> (t = Stuck \<longrightarrow> (b, [Call f_'proc], n, Stuck) \<notin> exec_handlers \<Gamma>)); \<And>r s'. R r (ret_xf s') = R' r (ret_xf' s'); \<And>s'. G s' \<Longrightarrow> Q (globals s') \<longrightarrow> s' \<in> Q'; cstate_relation a (globals x); P a; Q (globals x); \<not> snd (dspec_f a); G x; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Abrupt x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!