diff --git a/thys/Native_Word/Code_Target_Word_Base.thy b/thys/Native_Word/Code_Target_Word_Base.thy --- a/thys/Native_Word/Code_Target_Word_Base.thy +++ b/thys/Native_Word/Code_Target_Word_Base.thy @@ -1,398 +1,386 @@ (* Title: Code_Target_Word_Base.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Common base for target language implementations of word types\ theory Code_Target_Word_Base imports "HOL-Library.Word" "Word_Lib.Signed_Division_Word" "Word_Lib.More_Word" begin subsection \More on conversions\ lemma int_of_integer_unsigned_eq [simp]: \int_of_integer (unsigned w) = uint w\ by transfer simp lemma int_of_integer_signed_eq [simp]: \int_of_integer (signed w) = sint w\ by transfer simp -context - includes integer.lifting -begin - -lift_definition word_of_integer :: "integer \ 'a :: len word" is word_of_int . - -lemma word_of_integer_code [code]: "word_of_integer n = word_of_int (int_of_integer n)" - by (fact word_of_integer.rep_eq) - -end - -lemma word_of_int_of_integer_eq [simp]: - \word_of_int (int_of_integer k) = word_of_integer k\ - by (simp add: word_of_integer.rep_eq) +abbreviation word_of_integer :: \integer \ 'a::len word\ + where \word_of_integer k \ word_of_int (int_of_integer k)\ subsection \Quickcheck conversion functions\ context includes state_combinator_syntax begin definition qc_random_cnv :: "(natural \ 'a::term_of) \ natural \ Random.seed \ ('a \ (unit \ Code_Evaluation.term)) \ Random.seed" where "qc_random_cnv a_of_natural i = Random.range (i + 1) \\ (\k. Pair ( let n = a_of_natural k in (n, \_. Code_Evaluation.term_of n)))" end definition qc_exhaustive_cnv :: "(natural \ 'a) \ ('a \ (bool \ term list) option) \ natural \ (bool \ term list) option" where "qc_exhaustive_cnv a_of_natural f d = Quickcheck_Exhaustive.exhaustive (%x. f (a_of_natural x)) d" definition qc_full_exhaustive_cnv :: "(natural \ ('a::term_of)) \ ('a \ (unit \ term) \ (bool \ term list) option) \ natural \ (bool \ term list) option" where "qc_full_exhaustive_cnv a_of_natural f d = Quickcheck_Exhaustive.full_exhaustive (%(x, xt). f (a_of_natural x, %_. Code_Evaluation.term_of (a_of_natural x))) d" declare [[quickcheck_narrowing_ghc_options = "-XTypeSynonymInstances"]] definition qc_narrowing_drawn_from :: "'a list \ integer \ _" where "qc_narrowing_drawn_from xs = foldr Quickcheck_Narrowing.sum (map Quickcheck_Narrowing.cons (butlast xs)) (Quickcheck_Narrowing.cons (last xs))" locale quickcheck_narrowing_samples = fixes a_of_integer :: "integer \ 'a \ 'a :: {partial_term_of, term_of}" and zero :: "'a" and tr :: "typerep" begin function narrowing_samples :: "integer \ 'a list" where "narrowing_samples i = (if i > 0 then let (a, a') = a_of_integer i in narrowing_samples (i - 1) @ [a, a'] else [zero])" by pat_completeness auto termination including integer.lifting proof(relation "measure nat_of_integer") fix i :: integer assume "0 < i" thus "(i - 1, i) \ measure nat_of_integer" by simp(transfer, simp) qed simp definition partial_term_of_sample :: "integer \ 'a" where "partial_term_of_sample i = (if i < 0 then undefined else if i = 0 then zero else if i mod 2 = 0 then snd (a_of_integer (i div 2)) else fst (a_of_integer (i div 2 + 1)))" lemma partial_term_of_code: "partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_variable p t) \ Code_Evaluation.Free (STR ''_'') tr" "partial_term_of (ty :: 'a itself) (Quickcheck_Narrowing.Narrowing_constructor i []) \ Code_Evaluation.term_of (partial_term_of_sample i)" by (rule partial_term_of_anything)+ end lemmas [code] = quickcheck_narrowing_samples.narrowing_samples.simps quickcheck_narrowing_samples.partial_term_of_sample_def subsection \More on division\ lemma div_half_nat: fixes x y :: nat assumes "y \ 0" shows "(x div y, x mod y) = (let q = 2 * (x div 2 div y); r = x - q * y in if y \ r then (q + 1, r - y) else (q, r))" proof - let ?q = "2 * (x div 2 div y)" have q: "?q = x div y - x div y mod 2" by(metis div_mult2_eq mult.commute minus_mod_eq_mult_div [symmetric]) let ?r = "x - ?q * y" have r: "?r = x mod y + x div y mod 2 * y" by(simp add: q diff_mult_distrib minus_mod_eq_div_mult [symmetric])(metis diff_diff_cancel mod_less_eq_dividend mod_mult2_eq add.commute mult.commute) show ?thesis proof(cases "y \ x - ?q * y") case True with assms q have "x div y mod 2 \ 0" unfolding r by (metis Nat.add_0_right diff_0_eq_0 diff_Suc_1 le_div_geq mod2_gr_0 mod_div_trivial mult_0 neq0_conv numeral_1_eq_Suc_0 numerals(1)) hence "x div y = ?q + 1" unfolding q by simp moreover hence "x mod y = ?r - y" by simp(metis minus_div_mult_eq_mod [symmetric] diff_commute diff_diff_left mult_Suc) ultimately show ?thesis using True by(simp add: Let_def) next case False hence "x div y mod 2 = 0" unfolding r by(simp add: not_le)(metis Nat.add_0_right assms div_less div_mult_self2 mod_div_trivial mult.commute) hence "x div y = ?q" unfolding q by simp moreover hence "x mod y = ?r" by (metis minus_div_mult_eq_mod [symmetric]) ultimately show ?thesis using False by(simp add: Let_def) qed qed lemma div_half_word: fixes x y :: "'a :: len word" assumes "y \ 0" shows "(x div y, x mod y) = (let q = push_bit 1 (drop_bit 1 x div y); r = x - q * y in if y \ r then (q + 1, r - y) else (q, r))" proof - obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)" by (rule that [of \unat x\]) simp_all moreover obtain m where m: "y = of_nat m" "m < 2 ^ LENGTH('a)" by (rule that [of \unat y\]) simp_all ultimately have [simp]: \unat (of_nat n :: 'a word) = n\ \unat (of_nat m :: 'a word) = m\ by (transfer, simp add: take_bit_of_nat take_bit_nat_eq_self_iff)+ let ?q = "push_bit 1 (drop_bit 1 x div y)" let ?q' = "2 * (n div 2 div m)" have "n div 2 div m < 2 ^ LENGTH('a)" using n by (metis of_nat_inverse uno_simps(2) unsigned_less) hence q: "?q = of_nat ?q'" using n m by (auto simp add: drop_bit_eq_div word_arith_nat_div uno_simps take_bit_nat_eq_self unsigned_of_nat) from assms have "m \ 0" using m by -(rule notI, simp) from n have "2 * (n div 2 div m) < 2 ^ LENGTH('a)" by (metis mult.commute div_mult2_eq minus_mod_eq_mult_div [symmetric] less_imp_diff_less of_nat_inverse unsigned_less uno_simps(2)) moreover have "2 * (n div 2 div m) * m < 2 ^ LENGTH('a)" using n unfolding div_mult2_eq[symmetric] by(subst (2) mult.commute)(simp add: minus_mod_eq_div_mult [symmetric] diff_mult_distrib minus_mod_eq_mult_div [symmetric] div_mult2_eq) moreover have "2 * (n div 2 div m) * m \ n" by (simp flip: div_mult2_eq ac_simps) ultimately have r: "x - ?q * y = of_nat (n - ?q' * m)" and "y \ x - ?q * y \ of_nat (n - ?q' * m) - y = of_nat (n - ?q' * m - m)" using n m unfolding q apply (simp_all add: of_nat_diff) apply (subst of_nat_diff) apply (cases \LENGTH('a) \ 2\) apply (simp_all add: word_le_nat_alt take_bit_nat_eq_self unat_sub_if' unat_word_ariths unsigned_of_nat) done then show ?thesis using n m div_half_nat [OF \m \ 0\, of n] unfolding q by (simp add: word_le_nat_alt word_div_def word_mod_def Let_def take_bit_nat_eq_self unsigned_of_nat flip: zdiv_int zmod_int split del: if_split split: if_split_asm) qed text \Division on @{typ "'a word"} is unsigned, but Scala and OCaml only have signed division and modulus.\ lemma [code]: "x sdiv y = (let x' = sint x; y' = sint y; negative = (x' < 0) \ (y' < 0); result = abs x' div abs y' in word_of_int (if negative then -result else result))" for x y :: \'a::len word\ by (simp add: sdiv_word_def signed_divide_int_def sgn_if Let_def not_less not_le) lemma [code]: "x smod y = (let x' = sint x; y' = sint y; negative = (x' < 0); result = abs x' mod abs y' in word_of_int (if negative then -result else result))" for x y :: \'a::len word\ proof - have *: \k mod l = k - k div l * l\ for k l :: int by (simp add: minus_div_mult_eq_mod) show ?thesis by (simp add: smod_word_def signed_modulo_int_def signed_divide_int_def * sgn_if Let_def) qed text \ This algorithm implements unsigned division in terms of signed division. Taken from Hacker's Delight. \ lemma divmod_via_sdivmod: fixes x y :: "'a :: len word" assumes "y \ 0" shows "(x div y, x mod y) = (if push_bit (LENGTH('a) - 1) 1 \ y then if x < y then (0, x) else (1, x - y) else let q = (push_bit 1 (drop_bit 1 x sdiv y)); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" proof(cases "push_bit (LENGTH('a) - 1) 1 \ y") case True note y = this show ?thesis proof(cases "x < y") case True then have "x mod y = x" by transfer simp then show ?thesis using True y using bits_mod_div_trivial [of x y] by simp next case False obtain n where n: "y = of_nat n" "n < 2 ^ LENGTH('a)" by (rule that [of \unat y\]) simp_all have "unat x < 2 ^ LENGTH('a)" by (rule unsigned_less) also have "\ = 2 * 2 ^ (LENGTH('a) - 1)" by(metis Suc_pred len_gt_0 power_Suc One_nat_def) also have "\ \ 2 * n" using y n by transfer (simp add: take_bit_eq_mod) finally have div: "x div of_nat n = 1" using False n by (simp add: take_bit_nat_eq_self unsigned_of_nat word_div_eq_1_iff) moreover have "x mod y = x - x div y * y" by (simp add: minus_div_mult_eq_mod) with div n have "x mod y = x - y" by simp ultimately show ?thesis using False y n by simp qed next case False note y = this obtain n where n: "x = of_nat n" "n < 2 ^ LENGTH('a)" by (rule that [of \unat x\]) simp_all hence "int n div 2 + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)" by (cases \LENGTH('a)\) (auto dest: less_imp_of_nat_less [where ?'a = int]) with y n have "sint (drop_bit 1 x) = uint (drop_bit 1 x)" by (cases \LENGTH('a)\) (auto simp add: sint_uint drop_bit_eq_div take_bit_nat_eq_self uint_div_distrib signed_take_bit_int_eq_self_iff unsigned_of_nat) moreover have "uint y + 2 ^ (LENGTH('a) - Suc 0) < 2 ^ LENGTH('a)" using y by (cases \LENGTH('a)\) (simp_all add: not_le word_less_alt uint_power_lower) then have "sint y = uint y" apply (cases \LENGTH('a)\) apply (auto simp add: sint_uint signed_take_bit_int_eq_self_iff) using uint_ge_0 [of y] by linarith ultimately show ?thesis using y apply (subst div_half_word [OF assms]) apply (simp add: sdiv_word_def signed_divide_int_def flip: uint_div) done qed subsection \More on misc operations\ context includes bit_operations_syntax begin lemma word_of_int_code: "uint (word_of_int x :: 'a word) = x AND mask (LENGTH('a :: len))" by (simp add: unsigned_of_int take_bit_eq_mask) lemma word_and_mask_or_conv_and_mask: "bit n index \ (n AND mask index) OR (push_bit index 1) = n AND mask (index + 1)" for n :: \'a::len word\ by (rule bit_eqI) (auto simp add: bit_simps) lemma uint_and_mask_or_full: fixes n :: "'a :: len word" assumes "bit n (LENGTH('a) - 1)" and "mask1 = mask (LENGTH('a) - 1)" and "mask2 = push_bit (LENGTH('a) - 1) 1" shows "uint (n AND mask1) OR mask2 = uint n" proof - have "mask2 = uint (push_bit (LENGTH('a) - 1) 1 :: 'a word)" using assms by transfer (simp add: take_bit_push_bit) hence "uint (n AND mask1) OR mask2 = uint (n AND mask1 OR (push_bit (LENGTH('a) - 1) 1 :: 'a word))" by(simp add: uint_or) also have "\ = uint (n AND mask (LENGTH('a) - 1 + 1))" using assms by(simp only: word_and_mask_or_conv_and_mask) also have "\ = uint n" by simp finally show ?thesis . qed lemma word_of_int_via_signed: fixes mask assumes mask_def: "mask = Bit_Operations.mask LENGTH('a)" and shift_def: "shift = push_bit LENGTH('a) 1" and index_def: "index = LENGTH('a) - 1" and overflow_def:"overflow = push_bit (LENGTH('a) - 1) 1" and least_def: "least = - overflow" shows "(word_of_int i :: 'a :: len word) = (let i' = i AND mask in if bit i' index then if i' - shift < least \ overflow \ i' - shift then arbitrary1 i' else word_of_int (i' - shift) else if i' < least \ overflow \ i' then arbitrary2 i' else word_of_int i')" proof - define i' where "i' = i AND mask" have "shift = mask + 1" unfolding assms by (simp add: mask_eq_exp_minus_1) hence "i' < shift" by (simp add: mask_def i'_def) show ?thesis proof(cases "bit i' index") case True then have unf: "i' = overflow OR i'" apply (simp add: assms i'_def flip: take_bit_eq_mask) apply (rule bit_eqI) apply (auto simp add: bit_take_bit_iff bit_or_iff bit_exp_iff) done have \overflow \ overflow OR i'\ by (simp add: i'_def mask_def or_greater_eq) then have "overflow \ i'" by (subst unf) hence "i' - shift < least \ False" unfolding assms by(cases "LENGTH('a)")(simp_all add: not_less) moreover have "overflow \ i' - shift \ False" using \i' < shift\ unfolding assms by(cases "LENGTH('a)")(auto simp add: not_le elim: less_le_trans) moreover have "word_of_int (i' - shift) = (word_of_int i :: 'a word)" using \i' < shift\ by (simp add: i'_def shift_def mask_def word_of_int_eq_iff flip: take_bit_eq_mask) ultimately show ?thesis using True by(simp add: Let_def i'_def) next case False have "i' = i AND Bit_Operations.mask (LENGTH('a) - 1)" apply (rule bit_eqI) apply (use False in \auto simp add: bit_simps assms i'_def\) apply (auto simp add: less_le) done also have "\ \ Bit_Operations.mask (LENGTH('a) - 1)" using AND_upper2 mask_nonnegative_int by blast also have "\ < overflow" by (simp add: mask_int_def overflow_def) also have "least \ 0" unfolding least_def overflow_def by simp have "0 \ i'" by (simp add: i'_def mask_def) hence "least \ i'" using \least \ 0\ by simp moreover have "word_of_int i' = (word_of_int i :: 'a word)" by (simp add: i'_def mask_def of_int_and_eq of_int_mask_eq) ultimately show ?thesis using False by(simp add: Let_def i'_def) qed qed end subsection \Code generator setup\ text \ The separate code target \SML_word\ collects setups for the code generator that PolyML does not provide. \ setup \Code_Target.add_derived_target ("SML_word", [(Code_ML.target_SML, I)])\ code_identifier code_module Code_Target_Word_Base \ (SML) Word and (Haskell) Word and (OCaml) Word and (Scala) Word text \Misc\ lemmas word_sdiv_def = sdiv_word_def lemmas word_smod_def = smod_word_def end diff --git a/thys/Native_Word/Uint.thy b/thys/Native_Word/Uint.thy --- a/thys/Native_Word/Uint.thy +++ b/thys/Native_Word/Uint.thy @@ -1,825 +1,824 @@ (* Title: Uint.thy Author: Peter Lammich, TU Munich Author: Andreas Lochbihler, ETH Zurich *) chapter \Unsigned words of default size\ theory Uint imports Word_Type_Copies Code_Target_Integer_Bit begin text \ This theory provides access to words in the target languages of the code generator whose bit width is the default of the target language. To that end, the type \uint\ models words of width \dflt_size\, but \dflt_size\ is known only to be positive. Usage restrictions: Default-size words (type \uint\) cannot be used for evaluation, because the results depend on the particular choice of word size in the target language and implementation. Symbolic evaluation has not yet been set up for \uint\. \ text \The default size type\ typedecl dflt_size instantiation dflt_size :: typerep begin definition "typerep_class.typerep \ \_ :: dflt_size itself. Typerep.Typerep (STR ''Uint.dflt_size'') []" instance .. end consts dflt_size_aux :: "nat" specification (dflt_size_aux) dflt_size_aux_g0: "dflt_size_aux > 0" by auto hide_fact dflt_size_aux_def instantiation dflt_size :: len begin definition "len_of_dflt_size (_ :: dflt_size itself) \ dflt_size_aux" instance by(intro_classes)(simp add: len_of_dflt_size_def dflt_size_aux_g0) end abbreviation "dflt_size \ len_of (TYPE (dflt_size))" context includes integer.lifting begin lift_definition dflt_size_integer :: integer is "int dflt_size" . declare dflt_size_integer_def[code del] \ \The code generator will substitute a machine-dependent value for this constant\ lemma dflt_size_by_int[code]: "dflt_size = nat_of_integer dflt_size_integer" by transfer simp lemma dflt_size[simp]: "dflt_size > 0" "dflt_size \ Suc 0" "\ dflt_size < Suc 0" using len_gt_0[where 'a=dflt_size] by (simp_all del: len_gt_0) end section \Type definition and primitive operations\ typedef uint = \UNIV :: dflt_size word set\ .. global_interpretation uint: word_type_copy Abs_uint Rep_uint using type_definition_uint by (rule word_type_copy.intro) setup_lifting type_definition_uint declare uint.of_word_of [code abstype] declare Quotient_uint [transfer_rule] instantiation uint :: \{comm_ring_1, semiring_modulo, equal, linorder}\ begin lift_definition zero_uint :: uint is 0 . lift_definition one_uint :: uint is 1 . lift_definition plus_uint :: \uint \ uint \ uint\ is \(+)\ . lift_definition uminus_uint :: \uint \ uint\ is uminus . lift_definition minus_uint :: \uint \ uint \ uint\ is \(-)\ . lift_definition times_uint :: \uint \ uint \ uint\ is \(*)\ . lift_definition divide_uint :: \uint \ uint \ uint\ is \(div)\ . lift_definition modulo_uint :: \uint \ uint \ uint\ is \(mod)\ . lift_definition equal_uint :: \uint \ uint \ bool\ is \HOL.equal\ . lift_definition less_eq_uint :: \uint \ uint \ bool\ is \(\)\ . lift_definition less_uint :: \uint \ uint \ bool\ is \(<)\ . global_interpretation uint: word_type_copy_ring Abs_uint Rep_uint by standard (fact zero_uint.rep_eq one_uint.rep_eq plus_uint.rep_eq uminus_uint.rep_eq minus_uint.rep_eq times_uint.rep_eq divide_uint.rep_eq modulo_uint.rep_eq equal_uint.rep_eq less_eq_uint.rep_eq less_uint.rep_eq)+ instance proof - show \OFCLASS(uint, comm_ring_1_class)\ by (rule uint.of_class_comm_ring_1) show \OFCLASS(uint, semiring_modulo_class)\ by (fact uint.of_class_semiring_modulo) show \OFCLASS(uint, equal_class)\ by (fact uint.of_class_equal) show \OFCLASS(uint, linorder_class)\ by (fact uint.of_class_linorder) qed end instantiation uint :: ring_bit_operations begin lift_definition bit_uint :: \uint \ nat \ bool\ is bit . lift_definition not_uint :: \uint \ uint\ is \Bit_Operations.not\ . lift_definition and_uint :: \uint \ uint \ uint\ is \Bit_Operations.and\ . lift_definition or_uint :: \uint \ uint \ uint\ is \Bit_Operations.or\ . lift_definition xor_uint :: \uint \ uint \ uint\ is \Bit_Operations.xor\ . lift_definition mask_uint :: \nat \ uint\ is mask . lift_definition push_bit_uint :: \nat \ uint \ uint\ is push_bit . lift_definition drop_bit_uint :: \nat \ uint \ uint\ is drop_bit . lift_definition signed_drop_bit_uint :: \nat \ uint \ uint\ is signed_drop_bit . lift_definition take_bit_uint :: \nat \ uint \ uint\ is take_bit . lift_definition set_bit_uint :: \nat \ uint \ uint\ is Bit_Operations.set_bit . lift_definition unset_bit_uint :: \nat \ uint \ uint\ is unset_bit . lift_definition flip_bit_uint :: \nat \ uint \ uint\ is flip_bit . global_interpretation uint: word_type_copy_bits Abs_uint Rep_uint signed_drop_bit_uint by standard (fact bit_uint.rep_eq not_uint.rep_eq and_uint.rep_eq or_uint.rep_eq xor_uint.rep_eq mask_uint.rep_eq push_bit_uint.rep_eq drop_bit_uint.rep_eq signed_drop_bit_uint.rep_eq take_bit_uint.rep_eq set_bit_uint.rep_eq unset_bit_uint.rep_eq flip_bit_uint.rep_eq)+ instance by (fact uint.of_class_ring_bit_operations) end lift_definition uint_of_nat :: \nat \ uint\ is word_of_nat . lift_definition nat_of_uint :: \uint \ nat\ is unat . lift_definition uint_of_int :: \int \ uint\ is word_of_int . lift_definition int_of_uint :: \uint \ int\ is uint . context includes integer.lifting begin lift_definition Uint :: \integer \ uint\ is word_of_int . lift_definition integer_of_uint :: \uint \ integer\ is uint . end global_interpretation uint: word_type_copy_more Abs_uint Rep_uint signed_drop_bit_uint uint_of_nat nat_of_uint uint_of_int int_of_uint Uint integer_of_uint apply standard apply (simp_all add: uint_of_nat.rep_eq nat_of_uint.rep_eq uint_of_int.rep_eq int_of_uint.rep_eq Uint.rep_eq integer_of_uint.rep_eq integer_eq_iff) done instantiation uint :: "{size, msb, lsb, set_bit, bit_comprehension}" begin lift_definition size_uint :: \uint \ nat\ is size . lift_definition msb_uint :: \uint \ bool\ is msb . lift_definition lsb_uint :: \uint \ bool\ is lsb . text \Workaround: avoid name space clash by spelling out \<^text>\lift_definition\ explicitly.\ definition set_bit_uint :: \uint \ nat \ bool \ uint\ where set_bit_uint_eq: \set_bit_uint a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ context includes lifting_syntax begin lemma set_bit_uint_transfer [transfer_rule]: \(cr_uint ===> (=) ===> (\) ===> cr_uint) Generic_set_bit.set_bit Generic_set_bit.set_bit\ by (simp only: set_bit_eq [abs_def] set_bit_uint_eq [abs_def]) transfer_prover end lift_definition set_bits_uint :: \(nat \ bool) \ uint\ is set_bits . lift_definition set_bits_aux_uint :: \(nat \ bool) \ nat \ uint \ uint\ is set_bits_aux . global_interpretation uint: word_type_copy_misc Abs_uint Rep_uint signed_drop_bit_uint uint_of_nat nat_of_uint uint_of_int int_of_uint Uint integer_of_uint dflt_size set_bits_aux_uint by (standard; transfer) simp_all instance using uint.of_class_bit_comprehension uint.of_class_set_bit uint.of_class_lsb by simp_all standard end section \Code setup\ code_printing code_module Uint \ (SML) \ structure Uint : sig val set_bit : Word.word -> IntInf.int -> bool -> Word.word val shiftl : Word.word -> IntInf.int -> Word.word val shiftr : Word.word -> IntInf.int -> Word.word val shiftr_signed : Word.word -> IntInf.int -> Word.word val test_bit : Word.word -> IntInf.int -> bool end = struct fun set_bit x n b = let val mask = Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n)) in if b then Word.orb (x, mask) else Word.andb (x, Word.notb mask) end fun shiftl x n = Word.<< (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr x n = Word.>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr_signed x n = Word.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun test_bit x n = Word.andb (x, Word.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word.fromInt 0 end; (* struct Uint *)\ code_reserved SML Uint code_printing code_module Uint \ (Haskell) \module Uint(Int, Word, dflt_size) where import qualified Prelude import Data.Int(Int) import Data.Word(Word) import qualified Data.Bits dflt_size :: Prelude.Integer dflt_size = Prelude.toInteger (bitSize_aux (0::Word)) where bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int bitSize_aux = Data.Bits.bitSize\ and (Haskell_Quickcheck) \module Uint(Int, Word, dflt_size) where import qualified Prelude import Data.Int(Int) import Data.Word(Word) import qualified Data.Bits dflt_size :: Prelude.Int dflt_size = bitSize_aux (0::Word) where bitSize_aux :: (Data.Bits.Bits a, Prelude.Bounded a) => a -> Int bitSize_aux = Data.Bits.bitSize \ code_reserved Haskell Uint dflt_size text \ OCaml and Scala provide only signed bit numbers, so we use these and implement sign-sensitive operations like comparisons manually. \ code_printing code_module "Uint" \ (OCaml) \module Uint : sig type t = int val dflt_size : Z.t val less : t -> t -> bool val less_eq : t -> t -> bool val set_bit : t -> Z.t -> bool -> t val shiftl : t -> Z.t -> t val shiftr : t -> Z.t -> t val shiftr_signed : t -> Z.t -> t val test_bit : t -> Z.t -> bool val int_mask : int val int32_mask : int32 val int64_mask : int64 end = struct type t = int let dflt_size = Z.of_int Sys.int_size;; (* negative numbers have their highest bit set, so they are greater than positive ones *) let less x y = if x<0 then y<0 && x 0;; let int_mask = if Sys.int_size < 32 then lnot 0 else 0xFFFFFFFF;; let int32_mask = if Sys.int_size < 32 then Int32.pred (Int32.shift_left Int32.one Sys.int_size) else Int32.of_string "0xFFFFFFFF";; let int64_mask = if Sys.int_size < 64 then Int64.pred (Int64.shift_left Int64.one Sys.int_size) else Int64.of_string "0xFFFFFFFFFFFFFFFF";; end;; (*struct Uint*)\ code_reserved OCaml Uint code_printing code_module Uint \ (Scala) \object Uint { def dflt_size : BigInt = BigInt(32) def less(x: Int, y: Int) : Boolean = if (x < 0) y < 0 && x < y else y < 0 || x < y def less_eq(x: Int, y: Int) : Boolean = if (x < 0) y < 0 && x <= y else y < 0 || x <= y def set_bit(x: Int, n: BigInt, b: Boolean) : Int = if (b) x | (1 << n.intValue) else x & (1 << n.intValue).unary_~ def shiftl(x: Int, n: BigInt) : Int = x << n.intValue def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue def test_bit(x: Int, n: BigInt) : Boolean = (x & (1 << n.intValue)) != 0 } /* object Uint */\ code_reserved Scala Uint text \ OCaml's conversion from Big\_int to int demands that the value fits into a signed integer. The following justifies the implementation. \ context includes integer.lifting bit_operations_syntax begin definition wivs_mask :: int where "wivs_mask = 2^ dflt_size - 1" lift_definition wivs_mask_integer :: integer is wivs_mask . lemma [code]: "wivs_mask_integer = 2 ^ dflt_size - 1" by transfer (simp add: wivs_mask_def) definition wivs_shift :: int where "wivs_shift = 2 ^ dflt_size" lift_definition wivs_shift_integer :: integer is wivs_shift . lemma [code]: "wivs_shift_integer = 2 ^ dflt_size" by transfer (simp add: wivs_shift_def) definition wivs_index :: nat where "wivs_index == dflt_size - 1" lift_definition wivs_index_integer :: integer is "int wivs_index". lemma wivs_index_integer_code[code]: "wivs_index_integer = dflt_size_integer - 1" by transfer (simp add: wivs_index_def of_nat_diff) definition wivs_overflow :: int where "wivs_overflow == 2^ (dflt_size - 1)" lift_definition wivs_overflow_integer :: integer is wivs_overflow . lemma [code]: "wivs_overflow_integer = 2 ^ (dflt_size - 1)" by transfer (simp add: wivs_overflow_def) definition wivs_least :: int where "wivs_least == - wivs_overflow" lift_definition wivs_least_integer :: integer is wivs_least . lemma [code]: "wivs_least_integer = - (2 ^ (dflt_size - 1))" by transfer (simp add: wivs_overflow_def wivs_least_def) definition Uint_signed :: "integer \ uint" where "Uint_signed i = (if i < wivs_least_integer \ wivs_overflow_integer \ i then undefined Uint i else Uint i)" lemma Uint_code [code]: "Uint i = (let i' = i AND wivs_mask_integer in if bit i' wivs_index then Uint_signed (i' - wivs_shift_integer) else Uint_signed i')" including undefined_transfer unfolding Uint_signed_def apply transfer apply (subst word_of_int_via_signed) apply (auto simp add: push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed wivs_mask_def wivs_index_def wivs_overflow_def wivs_least_def wivs_shift_def) done lemma Uint_signed_code [code]: "Rep_uint (Uint_signed i) = (if i < wivs_least_integer \ i \ wivs_overflow_integer then Rep_uint (undefined Uint i) else word_of_int (int_of_integer_symbolic i))" - unfolding Uint_signed_def Uint_def int_of_integer_symbolic_def word_of_integer_def - by(simp add: Abs_uint_inverse) + unfolding Uint_signed_def Uint_def int_of_integer_symbolic_def by(simp add: Abs_uint_inverse) end text \ Avoid @{term Abs_uint} in generated code, use @{term Rep_uint'} instead. The symbolic implementations for code\_simp use @{term Rep_uint}. The new destructor @{term Rep_uint'} is executable. As the simplifier is given the [code abstract] equations literally, we cannot implement @{term Rep_uint} directly, because that makes code\_simp loop. If code generation raises Match, some equation probably contains @{term Rep_uint} ([code abstract] equations for @{typ uint} may use @{term Rep_uint} because these instances will be folded away.) \ definition Rep_uint' where [simp]: "Rep_uint' = Rep_uint" lemma Rep_uint'_code [code]: "Rep_uint' x = (BITS n. bit x n)" unfolding Rep_uint'_def by transfer (simp add: set_bits_bit_eq) lift_definition Abs_uint' :: "dflt_size word \ uint" is "\x :: dflt_size word. x" . lemma Abs_uint'_code [code]: "Abs_uint' x = Uint (integer_of_int (uint x))" including integer.lifting by transfer simp declare [[code drop: "term_of_class.term_of :: uint \ _"]] lemma term_of_uint_code [code]: defines "TR \ typerep.Typerep" and "bit0 \ STR ''Numeral_Type.bit0''" shows "term_of_class.term_of x = Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint.uint.Abs_uint'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR (STR ''Uint.dflt_size'') []], TR (STR ''Uint.uint'') []])) (term_of_class.term_of (Rep_uint' x))" by(simp add: term_of_anything) text \Important: We must prevent the reflection oracle (eval-tac) to use our machine-dependent type. \ code_printing type_constructor uint \ (SML) "Word.word" and (Haskell) "Uint.Word" and (OCaml) "Uint.t" and (Scala) "Int" and (Eval) "*** \"Error: Machine dependent type\" ***" and (Quickcheck) "Word.word" | constant dflt_size_integer \ (SML) "(IntInf.fromLarge (Int.toLarge Word.wordSize))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.wordSize" and (Haskell) "Uint.dflt'_size" and (OCaml) "Uint.dflt'_size" and (Scala) "Uint.dflt'_size" | constant Uint \ (SML) "Word.fromLargeInt (IntInf.toLarge _)" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.fromInt" and (Haskell) "(Prelude.fromInteger _ :: Uint.Word)" and (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint.Word)" and (Scala) "_.intValue" | constant Uint_signed \ (OCaml) "Z.to'_int" | constant "0 :: uint" \ (SML) "(Word.fromInt 0)" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "(Word.fromInt 0)" and (Haskell) "(0 :: Uint.Word)" and (OCaml) "0" and (Scala) "0" | constant "1 :: uint" \ (SML) "(Word.fromInt 1)" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "(Word.fromInt 1)" and (Haskell) "(1 :: Uint.Word)" and (OCaml) "1" and (Scala) "1" | constant "plus :: uint \ _ " \ (SML) "Word.+ ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.+ ((_), (_))" and (Haskell) infixl 6 "+" and (OCaml) "Pervasives.(+)" and (Scala) infixl 7 "+" | constant "uminus :: uint \ _" \ (SML) "Word.~" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.~" and (Haskell) "negate" and (OCaml) "Pervasives.(~-)" and (Scala) "!(- _)" | constant "minus :: uint \ _" \ (SML) "Word.- ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.- ((_), (_))" and (Haskell) infixl 6 "-" and (OCaml) "Pervasives.(-)" and (Scala) infixl 7 "-" | constant "times :: uint \ _ \ _" \ (SML) "Word.* ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.* ((_), (_))" and (Haskell) infixl 7 "*" and (OCaml) "Pervasives.( * )" and (Scala) infixl 8 "*" | constant "HOL.equal :: uint \ _ \ bool" \ (SML) "!((_ : Word.word) = _)" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "!((_ : Word.word) = _)" and (Haskell) infix 4 "==" and (OCaml) "(Pervasives.(=):Uint.t -> Uint.t -> bool)" and (Scala) infixl 5 "==" | class_instance uint :: equal \ (Haskell) - | constant "less_eq :: uint \ _ \ bool" \ (SML) "Word.<= ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.<= ((_), (_))" and (Haskell) infix 4 "<=" and (OCaml) "Uint.less'_eq" and (Scala) "Uint.less'_eq" | constant "less :: uint \ _ \ bool" \ (SML) "Word.< ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.< ((_), (_))" and (Haskell) infix 4 "<" and (OCaml) "Uint.less" and (Scala) "Uint.less" | constant "Bit_Operations.not :: uint \ _" \ (SML) "Word.notb" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.notb" and (Haskell) "Data'_Bits.complement" and (OCaml) "Pervasives.lnot" and (Scala) "_.unary'_~" | constant "Bit_Operations.and :: uint \ _" \ (SML) "Word.andb ((_),/ (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.andb ((_),/ (_))" and (Haskell) infixl 7 "Data_Bits..&." and (OCaml) "Pervasives.(land)" and (Scala) infixl 3 "&" | constant "Bit_Operations.or :: uint \ _" \ (SML) "Word.orb ((_),/ (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.orb ((_),/ (_))" and (Haskell) infixl 5 "Data_Bits..|." and (OCaml) "Pervasives.(lor)" and (Scala) infixl 1 "|" | constant "Bit_Operations.xor :: uint \ _" \ (SML) "Word.xorb ((_),/ (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.xorb ((_),/ (_))" and (Haskell) "Data'_Bits.xor" and (OCaml) "Pervasives.(lxor)" and (Scala) infixl 2 "^" definition uint_divmod :: "uint \ uint \ uint \ uint" where "uint_divmod x y = (if y = 0 then (undefined ((div) :: uint \ _) x (0 :: uint), undefined ((mod) :: uint \ _) x (0 :: uint)) else (x div y, x mod y))" definition uint_div :: "uint \ uint \ uint" where "uint_div x y = fst (uint_divmod x y)" definition uint_mod :: "uint \ uint \ uint" where "uint_mod x y = snd (uint_divmod x y)" lemma div_uint_code [code]: "x div y = (if y = 0 then 0 else uint_div x y)" including undefined_transfer unfolding uint_divmod_def uint_div_def by transfer(simp add: word_div_def) lemma mod_uint_code [code]: "x mod y = (if y = 0 then x else uint_mod x y)" including undefined_transfer unfolding uint_mod_def uint_divmod_def by transfer(simp add: word_mod_def) definition uint_sdiv :: "uint \ uint \ uint" where [code del]: "uint_sdiv x y = (if y = 0 then undefined ((div) :: uint \ _) x (0 :: uint) else Abs_uint (Rep_uint x sdiv Rep_uint y))" definition div0_uint :: "uint \ uint" where [code del]: "div0_uint x = undefined ((div) :: uint \ _) x (0 :: uint)" declare [[code abort: div0_uint]] definition mod0_uint :: "uint \ uint" where [code del]: "mod0_uint x = undefined ((mod) :: uint \ _) x (0 :: uint)" declare [[code abort: mod0_uint]] definition wivs_overflow_uint :: uint where "wivs_overflow_uint \ push_bit (dflt_size - 1) 1" lemma Rep_uint_wivs_overflow_uint_eq: \Rep_uint wivs_overflow_uint = 2 ^ (dflt_size - Suc 0)\ by (simp add: wivs_overflow_uint_def one_uint.rep_eq push_bit_uint.rep_eq uint.word_of_power push_bit_eq_mult) lemma wivs_overflow_uint_greater_eq_0: \wivs_overflow_uint > 0\ apply (simp add: less_uint.rep_eq zero_uint.rep_eq Rep_uint_wivs_overflow_uint_eq) apply transfer apply (simp add: take_bit_push_bit push_bit_eq_mult) done lemma uint_divmod_code [code]: "uint_divmod x y = (if wivs_overflow_uint \ y then if x < y then (0, x) else (1, x - y) else if y = 0 then (div0_uint x, mod0_uint x) else let q = push_bit 1 (uint_sdiv (drop_bit 1 x) y); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" proof (cases \y = 0\) case True moreover have \x \ 0\ by transfer simp moreover note wivs_overflow_uint_greater_eq_0 ultimately show ?thesis by (auto simp add: uint_divmod_def div0_uint_def mod0_uint_def not_less) next case False then show ?thesis including undefined_transfer unfolding uint_divmod_def uint_sdiv_def div0_uint_def mod0_uint_def wivs_overflow_uint_def apply transfer apply (simp add: divmod_via_sdivmod push_bit_of_1) done qed lemma uint_sdiv_code [code]: "Rep_uint (uint_sdiv x y) = (if y = 0 then Rep_uint (undefined ((div) :: uint \ _) x (0 :: uint)) else Rep_uint x sdiv Rep_uint y)" unfolding uint_sdiv_def by(simp add: Abs_uint_inverse) text \ Note that we only need a translation for signed division, but not for the remainder because @{thm uint_divmod_code} computes both with division only. \ code_printing constant uint_div \ (SML) "Word.div ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.div ((_), (_))" and (Haskell) "Prelude.div" | constant uint_mod \ (SML) "Word.mod ((_), (_))" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Word.mod ((_), (_))" and (Haskell) "Prelude.mod" | constant uint_divmod \ (Haskell) "divmod" | constant uint_sdiv \ (OCaml) "Pervasives.('/)" and (Scala) "_ '/ _" definition uint_test_bit :: "uint \ integer \ bool" where [code del]: "uint_test_bit x n = (if n < 0 \ dflt_size_integer \ n then undefined (bit :: uint \ _) x n else bit x (nat_of_integer n))" lemma test_bit_uint_code [code]: "bit x n \ n < dflt_size \ uint_test_bit x (integer_of_nat n)" including undefined_transfer integer.lifting unfolding uint_test_bit_def by (transfer, simp, transfer, simp) lemma uint_test_bit_code [code]: "uint_test_bit w n = (if n < 0 \ dflt_size_integer \ n then undefined (bit :: uint \ _) w n else bit (Rep_uint w) (nat_of_integer n))" unfolding uint_test_bit_def by(simp add: bit_uint.rep_eq) code_printing constant uint_test_bit \ (SML) "Uint.test'_bit" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Uint.test'_bit" and (Haskell) "Data'_Bits.testBitBounded" and (OCaml) "Uint.test'_bit" and (Scala) "Uint.test'_bit" definition uint_set_bit :: "uint \ integer \ bool \ uint" where [code del]: "uint_set_bit x n b = (if n < 0 \ dflt_size_integer \ n then undefined (set_bit :: uint \ _) x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_uint_code [code]: "set_bit x n b = (if n < dflt_size then uint_set_bit x (integer_of_nat n) b else x)" including undefined_transfer integer.lifting unfolding uint_set_bit_def by (transfer) (auto cong: conj_cong simp add: not_less set_bit_beyond word_size) lemma uint_set_bit_code [code]: "Rep_uint (uint_set_bit w n b) = (if n < 0 \ dflt_size_integer \ n then Rep_uint (undefined (set_bit :: uint \ _) w n b) else set_bit (Rep_uint w) (nat_of_integer n) b)" including undefined_transfer integer.lifting unfolding uint_set_bit_def by transfer simp code_printing constant uint_set_bit \ (SML) "Uint.set'_bit" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Uint.set'_bit" and (Haskell) "Data'_Bits.setBitBounded" and (OCaml) "Uint.set'_bit" and (Scala) "Uint.set'_bit" definition uint_shiftl :: "uint \ integer \ uint" where [code del]: "uint_shiftl x n = (if n < 0 \ dflt_size_integer \ n then undefined (push_bit :: nat \ uint \ _) x n else push_bit (nat_of_integer n) x)" lemma shiftl_uint_code [code]: "push_bit n x = (if n < dflt_size then uint_shiftl x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint_shiftl_def by (transfer fixing: n) simp lemma uint_shiftl_code [code]: "Rep_uint (uint_shiftl w n) = (if n < 0 \ dflt_size_integer \ n then Rep_uint (undefined (push_bit :: nat \ uint \ _) w n) else push_bit (nat_of_integer n) (Rep_uint w))" including undefined_transfer integer.lifting unfolding uint_shiftl_def by transfer simp code_printing constant uint_shiftl \ (SML) "Uint.shiftl" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Uint.shiftl" and (Haskell) "Data'_Bits.shiftlBounded" and (OCaml) "Uint.shiftl" and (Scala) "Uint.shiftl" definition uint_shiftr :: "uint \ integer \ uint" where [code del]: "uint_shiftr x n = (if n < 0 \ dflt_size_integer \ n then undefined (drop_bit :: nat \ uint \ _) x n else drop_bit (nat_of_integer n) x)" lemma shiftr_uint_code [code]: "drop_bit n x = (if n < dflt_size then uint_shiftr x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint_shiftr_def by (transfer fixing: n) simp lemma uint_shiftr_code [code]: "Rep_uint (uint_shiftr w n) = (if n < 0 \ dflt_size_integer \ n then Rep_uint (undefined (drop_bit :: nat \ uint \ _) w n) else drop_bit (nat_of_integer n) (Rep_uint w))" including undefined_transfer integer.lifting unfolding uint_shiftr_def by transfer simp code_printing constant uint_shiftr \ (SML) "Uint.shiftr" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Uint.shiftr" and (Haskell) "Data'_Bits.shiftrBounded" and (OCaml) "Uint.shiftr" and (Scala) "Uint.shiftr" definition uint_sshiftr :: "uint \ integer \ uint" where [code del]: "uint_sshiftr x n = (if n < 0 \ dflt_size_integer \ n then undefined signed_drop_bit_uint n x else signed_drop_bit_uint (nat_of_integer n) x)" lemma sshiftr_uint_code [code]: "signed_drop_bit_uint n x = (if n < dflt_size then uint_sshiftr x (integer_of_nat n) else if bit x wivs_index then -1 else 0)" including undefined_transfer integer.lifting unfolding uint_sshiftr_def by transfer(simp add: not_less signed_drop_bit_beyond word_size wivs_index_def) lemma uint_sshiftr_code [code]: "Rep_uint (uint_sshiftr w n) = (if n < 0 \ dflt_size_integer \ n then Rep_uint (undefined signed_drop_bit_uint n w) else signed_drop_bit (nat_of_integer n) (Rep_uint w))" including undefined_transfer integer.lifting unfolding uint_sshiftr_def by transfer simp code_printing constant uint_sshiftr \ (SML) "Uint.shiftr'_signed" and (Eval) "(raise (Fail \"Machine dependent code\"))" and (Quickcheck) "Uint.shiftr'_signed" and (Haskell) "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint.Int) _)) :: Uint.Word)" and (OCaml) "Uint.shiftr'_signed" and (Scala) "Uint.shiftr'_signed" lemma uint_msb_test_bit: "msb x \ bit (x :: uint) wivs_index" by transfer (simp add: msb_word_iff_bit wivs_index_def) lemma msb_uint_code [code]: "msb x \ uint_test_bit x wivs_index_integer" apply(simp add: uint_test_bit_def uint_msb_test_bit wivs_index_integer_code dflt_size_integer_def wivs_index_def) by (metis (full_types) One_nat_def dflt_size(2) less_iff_diff_less_0 nat_of_integer_of_nat of_nat_1 of_nat_diff of_nat_less_0_iff wivs_index_def) lemma uint_of_int_code [code]: "uint_of_int i = (BITS n. bit i n)" by transfer (simp add: word_of_int_conv_set_bits) section \Quickcheck setup\ definition uint_of_natural :: "natural \ uint" where "uint_of_natural x \ Uint (integer_of_natural x)" instantiation uint :: "{random, exhaustive, full_exhaustive}" begin definition "random_uint \ qc_random_cnv uint_of_natural" definition "exhaustive_uint \ qc_exhaustive_cnv uint_of_natural" definition "full_exhaustive_uint \ qc_full_exhaustive_cnv uint_of_natural" instance .. end instantiation uint :: narrowing begin interpretation quickcheck_narrowing_samples "\i. (Uint i, Uint (- i))" "0" "Typerep.Typerep (STR ''Uint.uint'') []" . definition "narrowing_uint d = qc_narrowing_drawn_from (narrowing_samples d) d" declare [[code drop: "partial_term_of :: uint itself \ _"]] lemmas partial_term_of_uint [code] = partial_term_of_code instance .. end end diff --git a/thys/Native_Word/Uint32.thy b/thys/Native_Word/Uint32.thy --- a/thys/Native_Word/Uint32.thy +++ b/thys/Native_Word/Uint32.thy @@ -1,692 +1,692 @@ (* Title: Uint32.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Unsigned words of 32 bits\ theory Uint32 imports Word_Type_Copies Code_Target_Integer_Bit begin section \Type definition and primitive operations\ typedef uint32 = \UNIV :: 32 word set\ .. global_interpretation uint32: word_type_copy Abs_uint32 Rep_uint32 using type_definition_uint32 by (rule word_type_copy.intro) setup_lifting type_definition_uint32 declare uint32.of_word_of [code abstype] declare Quotient_uint32 [transfer_rule] instantiation uint32 :: \{comm_ring_1, semiring_modulo, equal, linorder}\ begin lift_definition zero_uint32 :: uint32 is 0 . lift_definition one_uint32 :: uint32 is 1 . lift_definition plus_uint32 :: \uint32 \ uint32 \ uint32\ is \(+)\ . lift_definition uminus_uint32 :: \uint32 \ uint32\ is uminus . lift_definition minus_uint32 :: \uint32 \ uint32 \ uint32\ is \(-)\ . lift_definition times_uint32 :: \uint32 \ uint32 \ uint32\ is \(*)\ . lift_definition divide_uint32 :: \uint32 \ uint32 \ uint32\ is \(div)\ . lift_definition modulo_uint32 :: \uint32 \ uint32 \ uint32\ is \(mod)\ . lift_definition equal_uint32 :: \uint32 \ uint32 \ bool\ is \HOL.equal\ . lift_definition less_eq_uint32 :: \uint32 \ uint32 \ bool\ is \(\)\ . lift_definition less_uint32 :: \uint32 \ uint32 \ bool\ is \(<)\ . global_interpretation uint32: word_type_copy_ring Abs_uint32 Rep_uint32 by standard (fact zero_uint32.rep_eq one_uint32.rep_eq plus_uint32.rep_eq uminus_uint32.rep_eq minus_uint32.rep_eq times_uint32.rep_eq divide_uint32.rep_eq modulo_uint32.rep_eq equal_uint32.rep_eq less_eq_uint32.rep_eq less_uint32.rep_eq)+ instance proof - show \OFCLASS(uint32, comm_ring_1_class)\ by (rule uint32.of_class_comm_ring_1) show \OFCLASS(uint32, semiring_modulo_class)\ by (fact uint32.of_class_semiring_modulo) show \OFCLASS(uint32, equal_class)\ by (fact uint32.of_class_equal) show \OFCLASS(uint32, linorder_class)\ by (fact uint32.of_class_linorder) qed end instantiation uint32 :: ring_bit_operations begin lift_definition bit_uint32 :: \uint32 \ nat \ bool\ is bit . lift_definition not_uint32 :: \uint32 \ uint32\ is \Bit_Operations.not\ . lift_definition and_uint32 :: \uint32 \ uint32 \ uint32\ is \Bit_Operations.and\ . lift_definition or_uint32 :: \uint32 \ uint32 \ uint32\ is \Bit_Operations.or\ . lift_definition xor_uint32 :: \uint32 \ uint32 \ uint32\ is \Bit_Operations.xor\ . lift_definition mask_uint32 :: \nat \ uint32\ is mask . lift_definition push_bit_uint32 :: \nat \ uint32 \ uint32\ is push_bit . lift_definition drop_bit_uint32 :: \nat \ uint32 \ uint32\ is drop_bit . lift_definition signed_drop_bit_uint32 :: \nat \ uint32 \ uint32\ is signed_drop_bit . lift_definition take_bit_uint32 :: \nat \ uint32 \ uint32\ is take_bit . lift_definition set_bit_uint32 :: \nat \ uint32 \ uint32\ is Bit_Operations.set_bit . lift_definition unset_bit_uint32 :: \nat \ uint32 \ uint32\ is unset_bit . lift_definition flip_bit_uint32 :: \nat \ uint32 \ uint32\ is flip_bit . global_interpretation uint32: word_type_copy_bits Abs_uint32 Rep_uint32 signed_drop_bit_uint32 by standard (fact bit_uint32.rep_eq not_uint32.rep_eq and_uint32.rep_eq or_uint32.rep_eq xor_uint32.rep_eq mask_uint32.rep_eq push_bit_uint32.rep_eq drop_bit_uint32.rep_eq signed_drop_bit_uint32.rep_eq take_bit_uint32.rep_eq set_bit_uint32.rep_eq unset_bit_uint32.rep_eq flip_bit_uint32.rep_eq)+ instance by (fact uint32.of_class_ring_bit_operations) end lift_definition uint32_of_nat :: \nat \ uint32\ is word_of_nat . lift_definition nat_of_uint32 :: \uint32 \ nat\ is unat . lift_definition uint32_of_int :: \int \ uint32\ is word_of_int . lift_definition int_of_uint32 :: \uint32 \ int\ is uint . context includes integer.lifting begin lift_definition Uint32 :: \integer \ uint32\ is word_of_int . lift_definition integer_of_uint32 :: \uint32 \ integer\ is uint . end global_interpretation uint32: word_type_copy_more Abs_uint32 Rep_uint32 signed_drop_bit_uint32 uint32_of_nat nat_of_uint32 uint32_of_int int_of_uint32 Uint32 integer_of_uint32 apply standard apply (simp_all add: uint32_of_nat.rep_eq nat_of_uint32.rep_eq uint32_of_int.rep_eq int_of_uint32.rep_eq Uint32.rep_eq integer_of_uint32.rep_eq integer_eq_iff) done instantiation uint32 :: "{size, msb, lsb, set_bit, bit_comprehension}" begin lift_definition size_uint32 :: \uint32 \ nat\ is size . lift_definition msb_uint32 :: \uint32 \ bool\ is msb . lift_definition lsb_uint32 :: \uint32 \ bool\ is lsb . text \Workaround: avoid name space clash by spelling out \<^text>\lift_definition\ explicitly.\ definition set_bit_uint32 :: \uint32 \ nat \ bool \ uint32\ where set_bit_uint32_eq: \set_bit_uint32 a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ context includes lifting_syntax begin lemma set_bit_uint32_transfer [transfer_rule]: \(cr_uint32 ===> (=) ===> (\) ===> cr_uint32) Generic_set_bit.set_bit Generic_set_bit.set_bit\ by (simp only: set_bit_eq [abs_def] set_bit_uint32_eq [abs_def]) transfer_prover end lift_definition set_bits_uint32 :: \(nat \ bool) \ uint32\ is set_bits . lift_definition set_bits_aux_uint32 :: \(nat \ bool) \ nat \ uint32 \ uint32\ is set_bits_aux . global_interpretation uint32: word_type_copy_misc Abs_uint32 Rep_uint32 signed_drop_bit_uint32 uint32_of_nat nat_of_uint32 uint32_of_int int_of_uint32 Uint32 integer_of_uint32 32 set_bits_aux_uint32 by (standard; transfer) simp_all instance using uint32.of_class_bit_comprehension uint32.of_class_set_bit uint32.of_class_lsb by simp_all standard end section \Code setup\ code_printing code_module Uint32 \ (SML) \(* Test that words can handle numbers between 0 and 31 *) val _ = if 5 <= Word.wordSize then () else raise (Fail ("wordSize less than 5")); structure Uint32 : sig val set_bit : Word32.word -> IntInf.int -> bool -> Word32.word val shiftl : Word32.word -> IntInf.int -> Word32.word val shiftr : Word32.word -> IntInf.int -> Word32.word val shiftr_signed : Word32.word -> IntInf.int -> Word32.word val test_bit : Word32.word -> IntInf.int -> bool end = struct fun set_bit x n b = let val mask = Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n)) in if b then Word32.orb (x, mask) else Word32.andb (x, Word32.notb mask) end fun shiftl x n = Word32.<< (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr x n = Word32.>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun shiftr_signed x n = Word32.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) fun test_bit x n = Word32.andb (x, Word32.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word32.fromInt 0 end; (* struct Uint32 *)\ code_reserved SML Uint32 code_printing code_module Uint32 \ (Haskell) \module Uint32(Int32, Word32) where import Data.Int(Int32) import Data.Word(Word32)\ code_reserved Haskell Uint32 text \ OCaml and Scala provide only signed 32bit numbers, so we use these and implement sign-sensitive operations like comparisons manually. \ code_printing code_module "Uint32" \ (OCaml) \module Uint32 : sig val less : int32 -> int32 -> bool val less_eq : int32 -> int32 -> bool val set_bit : int32 -> Z.t -> bool -> int32 val shiftl : int32 -> Z.t -> int32 val shiftr : int32 -> Z.t -> int32 val shiftr_signed : int32 -> Z.t -> int32 val test_bit : int32 -> Z.t -> bool end = struct (* negative numbers have their highest bit set, so they are greater than positive ones *) let less x y = if Int32.compare x Int32.zero < 0 then Int32.compare y Int32.zero < 0 && Int32.compare x y < 0 else Int32.compare y Int32.zero < 0 || Int32.compare x y < 0;; let less_eq x y = if Int32.compare x Int32.zero < 0 then Int32.compare y Int32.zero < 0 && Int32.compare x y <= 0 else Int32.compare y Int32.zero < 0 || Int32.compare x y <= 0;; let set_bit x n b = let mask = Int32.shift_left Int32.one (Z.to_int n) in if b then Int32.logor x mask else Int32.logand x (Int32.lognot mask);; let shiftl x n = Int32.shift_left x (Z.to_int n);; let shiftr x n = Int32.shift_right_logical x (Z.to_int n);; let shiftr_signed x n = Int32.shift_right x (Z.to_int n);; let test_bit x n = Int32.compare (Int32.logand x (Int32.shift_left Int32.one (Z.to_int n))) Int32.zero <> 0;; end;; (*struct Uint32*)\ code_reserved OCaml Uint32 code_printing code_module Uint32 \ (Scala) \object Uint32 { def less(x: Int, y: Int) : Boolean = if (x < 0) y < 0 && x < y else y < 0 || x < y def less_eq(x: Int, y: Int) : Boolean = if (x < 0) y < 0 && x <= y else y < 0 || x <= y def set_bit(x: Int, n: BigInt, b: Boolean) : Int = if (b) x | (1 << n.intValue) else x & (1 << n.intValue).unary_~ def shiftl(x: Int, n: BigInt) : Int = x << n.intValue def shiftr(x: Int, n: BigInt) : Int = x >>> n.intValue def shiftr_signed(x: Int, n: BigInt) : Int = x >> n.intValue def test_bit(x: Int, n: BigInt) : Boolean = (x & (1 << n.intValue)) != 0 } /* object Uint32 */\ code_reserved Scala Uint32 text \ OCaml's conversion from Big\_int to int32 demands that the value fits int a signed 32-bit integer. The following justifies the implementation. \ context includes bit_operations_syntax begin definition Uint32_signed :: "integer \ uint32" where "Uint32_signed i = (if i < -(0x80000000) \ i \ 0x80000000 then undefined Uint32 i else Uint32 i)" lemma Uint32_code [code]: "Uint32 i = (let i' = i AND 0xFFFFFFFF in if bit i' 31 then Uint32_signed (i' - 0x100000000) else Uint32_signed i')" including undefined_transfer integer.lifting unfolding Uint32_signed_def apply transfer apply (subst word_of_int_via_signed) apply (auto simp add: push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong) done lemma Uint32_signed_code [code]: "Rep_uint32 (Uint32_signed i) = (if i < -(0x80000000) \ i \ 0x80000000 then Rep_uint32 (undefined Uint32 i) else word_of_int (int_of_integer_symbolic i))" -unfolding Uint32_signed_def Uint32_def int_of_integer_symbolic_def word_of_integer_def +unfolding Uint32_signed_def Uint32_def int_of_integer_symbolic_def by(simp add: Abs_uint32_inverse) end text \ Avoid @{term Abs_uint32} in generated code, use @{term Rep_uint32'} instead. The symbolic implementations for code\_simp use @{term Rep_uint32}. The new destructor @{term Rep_uint32'} is executable. As the simplifier is given the [code abstract] equations literally, we cannot implement @{term Rep_uint32} directly, because that makes code\_simp loop. If code generation raises Match, some equation probably contains @{term Rep_uint32} ([code abstract] equations for @{typ uint32} may use @{term Rep_uint32} because these instances will be folded away.) To convert @{typ "32 word"} values into @{typ uint32}, use @{term "Abs_uint32'"}. \ definition Rep_uint32' where [simp]: "Rep_uint32' = Rep_uint32" lemma Rep_uint32'_transfer [transfer_rule]: "rel_fun cr_uint32 (=) (\x. x) Rep_uint32'" unfolding Rep_uint32'_def by(rule uint32.rep_transfer) lemma Rep_uint32'_code [code]: "Rep_uint32' x = (BITS n. bit x n)" by transfer (simp add: set_bits_bit_eq) lift_definition Abs_uint32' :: "32 word \ uint32" is "\x :: 32 word. x" . lemma Abs_uint32'_code [code]: "Abs_uint32' x = Uint32 (integer_of_int (uint x))" including integer.lifting by transfer simp declare [[code drop: "term_of_class.term_of :: uint32 \ _"]] lemma term_of_uint32_code [code]: defines "TR \ typerep.Typerep" and "bit0 \ STR ''Numeral_Type.bit0''" shows "term_of_class.term_of x = Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint32.uint32.Abs_uint32'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]], TR (STR ''Uint32.uint32'') []])) (term_of_class.term_of (Rep_uint32' x))" by(simp add: term_of_anything) code_printing type_constructor uint32 \ (SML) "Word32.word" and (Haskell) "Uint32.Word32" and (OCaml) "int32" and (Scala) "Int" and (Eval) "Word32.word" | constant Uint32 \ (SML) "Word32.fromLargeInt (IntInf.toLarge _)" and (Haskell) "(Prelude.fromInteger _ :: Uint32.Word32)" and (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Word32)" and (Scala) "_.intValue" | constant Uint32_signed \ (OCaml) "Z.to'_int32" | constant "0 :: uint32" \ (SML) "(Word32.fromInt 0)" and (Haskell) "(0 :: Uint32.Word32)" and (OCaml) "Int32.zero" and (Scala) "0" | constant "1 :: uint32" \ (SML) "(Word32.fromInt 1)" and (Haskell) "(1 :: Uint32.Word32)" and (OCaml) "Int32.one" and (Scala) "1" | constant "plus :: uint32 \ _ " \ (SML) "Word32.+ ((_), (_))" and (Haskell) infixl 6 "+" and (OCaml) "Int32.add" and (Scala) infixl 7 "+" | constant "uminus :: uint32 \ _" \ (SML) "Word32.~" and (Haskell) "negate" and (OCaml) "Int32.neg" and (Scala) "!(- _)" | constant "minus :: uint32 \ _" \ (SML) "Word32.- ((_), (_))" and (Haskell) infixl 6 "-" and (OCaml) "Int32.sub" and (Scala) infixl 7 "-" | constant "times :: uint32 \ _ \ _" \ (SML) "Word32.* ((_), (_))" and (Haskell) infixl 7 "*" and (OCaml) "Int32.mul" and (Scala) infixl 8 "*" | constant "HOL.equal :: uint32 \ _ \ bool" \ (SML) "!((_ : Word32.word) = _)" and (Haskell) infix 4 "==" and (OCaml) "(Int32.compare _ _ = 0)" and (Scala) infixl 5 "==" | class_instance uint32 :: equal \ (Haskell) - | constant "less_eq :: uint32 \ _ \ bool" \ (SML) "Word32.<= ((_), (_))" and (Haskell) infix 4 "<=" and (OCaml) "Uint32.less'_eq" and (Scala) "Uint32.less'_eq" | constant "less :: uint32 \ _ \ bool" \ (SML) "Word32.< ((_), (_))" and (Haskell) infix 4 "<" and (OCaml) "Uint32.less" and (Scala) "Uint32.less" | constant "Bit_Operations.not :: uint32 \ _" \ (SML) "Word32.notb" and (Haskell) "Data'_Bits.complement" and (OCaml) "Int32.lognot" and (Scala) "_.unary'_~" | constant "Bit_Operations.and :: uint32 \ _" \ (SML) "Word32.andb ((_),/ (_))" and (Haskell) infixl 7 "Data_Bits..&." and (OCaml) "Int32.logand" and (Scala) infixl 3 "&" | constant "Bit_Operations.or :: uint32 \ _" \ (SML) "Word32.orb ((_),/ (_))" and (Haskell) infixl 5 "Data_Bits..|." and (OCaml) "Int32.logor" and (Scala) infixl 1 "|" | constant "Bit_Operations.xor :: uint32 \ _" \ (SML) "Word32.xorb ((_),/ (_))" and (Haskell) "Data'_Bits.xor" and (OCaml) "Int32.logxor" and (Scala) infixl 2 "^" definition uint32_divmod :: "uint32 \ uint32 \ uint32 \ uint32" where "uint32_divmod x y = (if y = 0 then (undefined ((div) :: uint32 \ _) x (0 :: uint32), undefined ((mod) :: uint32 \ _) x (0 :: uint32)) else (x div y, x mod y))" definition uint32_div :: "uint32 \ uint32 \ uint32" where "uint32_div x y = fst (uint32_divmod x y)" definition uint32_mod :: "uint32 \ uint32 \ uint32" where "uint32_mod x y = snd (uint32_divmod x y)" lemma div_uint32_code [code]: "x div y = (if y = 0 then 0 else uint32_div x y)" including undefined_transfer unfolding uint32_divmod_def uint32_div_def by transfer (simp add: word_div_def) lemma mod_uint32_code [code]: "x mod y = (if y = 0 then x else uint32_mod x y)" including undefined_transfer unfolding uint32_mod_def uint32_divmod_def by transfer (simp add: word_mod_def) definition uint32_sdiv :: "uint32 \ uint32 \ uint32" where [code del]: "uint32_sdiv x y = (if y = 0 then undefined ((div) :: uint32 \ _) x (0 :: uint32) else Abs_uint32 (Rep_uint32 x sdiv Rep_uint32 y))" definition div0_uint32 :: "uint32 \ uint32" where [code del]: "div0_uint32 x = undefined ((div) :: uint32 \ _) x (0 :: uint32)" declare [[code abort: div0_uint32]] definition mod0_uint32 :: "uint32 \ uint32" where [code del]: "mod0_uint32 x = undefined ((mod) :: uint32 \ _) x (0 :: uint32)" declare [[code abort: mod0_uint32]] lemma uint32_divmod_code [code]: "uint32_divmod x y = (if 0x80000000 \ y then if x < y then (0, x) else (1, x - y) else if y = 0 then (div0_uint32 x, mod0_uint32 x) else let q = push_bit 1 (uint32_sdiv (drop_bit 1 x) y); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" including undefined_transfer unfolding uint32_divmod_def uint32_sdiv_def div0_uint32_def mod0_uint32_def less_eq_uint32.rep_eq apply transfer apply (simp add: divmod_via_sdivmod push_bit_eq_mult) done lemma uint32_sdiv_code [code]: "Rep_uint32 (uint32_sdiv x y) = (if y = 0 then Rep_uint32 (undefined ((div) :: uint32 \ _) x (0 :: uint32)) else Rep_uint32 x sdiv Rep_uint32 y)" unfolding uint32_sdiv_def by(simp add: Abs_uint32_inverse) text \ Note that we only need a translation for signed division, but not for the remainder because @{thm uint32_divmod_code} computes both with division only. \ code_printing constant uint32_div \ (SML) "Word32.div ((_), (_))" and (Haskell) "Prelude.div" | constant uint32_mod \ (SML) "Word32.mod ((_), (_))" and (Haskell) "Prelude.mod" | constant uint32_divmod \ (Haskell) "divmod" | constant uint32_sdiv \ (OCaml) "Int32.div" and (Scala) "_ '/ _" definition uint32_test_bit :: "uint32 \ integer \ bool" where [code del]: "uint32_test_bit x n = (if n < 0 \ 31 < n then undefined (bit :: uint32 \ _) x n else bit x (nat_of_integer n))" lemma test_bit_uint32_code [code]: "bit x n \ n < 32 \ uint32_test_bit x (integer_of_nat n)" including undefined_transfer integer.lifting unfolding uint32_test_bit_def by (transfer, simp, transfer, simp) lemma uint32_test_bit_code [code]: "uint32_test_bit w n = (if n < 0 \ 31 < n then undefined (bit :: uint32 \ _) w n else bit (Rep_uint32 w) (nat_of_integer n))" unfolding uint32_test_bit_def by(simp add: bit_uint32.rep_eq) code_printing constant uint32_test_bit \ (SML) "Uint32.test'_bit" and (Haskell) "Data'_Bits.testBitBounded" and (OCaml) "Uint32.test'_bit" and (Scala) "Uint32.test'_bit" and (Eval) "(fn w => fn n => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_test'_bit out of bounds\") else Uint32.test'_bit w n)" definition uint32_set_bit :: "uint32 \ integer \ bool \ uint32" where [code del]: "uint32_set_bit x n b = (if n < 0 \ 31 < n then undefined (set_bit :: uint32 \ _) x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_uint32_code [code]: "set_bit x n b = (if n < 32 then uint32_set_bit x (integer_of_nat n) b else x)" including undefined_transfer integer.lifting unfolding uint32_set_bit_def by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size) lemma uint32_set_bit_code [code]: "Rep_uint32 (uint32_set_bit w n b) = (if n < 0 \ 31 < n then Rep_uint32 (undefined (set_bit :: uint32 \ _) w n b) else set_bit (Rep_uint32 w) (nat_of_integer n) b)" including undefined_transfer unfolding uint32_set_bit_def by transfer simp code_printing constant uint32_set_bit \ (SML) "Uint32.set'_bit" and (Haskell) "Data'_Bits.setBitBounded" and (OCaml) "Uint32.set'_bit" and (Scala) "Uint32.set'_bit" and (Eval) "(fn w => fn n => fn b => if n < 0 orelse 32 <= n then raise (Fail \"argument to uint32'_set'_bit out of bounds\") else Uint32.set'_bit x n b)" definition uint32_shiftl :: "uint32 \ integer \ uint32" where [code del]: "uint32_shiftl x n = (if n < 0 \ 32 \ n then undefined (push_bit :: nat \ uint32 \ _) x n else push_bit (nat_of_integer n) x)" lemma shiftl_uint32_code [code]: "push_bit n x = (if n < 32 then uint32_shiftl x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint32_shiftl_def by transfer simp lemma uint32_shiftl_code [code]: "Rep_uint32 (uint32_shiftl w n) = (if n < 0 \ 32 \ n then Rep_uint32 (undefined (push_bit :: nat \ uint32 \ _) w n) else push_bit (nat_of_integer n) (Rep_uint32 w))" including undefined_transfer unfolding uint32_shiftl_def by transfer simp code_printing constant uint32_shiftl \ (SML) "Uint32.shiftl" and (Haskell) "Data'_Bits.shiftlBounded" and (OCaml) "Uint32.shiftl" and (Scala) "Uint32.shiftl" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftl out of bounds\" else Uint32.shiftl x i)" definition uint32_shiftr :: "uint32 \ integer \ uint32" where [code del]: "uint32_shiftr x n = (if n < 0 \ 32 \ n then undefined (drop_bit :: nat \ uint32 \ _) x n else drop_bit (nat_of_integer n) x)" lemma shiftr_uint32_code [code]: "drop_bit n x = (if n < 32 then uint32_shiftr x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint32_shiftr_def by transfer simp lemma uint32_shiftr_code [code]: "Rep_uint32 (uint32_shiftr w n) = (if n < 0 \ 32 \ n then Rep_uint32 (undefined (drop_bit :: nat \ uint32 \ _) w n) else drop_bit (nat_of_integer n) (Rep_uint32 w))" including undefined_transfer unfolding uint32_shiftr_def by transfer simp code_printing constant uint32_shiftr \ (SML) "Uint32.shiftr" and (Haskell) "Data'_Bits.shiftrBounded" and (OCaml) "Uint32.shiftr" and (Scala) "Uint32.shiftr" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr out of bounds\" else Uint32.shiftr x i)" definition uint32_sshiftr :: "uint32 \ integer \ uint32" where [code del]: "uint32_sshiftr x n = (if n < 0 \ 32 \ n then undefined signed_drop_bit_uint32 n x else signed_drop_bit_uint32 (nat_of_integer n) x)" lemma sshiftr_uint32_code [code]: "signed_drop_bit_uint32 n x = (if n < 32 then uint32_sshiftr x (integer_of_nat n) else if bit x 31 then - 1 else 0)" including undefined_transfer integer.lifting unfolding uint32_sshiftr_def by transfer (simp add: not_less signed_drop_bit_beyond) lemma uint32_sshiftr_code [code]: "Rep_uint32 (uint32_sshiftr w n) = (if n < 0 \ 32 \ n then Rep_uint32 (undefined signed_drop_bit_uint32 n w) else signed_drop_bit (nat_of_integer n) (Rep_uint32 w))" including undefined_transfer unfolding uint32_sshiftr_def by transfer simp code_printing constant uint32_sshiftr \ (SML) "Uint32.shiftr'_signed" and (Haskell) "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint32.Int32) _)) :: Uint32.Word32)" and (OCaml) "Uint32.shiftr'_signed" and (Scala) "Uint32.shiftr'_signed" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 32 then raise Fail \"argument to uint32'_shiftr'_signed out of bounds\" else Uint32.shiftr'_signed x i)" context includes bit_operations_syntax begin lemma uint32_msb_test_bit: "msb x \ bit (x :: uint32) 31" by transfer (simp add: msb_word_iff_bit) lemma msb_uint32_code [code]: "msb x \ uint32_test_bit x 31" by (simp add: uint32_test_bit_def uint32_msb_test_bit) lemma uint32_of_int_code [code]: "uint32_of_int i = Uint32 (integer_of_int i)" including integer.lifting by transfer simp lemma int_of_uint32_code [code]: "int_of_uint32 x = int_of_integer (integer_of_uint32 x)" including integer.lifting by transfer simp lemma uint32_of_nat_code [code]: "uint32_of_nat = uint32_of_int \ int" by transfer (simp add: fun_eq_iff) lemma nat_of_uint32_code [code]: "nat_of_uint32 x = nat_of_integer (integer_of_uint32 x)" unfolding integer_of_uint32_def including integer.lifting by transfer simp definition integer_of_uint32_signed :: "uint32 \ integer" where "integer_of_uint32_signed n = (if bit n 31 then undefined integer_of_uint32 n else integer_of_uint32 n)" lemma integer_of_uint32_signed_code [code]: "integer_of_uint32_signed n = (if bit n 31 then undefined integer_of_uint32 n else integer_of_int (uint (Rep_uint32' n)))" by (simp add: integer_of_uint32_signed_def integer_of_uint32_def) lemma integer_of_uint32_code [code]: "integer_of_uint32 n = (if bit n 31 then integer_of_uint32_signed (n AND 0x7FFFFFFF) OR 0x80000000 else integer_of_uint32_signed n)" proof - have \integer_of_uint32_signed (n AND 0x7FFFFFFF) OR 0x80000000 = Bit_Operations.set_bit 31 (integer_of_uint32_signed (take_bit 31 n))\ by (simp add: take_bit_eq_mask set_bit_eq_or push_bit_eq_mult mask_eq_exp_minus_1) moreover have \integer_of_uint32 n = Bit_Operations.set_bit 31 (integer_of_uint32 (take_bit 31 n))\ if \bit n 31\ proof (rule bit_eqI) fix m from that show \bit (integer_of_uint32 n) m = bit (Bit_Operations.set_bit 31 (integer_of_uint32 (take_bit 31 n))) m\ for m including integer.lifting by transfer (auto simp add: bit_simps dest: bit_imp_le_length) qed ultimately show ?thesis by simp (simp add: integer_of_uint32_signed_def bit_simps) qed end code_printing constant "integer_of_uint32" \ (SML) "IntInf.fromLarge (Word32.toLargeInt _) : IntInf.int" and (Haskell) "Prelude.toInteger" | constant "integer_of_uint32_signed" \ (OCaml) "Z.of'_int32" and (Scala) "BigInt" section \Quickcheck setup\ definition uint32_of_natural :: "natural \ uint32" where "uint32_of_natural x \ Uint32 (integer_of_natural x)" instantiation uint32 :: "{random, exhaustive, full_exhaustive}" begin definition "random_uint32 \ qc_random_cnv uint32_of_natural" definition "exhaustive_uint32 \ qc_exhaustive_cnv uint32_of_natural" definition "full_exhaustive_uint32 \ qc_full_exhaustive_cnv uint32_of_natural" instance .. end instantiation uint32 :: narrowing begin interpretation quickcheck_narrowing_samples "\i. let x = Uint32 i in (x, 0xFFFFFFFF - x)" "0" "Typerep.Typerep (STR ''Uint32.uint32'') []" . definition "narrowing_uint32 d = qc_narrowing_drawn_from (narrowing_samples d) d" declare [[code drop: "partial_term_of :: uint32 itself \ _"]] lemmas partial_term_of_uint32 [code] = partial_term_of_code instance .. end end diff --git a/thys/Native_Word/Uint64.thy b/thys/Native_Word/Uint64.thy --- a/thys/Native_Word/Uint64.thy +++ b/thys/Native_Word/Uint64.thy @@ -1,889 +1,889 @@ (* Title: Uint64.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Unsigned words of 64 bits\ theory Uint64 imports Word_Type_Copies Code_Target_Integer_Bit begin text \ PolyML (in version 5.7) provides a Word64 structure only when run in 64-bit mode. Therefore, we by default provide an implementation of 64-bit words using \verb$IntInf.int$ and masking. The code target \texttt{SML\_word} replaces this implementation and maps the operations directly to the \verb$Word64$ structure provided by the Standard ML implementations. The \verb$Eval$ target used by @{command value} and @{method eval} dynamically tests at runtime for the version of PolyML and uses PolyML's Word64 structure if it detects a 64-bit version which does not suffer from a division bug found in PolyML 5.6. \ section \Type definition and primitive operations\ typedef uint64 = \UNIV :: 64 word set\ .. global_interpretation uint64: word_type_copy Abs_uint64 Rep_uint64 using type_definition_uint64 by (rule word_type_copy.intro) setup_lifting type_definition_uint64 declare uint64.of_word_of [code abstype] declare Quotient_uint64 [transfer_rule] instantiation uint64 :: \{comm_ring_1, semiring_modulo, equal, linorder}\ begin lift_definition zero_uint64 :: uint64 is 0 . lift_definition one_uint64 :: uint64 is 1 . lift_definition plus_uint64 :: \uint64 \ uint64 \ uint64\ is \(+)\ . lift_definition uminus_uint64 :: \uint64 \ uint64\ is uminus . lift_definition minus_uint64 :: \uint64 \ uint64 \ uint64\ is \(-)\ . lift_definition times_uint64 :: \uint64 \ uint64 \ uint64\ is \(*)\ . lift_definition divide_uint64 :: \uint64 \ uint64 \ uint64\ is \(div)\ . lift_definition modulo_uint64 :: \uint64 \ uint64 \ uint64\ is \(mod)\ . lift_definition equal_uint64 :: \uint64 \ uint64 \ bool\ is \HOL.equal\ . lift_definition less_eq_uint64 :: \uint64 \ uint64 \ bool\ is \(\)\ . lift_definition less_uint64 :: \uint64 \ uint64 \ bool\ is \(<)\ . global_interpretation uint64: word_type_copy_ring Abs_uint64 Rep_uint64 by standard (fact zero_uint64.rep_eq one_uint64.rep_eq plus_uint64.rep_eq uminus_uint64.rep_eq minus_uint64.rep_eq times_uint64.rep_eq divide_uint64.rep_eq modulo_uint64.rep_eq equal_uint64.rep_eq less_eq_uint64.rep_eq less_uint64.rep_eq)+ instance proof - show \OFCLASS(uint64, comm_ring_1_class)\ by (rule uint64.of_class_comm_ring_1) show \OFCLASS(uint64, semiring_modulo_class)\ by (fact uint64.of_class_semiring_modulo) show \OFCLASS(uint64, equal_class)\ by (fact uint64.of_class_equal) show \OFCLASS(uint64, linorder_class)\ by (fact uint64.of_class_linorder) qed end instantiation uint64 :: ring_bit_operations begin lift_definition bit_uint64 :: \uint64 \ nat \ bool\ is bit . lift_definition not_uint64 :: \uint64 \ uint64\ is \Bit_Operations.not\ . lift_definition and_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.and\ . lift_definition or_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.or\ . lift_definition xor_uint64 :: \uint64 \ uint64 \ uint64\ is \Bit_Operations.xor\ . lift_definition mask_uint64 :: \nat \ uint64\ is mask . lift_definition push_bit_uint64 :: \nat \ uint64 \ uint64\ is push_bit . lift_definition drop_bit_uint64 :: \nat \ uint64 \ uint64\ is drop_bit . lift_definition signed_drop_bit_uint64 :: \nat \ uint64 \ uint64\ is signed_drop_bit . lift_definition take_bit_uint64 :: \nat \ uint64 \ uint64\ is take_bit . lift_definition set_bit_uint64 :: \nat \ uint64 \ uint64\ is Bit_Operations.set_bit . lift_definition unset_bit_uint64 :: \nat \ uint64 \ uint64\ is unset_bit . lift_definition flip_bit_uint64 :: \nat \ uint64 \ uint64\ is flip_bit . global_interpretation uint64: word_type_copy_bits Abs_uint64 Rep_uint64 signed_drop_bit_uint64 by standard (fact bit_uint64.rep_eq not_uint64.rep_eq and_uint64.rep_eq or_uint64.rep_eq xor_uint64.rep_eq mask_uint64.rep_eq push_bit_uint64.rep_eq drop_bit_uint64.rep_eq signed_drop_bit_uint64.rep_eq take_bit_uint64.rep_eq set_bit_uint64.rep_eq unset_bit_uint64.rep_eq flip_bit_uint64.rep_eq)+ instance by (fact uint64.of_class_ring_bit_operations) end lift_definition uint64_of_nat :: \nat \ uint64\ is word_of_nat . lift_definition nat_of_uint64 :: \uint64 \ nat\ is unat . lift_definition uint64_of_int :: \int \ uint64\ is word_of_int . lift_definition int_of_uint64 :: \uint64 \ int\ is uint . context includes integer.lifting begin lift_definition Uint64 :: \integer \ uint64\ is word_of_int . lift_definition integer_of_uint64 :: \uint64 \ integer\ is uint . end global_interpretation uint64: word_type_copy_more Abs_uint64 Rep_uint64 signed_drop_bit_uint64 uint64_of_nat nat_of_uint64 uint64_of_int int_of_uint64 Uint64 integer_of_uint64 apply standard apply (simp_all add: uint64_of_nat.rep_eq nat_of_uint64.rep_eq uint64_of_int.rep_eq int_of_uint64.rep_eq Uint64.rep_eq integer_of_uint64.rep_eq integer_eq_iff) done instantiation uint64 :: "{size, msb, lsb, set_bit, bit_comprehension}" begin lift_definition size_uint64 :: \uint64 \ nat\ is size . lift_definition msb_uint64 :: \uint64 \ bool\ is msb . lift_definition lsb_uint64 :: \uint64 \ bool\ is lsb . text \Workaround: avoid name space clash by spelling out \<^text>\lift_definition\ explicitly.\ definition set_bit_uint64 :: \uint64 \ nat \ bool \ uint64\ where set_bit_uint64_eq: \set_bit_uint64 a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ context includes lifting_syntax begin lemma set_bit_uint64_transfer [transfer_rule]: \(cr_uint64 ===> (=) ===> (\) ===> cr_uint64) Generic_set_bit.set_bit Generic_set_bit.set_bit\ by (simp only: set_bit_eq [abs_def] set_bit_uint64_eq [abs_def]) transfer_prover end lift_definition set_bits_uint64 :: \(nat \ bool) \ uint64\ is set_bits . lift_definition set_bits_aux_uint64 :: \(nat \ bool) \ nat \ uint64 \ uint64\ is set_bits_aux . global_interpretation uint64: word_type_copy_misc Abs_uint64 Rep_uint64 signed_drop_bit_uint64 uint64_of_nat nat_of_uint64 uint64_of_int int_of_uint64 Uint64 integer_of_uint64 64 set_bits_aux_uint64 by (standard; transfer) simp_all instance using uint64.of_class_bit_comprehension uint64.of_class_set_bit uint64.of_class_lsb by simp_all standard end section \Code setup\ text \ For SML, we generate an implementation of unsigned 64-bit words using \verb$IntInf.int$. If @{ML "LargeWord.wordSize > 63"} of the Isabelle/ML runtime environment holds, then we assume that there is also a \Word64\ structure available and accordingly replace the implementation for the target \verb$Eval$. \ code_printing code_module "Uint64" \ (SML) \(* Test that words can handle numbers between 0 and 63 *) val _ = if 6 <= Word.wordSize then () else raise (Fail ("wordSize less than 6")); structure Uint64 : sig eqtype uint64; val zero : uint64; val one : uint64; val fromInt : IntInf.int -> uint64; val toInt : uint64 -> IntInf.int; val toLarge : uint64 -> LargeWord.word; val fromLarge : LargeWord.word -> uint64 val plus : uint64 -> uint64 -> uint64; val minus : uint64 -> uint64 -> uint64; val times : uint64 -> uint64 -> uint64; val divide : uint64 -> uint64 -> uint64; val modulus : uint64 -> uint64 -> uint64; val negate : uint64 -> uint64; val less_eq : uint64 -> uint64 -> bool; val less : uint64 -> uint64 -> bool; val notb : uint64 -> uint64; val andb : uint64 -> uint64 -> uint64; val orb : uint64 -> uint64 -> uint64; val xorb : uint64 -> uint64 -> uint64; val shiftl : uint64 -> IntInf.int -> uint64; val shiftr : uint64 -> IntInf.int -> uint64; val shiftr_signed : uint64 -> IntInf.int -> uint64; val set_bit : uint64 -> IntInf.int -> bool -> uint64; val test_bit : uint64 -> IntInf.int -> bool; end = struct type uint64 = IntInf.int; val mask = 0xFFFFFFFFFFFFFFFF : IntInf.int; val zero = 0 : IntInf.int; val one = 1 : IntInf.int; fun fromInt x = IntInf.andb(x, mask); fun toInt x = x fun toLarge x = LargeWord.fromLargeInt (IntInf.toLarge x); fun fromLarge x = IntInf.fromLarge (LargeWord.toLargeInt x); fun plus x y = IntInf.andb(IntInf.+(x, y), mask); fun minus x y = IntInf.andb(IntInf.-(x, y), mask); fun negate x = IntInf.andb(IntInf.~(x), mask); fun times x y = IntInf.andb(IntInf.*(x, y), mask); fun divide x y = IntInf.div(x, y); fun modulus x y = IntInf.mod(x, y); fun less_eq x y = IntInf.<=(x, y); fun less x y = IntInf.<(x, y); fun notb x = IntInf.andb(IntInf.notb(x), mask); fun orb x y = IntInf.orb(x, y); fun andb x y = IntInf.andb(x, y); fun xorb x y = IntInf.xorb(x, y); val maxWord = IntInf.pow (2, Word.wordSize); fun shiftl x n = if n < maxWord then IntInf.andb(IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n)), mask) else 0; fun shiftr x n = if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) else 0; val msb_mask = 0x8000000000000000 : IntInf.int; fun shiftr_signed x i = if IntInf.andb(x, msb_mask) = 0 then shiftr x i else if i >= 64 then 0xFFFFFFFFFFFFFFFF else let val x' = shiftr x i val m' = IntInf.andb(IntInf.<<(mask, Word.max(0w64 - Word.fromLargeInt (IntInf.toLarge i), 0w0)), mask) in IntInf.orb(x', m') end; fun test_bit x n = if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0 else false; fun set_bit x n b = if n < 64 then if b then IntInf.orb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) else IntInf.andb (x, IntInf.notb (IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n)))) else x; end \ code_reserved SML Uint64 setup \ let val polyml64 = LargeWord.wordSize > 63; (* PolyML 5.6 has bugs in its Word64 implementation. We test for one such bug and refrain from using Word64 in that case. Testing is done with dynamic code evaluation such that the compiler does not choke on the Word64 structure, which need not be present in a 32bit environment. *) val error_msg = "Buggy Word64 structure"; val test_code = "val _ = if Word64.div (0w18446744073709551611 : Word64.word, 0w3) = 0w6148914691236517203 then ()\n" ^ "else raise (Fail \"" ^ error_msg ^ "\");"; val f = Exn.interruptible_capture (fn () => ML_Compiler.eval ML_Compiler.flags Position.none (ML_Lex.tokenize test_code)) val use_Word64 = polyml64 andalso (case f () of Exn.Res _ => true | Exn.Exn (e as ERROR m) => if String.isSuffix error_msg m then false else Exn.reraise e | Exn.Exn e => Exn.reraise e) ; val newline = "\n"; val content = "structure Uint64 : sig" ^ newline ^ " eqtype uint64;" ^ newline ^ " val zero : uint64;" ^ newline ^ " val one : uint64;" ^ newline ^ " val fromInt : IntInf.int -> uint64;" ^ newline ^ " val toInt : uint64 -> IntInf.int;" ^ newline ^ " val toLarge : uint64 -> LargeWord.word;" ^ newline ^ " val fromLarge : LargeWord.word -> uint64" ^ newline ^ " val plus : uint64 -> uint64 -> uint64;" ^ newline ^ " val minus : uint64 -> uint64 -> uint64;" ^ newline ^ " val times : uint64 -> uint64 -> uint64;" ^ newline ^ " val divide : uint64 -> uint64 -> uint64;" ^ newline ^ " val modulus : uint64 -> uint64 -> uint64;" ^ newline ^ " val negate : uint64 -> uint64;" ^ newline ^ " val less_eq : uint64 -> uint64 -> bool;" ^ newline ^ " val less : uint64 -> uint64 -> bool;" ^ newline ^ " val notb : uint64 -> uint64;" ^ newline ^ " val andb : uint64 -> uint64 -> uint64;" ^ newline ^ " val orb : uint64 -> uint64 -> uint64;" ^ newline ^ " val xorb : uint64 -> uint64 -> uint64;" ^ newline ^ " val shiftl : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val shiftr : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val shiftr_signed : uint64 -> IntInf.int -> uint64;" ^ newline ^ " val set_bit : uint64 -> IntInf.int -> bool -> uint64;" ^ newline ^ " val test_bit : uint64 -> IntInf.int -> bool;" ^ newline ^ "end = struct" ^ newline ^ "" ^ newline ^ "type uint64 = Word64.word;" ^ newline ^ "" ^ newline ^ "val zero = (0wx0 : uint64);" ^ newline ^ "" ^ newline ^ "val one = (0wx1 : uint64);" ^ newline ^ "" ^ newline ^ "fun fromInt x = Word64.fromLargeInt (IntInf.toLarge x);" ^ newline ^ "" ^ newline ^ "fun toInt x = IntInf.fromLarge (Word64.toLargeInt x);" ^ newline ^ "" ^ newline ^ "fun fromLarge x = Word64.fromLarge x;" ^ newline ^ "" ^ newline ^ "fun toLarge x = Word64.toLarge x;" ^ newline ^ "" ^ newline ^ "fun plus x y = Word64.+(x, y);" ^ newline ^ "" ^ newline ^ "fun minus x y = Word64.-(x, y);" ^ newline ^ "" ^ newline ^ "fun negate x = Word64.~(x);" ^ newline ^ "" ^ newline ^ "fun times x y = Word64.*(x, y);" ^ newline ^ "" ^ newline ^ "fun divide x y = Word64.div(x, y);" ^ newline ^ "" ^ newline ^ "fun modulus x y = Word64.mod(x, y);" ^ newline ^ "" ^ newline ^ "fun less_eq x y = Word64.<=(x, y);" ^ newline ^ "" ^ newline ^ "fun less x y = Word64.<(x, y);" ^ newline ^ "" ^ newline ^ "fun set_bit x n b =" ^ newline ^ " let val mask = Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ " in if b then Word64.orb (x, mask)" ^ newline ^ " else Word64.andb (x, Word64.notb mask)" ^ newline ^ " end" ^ newline ^ "" ^ newline ^ "fun shiftl x n =" ^ newline ^ " Word64.<< (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun shiftr x n =" ^ newline ^ " Word64.>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun shiftr_signed x n =" ^ newline ^ " Word64.~>> (x, Word.fromLargeInt (IntInf.toLarge n))" ^ newline ^ "" ^ newline ^ "fun test_bit x n =" ^ newline ^ " Word64.andb (x, Word64.<< (0wx1, Word.fromLargeInt (IntInf.toLarge n))) <> Word64.fromInt 0" ^ newline ^ "" ^ newline ^ "val notb = Word64.notb" ^ newline ^ "" ^ newline ^ "fun andb x y = Word64.andb(x, y);" ^ newline ^ "" ^ newline ^ "fun orb x y = Word64.orb(x, y);" ^ newline ^ "" ^ newline ^ "fun xorb x y = Word64.xorb(x, y);" ^ newline ^ "" ^ newline ^ "end (*struct Uint64*)" val target_SML64 = "SML_word"; in (if use_Word64 then Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(Code_Runtime.target, SOME (content, []))])) else I) #> Code_Target.set_printings (Code_Symbol.Module ("Uint64", [(target_SML64, SOME (content, []))])) end \ code_printing code_module Uint64 \ (Haskell) \module Uint64(Int64, Word64) where import Data.Int(Int64) import Data.Word(Word64)\ code_reserved Haskell Uint64 text \ OCaml and Scala provide only signed 64bit numbers, so we use these and implement sign-sensitive operations like comparisons manually. \ code_printing code_module "Uint64" \ (OCaml) \module Uint64 : sig val less : int64 -> int64 -> bool val less_eq : int64 -> int64 -> bool val set_bit : int64 -> Z.t -> bool -> int64 val shiftl : int64 -> Z.t -> int64 val shiftr : int64 -> Z.t -> int64 val shiftr_signed : int64 -> Z.t -> int64 val test_bit : int64 -> Z.t -> bool end = struct (* negative numbers have their highest bit set, so they are greater than positive ones *) let less x y = if Int64.compare x Int64.zero < 0 then Int64.compare y Int64.zero < 0 && Int64.compare x y < 0 else Int64.compare y Int64.zero < 0 || Int64.compare x y < 0;; let less_eq x y = if Int64.compare x Int64.zero < 0 then Int64.compare y Int64.zero < 0 && Int64.compare x y <= 0 else Int64.compare y Int64.zero < 0 || Int64.compare x y <= 0;; let set_bit x n b = let mask = Int64.shift_left Int64.one (Z.to_int n) in if b then Int64.logor x mask else Int64.logand x (Int64.lognot mask);; let shiftl x n = Int64.shift_left x (Z.to_int n);; let shiftr x n = Int64.shift_right_logical x (Z.to_int n);; let shiftr_signed x n = Int64.shift_right x (Z.to_int n);; let test_bit x n = Int64.compare (Int64.logand x (Int64.shift_left Int64.one (Z.to_int n))) Int64.zero <> 0;; end;; (*struct Uint64*)\ code_reserved OCaml Uint64 code_printing code_module Uint64 \ (Scala) \object Uint64 { def less(x: Long, y: Long) : Boolean = if (x < 0) y < 0 && x < y else y < 0 || x < y def less_eq(x: Long, y: Long) : Boolean = if (x < 0) y < 0 && x <= y else y < 0 || x <= y def set_bit(x: Long, n: BigInt, b: Boolean) : Long = if (b) x | (1L << n.intValue) else x & (1L << n.intValue).unary_~ def shiftl(x: Long, n: BigInt) : Long = x << n.intValue def shiftr(x: Long, n: BigInt) : Long = x >>> n.intValue def shiftr_signed(x: Long, n: BigInt) : Long = x >> n.intValue def test_bit(x: Long, n: BigInt) : Boolean = (x & (1L << n.intValue)) != 0 } /* object Uint64 */\ code_reserved Scala Uint64 text \ OCaml's conversion from Big\_int to int64 demands that the value fits int a signed 64-bit integer. The following justifies the implementation. \ context includes bit_operations_syntax begin definition Uint64_signed :: "integer \ uint64" where "Uint64_signed i = (if i < -(0x8000000000000000) \ i \ 0x8000000000000000 then undefined Uint64 i else Uint64 i)" lemma Uint64_code [code]: "Uint64 i = (let i' = i AND 0xFFFFFFFFFFFFFFFF in if bit i' 63 then Uint64_signed (i' - 0x10000000000000000) else Uint64_signed i')" including undefined_transfer integer.lifting unfolding Uint64_signed_def apply transfer apply (subst word_of_int_via_signed) apply (auto simp add: push_bit_of_1 mask_eq_exp_minus_1 word_of_int_via_signed cong del: if_cong) done lemma Uint64_signed_code [code]: "Rep_uint64 (Uint64_signed i) = (if i < -(0x8000000000000000) \ i \ 0x8000000000000000 then Rep_uint64 (undefined Uint64 i) else word_of_int (int_of_integer_symbolic i))" -unfolding Uint64_signed_def Uint64_def int_of_integer_symbolic_def word_of_integer_def +unfolding Uint64_signed_def Uint64_def int_of_integer_symbolic_def by(simp add: Abs_uint64_inverse) end text \ Avoid @{term Abs_uint64} in generated code, use @{term Rep_uint64'} instead. The symbolic implementations for code\_simp use @{term Rep_uint64}. The new destructor @{term Rep_uint64'} is executable. As the simplifier is given the [code abstract] equations literally, we cannot implement @{term Rep_uint64} directly, because that makes code\_simp loop. If code generation raises Match, some equation probably contains @{term Rep_uint64} ([code abstract] equations for @{typ uint64} may use @{term Rep_uint64} because these instances will be folded away.) To convert @{typ "64 word"} values into @{typ uint64}, use @{term "Abs_uint64'"}. \ definition Rep_uint64' where [simp]: "Rep_uint64' = Rep_uint64" lemma Rep_uint64'_transfer [transfer_rule]: "rel_fun cr_uint64 (=) (\x. x) Rep_uint64'" unfolding Rep_uint64'_def by(rule uint64.rep_transfer) lemma Rep_uint64'_code [code]: "Rep_uint64' x = (BITS n. bit x n)" by transfer (simp add: set_bits_bit_eq) lift_definition Abs_uint64' :: "64 word \ uint64" is "\x :: 64 word. x" . lemma Abs_uint64'_code [code]: "Abs_uint64' x = Uint64 (integer_of_int (uint x))" including integer.lifting by transfer simp declare [[code drop: "term_of_class.term_of :: uint64 \ _"]] lemma term_of_uint64_code [code]: defines "TR \ typerep.Typerep" and "bit0 \ STR ''Numeral_Type.bit0''" shows "term_of_class.term_of x = Code_Evaluation.App (Code_Evaluation.Const (STR ''Uint64.uint64.Abs_uint64'') (TR (STR ''fun'') [TR (STR ''Word.word'') [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR bit0 [TR (STR ''Numeral_Type.num1'') []]]]]]]], TR (STR ''Uint64.uint64'') []])) (term_of_class.term_of (Rep_uint64' x))" by(simp add: term_of_anything) code_printing type_constructor uint64 \ (SML) "Uint64.uint64" and (Haskell) "Uint64.Word64" and (OCaml) "int64" and (Scala) "Long" | constant Uint64 \ (SML) "Uint64.fromInt" and (Haskell) "(Prelude.fromInteger _ :: Uint64.Word64)" and (Haskell_Quickcheck) "(Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Word64)" and (Scala) "_.longValue" | constant Uint64_signed \ (OCaml) "Z.to'_int64" | constant "0 :: uint64" \ (SML) "Uint64.zero" and (Haskell) "(0 :: Uint64.Word64)" and (OCaml) "Int64.zero" and (Scala) "0" | constant "1 :: uint64" \ (SML) "Uint64.one" and (Haskell) "(1 :: Uint64.Word64)" and (OCaml) "Int64.one" and (Scala) "1" | constant "plus :: uint64 \ _ " \ (SML) "Uint64.plus" and (Haskell) infixl 6 "+" and (OCaml) "Int64.add" and (Scala) infixl 7 "+" | constant "uminus :: uint64 \ _" \ (SML) "Uint64.negate" and (Haskell) "negate" and (OCaml) "Int64.neg" and (Scala) "!(- _)" | constant "minus :: uint64 \ _" \ (SML) "Uint64.minus" and (Haskell) infixl 6 "-" and (OCaml) "Int64.sub" and (Scala) infixl 7 "-" | constant "times :: uint64 \ _ \ _" \ (SML) "Uint64.times" and (Haskell) infixl 7 "*" and (OCaml) "Int64.mul" and (Scala) infixl 8 "*" | constant "HOL.equal :: uint64 \ _ \ bool" \ (SML) "!((_ : Uint64.uint64) = _)" and (Haskell) infix 4 "==" and (OCaml) "(Int64.compare _ _ = 0)" and (Scala) infixl 5 "==" | class_instance uint64 :: equal \ (Haskell) - | constant "less_eq :: uint64 \ _ \ bool" \ (SML) "Uint64.less'_eq" and (Haskell) infix 4 "<=" and (OCaml) "Uint64.less'_eq" and (Scala) "Uint64.less'_eq" | constant "less :: uint64 \ _ \ bool" \ (SML) "Uint64.less" and (Haskell) infix 4 "<" and (OCaml) "Uint64.less" and (Scala) "Uint64.less" | constant "Bit_Operations.not :: uint64 \ _" \ (SML) "Uint64.notb" and (Haskell) "Data'_Bits.complement" and (OCaml) "Int64.lognot" and (Scala) "_.unary'_~" | constant "Bit_Operations.and :: uint64 \ _" \ (SML) "Uint64.andb" and (Haskell) infixl 7 "Data_Bits..&." and (OCaml) "Int64.logand" and (Scala) infixl 3 "&" | constant "Bit_Operations.or :: uint64 \ _" \ (SML) "Uint64.orb" and (Haskell) infixl 5 "Data_Bits..|." and (OCaml) "Int64.logor" and (Scala) infixl 1 "|" | constant "Bit_Operations.xor :: uint64 \ _" \ (SML) "Uint64.xorb" and (Haskell) "Data'_Bits.xor" and (OCaml) "Int64.logxor" and (Scala) infixl 2 "^" definition uint64_divmod :: "uint64 \ uint64 \ uint64 \ uint64" where "uint64_divmod x y = (if y = 0 then (undefined ((div) :: uint64 \ _) x (0 :: uint64), undefined ((mod) :: uint64 \ _) x (0 :: uint64)) else (x div y, x mod y))" definition uint64_div :: "uint64 \ uint64 \ uint64" where "uint64_div x y = fst (uint64_divmod x y)" definition uint64_mod :: "uint64 \ uint64 \ uint64" where "uint64_mod x y = snd (uint64_divmod x y)" lemma div_uint64_code [code]: "x div y = (if y = 0 then 0 else uint64_div x y)" including undefined_transfer unfolding uint64_divmod_def uint64_div_def by transfer (simp add: word_div_def) lemma mod_uint64_code [code]: "x mod y = (if y = 0 then x else uint64_mod x y)" including undefined_transfer unfolding uint64_mod_def uint64_divmod_def by transfer (simp add: word_mod_def) definition uint64_sdiv :: "uint64 \ uint64 \ uint64" where [code del]: "uint64_sdiv x y = (if y = 0 then undefined ((div) :: uint64 \ _) x (0 :: uint64) else Abs_uint64 (Rep_uint64 x sdiv Rep_uint64 y))" definition div0_uint64 :: "uint64 \ uint64" where [code del]: "div0_uint64 x = undefined ((div) :: uint64 \ _) x (0 :: uint64)" declare [[code abort: div0_uint64]] definition mod0_uint64 :: "uint64 \ uint64" where [code del]: "mod0_uint64 x = undefined ((mod) :: uint64 \ _) x (0 :: uint64)" declare [[code abort: mod0_uint64]] lemma uint64_divmod_code [code]: "uint64_divmod x y = (if 0x8000000000000000 \ y then if x < y then (0, x) else (1, x - y) else if y = 0 then (div0_uint64 x, mod0_uint64 x) else let q = push_bit 1 (uint64_sdiv (drop_bit 1 x) y); r = x - q * y in if r \ y then (q + 1, r - y) else (q, r))" including undefined_transfer unfolding uint64_divmod_def uint64_sdiv_def div0_uint64_def mod0_uint64_def less_eq_uint64.rep_eq apply transfer apply (simp add: divmod_via_sdivmod push_bit_eq_mult) done lemma uint64_sdiv_code [code]: "Rep_uint64 (uint64_sdiv x y) = (if y = 0 then Rep_uint64 (undefined ((div) :: uint64 \ _) x (0 :: uint64)) else Rep_uint64 x sdiv Rep_uint64 y)" unfolding uint64_sdiv_def by(simp add: Abs_uint64_inverse) text \ Note that we only need a translation for signed division, but not for the remainder because @{thm uint64_divmod_code} computes both with division only. \ code_printing constant uint64_div \ (SML) "Uint64.divide" and (Haskell) "Prelude.div" | constant uint64_mod \ (SML) "Uint64.modulus" and (Haskell) "Prelude.mod" | constant uint64_divmod \ (Haskell) "divmod" | constant uint64_sdiv \ (OCaml) "Int64.div" and (Scala) "_ '/ _" definition uint64_test_bit :: "uint64 \ integer \ bool" where [code del]: "uint64_test_bit x n = (if n < 0 \ 63 < n then undefined (bit :: uint64 \ _) x n else bit x (nat_of_integer n))" lemma bit_uint64_code [code]: "bit x n \ n < 64 \ uint64_test_bit x (integer_of_nat n)" including undefined_transfer integer.lifting unfolding uint64_test_bit_def by transfer (auto dest: bit_imp_le_length) lemma uint64_test_bit_code [code]: "uint64_test_bit w n = (if n < 0 \ 63 < n then undefined (bit :: uint64 \ _) w n else bit (Rep_uint64 w) (nat_of_integer n))" unfolding uint64_test_bit_def by(simp add: bit_uint64.rep_eq) code_printing constant uint64_test_bit \ (SML) "Uint64.test'_bit" and (Haskell) "Data'_Bits.testBitBounded" and (OCaml) "Uint64.test'_bit" and (Scala) "Uint64.test'_bit" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_test'_bit out of bounds\") else Uint64.test'_bit x i)" definition uint64_set_bit :: "uint64 \ integer \ bool \ uint64" where [code del]: "uint64_set_bit x n b = (if n < 0 \ 63 < n then undefined (set_bit :: uint64 \ _) x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_uint64_code [code]: "set_bit x n b = (if n < 64 then uint64_set_bit x (integer_of_nat n) b else x)" including undefined_transfer integer.lifting unfolding uint64_set_bit_def by(transfer)(auto cong: conj_cong simp add: not_less set_bit_beyond word_size) lemma uint64_set_bit_code [code]: "Rep_uint64 (uint64_set_bit w n b) = (if n < 0 \ 63 < n then Rep_uint64 (undefined (set_bit :: uint64 \ _) w n b) else set_bit (Rep_uint64 w) (nat_of_integer n) b)" including undefined_transfer unfolding uint64_set_bit_def by transfer simp code_printing constant uint64_set_bit \ (SML) "Uint64.set'_bit" and (Haskell) "Data'_Bits.setBitBounded" and (OCaml) "Uint64.set'_bit" and (Scala) "Uint64.set'_bit" and (Eval) "(fn x => fn i => fn b => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_set'_bit out of bounds\") else Uint64.set'_bit x i b)" definition uint64_shiftl :: "uint64 \ integer \ uint64" where [code del]: "uint64_shiftl x n = (if n < 0 \ 64 \ n then undefined (push_bit :: nat \ uint64 \ _) x n else push_bit (nat_of_integer n) x)" lemma shiftl_uint64_code [code]: "push_bit n x = (if n < 64 then uint64_shiftl x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint64_shiftl_def by transfer simp lemma uint64_shiftl_code [code]: "Rep_uint64 (uint64_shiftl w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined (push_bit :: nat \ uint64 \ _) w n) else push_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_shiftl_def by transfer simp code_printing constant uint64_shiftl \ (SML) "Uint64.shiftl" and (Haskell) "Data'_Bits.shiftlBounded" and (OCaml) "Uint64.shiftl" and (Scala) "Uint64.shiftl" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftl out of bounds\") else Uint64.shiftl x i)" definition uint64_shiftr :: "uint64 \ integer \ uint64" where [code del]: "uint64_shiftr x n = (if n < 0 \ 64 \ n then undefined (drop_bit :: nat \ uint64 \ _) x n else drop_bit (nat_of_integer n) x)" lemma shiftr_uint64_code [code]: "drop_bit n x = (if n < 64 then uint64_shiftr x (integer_of_nat n) else 0)" including undefined_transfer integer.lifting unfolding uint64_shiftr_def by transfer simp lemma uint64_shiftr_code [code]: "Rep_uint64 (uint64_shiftr w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined (drop_bit :: nat \ uint64 \ _) w n) else drop_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_shiftr_def by transfer simp code_printing constant uint64_shiftr \ (SML) "Uint64.shiftr" and (Haskell) "Data'_Bits.shiftrBounded" and (OCaml) "Uint64.shiftr" and (Scala) "Uint64.shiftr" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr out of bounds\") else Uint64.shiftr x i)" definition uint64_sshiftr :: "uint64 \ integer \ uint64" where [code del]: "uint64_sshiftr x n = (if n < 0 \ 64 \ n then undefined signed_drop_bit_uint64 n x else signed_drop_bit_uint64 (nat_of_integer n) x)" lemma sshiftr_uint64_code [code]: "signed_drop_bit_uint64 n x = (if n < 64 then uint64_sshiftr x (integer_of_nat n) else if bit x 63 then - 1 else 0)" including undefined_transfer integer.lifting unfolding uint64_sshiftr_def by transfer (simp add: not_less signed_drop_bit_beyond) lemma uint64_sshiftr_code [code]: "Rep_uint64 (uint64_sshiftr w n) = (if n < 0 \ 64 \ n then Rep_uint64 (undefined signed_drop_bit_uint64 n w) else signed_drop_bit (nat_of_integer n) (Rep_uint64 w))" including undefined_transfer unfolding uint64_sshiftr_def by transfer simp code_printing constant uint64_sshiftr \ (SML) "Uint64.shiftr'_signed" and (Haskell) "(Prelude.fromInteger (Prelude.toInteger (Data'_Bits.shiftrBounded (Prelude.fromInteger (Prelude.toInteger _) :: Uint64.Int64) _)) :: Uint64.Word64)" and (OCaml) "Uint64.shiftr'_signed" and (Scala) "Uint64.shiftr'_signed" and (Eval) "(fn x => fn i => if i < 0 orelse i >= 64 then raise (Fail \"argument to uint64'_shiftr'_signed out of bounds\") else Uint64.shiftr'_signed x i)" context includes bit_operations_syntax begin lemma uint64_msb_test_bit: "msb x \ bit (x :: uint64) 63" by transfer (simp add: msb_word_iff_bit) lemma msb_uint64_code [code]: "msb x \ uint64_test_bit x 63" by (simp add: uint64_test_bit_def uint64_msb_test_bit) lemma uint64_of_int_code [code]: "uint64_of_int i = Uint64 (integer_of_int i)" including integer.lifting by transfer simp lemma int_of_uint64_code [code]: "int_of_uint64 x = int_of_integer (integer_of_uint64 x)" including integer.lifting by transfer simp lemma uint64_of_nat_code [code]: "uint64_of_nat = uint64_of_int \ int" by transfer (simp add: fun_eq_iff) lemma nat_of_uint64_code [code]: "nat_of_uint64 x = nat_of_integer (integer_of_uint64 x)" unfolding integer_of_uint64_def including integer.lifting by transfer simp definition integer_of_uint64_signed :: "uint64 \ integer" where "integer_of_uint64_signed n = (if bit n 63 then undefined integer_of_uint64 n else integer_of_uint64 n)" lemma integer_of_uint64_signed_code [code]: "integer_of_uint64_signed n = (if bit n 63 then undefined integer_of_uint64 n else integer_of_int (uint (Rep_uint64' n)))" by (simp add: integer_of_uint64_signed_def integer_of_uint64_def) lemma integer_of_uint64_code [code]: "integer_of_uint64 n = (if bit n 63 then integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 else integer_of_uint64_signed n)" proof - have \integer_of_uint64_signed (n AND 0x7FFFFFFFFFFFFFFF) OR 0x8000000000000000 = Bit_Operations.set_bit 63 (integer_of_uint64_signed (take_bit 63 n))\ by (simp add: take_bit_eq_mask set_bit_eq_or push_bit_eq_mult mask_eq_exp_minus_1) moreover have \integer_of_uint64 n = Bit_Operations.set_bit 63 (integer_of_uint64 (take_bit 63 n))\ if \bit n 63\ proof (rule bit_eqI) fix m from that show \bit (integer_of_uint64 n) m = bit (Bit_Operations.set_bit 63 (integer_of_uint64 (take_bit 63 n))) m\ for m including integer.lifting by transfer (auto simp add: bit_simps dest: bit_imp_le_length) qed ultimately show ?thesis by simp (simp add: integer_of_uint64_signed_def bit_simps) qed end code_printing constant "integer_of_uint64" \ (SML) "Uint64.toInt" and (Haskell) "Prelude.toInteger" | constant "integer_of_uint64_signed" \ (OCaml) "Z.of'_int64" and (Scala) "BigInt" section \Quickcheck setup\ definition uint64_of_natural :: "natural \ uint64" where "uint64_of_natural x \ Uint64 (integer_of_natural x)" instantiation uint64 :: "{random, exhaustive, full_exhaustive}" begin definition "random_uint64 \ qc_random_cnv uint64_of_natural" definition "exhaustive_uint64 \ qc_exhaustive_cnv uint64_of_natural" definition "full_exhaustive_uint64 \ qc_full_exhaustive_cnv uint64_of_natural" instance .. end instantiation uint64 :: narrowing begin interpretation quickcheck_narrowing_samples "\i. let x = Uint64 i in (x, 0xFFFFFFFFFFFFFFFF - x)" "0" "Typerep.Typerep (STR ''Uint64.uint64'') []" . definition "narrowing_uint64 d = qc_narrowing_drawn_from (narrowing_samples d) d" declare [[code drop: "partial_term_of :: uint64 itself \ _"]] lemmas partial_term_of_uint64 [code] = partial_term_of_code instance .. end end diff --git a/thys/Native_Word/Word_Type_Copies.thy b/thys/Native_Word/Word_Type_Copies.thy --- a/thys/Native_Word/Word_Type_Copies.thy +++ b/thys/Native_Word/Word_Type_Copies.thy @@ -1,329 +1,329 @@ (* Title: Word_Type_Copies.thy Author: Florian Haftmann, TU Muenchen *) chapter \Systematic approach towards type copies of word type\ theory Word_Type_Copies imports "HOL-Library.Word" "Word_Lib.Most_significant_bit" "Word_Lib.Least_significant_bit" "Word_Lib.Generic_set_bit" "Word_Lib.Bit_Comprehension" "Code_Target_Word_Base" begin text \The lifting machinery is not localized, hence the abstract proofs are carried out using morphisms.\ locale word_type_copy = fixes of_word :: \'b::len word \ 'a\ and word_of :: \'a \ 'b word\ assumes type_definition: \type_definition word_of of_word UNIV\ begin lemma word_of_word: \word_of (of_word w) = w\ using type_definition by (simp add: type_definition_def) lemma of_word_of [code abstype]: \of_word (word_of p) = p\ \ \Use an abstract type for code generation to disable pattern matching on \<^term>\of_word\.\ using type_definition by (simp add: type_definition_def) lemma word_of_eqI: \p = q\ if \word_of p = word_of q\ proof - from that have \of_word (word_of p) = of_word (word_of q)\ by simp then show ?thesis by (simp add: of_word_of) qed lemma eq_iff_word_of: \p = q \ word_of p = word_of q\ by (auto intro: word_of_eqI) end bundle constraintless begin declaration \ let val cs = map (rpair NONE o fst o dest_Const) [\<^term>\0\, \<^term>\(+)\, \<^term>\uminus\, \<^term>\(-)\, \<^term>\1\, \<^term>\(*)\, \<^term>\(div)\, \<^term>\(mod)\, \<^term>\HOL.equal\, \<^term>\(\)\, \<^term>\(<)\, \<^term>\(dvd)\, \<^term>\of_bool\, \<^term>\numeral\, \<^term>\of_nat\, \<^term>\bit\, \<^term>\Bit_Operations.not\, \<^term>\Bit_Operations.and\, \<^term>\Bit_Operations.or\, \<^term>\Bit_Operations.xor\, \<^term>\mask\, \<^term>\push_bit\, \<^term>\drop_bit\, \<^term>\take_bit\, \<^term>\Bit_Operations.set_bit\, \<^term>\unset_bit\, \<^term>\flip_bit\, \<^term>\msb\, \<^term>\lsb\, \<^term>\size\, \<^term>\Generic_set_bit.set_bit\, \<^term>\set_bits\] in K (Context.mapping I (fold Proof_Context.add_const_constraint cs)) end \ end locale word_type_copy_ring = word_type_copy opening constraintless + constrains word_of :: \'a \ 'b::len word\ assumes word_of_0 [code]: \word_of 0 = 0\ and word_of_1 [code]: \word_of 1 = 1\ and word_of_add [code]: \word_of (p + q) = word_of p + word_of q\ and word_of_minus [code]: \word_of (- p) = - (word_of p)\ and word_of_diff [code]: \word_of (p - q) = word_of p - word_of q\ and word_of_mult [code]: \word_of (p * q) = word_of p * word_of q\ and word_of_div [code]: \word_of (p div q) = word_of p div word_of q\ and word_of_mod [code]: \word_of (p mod q) = word_of p mod word_of q\ and equal_iff_word_of [code]: \HOL.equal p q \ HOL.equal (word_of p) (word_of q)\ and less_eq_iff_word_of [code]: \p \ q \ word_of p \ word_of q\ and less_iff_word_of [code]: \p < q \ word_of p < word_of q\ begin lemma of_class_comm_ring_1: \OFCLASS('a, comm_ring_1_class)\ by standard (simp_all add: eq_iff_word_of word_of_0 word_of_1 word_of_add word_of_minus word_of_diff word_of_mult algebra_simps) lemma of_class_semiring_modulo: \OFCLASS('a, semiring_modulo_class)\ by standard (simp_all add: eq_iff_word_of word_of_0 word_of_1 word_of_add word_of_minus word_of_diff word_of_mult word_of_mod word_of_div algebra_simps mod_mult_div_eq) lemma of_class_equal: \OFCLASS('a, equal_class)\ by standard (simp add: eq_iff_word_of equal_iff_word_of equal) lemma of_class_linorder: \OFCLASS('a, linorder_class)\ by standard (auto simp add: eq_iff_word_of less_eq_iff_word_of less_iff_word_of) end locale word_type_copy_bits = word_type_copy_ring opening constraintless bit_operations_syntax + constrains word_of :: \'a::{comm_ring_1, semiring_modulo, equal, linorder} \ 'b::len word\ fixes signed_drop_bit :: \nat \ 'a \ 'a\ assumes bit_eq_word_of [code]: \bit p = bit (word_of p)\ and word_of_not [code]: \word_of (NOT p) = NOT (word_of p)\ and word_of_and [code]: \word_of (p AND q) = word_of p AND word_of q\ and word_of_or [code]: \word_of (p OR q) = word_of p OR word_of q\ and word_of_xor [code]: \word_of (p XOR q) = word_of p XOR word_of q\ and word_of_mask [code]: \word_of (mask n) = mask n\ and word_of_push_bit [code]: \word_of (push_bit n p) = push_bit n (word_of p)\ and word_of_drop_bit [code]: \word_of (drop_bit n p) = drop_bit n (word_of p)\ and word_of_signed_drop_bit [code]: \word_of (signed_drop_bit n p) = Word.signed_drop_bit n (word_of p)\ and word_of_take_bit [code]: \word_of (take_bit n p) = take_bit n (word_of p)\ and word_of_set_bit [code]: \word_of (Bit_Operations.set_bit n p) = Bit_Operations.set_bit n (word_of p)\ and word_of_unset_bit [code]: \word_of (unset_bit n p) = unset_bit n (word_of p)\ and word_of_flip_bit [code]: \word_of (flip_bit n p) = flip_bit n (word_of p)\ begin lemma word_of_bool: \word_of (of_bool n) = of_bool n\ by (simp add: word_of_0 word_of_1) lemma word_of_nat: \word_of (of_nat n) = of_nat n\ by (induction n) (simp_all add: word_of_0 word_of_1 word_of_add) lemma word_of_numeral [simp]: \word_of (numeral n) = numeral n\ proof - have \word_of (of_nat (numeral n)) = of_nat (numeral n)\ by (simp only: word_of_nat) then show ?thesis by simp qed lemma word_of_power: \word_of (p ^ n) = word_of p ^ n\ by (induction n) (simp_all add: word_of_1 word_of_mult) lemma even_iff_word_of: \2 dvd p \ 2 dvd word_of p\ (is \?P \ ?Q\) proof assume ?P then obtain q where \p = 2 * q\ .. then show ?Q by (simp add: word_of_mult) next assume ?Q then obtain w where \word_of p = 2 * w\ .. then have \of_word (word_of p) = of_word (2 * w)\ by simp then have \p = 2 * of_word w\ by (simp add: eq_iff_word_of word_of_word word_of_mult) then show ?P by simp qed lemma of_class_ring_bit_operations: \OFCLASS('a, ring_bit_operations_class)\ proof - have induct: \P p\ if stable: \(\p. p div 2 = p \ P p)\ and rec: \(\p b. P p \ (of_bool b + 2 * p) div 2 = p \ P (of_bool b + 2 * p))\ for p :: 'a and P proof - from stable have stable': \(\p. word_of p div 2 = word_of p \ P p)\ by (simp add: eq_iff_word_of word_of_div) from rec have rec': \(\p b. P p \ (of_bool b + 2 * word_of p) div 2 = word_of p \ P (of_bool b + 2 * p))\ by (simp add: eq_iff_word_of word_of_add word_of_bool word_of_mult word_of_div) define w where \w = word_of p\ then have \p = of_word w\ by (simp add: of_word_of) also have \P (of_word w)\ proof (induction w rule: bits_induct) case (stable w) show ?case by (rule stable') (simp add: word_of_word stable) next case (rec w b) have \P (of_bool b + 2 * of_word w)\ by (rule rec') (simp_all add: word_of_word rec) also have \of_bool b + 2 * of_word w = of_word (of_bool b + 2 * w)\ by (simp add: eq_iff_word_of word_of_word word_of_add word_of_1 word_of_mult word_of_0) finally show ?case . qed finally show \P p\ . qed have \class.semiring_parity_axioms (+) (0::'a) (*) 1 (mod)\ by standard (simp_all add: eq_iff_word_of word_of_0 word_of_1 even_iff_word_of word_of_mod even_iff_mod_2_eq_zero) with of_class_semiring_modulo have \OFCLASS('a, semiring_parity_class)\ by (rule semiring_parity_class.intro) moreover have \class.semiring_bits_axioms (+) (-) (0::'a) (*) 1 (div) (mod) bit\ apply (standard, fact induct) apply (simp_all only: eq_iff_word_of word_of_0 word_of_1 word_of_bool word_of_numeral word_of_add word_of_diff word_of_mult word_of_div word_of_mod word_of_power even_iff_word_of bit_eq_word_of push_bit_take_bit drop_bit_take_bit even_drop_bit_iff_not_bit flip: push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod mask_eq_exp_minus_1) apply (auto simp add: ac_simps bit_simps drop_bit_exp_eq) done ultimately have \OFCLASS('a, semiring_bits_class)\ by (rule semiring_bits_class.intro) moreover have \class.semiring_bit_operations_axioms (+) (-) (*) (1::'a) (div) (mod) bit (AND) (OR) (XOR) mask Bit_Operations.set_bit unset_bit flip_bit push_bit drop_bit take_bit\ by standard (simp_all add: eq_iff_word_of word_of_push_bit word_of_power bit_eq_word_of word_of_and word_of_or word_of_xor word_of_mask word_of_diff word_of_1 bit_simps word_of_set_bit set_bit_eq_or word_of_unset_bit word_of_flip_bit flip_bit_eq_xor word_of_mult word_of_drop_bit word_of_div word_of_take_bit word_of_mod flip: mask_eq_exp_minus_1 push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod) ultimately have \OFCLASS('a, semiring_bit_operations_class)\ by (rule semiring_bit_operations_class.intro) moreover have \OFCLASS('a, ring_parity_class)\ using \OFCLASS('a, semiring_parity_class)\ by (rule ring_parity_class.intro) standard moreover have \class.ring_bit_operations_axioms (+) (-) (0::'a) (*) 1 bit uminus NOT\ by standard (simp_all add: eq_iff_word_of word_of_power bit_eq_word_of word_of_diff word_of_1 bit_simps linorder_not_le word_of_not word_of_0 word_of_minus minus_eq_not_minus_1) ultimately show \OFCLASS('a, ring_bit_operations_class)\ by (rule ring_bit_operations_class.intro) qed lemma [code]: \take_bit n a = a AND mask n\ for a :: 'a by (simp add: eq_iff_word_of word_of_take_bit word_of_and word_of_mask take_bit_eq_mask) lemma [code]: \mask (Suc n) = push_bit n (1 :: 'a) OR mask n\ \mask 0 = (0 :: 'a)\ by (simp_all add: eq_iff_word_of word_of_mask word_of_or word_of_push_bit word_of_0 word_of_1 mask_Suc_exp) lemma [code]: \Bit_Operations.set_bit n w = w OR push_bit n 1\ for w :: 'a by (simp add: eq_iff_word_of word_of_set_bit word_of_or word_of_push_bit word_of_1 set_bit_eq_or) lemma [code]: \unset_bit n w = w AND NOT (push_bit n 1)\ for w :: 'a by (simp add: eq_iff_word_of word_of_unset_bit word_of_and word_of_not word_of_push_bit word_of_1 unset_bit_eq_and_not) lemma [code]: \flip_bit n w = w XOR push_bit n 1\ for w :: 'a by (simp add: eq_iff_word_of word_of_flip_bit word_of_xor word_of_push_bit word_of_1 flip_bit_eq_xor) end locale word_type_copy_more = word_type_copy_bits + constrains word_of :: \'a::{ring_bit_operations, equal, linorder} \ 'b::len word\ fixes of_nat :: \nat \ 'a\ and nat_of :: \'a \ nat\ and of_int :: \int \ 'a\ and int_of :: \'a \ int\ and of_integer :: \integer \ 'a\ and integer_of :: \'a \ integer\ assumes word_of_nat_eq: \word_of (of_nat n) = word_of_nat n\ and nat_of_eq_word_of: \nat_of p = unat (word_of p)\ and word_of_int_eq: \word_of (of_int k) = word_of_int k\ and int_of_eq_word_of: \int_of p = uint (word_of p)\ and word_of_integer_eq: \word_of (of_integer l) = word_of_integer l\ and integer_of_eq_word_of: \integer_of p = unsigned (word_of p)\ begin lemma of_word_numeral [code_post]: \of_word (numeral n) = numeral n\ by (simp add: eq_iff_word_of word_of_word) lemma of_word_0 [code_post]: \of_word 0 = 0\ by (simp add: eq_iff_word_of word_of_0 word_of_word) lemma of_word_1 [code_post]: \of_word 1 = 1\ by (simp add: eq_iff_word_of word_of_1 word_of_word) text \Use pretty numerals from integer for pretty printing\ lemma numeral_eq_integer [code_unfold]: \numeral n = of_integer (numeral n)\ - by (simp add: eq_iff_word_of word_of_integer_eq word_of_integer.rep_eq) + by (simp add: eq_iff_word_of word_of_integer_eq) lemma neg_numeral_eq_integer [code_unfold]: \- numeral n = of_integer (- numeral n)\ - by (simp add: eq_iff_word_of word_of_integer_eq word_of_minus word_of_integer.rep_eq) + by (simp add: eq_iff_word_of word_of_integer_eq word_of_minus) end locale word_type_copy_misc = word_type_copy_more opening constraintless bit_operations_syntax + constrains word_of :: \'a::{ring_bit_operations, equal, linorder} \ 'b::len word\ fixes size :: nat and set_bits_aux :: \(nat \ bool) \ nat \ 'a \ 'a\ assumes size_eq_length: \size = LENGTH('b::len)\ and msb_iff_word_of [code]: \msb p \ msb (word_of p)\ and lsb_iff_word_of [code]: \lsb p \ lsb (word_of p)\ and size_eq_word_of: \Nat.size (p :: 'a) = Nat.size (word_of p)\ and word_of_generic_set_bit [code]: \word_of (Generic_set_bit.set_bit p n b) = Generic_set_bit.set_bit (word_of p) n b\ and word_of_set_bits: \word_of (set_bits P) = set_bits P\ and word_of_set_bits_aux: \word_of (set_bits_aux P n p) = Bit_Comprehension.set_bits_aux P n (word_of p)\ begin lemma size_eq [code]: \Nat.size p = size\ for p :: 'a by (simp add: size_eq_length size_eq_word_of word_size) lemma set_bits_aux_code [code]: \set_bits_aux f n w = (if n = 0 then w else let n' = n - 1 in set_bits_aux f n' (push_bit 1 w OR (if f n' then 1 else 0)))\ by (simp add: eq_iff_word_of word_of_set_bits_aux Let_def word_of_mult word_of_or word_of_0 word_of_1 set_bits_aux_rec [of f n]) lemma set_bits_code [code]: \set_bits P = set_bits_aux P size 0\ by (simp add: fun_eq_iff eq_iff_word_of word_of_set_bits word_of_set_bits_aux word_of_0 size_eq_length set_bits_conv_set_bits_aux) lemma of_class_lsb: \OFCLASS('a, lsb_class)\ by standard (simp add: fun_eq_iff lsb_iff_word_of even_iff_word_of lsb_odd) lemma of_class_set_bit: \OFCLASS('a, set_bit_class)\ by standard (simp add: eq_iff_word_of word_of_generic_set_bit bit_eq_word_of word_of_power word_of_0 bit_simps linorder_not_le) lemma of_class_bit_comprehension: \OFCLASS('a, bit_comprehension_class)\ by standard (simp add: eq_iff_word_of word_of_set_bits bit_eq_word_of set_bits_bit_eq) end end