option_map_def -> map_option_case for 2014-RC0

proof/access-control/Dpolicy.thy

@@ -219,7 +219,7 @@ abbreviation
 lemma transform_asid_rev_transform_mapping [simp]:
   "valid_asid_mapping mapping \<Longrightarrow>
    transform_asid_rev ` set_option (transform_mapping mapping) = fst ` set_option mapping"
-  apply (simp add:transform_mapping_def option_map_def)
+  apply (simp add:transform_mapping_def map_option_case)
   apply (case_tac mapping)
    apply clarsimp+
   done

proof/crefine/CSpace_C.thy

@@ -119,7 +119,7 @@ lemma Arch_maskCapRights_ccorres [corres]:
     apply (unfold ccap_relation_def)[1] 
     apply (simp add: cap_small_frame_cap_lift [THEN iffD1])
     apply (clarsimp simp: cap_to_H_def)
-    apply (simp add: option_map_def split: option.splits)
+    apply (simp add: map_option_case split: option.splits)
     apply (clarsimp simp add: cap_to_H_def Let_def split: cap_CL.splits split_if_asm)
        apply (simp add: cap_small_frame_cap_lift_def) 
        apply (simp add: ccap_rights_relation_def)
@@ -141,7 +141,7 @@ lemma Arch_maskCapRights_ccorres [corres]:
       apply (unfold ccap_relation_def)[1] 
       apply (simp add: cap_frame_cap_lift [THEN iffD1])
       apply (clarsimp simp: cap_to_H_def)
-      apply (simp add: option_map_def split: option.splits)
+      apply (simp add: map_option_case split: option.splits)
       apply (clarsimp simp add: isCap_simps pageSize_def cap_to_H_def Let_def
                          split: cap_CL.splits split_if_asm)
        apply (simp add: cap_frame_cap_lift_def) 
@@ -267,7 +267,7 @@ lemma maskCapRights_ccorres [corres]:
             apply (unfold ccap_relation_def)[1]
             apply (simp add: cap_async_endpoint_cap_lift [THEN iffD1])
             apply (clarsimp simp: cap_to_H_def)
-            apply (simp add: option_map_def split: option.splits)
+            apply (simp add: map_option_case split: option.splits)
             apply (clarsimp simp add: cap_to_H_def Let_def
                                split: cap_CL.splits split_if_asm)
             apply (simp add: cap_async_endpoint_cap_lift_def)
@@ -303,7 +303,7 @@ lemma maskCapRights_ccorres [corres]:
           apply (unfold ccap_relation_def)[1]
           apply (simp add: cap_endpoint_cap_lift [THEN iffD1])
           apply (clarsimp simp: cap_to_H_def)
-          apply (simp add: option_map_def split: option.splits)
+          apply (simp add: map_option_case split: option.splits)
           apply (clarsimp simp add: cap_to_H_def Let_def
                              split: cap_CL.splits split_if_asm)
           apply (simp add: cap_endpoint_cap_lift_def)
@@ -2711,7 +2711,7 @@ lemma Arch_sameRegionAs_spec:
        apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(13))
        apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(13))
        apply (frule cap_get_tag_isCap_unfolded_H_cap)
-       apply (simp add: ccap_relation_def  option_map_def)
+       apply (simp add: ccap_relation_def  map_option_case)
        apply (simp add: cap_asid_pool_cap_lift)
        apply (simp add: cap_to_H_def)
        apply (case_tac "capASIDPool_CL (cap_asid_pool_cap_lift cap_a) = 
@@ -2905,7 +2905,7 @@ lemma Arch_sameRegionAs_spec:
    apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(14))
    apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(14))
    apply (frule cap_get_tag_isCap_unfolded_H_cap)
-   apply (simp add: ccap_relation_def  option_map_def)
+   apply (simp add: ccap_relation_def  map_option_case)
    apply (simp add: cap_page_table_cap_lift)
    apply (simp add: cap_to_H_def)
    apply (case_tac "capPTBasePtr_CL (cap_page_table_cap_lift cap_a) = 
@@ -2924,7 +2924,7 @@ lemma Arch_sameRegionAs_spec:
   apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(15))
   apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(15))
   apply (frule cap_get_tag_isCap_unfolded_H_cap)
