diff --git a/thys/Complx/ex/SumArr.thy b/thys/Complx/ex/SumArr.thy --- a/thys/Complx/ex/SumArr.thy +++ b/thys/Complx/ex/SumArr.thy @@ -1,448 +1,448 @@ (* * 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) *) section \Case-study\ theory SumArr imports "../OG_Syntax" - Word_Lib.Word_Lemmas_32 + Word_Lib.Word_32 begin type_synonym routine = nat type_synonym word32 = "32 word" type_synonym funcs = "string \ nat" datatype faults = Overflow | InvalidMem type_synonym 'a array = "'a list" text \Sumarr computes the combined sum of all the elements of multiple arrays. It does this by running a number of threads in parallel, each computing the sum of elements of one of the arrays, and then adding the result to a global variable gsum shared by all threads. \ record sumarr_state = \ \local variables of threads\ tarr :: "routine \ word32 array" tid :: "routine \ word32" ti :: "routine \ word32" tsum :: "routine \ word32" \ \global variables\ glock :: nat gsum :: word32 gdone :: word32 garr :: "(word32 array) array" \ \ghost variables\ ghost_lock :: "routine \ bool" definition NSUM :: word32 where "NSUM = 10" definition MAXSUM :: word32 where "MAXSUM = 1500" definition array_length :: "'a array \ word32" where "array_length arr \ of_nat (length arr)" definition array_nth :: "'a array \ word32 \'a" where "array_nth arr n \ arr ! unat n" definition array_in_bound :: "'a array \ word32 \ bool" where "array_in_bound arr idx \ unat idx < (length arr)" definition array_nat_sum :: "('a :: len) word array \ nat" where "array_nat_sum arr \ sum_list (map unat arr)" definition "local_sum arr \ of_nat (min (unat MAXSUM) (array_nat_sum arr))" definition "global_sum arr \ sum_list (map local_sum arr)" definition "tarr_inv s i \ length (tarr s i) = unat NSUM \ tarr s i = garr s ! i" abbreviation "sumarr_inv_till_lock s i \ \gdone s !! i \ ((\ (ghost_lock s) (1 - i)) \ ((gdone s = 0 \ gsum s = 0) \ (gdone s !! (1 - i) \ gsum s = local_sum (garr s !(1 - i)))))" abbreviation "lock_inv s \ (glock s = fromEnum (ghost_lock s 0) + fromEnum (ghost_lock s 1)) \ (\(ghost_lock s) 0 \ \(ghost_lock s) 1)" abbreviation "garr_inv s i \ (\a b. garr s = [a, b]) \ length (garr s ! (1-i)) = unat NSUM" abbreviation "sumarr_inv s i \ lock_inv s \ tarr_inv s i \ garr_inv s i \ tid s i = (of_nat i + 1)" definition lock :: "routine \ (sumarr_state, funcs, faults) ann_com" where "lock i \ \ \sumarr_inv i \ \tsum i = local_sum (\tarr i) \ \sumarr_inv_till_lock i\ AWAIT \glock = 0 THEN \glock:=1,, \ghost_lock:=\ghost_lock (i:= True) END" definition "sumarr_in_lock1 s i \ \gdone s !! i \ ((gdone s = 0 \ gsum s = local_sum (tarr s i)) \ (gdone s !! (1 - i) \ \ gdone s !! i \ gsum s = global_sum (garr s)))" definition "sumarr_in_lock2 s i \ (gdone s !! i \ \ gdone s !! (1 - i) \ gsum s = local_sum (tarr s i)) \ (gdone s !! i \ gdone s !! (1 - i) \ gsum s = global_sum (garr s))" definition unlock :: "routine \ (sumarr_state, funcs, faults) ann_com" where "unlock i \ \ \sumarr_inv i \ \tsum i = local_sum (\tarr i) \ \glock = 1 \ \ghost_lock i \ \gdone !! (unat (\tid i - 1)) \ \sumarr_in_lock2 i \ \\glock := 0,, \ghost_lock:=\ghost_lock (i:= False)\" definition "local_postcond s i \ (\ (ghost_lock s) (1 - i) \ gsum s = (if gdone s !! 0 \ gdone s !! 1 then global_sum (garr s) else local_sum (garr s ! i))) \ gdone s !! i \ \ghost_lock s i" definition sumarr :: "routine \ (sumarr_state, funcs, faults) ann_com" where "sumarr i \ \\sumarr_inv i \ \sumarr_inv_till_lock i\ \tsum:=\tsum(i:=0) ;; \ \tsum i = 0 \ \sumarr_inv i \ \sumarr_inv_till_lock i\ \ti:=\ti(i:=0) ;; TRY \ \tsum i = 0 \ \sumarr_inv i \ \ti i = 0 \ \sumarr_inv_till_lock i\ WHILE \ti i < NSUM INV \ \sumarr_inv i \ \ti i \ NSUM \ \tsum i \ MAXSUM \ \tsum i = local_sum (take (unat (\ti i)) (\tarr i)) \ \sumarr_inv_till_lock i\ DO \ \sumarr_inv i \ \ti i < NSUM \ \tsum i \ MAXSUM \ \tsum i = local_sum (take (unat (\ti i)) (\tarr i)) \ \sumarr_inv_till_lock i\ (InvalidMem, \ array_in_bound (\tarr i) (\ti i) \) \ \ \sumarr_inv i \ \ti i < NSUM \ \tsum i \ MAXSUM \ \tsum i = local_sum (take (unat (\ti i)) (\tarr i)) \ \sumarr_inv_till_lock i\ \tsum:=\tsum(i:=\tsum i + array_nth (\tarr i) (\ti i));; \ \sumarr_inv i \ \ti i < NSUM \ local_sum (take (unat (\ti i)) (\tarr i)) \ MAXSUM \ (\tsum i < MAXSUM \ array_nth (\tarr i) (\ti i) < MAXSUM \ \tsum i = local_sum (take (Suc (unat (\ti i))) (\tarr i))) \ (array_nth (\tarr i) (\ti i) \ MAXSUM \ \tsum i \ MAXSUM\ local_sum (\tarr i) = MAXSUM) \ \sumarr_inv_till_lock i \ (InvalidMem, \ array_in_bound (\tarr i) (\ti i) \) \ \ \sumarr_inv i \ \ti i < NSUM \ (\tsum i < MAXSUM \ array_nth (\tarr i) (\ti i) < MAXSUM \ \tsum i = local_sum (take (Suc (unat (\ti i))) (\tarr i))) \ (array_nth (\tarr i) (\ti i) \ MAXSUM \ \tsum i \ MAXSUM \ local_sum (\tarr i) = MAXSUM) \ \sumarr_inv_till_lock i\ IF array_nth (\tarr i) (\ti i) \ MAXSUM \ \tsum i \ MAXSUM THEN \ \sumarr_inv i \ \ti i < NSUM \ local_sum (\tarr i) = MAXSUM \ \sumarr_inv_till_lock i\ \tsum:=\tsum(i:=MAXSUM);; \ \sumarr_inv i \ \ti i < NSUM \ \tsum i \ MAXSUM \ \tsum i = local_sum (\tarr i) \ \sumarr_inv_till_lock i \ THROW ELSE \ \sumarr_inv i \ \ti i < NSUM \ \tsum i \ MAXSUM \ \tsum i = local_sum (take (Suc (unat (\ti i))) (\tarr i)) \ \sumarr_inv_till_lock i\ SKIP FI;; \ \sumarr_inv i \ \ti i < NSUM \ \tsum i \ MAXSUM \ \tsum i = local_sum (take (Suc (unat (\ti i))) (\tarr i)) \ \sumarr_inv_till_lock i \ \ti:=\ti(i:=\ti i + 1) OD CATCH \ \sumarr_inv i \ \tsum i = local_sum (\tarr i) \ \sumarr_inv_till_lock i\ SKIP END;; \ \sumarr_inv i \ \tsum i = local_sum (\tarr i) \ \sumarr_inv_till_lock i\ SCALL (''lock'', i) 0;; \ \sumarr_inv i \ \tsum i = local_sum (\tarr i) \ \glock = 1 \ \ghost_lock i \ \sumarr_inv_till_lock i \ \gsum:=\gsum + \tsum i ;; \ \sumarr_inv i \ \tsum i = local_sum (\tarr i) \ \glock = 1 \ \ghost_lock i \ \sumarr_in_lock1 i \ \gdone:=(\gdone OR \tid i) ;; \ \sumarr_inv i \ \tsum i = local_sum (\tarr i) \ \glock = 1 \ \ghost_lock i \ \gdone !! (unat (\tid i - 1)) \ \sumarr_in_lock2 i \ SCALL (''unlock'', i) 0" definition precond where "precond s \ (glock s) = 0 \ (gsum s) = 0\ (gdone s) = 0 \ (\a b. garr s = [a, b]) \ (\xs\set (garr s). length xs = unat NSUM) \ (ghost_lock s) 0 = False \ (ghost_lock s) 1 = False" definition postcond where "postcond s \ (gsum s) = global_sum (garr s) \ (\i < 2. (gdone s) !! i)" definition "call_sumarr i \ \length (\garr ! i) = unat NSUM \ \lock_inv \ \garr_inv i \ \sumarr_inv_till_lock i\ CALLX (\s. s\tarr:=(tarr s)(i:=garr s ! i), tid:=(tid s)(i:=of_nat i+1), ti:=(ti s)(i:=undefined), tsum:=(tsum s)(i:=undefined)\) \\sumarr_inv i \ \sumarr_inv_till_lock i\ (''sumarr'', i) 0 (\s t. t\tarr:= (tarr t)(i:=(tarr s) i), tid:=(tid t)(i:=(tid s i)), ti:=(ti t)(i:=(ti s i)), tsum:=(tsum t)(i:=(tsum s i))\) (\_ _. Skip) \\local_postcond i\ \\local_postcond i\ \False\ \False\" definition "\ \ map_of (map (\i. ((''sumarr'', i), com (sumarr i))) [0..<2]) ++ map_of (map (\i. ((''lock'', i), com (lock i))) [0..<2]) ++ map_of (map (\i. ((''unlock'', i), com (unlock i))) [0..<2])" definition "\ \ map_of (map (\i. ((''sumarr'', i), [ann (sumarr i)])) [0..<2]) ++ map_of (map (\i. ((''lock'', i), [ann (lock i)])) [0..<2]) ++ map_of (map (\i. ((''unlock'', i), [ann (unlock i)])) [0..<2])" declare [[goals_limit = 10]] lemma [simp]: "local_sum [] = 0" by (simp add: local_sum_def array_nat_sum_def) lemma MAXSUM_le_plus: "x < MAXSUM \ MAXSUM \ MAXSUM + x" unfolding MAXSUM_def apply (rule word_le_plus[rotated], assumption) apply clarsimp done lemma local_sum_Suc: "\n < length arr; local_sum (take n arr) + arr ! n < MAXSUM; arr ! n < MAXSUM\ \ local_sum (take n arr) + arr ! n = local_sum (take (Suc n) arr)" apply (subst take_Suc_conv_app_nth) apply clarsimp apply (clarsimp simp: local_sum_def array_nat_sum_def ) apply (subst (asm) min_def, clarsimp split: if_splits) apply (clarsimp simp: MAXSUM_le_plus word_not_le[symmetric]) apply (subst min_absorb2) apply (subst of_nat_mono_maybe_le[where 'a=32]) apply (clarsimp simp: MAXSUM_def) apply (clarsimp simp: MAXSUM_def) apply unat_arith apply (clarsimp simp: MAXSUM_def) apply unat_arith apply clarsimp done lemma local_sum_MAXSUM: "k < length arr \ MAXSUM \ arr ! k \ local_sum arr = MAXSUM" apply (clarsimp simp: local_sum_def array_nat_sum_def) apply (rule word_unat.Rep_inverse') apply (rule min_absorb1[symmetric]) apply (subst (asm) word_le_nat_alt) apply (rule le_trans[rotated]) apply (rule elem_le_sum_list) apply simp apply clarsimp done lemma local_sum_MAXSUM': "k < length arr \ MAXSUM \ local_sum (take k arr) + arr ! k \ local_sum (take k arr) \ MAXSUM \ arr ! k \ MAXSUM \ local_sum arr = MAXSUM" apply (clarsimp simp: local_sum_def array_nat_sum_def) apply (rule word_unat.Rep_inverse') apply (rule min_absorb1[symmetric]) apply (subst (asm) word_le_nat_alt) apply (subst (asm) unat_plus_simple[THEN iffD1]) apply (rule word_add_le_mono2[where i=0, simplified]) apply (clarsimp simp: MAXSUM_def) apply unat_arith apply (rule le_trans, assumption) apply (subst unat_of_nat_eq) apply (clarsimp simp: MAXSUM_def min.strict_coboundedI1) by (subst id_take_nth_drop[where i=k], simp, clarsimp simp: trans_le_add1) lemma word_min_0[simp]: "min (x::'a::len word) 0 = 0" "min 0 (x::'a::len word) = 0" by (simp add:min_def)+ ML \fun TRY' tac i = TRY (tac i)\ lemma imp_disjL_context': "((P \ R) \ (Q \ R)) = ((P \ R) \ (\P \ Q \ R))" by auto lemma map_of_prod_1[simp]: "i < n \ map_of (map (\i. ((p, i), g i)) [0.. p \ q \ (m ++ map_of (map (\i. ((p, i), g i)) [0.. \ (''sumarr'',n) = Some (com (sumarr n))" "n < 2 \ \ (''sumarr'',n) = Some ([ann (sumarr n)])" "n < 2 \ \ (''lock'',n) = Some (com (lock n))" "n < 2 \ \ (''lock'',n) = Some ([ann (lock n)])" "n < 2 \ \ (''unlock'',n) = Some (com (unlock n))" "n < 2 \ \ (''unlock'',n) = Some ([ann (unlock n)])" "[ann (sumarr n)]!0 = ann (sumarr n)" "[ann (lock n)]!0 = ann (lock n)" "[ann (unlock n)]!0 = ann (unlock n)" by (simp add: \_def \_def)+ lemmas sumarr_proc_simp_unfolded = sumarr_proc_simp[unfolded sumarr_def unlock_def lock_def oghoare_simps] lemma oghoare_sumarr: notes sumarr_proc_simp_unfolded[proc_simp add] shows "i < 2 \ \, \ |\\<^bsub>/F\<^esub> sumarr i \\local_postcond i\, \False\" unfolding sumarr_def unlock_def lock_def ann_call_def call_def block_def apply simp apply oghoare (*23*) unfolding tarr_inv_def array_length_def array_nth_def array_in_bound_def sumarr_in_lock1_def sumarr_in_lock2_def apply (tactic "PARALLEL_ALLGOALS ((TRY' o SOLVED') (clarsimp_tac (@{context} addsimps @{thms local_postcond_def global_sum_def ex_in_conv[symmetric]}) THEN_ALL_NEW fast_force_tac (@{context} addSDs @{thms less_2_cases} addIs @{thms local_sum_Suc unat_mono} ) ))") (*2*) apply clarsimp apply (rule conjI) apply (fastforce intro!: local_sum_Suc unat_mono) apply (subst imp_disjL_context') apply (rule conjI) apply clarsimp apply (erule local_sum_MAXSUM[rotated]) apply unat_arith apply (clarsimp simp: not_le) apply (erule (1) local_sum_MAXSUM'[rotated] ; unat_arith) apply clarsimp apply unat_arith done lemma less_than_two_2[simp]: "i < 2 \ Suc 0 - i < 2" by arith lemma oghoare_call_sumarr: notes sumarr_proc_simp[proc_simp add] shows "i < 2 \ \, \ |\\<^bsub>/F\<^esub> call_sumarr i \\local_postcond i\, \False\" unfolding call_sumarr_def ann_call_def call_def block_def tarr_inv_def apply oghoare (*10*) apply (clarsimp; fail | ((simp only: pre.simps)?, rule oghoare_sumarr))+ apply (clarsimp simp: sumarr_def tarr_inv_def) apply (clarsimp simp: local_postcond_def; fail)+ done lemma less_than_two_inv[simp]: "i < 2 \ j < 2 \ i \ j \ Suc 0 - i = j" by simp lemma inter_aux_call_sumarr[simplified]: notes sumarr_proc_simp_unfolded[proc_simp add] com.simps[oghoare_simps add] shows "i < 2 \ j < 2 \ i \ j \ interfree_aux \ \ F (com (call_sumarr i), (ann (call_sumarr i), \\local_postcond i\, \False\), com (call_sumarr j), ann (call_sumarr j))" unfolding call_sumarr_def ann_call_def call_def block_def tarr_inv_def sumarr_def lock_def unlock_def apply oghoare_interfree_aux (*650*) unfolding tarr_inv_def local_postcond_def sumarr_in_lock1_def sumarr_in_lock2_def by (tactic "PARALLEL_ALLGOALS ( TRY' (remove_single_Bound_mem @{context}) THEN' (TRY' o SOLVED') (clarsimp_tac @{context} THEN_ALL_NEW fast_force_tac (@{context} addSDs @{thms less_2_cases}) ))") (* 2 minutes *) lemma pre_call_sumarr: "i < 2 \ precond x \ x \ pre (ann (call_sumarr i))" unfolding precond_def call_sumarr_def ann_call_def by (fastforce dest: less_2_cases simp: array_length_def) lemma post_call_sumarr: "local_postcond x 0 \ local_postcond x 1 \ postcond x" unfolding postcond_def local_postcond_def by (fastforce dest: less_2_cases split: if_splits) lemma sumarr_correct: "\, \ |\\<^bsub>/F\<^esub> \\precond\ COBEGIN SCHEME [0 \ m < 2] call_sumarr m \\local_postcond m\,\False\ COEND \\postcond\, \False\" apply oghoare (* 5 subgoals *) apply (fastforce simp: pre_call_sumarr) apply (rule oghoare_call_sumarr, simp) apply (clarsimp simp: post_call_sumarr) apply (simp add: inter_aux_call_sumarr) apply clarsimp done end diff --git a/thys/IEEE_Floating_Point/FP64.thy b/thys/IEEE_Floating_Point/FP64.thy --- a/thys/IEEE_Floating_Point/FP64.thy +++ b/thys/IEEE_Floating_Point/FP64.thy @@ -1,84 +1,84 @@ theory FP64 imports IEEE - Word_Lib.Word_Lemmas_64 + Word_Lib.Word_64 begin section \Concrete encodings\ text \Floating point operations defined as operations on words. Called ''fixed precision'' (fp) word in HOL4.\ type_synonym float64 = "(11,52)float" type_synonym fp64 = "64 word" lift_definition fp64_of_float :: "float64 \ fp64" is "\(s::1 word, e::11 word, f::52 word). word_cat s (word_cat e f::63 word)" . lift_definition float_of_fp64 :: "fp64 \ float64" is "\x. apsnd word_split (word_split x::1 word * 63 word)" . definition "rel_fp64 \ (\x (y::word64). x = float_of_fp64 y)" definition eq_fp64::"float64 \ float64 \ bool" where [simp]: "eq_fp64 \ (=)" lemma float_of_fp64_inverse[simp]: "fp64_of_float (float_of_fp64 a) = a" by (auto simp: fp64_of_float_def float_of_fp64_def Abs_float_inverse apsnd_def map_prod_def word_size dest!: word_cat_split_alt[rotated] split: prod.splits) lemma float_of_fp64_inj_iff[simp]: "fp64_of_float r = fp64_of_float s \ r = s" using Rep_float_inject by (force simp: fp64_of_float_def word_cat_inj word_size split: prod.splits) lemma fp64_of_float_inverse[simp]: "float_of_fp64 (fp64_of_float a) = a" using float_of_fp64_inj_iff float_of_fp64_inverse by blast lemma Quotientfp: "Quotient eq_fp64 fp64_of_float float_of_fp64 rel_fp64" \\\<^term>\eq_fp64\ is a workaround to prevent a (failing -- TODO: why?) code setup in \setup_lifting\.\ by (force intro!: QuotientI simp: rel_fp64_def) setup_lifting Quotientfp lift_definition fp64_lessThan::"fp64 \ fp64 \ bool" is "flt::float64\float64\bool" by simp lift_definition fp64_lessEqual::"fp64 \ fp64 \ bool" is "fle::float64\float64\bool" by simp lift_definition fp64_greaterThan::"fp64 \ fp64 \ bool" is "fgt::float64\float64\bool" by simp lift_definition fp64_greaterEqual::"fp64 \ fp64 \ bool" is "fge::float64\float64\bool" by simp lift_definition fp64_equal::"fp64 \ fp64 \ bool" is "feq::float64\float64\bool" by simp lift_definition fp64_abs::"fp64 \ fp64" is "abs::float64\float64" by simp lift_definition fp64_negate::"fp64 \ fp64" is "uminus::float64\float64" by simp lift_definition fp64_sqrt::"roundmode \ fp64 \ fp64" is "fsqrt::roundmode\float64\float64" by simp lift_definition fp64_add::"roundmode \ fp64 \ fp64 \ fp64" is "fadd::roundmode\float64\float64\float64" by simp lift_definition fp64_sub::"roundmode \ fp64 \ fp64 \ fp64" is "fsub::roundmode\float64\float64\float64" by simp lift_definition fp64_mul::"roundmode \ fp64 \ fp64 \ fp64" is "fmul::roundmode\float64\float64\float64" by simp lift_definition fp64_div::"roundmode \ fp64 \ fp64 \ fp64" is "fdiv::roundmode\float64\float64\float64" by simp lift_definition fp64_mul_add::"roundmode \ fp64 \ fp64 \ fp64 \ fp64" is "fmul_add::roundmode\float64\float64\float64\float64" by simp end diff --git a/thys/Word_Lib/Examples.thy b/thys/Word_Lib/Examples.thy --- a/thys/Word_Lib/Examples.thy +++ b/thys/Word_Lib/Examples.thy @@ -1,217 +1,217 @@ theory Examples imports Bitwise Next_and_Prev Generic_set_bit Word_Syntax begin text "modulus" lemma "(27 :: 4 word) = -5" by simp lemma "(27 :: 4 word) = 11" by simp lemma "27 \ (11 :: 6 word)" by simp text "signed" lemma "(127 :: 6 word) = -1" by simp text "number ring simps" lemma "27 + 11 = (38::'a::len word)" "27 + 11 = (6::5 word)" "7 * 3 = (21::'a::len word)" "11 - 27 = (-16::'a::len word)" "- (- 11) = (11::'a::len word)" "-40 + 1 = (-39::'a::len word)" by simp_all lemma "word_pred 2 = 1" by simp lemma "word_succ (- 3) = -2" by simp lemma "23 < (27::8 word)" by simp lemma "23 \ (27::8 word)" by simp lemma "\ 23 < (27::2 word)" by simp lemma "0 < (4::3 word)" by simp lemma "1 < (4::3 word)" by simp lemma "0 < (1::3 word)" by simp text "ring operations" lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp text "casting" lemma "uint (234567 :: 10 word) = 71" by simp lemma "uint (-234567 :: 10 word) = 953" by simp lemma "sint (234567 :: 10 word) = 71" by simp lemma "sint (-234567 :: 10 word) = -71" by simp lemma "uint (1 :: 10 word) = 1" by simp lemma "unat (-234567 :: 10 word) = 953" by simp lemma "unat (1 :: 10 word) = 1" by simp lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)" by simp lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp text "reducing goals to nat or int and arith:" lemma "i < x \ i < i + 1" for i x :: "'a::len word" by unat_arith lemma "i < x \ i < i + 1" for i x :: "'a::len word" by unat_arith text "bool lists" lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by (simp add: numeral_eq_Suc) text "bit operations" lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp lemma "0xF0 XOR 0xFF = (0x0F :: 8 word)" by simp lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp lemma "0 AND 5 = (0 :: 8 word)" by simp lemma "1 AND 1 = (1 :: 8 word)" by simp lemma "1 AND 0 = (0 :: 8 word)" by simp lemma "1 AND 5 = (1 :: 8 word)" by simp lemma "1 OR 6 = (7 :: 8 word)" by simp lemma "1 OR 1 = (1 :: 8 word)" by simp lemma "1 XOR 7 = (6 :: 8 word)" by simp lemma "1 XOR 1 = (0 :: 8 word)" by simp lemma "NOT 1 = (254 :: 8 word)" by simp lemma "NOT 0 = (255 :: 8 word)" by simp lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp lemma "(0b0010 :: 4 word) !! 1" by simp lemma "\ (0b0010 :: 4 word) !! 0" by simp lemma "\ (0b1000 :: 3 word) !! 4" by simp lemma "\ (1 :: 3 word) !! 2" by simp lemma "(0b11000 :: 10 word) !! n = (n = 4 \ n = 3)" by (auto simp add: bin_nth_Bit0 bin_nth_Bit1) lemma "set_bit 55 7 True = (183::'a::len word)" by simp lemma "set_bit 0b0010 7 True = (0b10000010::'a::len word)" by simp lemma "set_bit 0b0010 1 False = (0::'a::len word)" by simp lemma "set_bit 1 3 True = (0b1001::'a::len word)" by simp lemma "set_bit 1 0 False = (0::'a::len word)" by simp lemma "set_bit 0 3 True = (0b1000::'a::len word)" by simp lemma "set_bit 0 3 False = (0::'a::len word)" by simp lemma "odd (0b0101::'a::len word)" by simp lemma "even (0b1000::'a::len word)" by simp lemma "odd (1::'a::len word)" by simp lemma "even (0::'a::len word)" by simp lemma "\ msb (0b0101::4 word)" by simp lemma "msb (0b1000::4 word)" by simp lemma "\ msb (1::4 word)" by simp lemma "\ msb (0::4 word)" by simp lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)" by simp lemma "0b1011 << 2 = (0b101100::'a::len word)" by simp lemma "0b1011 >> 2 = (0b10::8 word)" by simp lemma "0b1011 >>> 2 = (0b10::8 word)" by simp lemma "1 << 2 = (0b100::'a::len word)" apply simp? oops lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp lemma "slice 3 (1::6 word) = (0::3 word)" apply simp? oops lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp lemma "word_rotr 2 0 = (0::4 word)" by simp lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" proof - have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)" by (simp only: word_ao_dist2) also have "0xff00 OR 0x00ff = (-1::16 word)" by simp also have "x AND -1 = x" by simp finally show ?thesis . qed lemma "word_next (2:: 8 word) = 3" by eval lemma "word_next (255:: 8 word) = 255" by eval lemma "word_prev (2:: 8 word) = 1" by eval lemma "word_prev (0:: 8 word) = 0" by eval text "proofs using bitwise expansion" lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)" by word_bitwise lemma "(x AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)" for x :: "10 word" by word_bitwise lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3" for x :: "12 word" by word_bitwise text "some problems require further reasoning after bit expansion" lemma "x \ 42 \ x \ 89" for x :: "8 word" apply word_bitwise apply blast done lemma "(x AND 1023) = 0 \ x \ -1024" for x :: \32 word\ apply word_bitwise apply clarsimp done text "operations like shifts by non-numerals will expose some internal list representations but may still be easy to solve" lemma shiftr_overflow: "32 \ a \ b >> a = 0" for b :: \32 word\ apply word_bitwise apply simp done (* testing for presence of word_bitwise *) -lemma "((x :: word32) >> 3) AND 7 = (x AND 56) >> 3" +lemma "((x :: 32 word) >> 3) AND 7 = (x AND 56) >> 3" by word_bitwise (* Tests *) lemma - "( 4 :: word32) sdiv 4 = 1" - "(-4 :: word32) sdiv 4 = -1" - "(-3 :: word32) sdiv 4 = 0" - "( 3 :: word32) sdiv -4 = 0" - "(-3 :: word32) sdiv -4 = 0" - "(-5 :: word32) sdiv -4 = 1" - "( 5 :: word32) sdiv -4 = -1" + "( 4 :: 32 word) sdiv 4 = 1" + "(-4 :: 32 word) sdiv 4 = -1" + "(-3 :: 32 word) sdiv 4 = 0" + "( 3 :: 32 word) sdiv -4 = 0" + "(-3 :: 32 word) sdiv -4 = 0" + "(-5 :: 32 word) sdiv -4 = 1" + "( 5 :: 32 word) sdiv -4 = -1" by (simp_all add: sdiv_word_def signed_divide_int_def) lemma - "( 4 :: word32) smod 4 = 0" - "( 3 :: word32) smod 4 = 3" - "(-3 :: word32) smod 4 = -3" - "( 3 :: word32) smod -4 = 3" - "(-3 :: word32) smod -4 = -3" - "(-5 :: word32) smod -4 = -1" - "( 5 :: word32) smod -4 = 1" + "( 4 :: 32 word) smod 4 = 0" + "( 3 :: 32 word) smod 4 = 3" + "(-3 :: 32 word) smod 4 = -3" + "( 3 :: 32 word) smod -4 = 3" + "(-3 :: 32 word) smod -4 = -3" + "(-5 :: 32 word) smod -4 = -1" + "( 5 :: 32 word) smod -4 = 1" by (simp_all add: smod_word_def signed_modulo_int_def signed_divide_int_def) end diff --git a/thys/Word_Lib/Guide.thy b/thys/Word_Lib/Guide.thy --- a/thys/Word_Lib/Guide.thy +++ b/thys/Word_Lib/Guide.thy @@ -1,312 +1,327 @@ (*<*) theory Guide imports Word_Lib_Sumo begin hide_const (open) Generic_set_bit.set_bit (*>*) section \A short overview over bit operations and word types\ subsection \Basic theories and key ideas\ text \ When formalizing bit operations, it is tempting to represent bit values as explicit lists over a binary type. This however is a bad idea, mainly due to the inherent ambiguities in representation concerning repeating leading bits. Hence this approach avoids such explicit lists altogether following an algebraic path: \<^item> Bit values are represented by numeric types: idealized unbounded bit values can be represented by type \<^typ>\int\, bounded bit values by quotient types over \<^typ>\int\, aka \<^typ>\'a word\. \<^item> (A special case are idealized unbounded bit values ending in @{term [source] 0} which can be represented by type \<^typ>\nat\ but only support a restricted set of operations). The most fundamental ideas are developed in theory \<^theory>\HOL.Parity\ (which is part of \<^theory>\Main\): \<^item> Multiplication by \<^term>\2 :: int\ is a bit shift to the left and \<^item> Division by \<^term>\2 :: int\ is a bit shift to the right. \<^item> Concerning bounded bit values, iterated shifts to the left may result in eliminating all bits by shifting them all beyond the boundary. The property \<^prop>\(2 :: int) ^ n \ 0\ represents that \<^term>\n\ is \<^emph>\not\ beyond that boundary. \<^item> The projection on a single bit is then @{thm [mode=iff] bit_iff_odd [where ?'a = int, no_vars]}. \<^item> This leads to the most fundamental properties of bit values: \<^item> Equality rule: @{thm [display, mode=iff] bit_eq_iff [where ?'a = int, no_vars]} \<^item> Induction rule: @{thm [display, mode=iff] bits_induct [where ?'a = int, no_vars]} On top of this, the following generic operations are provided after import of theory \<^theory>\HOL-Library.Bit_Operations\: \<^item> Singleton \<^term>\n\th bit: \<^term>\(2 :: int) ^ n\ \<^item> Bit mask upto bit \<^term>\n\: @{thm mask_eq_exp_minus_1 [where ?'a = int, no_vars]} \<^item> Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]} \<^item> Right shift: @{thm drop_bit_eq_div [where ?'a = int, no_vars]} \<^item> Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]} \<^item> Negation: @{thm [mode=iff] bit_not_iff [where ?'a = int, no_vars]} \<^item> And: @{thm [mode=iff] bit_and_iff [where ?'a = int, no_vars]} \<^item> Or: @{thm [mode=iff] bit_or_iff [where ?'a = int, no_vars]} \<^item> Xor: @{thm [mode=iff] bit_xor_iff [where ?'a = int, no_vars]} \<^item> Set a single bit: @{thm set_bit_def [where ?'a = int, no_vars]} \<^item> Unset a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]} \<^item> Flip a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]} \<^item> Signed truncation, or modulus centered around \<^term>\0::int\: @{thm [display] signed_take_bit_def [where ?'a = int, no_vars]} \<^item> (Bounded) conversion from and to a list of bits: @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} Proper word types are introduced in theory \<^theory>\HOL-Library.Word\, with the following specific operations: \<^item> Standard arithmetic: @{term \(+) :: 'a::len word \ 'a word \ 'a word\}, @{term \uminus :: 'a::len word \ 'a word\}, @{term \(-) :: 'a::len word \ 'a word \ 'a word\}, @{term \(*) :: 'a::len word \ 'a word \ 'a word\}, @{term \0 :: 'a::len word\}, @{term \1 :: 'a::len word\}, numerals etc. \<^item> Standard bit operations: see above. \<^item> Conversion with unsigned interpretation of words: \<^item> @{term [source] \unsigned :: 'a::len word \ 'b::semiring_1\} \<^item> Important special cases as abbreviations: \<^item> @{term [source] \unat :: 'a::len word \ nat\} \<^item> @{term [source] \uint :: 'a::len word \ int\} \<^item> @{term [source] \ucast :: 'a::len word \ 'b::len word\} \<^item> Conversion with signed interpretation of words: \<^item> @{term [source] \signed :: 'a::len word \ 'b::ring_1\} \<^item> Important special cases as abbreviations: \<^item> @{term [source] \sint :: 'a::len word \ int\} \<^item> @{term [source] \scast :: 'a::len word \ 'b::len word\} \<^item> Operations with unsigned interpretation of words: \<^item> @{thm [mode=iff] word_le_nat_alt [no_vars]} \<^item> @{thm [mode=iff] word_less_nat_alt [no_vars]} \<^item> @{thm unat_div_distrib [no_vars]} \<^item> @{thm unat_drop_bit_eq [no_vars]} \<^item> @{thm unat_mod_distrib [no_vars]} \<^item> @{thm [mode=iff] udvd_iff_dvd [no_vars]} \<^item> Operations with signed interpretation of words: \<^item> @{thm [mode=iff] word_sle_eq [no_vars]} \<^item> @{thm [mode=iff] word_sless_alt [no_vars]} \<^item> @{thm sint_signed_drop_bit_eq [no_vars]} \<^item> Rotation and reversal: \<^item> @{term [source] \word_rotl :: nat \ 'a::len word \ 'a word\} \<^item> @{term [source] \word_rotr :: nat \ 'a::len word \ 'a word\} \<^item> @{term [source] \word_roti :: int \ 'a::len word \ 'a word\} \<^item> @{term [source] \word_reverse :: 'a::len word \ 'a word\} \<^item> Concatenation: @{term [source, display] \word_cat :: 'a::len word \ 'b::len word \ 'c::len word\} For proofs about words the following default strategies are applicable: \<^item> Using bit extensionality (facts \<^text>\bit_eq_iff\, \<^text>\bit_eqI\). \<^item> Using the @{method transfer} method. \ subsection \More library theories\ text \ Note: currently, the theories listed here are hardly separate entities since they import each other in various ways. Always inspect them to understand what you pull in if you want to import one. \<^descr>[Syntax] \<^descr>[\<^theory>\Word_Lib.Hex_Words\] Printing word numerals as hexadecimal numerals. \<^descr>[\<^theory>\Word_Lib.Type_Syntax\] Pretty type-sensitive syntax for cast operations. \<^descr>[\<^theory>\Word_Lib.Word_Syntax\] Specific ASCII syntax for prominent bit operations on word. \<^descr>[Proof tools] \<^descr>[\<^theory>\Word_Lib.Norm_Words\] Rewriting word numerals to normal forms. \<^descr>[\<^theory>\Word_Lib.Bitwise\] Method @{method word_bitwise} decomposes word equalities and inequalities into bit propositions. \<^descr>[\<^theory>\Word_Lib.Word_EqI\] Method @{method word_eqI_solve} decomposes word equalities and inequalities into bit propositions. \<^descr>[Operations] \<^descr>[\<^theory>\Word_Lib.Least_significant_bit\] The least significant bit as an alias: @{thm [mode=iff] lsb_odd [where ?'a = int, no_vars]} \<^descr>[\<^theory>\Word_Lib.Most_significant_bit\] The most significant bit: \<^item> @{thm [mode=iff] msb_int_def [of k]} \<^item> @{thm [mode=iff] word_msb_sint [no_vars]} \<^item> @{thm [mode=iff] msb_word_iff_sless_0 [no_vars]} \<^item> @{thm [mode=iff] msb_word_iff_bit [no_vars]} \<^descr>[\<^theory>\Word_Lib.Traditional_Infix_Syntax\] Clones of existing operations decorated with traditional syntax: \<^item> @{thm test_bit_eq_bit [no_vars]} \<^item> @{thm shiftl_eq_push_bit [no_vars]} \<^item> @{thm shiftr_eq_drop_bit [no_vars]} \<^item> @{thm sshiftr_eq [no_vars]} \<^descr>[\<^theory>\Word_Lib.Word_Lib\] Various operations on word, particularly: \<^item> @{term [source] \(sdiv) :: 'a::len word \ 'a word \ 'a word\} \<^item> @{term [source] \(smod) :: 'a::len word \ 'a word \ 'a word\} \<^descr>[\<^theory>\Word_Lib.Aligned\] \ \<^item> @{thm [mode=iff] is_aligned_iff_udvd [no_vars]} \<^descr>[\<^theory>\Word_Lib.Next_and_Prev\] \ \<^item> @{thm word_next_unfold [no_vars]} \<^item> @{thm word_prev_unfold [no_vars]} \<^descr>[Types] \<^descr>[\<^theory>\Word_Lib.Signed_Words\] Formal tagging of word types with a \<^text>\signed\ marker. \<^descr>[Mechanisms] \<^descr>[\<^theory>\Word_Lib.Enumeration_Word\] More on explicit enumeration of word types. \<^descr>[Lemmas] Collections of lemmas: \<^descr>[\<^theory>\Word_Lib.Word_Lemmas\] generic. - \<^descr>[\<^theory>\Word_Lib.Word_Lemmas_32\] for 32-bit words. + \<^descr>[Lemmas] - \<^descr>[\<^theory>\Word_Lib.Word_Lemmas_64\] for 64-bit words. + Words of fixed length: + + \<^descr>[\<^theory>\Word_Lib.Word_8\] for 8-bit words. + + \<^descr>[\<^theory>\Word_Lib.Word_16\] for 16-bit words. + + \<^descr>[\<^theory>\Word_Lib.Word_32\] for 32-bit words. + + \<^descr>[\<^theory>\Word_Lib.Word_64\] for 64-bit words. \ subsection \More library sessions\ text \ \<^descr>[\<^text>\Native_Word\] Makes machine words and machine arithmetic available for code generation. It provides a common abstraction that hides the differences between the different target languages. The code generator maps these operations to the APIs of the target languages. \ subsection \Legacy theories\ text \ The following theories contain material which has been factored out since it is not recommended to use it in new applications, mostly because matters can be expressed succinctly using already existing operations. This section gives some indication how to migrate away from those theories. However theorem coverage may still be terse in some cases. \<^descr>[\<^theory>\Word_Lib.Generic_set_bit\] Kind of an alias: @{thm set_bit_eq [no_vars]} \<^descr>[\<^theory>\Word_Lib.Typedef_Morphisms\] A low-level extension to HOL typedef providing conversions along type morphisms. The @{method transfer} method seems to be sufficient for most applications though. \<^descr>[\<^theory>\Word_Lib.Bit_Comprehension\] Comprehension syntax for bit values over predicates \<^typ>\nat \ bool\. For \<^typ>\'a::len word\, straightforward alternatives exist; difficult to handle for \<^typ>\int\. \<^descr>[\<^theory>\Word_Lib.Reversed_Bit_Lists\] Representation of bit values as explicit list in \<^emph>\reversed\ order. This should rarely be necessary: the \<^const>\bit\ projection should be sufficient in most cases. In case explicit lists are needed, existing operations can be used: @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} + + \<^descr>[\<^theory>\Word_Lib.Word_Lib_Sumo\] + + An entry point importing any theory in that session. Intended + for backward compatibility: start importing this theory when + migrating applications to Isabelle2021, and later sort out + what you really need. \ (*<*) end (*>*) diff --git a/thys/Word_Lib/Word_16.thy b/thys/Word_Lib/Word_16.thy new file mode 100644 --- /dev/null +++ b/thys/Word_Lib/Word_16.thy @@ -0,0 +1,18 @@ +(* + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +section "Words of Length 16" + +theory Word_16 +imports + Word_Lemmas + Word_Syntax +begin + +type_synonym word16 = "16 word" +lemma len16: "len_of (x :: 16 itself) = 16" by simp + +end diff --git a/thys/Word_Lib/Word_Lemmas_32.thy b/thys/Word_Lib/Word_32.thy rename from thys/Word_Lib/Word_Lemmas_32.thy rename to thys/Word_Lib/Word_32.thy --- a/thys/Word_Lib/Word_Lemmas_32.thy +++ b/thys/Word_Lib/Word_32.thy @@ -1,306 +1,338 @@ (* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) -section "Lemmas for Word Length 32" +section "Words of Length 32" -theory Word_Lemmas_32 -imports - Word_Lemmas - Word_Setup_32 - Word_Syntax +theory Word_32 + imports + Word_Lemmas + Word_8 + Word_16 + Word_Syntax begin +type_synonym word32 = "32 word" +lemma len32: "len_of (x :: 32 itself) = 32" by simp + +type_synonym machine_word_len = 32 +type_synonym machine_word = "machine_word_len word" + +definition word_bits :: nat +where + "word_bits = LENGTH(machine_word_len)" + +text \The following two are numerals so they can be used as nats and words.\ +definition word_size_bits :: "'a :: numeral" +where + "word_size_bits = 2" + +definition word_size :: "'a :: numeral" +where + "word_size = 4" + +lemma word_bits_conv[code]: + "word_bits = 32" + unfolding word_bits_def by simp + +lemma word_size_word_size_bits: + "(word_size::nat) = 2 ^ word_size_bits" + unfolding word_size_def word_size_bits_def by simp + +lemma word_bits_word_size_conv: + "word_bits = word_size * 8" + unfolding word_bits_def word_size_def by simp + lemma ucast_8_32_inj: "inj (ucast :: 8 word \ 32 word)" by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size) lemma upto_2_helper: "{0..<2 :: 32 word} = {0, 1}" by (safe; simp) unat_arith lemmas upper_bits_unset_is_l2p_32 = upper_bits_unset_is_l2p [where 'a=32, folded word_bits_def] lemmas le_2p_upper_bits_32 = le_2p_upper_bits [where 'a=32, folded word_bits_def] lemmas le2p_bits_unset_32 = le2p_bits_unset[where 'a=32, folded word_bits_def] lemma word_bits_len_of: "len_of TYPE (32) = word_bits" by (simp add: word_bits_conv) lemmas unat_power_lower32' = unat_power_lower[where 'a=32] lemmas unat_power_lower32 [simp] = unat_power_lower32'[unfolded word_bits_len_of] lemmas word32_less_sub_le' = word_less_sub_le[where 'a = 32] lemmas word32_less_sub_le[simp] = word32_less_sub_le' [folded word_bits_def] lemma word_bits_size: "size (w::word32) = word_bits" by (simp add: word_bits_def word_size) lemmas word32_power_less_1' = word_power_less_1[where 'a = 32] lemmas word32_power_less_1[simp] = word32_power_less_1'[folded word_bits_def] lemma of_nat32_0: "\of_nat n = (0::word32); n < 2 ^ word_bits\ \ n = 0" by (erule of_nat_0, simp add: word_bits_def) lemma unat_mask_2_less_4: "unat (p && mask 2 :: word32) < 4" apply (rule unat_less_helper) apply (rule order_le_less_trans, rule word_and_le1) apply (simp add: mask_eq) done lemmas unat_of_nat32' = unat_of_nat_eq[where 'a=32] lemmas unat_of_nat32 = unat_of_nat32'[unfolded word_bits_len_of] lemmas word_power_nonzero_32 = word_power_nonzero [where 'a=32, folded word_bits_def] lemmas unat_mult_simple = iffD1 [OF unat_mult_lem [where 'a = 32, unfolded word_bits_len_of]] lemmas div_power_helper_32 = div_power_helper [where 'a=32, folded word_bits_def] lemma n_less_word_bits: "(n < word_bits) = (n < 32)" by (simp add: word_bits_def) lemmas of_nat_less_pow_32 = of_nat_power [where 'a=32, folded word_bits_def] lemma lt_word_bits_lt_pow: "sz < word_bits \ sz < 2 ^ word_bits" by (simp add: word_bits_conv) lemma unat_less_word_bits: fixes y :: word32 shows "x < unat y \ x < 2 ^ word_bits" unfolding word_bits_def by (rule order_less_trans [OF _ unat_lt2p]) lemmas unat_mask_word32' = unat_mask[where 'a=32] lemmas unat_mask_word32 = unat_mask_word32'[folded word_bits_def] lemma unat_less_2p_word_bits: "unat (x :: 32 word) < 2 ^ word_bits" apply (simp only: word_bits_def) apply (rule unat_lt2p) done lemma Suc_unat_mask_div: "Suc (unat (mask sz div word_size::word32)) = 2 ^ (min sz word_bits - 2)" apply (case_tac "sz < word_bits") apply (case_tac "2 \ sz") apply (clarsimp simp: word_size_def word_bits_def min_def mask_eq) apply (drule (2) Suc_div_unat_helper [where 'a=32 and sz=sz and us=2, simplified, symmetric]) apply (simp add: not_le word_size_def word_bits_def) apply (case_tac sz, simp add: unat_word_ariths) apply (case_tac nat, simp add: unat_word_ariths unat_mask_word32 min_def word_bits_def) apply simp apply (simp add: unat_word_ariths unat_mask_word32 min_def word_bits_def word_size_def) done lemmas word32_minus_one_le' = word_minus_one_le[where 'a=32] lemmas word32_minus_one_le = word32_minus_one_le'[simplified] lemma ucast_not_helper: fixes a::word8 assumes a: "a \ 0xFF" shows "ucast a \ (0xFF::word32)" proof assume "ucast a = (0xFF::word32)" also have "(0xFF::word32) = ucast (0xFF::word8)" by simp finally show False using a apply - apply (drule up_ucast_inj, simp) apply simp done qed lemma less_4_cases: "(x::word32) < 4 \ x=0 \ x=1 \ x=2 \ x=3" apply clarsimp apply (drule word_less_cases, erule disjE, simp, simp)+ done lemma unat_ucast_8_32: fixes x :: "word8" shows "unat (ucast x :: word32) = unat x" by transfer simp lemma if_then_1_else_0: "((if P then 1 else 0) = (0 :: word32)) = (\ P)" by simp lemma if_then_0_else_1: "((if P then 0 else 1) = (0 :: word32)) = (P)" by simp lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0 lemma ucast_le_ucast_8_32: "(ucast x \ (ucast y :: word32)) = (x \ (y :: word8))" by (simp add: ucast_le_ucast) lemma in_16_range: "0 \ S \ r \ (\x. r + x * (16 :: word32)) ` S" "n - 1 \ S \ (r + (16 * n - 16)) \ (\x :: word32. r + x * 16) ` S" by (clarsimp simp: image_def elim!: bexI[rotated])+ lemma eq_2_32_0: "(2 ^ 32 :: word32) = 0" by simp lemma x_less_2_0_1: fixes x :: word32 shows "x < 2 \ x = 0 \ x = 1" by (rule x_less_2_0_1') auto lemmas mask_32_max_word = max_word_mask [symmetric, where 'a=32, simplified] lemma of_nat32_n_less_equal_power_2: "n < 32 \ ((of_nat n)::32 word) < 2 ^ n" by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size) lemma word_rsplit_0: "word_rsplit (0 :: word32) = [0, 0, 0, 0 :: word8]" by (simp add: word_rsplit_def bin_rsplit_def) lemma unat_ucast_10_32 : fixes x :: "10 word" shows "unat (ucast x :: word32) = unat x" by transfer simp lemma bool_mask [simp]: fixes x :: word32 shows "(0 < x && 1) = (x && 1 = 1)" by (rule bool_mask') auto lemma word32_bounds: "- (2 ^ (size (x :: word32) - 1)) = (-2147483648 :: int)" "((2 ^ (size (x :: word32) - 1)) - 1) = (2147483647 :: int)" "- (2 ^ (size (y :: 32 signed word) - 1)) = (-2147483648 :: int)" "((2 ^ (size (y :: 32 signed word) - 1)) - 1) = (2147483647 :: int)" by (simp_all add: word_size) lemma word_ge_min:"sint (x::32 word) \ -2147483648" by (metis sint_ge word32_bounds(1) word_size) lemmas signed_arith_ineq_checks_to_eq_word32' = signed_arith_ineq_checks_to_eq[where 'a=32] signed_arith_ineq_checks_to_eq[where 'a="32 signed"] lemmas signed_arith_ineq_checks_to_eq_word32 = signed_arith_ineq_checks_to_eq_word32' [unfolded word32_bounds] lemmas signed_mult_eq_checks32_to_64' = signed_mult_eq_checks_double_size[where 'a=32 and 'b=64] signed_mult_eq_checks_double_size[where 'a="32 signed" and 'b=64] lemmas signed_mult_eq_checks32_to_64 = signed_mult_eq_checks32_to_64'[simplified] lemmas sdiv_word32_max' = sdiv_word_max [where 'a=32] sdiv_word_max [where 'a="32 signed"] lemmas sdiv_word32_max = sdiv_word32_max'[simplified word_size, simplified] lemmas sdiv_word32_min' = sdiv_word_min [where 'a=32] sdiv_word_min [where 'a="32 signed"] lemmas sdiv_word32_min = sdiv_word32_min' [simplified word_size, simplified] lemmas sint32_of_int_eq' = sint_of_int_eq [where 'a=32] lemmas sint32_of_int_eq = sint32_of_int_eq' [simplified] lemma ucast_of_nats [simp]: "(ucast (of_nat x :: word32) :: sword32) = (of_nat x)" "(ucast (of_nat x :: word32) :: sword16) = (of_nat x)" "(ucast (of_nat x :: word32) :: sword8) = (of_nat x)" "(ucast (of_nat x :: word16) :: sword16) = (of_nat x)" "(ucast (of_nat x :: word16) :: sword8) = (of_nat x)" "(ucast (of_nat x :: word8) :: sword8) = (of_nat x)" by (simp_all add: of_nat_take_bit take_bit_word_eq_self) lemmas signed_shift_guard_simpler_32' = power_strict_increasing_iff[where b="2 :: nat" and y=31] lemmas signed_shift_guard_simpler_32 = signed_shift_guard_simpler_32'[simplified] lemma word32_31_less: "31 < len_of TYPE (32 signed)" "31 > (0 :: nat)" "31 < len_of TYPE (32)" "31 > (0 :: nat)" by auto lemmas signed_shift_guard_to_word_32 = signed_shift_guard_to_word[OF word32_31_less(1-2)] signed_shift_guard_to_word[OF word32_31_less(3-4)] lemma le_step_down_word_3: fixes x :: "32 word" shows "\x \ y; x \ y; y < 2 ^ 32 - 1\ \ x \ y - 1" by (rule le_step_down_word_2, assumption+) lemma shiftr_1: "(x::word32) >> 1 = 0 \ x < 2" by word_bitwise clarsimp lemma has_zero_byte: "~~ (((((v::word32) && 0x7f7f7f7f) + 0x7f7f7f7f) || v) || 0x7f7f7f7f) \ 0 \ v && 0xff000000 = 0 \ v && 0xff0000 = 0 \ v && 0xff00 = 0 \ v && 0xff = 0" apply clarsimp apply word_bitwise by metis lemma mask_step_down_32: \\x. mask x = b\ if \b && 1 = 1\ and \\x. x < 32 \ mask x = b >> 1\ for b :: \32word\ proof - from \b && 1 = 1\ have \odd b\ by (auto simp add: mod_2_eq_odd and_one_eq) then have \b mod 2 = 1\ using odd_iff_mod_2_eq_one by blast from \\x. x < 32 \ mask x = b >> 1\ obtain x where \x < 32\ \mask x = b >> 1\ by blast then have \mask x = b div 2\ using shiftr1_is_div_2 [of b] by simp with \b mod 2 = 1\ have \2 * mask x + 1 = 2 * (b div 2) + b mod 2\ by (simp only:) also have \\ = b\ by (simp add: mult_div_mod_eq) finally have \2 * mask x + 1 = b\ . moreover have \mask (Suc x) = 2 * mask x + (1 :: 'a::len word)\ by (simp add: mask_Suc_rec) ultimately show ?thesis by auto qed lemma unat_of_int_32: "\i \ 0; i \2 ^ 31\ \ (unat ((of_int i)::sword32)) = nat i" unfolding unat_eq_nat_uint apply (subst eq_nat_nat_iff) apply (auto simp add: take_bit_int_eq_self) done lemmas word_ctz_not_minus_1_32 = word_ctz_not_minus_1[where 'a=32, simplified] (* Helper for packing then unpacking a 64-bit variable. *) lemma cast_chunk_assemble_id_64[simp]: "(((ucast ((ucast (x::64 word))::32 word))::64 word) || (((ucast ((ucast (x >> 32))::32 word))::64 word) << 32)) = x" by (simp add:cast_chunk_assemble_id) (* Another variant of packing and unpacking a 64-bit variable. *) lemma cast_chunk_assemble_id_64'[simp]: "(((ucast ((scast (x::64 word))::32 word))::64 word) || (((ucast ((scast (x >> 32))::32 word))::64 word) << 32)) = x" by (simp add:cast_chunk_scast_assemble_id) (* Specialisations of down_cast_same for adding to local simpsets. *) lemma cast_down_u64: "(scast::64 word \ 32 word) = (ucast::64 word \ 32 word)" apply (subst down_cast_same[symmetric]) apply (simp add:is_down)+ done lemma cast_down_s64: "(scast::64 sword \ 32 word) = (ucast::64 sword \ 32 word)" apply (subst down_cast_same[symmetric]) apply (simp add:is_down)+ done end diff --git a/thys/Word_Lib/Word_Lemmas_64.thy b/thys/Word_Lib/Word_64.thy rename from thys/Word_Lib/Word_Lemmas_64.thy rename to thys/Word_Lib/Word_64.thy --- a/thys/Word_Lib/Word_Lemmas_64.thy +++ b/thys/Word_Lib/Word_64.thy @@ -1,295 +1,327 @@ (* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) -section "Lemmas for Word Length 64" +section "Words of Length 64" -theory Word_Lemmas_64 -imports - Word_Lemmas - Word_Setup_64 - Word_Syntax +theory Word_64 + imports + Word_Lemmas + Word_8 + Word_16 + Word_Syntax begin +type_synonym word64 = "64 word" +lemma len64: "len_of (x :: 64 itself) = 64" by simp + +type_synonym machine_word_len = 64 +type_synonym machine_word = "machine_word_len word" + +definition word_bits :: nat +where + "word_bits = LENGTH(machine_word_len)" + +text \The following two are numerals so they can be used as nats and words.\ +definition word_size_bits :: "'a :: numeral" +where + "word_size_bits = 3" + +definition word_size :: "'a :: numeral" +where + "word_size = 8" + +lemma word_bits_conv[code]: + "word_bits = 64" + unfolding word_bits_def by simp + +lemma word_size_word_size_bits: + "(word_size::nat) = 2 ^ word_size_bits" + unfolding word_size_def word_size_bits_def by simp + +lemma word_bits_word_size_conv: + "word_bits = word_size * 8" + unfolding word_bits_def word_size_def by simp + lemma ucast_8_64_inj: "inj (ucast :: 8 word \ 64 word)" by (rule down_ucast_inj) (clarsimp simp: is_down_def target_size source_size) lemma upto_2_helper: "{0..<2 :: 64 word} = {0, 1}" by (safe; simp) unat_arith lemmas upper_bits_unset_is_l2p_64 = upper_bits_unset_is_l2p [where 'a=64, folded word_bits_def] lemmas le_2p_upper_bits_64 = le_2p_upper_bits [where 'a=64, folded word_bits_def] lemmas le2p_bits_unset_64 = le2p_bits_unset[where 'a=64, folded word_bits_def] lemma word_bits_len_of: "len_of TYPE (64) = word_bits" by (simp add: word_bits_conv) lemmas unat_power_lower64' = unat_power_lower[where 'a=64] lemmas unat_power_lower64 [simp] = unat_power_lower64'[unfolded word_bits_len_of] lemmas word64_less_sub_le' = word_less_sub_le[where 'a = 64] lemmas word64_less_sub_le[simp] = word64_less_sub_le' [folded word_bits_def] lemma word_bits_size: "size (w::word64) = word_bits" by (simp add: word_bits_def word_size) lemmas word64_power_less_1' = word_power_less_1[where 'a = 64] lemmas word64_power_less_1[simp] = word64_power_less_1'[folded word_bits_def] lemma of_nat64_0: "\of_nat n = (0::word64); n < 2 ^ word_bits\ \ n = 0" by (erule of_nat_0, simp add: word_bits_def) lemma unat_mask_2_less_4: "unat (p && mask 2 :: word64) < 4" apply (rule unat_less_helper) apply (rule order_le_less_trans, rule word_and_le1) apply (simp add: mask_eq) done lemmas unat_of_nat64' = unat_of_nat_eq[where 'a=64] lemmas unat_of_nat64 = unat_of_nat64'[unfolded word_bits_len_of] lemmas word_power_nonzero_64 = word_power_nonzero [where 'a=64, folded word_bits_def] lemmas unat_mult_simple = iffD1 [OF unat_mult_lem [where 'a = 64, unfolded word_bits_len_of]] lemmas div_power_helper_64 = div_power_helper [where 'a=64, folded word_bits_def] lemma n_less_word_bits: "(n < word_bits) = (n < 64)" by (simp add: word_bits_def) lemmas of_nat_less_pow_64 = of_nat_power [where 'a=64, folded word_bits_def] lemma lt_word_bits_lt_pow: "sz < word_bits \ sz < 2 ^ word_bits" by (simp add: word_bits_conv) lemma unat_less_word_bits: fixes y :: word64 shows "x < unat y \ x < 2 ^ word_bits" unfolding word_bits_def by (rule order_less_trans [OF _ unat_lt2p]) lemmas unat_mask_word64' = unat_mask[where 'a=64] lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def] lemma unat_less_2p_word_bits: "unat (x :: 64 word) < 2 ^ word_bits" apply (simp only: word_bits_def) apply (rule unat_lt2p) done lemma Suc_unat_mask_div: "Suc (unat (mask sz div word_size::word64)) = 2 ^ (min sz word_bits - 3)" apply (case_tac "sz < word_bits") apply (case_tac "3 \ sz") apply (clarsimp simp: word_size_def word_bits_def min_def mask_eq) apply (drule (2) Suc_div_unat_helper [where 'a=64 and sz=sz and us=3, simplified, symmetric]) apply (simp add: not_le word_size_def word_bits_def) apply (case_tac sz, simp add: unat_word_ariths) apply (case_tac nat, simp add: unat_word_ariths unat_mask_word64 min_def word_bits_def) apply (case_tac nata, simp add: unat_word_ariths unat_mask_word64 word_bits_def) apply simp apply (simp add: unat_word_ariths unat_mask_word64 min_def word_bits_def word_size_def) done lemmas word64_minus_one_le' = word_minus_one_le[where 'a=64] lemmas word64_minus_one_le = word64_minus_one_le'[simplified] lemma ucast_not_helper: fixes a::word8 assumes a: "a \ 0xFF" shows "ucast a \ (0xFF::word64)" proof assume "ucast a = (0xFF::word64)" also have "(0xFF::word64) = ucast (0xFF::word8)" by simp finally show False using a apply - apply (drule up_ucast_inj, simp) apply simp done qed lemma less_4_cases: "(x::word64) < 4 \ x=0 \ x=1 \ x=2 \ x=3" apply clarsimp apply (drule word_less_cases, erule disjE, simp, simp)+ done lemma if_then_1_else_0: "((if P then 1 else 0) = (0 :: word64)) = (\ P)" by simp lemma if_then_0_else_1: "((if P then 0 else 1) = (0 :: word64)) = (P)" by simp lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0 lemma ucast_le_ucast_8_64: "(ucast x \ (ucast y :: word64)) = (x \ (y :: word8))" by (simp add: ucast_le_ucast) lemma in_16_range: "0 \ S \ r \ (\x. r + x * (16 :: word64)) ` S" "n - 1 \ S \ (r + (16 * n - 16)) \ (\x :: word64. r + x * 16) ` S" by (clarsimp simp: image_def elim!: bexI[rotated])+ lemma eq_2_64_0: "(2 ^ 64 :: word64) = 0" by simp lemma x_less_2_0_1: fixes x :: word64 shows "x < 2 \ x = 0 \ x = 1" by (rule x_less_2_0_1') auto lemmas mask_64_max_word = max_word_mask [symmetric, where 'a=64, simplified] lemma of_nat64_n_less_equal_power_2: "n < 64 \ ((of_nat n)::64 word) < 2 ^ n" by (rule of_nat_n_less_equal_power_2, clarsimp simp: word_size) lemma word_rsplit_0: "word_rsplit (0 :: word64) = [0, 0, 0, 0, 0, 0, 0, 0 :: word8]" by (simp add: word_rsplit_def bin_rsplit_def) lemma unat_ucast_10_64 : fixes x :: "10 word" shows "unat (ucast x :: word64) = unat x" by transfer simp lemma bool_mask [simp]: fixes x :: word64 shows "(0 < x && 1) = (x && 1 = 1)" by (rule bool_mask') auto lemma word64_bounds: "- (2 ^ (size (x :: word64) - 1)) = (-9223372036854775808 :: int)" "((2 ^ (size (x :: word64) - 1)) - 1) = (9223372036854775807 :: int)" "- (2 ^ (size (y :: 64 signed word) - 1)) = (-9223372036854775808 :: int)" "((2 ^ (size (y :: 64 signed word) - 1)) - 1) = (9223372036854775807 :: int)" by (simp_all add: word_size) lemma word_ge_min:"sint (x::64 word) \ -9223372036854775808" by (metis sint_ge word64_bounds(1) word_size) lemmas signed_arith_ineq_checks_to_eq_word64' = signed_arith_ineq_checks_to_eq[where 'a=64] signed_arith_ineq_checks_to_eq[where 'a="64 signed"] lemmas signed_arith_ineq_checks_to_eq_word64 = signed_arith_ineq_checks_to_eq_word64' [unfolded word64_bounds] lemmas signed_mult_eq_checks64_to_64' = signed_mult_eq_checks_double_size[where 'a=64 and 'b=64] signed_mult_eq_checks_double_size[where 'a="64 signed" and 'b=64] lemmas signed_mult_eq_checks64_to_64 = signed_mult_eq_checks64_to_64'[simplified] lemmas sdiv_word64_max' = sdiv_word_max [where 'a=64] sdiv_word_max [where 'a="64 signed"] lemmas sdiv_word64_max = sdiv_word64_max'[simplified word_size, simplified] lemmas sdiv_word64_min' = sdiv_word_min [where 'a=64] sdiv_word_min [where 'a="64 signed"] lemmas sdiv_word64_min = sdiv_word64_min' [simplified word_size, simplified] lemmas sint64_of_int_eq' = sint_of_int_eq [where 'a=64] lemmas sint64_of_int_eq = sint64_of_int_eq' [simplified] lemma ucast_of_nats [simp]: "(ucast (of_nat x :: word64) :: sword64) = (of_nat x)" "(ucast (of_nat x :: word64) :: sword16) = (of_nat x)" "(ucast (of_nat x :: word64) :: sword8) = (of_nat x)" "(ucast (of_nat x :: word16) :: sword16) = (of_nat x)" "(ucast (of_nat x :: word16) :: sword8) = (of_nat x)" "(ucast (of_nat x :: word8) :: sword8) = (of_nat x)" by (simp_all add: of_nat_take_bit take_bit_word_eq_self) lemmas signed_shift_guard_simpler_64' = power_strict_increasing_iff[where b="2 :: nat" and y=31] lemmas signed_shift_guard_simpler_64 = signed_shift_guard_simpler_64'[simplified] lemma word64_31_less: "31 < len_of TYPE (64 signed)" "31 > (0 :: nat)" "31 < len_of TYPE (64)" "31 > (0 :: nat)" by auto lemmas signed_shift_guard_to_word_64 = signed_shift_guard_to_word[OF word64_31_less(1-2)] signed_shift_guard_to_word[OF word64_31_less(3-4)] lemma le_step_down_word_3: fixes x :: "64 word" shows "\x \ y; x \ y; y < 2 ^ 64 - 1\ \ x \ y - 1" by (rule le_step_down_word_2, assumption+) lemma shiftr_1: "(x::word64) >> 1 = 0 \ x < 2" by word_bitwise clarsimp lemma mask_step_down_64: \\x. mask x = b\ if \b && 1 = 1\ and \\x. x < 64 \ mask x = b >> 1\ for b :: \64word\ proof - from \b && 1 = 1\ have \odd b\ by (auto simp add: mod_2_eq_odd and_one_eq) then have \b mod 2 = 1\ using odd_iff_mod_2_eq_one by blast from \\x. x < 64 \ mask x = b >> 1\ obtain x where \x < 64\ \mask x = b >> 1\ by blast then have \mask x = b div 2\ using shiftr1_is_div_2 [of b] by simp with \b mod 2 = 1\ have \2 * mask x + 1 = 2 * (b div 2) + b mod 2\ by (simp only:) also have \\ = b\ by (simp add: mult_div_mod_eq) finally have \2 * mask x + 1 = b\ . moreover have \mask (Suc x) = 2 * mask x + (1 :: 'a::len word)\ by (simp add: mask_Suc_rec) ultimately show ?thesis by auto qed lemma unat_of_int_64: "\i \ 0; i \ 2 ^ 63\ \ (unat ((of_int i)::sword64)) = nat i" unfolding unat_eq_nat_uint apply (subst eq_nat_nat_iff) apply (simp_all add: take_bit_int_eq_self) done lemmas word_ctz_not_minus_1_64 = word_ctz_not_minus_1[where 'a=64, simplified] (* Helper for packing then unpacking a 64-bit variable. *) lemma cast_chunk_assemble_id_64[simp]: "(((ucast ((ucast (x::64 word))::32 word))::64 word) || (((ucast ((ucast (x >> 32))::32 word))::64 word) << 32)) = x" by (simp add:cast_chunk_assemble_id) (* Another variant of packing and unpacking a 64-bit variable. *) lemma cast_chunk_assemble_id_64'[simp]: "(((ucast ((scast (x::64 word))::32 word))::64 word) || (((ucast ((scast (x >> 32))::32 word))::64 word) << 32)) = x" by (simp add:cast_chunk_scast_assemble_id) (* Specialisations of down_cast_same for adding to local simpsets. *) lemma cast_down_u64: "(scast::64 word \ 32 word) = (ucast::64 word \ 32 word)" apply (subst down_cast_same[symmetric]) apply (simp add:is_down)+ done lemma cast_down_s64: "(scast::64 sword \ 32 word) = (ucast::64 sword \ 32 word)" apply (subst down_cast_same[symmetric]) apply (simp add:is_down)+ done end diff --git a/thys/Word_Lib/Word_8.thy b/thys/Word_Lib/Word_8.thy new file mode 100644 --- /dev/null +++ b/thys/Word_Lib/Word_8.thy @@ -0,0 +1,18 @@ +(* + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +section "Words of Length 8" + +theory Word_8 +imports + Word_Lemmas + Word_Syntax +begin + +type_synonym word8 = "8 word" +lemma len8: "len_of (x :: 8 itself) = 8" by simp + +end diff --git a/thys/Word_Lib/Word_Lib_Sumo.thy b/thys/Word_Lib/Word_Lib_Sumo.thy --- a/thys/Word_Lib/Word_Lib_Sumo.thy +++ b/thys/Word_Lib/Word_Lib_Sumo.thy @@ -1,84 +1,84 @@ section \Ancient comprehensive Word Library\ theory Word_Lib_Sumo imports "HOL-Library.Word" Aligned Ancient_Numeral Bit_Comprehension Bits_Int Bitwise_Signed Bitwise Enumeration_Word Generic_set_bit Hex_Words Least_significant_bit More_Arithmetic More_Divides More_List More_Misc Strict_part_mono Most_significant_bit Next_and_Prev Norm_Words Reversed_Bit_Lists Rsplit Signed_Words Traditional_Infix_Syntax Typedef_Morphisms Type_Syntax Word_EqI - Word_Lemmas_32 - Word_Lemmas_64 + Word_Lib Word_Lemmas - Word_Lib - Word_Setup_32 - Word_Setup_64 + Word_8 + Word_16 + Word_32 + Word_64 Word_Syntax begin declare signed_take_bit_Suc [simp] lemmas bshiftr1_def = bshiftr1_eq lemmas is_down_def = is_down_eq lemmas is_up_def = is_up_eq lemmas mask_def = mask_eq_decr_exp lemmas scast_def = scast_eq lemmas shiftl1_def = shiftl1_eq lemmas shiftr1_def = shiftr1_eq lemmas sshiftr1_def = sshiftr1_eq lemmas sshiftr_def = sshiftr_eq_funpow_sshiftr1 lemmas to_bl_def = to_bl_eq lemmas ucast_def = ucast_eq lemmas unat_def = unat_eq_nat_uint lemmas word_cat_def = word_cat_eq lemmas word_reverse_def = word_reverse_eq_of_bl_rev_to_bl lemmas word_roti_def = word_roti_eq_word_rotr_word_rotl lemmas word_rotl_def = word_rotl_eq lemmas word_rotr_def = word_rotr_eq lemmas word_sle_def = word_sle_eq lemmas word_sless_def = word_sless_eq lemmas uint_0 = uint_nonnegative lemmas uint_lt = uint_bounded lemmas uint_mod_same = uint_idem lemmas of_nth_def = word_set_bits_def lemmas of_nat_word_eq_iff = word_of_nat_eq_iff lemmas of_nat_word_eq_0_iff = word_of_nat_eq_0_iff lemmas of_int_word_eq_iff = word_of_int_eq_iff lemmas of_int_word_eq_0_iff = word_of_int_eq_0_iff lemmas word_next_def = word_next_unfold lemmas word_prev_def = word_prev_unfold lemmas is_aligned_def = is_aligned_iff_dvd_nat lemma shiftl_transfer [transfer_rule]: includes lifting_syntax shows "(pcr_word ===> (=) ===> pcr_word) (<<) (<<)" by (unfold shiftl_eq_push_bit) transfer_prover end diff --git a/thys/Word_Lib/Word_Setup_32.thy b/thys/Word_Lib/Word_Setup_32.thy --- a/thys/Word_Lib/Word_Setup_32.thy +++ b/thys/Word_Lib/Word_Setup_32.thy @@ -1,43 +1,16 @@ (* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section "32-Bit Machine Word Setup" theory Word_Setup_32 imports "HOL-Library.Word" begin text \This theory defines standard platform-specific word size and alignment.\ -type_synonym machine_word_len = 32 -type_synonym machine_word = "machine_word_len word" - -definition word_bits :: nat -where - "word_bits = LENGTH(machine_word_len)" - -text \The following two are numerals so they can be used as nats and words.\ -definition word_size_bits :: "'a :: numeral" -where - "word_size_bits = 2" - -definition word_size :: "'a :: numeral" -where - "word_size = 4" - -lemma word_bits_conv[code]: - "word_bits = 32" - unfolding word_bits_def by simp - -lemma word_size_word_size_bits: - "(word_size::nat) = 2 ^ word_size_bits" - unfolding word_size_def word_size_bits_def by simp - -lemma word_bits_word_size_conv: - "word_bits = word_size * 8" - unfolding word_bits_def word_size_def by simp end diff --git a/thys/Word_Lib/Word_Setup_64.thy b/thys/Word_Lib/Word_Setup_64.thy --- a/thys/Word_Lib/Word_Setup_64.thy +++ b/thys/Word_Lib/Word_Setup_64.thy @@ -1,43 +1,15 @@ (* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section "64-Bit Machine Word Setup" theory Word_Setup_64 imports "HOL-Library.Word" begin text \This theory defines standard platform-specific word size and alignment.\ -type_synonym machine_word_len = 64 -type_synonym machine_word = "machine_word_len word" - -definition word_bits :: nat -where - "word_bits = LENGTH(machine_word_len)" - -text \The following two are numerals so they can be used as nats and words.\ -definition word_size_bits :: "'a :: numeral" -where - "word_size_bits = 3" - -definition word_size :: "'a :: numeral" -where - "word_size = 8" - -lemma word_bits_conv[code]: - "word_bits = 64" - unfolding word_bits_def by simp - -lemma word_size_word_size_bits: - "(word_size::nat) = 2 ^ word_size_bits" - unfolding word_size_def word_size_bits_def by simp - -lemma word_bits_word_size_conv: - "word_bits = word_size * 8" - unfolding word_bits_def word_size_def by simp - end diff --git a/thys/Word_Lib/Word_Syntax.thy b/thys/Word_Lib/Word_Syntax.thy --- a/thys/Word_Lib/Word_Syntax.thy +++ b/thys/Word_Lib/Word_Syntax.thy @@ -1,47 +1,36 @@ (* * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) section "Additional Syntax for Word Bit Operations" theory Word_Syntax imports "HOL-Library.Word" - Bitwise begin text \Additional bit and type syntax that forces word types.\ -type_synonym word8 = "8 word" -type_synonym word16 = "16 word" -type_synonym word32 = "32 word" -type_synonym word64 = "64 word" - -lemma len8: "len_of (x :: 8 itself) = 8" by simp -lemma len16: "len_of (x :: 16 itself) = 16" by simp -lemma len32: "len_of (x :: 32 itself) = 32" by simp -lemma len64: "len_of (x :: 64 itself) = 64" by simp - abbreviation wordNOT :: "'a::len word \ 'a word" ("~~ _" [70] 71) where "~~ x == NOT x" abbreviation wordAND :: "'a::len word \ 'a word \ 'a word" (infixr "&&" 64) where "a && b == a AND b" abbreviation wordOR :: "'a::len word \ 'a word \ 'a word" (infixr "||" 59) where "a || b == a OR b" abbreviation wordXOR :: "'a::len word \ 'a word \ 'a word" (infixr "xor" 59) where "a xor b == a XOR b" end