diff --git a/tools/c-parser/PackedTypes.thy b/tools/c-parser/PackedTypes.thy index 0367e188f..e45fa269e 100644 --- a/tools/c-parser/PackedTypes.thy +++ b/tools/c-parser/PackedTypes.thy @@ -5,7 +5,7 @@ *) theory PackedTypes -imports "Word_Lib.WordSetup" CProof +imports CProof begin section \Underlying definitions for the class axioms\ diff --git a/tools/c-parser/umm_heap/ARM/Addr_Type.thy b/tools/c-parser/umm_heap/ARM/Addr_Type.thy index e115cf155..5ed4eeb57 100644 --- a/tools/c-parser/umm_heap/ARM/Addr_Type.thy +++ b/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" diff --git a/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy index 4feff6cfc..92a20f552 100644 --- a/tools/c-parser/umm_heap/ARM/Word_Mem_Encoding.thy +++ b/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 *) diff --git a/tools/c-parser/umm_heap/CTypes.thy b/tools/c-parser/umm_heap/CTypes.thy index a371a64a0..f53516d5d 100644 --- a/tools/c-parser/umm_heap/CTypes.thy +++ b/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) diff --git a/tools/c-parser/umm_heap/CTypesBase.thy b/tools/c-parser/umm_heap/CTypesBase.thy index 200866d7e..6aadefd96 100644 --- a/tools/c-parser/umm_heap/CTypesBase.thy +++ b/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 diff --git a/tools/c-parser/umm_heap/TypHeap.thy b/tools/c-parser/umm_heap/TypHeap.thy index 2d19ef02f..6bb6d8384 100644 --- a/tools/c-parser/umm_heap/TypHeap.thy +++ b/tools/c-parser/umm_heap/TypHeap.thy @@ -322,7 +322,7 @@ lemma s_footprintD2: lemma s_footprint_restrict: "x \ s_footprint p \ (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) \ fst (d x)" diff --git a/tools/c-parser/umm_heap/Vanilla32.thy b/tools/c-parser/umm_heap/Vanilla32.thy index 1f081de40..d1e40a8f1 100644 --- a/tools/c-parser/umm_heap/Vanilla32.thy +++ b/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 \ typ_info_t begin definition typ_info_word: "typ_info_word (w::'a::len8 word itself) \ 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)" diff --git a/tools/c-parser/umm_heap/Vanilla32_Preliminaries.thy b/tools/c-parser/umm_heap/Vanilla32_Preliminaries.thy index 38d6635da..cdf76c6d7 100644 --- a/tools/c-parser/umm_heap/Vanilla32_Preliminaries.thy +++ b/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