-  apply (simp add: ccap_relation_def  option_map_def)
+  apply (simp add: ccap_relation_def  map_option_case)
   apply (simp add: cap_page_directory_cap_lift)
   apply (simp add: cap_to_H_def)
   apply (case_tac "capPDBasePtr_CL (cap_page_directory_cap_lift cap_a) = 
@@ -3094,7 +3094,7 @@ lemma ccap_relation_get_capSizeBits_untyped:
    get_capSizeBits_CL (cap_lift ccap) = bits"
   apply (frule cap_get_tag_isCap_unfolded_H_cap)
   apply (clarsimp simp: get_capSizeBits_CL_def ccap_relation_def
-                        option_map_def cap_to_H_def cap_lift_def cap_tag_defs)
+                        map_option_case cap_to_H_def cap_lift_def cap_tag_defs)
   done
 
 definition
@@ -3282,7 +3282,7 @@ lemma ccap_relation_get_capPtr_untyped:
    get_capPtr_CL (cap_lift ccap) = Ptr word"
   apply (frule cap_get_tag_isCap_unfolded_H_cap)
   apply (clarsimp simp: get_capPtr_CL_def ccap_relation_def
-                        option_map_def cap_to_H_def cap_lift_def cap_tag_defs)
+                        map_option_case cap_to_H_def cap_lift_def cap_tag_defs)
   done
 
 lemma cap_get_tag_isArchCap_unfolded_H_cap:
@@ -3314,7 +3314,7 @@ lemma sameRegionAs_spec:
                           isCap_simps cap_tag_defs from_bool_def false_def)[1]
               apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(1))
               apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(1))
-              apply (simp add: ccap_relation_def option_map_def)
+              apply (simp add: ccap_relation_def map_option_case)
               apply (simp add: cap_thread_cap_lift)
               apply (simp add: cap_to_H_def)
              apply (clarsimp simp: bool_case_If ctcb_ptr_to_tcb_ptr_def if_distrib
@@ -3328,7 +3328,7 @@ lemma sameRegionAs_spec:
                         isCap_simps cap_tag_defs from_bool_def false_def)[1]
             apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(3))
             apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(3))
-            apply (simp add: ccap_relation_def option_map_def)
+            apply (simp add: ccap_relation_def map_option_case)
             apply (simp add: cap_async_endpoint_cap_lift)
             apply (simp add: cap_to_H_def)
             apply (clarsimp split: split_if)
@@ -3339,7 +3339,7 @@ lemma sameRegionAs_spec:
                       isCap_simps cap_tag_defs from_bool_def false_def)[1]
            apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(5))
            apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(5))
-           apply (simp add: ccap_relation_def option_map_def)
+           apply (simp add: ccap_relation_def map_option_case)
            apply (simp add: cap_irq_handler_cap_lift)
            apply (simp add: cap_to_H_def)
            apply (clarsimp simp: up_ucast_inj_eq c_valid_cap_def
@@ -3354,7 +3354,7 @@ lemma sameRegionAs_spec:
                       isCap_simps cap_tag_defs from_bool_def false_def)[1]
           apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(4))
           apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(4))
-          apply (simp add: ccap_relation_def option_map_def)
+          apply (simp add: ccap_relation_def map_option_case)
           apply (simp add: cap_endpoint_cap_lift)
           apply (simp add: cap_to_H_def)
           apply (clarsimp split: split_if)
@@ -3383,7 +3383,7 @@ lemma sameRegionAs_spec:
       apply (clarsimp simp: isArchCap_tag_def2)     
      apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(8))
      apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(8))
-     apply (simp add: ccap_relation_def option_map_def)
+     apply (simp add: ccap_relation_def map_option_case)
      apply (simp add: cap_reply_cap_lift)
      apply (simp add: cap_to_H_def ctcb_ptr_to_tcb_ptr_def)
      apply (clarsimp split: split_if)
@@ -3410,7 +3410,7 @@ lemma sameRegionAs_spec:
                           ccap_relation_get_capSizeBits_physical
                           ccap_relation_get_capSizeBits_untyped)
     apply (intro conjI impI)
