From 0102ef172a6346e0adae5a432f99ae8f682544a6 Mon Sep 17 00:00:00 2001 From: Matthew Brecknell Date: Thu, 24 Aug 2017 17:23:37 +1000 Subject: [PATCH] Isabelle2017: remove String_Compare This was a workaround for an Isabelle2016-1 performace regression, and is no longer required. --- camkes/glue-spec/CIMP.thy | 2 +- lib/Lib.thy | 1 - lib/String_Compare.thy | 142 ------------------ proof/asmrefine/SEL4GlobalsSwap.thy | 2 - proof/asmrefine/SEL4GraphRefine.thy | 1 - proof/asmrefine/SEL4SimplExport.thy | 2 - spec/cspec/ARM/Kernel_C.thy | 2 - spec/cspec/ARM_HYP/Kernel_C.thy | 2 - spec/cspec/X64/Kernel_C.thy | 2 - .../autocorres/tools/release_files/LIB_FILES | 3 - tools/c-parser/CTranslation.thy | 3 - tools/c-parser/umm_heap/StructSupport.thy | 2 +- 12 files changed, 2 insertions(+), 162 deletions(-) delete mode 100644 lib/String_Compare.thy diff --git a/camkes/glue-spec/CIMP.thy b/camkes/glue-spec/CIMP.thy index 8c8842cb4..c7f5c7b44 100644 --- a/camkes/glue-spec/CIMP.thy +++ b/camkes/glue-spec/CIMP.thy @@ -10,7 +10,7 @@ chapter {* Concurrent Imperative Syntax and Semantics \label{s:cimp} *} (*<*) theory CIMP -imports "../../lib/String_Compare" +imports Main begin (*>*) text {* diff --git a/lib/Lib.thy b/lib/Lib.thy index ee7654787..18566b284 100644 --- a/lib/Lib.thy +++ b/lib/Lib.thy @@ -16,7 +16,6 @@ chapter "Library" theory Lib imports - String_Compare Value_Abbreviation Try_Methods Eval_Bool diff --git a/lib/String_Compare.thy b/lib/String_Compare.thy deleted file mode 100644 index 8190e6e3c..000000000 --- a/lib/String_Compare.thy +++ /dev/null @@ -1,142 +0,0 @@ -(* - * - * Copyright 2016, Data61, CSIRO - * - * This software may be distributed and modified according to the terms of - * the BSD 2-Clause license. Note that NO WARRANTY is provided. - * See "LICENSE_BSD2.txt" for details. - * - * @TAG(DATA61_BSD) - *) - -theory String_Compare -imports Main -begin - -(* Speed up string comparisons in Isabelle2016-1. - We replace simp rule Char_eq_Char_iff with one which normalises in fewer steps. *) - -(* Beware that this might reappear during theory merges. *) -declare Char_eq_Char_iff [simp del] - -lemma pos_divmod_nat_rel_mult_2: - assumes "0 \ b" - assumes "divmod_nat_rel a b (q, r)" - shows "divmod_nat_rel (1 + 2*a) (2*b) (q, 1 + 2*r)" - using assms unfolding divmod_nat_rel_def by auto - -lemma pos_nat_mod_mult_2: - fixes a b :: nat - assumes "0 \ a" - shows "(1 + 2 * b) mod (2 * a) = 1 + 2 * (b mod a)" - using pos_divmod_nat_rel_mult_2 [OF assms divmod_nat_rel] - by (rule mod_nat_unique) - -lemma pos_nat_mod_mult_2_r: - fixes a b :: nat - assumes "0 \ a" - shows "(2 * b + 1) mod (2 * a) = 2 * (b mod a) + 1" - using pos_nat_mod_mult_2 by simp - -lemma num_double: "num.Bit0 num.One * n = num.Bit0 n" - by (metis (no_types, lifting) mult_2 numeral_Bit0 numeral_eq_iff - numeral_times_numeral) - -lemma num_Bit0_mod_pow2_Suc: - "numeral (num.Bit0 n) mod (2::nat) ^ Suc i = 2 * (numeral n mod 2 ^ i)" - by (metis mod_mult_mult1 mult_2 numeral_Bit0 power_Suc) - -lemma num_Bit1_mod_pow2_Suc: - "numeral (num.Bit1 n) mod (2::nat) ^ Suc i = 2 * (numeral n mod 2 ^ i) + 1" - unfolding power_Suc numeral_Bit1 mult_2[symmetric] - by (rule pos_nat_mod_mult_2_r) simp - -datatype peano = Peano_Z | Peano_S peano - -primrec - peano_of_nat :: "nat \ peano" -where - "peano_of_nat 0 = Peano_Z" -| "peano_of_nat (Suc n) = Peano_S (peano_of_nat n)" - -fun - truncate_num :: "peano \ num \ num option" -where - "truncate_num Peano_Z n = None" -| "truncate_num (Peano_S p) num.One = Some num.One" -| "truncate_num (Peano_S p) (num.Bit0 n') = map_option num.Bit0 (truncate_num p n')" -| "truncate_num (Peano_S p) (num.Bit1 n') = Some (case_option num.One num.Bit1 (truncate_num p n'))" - -lemma truncate_num: - "(numeral n :: nat) mod 2 ^ d = case_option 0 numeral (truncate_num (peano_of_nat d) n)" - proof (induct d arbitrary: n) - case 0 show ?case by (cases n) auto - next - case (Suc d) show ?case - proof (cases n) - case One thus ?thesis - apply simp - apply (rule mod_less) - using less_2_cases not_less_eq by fastforce - next - case (Bit0 m) thus ?thesis - unfolding Bit0 Suc num_Bit0_mod_pow2_Suc - by (clarsimp simp: num_double split: option.splits) - next - case (Bit1 m) show ?thesis - unfolding Bit1 Suc num_Bit1_mod_pow2_Suc - by (clarsimp simp: num_double split: option.splits) - qed - qed - -fun - truncate_num_all_zero :: "peano \ num \ bool" -where - "truncate_num_all_zero Peano_Z n = True" -| "truncate_num_all_zero (Peano_S d) (num.Bit0 n) = truncate_num_all_zero d n" -| "truncate_num_all_zero (Peano_S d) _ = False" - -lemma truncate_num_all_zero: "truncate_num_all_zero d n \ truncate_num d n = None" - by (induct n arbitrary: d; case_tac d; simp) - -fun - truncate_num_compare :: "peano \ num \ num \ bool" -where - "truncate_num_compare Peano_Z m n = True" -| "truncate_num_compare (Peano_S d) num.One num.One = True" -| "truncate_num_compare (Peano_S d) num.One (num.Bit1 n) = truncate_num_all_zero d n" -| "truncate_num_compare (Peano_S d) (num.Bit1 m) num.One = truncate_num_all_zero d m" -| "truncate_num_compare (Peano_S d) (num.Bit0 m) (num.Bit0 n) = truncate_num_compare d m n" -| "truncate_num_compare (Peano_S d) (num.Bit1 m) (num.Bit1 n) = truncate_num_compare d m n" -| "truncate_num_compare (Peano_S d) num.One (num.Bit0 _) = False" -| "truncate_num_compare (Peano_S d) (num.Bit0 _) num.One = False" -| "truncate_num_compare (Peano_S d) (num.Bit0 _) (num.Bit1 _) = False" -| "truncate_num_compare (Peano_S d) (num.Bit1 _) (num.Bit0 _) = False" - -lemma truncate_num_compare: - "truncate_num_compare d m n \ truncate_num d m = truncate_num d n" - proof - - have inj_Bit0: "inj num.Bit0" by (auto intro: injI) - show ?thesis - by (induction d m n rule: truncate_num_compare.induct; - clarsimp simp: truncate_num_all_zero map_option_case - inj_eq[OF option.inj_map, OF inj_Bit0] - split: option.splits) - qed - -abbreviation - "peano_8 \ Peano_S (Peano_S (Peano_S (Peano_S (Peano_S (Peano_S (Peano_S (Peano_S Peano_Z)))))))" - -lemma numeral_mod_256: - "(numeral n :: nat) mod 256 = case_option 0 numeral (truncate_num peano_8 n)" - proof - - have "peano_of_nat 8 \ peano_8" by (simp add: eval_nat_numeral) - thus ?thesis using truncate_num[where d=8] by simp - qed - -lemma Char_eq_iff_truncate_num_compare [simp]: - "Char k = Char l \ truncate_num_compare peano_8 k l" - unfolding Char_eq_Char_iff numeral_mod_256 truncate_num_compare - by (simp split: option.splits) - -end diff --git a/proof/asmrefine/SEL4GlobalsSwap.thy b/proof/asmrefine/SEL4GlobalsSwap.thy index b8e208882..088a78be0 100644 --- a/proof/asmrefine/SEL4GlobalsSwap.thy +++ b/proof/asmrefine/SEL4GlobalsSwap.thy @@ -17,8 +17,6 @@ imports "../../tools/asmrefine/GlobalsSwap" begin -declare Char_eq_Char_iff [simp del] - lemma globals_update_id: "globals_update id = id" by (rule ext, simp) diff --git a/proof/asmrefine/SEL4GraphRefine.thy b/proof/asmrefine/SEL4GraphRefine.thy index f4dbd26cf..6794b8a4f 100644 --- a/proof/asmrefine/SEL4GraphRefine.thy +++ b/proof/asmrefine/SEL4GraphRefine.thy @@ -16,7 +16,6 @@ imports "SEL4SimplExport" begin -declare Char_eq_Char_iff [simp del] declare ptr_add_assertion_uint [simp del] ML {* diff --git a/proof/asmrefine/SEL4SimplExport.thy b/proof/asmrefine/SEL4SimplExport.thy index 45992b556..49b200050 100644 --- a/proof/asmrefine/SEL4SimplExport.thy +++ b/proof/asmrefine/SEL4SimplExport.thy @@ -16,8 +16,6 @@ imports begin -declare Char_eq_Char_iff [simp del] - ML {* val csenv = let val the_csenv = CalculateState.get_csenv @{theory} "../c/build/$L4V_ARCH/kernel_all.c_pp" |> the diff --git a/spec/cspec/ARM/Kernel_C.thy b/spec/cspec/ARM/Kernel_C.thy index ff4adc3b9..e4951c3d5 100644 --- a/spec/cspec/ARM/Kernel_C.thy +++ b/spec/cspec/ARM/Kernel_C.thy @@ -15,8 +15,6 @@ imports "../../../tools/asmrefine/CommonOps" begin -declare Char_eq_Char_iff [simp del] - context begin interpretation Arch . requalify_types diff --git a/spec/cspec/ARM_HYP/Kernel_C.thy b/spec/cspec/ARM_HYP/Kernel_C.thy index ff4adc3b9..e4951c3d5 100644 --- a/spec/cspec/ARM_HYP/Kernel_C.thy +++ b/spec/cspec/ARM_HYP/Kernel_C.thy @@ -15,8 +15,6 @@ imports "../../../tools/asmrefine/CommonOps" begin -declare Char_eq_Char_iff [simp del] - context begin interpretation Arch . requalify_types diff --git a/spec/cspec/X64/Kernel_C.thy b/spec/cspec/X64/Kernel_C.thy index a2d7874ce..7d9004211 100644 --- a/spec/cspec/X64/Kernel_C.thy +++ b/spec/cspec/X64/Kernel_C.thy @@ -15,8 +15,6 @@ imports "../../../tools/asmrefine/CommonOps" begin -declare Char_eq_Char_iff [simp del] - context begin interpretation Arch . requalify_types diff --git a/tools/autocorres/tools/release_files/LIB_FILES b/tools/autocorres/tools/release_files/LIB_FILES index dd3986e41..a02cde158 100644 --- a/tools/autocorres/tools/release_files/LIB_FILES +++ b/tools/autocorres/tools/release_files/LIB_FILES @@ -54,9 +54,6 @@ Monad_WP/wp/WP.thy: Monad_WP/wp/WPC.thy: "Weakest-precondition" method for operating on Hoare-triples. -String_Compare.thy: - Work around slow string comparison in Isabelle2016-1. - StringOrd.thy: Ostensibly required by the C parser. diff --git a/tools/c-parser/CTranslation.thy b/tools/c-parser/CTranslation.thy index 7e75af279..96110ae47 100644 --- a/tools/c-parser/CTranslation.thy +++ b/tools/c-parser/CTranslation.thy @@ -10,7 +10,6 @@ theory CTranslation imports - "../../lib/String_Compare" "PackedTypes" "PrettyProgs" "StaticFun" @@ -26,8 +25,6 @@ and "c_defs" begin -declare Char_eq_Char_iff [simp del] - lemma TWO: "Suc (Suc 0) = 2" by arith diff --git a/tools/c-parser/umm_heap/StructSupport.thy b/tools/c-parser/umm_heap/StructSupport.thy index 9973af99d..e2b592393 100644 --- a/tools/c-parser/umm_heap/StructSupport.thy +++ b/tools/c-parser/umm_heap/StructSupport.thy @@ -9,7 +9,7 @@ *) theory StructSupport -imports SepCode SepInv "../../../lib/String_Compare" "../../../lib/Apply_Trace_Cmd" +imports SepCode SepInv "../../../lib/Apply_Trace_Cmd" begin lemma field_lookup_list_Some2 [rule_format]: