diff --git a/proof/drefine/Arch_DR.thy b/proof/drefine/Arch_DR.thy
index c182d080a..d8c17a658 100644
--- a/proof/drefine/Arch_DR.thy
+++ b/proof/drefine/Arch_DR.thy
@@ -1117,7 +1117,7 @@ lemma set_cap_opt_cap':
                           split del:if_split cong: if_cong bind_cong;
     wpsimp wp: select_wp)
        apply (safe elim!:rsubst[where P=P] intro!: ext)
-       apply (clarsimp simp:opt_cap_def slots_of_def opt_object_def object_slots_def)+
+         apply (clarsimp simp:opt_cap_def slots_of_def opt_object_def object_slots_def)+
   done
 
 lemma set_cap_opt_cap:
@@ -1213,7 +1213,7 @@ lemma invoke_page_table_corres:
                     corres_split[OF _ corres_alternate1[OF dcorres_clear_object_caps_pt]])
            apply (rule dcorres_symb_exec_r)
              apply (rule corres_split[OF _ get_cap_corres])
-                apply (rule_tac P="\<lambda>y s. cte_wp_at ((=xb)) (a,b) s \<and>
+                apply (rule_tac P="\<lambda>y s. cte_wp_at ((=) xb) (a,b) s \<and>
                                     caps_of_state s' = caps_of_state s" in set_cap_corres_stronger)
                  apply (clarsimp simp:cte_wp_at_caps_of_state)
                  apply (clarsimp simp:is_arch_diminished_def transform_mapping_def update_map_data_def)
@@ -1652,7 +1652,7 @@ lemma invoke_page_corres:
    apply (rule corres_guard_imp)
      apply (rule corres_split[OF _ dcorres_unmap_page])
        apply (rule corres_split[OF _ get_cap_corres])
-          apply (rule_tac P="\<lambda>y s. cte_wp_at ((=x)) (a,b) s \<and>
+          apply (rule_tac P="\<lambda>y s. cte_wp_at ((=) x) (a,b) s \<and>
                                     caps_of_state s' = caps_of_state s"
             in set_cap_corres_stronger)
            apply (clarsimp simp:cte_wp_at_caps_of_state)
@@ -1808,7 +1808,7 @@ proof -
                  apply (clarsimp simp: valid_cap_simps cap_aligned_def)
                  apply (drule ex_cte_cap_to_not_idle,
                    auto simp: not_idle_thread_def)[1]
-                     apply (subst safe_parent_is_parent[where m=empty],
+                     apply (subst safe_parent_is_parent[where m=Map.empty],
                        auto simp: safe_parent_for_def
                        is_physical_def arch_is_physical_def)[1]
                     apply (case_tac cref,clarsimp)
diff --git a/proof/drefine/Corres_D.thy b/proof/drefine/Corres_D.thy
index 66a40304f..0c1008c0e 100644
--- a/proof/drefine/Corres_D.thy
+++ b/proof/drefine/Corres_D.thy
@@ -29,7 +29,7 @@ lemma select_ext_select[simp]: "select_ext a S = (select S :: ('b, unit) s_monad
                  return_def bind_def fail_def image_def
           split: if_split_asm)
 
-lemma OR_choice_OR[simp]: "(OR_choice c (f :: ('a,unit) s_monad) g) = (f OR g)"
+lemma OR_choice_OR[simp]: "(OR_choice c (f :: ('a,unit) s_monad) g) = (f \<sqinter> g)"
   apply (rule ext, rename_tac s)
   apply (clarsimp simp: OR_choice_def alternative_def get_def select_def return_def bind_def
                         select_f_def mk_ef_def wrap_ext_unit_def wrap_ext_bool_unit_def image_def
@@ -166,7 +166,7 @@ using assms
 by (fastforce simp:corres_underlying_def)
 
 lemma dcorres_absorb_get_l:
-  assumes "!!s'. \<lbrakk> P (transform s');P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=s')) (f (transform s')) g"
+  assumes "!!s'. \<lbrakk> P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g"
   shows "dcorres rv P P' (do t\<leftarrow> get; f t od)  g"
   apply (rule corres_symb_exec_l [where Q="%x. P and ((=) x)"])
     apply (rule dcorres_expand_pfx)
@@ -178,7 +178,7 @@ lemma dcorres_absorb_get_l:
 lemma dcorres_expand_get_l:
   assumes "dcorres rv P P' (do t\<leftarrow>get; f t od) g"
   shows "\<lbrakk> P (transform s'); P' s'\<rbrakk> \<Longrightarrow>
-         dcorres rv ((=) (transform s')) ((=s')) (f (transform s')) g"
+         dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g"
   using assms
   by (simp add:get_def corres_underlying_def bind_def)
 
@@ -216,7 +216,7 @@ lemma dcorres_get:
           \<Longrightarrow> dcorres r ((=) s) ((=) s') (f s) (f' s')"
   shows "dcorres r P P' (do s\<leftarrow>get;f s od) (do s'\<leftarrow> get; f' s' od)"
   apply (rule dcorres_expand_pfx)
-  apply (rule_tac r'="\<lambda>r r'. s=r \<and> s'=r'" and P="%x. (=s)" and P'="%x. (=s')" in corres_underlying_split)
+  apply (rule_tac r'="\<lambda>r r'. s=r \<and> s'=r'" and P="%x. (=) s" and P'="%x. (=) s'" in corres_underlying_split)
     apply (clarsimp simp: corres_underlying_def get_def)
     apply wp+
   apply (drule A)
@@ -239,8 +239,8 @@ lemma dcorres_gets_the:
     apply (clarsimp split:option.splits simp:corres_free_fail)
       apply (subgoal_tac "\<exists>obj. g x \<noteq> None")
       apply (clarsimp split:option.splits)
-      apply (rule_tac Q="(=)(transform xa)" and Q'="(=xa)" in corres_guard_imp)
-    apply (simp add:A)+
+      apply (rule_tac Q="(=)(transform xa)" and Q'="(=) xa" in corres_guard_imp)
+    apply (simp add: A)+
   using B
   apply (wp|clarsimp)+
 done
diff --git a/proof/drefine/Finalise_DR.thy b/proof/drefine/Finalise_DR.thy
index 7c646c857..ab9667d3a 100644
--- a/proof/drefine/Finalise_DR.thy
+++ b/proof/drefine/Finalise_DR.thy
@@ -444,7 +444,7 @@ lemma finalise_cancel_ipc:
       tcb_at_cte_at_2[unfolded tcb_at_def])
    apply (simp add:cancel_signal_def)
    apply (rule corres_guard_imp)
-     apply (rule_tac Q'="\<lambda>r. valid_ntfn r and (=s')" in corres_symb_exec_r)
+     apply (rule_tac Q'="\<lambda>r. valid_ntfn r and (=) s'" in corres_symb_exec_r)
         apply (rule corres_symb_exec_r)
            apply (rule corres_dummy_return_pl)
            apply (rule corres_split[ OF _ corres_dummy_set_notification])
@@ -2616,7 +2616,7 @@ lemma prepare_thread_delete_dcorres: "dcorres dc P P' (CSpace_D.prepare_thread_d
 lemma dcorres_finalise_cap:
   "cdlcap = transform_cap cap \<Longrightarrow>
       dcorres (\<lambda>r r'. fst r = transform_cap (fst r'))
-             \<top> (invs and valid_cap cap and valid_pdpt_objs and cte_wp_at ((=cap)) slot and valid_etcbs)
+             \<top> (invs and valid_cap cap and valid_pdpt_objs and cte_wp_at ((=) cap) slot and valid_etcbs)
           (CSpace_D.finalise_cap cdlcap final)
           (CSpace_A.finalise_cap cap final)"
   apply (case_tac cap)
diff --git a/proof/drefine/Intent_DR.thy b/proof/drefine/Intent_DR.thy
index 45a11bf8f..a9762a862 100644
--- a/proof/drefine/Intent_DR.thy
+++ b/proof/drefine/Intent_DR.thy
@@ -316,7 +316,7 @@ lemma set_cxt_none_det_intent_corres:
              (KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set cxt) obj')))"
   apply (clarsimp simp:bind_assoc opt_object_def corrupt_tcb_intent_def get_thread_def gets_def gets_the_def)
   apply (rule corres_guard_imp)
-    apply (rule_tac P="(=)(transform s')" and Q="(=s')"
+    apply (rule_tac P="(=)(transform s')" and Q="(=) s'"
        and x="transform_full_intent (machine_state (update_kheap ((kheap s')(y\<mapsto>(TCB (tcb_arch_update (arch_tcb_context_set cxt) obj')))) s'))
        y (tcb_arch_update (arch_tcb_context_set cxt) obj')"
        in select_pick_corres)
@@ -383,7 +383,7 @@ lemma dummy_corrupt_tcb_intent_corres:
   apply (clarsimp simp:tcb_at_def)
   apply (drule(1) valid_etcbs_get_tcb_get_etcb, clarsimp)
   apply (rule corres_guard_imp)
-    apply (rule_tac P="(=)(transform s')" and Q="(=s')"
+    apply (rule_tac P="(=)(transform s')" and Q="(=) s'"
        and x = "transform_full_intent (machine_state s') y tcb" in select_pick_corres)
     apply (clarsimp simp:update_thread_def gets_the_def gets_def bind_assoc)
     apply (rule dcorres_absorb_get_l)
@@ -476,7 +476,7 @@ lemma dcorres_dummy_corrupt_frame: "dcorres dc \<top> valid_etcbs
   apply (simp add:corrupt_frame_def)
   apply (rule dcorres_expand_pfx)
   apply (rule corres_guard_imp)
-    apply (rule_tac P="(=)(transform s')" and Q="(=s')"
+    apply (rule_tac P="(=)(transform s')" and Q="(=) s'"
       and x = "\<lambda>x. transform_full_intent (machine_state s') x (the (get_tcb x s'))"  in select_pick_corres)
     apply (clarsimp simp:get_def put_def modify_def assert_def bind_def return_def)
     apply (subst corres_singleton)
@@ -1194,13 +1194,13 @@ lemma get_ipc_buffer_words_empty_list[simp]:
 
 lemma evalMonad_mapM:
   "\<lbrakk>\<forall>r\<in>(set ls). evalMonad (f r) sa = evalMonad (g r) sb;
-    \<And>s r. \<lbrace>(=s\<rbrace>f) r\<lbrace>\<lambda>r. (=) s\<rbrace>;
-    \<And>s r. \<lbrace>(=s\<rbrace>g) r\<lbrace>\<lambda>r. (=) s\<rbrace>;
+    \<And>s r. \<lbrace>(=) s\<rbrace> f r\<lbrace>\<lambda>r. (=) s\<rbrace>;
+    \<And>s r. \<lbrace>(=) s\<rbrace> g r\<lbrace>\<lambda>r. (=) s\<rbrace>;
     \<And>r. empty_when_fail (f r);
     \<And>r. empty_when_fail (g r);
     \<And>r P. weak_det_spec P (f r);
     \<And>r P. weak_det_spec P (g r)\<rbrakk>
-   \<Longrightarrow> evalMonad (mapM f ls) sa= evalMonad (mapM g ls) sb"
+   \<Longrightarrow> evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb"
 proof(induct ls)
   case Nil
   show ?case by (clarsimp simp:mapM_def sequence_def)
diff --git a/proof/drefine/Interrupt_DR.thy b/proof/drefine/Interrupt_DR.thy
index 12cdd3eb1..ee596c0d8 100644
--- a/proof/drefine/Interrupt_DR.thy
+++ b/proof/drefine/Interrupt_DR.thy
@@ -287,7 +287,7 @@ lemma handle_interrupt_corres:
   apply (clarsimp split:irq_state.splits simp:corres_free_fail | rule conjI)+
    apply (simp add:Interrupt_D.handle_interrupt_def bind_assoc)
    apply (rule corres_guard_imp)
-     apply (rule_tac Q'="(=s')" in corres_split[OF _ dcorres_get_irq_slot])
+     apply (rule_tac Q'="(=) s'" in corres_split[OF _ dcorres_get_irq_slot])
        apply (rule_tac R'="\<lambda>rv.  (\<lambda>s. (is_ntfn_cap rv \<longrightarrow> ntfn_at (obj_ref_of rv) s)) and invs and valid_etcbs"
           in corres_split[OF _ option_get_cap_corres])
           apply (case_tac rv'a)
diff --git a/proof/drefine/Ipc_DR.thy b/proof/drefine/Ipc_DR.thy
index 925d91f55..1f6acca35 100644
--- a/proof/drefine/Ipc_DR.thy
+++ b/proof/drefine/Ipc_DR.thy
@@ -15,7 +15,7 @@ begin
 context begin interpretation Arch . (*FIXME: arch_split*)
 
 abbreviation
-"thread_is_running y s \<equiv> st_tcb_at ((=Structures_A.thread_state.Running)) y s"
+  "thread_is_running y s \<equiv> st_tcb_at ((=) Structures_A.Running) y s"
 
 lemmas [wp] = abs_typ_at_lifts[OF set_simple_ko_typ_at]
 
@@ -2823,7 +2823,7 @@ lemma send_fault_ipc_corres:
   apply (simp add:Endpoint_D.send_fault_ipc_def Ipc_A.send_fault_ipc_def)
   apply (rule dcorres_expand_pfx)
   apply (rule corres_guard_imp)
-    apply (rule_tac P'="(=s')" in thread_get_corresE[where tcb' = tcb and etcb'=etcb])
+    apply (rule_tac P'="(=) s'" in thread_get_corresE[where tcb' = tcb and etcb'=etcb])
      apply simp_all
    prefer 2
    apply (rule conjI)
diff --git a/proof/drefine/KHeap_DR.thy b/proof/drefine/KHeap_DR.thy
index 047dcec89..ff733dedb 100644
--- a/proof/drefine/KHeap_DR.thy
+++ b/proof/drefine/KHeap_DR.thy
@@ -22,51 +22,46 @@ lemma nat_bl_to_bin_surj:
   using n_less_equal_power_2[where n=n, folded of_nat_less_iff, simplified]
   apply (rule_tac x="bin_to_bl n (int n)" in exI)
   apply (simp only: bin_bl_bin bintrunc_mod2p)
-  apply (simp add: int_mod_eq')
+  apply simp
   done
 
-lemma
-transform_tcb_slot_0:
+lemma transform_tcb_slot_0:
   "transform_cslot_ptr (a, tcb_cnode_index 0) = (a,tcb_cspace_slot)"
   apply (clarsimp simp:transform_cslot_ptr_def)
   apply (unfold tcb_cspace_slot_def)
   apply (simp add: tcb_cnode_index_def bl_to_bin_def)
-done
+  done
 
-lemma
-transform_tcb_slot_1:
+lemma transform_tcb_slot_1:
   "transform_cslot_ptr (a,tcb_cnode_index 1) = (a,tcb_vspace_slot)"
   apply (clarsimp simp:transform_cslot_ptr_def)
   apply (unfold tcb_vspace_slot_def)
   apply (simp add: tcb_cnode_index_def)
-done
+  done
 
-lemma
-transform_tcb_slot_2:
+lemma transform_tcb_slot_2:
   "transform_cslot_ptr (a,tcb_cnode_index 2) = (a,tcb_replycap_slot)"
   apply (clarsimp simp:transform_cslot_ptr_def)
   apply (unfold tcb_replycap_slot_def)
   apply (simp add: tcb_cnode_index_def)
   apply (simp add:bl_to_bin_def)
-done
+  done
 
-lemma
-transform_tcb_slot_3:
+lemma transform_tcb_slot_3:
   "transform_cslot_ptr (a,tcb_cnode_index 3) = (a,tcb_caller_slot)"
   apply (clarsimp simp:transform_cslot_ptr_def)
   apply (unfold tcb_caller_slot_def)
   apply (simp add: tcb_cnode_index_def)
   apply (simp add:bl_to_bin_def)
-done
+  done
 
-lemma
-transform_tcb_slot_4:
+lemma transform_tcb_slot_4:
   "transform_cslot_ptr (a,tcb_cnode_index 4) = (a,tcb_ipcbuffer_slot)"
   apply (clarsimp simp:transform_cslot_ptr_def)
   apply (unfold tcb_ipcbuffer_slot_def)
   apply (simp add: tcb_cnode_index_def)
   apply (simp add:bl_to_bin_def)
-done
+  done
 
 lemmas transform_tcb_slot_simp =
   transform_tcb_slot_0 transform_tcb_slot_1
@@ -76,10 +71,7 @@ lemmas transform_tcb_slot_simp =
 lemma cap_table_at_cte_wp_at_length:
   "\<lbrakk> cap_table_at n p s; cte_wp_at P (p, p') s \<rbrakk>
         \<Longrightarrow> length p' = n"
-  apply (clarsimp simp: cte_wp_at_cases obj_at_def is_cap_table
-                        well_formed_cnode_n_def length_set_helper)
-  apply auto
-  done
+  by (auto simp: cte_wp_at_cases obj_at_def is_cap_table well_formed_cnode_n_def length_set_helper)
 
 context
 begin
@@ -248,10 +240,10 @@ lemma get_cur_thread_corres:
      (gets_the cdl_current_thread)
      (gets cur_thread)"
   apply (simp add:gets_the_def gets_def)
-    apply (rule dcorres_absorb_get_l)
-    apply (rule dcorres_absorb_get_r)
-    apply (clarsimp simp:assert_opt_def transform_def transform_current_thread_def)
-    apply (simp add:corres_underlying_def not_idle_thread_def)
+  apply (rule dcorres_absorb_get_l)
+  apply (rule dcorres_absorb_get_r)
+  apply (clarsimp simp:assert_opt_def transform_def transform_current_thread_def)
+  apply (simp add:corres_underlying_def not_idle_thread_def)
   done
 
 lemma not_in_dom_dest:
@@ -266,18 +258,17 @@ lemma nat_to_bl_dest:
   "b\<in>Collect (%x. length x= n)\<Longrightarrow> nat_to_bl n (nat (bl_to_bin b)) = Some b"
   apply (unfold nat_to_bl_def)
   apply (subgoal_tac "0 \<le> bl_to_bin b")
-  apply (subst nat_0_le)
+   apply (subst nat_0_le)
     apply simp
-    apply (subgoal_tac "length b = n")
+   apply (subgoal_tac "length b = n")
     apply (erule subst[where s="length b" and t=n])
     apply (subst bl_bin_bl)
     apply (simp add: not_le)
-    apply (simp add: nat_less_iff[OF bl_to_bin_ge0])
     apply (clarsimp simp: bl_to_bin_lt2p)
-  apply clarsimp
+   apply clarsimp
   apply (simp add:not_less)
   apply (rule bl_to_bin_ge0)
-done
+  done
 
 lemma bl_to_bin_tcb_cnode_index_le0:
   "n < 8 \<Longrightarrow> (bl_to_bin (tcb_cnode_index n) \<le> 0) = (n = 0)"
@@ -346,7 +337,7 @@ lemma get_cap_no_fail:
   done
 
 lemma get_cap_helper:
-  "dcorres r P (P') f (get_cap slot >>= g) \<Longrightarrow> dcorres r P (P' and (cte_wp_at ((=cap)) slot)) f  (g cap)"
+  "dcorres r P (P') f (get_cap slot >>= g) \<Longrightarrow> dcorres r P (P' and (cte_wp_at ((=) cap) slot)) f  (g cap)"
   by (clarsimp simp:bind_def corres_underlying_def cte_wp_at_def)
 
 lemma get_cap_corres:
@@ -390,11 +381,7 @@ lemma nat2p: "nat (2^(x::nat)) = 2^(x::nat)"
 
 lemma nat_to_bl_to_bin:
   "nat_to_bl bits n = Some xs \<Longrightarrow> n = nat (bl_to_bin xs)"
-  apply (clarsimp simp:nat_to_bl_def bin_bl_bin' bintrunc_mod2p)
-  apply (subst mod_pos_pos_trivial,simp_all)
-  apply (rule iffD1[OF zless_nat_eq_int_zless])
-  apply (simp add:nat2p)
-  done
+  by (clarsimp simp:nat_to_bl_def bin_bl_bin' bintrunc_mod2p)
 
 lemma cap_counts_inv:
 assumes "\<And>cap. P cap\<Longrightarrow> cap_counts cap"
@@ -2728,7 +2715,7 @@ lemma set_parent_corres:
   done
 
 lemma set_tcb_capslot_weak_valid_mdb:
-  "\<lbrace>weak_valid_mdb and cte_wp_at ((=cap.NullCap)) slot\<rbrace> set_cap cap slot \<lbrace>\<lambda>r s. weak_valid_mdb s\<rbrace> "
+  "\<lbrace>weak_valid_mdb and cte_wp_at ((=) cap.NullCap) slot\<rbrace> set_cap cap slot \<lbrace>\<lambda>r s. weak_valid_mdb s\<rbrace> "
   apply (simp add: weak_valid_mdb_def cte_wp_at_caps_of_state swp_def)
   apply (wp set_cap_caps_of_state2)
   apply (case_tac slot)
@@ -2742,7 +2729,7 @@ lemma get_tcb_reply_cap_wp_cte_at:
     \<lbrace>\<lambda>rv. cte_wp_at ((\<noteq>) cap.NullCap) (obj_ref_of rv, tcb_cnode_index 2)\<rbrace>"
   apply (rule hoare_post_imp
      [where Q="\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid,tcb_cnode_index 2)
-       and tcb_at sid and valid_objs and cte_wp_at ((=r)) (sid,tcb_cnode_index 2)"])
+       and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"])
    apply clarsimp
    apply (frule cte_wp_tcb_cap_valid)
     apply simp+
@@ -2756,51 +2743,51 @@ lemma get_tcb_reply_cap_wp_master_cap:
     \<lbrace>\<lambda>rv s. (is_master_reply_cap rv)  \<rbrace>"
   apply (rule hoare_post_imp
      [where Q="\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid,tcb_cnode_index 2)
-       and tcb_at sid and valid_objs and cte_wp_at ((=r)) (sid,tcb_cnode_index 2)"])
+       and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"])
    apply clarsimp
    apply (frule cte_wp_tcb_cap_valid)
     apply simp+
    apply (clarsimp simp :cte_wp_at_def tcb_cap_valid_def st_tcb_at_def obj_at_def is_master_reply_cap_def split:cap.splits)
   apply (wp get_cap_cte_wp_at_rv)
-     apply (clarsimp simp:cte_wp_at_def)+
+  apply (clarsimp simp:cte_wp_at_def)+
   done
 
 lemma get_tcb_reply_cap_wp_original_cap:
     "\<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid,tcb_cnode_index 2) and valid_mdb \<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2)
     \<lbrace>\<lambda>rv s. is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)\<rbrace>"
-   apply (rule hoare_post_imp
+  apply (rule hoare_post_imp
      [where Q="\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid,tcb_cnode_index 2) and valid_mdb
-       and tcb_at sid and valid_objs and cte_wp_at ((=r)) (sid,tcb_cnode_index 2)"])
+       and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"])
    apply clarsimp
    apply (subgoal_tac "is_master_reply_cap r \<and> obj_ref_of r = sid")
-     apply clarsimp
-     apply (frule cte_wp_tcb_cap_valid)
+    apply clarsimp
+    apply (frule cte_wp_tcb_cap_valid)
      apply simp+
-     apply (clarsimp simp:valid_mdb_def reply_master_revocable_def)
-     apply (drule_tac x = "obj_ref_of r" in spec)
-     apply (drule_tac x = "tcb_cnode_index 2" in spec)
-     apply (drule_tac x = r in spec)
-     apply (drule iffD1[OF cte_wp_at_caps_of_state])+
-     apply clarsimp
+    apply (clarsimp simp:valid_mdb_def reply_master_revocable_def)
+    apply (drule_tac x = "obj_ref_of r" in spec)
+    apply (drule_tac x = "tcb_cnode_index 2" in spec)
+    apply (drule_tac x = r in spec)
+    apply (drule iffD1[OF cte_wp_at_caps_of_state])+
+    apply clarsimp
    apply (frule cte_wp_tcb_cap_valid)
-     apply (clarsimp simp :cte_wp_at_def tcb_cap_valid_def st_tcb_at_def obj_at_def is_master_reply_cap_def split:cap.splits)+
-   apply (wp get_cap_cte_wp_at_rv)
-     apply (clarsimp simp:cte_wp_at_def)+
-done
+    apply (clarsimp simp :cte_wp_at_def tcb_cap_valid_def st_tcb_at_def obj_at_def is_master_reply_cap_def split:cap.splits)+
+  apply (wp get_cap_cte_wp_at_rv)
+  apply (clarsimp simp:cte_wp_at_def)+
+  done
 
 lemma get_tcb_reply_cap_wp_obj_ref:
     "\<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid,tcb_cnode_index 2) \<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2)
     \<lbrace>\<lambda>rv s. (obj_ref_of rv = sid) \<rbrace>"
-   apply (rule hoare_post_imp
+  apply (rule hoare_post_imp
      [where Q="\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid,tcb_cnode_index 2)
-       and tcb_at sid and valid_objs and cte_wp_at ((=r)) (sid,tcb_cnode_index 2)"])
+       and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"])
    apply clarsimp
    apply (frule cte_wp_tcb_cap_valid)
-   apply simp+
+    apply simp+
    apply (clarsimp simp :cte_wp_at_def tcb_cap_valid_def st_tcb_at_def obj_at_def is_master_reply_cap_def split:cap.splits)
-   apply (wp get_cap_cte_wp_at_rv)
-     apply (clarsimp simp:cte_wp_at_def)+
-done
+  apply (wp get_cap_cte_wp_at_rv)
+  apply (clarsimp simp:cte_wp_at_def)+
+  done
 
 lemma tcb_reply_cap_cte_wp_at:
   "\<lbrakk>valid_objs s;st_tcb_at (\<lambda>r. \<not> inactive r \<and> \<not> idle r) sid s\<rbrakk>
@@ -3104,7 +3091,7 @@ lemma resolve_address_bits_error_corres:
      \<not> in_recursive_branch ref cap;
      cap = cap.CNodeCap oref radix_bits guard;
      valid_cap cap s;valid_idle s;length ref \<le> 32;valid_objs s\<rbrakk>
-    \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. (fst r) = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) \<top> ((=s))
+    \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. (fst r) = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) \<top> ((=) s)
     ( CSpace_D.resolve_address_bits (cap') (of_bl ref) (length ref) )
     ( CSpace_A.resolve_address_bits (cap,ref) )"
   apply (subst KHeap_DR.resolve_address_bits.simps)
@@ -3148,7 +3135,7 @@ lemma resolve_address_bits_error_corres:
 
 lemma resolve_address_bits_terminate_corres:
   "\<lbrakk>in_terminate_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap'=transform_cap cap; valid_cap cap s;valid_idle s;length ref \<le> 32;valid_objs s\<rbrakk>
-      \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) \<top> ((=s))
+      \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) \<top> ((=) s)
     ( CSpace_D.resolve_address_bits cap' (of_bl ref) (length ref) )
     ( CSpace_A.resolve_address_bits (cap,ref) )"
   apply (subst KHeap_DR.resolve_address_bits.simps,frule resolve_address_bits_terminate_branch[where 'a=det_ext],fastforce)
@@ -3364,8 +3351,6 @@ lemma dcorres_injection_handler_rhs:
      apply (clarsimp simp:throwError_def return_def corres_underlying_def)+
   done
 
-crunch valid_etcbs[wp]: resolve_address_bits "valid_etcbs"
-
 lemma not_idle_thread_resolve_address_bits:
   "\<lbrace>valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread and valid_etcbs\<rbrace>
     CSpace_A.resolve_address_bits (tcb_ctable obj, blist)
diff --git a/proof/drefine/Lemmas_D.thy b/proof/drefine/Lemmas_D.thy
index b4cfce903..6f78d0aca 100644
--- a/proof/drefine/Lemmas_D.thy
+++ b/proof/drefine/Lemmas_D.thy
@@ -17,7 +17,7 @@
 
 theory Lemmas_D
 imports
-  Include_D
+  "DBaseRefine.Include_D"
   MoreHOL
   MoreCorres
   "ExecSpec.InvocationLabels_H"
diff --git a/proof/drefine/StateTranslationProofs_DR.thy b/proof/drefine/StateTranslationProofs_DR.thy
index 9ba812323..34f818c27 100644
--- a/proof/drefine/StateTranslationProofs_DR.thy
+++ b/proof/drefine/StateTranslationProofs_DR.thy
@@ -119,7 +119,7 @@ lemma transform_full_intent_cong:
   by (simp add: transform_full_intent_def get_tcb_message_info_def get_tcb_mrs_def Suc_le_eq get_ipc_buffer_words_def)
 
 lemma caps_of_state_eq_lift:
-    "\<forall>cap. cte_wp_at ((=cap)) p s = cte_wp_at ((=cap)) p s' \<Longrightarrow>  caps_of_state s p = caps_of_state s' p"
+  "\<forall>cap. cte_wp_at ((=) cap) p s = cte_wp_at ((=) cap) p s' \<Longrightarrow>  caps_of_state s p = caps_of_state s' p"
   apply (simp add:cte_wp_at_def caps_of_state_def)
   done
 
@@ -134,9 +134,9 @@ lemma caps_of_state_irrelavent_simp:
 fun
    caps_of_object :: "kernel_object \<Rightarrow> (bool list \<rightharpoonup> cap)"
 where
-  "caps_of_object (Structures_A.CNode sz c) = (if well_formed_cnode_n sz c then c else empty)"
+    "caps_of_object (Structures_A.CNode sz c) = (if well_formed_cnode_n sz c then c else Map.empty)"
   | "caps_of_object (Structures_A.TCB t) = (\<lambda>n. option_map (\<lambda>(f, _). f t) (tcb_cap_cases n))"
-  | "caps_of_object _                    = empty"
+  | "caps_of_object _                    = Map.empty"
 
 lemma caps_of_state_def2:
   "caps_of_state s = (\<lambda>ptr. case (option_map caps_of_object (kheap s (fst ptr))) of
diff --git a/proof/drefine/Syscall_DR.thy b/proof/drefine/Syscall_DR.thy
index b68169f39..240412982 100644
--- a/proof/drefine/Syscall_DR.thy
+++ b/proof/drefine/Syscall_DR.thy
@@ -258,7 +258,7 @@ lemma decode_domain_corres:
 
 lemma decode_domain_cap_label_not_match:
   "\<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'\<rbrakk>
-    \<Longrightarrow> \<lbrace>(=s\<rbrace>Decode_A.decode_domain_invocation) label' args' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=s\<rbrace>)"
+    \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>"
   apply (case_tac "invocation_type label' = DomainSetSet")
    apply (clarsimp simp: Decode_A.decode_domain_invocation_def transform_intent_def)+
    apply (clarsimp simp: transform_intent_domain_def split: option.splits list.splits)
diff --git a/proof/drefine/Tcb_DR.thy b/proof/drefine/Tcb_DR.thy
index 7a4e1b224..1715bf506 100644
--- a/proof/drefine/Tcb_DR.thy
+++ b/proof/drefine/Tcb_DR.thy
@@ -190,7 +190,7 @@ lemma decode_set_space_translate_tcb_invocation:
 
 lemma decode_tcb_cap_label_not_match:
   "\<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = Structures_A.ThreadCap t\<rbrakk>
-    \<Longrightarrow> \<lbrace>(=s\<rbrace>Decode_A.decode_tcb_invocation) label' args' cap' slot' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=s\<rbrace>)"
+    \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_tcb_invocation label' args' cap' slot' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>"
   apply (simp add:Decode_A.decode_tcb_invocation_def)
   apply (case_tac "invocation_type label'")
     apply (simp_all add:transform_intent_def)