theory ArchADT_IF_Refine_C

lemma corres_dmo_getExMonitor_C:
  "corres_underlying rf_sr nf nf' (=) \<top> \<top> (doMachineOp getExMonitor) (doMachineOp_C getExMonitor)" apply (clarsimp simp: doMachineOp_def doMachineOp_C_def) apply (rule corres_guard_imp) apply (rule_tac r'="\<lambda>ms ms'. exclusive_state ms = exclusive_state ms' \<and>
                                 machine_state_rest ms = machine_state_rest ms' \<and>
                                 irq_masks ms = irq_masks ms' \<and> equiv_irq_state ms ms' \<and>
                                 device_state ms = device_state ms'"
                and P="\<top>" and P'="\<top>" in corres_split) apply (clarsimp simp: rf_sr_def cstate_relation_def cmachine_state_relation_def Let_def) apply (rule_tac r'="\<lambda>(r, ms) (r', ms'). r = r' \<and> ms = rv \<and> ms' = rv'"
              in corres_split) apply (rule corres_trivial, rule corres_select_f') apply (clarsimp simp: getExMonitor_def machine_rest_lift_def Nondet_Monad.bind_def gets_def
                                get_def return_def modify_def put_def select_f_def) apply (clarsimp simp: getExMonitor_no_fail[simplified no_fail_def]) apply (clarsimp simp: split_def) apply (rule_tac r'=dc and P="\<lambda>s. underlying_memory (snd ((aa, b), ba)) =
                                         underlying_memory (ksMachineState s)"
                              and P'="\<lambda>s. underlying_memory (snd ((aa, b), bc)) =
                                          underlying_memory (phantom_machine_state_' (globals s))"
                in corres_split) apply (rule corres_modify) apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def
                                 cmachine_state_relation_def Let_def) apply (rule corres_trivial, clarsimp) apply (wp hoare_TrueI)+ apply (rule TrueI conjI | clarsimp simp: getExMonitor_def machine_rest_lift_def Nondet_Monad.bind_def
                                            gets_def get_def return_def modify_def put_def select_f_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr nf nf' (=) (\<lambda>_. True) (\<lambda>_. True) (doMachineOp getExMonitor) (doMachineOp_C getExMonitor) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr nf nf' (=) (\<lambda>_. True) (\<lambda>_. True) (do ms <- gets ksMachineState;
(r, ms') <- select_f (getExMonitor ms);
y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od) (do ms <- gets (\<lambda>s. phantom_machine_state_' (globals s));
(r, ms') <- select_f (getExMonitor ms);
y <- modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>);
return r
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying rf_sr nf nf' (=) ?Q ?Q' (do ms <- gets ksMachineState;
(r, ms') <- select_f (getExMonitor ms);
y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od) (do ms <- gets (\<lambda>s. phantom_machine_state_' (globals s));
(r, ms') <- select_f (getExMonitor ms);
y <- modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>);
return r
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. True \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres_underlying rf_sr nf nf' (\<lambda>ms ms'. exclusive_state ms = exclusive_state ms' \<and> machine_state_rest ms = machine_state_rest ms' \<and> irq_masks ms = irq_masks ms' \<and> equiv_irq_state ms ms' \<and> device_state ms = device_state ms') (\<lambda>_. True) (\<lambda>_. True) (gets ksMachineState) (gets (\<lambda>s. phantom_machine_state_' (globals s)))
 2. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> corres_underlying rf_sr nf nf' (=) (?R4 rv) (?R'4 rv') (do (r, ms') <- select_f (getExMonitor rv);
y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od) (do (r, ms') <- select_f (getExMonitor rv');
y <- modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>);
return r
od)
 3. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>?R'4\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> corres_underlying rf_sr nf nf' (=) (?R4 rv) (?R'4 rv') (do (r, ms') <- select_f (getExMonitor rv);
y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od) (do (r, ms') <- select_f (getExMonitor rv');
y <- modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>);
return r
od)
 2. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> corres_underlying rf_sr nf nf' (\<lambda>(r, ms) (r', ms'). r = r' \<and> ms = rv \<and> ms' = rv') (?P21 rv) (?P'23 rv') (select_f (getExMonitor rv)) (select_f (getExMonitor rv'))
 2. \<And>rv rv' rva rv'a. \<lbrakk>exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv'; (case rva of (r, ms) \<Rightarrow> \<lambda>(r', ms'). r = r' \<and> ms = rv \<and> ms' = rv') rv'a\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' (=) (?R17 rv rv' rva) (?R'17 rv rv' rv'a) (case rva of (r, ms') \<Rightarrow> do y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od) (case rv'a of (r, ms') \<Rightarrow> do y <- modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>);
return r
od)
 3. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q22 rv\<rbrace> select_f (getExMonitor rv) \<lbrace>?R17 rv rv'\<rbrace>
 4. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q'24 rv'\<rbrace> select_f (getExMonitor rv') \<lbrace>?R'17 rv rv'\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. ?P21 rv and ?Q22 rv\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>\<lambda>rv'. ?P'23 rv' and ?Q'24 rv'\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' s s'. \<lbrakk>exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv'; True; True\<rbrakk> \<Longrightarrow> \<forall>s'\<in>fst (getExMonitor rv'). \<exists>s\<in>fst (getExMonitor rv). (case s of (r, ms) \<Rightarrow> \<lambda>(r', ms'). r = r' \<and> ms = rv \<and> ms' = rv') s'
 2. \<And>rv rv'. \<lbrakk>exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv'; nf'\<rbrakk> \<Longrightarrow> \<not> snd (getExMonitor rv')
 3. \<And>rv rv' rva rv'a. \<lbrakk>exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv'; (case rva of (r, ms) \<Rightarrow> \<lambda>(r', ms'). r = r' \<and> ms = rv \<and> ms' = rv') rv'a\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' (=) (?R17 rv rv' rva) (?R'17 rv rv' rv'a) (case rva of (r, ms') \<Rightarrow> do y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od) (case rv'a of (r, ms') \<Rightarrow> do y <- modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>);
return r
od)
 4. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q22 rv\<rbrace> select_f (getExMonitor rv) \<lbrace>?R17 rv rv'\<rbrace>
 5. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q'24 rv'\<rbrace> select_f (getExMonitor rv') \<lbrace>?R'17 rv rv'\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q22 rv\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'24 rv'\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv'. \<lbrakk>exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv'; nf'\<rbrakk> \<Longrightarrow> \<not> snd (getExMonitor rv')
 2. \<And>rv rv' rva rv'a. \<lbrakk>exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv'; (case rva of (r, ms) \<Rightarrow> \<lambda>(r', ms'). r = r' \<and> ms = rv \<and> ms' = rv') rv'a\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' (=) (?R17 rv rv' rva) (?R'17 rv rv' rv'a) (case rva of (r, ms') \<Rightarrow> do y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od) (case rv'a of (r, ms') \<Rightarrow> do y <- modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>);
return r
od)
 3. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q22 rv\<rbrace> select_f (getExMonitor rv) \<lbrace>?R17 rv rv'\<rbrace>
 4. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q'24 rv'\<rbrace> select_f (getExMonitor rv') \<lbrace>?R'17 rv rv'\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q22 rv\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'24 rv'\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv'; (case rva of (r, ms) \<Rightarrow> \<lambda>(r', ms'). r = r' \<and> ms = rv \<and> ms' = rv') rv'a\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' (=) (?R17 rv rv' rva) (?R'17 rv rv' rv'a) (case rva of (r, ms') \<Rightarrow> do y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od) (case rv'a of (r, ms') \<Rightarrow> do y <- modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>);
return r
od)
 2. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q22 rv\<rbrace> select_f (getExMonitor rv) \<lbrace>?R17 rv rv'\<rbrace>
 3. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q'24 rv'\<rbrace> select_f (getExMonitor rv') \<lbrace>?R'17 rv rv'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q22 rv\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'24 rv'\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>b ba aa bc. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' (=) (?R17 ba bc ((aa, b), ba)) (?R'17 ba bc ((aa, b), bc)) (do y <- modify (ksMachineState_update (\<lambda>_. ba));
return (aa, b)
od) (do y <- modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := bc\<rparr>\<rparr>);
return (aa, b)
od)
 2. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q22 rv\<rbrace> select_f (getExMonitor rv) \<lbrace>?R17 rv rv'\<rbrace>
 3. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q'24 rv'\<rbrace> select_f (getExMonitor rv') \<lbrace>?R'17 rv rv'\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q22 rv\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'24 rv'\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>b ba aa bc. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' dc (\<lambda>s. underlying_memory (snd ((aa, b), ba)) = underlying_memory (ksMachineState s)) (\<lambda>s. underlying_memory (snd ((aa, b), bc)) = underlying_memory (phantom_machine_state_' (globals s))) (modify (ksMachineState_update (\<lambda>_. ba))) (modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := bc\<rparr>\<rparr>))
 2. \<And>b ba aa bc rv rv'. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc; dc rv rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' (=) (?R37 b ba aa bc rv) (?R'37 b ba aa bc rv') (return (aa, b)) (return (aa, b))
 3. \<And>b ba aa bc. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc\<rbrakk> \<Longrightarrow> \<lbrace>?Q46 ba bc ((aa, b), ba)\<rbrace> modify (ksMachineState_update (\<lambda>_. ba)) \<lbrace>?R37 b ba aa bc\<rbrace>
 4. \<And>b ba aa bc. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 ba bc ((aa, b), bc)\<rbrace> modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := bc\<rparr>\<rparr>) \<lbrace>?R'37 b ba aa bc\<rbrace>
 5. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q22 rv\<rbrace> select_f (getExMonitor rv) \<lbrace>\<lambda>a. (\<lambda>s. underlying_memory (snd a) = underlying_memory (ksMachineState s)) and ?Q46 rv rv' a\<rbrace>
 6. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q'24 rv'\<rbrace> select_f (getExMonitor rv') \<lbrace>\<lambda>a. (\<lambda>s. underlying_memory (snd a) = underlying_memory (phantom_machine_state_' (globals s))) and ?Q'45 rv rv' a\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q22 rv\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'24 rv'\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>b ba aa bc s s'. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc; underlying_memory (snd ((aa, b), ba)) = underlying_memory (ksMachineState s); underlying_memory (snd ((aa, b), bc)) = underlying_memory (phantom_machine_state_' (globals s')); (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s\<lparr>ksMachineState := ba\<rparr>, s'\<lparr>globals := globals s'\<lparr>phantom_machine_state_' := bc\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>b ba aa bc rv rv'. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc; dc rv rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' (=) (?R37 b ba aa bc rv) (?R'37 b ba aa bc rv') (return (aa, b)) (return (aa, b))
 3. \<And>b ba aa bc. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc\<rbrakk> \<Longrightarrow> \<lbrace>?Q46 ba bc ((aa, b), ba)\<rbrace> modify (ksMachineState_update (\<lambda>_. ba)) \<lbrace>?R37 b ba aa bc\<rbrace>
 4. \<And>b ba aa bc. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 ba bc ((aa, b), bc)\<rbrace> modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := bc\<rparr>\<rparr>) \<lbrace>?R'37 b ba aa bc\<rbrace>
 5. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q22 rv\<rbrace> select_f (getExMonitor rv) \<lbrace>\<lambda>a. (\<lambda>s. underlying_memory (snd a) = underlying_memory (ksMachineState s)) and ?Q46 rv rv' a\<rbrace>
 6. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q'24 rv'\<rbrace> select_f (getExMonitor rv') \<lbrace>\<lambda>a. (\<lambda>s. underlying_memory (snd a) = underlying_memory (phantom_machine_state_' (globals s))) and ?Q'45 rv rv' a\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q22 rv\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'24 rv'\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>b ba aa bc rv rv'. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc; dc rv rv'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' (=) (?R37 b ba aa bc rv) (?R'37 b ba aa bc rv') (return (aa, b)) (return (aa, b))
 2. \<And>b ba aa bc. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc\<rbrakk> \<Longrightarrow> \<lbrace>?Q46 ba bc ((aa, b), ba)\<rbrace> modify (ksMachineState_update (\<lambda>_. ba)) \<lbrace>?R37 b ba aa bc\<rbrace>
 3. \<And>b ba aa bc. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 ba bc ((aa, b), bc)\<rbrace> modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := bc\<rparr>\<rparr>) \<lbrace>?R'37 b ba aa bc\<rbrace>
 4. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q22 rv\<rbrace> select_f (getExMonitor rv) \<lbrace>\<lambda>a. (\<lambda>s. underlying_memory (snd a) = underlying_memory (ksMachineState s)) and ?Q46 rv rv' a\<rbrace>
 5. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q'24 rv'\<rbrace> select_f (getExMonitor rv') \<lbrace>\<lambda>a. (\<lambda>s. underlying_memory (snd a) = underlying_memory (phantom_machine_state_' (globals s))) and ?Q'45 rv rv' a\<rbrace>
 6. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q22 rv\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'24 rv'\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>b ba aa bc. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc\<rbrakk> \<Longrightarrow> \<lbrace>?Q46 ba bc ((aa, b), ba)\<rbrace> modify (ksMachineState_update (\<lambda>_. ba)) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>b ba aa bc. \<lbrakk>exclusive_state ba = exclusive_state bc; machine_state_rest ba = machine_state_rest bc; irq_masks ba = irq_masks bc; equiv_irq_state ba bc; device_state ba = device_state bc\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 ba bc ((aa, b), bc)\<rbrace> modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := bc\<rparr>\<rparr>) \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q22 rv\<rbrace> select_f (getExMonitor rv) \<lbrace>\<lambda>a. (\<lambda>s. underlying_memory (snd a) = underlying_memory (ksMachineState s)) and ?Q46 rv rv' a\<rbrace>
 4. \<And>rv rv'. exclusive_state rv = exclusive_state rv' \<and> machine_state_rest rv = machine_state_rest rv' \<and> irq_masks rv = irq_masks rv' \<and> equiv_irq_state rv rv' \<and> device_state rv = device_state rv' \<Longrightarrow> \<lbrace>?Q'24 rv'\<rbrace> select_f (getExMonitor rv') \<lbrace>\<lambda>a. (\<lambda>s. underlying_memory (snd a) = underlying_memory (phantom_machine_state_' (globals s))) and ?Q'45 rv rv' a\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q22 rv\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'24 rv'\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>a. \<forall>x\<in>fst (getExMonitor (ksMachineState s)). ((\<lambda>s. underlying_memory (snd x) = underlying_memory (ksMachineState s)) and ?Q69 (snd (fst x)) (fst (fst x)) (fst x) (ksMachineState s) x) a)) s)) s
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>a. \<forall>x\<in>fst (getExMonitor (phantom_machine_state_' (globals s))). ((\<lambda>s. underlying_memory (snd x) = underlying_memory (phantom_machine_state_' (globals s))) and ?Q'75 (snd (fst x)) (fst (fst x)) (fst x) (phantom_machine_state_' (globals s)) x) a)) s)) s proof (prove)
goal:
No subgoals!