c-parser: update umm_heap/* for 2016

tools/c-parser/umm_heap/Arrays.thy

@@ -313,7 +313,7 @@ next
   fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
   { fix a :: "('a \<times> 'b)['n::finite]" and i
     have "\<lbrakk>set_array a \<subseteq> {(x, y). R x y}; i < CARD('n)\<rbrakk> \<Longrightarrow> R (fst (a.[i])) (snd (a.[i]))"
-      by (meson Collect_splitD in_set_array_index_conv subset_iff)
+      by (meson Collect_case_prodD in_set_array_index_conv subset_iff)
   } note conv1 = this
   { fix a :: "'a['n::finite]" and b :: "'b['n]"
     let ?z = "zip_array a b"

tools/c-parser/umm_heap/ArraysMemInstance.thy

@@ -33,8 +33,10 @@ begin
 instance ..
 end
 
-defs (overloaded)
-  typ_info_array: "typ_info_t (w::('a::c_type,'b::finite) array itself) \<equiv> array_tag w"
+overloading typ_info_array \<equiv> typ_info_t begin
+definition
+  typ_info_array: "typ_info_array (w::('a::c_type,'b::finite) array itself) \<equiv> array_tag w"
+end
 
 lemma field_names_array_tag_length [rule_format]:
   "x \<in> set (field_names_list (array_tag_n n)) \<longrightarrow> length x < n"

tools/c-parser/umm_heap/CTypesBase.thy

@@ -239,7 +239,7 @@ lemma intvl_self_offset:
   shows False
 proof -
   let ?j = "2^len_of TYPE('a) - x"
-  from b have b': "of_nat x + of_nat ?j  = (0::'a::len word)" by simp
+  from b have b': "of_nat x + of_nat ?j  = (0::'a::len word)" using of_nat_2p by auto
   moreover from a b have "?j < n" by arith
   with b b' c show  ?thesis by (force simp: intvl_def)
 qed

tools/c-parser/umm_heap/CTypesDefs.thy

@@ -142,8 +142,8 @@ where
 
 | fa5: "access_ti_pair (DTPair t nm) = access_ti t"
 
-text {* access_ti\<^sub>0 overlays the representation of an object on a
-        list of zero bytes *}
+text \<open>@{text access_ti\<^sub>0} overlays the representation of an object on a
+        list of zero bytes\<close>
 
 definition access_ti\<^sub>0 :: "'a typ_info \<Rightarrow> ('a \<Rightarrow> byte list)" where
   "access_ti\<^sub>0 t \<equiv> \<lambda>v. access_ti t v (replicate (size_td t) 0)"

tools/c-parser/umm_heap/CompoundCTypesEx.thy

@@ -32,9 +32,11 @@ begin
 instance ..
 end
 
-defs (overloaded)
-x_struct_ex_typ_tag: "typ_info_t (t::'a x_struct_ex_ext itself) \<equiv>
+overloading x_struct_ex_typ_tag \<equiv> typ_info_t begin
+definition
+x_struct_ex_typ_tag: "x_struct_ex_typ_tag (t::'a x_struct_ex_ext itself) \<equiv>
     (x_struct_ex_tag::'a x_struct_ex_scheme typ_info)"
+end
 
 
 lemma aggregate_x_struct_ex_tag [simp]:
@@ -132,9 +134,12 @@ begin
 instance ..
 end
 
-defs (overloaded)
-y_struct_ex_typ_tag: "typ_info_t (t::'a y_struct_ex_ext itself) \<equiv>
+overloading y_struct_ex_typ_tag \<equiv> typ_info_t
+begin
+definition
+y_struct_ex_typ_tag: "y_struct_ex_typ_tag (t::'a y_struct_ex_ext itself) \<equiv>
     (y_struct_ex_tag::'a y_struct_ex_scheme typ_info)"
+end
 
 instantiation y_struct_ex_ext :: (unit_class) mem_type
 begin

tools/c-parser/umm_heap/SepFrame.thy

@@ -127,11 +127,17 @@ where
 
 instance state_ext :: (heap_state_type',type) heap_state_type' ..
 
-defs (overloaded)
-  hs_mem_state [simp]: "hst_mem \<equiv> hst_mem \<circ> globals"
-  hs_mem_update_state [simp]: "hst_mem_update \<equiv> globals_update \<circ> hst_mem_update"
-  hs_htd_state[simp]: "hst_htd \<equiv> hst_htd \<circ> globals"
-  hs_htd_update_state [simp]: "hst_htd_update \<equiv> globals_update \<circ> hst_htd_update"
+overloading
+  hs_mem_state \<equiv> hst_mem
+  hs_mem_update_state \<equiv> hst_mem_update
+  hs_htd_state \<equiv> hst_htd
+  hs_htd_update_state \<equiv> hst_htd_update
+begin
+  definition hs_mem_state [simp]: "hs_mem_state \<equiv> hst_mem \<circ> globals"
+  definition hs_mem_update_state [simp]: "hs_mem_update_state \<equiv> globals_update \<circ> hst_mem_update"
+  definition hs_htd_state[simp]: "hs_htd_state \<equiv> hst_htd \<circ> globals"
+  definition hs_htd_update_state [simp]: "hs_htd_update_state \<equiv> globals_update \<circ> hst_htd_update"
+end
 
 instance state_ext :: (heap_state_type,type) heap_state_type
   apply intro_classes

tools/c-parser/umm_heap/StructSupport.thy

@@ -158,8 +158,8 @@ lemmas fl_simps = fl_final_pad fl_ti_pad_combine
 lemma access_ti_props_simps [simp]:
   "\<forall>g x. access_ti (adjust_ti (tag::'a typ_info) (f::'b \<Rightarrow> 'a) g) x = access_ti tag (f x)"
   "\<forall>g x. access_ti_struct (map_td_struct (\<lambda>n algn d. update_desc f g d) (st::'a field_desc typ_struct)) x = access_ti_struct st (f x)"
-  "\<forall>g x. access_ti_list (map_td_list (\<lambda>n algn d. update_desc f g d) (ts\<Colon>('a field_desc typ_desc, char list) dt_pair list)) x = access_ti_list ts (f x)"
-  "\<forall>g x. access_ti_pair (map_td_pair (\<lambda>n algn d. update_desc f g d) (k\<Colon>('a field_desc typ_desc, char list) dt_pair)) x = access_ti_pair k (f x)"
+  "\<forall>g x. access_ti_list (map_td_list (\<lambda>n algn d. update_desc f g d) (ts::('a field_desc typ_desc, char list) dt_pair list)) x = access_ti_list ts (f x)"
+  "\<forall>g x. access_ti_pair (map_td_pair (\<lambda>n algn d. update_desc f g d) (k::('a field_desc typ_desc, char list) dt_pair)) x = access_ti_pair k (f x)"
 unfolding adjust_ti_def
 apply(induct tag and st and ts and k)
      apply (auto simp: update_desc_def)
@@ -235,8 +235,8 @@ lemma field_names_adjust_ti:
   shows
   "wf_fd ti \<longrightarrow> field_names (adjust_ti (ti::'a typ_info) f g) t = field_names ti t"
   "wf_fd_struct st \<longrightarrow> field_names_struct ((map_td_struct (\<lambda>n algn d. update_desc f g d) (st::'a field_desc typ_struct))) t = field_names_struct st t"
-  "wf_fd_list ts \<longrightarrow> field_names_list (map_td_list (\<lambda>n algn d. update_desc f g d) (ts\<Colon>('a field_desc typ_desc, char list) dt_pair list)) t = field_names_list ts t"
-  "wf_fd_pair x \<longrightarrow> field_names_pair (map_td_pair (\<lambda>n algn d. update_desc f g d) (x\<Colon>('a field_desc typ_desc, char list) dt_pair)) t = field_names_pair x t" using assms
+  "wf_fd_list ts \<longrightarrow> field_names_list (map_td_list (\<lambda>n algn d. update_desc f g d) (ts::('a field_desc typ_desc, char list) dt_pair list)) t = field_names_list ts t"
+  "wf_fd_pair x \<longrightarrow> field_names_pair (map_td_pair (\<lambda>n algn d. update_desc f g d) (x::('a field_desc typ_desc, char list) dt_pair)) t = field_names_pair x t" using assms
 apply(induct ti and st and ts and x)
      apply(auto simp: adjust_ti_def)
 done

tools/c-parser/umm_heap/Vanilla32.thy

@@ -26,8 +26,9 @@ definition "unit_tag \<equiv> TypDesc (TypScalar 1 0
 
 declare unit_tag_def [simp]
 
-defs (overloaded)
-  typ_info_unit [simp]: "typ_info_t (x::unit itself) \<equiv> unit_tag"
+overloading typ_info_unit \<equiv> typ_info_t begin
+  definition typ_info_unit [simp]: "typ_info_unit (x::unit itself) \<equiv> unit_tag"
+end
 
 instantiation unit :: mem_type
 begin
@@ -139,12 +140,15 @@ instance signed :: (len8) len8
   apply (metis len8_width len_signed)
   done
 
-defs (overloaded)
-  typ_info_word: "typ_info_t (w::'a::len8 word itself) \<equiv> word_tag w"
-
-defs (overloaded)
-  typ_name_itself_word: "typ_name_itself (w::'a::len8 word itself) \<equiv> typ_name (typ_info_t w)"
+overloading typ_info_word \<equiv> typ_info_t begin
+definition
+  typ_info_word: "typ_info_word (w::'a::len8 word itself) \<equiv> word_tag w"
+end
 
+overloading typ_name_itself_word \<equiv> typ_name_itself begin
+definition
+  typ_name_itself_word: "typ_name_itself_word (w::'a::len8 word itself) \<equiv> typ_name (typ_info_t w)"
+end
 
 lemma align_of_word:
   "align_of TYPE('a::len8 word) = len_of TYPE('a) div 8"
@@ -341,21 +345,26 @@ begin
 instance ..
 end
 
-defs (overloaded)
+overloading typ_info_ptr \<equiv> typ_info_t begin
+definition typ_info_ptr :: "'a::c_type ptr itself \<Rightarrow> 'a::c_type ptr field_desc typ_desc" where
   typ_info_ptr:
-  "typ_info_t (p::'a::c_type ptr itself) \<equiv> TypDesc
+  "typ_info_ptr (p::'a::c_type ptr itself) \<equiv> TypDesc
     (TypScalar 4 2 \<lparr> field_access = \<lambda>p bs. rev (word_rsplit (ptr_val p)),
         field_update = \<lambda>bs v. Ptr (word_rcat (rev bs)::addr) \<rparr> )
     (typ_name_itself TYPE('a) @ ''+ptr'')"
+end
 
-defs (overloaded)
-  typ_name_itself_ptr:
-  "typ_name_itself (p::'a::c_type ptr itself) \<equiv>
-    typ_name_itself TYPE('a) @ ''+ptr''"
+overloading typ_name_itself_ptr \<equiv> typ_name_itself begin
+definition typ_name_itself_ptr:
+  "typ_name_itself_ptr (p::'b::c_type ptr itself) \<equiv>
+    typ_name_itself TYPE('b) @ ''+ptr''"
+end
 
-defs (overloaded)
+overloading typ_name_itself_unit \<equiv> typ_name_itself begin
+definition
   typ_name_itself_unit [simp]:
-  "typ_name_itself (p::unit itself) \<equiv> ''void''"
+  "typ_name_itself_unit (p::unit itself) \<equiv> ''void''"
+end
 
 lemma align_of_ptr [simp]:
   "align_of (p::'a::c_type ptr itself) = 4"