theory KHeap_DR

lemma dcorres_machine_op_noop:
  "\<lbrakk> \<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> \<rbrakk>
       \<Longrightarrow> dcorres dc \<top> \<top> (return ()) (do_machine_op mop)" supply if_cong[cong] apply (simp add: do_machine_op_def) apply (rule corres_guard_imp) apply (rule corres_symb_exec_r[OF _ _ gets_wp]) apply (rule corres_symb_exec_r) apply (simp add: split_beta) apply (rule corres_split[where r'=dc, THEN corres_add_noop_lhs,
                                  OF _ _ return_wp]) apply (simp add: return_modify) apply (rule_tac P=\<top> and P'="\<lambda>s. underlying_memory (snd rv)
                    = underlying_memory (machine_state s)" in corres_modify) apply (clarsimp simp: transform_def transform_objects_def2
                                 transform_current_thread_def) apply (rule corres_trivial, simp) apply (wp | simp)+ apply clarsimp apply (drule use_valid, assumption, rule refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do_machine_op mop) proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do_machine_op mop) proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do ms <- gets machine_state;
(r, ms') <- select_f (mop ms);
y <- modify (update_machine ms');
return r
od) proof (prove)
goal (3 subgoals):
 1. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> dcorres dc ?Q ?Q' (return ()) (do ms <- gets machine_state;
(r, ms') <- select_f (mop ms);
y <- modify (update_machine ms');
return r
od)
 2. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>ms. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> dcorres dc ?Q (?Q'4 ms) (return ()) (do (r, ms') <- select_f (mop ms);
y <- modify (update_machine ms');
return r
od)
 2. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'\<rbrace> gets machine_state \<lbrace>?Q'4\<rbrace>
 3. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail ?Q' (gets machine_state)
 4. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q s
 5. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>ms rv. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> dcorres dc ?Q (?Q'14 ms rv) (return ()) (case rv of (r, ms') \<Rightarrow> do y <- modify (update_machine ms');
return r
od)
 2. \<And>ms. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'4 ms\<rbrace> select_f (mop ms) \<lbrace>?Q'14 ms\<rbrace>
 3. \<And>ms s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; ?Q'4 ms s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (mop ms) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>ms. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (?Q'4 ms) (select_f (mop ms))
 5. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'\<rbrace> gets machine_state \<lbrace>?Q'4\<rbrace>
 6. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail ?Q' (gets machine_state)
 7. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q s
 8. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>ms rv. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> dcorres dc ?Q (?Q'14 ms rv) (return ()) (do y <- modify (update_machine (snd rv));
return (fst rv)
od)
 2. \<And>ms. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'4 ms\<rbrace> select_f (mop ms) \<lbrace>?Q'14 ms\<rbrace>
 3. \<And>ms s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; ?Q'4 ms s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (mop ms) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>ms. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (?Q'4 ms) (select_f (mop ms))
 5. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'\<rbrace> gets machine_state \<lbrace>?Q'4\<rbrace>
 6. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail ?Q' (gets machine_state)
 7. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q s
 8. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (10 subgoals):
 1. \<And>ms rv. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> dcorres dc ?P29 (?P'20 ms rv) (return ()) (modify (update_machine (snd rv)))
 2. \<And>ms rv uu_ y. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; dc uu_ y\<rbrakk> \<Longrightarrow> dcorres dc (?R27 uu_) (?R'20 ms rv y) (return ()) (return (fst rv))
 3. \<And>ms rv. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'20 ms rv\<rbrace> modify (update_machine (snd rv)) \<lbrace>?R'20 ms rv\<rbrace>
 4. \<And>ms. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'4 ms\<rbrace> select_f (mop ms) \<lbrace>\<lambda>rv. ?P'20 ms rv and ?Q'20 ms rv\<rbrace>
 5. \<And>ms s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; ?Q'4 ms s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (mop ms) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>ms. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (?Q'4 ms) (select_f (mop ms))
 7. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'\<rbrace> gets machine_state \<lbrace>?Q'4\<rbrace>
 8. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail ?Q' (gets machine_state)
 9. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> (?P29 and ?R27 ()) s
 10. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (10 subgoals):
 1. \<And>ms rv. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> dcorres dc ?P29 (?P'20 ms rv) (modify id) (modify (update_machine (snd rv)))
 2. \<And>ms rv uu_ y. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; dc uu_ y\<rbrakk> \<Longrightarrow> dcorres dc (?R27 uu_) (?R'20 ms rv y) (return ()) (return (fst rv))
 3. \<And>ms rv. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'20 ms rv\<rbrace> modify (update_machine (snd rv)) \<lbrace>?R'20 ms rv\<rbrace>
 4. \<And>ms. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'4 ms\<rbrace> select_f (mop ms) \<lbrace>\<lambda>rv. ?P'20 ms rv and ?Q'20 ms rv\<rbrace>
 5. \<And>ms s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; ?Q'4 ms s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (mop ms) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>ms. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (?Q'4 ms) (select_f (mop ms))
 7. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'\<rbrace> gets machine_state \<lbrace>?Q'4\<rbrace>
 8. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail ?Q' (gets machine_state)
 9. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> (?P29 and ?R27 ()) s
 10. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (10 subgoals):
 1. \<And>ms rv s s'. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True; underlying_memory (snd rv) = underlying_memory (machine_state s'); (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (id s, update_machine (snd rv) s') \<in> {ss'. transform (snd ss') = fst ss'}
 2. \<And>ms rv uu_ y. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; dc uu_ y\<rbrakk> \<Longrightarrow> dcorres dc (?R27 uu_) (?R'20 ms rv y) (return ()) (return (fst rv))
 3. \<And>ms rv. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'20 ms rv\<rbrace> modify (update_machine (snd rv)) \<lbrace>?R'20 ms rv\<rbrace>
 4. \<And>ms. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'4 ms\<rbrace> select_f (mop ms) \<lbrace>\<lambda>rv. (\<lambda>s. underlying_memory (snd rv) = underlying_memory (machine_state s)) and ?Q'20 ms rv\<rbrace>
 5. \<And>ms s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; ?Q'4 ms s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (mop ms) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>ms. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (?Q'4 ms) (select_f (mop ms))
 7. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'\<rbrace> gets machine_state \<lbrace>?Q'4\<rbrace>
 8. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail ?Q' (gets machine_state)
 9. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R27 ()) s
 10. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (9 subgoals):
 1. \<And>ms rv uu_ y. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; dc uu_ y\<rbrakk> \<Longrightarrow> dcorres dc (?R27 uu_) (?R'20 ms rv y) (return ()) (return (fst rv))
 2. \<And>ms rv. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'20 ms rv\<rbrace> modify (update_machine (snd rv)) \<lbrace>?R'20 ms rv\<rbrace>
 3. \<And>ms. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'4 ms\<rbrace> select_f (mop ms) \<lbrace>\<lambda>rv. (\<lambda>s. underlying_memory (snd rv) = underlying_memory (machine_state s)) and ?Q'20 ms rv\<rbrace>
 4. \<And>ms s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; ?Q'4 ms s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (mop ms) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>ms. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (?Q'4 ms) (select_f (mop ms))
 6. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'\<rbrace> gets machine_state \<lbrace>?Q'4\<rbrace>
 7. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail ?Q' (gets machine_state)
 8. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R27 ()) s
 9. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>ms rv. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'20 ms rv\<rbrace> modify (update_machine (snd rv)) \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>ms. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'4 ms\<rbrace> select_f (mop ms) \<lbrace>\<lambda>rv. (\<lambda>s. underlying_memory (snd rv) = underlying_memory (machine_state s)) and ?Q'20 ms rv\<rbrace>
 3. \<And>ms s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; ?Q'4 ms s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (mop ms) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>ms. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail (?Q'4 ms) (select_f (mop ms))
 5. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<lbrace>?Q'\<rbrace> gets machine_state \<lbrace>?Q'4\<rbrace>
 6. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; False\<rbrakk> \<Longrightarrow> no_fail ?Q' (gets machine_state)
 7. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True)) s
 8. \<And>s. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; True\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>) \<Longrightarrow> \<forall>x\<in>fst (mop (machine_state s)). underlying_memory (snd x) = underlying_memory (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; (a, b) \<in> fst (mop (machine_state s))\<rbrakk> \<Longrightarrow> underlying_memory b = underlying_memory (machine_state s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>; underlying_memory b = underlying_memory (machine_state s)\<rbrakk> \<Longrightarrow> underlying_memory b = underlying_memory (machine_state s) proof (prove)
goal:
No subgoals!