theory AutoCorres_C

lemma autocorres_transfer_spec:
  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. \<Gamma>\<turnstile> (Collect (\<lambda>s. s0 = s \<and> P s)) Call f_'proc (Collect (Q s0))"
  assumes precond_deps:
    "\<And>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. P cs \<and> s = globals cs \<and> arg_rel cs \<rbrace>
           ac_f
         \<lbrace>\<lambda>r s'. \<exists>cs'. s' = globals cs' \<and> 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 (drule_tac ?s0.1=s in exec_normal[OF _ _ c_spec[rule_format], rotated]) apply (blast dest: precond_deps) apply (blast dest: postcond_deps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P cs \<and> s = globals cs \<and> arg_rel cs\<rbrace> ac_f \<lbrace>\<lambda>r s'. \<exists>cs'. s' = globals cs' \<and> 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> \<exists>cs'. b = globals cs' \<and> 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> \<exists>cs'. globals ba = globals cs' \<and> 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> \<exists>cs'. globals ba = globals cs' \<and> 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\<rbrakk> \<Longrightarrow> s \<in> {sa. s = sa \<and> P sa}
 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; ba \<in> Collect (Q s)\<rbrakk> \<Longrightarrow> \<exists>cs'. globals ba = globals cs' \<and> 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; ba \<in> Collect (Q s)\<rbrakk> \<Longrightarrow> \<exists>cs'. globals ba = globals cs' \<and> ret_xf ba = ret_xf cs' \<and> Q cs cs' proof (prove)
goal:
No subgoals!
flex-flex pairs:
\<lambda>s ba. ?t196 s ba (typ_at' (?T195 s ba) (?p195 s ba) (?s195 s ba)) \<equiv>\<^sup>? \<lambda>s ba. ?t194 s ba (typ_at' (?T193 s ba) (?p193 s ba) (?s193 s ba))
\<lambda>s ba. ?t196 s ba (typ_at' (?T195 s ba) (?p195 s ba) (?s195 s ba\<lparr>ksMachineState := ksMachineState (?s195 s ba)\<lparr>irq_state := ?f195 s ba (irq_state (ksMachineState (?s195 s ba)))\<rparr>\<rparr>)) \<equiv>\<^sup>? \<lambda>s ba. ?t194 s ba (typ_at' (?T193 s ba) (?p193 s ba) (?s193 s ba\<lparr>ksMachineState := ksMachineState (?s193 s ba)\<lparr>irq_state := ?f193 s ba (irq_state (ksMachineState (?s193 s ba)))\<rparr>\<rparr>))
\<lambda>s ba. ?t161 s ba (typ_at' (?T160 s ba) (?p160 s ba) (?s160 s ba)) \<equiv>\<^sup>? \<lambda>s ba. ?t159 s ba (typ_at' (?T158 s ba) (?p158 s ba) (?s158 s ba))
\<lambda>s ba. ?t161 s ba (typ_at' (?T160 s ba) (?p160 s ba) (?s160 s ba\<lparr>ksMachineState := ksMachineState (?s160 s ba)\<lparr>irq_state := ?f160 s ba (irq_state (ksMachineState (?s160 s ba)))\<rparr>\<rparr>)) \<equiv>\<^sup>? \<lambda>s ba. ?t159 s ba (typ_at' (?T158 s ba) (?p158 s ba) (?s158 s ba\<lparr>ksMachineState := ksMachineState (?s158 s ba)\<lparr>irq_state := ?f158 s ba (irq_state (ksMachineState (?s158 s ba)))\<rparr>\<rparr>))