-       apply ((clarsimp simp: ccap_relation_def option_map_def
+       apply ((clarsimp simp: ccap_relation_def map_option_case
                               cap_untyped_cap_lift cap_to_H_def
                               field_simps valid_cap'_def)+)[4]
     apply (case_tac "capClass capb = PhysicalClass")
@@ -3429,7 +3429,7 @@ lemma sameRegionAs_spec:
     apply (clarsimp simp: isArchCap_tag_def2)     
    apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(10))
    apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(10))
-   apply (simp add: ccap_relation_def option_map_def)
+   apply (simp add: ccap_relation_def map_option_case)
    apply (simp add: cap_cnode_cap_lift)
    apply (simp add: cap_to_H_def)
    apply (clarsimp split: split_if bool.split)
@@ -3487,7 +3487,7 @@ lemma Arch_sameObjectAs_spec:
                             false_def from_bool_def)[1]
        apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(16), simp)
        apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(16), simp)
-       apply (simp add: ccap_relation_def option_map_def)
+       apply (simp add: ccap_relation_def map_option_case)
        apply (simp add: cap_small_frame_cap_lift)
        apply (clarsimp simp: cap_to_H_def capAligned_def from_bool_def
                       split: split_if bool.split
@@ -3497,7 +3497,7 @@ lemma Arch_sameObjectAs_spec:
                            false_def from_bool_def)[1]
       apply (frule_tac cap'=cap_a in cap_get_tag_isCap_unfolded_H_cap(17), simp)
       apply (frule_tac cap'=cap_b in cap_get_tag_isCap_unfolded_H_cap(17), simp)
-      apply (simp add: ccap_relation_def option_map_def)
+      apply (simp add: ccap_relation_def map_option_case)
       apply (simp add: cap_frame_cap_lift)
       apply (clarsimp simp: cap_to_H_def capAligned_def from_bool_def
                             c_valid_cap_def cl_valid_cap_def
@@ -3552,7 +3552,7 @@ lemma sameRegionAs_EndpointCap:
          simp_all add: isUntypedCap_def isEndpointCap_def isAsyncEndpointCap_def
              isCNodeCap_def isThreadCap_def isReplyCap_def isIRQControlCap_def
              isIRQHandlerCap_def isArchObjectCap_def)
-  apply (clarsimp simp: ccap_relation_def option_map_def)
+  apply (clarsimp simp: ccap_relation_def map_option_case)
   apply (case_tac "cap_lift capc", simp_all)
   apply (simp add: cap_to_H_def)
   apply (case_tac a, simp_all)
@@ -3575,7 +3575,7 @@ lemma sameRegionAs_AsyncEndpointCap:
          simp_all add: isUntypedCap_def isEndpointCap_def isAsyncEndpointCap_def
              isCNodeCap_def isThreadCap_def isReplyCap_def isIRQControlCap_def
              isIRQHandlerCap_def isArchObjectCap_def)
-  apply (clarsimp simp: ccap_relation_def option_map_def)
+  apply (clarsimp simp: ccap_relation_def map_option_case)
   apply (case_tac "cap_lift capc", simp_all)
   apply (simp add: cap_to_H_def)
   apply (case_tac a, simp_all)
@@ -3605,7 +3605,7 @@ lemma isMDBParentOf_spec:
 
   apply (rule conjI, clarsimp simp: typ_heap_simps dest!: lift_t_g)
   apply (intro conjI impI)
-     apply (simp add: ccte_relation_def option_map_def)
+     apply (simp add: ccte_relation_def map_option_case)
      apply (simp add: cte_lift_def)
      apply (clarsimp simp: cte_to_H_def mdb_node_to_H_def split: option.split_asm)
      apply (clarsimp simp: Let_def false_def from_bool_def to_bool_def
@@ -3617,7 +3617,7 @@ lemma isMDBParentOf_spec:
   apply (rule_tac x="cteCap cteb" in exI, rule conjI)
    apply (clarsimp simp: ccte_relation_ccap_relation typ_heap_simps
                   dest!: lift_t_g)
-  apply (clarsimp simp: ccte_relation_def option_map_def)
+  apply (clarsimp simp: ccte_relation_def map_option_case)
   apply (simp add: cte_lift_def)
   apply (clarsimp simp: cte_to_H_def mdb_node_to_H_def
                  split: option.split_asm)

proof/crefine/Finalise_C.thy

@@ -119,7 +119,7 @@ lemma ep_queue_relation_shift:
    apply simp
   apply simp
   apply (simp add: option_map2_def fun_eq_iff
-                   option_map_def)
+                   map_option_case)
   apply (drule_tac x=qHead in spec)+
   apply (clarsimp split: option.split_asm)
   done

proof/crefine/Ipc_C.thy

@@ -3449,7 +3449,7 @@ lemma lookupIPCBuffer_ccorres [corres]:
                            split: split_if_asm split del: split_if)
             apply (frule(1) cap_get_tag_isCap_unfolded_H_cap(17))
             apply (frule capFVMRights_range)
