theory ArchADT_IF_Refine_C

lemma corres_dmo_setExMonitor_C:
  "corres_underlying rf_sr nf nf' dc \<top> \<top> (doMachineOp (setExMonitor es)) (doMachineOp_C (setExMonitor es))" 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'). ms = rv\<lparr>exclusive_state := es\<rparr> \<and>
                                              ms' = rv'\<lparr>exclusive_state := es\<rparr>"
              in corres_split) apply (rule corres_trivial, rule corres_select_f') apply (clarsimp simp: setExMonitor_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: setExMonitor_no_fail[simplified no_fail_def]) apply (simp add: split_def) apply (rule_tac P="\<lambda>s. underlying_memory (snd rva) =
                               underlying_memory (ksMachineState s)"
                    and P'="\<lambda>s. underlying_memory (snd rv'a) =
                                underlying_memory (phantom_machine_state_' (globals s))"
                     in corres_modify) apply (clarsimp simp: rf_sr_def cstate_relation_def carch_state_relation_def
                              cmachine_state_relation_def Let_def) apply (wp hoare_TrueI)+ apply (rule TrueI conjI | clarsimp simp: setExMonitor_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' dc (\<lambda>_. True) (\<lambda>_. True) (doMachineOp (setExMonitor es)) (doMachineOp_C (setExMonitor es)) proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr nf nf' dc (\<lambda>_. True) (\<lambda>_. True) (do ms <- gets ksMachineState;
(r, ms') <- select_f (setExMonitor es ms);
modify (ksMachineState_update (\<lambda>_. ms'))
od) (do ms <- gets (\<lambda>s. phantom_machine_state_' (globals s));
(r, ms') <- select_f (setExMonitor es ms);
modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>)
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying rf_sr nf nf' dc ?Q ?Q' (do ms <- gets ksMachineState;
(r, ms') <- select_f (setExMonitor es ms);
modify (ksMachineState_update (\<lambda>_. ms'))
od) (do ms <- gets (\<lambda>s. phantom_machine_state_' (globals s));
(r, ms') <- select_f (setExMonitor es ms);
modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>)
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' dc (?R4 rv) (?R'4 rv') (do (r, ms') <- select_f (setExMonitor es rv);
modify (ksMachineState_update (\<lambda>_. ms'))
od) (do (r, ms') <- select_f (setExMonitor es rv');
modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>)
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' dc (?R4 rv) (?R'4 rv') (do (r, ms') <- select_f (setExMonitor es rv);
modify (ksMachineState_update (\<lambda>_. ms'))
od) (do (r, ms') <- select_f (setExMonitor es rv');
modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>)
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'). ms = rv\<lparr>exclusive_state := es\<rparr> \<and> ms' = rv'\<lparr>exclusive_state := es\<rparr>) (?P21 rv) (?P'23 rv') (select_f (setExMonitor es rv)) (select_f (setExMonitor es 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'). ms = rv\<lparr>exclusive_state := es\<rparr> \<and> ms' = rv'\<lparr>exclusive_state := es\<rparr>) rv'a\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' dc (?R17 rv rv' rva) (?R'17 rv rv' rv'a) (case rva of (r, ms') \<Rightarrow> modify (ksMachineState_update (\<lambda>_. ms'))) (case rv'a of (r, ms') \<Rightarrow> modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>))
 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 (setExMonitor es 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 (setExMonitor es 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 (setExMonitor es rv'). \<exists>s\<in>fst (setExMonitor es rv). (case s of (r, ms) \<Rightarrow> \<lambda>(r', ms'). ms = rv\<lparr>exclusive_state := es\<rparr> \<and> ms' = rv'\<lparr>exclusive_state := es\<rparr>) 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 (setExMonitor es 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'). ms = rv\<lparr>exclusive_state := es\<rparr> \<and> ms' = rv'\<lparr>exclusive_state := es\<rparr>) rv'a\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' dc (?R17 rv rv' rva) (?R'17 rv rv' rv'a) (case rva of (r, ms') \<Rightarrow> modify (ksMachineState_update (\<lambda>_. ms'))) (case rv'a of (r, ms') \<Rightarrow> modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>))
 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 (setExMonitor es 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 (setExMonitor es 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 (setExMonitor es 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'). ms = rv\<lparr>exclusive_state := es\<rparr> \<and> ms' = rv'\<lparr>exclusive_state := es\<rparr>) rv'a\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' dc (?R17 rv rv' rva) (?R'17 rv rv' rv'a) (case rva of (r, ms') \<Rightarrow> modify (ksMachineState_update (\<lambda>_. ms'))) (case rv'a of (r, ms') \<Rightarrow> modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>))
 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 (setExMonitor es 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 (setExMonitor es 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'). ms = rv\<lparr>exclusive_state := es\<rparr> \<and> ms' = rv'\<lparr>exclusive_state := es\<rparr>) rv'a\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' dc (?R17 rv rv' rva) (?R'17 rv rv' rv'a) (case rva of (r, ms') \<Rightarrow> modify (ksMachineState_update (\<lambda>_. ms'))) (case rv'a of (r, ms') \<Rightarrow> modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := ms'\<rparr>\<rparr>))
 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 (setExMonitor es 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 (setExMonitor es 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>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'; snd rva = rv\<lparr>exclusive_state := es\<rparr> \<and> snd rv'a = rv'\<lparr>exclusive_state := es\<rparr>\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' dc (?R17 rv rv' rva) (?R'17 rv rv' rv'a) (modify (ksMachineState_update (\<lambda>_. rv\<lparr>exclusive_state := es\<rparr>))) (modify (\<lambda>s. s\<lparr>globals := globals s\<lparr>phantom_machine_state_' := rv'\<lparr>exclusive_state := es\<rparr>\<rparr>\<rparr>))
 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 (setExMonitor es 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 (setExMonitor es 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>rv rv' rva rv'a 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'; snd rva = rv\<lparr>exclusive_state := es\<rparr> \<and> snd rv'a = rv'\<lparr>exclusive_state := es\<rparr>; underlying_memory (snd rva) = underlying_memory (ksMachineState s); underlying_memory (snd rv'a) = underlying_memory (phantom_machine_state_' (globals s')); (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> (s\<lparr>ksMachineState := rv\<lparr>exclusive_state := es\<rparr>\<rparr>, s'\<lparr>globals := globals s'\<lparr>phantom_machine_state_' := rv'\<lparr>exclusive_state := es\<rparr>\<rparr>\<rparr>) \<in> rf_sr
 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 (setExMonitor es rv) \<lbrace>\<lambda>rva s. underlying_memory (snd rva) = underlying_memory (ksMachineState s)\<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 (setExMonitor es rv') \<lbrace>\<lambda>rv'a s. underlying_memory (snd rv'a) = underlying_memory (phantom_machine_state_' (globals s))\<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 (6 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> \<lbrace>?Q22 rv\<rbrace> select_f (setExMonitor es rv) \<lbrace>\<lambda>rva s. underlying_memory (snd rva) = underlying_memory (ksMachineState s)\<rbrace>
 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>?Q'24 rv'\<rbrace> select_f (setExMonitor es rv') \<lbrace>\<lambda>rv'a s. underlying_memory (snd rv'a) = underlying_memory (phantom_machine_state_' (globals s))\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets ksMachineState \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q22 rv\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> gets (\<lambda>s. phantom_machine_state_' (globals s)) \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'24 rv'\<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 (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. \<forall>x\<in>fst (setExMonitor es (ksMachineState s)). underlying_memory (snd x) = underlying_memory (ksMachineState sa))) s)) s
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. \<forall>x\<in>fst (setExMonitor es (phantom_machine_state_' (globals s))). underlying_memory (snd x) = underlying_memory (phantom_machine_state_' (globals sa)))) s)) s proof (prove)
goal:
No subgoals!