theory AutoCorresModifiesProofs

lemma autocorres_modifies_transfer:
  notes hoare_seq_ext[wp]
  fixes \<Gamma> globals f' f_'proc modifies_eqn P xf
  assumes f'_def: "f' \<equiv> AC_call_L1 P globals xf (L1_call_simpl check_termination \<Gamma> f_'proc)"
  assumes f_modifies: "\<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call f_'proc {t. modifies_eqn (globals t) (globals \<sigma>)}"
  shows "\<lbrace> \<lambda>s. s = \<sigma> \<rbrace> f' \<lbrace> \<lambda>_ s. modifies_eqn s \<sigma> \<rbrace>" apply (clarsimp simp: f'_def AC_call_L1_def L2_call_L1_def L1_call_simpl_def) apply (simp add: liftM_def bind_assoc) apply wpsimp apply (clarsimp simp: in_monad select_def split: xstate.splits) by (case_tac xa; clarsimp dest!: exec_normal[OF singletonI _ f_modifies[rule_format]])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = \<sigma>\<rbrace> f' \<lbrace>\<lambda>_ s. modifies_eqn s \<sigma>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = \<sigma>\<rbrace> liftM (\<lambda>rv. case rv of Inr v \<Rightarrow> v) (do cur_gs <- get;
s <- select {s. globals s = cur_gs \<and> P s};
(rv, s') <- select_f ((do s <- get;
y <- assert (check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
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 (xf s'))
od) \<lbrace>\<lambda>_ s. modifies_eqn s \<sigma>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = \<sigma>\<rbrace> do x <- get;
x <- select {s. globals s = x \<and> P s};
x <- select_f ((do s <- get;
y <- assert (check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
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) x);
x <- case x of (rv, s') \<Rightarrow> do y <- put (globals s');
case rv of Inl x \<Rightarrow> fail | Inr x \<Rightarrow> return (Inr (xf s'))
od;
return (case x of Inr v \<Rightarrow> v)
od \<lbrace>\<lambda>_ s. modifies_eqn s \<sigma>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x b. \<lbrakk>(Inr (), b) \<in> fst ((do s <- get;
y <- assert (check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s);
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) x); P x; \<sigma> = globals x\<rbrakk> \<Longrightarrow> modifies_eqn (globals b) (globals x) proof (prove)
goal (1 subgoal):
 1. \<And>x b xa. \<lbrakk>P x; \<sigma> = globals x; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal x; \<forall>x1. xa = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal x\<rangle> \<Rightarrow> Normal x1 \<and> b = x1; \<forall>x2. xa \<noteq> Abrupt x2; \<forall>x3. xa \<noteq> Fault x3; xa \<noteq> Stuck\<rbrakk> \<Longrightarrow> modifies_eqn (globals b) (globals x)