isabelle-2021 cparser: Word_Lib include

Word_Lib was included multiple times in the graph, leading to name
shadowing. This commit makes Addr_Type the single point of entry.

Includes some cleanup/warning reductions.

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

tools/c-parser/PackedTypes.thy

@@ -5,7 +5,7 @@
  *)
 
 theory PackedTypes
-imports "Word_Lib.WordSetup" CProof
+imports CProof
 begin
 
 section \<open>Underlying definitions for the class axioms\<close>

tools/c-parser/umm_heap/ARM/Addr_Type.thy

@@ -7,7 +7,7 @@
 (* License: BSD, terms see file ./LICENSE *)
 
 theory Addr_Type
-imports "HOL-Library.Word"
+imports "Word_Lib.WordSetup"
 begin
 
 type_synonym addr_bitsize = "32"

tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy

@@ -5,7 +5,7 @@
  *)
 
 theory Word_Mem_Encoding
-  imports Vanilla32_Preliminaries "Word_Lib.Rsplit"
+  imports Vanilla32_Preliminaries
 begin
 
 (* Little-endian encoding *)

tools/c-parser/umm_heap/CTypes.thy

@@ -1009,8 +1009,6 @@ lemma fd_cons_access_update_list_append:
   apply(clarsimp simp: fd_cons_access_update_def)
   apply(drule_tac x="take (size_td_list xs) bs" in spec)
   apply clarsimp
-  apply(erule impE)
-   apply(clarsimp simp: min_def)
   apply(simp add: access_ti_append)
   apply(drule_tac x="drop (size_td_list xs) bs" in spec)
   apply clarsimp
@@ -1351,8 +1349,6 @@ lemma wf_lf_fd_cons':
     apply(rotate_tac -4)
     apply(drule_tac x="take (size_td_pair dt_pair) bs" in spec)
     apply clarsimp
-    apply(erule impE)
-     apply(clarsimp simp: min_def split: if_split_asm)
     apply(rotate_tac -1)
     apply(drule_tac x="take (size_td_pair dt_pair) bs'" in spec)
     apply(simp add: min_ll)
@@ -1645,8 +1641,6 @@ lemma wf_fd_cons [rule_format]:
     apply(rotate_tac -4)
     apply(drule_tac x="take (size_td_pair dt_pair) bs" in spec)
     apply clarsimp
-    apply(erule impE)
-     apply(clarsimp simp: min_def split: if_split_asm)
     apply(rotate_tac -1)
     apply(drule_tac x="take (size_td_pair dt_pair) bs'" in spec)
     apply(simp add: min_ll)

tools/c-parser/umm_heap/CTypesBase.thy

@@ -14,8 +14,6 @@
 theory CTypesBase
 imports
   Addr_Type
-  "HOL-Library.Prefix_Order"
-  "Word_Lib.Signed_Words"
 begin
 
 section "Type setup"
@@ -294,8 +292,6 @@ proof -
   show ?thesis unfolding intvl_def by (auto intro!: witness)
 qed
 
-declare of_nat_diff [simp]
-
 lemma intvl_self_offset:
   fixes p::"'a::len word"
   assumes a: "2^len_of TYPE('a) - n < x" and b: "x < 2^len_of TYPE('a)" and

tools/c-parser/umm_heap/TypHeap.thy

@@ -322,7 +322,7 @@ lemma s_footprintD2:
 
 lemma s_footprint_restrict:
   "x \<in> s_footprint p \<Longrightarrow> (s |` s_footprint p) x = s x"
-  by (rule restrict_in)
+  by (fact restrict_in)
 
 lemma restrict_s_fst:
   "fst (restrict_s d X x) \<Longrightarrow> fst (d x)"

tools/c-parser/umm_heap/Vanilla32.thy

@@ -4,14 +4,12 @@
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
-(* License: BSD, terms see file ./LICENSE *)
-
+(* FIXME: rename this theory, not about 32 any more *)
 theory Vanilla32
-imports Word_Mem_Encoding "Word_Lib.Word_Lib_Sumo" CTypes
+imports Word_Mem_Encoding CTypes
 begin
 
 
-
 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"
@@ -294,25 +292,25 @@ lemma align_td_ptr [simp]: "align_td (typ_info_t TYPE('a::c_type ptr)) = addr_al
 lemma ptr_add_word32_signed [simp]:
   fixes a :: "32 word ptr"
   shows "ptr_val (a +\<^sub>p x) = ptr_val a + 4 * of_int x"
-  by (cases a) (simp add: CTypesDefs.ptr_add_def scast_id)
+  by (cases a) (simp add: ptr_add_def)
 
 lemma ptr_add_word32 [simp]:
   fixes a :: "32 word ptr"
   shows "ptr_val (a +\<^sub>p uint x) = ptr_val a + 4 * x"
-  by (cases a) (simp add: ptr_add_def scast_id)
+  by (cases a) simp
 
 lemma ptr_add_word64_signed [simp]:
   fixes a :: "64 word ptr"
   shows "ptr_val (a +\<^sub>p x) = ptr_val a + 8 * of_int x"
-  by (cases a) (simp add: CTypesDefs.ptr_add_def scast_id)
+  by (cases a) (simp add: ptr_add_def)
 
 lemma ptr_add_word64 [simp]:
   fixes a :: "64 word ptr"
   shows "ptr_val (a +\<^sub>p uint x) = ptr_val a + 8 * x"
-  by (cases a) (simp add: ptr_add_def scast_id)
+  by (cases a) (simp add: ptr_add_def)
 
 lemma ptr_add_0_id[simp]:"x +\<^sub>p 0 = x"
-  by (simp add:CTypesDefs.ptr_add_def)
+  by (simp add: ptr_add_def)
 
 lemma from_bytes_ptr_to_bytes_ptr:
   "from_bytes (to_bytes (v::addr_bitsize word) bs) = (Ptr v :: 'a::c_type ptr)"

tools/c-parser/umm_heap/Vanilla32_Preliminaries.thy

@@ -6,6 +6,7 @@
 
 (* License: BSD, terms see file ./LICENSE *)
 
+(* FIXME: rename this theory, it's not about 32 any more *)
 theory Vanilla32_Preliminaries
 imports CTypes
 begin