-            apply (clarsimp simp: ccap_relation_def option_map_def
+            apply (clarsimp simp: ccap_relation_def map_option_case
                            split: option.splits)
             apply (simp add: cap_frame_cap_lift
                              generic_frame_cap_get_capFVMRights_CL_def)
@@ -3469,7 +3469,7 @@ lemma lookupIPCBuffer_ccorres [corres]:
         apply (clarsimp simp: pageSize_def option_to_0_def isCap_simps
                        split: split_if_asm)
         apply (frule(1) cap_get_tag_isCap_unfolded_H_cap(17))
-        apply (clarsimp simp: ccap_relation_def option_map_def
+        apply (clarsimp simp: ccap_relation_def map_option_case
                        split: option.splits)
         apply (simp add: cap_frame_cap_lift
                          generic_frame_cap_get_capFSize_CL_def
@@ -3489,7 +3489,7 @@ lemma lookupIPCBuffer_ccorres [corres]:
                           split: split_if_asm split del: split_if)
            apply (frule cap_get_tag_isCap_unfolded_H_cap(16), simp)
            apply (frule capFVMRights_range)
-           apply (clarsimp simp: ccap_relation_def option_map_def
+           apply (clarsimp simp: ccap_relation_def map_option_case
                           split: option.splits)
            apply (simp add: cap_small_frame_cap_lift
                             generic_frame_cap_get_capFVMRights_CL_def)
@@ -3509,7 +3509,7 @@ lemma lookupIPCBuffer_ccorres [corres]:
        apply (clarsimp simp: pageSize_def option_to_0_def isCap_simps
                       split: split_if_asm)
        apply (frule cap_get_tag_isCap_unfolded_H_cap(16), simp)
-       apply (clarsimp simp: ccap_relation_def option_map_def
+       apply (clarsimp simp: ccap_relation_def map_option_case
                       split: option.splits)
        apply (simp add: cap_small_frame_cap_lift
                         generic_frame_cap_get_capFSize_CL_def

proof/crefine/Refine_C.thy

@@ -964,7 +964,7 @@ lemma monadic_rewrite_\<Gamma>:
   using spec_refine
         spec_simulates_to_exec_simulates
   apply (simp add: spec_statefn_simulates_via_statefn
-                   o_def option_map_def)
+                   o_def map_option_case)
   apply (clarsimp simp: monadic_rewrite_def exec_C_def image_def)
   apply blast
   done

proof/crefine/SR_lemmas_C.thy

@@ -59,7 +59,7 @@ lemma cteMDBNode_C_update_lift [simp]:
 
 lemma ccap_relationE:
   "\<lbrakk>ccap_relation c v; \<And>vl. \<lbrakk> cap_lift v = Some vl; c = cap_to_H vl; c_valid_cap v\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
-  unfolding ccap_relation_def option_map_def 
+  unfolding ccap_relation_def map_option_case 
   apply clarsimp
   apply (drule sym)
   apply (clarsimp split: option.splits)

proof/crefine/StoreWord_C.thy

@@ -424,7 +424,7 @@ proof (intro allI impI)
     apply clarsimp
     apply (subgoal_tac "Some v = heap_to_page_data (ksPSpace \<sigma>)
                              (underlying_memory (ksMachineState \<sigma>)) x")
-     apply (clarsimp simp: heap_to_page_data_def Let_def option_map_def
+     apply (clarsimp simp: heap_to_page_data_def Let_def map_option_case
                     split: option.split_asm)
      apply (fastforce simp: cmap_relation_def dest: bspec)
     apply (clarsimp simp: heap_to_page_data_def Let_def)

proof/drefine/StateTranslationProofs_DR.thy

@@ -202,7 +202,7 @@ lemma transform_objects_update_kheap_same_caps:
          (transform_objects (update_kheap kh s))(ptr \<mapsto> transform_object (machine_state s) ptr (ekheap s ptr) ko'))"
   unfolding transform_objects_def
   apply (rule ext)
-  apply (simp add: option_map_def restrict_map_def map_add_def )
+  apply (simp add: map_option_case restrict_map_def map_add_def )
   done
 
 lemma transform_objects_update_same:

proof/drefine/Untyped_DR.thy

@@ -25,7 +25,7 @@ lemma detype_dcorres:
   apply (simp add: Untyped_D.detype_def transform_def
                    transform_current_thread_def Retype_A.detype_def transform_asid_table_def detype_ext_def)
   apply (rule ext)
-  apply (clarsimp simp: option_map_def restrict_map_def transform_objects_def
+  apply (clarsimp simp: map_option_case restrict_map_def transform_objects_def
                         map_add_def cte_wp_at_caps_of_state
                  split: option.split)
   apply (drule valid_global_refsD2)

proof/refine/CSpace_R.thy

@@ -6632,7 +6632,7 @@ lemma revokable:
    apply (simp add: n_def n'_def modify_map_apply)
    apply (simp add: modify_map_def const_def split: split_if_asm)
   apply (clarsimp simp: n_def)
-  apply (clarsimp simp add: modify_map_def option_map_def split: split_if_asm option.splits)
+  apply (clarsimp simp add: modify_map_def map_option_case split: split_if_asm option.splits)
      apply (case_tac aa, clarsimp, erule revokable_n')
     apply (case_tac a, clarsimp, erule revokable_n')
    apply (case_tac a, clarsimp, erule revokable_n')
@@ -6657,7 +6657,7 @@ lemma badge_n:
    apply (simp add: n_def n'_def modify_map_apply)
    apply (simp add: modify_map_def const_def split: split_if_asm)
   apply (clarsimp simp: n_def)
-  apply (clarsimp simp add: modify_map_def option_map_def split: split_if_asm option.splits)
+  apply (clarsimp simp add: modify_map_def map_option_case split: split_if_asm option.splits)
      apply (case_tac aa, clarsimp, erule badge_n')
     apply (case_tac a, clarsimp, erule badge_n')
    apply (case_tac a, clarsimp, erule badge_n')
@@ -11460,7 +11460,7 @@ lemma updateMDB_ctes_of_cases:
      updateMDB p f \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>"
   apply (simp add: updateMDB_def split del: split_if)
   apply (rule hoare_pre, wp getCTE_ctes_of)
-  apply (clarsimp simp: modify_map_def option_map_def
+  apply (clarsimp simp: modify_map_def map_option_case
                  split: option.split
           | rule conjI ext | erule rsubst[where P=P])+
   apply (case_tac y, simp)

proof/refine/Finalise_R.thy

@@ -2510,7 +2510,7 @@ lemma ipcCancel_cteCaps_of:
   apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def)
   apply (drule_tac x="mdbNext (cteMDBNode x)" in spec)
   apply clarsimp
-  apply (auto simp: o_def option_map_def fun_upd_def[symmetric])
+  apply (auto simp: o_def map_option_case fun_upd_def[symmetric])
   done
 
 lemma ipcCancel_cte_wp_at':

proof/refine/Invariants_H.thy

@@ -1697,7 +1697,7 @@ lemma lookupAround2_None2:
   "(snd (lookupAround2 x s) = None) = (\<forall>y. x < y \<longrightarrow> s y = None)"
   apply (simp add: lookupAround2_def Let_def split_def del: maybe_def
                split: option.splits)
-  apply (simp add: o_def option_map_is_None [where f=fst, unfolded option_map_def])
+  apply (simp add: o_def option_map_is_None [where f=fst, unfolded map_option_case])
   apply (simp add: lookupAround_def Let_def)
   apply fastforce
   done
@@ -1707,7 +1707,7 @@ lemma lookupAround2_char2:
   apply (simp add: lookupAround2_def Let_def split_def o_def
               del: maybe_def
               split: option.splits)
-  apply (simp add: o_def option_map_is_None [where f=fst, unfolded option_map_def])
+  apply (simp add: o_def option_map_is_None [where f=fst, unfolded map_option_case])
   apply (simp add: lookupAround_def Let_def)
   apply (rule conjI)
    apply fastforce

proof/refine/Ipc_R.thy

@@ -1851,7 +1851,7 @@ lemma do_fault_transfer_corres:
     apply (rule corres_assert_opt_assume)
      apply (clarsimp split: option.splits
                       simp: fault_rel_optionation_def assert_opt_def
-                            option_map_def)
+                            map_option_case)
      defer
      defer
      apply (clarsimp simp: fault_rel_optionation_def)