theory AutoCorres_C

lemma autocorres_transfer_spec_no_modifies:
  assumes ac_def:
    "ac_f \<equiv> AC_call_L1 arg_rel globals ret_xf (L1_call_simpl check_termination \<Gamma> f_'proc)"
  assumes c_spec:
    "\<forall>s0. hoarep \<Gamma> {} {} (P' s0) (Call f_'proc) (Collect (Q s0)) A" \<comment> \<open>syntax parser barfs...\<close>
  assumes c_modifies:
    "\<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call f_'proc {t. t may_not_modify_globals \<sigma>}"
  assumes c_spec_unify:
    "\<And>s0. P' s0 = {s. s0 = s \<and> P s}"
  assumes precond_deps:
    "\<And>s0 s t. \<lbrakk> arg_rel s; arg_rel t; globals s = globals t \<rbrakk> \<Longrightarrow> P s = P t"
  assumes postcond_deps:
    "\<And>s0 s0' s t. \<lbrakk> arg_rel s0; arg_rel s0'; globals s0 = globals s0';
                    ret_xf s = ret_xf t; globals s = globals t \<rbrakk> \<Longrightarrow> Q s0 s = Q s0' t"
  shows "\<lbrace>\<lambda>s. s = globals cs \<and> P cs \<and> arg_rel cs \<rbrace>
           ac_f
         \<lbrace>\<lambda>r s'. s' = globals cs \<and> (\<exists>cs'. r = ret_xf cs' \<and> Q cs cs') \<rbrace>" apply (clarsimp simp: valid_def ac_def AC_call_L1_def L2_call_L1_def L1_call_simpl_def
                        in_monad' in_liftM select_f_def in_select in_fail
                  split: sum.splits xstate.splits) apply (rename_tac r', case_tac r'; clarsimp) apply (rename_tac xst, case_tac xst; clarsimp) apply (frule_tac ?s0.1=s in exec_normal[OF _ _ c_spec[rule_format], rotated]) apply (clarsimp simp: c_spec_unify) apply (blast dest: precond_deps) apply (frule exec_normal[OF singletonI _ c_modifies[rule_format]]) apply (clarsimp simp: meq_def) apply (blast dest: postcond_deps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s = globals cs \<and> P cs \<and> arg_rel cs\<rbrace> ac_f \<lbrace>\<lambda>r s'. s' = globals cs \<and> (\<exists>cs'. r = ret_xf cs' \<and> Q cs cs')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b r'. \<lbrakk>\<forall>x2. r' = Inr x2 \<longrightarrow> (\<exists>s. arg_rel s \<and> globals s = globals cs \<and> (check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s) \<and> (\<exists>ba. x2 = ret_xf ba \<and> (\<exists>x. (\<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> ba = x1) \<and> (\<forall>x2. x \<noteq> Abrupt x2) \<and> (\<forall>x3. x \<noteq> Fault x3) \<and> x \<noteq> Stuck) \<and> b = globals ba)) \<and> a = x2; P cs; arg_rel cs; r' \<noteq> Inl ()\<rbrakk> \<Longrightarrow> b = globals cs \<and> (\<exists>cs'. a = ret_xf cs' \<and> Q cs cs') proof (prove)
goal (1 subgoal):
 1. \<And>s ba x. \<lbrakk>P cs; arg_rel cs; arg_rel s; globals s = globals cs; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> ba = x1; \<forall>x2. x \<noteq> Abrupt x2; \<forall>x3. x \<noteq> Fault x3; x \<noteq> Stuck\<rbrakk> \<Longrightarrow> globals ba = globals cs \<and> (\<exists>cs'. ret_xf ba = ret_xf cs' \<and> Q cs cs') proof (prove)
goal (1 subgoal):
 1. \<And>s ba. \<lbrakk>P cs; arg_rel cs; arg_rel s; globals s = globals cs; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal ba\<rbrakk> \<Longrightarrow> globals ba = globals cs \<and> (\<exists>cs'. ret_xf ba = ret_xf cs' \<and> Q cs cs') proof (prove)
goal (2 subgoals):
 1. \<And>s ba. \<lbrakk>P cs; arg_rel cs; arg_rel s; globals s = globals cs; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal ba\<rbrakk> \<Longrightarrow> s \<in> P' s
 2. \<And>s ba. \<lbrakk>P cs; arg_rel cs; arg_rel s; globals s = globals cs; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal ba; ba \<in> Collect (Q s)\<rbrakk> \<Longrightarrow> globals ba = globals cs \<and> (\<exists>cs'. ret_xf ba = ret_xf cs' \<and> Q cs cs') proof (prove)
goal (2 subgoals):
 1. \<And>s ba. \<lbrakk>P cs; arg_rel cs; arg_rel s; globals s = globals cs; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal ba\<rbrakk> \<Longrightarrow> P s
 2. \<And>s ba. \<lbrakk>P cs; arg_rel cs; arg_rel s; globals s = globals cs; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal ba; ba \<in> Collect (Q s)\<rbrakk> \<Longrightarrow> globals ba = globals cs \<and> (\<exists>cs'. ret_xf ba = ret_xf cs' \<and> Q cs cs') proof (prove)
goal (1 subgoal):
 1. \<And>s ba. \<lbrakk>P cs; arg_rel cs; arg_rel s; globals s = globals cs; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal ba; ba \<in> Collect (Q s)\<rbrakk> \<Longrightarrow> globals ba = globals cs \<and> (\<exists>cs'. ret_xf ba = ret_xf cs' \<and> Q cs cs') proof (prove)
goal (1 subgoal):
 1. \<And>s ba. \<lbrakk>P cs; arg_rel cs; arg_rel s; globals s = globals cs; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal ba; ba \<in> Collect (Q s); ba \<in> {t. t may_not_modify_globals s}\<rbrakk> \<Longrightarrow> globals ba = globals cs \<and> (\<exists>cs'. ret_xf ba = ret_xf cs' \<and> Q cs cs') proof (prove)
goal (1 subgoal):
 1. \<And>s ba. \<lbrakk>P cs; arg_rel cs; arg_rel s; globals s = globals cs; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal ba; Q s ba; globals ba = globals cs\<rbrakk> \<Longrightarrow> \<exists>cs'. ret_xf ba = ret_xf cs' \<and> Q cs cs' proof (prove)
goal:
No subgoals!
flex-flex pairs:
\<lambda>s ba. ?t190 s ba (typ_at' (?T189 s ba) (?p189 s ba) (?s189 s ba)) \<equiv>\<^sup>? \<lambda>s ba. ?t188 s ba (typ_at' (?T187 s ba) (?p187 s ba) (?s187 s ba))
\<lambda>s ba. ?t190 s ba (typ_at' (?T189 s ba) (?p189 s ba) (?s189 s ba\<lparr>ksMachineState := ksMachineState (?s189 s ba)\<lparr>irq_state := ?f189 s ba (irq_state (ksMachineState (?s189 s ba)))\<rparr>\<rparr>)) \<equiv>\<^sup>? \<lambda>s ba. ?t188 s ba (typ_at' (?T187 s ba) (?p187 s ba) (?s187 s ba\<lparr>ksMachineState := ksMachineState (?s187 s ba)\<lparr>irq_state := ?f187 s ba (irq_state (ksMachineState (?s187 s ba)))\<rparr>\<rparr>))
\<lambda>s ba. ?t158 s ba (typ_at' (?T157 s ba) (?p157 s ba) (?s157 s ba)) \<equiv>\<^sup>? \<lambda>s ba. ?t156 s ba (typ_at' (?T155 s ba) (?p155 s ba) (?s155 s ba))
\<lambda>s ba. ?t158 s ba (typ_at' (?T157 s ba) (?p157 s ba) (?s157 s ba\<lparr>ksMachineState := ksMachineState (?s157 s ba)\<lparr>irq_state := ?f157 s ba (irq_state (ksMachineState (?s157 s ba)))\<rparr>\<rparr>)) \<equiv>\<^sup>? \<lambda>s ba. ?t156 s ba (typ_at' (?T155 s ba) (?p155 s ba) (?s155 s ba\<lparr>ksMachineState := ksMachineState (?s155 s ba)\<lparr>irq_state := ?f155 s ba (irq_state (ksMachineState (?s155 s ba)))\<rparr>\<rparr>))