diff --git a/thys/Native_Word/Code_Target_Integer_Bit.thy b/thys/Native_Word/Code_Target_Integer_Bit.thy --- a/thys/Native_Word/Code_Target_Integer_Bit.thy +++ b/thys/Native_Word/Code_Target_Integer_Bit.thy @@ -1,683 +1,680 @@ (* Title: Code_Target_Integer_Bit.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Bit operations for target language integers\ theory Code_Target_Integer_Bit imports "HOL-Library.Word" "Code_Int_Integer_Conversion" "Word_Lib.Most_significant_bit" "Word_Lib.Least_significant_bit" "Word_Lib.Generic_set_bit" "Word_Lib.Bit_Comprehension" begin text \TODO: separate\ lemmas [transfer_rule] = identity_quotient fun_quotient Quotient_integer[folded integer.pcr_cr_eq] lemma undefined_transfer: assumes "Quotient R Abs Rep T" shows "T (Rep undefined) undefined" using assms unfolding Quotient_alt_def by blast bundle undefined_transfer = undefined_transfer[transfer_rule] section \More lemmas about @{typ integer}s\ context includes integer.lifting begin lemma bitval_integer_transfer [transfer_rule]: "(rel_fun (=) pcr_integer) of_bool of_bool" by(auto simp add: of_bool_def integer.pcr_cr_eq cr_integer_def) lemma integer_of_nat_less_0_conv [simp]: "\ integer_of_nat n < 0" by(transfer) simp lemma int_of_integer_pow: "int_of_integer (x ^ n) = int_of_integer x ^ n" by(induct n) simp_all lemma pow_integer_transfer [transfer_rule]: "(rel_fun pcr_integer (rel_fun (=) pcr_integer)) (^) (^)" by(auto 4 3 simp add: integer.pcr_cr_eq cr_integer_def int_of_integer_pow) lemma sub1_lt_0_iff [simp]: "Code_Numeral.sub n num.One < 0 \ False" by(cases n)(simp_all add: Code_Numeral.sub_code) lemma nat_of_integer_numeral [simp]: "nat_of_integer (numeral n) = numeral n" by transfer simp lemma nat_of_integer_sub1_conv_pred_numeral [simp]: "nat_of_integer (Code_Numeral.sub n num.One) = pred_numeral n" by(cases n)(simp_all add: Code_Numeral.sub_code) lemma nat_of_integer_1 [simp]: "nat_of_integer 1 = 1" by transfer simp lemma dup_1 [simp]: "Code_Numeral.dup 1 = 2" by transfer simp section \Bit operations on @{typ integer}\ text \Bit operations on @{typ integer} are the same as on @{typ int}\ lift_definition bin_rest_integer :: "integer \ integer" is \\k . k div 2\ . lift_definition bin_last_integer :: "integer \ bool" is odd . lift_definition Bit_integer :: "integer \ bool \ integer" is \\k b. of_bool b + 2 * k\ . end instantiation integer :: lsb begin context includes integer.lifting begin lift_definition lsb_integer :: "integer \ bool" is lsb . instance by (standard; transfer) (fact lsb_odd) end end instantiation integer :: msb begin context includes integer.lifting begin lift_definition msb_integer :: "integer \ bool" is msb . instance .. end end instantiation integer :: set_bit begin context includes integer.lifting begin lift_definition set_bit_integer :: "integer \ nat \ bool \ integer" is set_bit . instance apply standard apply transfer apply (simp add: bit_simps) done end end -abbreviation (input) wf_set_bits_integer -where "wf_set_bits_integer \ wf_set_bits_int" - section \Target language implementations\ text \ Unfortunately, this is not straightforward, because these API functions have different signatures and preconditions on the parameters: \begin{description} \item[Standard ML] Shifts in IntInf are given as word, but not IntInf. \item[Haskell] In the Data.Bits.Bits type class, shifts and bit indices are given as Int rather than Integer. \end{description} Additional constants take only parameters of type @{typ integer} rather than @{typ nat} and check the preconditions as far as possible (e.g., being non-negative) in a portable way. Manual implementations inside code\_printing perform the remaining range checks and convert these @{typ integer}s into the right type. For normalisation by evaluation, we derive custom code equations, because NBE does not know these code\_printing serialisations and would otherwise loop. \ code_printing code_module Integer_Bit \ (SML) \structure Integer_Bit : sig val test_bit : IntInf.int -> IntInf.int -> bool val set_bit : IntInf.int -> IntInf.int -> bool -> IntInf.int val shiftl : IntInf.int -> IntInf.int -> IntInf.int val shiftr : IntInf.int -> IntInf.int -> IntInf.int end = struct val maxWord = IntInf.pow (2, Word.wordSize); fun test_bit x n = if n < maxWord then IntInf.andb (x, IntInf.<< (1, Word.fromLargeInt (IntInf.toLarge n))) <> 0 else raise (Fail ("Bit index too large: " ^ IntInf.toString n)); fun set_bit x n b = if n < maxWord 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 raise (Fail ("Bit index too large: " ^ IntInf.toString n)); fun shiftl x n = if n < maxWord then IntInf.<< (x, Word.fromLargeInt (IntInf.toLarge n)) else raise (Fail ("Shift operand too large: " ^ IntInf.toString n)); fun shiftr x n = if n < maxWord then IntInf.~>> (x, Word.fromLargeInt (IntInf.toLarge n)) else raise (Fail ("Shift operand too large: " ^ IntInf.toString n)); end; (*struct Integer_Bit*)\ code_reserved SML Integer_Bit code_printing code_module Integer_Bit \ (OCaml) \module Integer_Bit : sig val test_bit : Z.t -> Z.t -> bool val shiftl : Z.t -> Z.t -> Z.t val shiftr : Z.t -> Z.t -> Z.t end = struct (* We do not need an explicit range checks here, because Big_int.int_of_big_int raises Failure if the argument does not fit into an int. *) let test_bit x n = Z.testbit x (Z.to_int n);; let shiftl x n = Z.shift_left x (Z.to_int n);; let shiftr x n = Z.shift_right x (Z.to_int n);; end;; (*struct Integer_Bit*)\ code_reserved OCaml Integer_Bit code_printing code_module Data_Bits \ (Haskell) \ module Data_Bits where { import qualified Data.Bits; {- The ...Bounded functions assume that the Integer argument for the shift or bit index fits into an Int, is non-negative and (for types of fixed bit width) less than bitSize -} infixl 7 .&.; infixl 6 `xor`; infixl 5 .|.; (.&.) :: Data.Bits.Bits a => a -> a -> a; (.&.) = (Data.Bits..&.); xor :: Data.Bits.Bits a => a -> a -> a; xor = Data.Bits.xor; (.|.) :: Data.Bits.Bits a => a -> a -> a; (.|.) = (Data.Bits..|.); complement :: Data.Bits.Bits a => a -> a; complement = Data.Bits.complement; testBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool; testBitUnbounded x b | b <= toInteger (Prelude.maxBound :: Int) = Data.Bits.testBit x (fromInteger b) | otherwise = error ("Bit index too large: " ++ show b) ; testBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool; testBitBounded x b = Data.Bits.testBit x (fromInteger b); setBitUnbounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a; setBitUnbounded x n b | n <= toInteger (Prelude.maxBound :: Int) = if b then Data.Bits.setBit x (fromInteger n) else Data.Bits.clearBit x (fromInteger n) | otherwise = error ("Bit index too large: " ++ show n) ; setBitBounded :: Data.Bits.Bits a => a -> Integer -> Bool -> a; setBitBounded x n True = Data.Bits.setBit x (fromInteger n); setBitBounded x n False = Data.Bits.clearBit x (fromInteger n); shiftlUnbounded :: Data.Bits.Bits a => a -> Integer -> a; shiftlUnbounded x n | n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftL x (fromInteger n) | otherwise = error ("Shift operand too large: " ++ show n) ; shiftlBounded :: Data.Bits.Bits a => a -> Integer -> a; shiftlBounded x n = Data.Bits.shiftL x (fromInteger n); shiftrUnbounded :: Data.Bits.Bits a => a -> Integer -> a; shiftrUnbounded x n | n <= toInteger (Prelude.maxBound :: Int) = Data.Bits.shiftR x (fromInteger n) | otherwise = error ("Shift operand too large: " ++ show n) ; shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Integer -> a; shiftrBounded x n = Data.Bits.shiftR x (fromInteger n); }\ and \ \@{theory HOL.Quickcheck_Narrowing} maps @{typ integer} to Haskell's Prelude.Int type instead of Integer. For compatibility with the Haskell target, we nevertheless provide bounded and unbounded functions.\ (Haskell_Quickcheck) \ module Data_Bits where { import qualified Data.Bits; {- The functions assume that the Int argument for the shift or bit index is non-negative and (for types of fixed bit width) less than bitSize -} infixl 7 .&.; infixl 6 `xor`; infixl 5 .|.; (.&.) :: Data.Bits.Bits a => a -> a -> a; (.&.) = (Data.Bits..&.); xor :: Data.Bits.Bits a => a -> a -> a; xor = Data.Bits.xor; (.|.) :: Data.Bits.Bits a => a -> a -> a; (.|.) = (Data.Bits..|.); complement :: Data.Bits.Bits a => a -> a; complement = Data.Bits.complement; testBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool; testBitUnbounded = Data.Bits.testBit; testBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool; testBitBounded = Data.Bits.testBit; setBitUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a; setBitUnbounded x n True = Data.Bits.setBit x n; setBitUnbounded x n False = Data.Bits.clearBit x n; setBitBounded :: Data.Bits.Bits a => a -> Prelude.Int -> Bool -> a; setBitBounded x n True = Data.Bits.setBit x n; setBitBounded x n False = Data.Bits.clearBit x n; shiftlUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a; shiftlUnbounded = Data.Bits.shiftL; shiftlBounded :: Data.Bits.Bits a => a -> Prelude.Int -> a; shiftlBounded = Data.Bits.shiftL; shiftrUnbounded :: Data.Bits.Bits a => a -> Prelude.Int -> a; shiftrUnbounded = Data.Bits.shiftR; shiftrBounded :: (Ord a, Data.Bits.Bits a) => a -> Prelude.Int -> a; shiftrBounded = Data.Bits.shiftR; }\ code_reserved Haskell Data_Bits code_printing code_module Integer_Bit \ (Scala) \object Integer_Bit { def testBit(x: BigInt, n: BigInt) : Boolean = if (n.isValidInt) x.testBit(n.toInt) else sys.error("Bit index too large: " + n.toString) def setBit(x: BigInt, n: BigInt, b: Boolean) : BigInt = if (n.isValidInt) if (b) x.setBit(n.toInt) else x.clearBit(n.toInt) else sys.error("Bit index too large: " + n.toString) def shiftl(x: BigInt, n: BigInt) : BigInt = if (n.isValidInt) x << n.toInt else sys.error("Shift index too large: " + n.toString) def shiftr(x: BigInt, n: BigInt) : BigInt = if (n.isValidInt) x << n.toInt else sys.error("Shift index too large: " + n.toString) } /* object Integer_Bit */\ code_printing constant "Bit_Operations.and :: integer \ integer \ integer" \ (SML) "IntInf.andb ((_),/ (_))" and (OCaml) "Z.logand" and (Haskell) "((Data'_Bits..&.) :: Integer -> Integer -> Integer)" and (Haskell_Quickcheck) "((Data'_Bits..&.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and (Scala) infixl 3 "&" | constant "Bit_Operations.or :: integer \ integer \ integer" \ (SML) "IntInf.orb ((_),/ (_))" and (OCaml) "Z.logor" and (Haskell) "((Data'_Bits..|.) :: Integer -> Integer -> Integer)" and (Haskell_Quickcheck) "((Data'_Bits..|.) :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and (Scala) infixl 1 "|" | constant "Bit_Operations.xor :: integer \ integer \ integer" \ (SML) "IntInf.xorb ((_),/ (_))" and (OCaml) "Z.logxor" and (Haskell) "(Data'_Bits.xor :: Integer -> Integer -> Integer)" and (Haskell_Quickcheck) "(Data'_Bits.xor :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and (Scala) infixl 2 "^" | constant "Bit_Operations.not :: integer \ integer" \ (SML) "IntInf.notb" and (OCaml) "Z.lognot" and (Haskell) "(Data'_Bits.complement :: Integer -> Integer)" and (Haskell_Quickcheck) "(Data'_Bits.complement :: Prelude.Int -> Prelude.Int)" and (Scala) "_.unary'_~" code_printing constant bin_rest_integer \ (SML) "IntInf.div ((_), 2)" and (OCaml) "Z.shift'_right/ _/ 1" and (Haskell) "(Data'_Bits.shiftrUnbounded _ 1 :: Integer)" and (Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded _ 1 :: Prelude.Int)" and (Scala) "_ >> 1" context includes integer.lifting bit_operations_syntax begin lemma bitNOT_integer_code [code]: fixes i :: integer shows "NOT i = - i - 1" by transfer (simp add: not_int_def) lemma bin_rest_integer_code [code nbe]: "bin_rest_integer i = i div 2" by transfer rule lemma bin_last_integer_code [code]: "bin_last_integer i \ i AND 1 \ 0" by transfer (simp add: and_one_eq odd_iff_mod_2_eq_one) lemma bin_last_integer_nbe [code nbe]: "bin_last_integer i \ i mod 2 \ 0" by transfer (simp add: odd_iff_mod_2_eq_one) lemma bitval_bin_last_integer [code_unfold]: "of_bool (bin_last_integer i) = i AND 1" by transfer (simp add: and_one_eq mod_2_eq_odd) end definition integer_test_bit :: "integer \ integer \ bool" where "integer_test_bit x n = (if n < 0 then undefined x n else bit x (nat_of_integer n))" declare [[code drop: \bit :: integer \ nat \ bool\]] lemma bit_integer_code [code]: "bit x n \ integer_test_bit x (integer_of_nat n)" by (simp add: integer_test_bit_def) lemma integer_test_bit_code [code]: "integer_test_bit x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)" "integer_test_bit 0 0 = False" "integer_test_bit 0 (Code_Numeral.Pos n) = False" "integer_test_bit (Code_Numeral.Pos num.One) 0 = True" "integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) 0 = False" "integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) 0 = True" "integer_test_bit (Code_Numeral.Pos num.One) (Code_Numeral.Pos n') = False" "integer_test_bit (Code_Numeral.Pos (num.Bit0 n)) (Code_Numeral.Pos n') = integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)" "integer_test_bit (Code_Numeral.Pos (num.Bit1 n)) (Code_Numeral.Pos n') = integer_test_bit (Code_Numeral.Pos n) (Code_Numeral.sub n' num.One)" "integer_test_bit (Code_Numeral.Neg num.One) 0 = True" "integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) 0 = False" "integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) 0 = True" "integer_test_bit (Code_Numeral.Neg num.One) (Code_Numeral.Pos n') = True" "integer_test_bit (Code_Numeral.Neg (num.Bit0 n)) (Code_Numeral.Pos n') = integer_test_bit (Code_Numeral.Neg n) (Code_Numeral.sub n' num.One)" "integer_test_bit (Code_Numeral.Neg (num.Bit1 n)) (Code_Numeral.Pos n') = integer_test_bit (Code_Numeral.Neg (n + num.One)) (Code_Numeral.sub n' num.One)" by (simp_all add: integer_test_bit_def bit_integer_def bit_0 flip: bit_not_int_iff') code_printing constant integer_test_bit \ (SML) "Integer'_Bit.test'_bit" and (OCaml) "Integer'_Bit.test'_bit" and (Haskell) "(Data'_Bits.testBitUnbounded :: Integer -> Integer -> Bool)" and (Haskell_Quickcheck) "(Data'_Bits.testBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool)" and (Scala) "Integer'_Bit.testBit" context includes integer.lifting bit_operations_syntax begin lemma lsb_integer_code [code]: fixes x :: integer shows "lsb x = bit x 0" by transfer(simp add: lsb_int_def) definition integer_set_bit :: "integer \ integer \ bool \ integer" where [code del]: "integer_set_bit x n b = (if n < 0 then undefined x n b else set_bit x (nat_of_integer n) b)" lemma set_bit_integer_code [code]: "set_bit x i b = integer_set_bit x (integer_of_nat i) b" by(simp add: integer_set_bit_def) lemma set_bit_integer_conv_masks: fixes x :: integer shows "set_bit x i b = (if b then x OR (push_bit i 1) else x AND NOT (push_bit i 1))" by (transfer; rule bit_eqI) (simp add: bit_simps) end code_printing constant integer_set_bit \ (SML) "Integer'_Bit.set'_bit" and (Haskell) "(Data'_Bits.setBitUnbounded :: Integer -> Integer -> Bool -> Integer)" and (Haskell_Quickcheck) "(Data'_Bits.setBitUnbounded :: Prelude.Int -> Prelude.Int -> Bool -> Prelude.Int)" and (Scala) "Integer'_Bit.setBit" text \ OCaml.Big\_int does not have a method for changing an individual bit, so we emulate that with masks. We prefer an Isabelle implementation, because this then takes care of the signs for AND and OR. \ context includes bit_operations_syntax begin lemma integer_set_bit_code [code]: "integer_set_bit x n b = (if n < 0 then undefined x n b else if b then x OR (push_bit (nat_of_integer n) 1) else x AND NOT (push_bit (nat_of_integer n) 1))" by (auto simp add: integer_set_bit_def not_less set_bit_eq set_bit_def unset_bit_def) end definition integer_shiftl :: "integer \ integer \ integer" where [code del]: "integer_shiftl x n = (if n < 0 then undefined x n else push_bit (nat_of_integer n) x)" declare [[code drop: \push_bit :: nat \ integer \ integer\]] lemma shiftl_integer_code [code]: fixes x :: integer shows "push_bit n x = integer_shiftl x (integer_of_nat n)" by(auto simp add: integer_shiftl_def) context includes integer.lifting begin lemma shiftl_integer_conv_mult_pow2: fixes x :: integer shows "push_bit n x = x * 2 ^ n" by (fact push_bit_eq_mult) lemma integer_shiftl_code [code]: "integer_shiftl x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)" "integer_shiftl x 0 = x" "integer_shiftl x (Code_Numeral.Pos n) = integer_shiftl (Code_Numeral.dup x) (Code_Numeral.sub n num.One)" "integer_shiftl 0 (Code_Numeral.Pos n) = 0" apply (simp_all add: integer_shiftl_def numeral_eq_Suc) apply transfer apply (simp add: ac_simps) done end code_printing constant integer_shiftl \ (SML) "Integer'_Bit.shiftl" and (OCaml) "Integer'_Bit.shiftl" and (Haskell) "(Data'_Bits.shiftlUnbounded :: Integer -> Integer -> Integer)" and (Haskell_Quickcheck) "(Data'_Bits.shiftlUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and (Scala) "Integer'_Bit.shiftl" definition integer_shiftr :: "integer \ integer \ integer" where [code del]: "integer_shiftr x n = (if n < 0 then undefined x n else drop_bit (nat_of_integer n) x)" declare [[code drop: \drop_bit :: nat \ integer \ integer\]] lemma shiftr_integer_conv_div_pow2: includes integer.lifting fixes x :: integer shows "drop_bit n x = x div 2 ^ n" by (fact drop_bit_eq_div) lemma shiftr_integer_code [code]: fixes x :: integer shows "drop_bit n x = integer_shiftr x (integer_of_nat n)" by(auto simp add: integer_shiftr_def) code_printing constant integer_shiftr \ (SML) "Integer'_Bit.shiftr" and (OCaml) "Integer'_Bit.shiftr" and (Haskell) "(Data'_Bits.shiftrUnbounded :: Integer -> Integer -> Integer)" and (Haskell_Quickcheck) "(Data'_Bits.shiftrUnbounded :: Prelude.Int -> Prelude.Int -> Prelude.Int)" and (Scala) "Integer'_Bit.shiftr" lemma integer_shiftr_code [code]: includes integer.lifting shows "integer_shiftr x (Code_Numeral.Neg n) = undefined x (Code_Numeral.Neg n)" "integer_shiftr x 0 = x" "integer_shiftr 0 (Code_Numeral.Pos n) = 0" "integer_shiftr (Code_Numeral.Pos num.One) (Code_Numeral.Pos n) = 0" "integer_shiftr (Code_Numeral.Pos (num.Bit0 n')) (Code_Numeral.Pos n) = integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)" "integer_shiftr (Code_Numeral.Pos (num.Bit1 n')) (Code_Numeral.Pos n) = integer_shiftr (Code_Numeral.Pos n') (Code_Numeral.sub n num.One)" "integer_shiftr (Code_Numeral.Neg num.One) (Code_Numeral.Pos n) = -1" "integer_shiftr (Code_Numeral.Neg (num.Bit0 n')) (Code_Numeral.Pos n) = integer_shiftr (Code_Numeral.Neg n') (Code_Numeral.sub n num.One)" "integer_shiftr (Code_Numeral.Neg (num.Bit1 n')) (Code_Numeral.Pos n) = integer_shiftr (Code_Numeral.Neg (Num.inc n')) (Code_Numeral.sub n num.One)" apply (simp_all add: integer_shiftr_def numeral_eq_Suc drop_bit_Suc) apply transfer apply simp apply transfer apply simp apply transfer apply (simp add: add_One) done context includes integer.lifting begin lemma Bit_integer_code [code]: "Bit_integer i False = push_bit 1 i" "Bit_integer i True = push_bit 1 i + 1" by (transfer; simp)+ lemma msb_integer_code [code]: "msb (x :: integer) \ x < 0" by transfer (simp add: msb_int_def) end context includes integer.lifting natural.lifting bit_operations_syntax begin lemma bitAND_integer_unfold [code]: "x AND y = (if x = 0 then 0 else if x = - 1 then y else Bit_integer (bin_rest_integer x AND bin_rest_integer y) (bin_last_integer x \ bin_last_integer y))" by transfer (auto simp add: algebra_simps and_int_rec [of _ \_ * 2\] and_int_rec [of \_ * 2\] and_int_rec [of \1 + _ * 2\] elim!: evenE oddE) lemma bitOR_integer_unfold [code]: "x OR y = (if x = 0 then y else if x = - 1 then - 1 else Bit_integer (bin_rest_integer x OR bin_rest_integer y) (bin_last_integer x \ bin_last_integer y))" by transfer (auto simp add: algebra_simps or_int_rec [of _ \_ * 2\] or_int_rec [of _ \1 + _ * 2\] or_int_rec [of \1 + _ * 2\] elim!: evenE oddE) lemma bitXOR_integer_unfold [code]: "x XOR y = (if x = 0 then y else if x = - 1 then NOT y else Bit_integer (bin_rest_integer x XOR bin_rest_integer y) (\ bin_last_integer x \ bin_last_integer y))" by transfer (auto simp add: algebra_simps xor_int_rec [of _ \_ * 2\] xor_int_rec [of \_ * 2\] xor_int_rec [of \1 + _ * 2\] elim!: evenE oddE) end section \Test code generator setup\ context includes bit_operations_syntax begin definition bit_integer_test :: "bool" where "bit_integer_test = (([ -1 AND 3, 1 AND -3, 3 AND 5, -3 AND (- 5) , -3 OR 1, 1 OR -3, 3 OR 5, -3 OR (- 5) , NOT 1, NOT (- 3) , -1 XOR 3, 1 XOR (- 3), 3 XOR 5, -5 XOR (- 3) , set_bit 5 4 True, set_bit (- 5) 2 True, set_bit 5 0 False, set_bit (- 5) 1 False , push_bit 2 1, push_bit 3 (- 1) , drop_bit 3 100, drop_bit 3 (- 100)] :: integer list) = [ 3, 1, 1, -7 , -3, -3, 7, -1 , -2, 2 , -4, -4, 6, 6 , 21, -1, 4, -7 , 4, -8 , 12, -13] \ [ bit (5 :: integer) 4, bit (5 :: integer) 2, bit (-5 :: integer) 4, bit (-5 :: integer) 2 , lsb (5 :: integer), lsb (4 :: integer), lsb (-1 :: integer), lsb (-2 :: integer), msb (5 :: integer), msb (0 :: integer), msb (-1 :: integer), msb (-2 :: integer)] = [ False, True, True, False, True, False, True, False, False, False, True, True])" export_code bit_integer_test checking SML Haskell? Haskell_Quickcheck? OCaml? Scala notepad begin have bit_integer_test by eval have bit_integer_test by normalization have bit_integer_test by code_simp end ML_val \val true = @{code bit_integer_test}\ lemma "x AND y = x OR (y :: integer)" quickcheck[random, expect=counterexample] quickcheck[exhaustive, expect=counterexample] oops lemma "(x :: integer) AND x = x OR x" quickcheck[narrowing, expect=no_counterexample] oops lemma "(f :: integer \ unit) = g" quickcheck[narrowing, size=3, expect=no_counterexample] by(simp add: fun_eq_iff) end hide_const bit_integer_test hide_fact bit_integer_test_def end diff --git a/thys/Word_Lib/Bit_Comprehension.thy b/thys/Word_Lib/Bit_Comprehension.thy --- a/thys/Word_Lib/Bit_Comprehension.thy +++ b/thys/Word_Lib/Bit_Comprehension.thy @@ -1,299 +1,88 @@ (* * Copyright Brian Huffman, PSU; Jeremy Dawson and Gerwin Klein, NICTA * * SPDX-License-Identifier: BSD-2-Clause *) section \Comprehension syntax for bit expressions\ theory Bit_Comprehension imports "HOL-Library.Word" begin class bit_comprehension = ring_bit_operations + fixes set_bits :: \(nat \ bool) \ 'a\ (binder \BITS \ 10) assumes set_bits_bit_eq: \set_bits (bit a) = a\ begin lemma set_bits_False_eq [simp]: \(BITS _. False) = 0\ using set_bits_bit_eq [of 0] by (simp add: bot_fun_def) end -instantiation int :: bit_comprehension -begin - -definition - \set_bits f = ( - if \n. \m\n. f m = f n then - let n = LEAST n. \m\n. f m = f n - in signed_take_bit n (horner_sum of_bool 2 (map f [0.. - -instance proof - fix k :: int - from int_bit_bound [of k] - obtain n where *: \\m. n \ m \ bit k m \ bit k n\ - and **: \n > 0 \ bit k (n - 1) \ bit k n\ - by blast - then have ***: \\n. \n'\n. bit k n' \ bit k n\ - by meson - have l: \(LEAST q. \m\q. bit k m \ bit k q) = n\ - apply (rule Least_equality) - using * apply blast - apply (metis "**" One_nat_def Suc_pred le_cases le0 neq0_conv not_less_eq_eq) - done - show \set_bits (bit k) = k\ - apply (simp only: *** set_bits_int_def horner_sum_bit_eq_take_bit l) - apply simp - apply (rule bit_eqI) - apply (simp add: bit_signed_take_bit_iff min_def) - apply (auto simp add: not_le bit_take_bit_iff dest: *) - done -qed - -end - -lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)" - by (simp add: set_bits_int_def) - -lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)" - by (simp add: set_bits_int_def) - -lemma set_bits_code [code]: - "set_bits = Code.abort (STR ''set_bits is unsupported on type int'') (\_. set_bits :: _ \ int)" - by simp - instantiation word :: (len) bit_comprehension begin definition word_set_bits_def: \(BITS n. P n) = (horner_sum of_bool 2 (map P [0.. instance by standard (simp add: word_set_bits_def horner_sum_bit_eq_take_bit) end lemma bit_set_bits_word_iff [bit_simps]: \bit (set_bits P :: 'a::len word) n \ n < LENGTH('a) \ P n\ by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff) lemma word_of_int_conv_set_bits: "word_of_int i = (BITS n. bit i n)" by (rule bit_eqI) (auto simp add: bit_simps) lemma set_bits_K_False [simp]: \set_bits (\_. False) = (0 :: 'a :: len word)\ by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff) -lemma set_bits_int_unfold': - \set_bits f = - (if \n. \n'\n. \ f n' then - let n = LEAST n. \n'\n. \ f n' - in horner_sum of_bool 2 (map f [0..n. \n'\n. f n' then - let n = LEAST n. \n'\n. f n' - in signed_take_bit n (horner_sum of_bool 2 (map f [0.. -proof (cases \\n. \m\n. f m \ f n\) - case True - then obtain q where q: \\m\q. f m \ f q\ - by blast - define n where \n = (LEAST n. \m\n. f m \ f n)\ - have \\m\n. f m \ f n\ - unfolding n_def - using q by (rule LeastI [of _ q]) - then have n: \\m. n \ m \ f m \ f n\ - by blast - from n_def have n_eq: \(LEAST q. \m\q. f m \ f n) = n\ - by (smt (verit, best) Least_le \\m\n. f m = f n\ dual_order.antisym wellorder_Least_lemma(1)) - show ?thesis - proof (cases \f n\) - case False - with n have *: \\n. \n'\n. \ f n'\ - by blast - have **: \(LEAST n. \n'\n. \ f n') = n\ - using False n_eq by simp - from * False show ?thesis - apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc) - apply (auto simp add: take_bit_horner_sum_bit_eq - bit_horner_sum_bit_iff take_map - signed_take_bit_def set_bits_int_def - horner_sum_bit_eq_take_bit simp del: upt.upt_Suc) - done - next - case True - with n have *: \\n. \n'\n. f n'\ - by blast - have ***: \\ (\n. \n'\n. \ f n')\ - apply (rule ccontr) - using * nat_le_linear by auto - have **: \(LEAST n. \n'\n. f n') = n\ - using True n_eq by simp - from * *** True show ?thesis - apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc) - apply (auto simp add: take_bit_horner_sum_bit_eq - bit_horner_sum_bit_iff take_map - signed_take_bit_def set_bits_int_def - horner_sum_bit_eq_take_bit nth_append simp del: upt.upt_Suc) - done - qed -next - case False - then show ?thesis - by (auto simp add: set_bits_int_def) -qed - lemma word_test_bit_set_bits: "bit (BITS n. f n :: 'a :: len word) n \ n < LENGTH('a) \ f n" by (fact bit_set_bits_word_iff) context includes bit_operations_syntax fixes f :: \nat \ bool\ begin definition set_bits_aux :: \nat \ 'a word \ 'a::len word\ where \set_bits_aux n w = push_bit n w OR take_bit n (set_bits f)\ lemma bit_set_bit_aux [bit_simps]: \bit (set_bits_aux n w) m \ m < LENGTH('a) \ (if m < n then f m else bit w (m - n))\ for w :: \'a::len word\ by (auto simp add: bit_simps set_bits_aux_def) corollary set_bits_conv_set_bits_aux: \set_bits f = (set_bits_aux LENGTH('a) 0 :: 'a :: len word)\ by (rule bit_word_eqI) (simp add: bit_simps) lemma set_bits_aux_0 [simp]: \set_bits_aux 0 w = w\ by (simp add: set_bits_aux_def) lemma set_bits_aux_Suc [simp]: \set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))\ by (rule bit_word_eqI) (auto simp add: bit_simps le_less_Suc_eq mult.commute [of _ 2]) lemma set_bits_aux_simps [code]: \set_bits_aux 0 w = w\ \set_bits_aux (Suc n) w = set_bits_aux n (push_bit 1 w OR (if f n then 1 else 0))\ by simp_all lemma set_bits_aux_rec: \set_bits_aux n w = (if n = 0 then w else let n' = n - 1 in set_bits_aux n' (push_bit 1 w OR (if f n' then 1 else 0)))\ by (cases n) simp_all end -inductive wf_set_bits_int :: "(nat \ bool) \ bool" - for f :: "nat \ bool" -where - zeros: "\n' \ n. \ f n' \ wf_set_bits_int f" -| ones: "\n' \ n. f n' \ wf_set_bits_int f" - -lemma wf_set_bits_int_simps: "wf_set_bits_int f \ (\n. (\n'\n. \ f n') \ (\n'\n. f n'))" -by(auto simp add: wf_set_bits_int.simps) - -lemma wf_set_bits_int_const [simp]: "wf_set_bits_int (\_. b)" -by(cases b)(auto intro: wf_set_bits_int.intros) - -lemma wf_set_bits_int_fun_upd [simp]: - "wf_set_bits_int (f(n := b)) \ wf_set_bits_int f" (is "?lhs \ ?rhs") -proof - assume ?lhs - then obtain n' - where "(\n''\n'. \ (f(n := b)) n'') \ (\n''\n'. (f(n := b)) n'')" - by(auto simp add: wf_set_bits_int_simps) - hence "(\n''\max (Suc n) n'. \ f n'') \ (\n''\max (Suc n) n'. f n'')" by auto - thus ?rhs by(auto simp only: wf_set_bits_int_simps) -next - assume ?rhs - then obtain n' where "(\n''\n'. \ f n'') \ (\n''\n'. f n'')" (is "?wf f n'") - by(auto simp add: wf_set_bits_int_simps) - hence "?wf (f(n := b)) (max (Suc n) n')" by auto - thus ?lhs by(auto simp only: wf_set_bits_int_simps) -qed - -lemma wf_set_bits_int_Suc [simp]: - "wf_set_bits_int (\n. f (Suc n)) \ wf_set_bits_int f" (is "?lhs \ ?rhs") -by(auto simp add: wf_set_bits_int_simps intro: le_SucI dest: Suc_le_D) - -context - fixes f - assumes wff: "wf_set_bits_int f" -begin - -lemma int_set_bits_unfold_BIT: - "set_bits f = of_bool (f 0) + (2 :: int) * set_bits (f \ Suc)" -using wff proof cases - case (zeros n) - show ?thesis - proof(cases "\n. \ f n") - case True - hence "f = (\_. False)" by auto - thus ?thesis using True by(simp add: o_def) - next - case False - then obtain n' where "f n'" by blast - with zeros have "(LEAST n. \n'\n. \ f n') = Suc (LEAST n. \n'\Suc n. \ f n')" - by(auto intro: Least_Suc) - also have "(\n. \n'\Suc n. \ f n') = (\n. \n'\n. \ f (Suc n'))" by(auto dest: Suc_le_D) - also from zeros have "\n'\n. \ f (Suc n')" by auto - ultimately show ?thesis using zeros - apply (simp (no_asm_simp) add: set_bits_int_unfold' exI - del: upt.upt_Suc flip: map_map split del: if_split) - apply (simp only: map_Suc_upt upt_conv_Cons) - apply simp - done - qed -next - case (ones n) - show ?thesis - proof(cases "\n. f n") - case True - hence "f = (\_. True)" by auto - thus ?thesis using True by(simp add: o_def) - next - case False - then obtain n' where "\ f n'" by blast - with ones have "(LEAST n. \n'\n. f n') = Suc (LEAST n. \n'\Suc n. f n')" - by(auto intro: Least_Suc) - also have "(\n. \n'\Suc n. f n') = (\n. \n'\n. f (Suc n'))" by(auto dest: Suc_le_D) - also from ones have "\n'\n. f (Suc n')" by auto - moreover from ones have "(\n. \n'\n. \ f n') = False" - by(auto intro!: exI[where x="max n m" for n m] simp add: max_def split: if_split_asm) - moreover hence "(\n. \n'\n. \ f (Suc n')) = False" - by(auto elim: allE[where x="Suc n" for n] dest: Suc_le_D) - ultimately show ?thesis using ones - apply (simp (no_asm_simp) add: set_bits_int_unfold' exI split del: if_split) - apply (auto simp add: Let_def hd_map map_tl[symmetric] map_map[symmetric] map_Suc_upt upt_conv_Cons signed_take_bit_Suc - not_le simp del: map_map) - done - qed -qed - -lemma bin_last_set_bits [simp]: - "odd (set_bits f :: int) = f 0" - by (subst int_set_bits_unfold_BIT) simp_all - -lemma bin_rest_set_bits [simp]: - "set_bits f div (2 :: int) = set_bits (f \ Suc)" - by (subst int_set_bits_unfold_BIT) simp_all - -lemma bin_nth_set_bits [simp]: - "bit (set_bits f :: int) m \ f m" -using wff proof (induction m arbitrary: f) - case 0 - then show ?case - by (simp add: Bit_Comprehension.bin_last_set_bits bit_0) -next - case Suc - from Suc.IH [of "f \ Suc"] Suc.prems show ?case - by (simp add: Bit_Comprehension.bin_rest_set_bits comp_def bit_Suc) -qed - end - -end diff --git a/thys/Word_Lib/Bit_Comprehension_Int.thy b/thys/Word_Lib/Bit_Comprehension_Int.thy new file mode 100644 --- /dev/null +++ b/thys/Word_Lib/Bit_Comprehension_Int.thy @@ -0,0 +1,225 @@ +(* + * Copyright Brian Huffman, PSU; Jeremy Dawson and Gerwin Klein, NICTA + * + * SPDX-License-Identifier: BSD-2-Clause + *) + +section \Comprehension syntax for \int\\ + +theory Bit_Comprehension_Int + imports + Bit_Comprehension +begin + +instantiation int :: bit_comprehension +begin + +definition + \set_bits f = ( + if \n. \m\n. f m = f n then + let n = LEAST n. \m\n. f m = f n + in signed_take_bit n (horner_sum of_bool 2 (map f [0.. + +instance proof + fix k :: int + from int_bit_bound [of k] + obtain n where *: \\m. n \ m \ bit k m \ bit k n\ + and **: \n > 0 \ bit k (n - 1) \ bit k n\ + by blast + then have ***: \\n. \n'\n. bit k n' \ bit k n\ + by meson + have l: \(LEAST q. \m\q. bit k m \ bit k q) = n\ + apply (rule Least_equality) + using * apply blast + apply (metis "**" One_nat_def Suc_pred le_cases le0 neq0_conv not_less_eq_eq) + done + show \set_bits (bit k) = k\ + apply (simp only: *** set_bits_int_def horner_sum_bit_eq_take_bit l) + apply simp + apply (rule bit_eqI) + apply (simp add: bit_signed_take_bit_iff min_def) + apply (auto simp add: not_le bit_take_bit_iff dest: *) + done +qed + +end + +lemma int_set_bits_K_False [simp]: "(BITS _. False) = (0 :: int)" + by (simp add: set_bits_int_def) + +lemma int_set_bits_K_True [simp]: "(BITS _. True) = (-1 :: int)" + by (simp add: set_bits_int_def) + +lemma set_bits_code [code]: + "set_bits = Code.abort (STR ''set_bits is unsupported on type int'') (\_. set_bits :: _ \ int)" + by simp + +lemma set_bits_int_unfold': + \set_bits f = + (if \n. \n'\n. \ f n' then + let n = LEAST n. \n'\n. \ f n' + in horner_sum of_bool 2 (map f [0..n. \n'\n. f n' then + let n = LEAST n. \n'\n. f n' + in signed_take_bit n (horner_sum of_bool 2 (map f [0.. +proof (cases \\n. \m\n. f m \ f n\) + case True + then obtain q where q: \\m\q. f m \ f q\ + by blast + define n where \n = (LEAST n. \m\n. f m \ f n)\ + have \\m\n. f m \ f n\ + unfolding n_def + using q by (rule LeastI [of _ q]) + then have n: \\m. n \ m \ f m \ f n\ + by blast + from n_def have n_eq: \(LEAST q. \m\q. f m \ f n) = n\ + by (smt (verit, best) Least_le \\m\n. f m = f n\ dual_order.antisym wellorder_Least_lemma(1)) + show ?thesis + proof (cases \f n\) + case False + with n have *: \\n. \n'\n. \ f n'\ + by blast + have **: \(LEAST n. \n'\n. \ f n') = n\ + using False n_eq by simp + from * False show ?thesis + apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc) + apply (auto simp add: take_bit_horner_sum_bit_eq + bit_horner_sum_bit_iff take_map + signed_take_bit_def set_bits_int_def + horner_sum_bit_eq_take_bit simp del: upt.upt_Suc) + done + next + case True + with n have *: \\n. \n'\n. f n'\ + by blast + have ***: \\ (\n. \n'\n. \ f n')\ + apply (rule ccontr) + using * nat_le_linear by auto + have **: \(LEAST n. \n'\n. f n') = n\ + using True n_eq by simp + from * *** True show ?thesis + apply (simp add: set_bits_int_def n_def [symmetric] ** del: upt.upt_Suc) + apply (auto simp add: take_bit_horner_sum_bit_eq + bit_horner_sum_bit_iff take_map + signed_take_bit_def set_bits_int_def + horner_sum_bit_eq_take_bit nth_append simp del: upt.upt_Suc) + done + qed +next + case False + then show ?thesis + by (auto simp add: set_bits_int_def) +qed + +inductive wf_set_bits_int :: "(nat \ bool) \ bool" + for f :: "nat \ bool" +where + zeros: "\n' \ n. \ f n' \ wf_set_bits_int f" +| ones: "\n' \ n. f n' \ wf_set_bits_int f" + +lemma wf_set_bits_int_simps: "wf_set_bits_int f \ (\n. (\n'\n. \ f n') \ (\n'\n. f n'))" +by(auto simp add: wf_set_bits_int.simps) + +lemma wf_set_bits_int_const [simp]: "wf_set_bits_int (\_. b)" +by(cases b)(auto intro: wf_set_bits_int.intros) + +lemma wf_set_bits_int_fun_upd [simp]: + "wf_set_bits_int (f(n := b)) \ wf_set_bits_int f" (is "?lhs \ ?rhs") +proof + assume ?lhs + then obtain n' + where "(\n''\n'. \ (f(n := b)) n'') \ (\n''\n'. (f(n := b)) n'')" + by(auto simp add: wf_set_bits_int_simps) + hence "(\n''\max (Suc n) n'. \ f n'') \ (\n''\max (Suc n) n'. f n'')" by auto + thus ?rhs by(auto simp only: wf_set_bits_int_simps) +next + assume ?rhs + then obtain n' where "(\n''\n'. \ f n'') \ (\n''\n'. f n'')" (is "?wf f n'") + by(auto simp add: wf_set_bits_int_simps) + hence "?wf (f(n := b)) (max (Suc n) n')" by auto + thus ?lhs by(auto simp only: wf_set_bits_int_simps) +qed + +lemma wf_set_bits_int_Suc [simp]: + "wf_set_bits_int (\n. f (Suc n)) \ wf_set_bits_int f" (is "?lhs \ ?rhs") +by(auto simp add: wf_set_bits_int_simps intro: le_SucI dest: Suc_le_D) + +context + fixes f + assumes wff: "wf_set_bits_int f" +begin + +lemma int_set_bits_unfold_BIT: + "set_bits f = of_bool (f 0) + (2 :: int) * set_bits (f \ Suc)" +using wff proof cases + case (zeros n) + show ?thesis + proof(cases "\n. \ f n") + case True + hence "f = (\_. False)" by auto + thus ?thesis using True by(simp add: o_def) + next + case False + then obtain n' where "f n'" by blast + with zeros have "(LEAST n. \n'\n. \ f n') = Suc (LEAST n. \n'\Suc n. \ f n')" + by(auto intro: Least_Suc) + also have "(\n. \n'\Suc n. \ f n') = (\n. \n'\n. \ f (Suc n'))" by(auto dest: Suc_le_D) + also from zeros have "\n'\n. \ f (Suc n')" by auto + ultimately show ?thesis using zeros + apply (simp (no_asm_simp) add: set_bits_int_unfold' exI + del: upt.upt_Suc flip: map_map split del: if_split) + apply (simp only: map_Suc_upt upt_conv_Cons) + apply simp + done + qed +next + case (ones n) + show ?thesis + proof(cases "\n. f n") + case True + hence "f = (\_. True)" by auto + thus ?thesis using True by(simp add: o_def) + next + case False + then obtain n' where "\ f n'" by blast + with ones have "(LEAST n. \n'\n. f n') = Suc (LEAST n. \n'\Suc n. f n')" + by(auto intro: Least_Suc) + also have "(\n. \n'\Suc n. f n') = (\n. \n'\n. f (Suc n'))" by(auto dest: Suc_le_D) + also from ones have "\n'\n. f (Suc n')" by auto + moreover from ones have "(\n. \n'\n. \ f n') = False" + by(auto intro!: exI[where x="max n m" for n m] simp add: max_def split: if_split_asm) + moreover hence "(\n. \n'\n. \ f (Suc n')) = False" + by(auto elim: allE[where x="Suc n" for n] dest: Suc_le_D) + ultimately show ?thesis using ones + apply (simp (no_asm_simp) add: set_bits_int_unfold' exI split del: if_split) + apply (auto simp add: Let_def hd_map map_tl[symmetric] map_map[symmetric] map_Suc_upt upt_conv_Cons signed_take_bit_Suc + not_le simp del: map_map) + done + qed +qed + +lemma bin_last_set_bits [simp]: + "odd (set_bits f :: int) = f 0" + by (subst int_set_bits_unfold_BIT) simp_all + +lemma bin_rest_set_bits [simp]: + "set_bits f div (2 :: int) = set_bits (f \ Suc)" + by (subst int_set_bits_unfold_BIT) simp_all + +lemma bin_nth_set_bits [simp]: + "bit (set_bits f :: int) m \ f m" +using wff proof (induction m arbitrary: f) + case 0 + then show ?case + by (simp add: Bit_Comprehension_Int.bin_last_set_bits bit_0) +next + case Suc + from Suc.IH [of "f \ Suc"] Suc.prems show ?case + by (simp add: Bit_Comprehension_Int.bin_rest_set_bits comp_def bit_Suc) +qed + +end + +end diff --git a/thys/Word_Lib/Guide.thy b/thys/Word_Lib/Guide.thy --- a/thys/Word_Lib/Guide.thy +++ b/thys/Word_Lib/Guide.thy @@ -1,424 +1,432 @@ (* * Copyright Florian Haftmann * * SPDX-License-Identifier: BSD-2-Clause *) (*<*) theory Guide imports Word_Lib_Sumo Machine_Word_32 Machine_Word_64 begin context semiring_bit_operations begin lemma bit_eq_iff: \a = b \ (\n. 2 ^ n \ 0 \ bit a n \ bit b n)\ using bit_eq_iff [of a b] by (simp add: possible_bit_def) end notation (output) Generic_set_bit.set_bit (\Generic'_set'_bit.set'_bit\) hide_const (open) Generic_set_bit.set_bit no_notation bit (infixl \!!\ 100) (*>*) section \A short overview over bit operations and word types\ subsection \Key principles\ text \ When formalizing bit operations, it is tempting to represent bit values as explicit lists over a binary type. This however is a bad idea, mainly due to the inherent ambiguities in representation concerning repeating leading bits. Hence this approach avoids such explicit lists altogether following an algebraic path: \<^item> Bit values are represented by numeric types: idealized unbounded bit values can be represented by type \<^typ>\int\, bounded bit values by quotient types over \<^typ>\int\, aka \<^typ>\'a word\. \<^item> (A special case are idealized unbounded bit values ending in @{term [source] 0} which can be represented by type \<^typ>\nat\ but only support a restricted set of operations). The fundamental principles are developed in theory \<^theory>\HOL.Bit_Operations\ (which is part of \<^theory>\Main\): \<^item> Multiplication by \<^term>\2 :: int\ is a bit shift to the left and \<^item> Division by \<^term>\2 :: int\ is a bit shift to the right. \<^item> Concerning bounded bit values, iterated shifts to the left may result in eliminating all bits by shifting them all beyond the boundary. The property \<^prop>\(2 :: int) ^ n \ 0\ represents that \<^term>\n\ is \<^emph>\not\ beyond that boundary. \<^item> The projection on a single bit is then @{thm [mode=iff] bit_iff_odd [where ?'a = int, no_vars]}. \<^item> This leads to the most fundamental properties of bit values: \<^item> Equality rule: @{thm [display, mode=iff] bit_eq_iff [where ?'a = int, no_vars]} \<^item> Induction rule: @{thm [display, mode=iff] bits_induct [where ?'a = int, no_vars]} \<^item> Characteristic properties @{prop [source] \bit (f x) n \ P x n\} are available in fact collection \<^text>\bit_simps\. On top of this, the following generic operations are provided: \<^item> Singleton \<^term>\n\th bit: \<^term>\(2 :: int) ^ n\ \<^item> Bit mask upto bit \<^term>\n\: @{thm mask_eq_exp_minus_1 [where ?'a = int, no_vars]} \<^item> Left shift: @{thm push_bit_eq_mult [where ?'a = int, no_vars]} \<^item> Right shift: @{thm drop_bit_eq_div [where ?'a = int, no_vars]} \<^item> Truncation: @{thm take_bit_eq_mod [where ?'a = int, no_vars]} \<^item> Bitwise negation: @{thm [mode=iff] bit_not_iff_eq [where ?'a = int, no_vars]} \<^item> Bitwise conjunction: @{thm [mode=iff] bit_and_iff [where ?'a = int, no_vars]} \<^item> Bitwise disjunction: @{thm [mode=iff] bit_or_iff [where ?'a = int, no_vars]} \<^item> Bitwise exclusive disjunction: @{thm [mode=iff] bit_xor_iff [where ?'a = int, no_vars]} \<^item> Setting a single bit: @{thm set_bit_def [where ?'a = int, no_vars]} \<^item> Unsetting a single bit: @{thm unset_bit_def [where ?'a = int, no_vars]} \<^item> Flipping a single bit: @{thm flip_bit_def [where ?'a = int, no_vars]} \<^item> Signed truncation, or modulus centered around \<^term>\0::int\: @{thm [display] signed_take_bit_def [where ?'a = int, no_vars]} \<^item> (Bounded) conversion from and to a list of bits: @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} Bit concatenation on \<^typ>\int\ as given by @{thm [display] concat_bit_def [no_vars]} appears quite technical but is the logical foundation for the quite natural bit concatenation on \<^typ>\'a word\ (see below). \ subsection \Core word theory\ text \ Proper word types are introduced in theory \<^theory>\HOL-Library.Word\, with the following specific operations: \<^item> Standard arithmetic: @{term \(+) :: 'a::len word \ 'a word \ 'a word\}, @{term \uminus :: 'a::len word \ 'a word\}, @{term \(-) :: 'a::len word \ 'a word \ 'a word\}, @{term \(*) :: 'a::len word \ 'a word \ 'a word\}, @{term \0 :: 'a::len word\}, @{term \1 :: 'a::len word\}, numerals etc. \<^item> Standard bit operations: see above. \<^item> Conversion with unsigned interpretation of words: \<^item> @{term [source] \unsigned :: 'a::len word \ 'b::semiring_1\} \<^item> Important special cases as abbreviations: \<^item> @{term [source] \unat :: 'a::len word \ nat\} \<^item> @{term [source] \uint :: 'a::len word \ int\} \<^item> @{term [source] \ucast :: 'a::len word \ 'b::len word\} \<^item> Conversion with signed interpretation of words: \<^item> @{term [source] \signed :: 'a::len word \ 'b::ring_1\} \<^item> Important special cases as abbreviations: \<^item> @{term [source] \sint :: 'a::len word \ int\} \<^item> @{term [source] \scast :: 'a::len word \ 'b::len word\} \<^item> Operations with unsigned interpretation of words: \<^item> @{thm [mode=iff] word_le_nat_alt [no_vars]} \<^item> @{thm [mode=iff] word_less_nat_alt [no_vars]} \<^item> @{thm unat_div_distrib [no_vars]} \<^item> @{thm unat_drop_bit_eq [no_vars]} \<^item> @{thm unat_mod_distrib [no_vars]} \<^item> @{thm [mode=iff] udvd_iff_dvd [no_vars]} \<^item> Operations with signed interpretation of words: \<^item> @{thm [mode=iff] word_sle_eq [no_vars]} \<^item> @{thm [mode=iff] word_sless_alt [no_vars]} \<^item> @{thm sint_signed_drop_bit_eq [no_vars]} \<^item> Rotation and reversal: \<^item> @{term [source] \word_rotl :: nat \ 'a::len word \ 'a word\} \<^item> @{term [source] \word_rotr :: nat \ 'a::len word \ 'a word\} \<^item> @{term [source] \word_roti :: int \ 'a::len word \ 'a word\} \<^item> @{term [source] \word_reverse :: 'a::len word \ 'a word\} \<^item> Concatenation: @{term [source, display] \word_cat :: 'a::len word \ 'b::len word \ 'c::len word\} For proofs about words the following default strategies are applicable: \<^item> Using bit extensionality (facts \<^text>\bit_eq_iff\, \<^text>\bit_word_eqI\; fact collection \<^text>\bit_simps\). \<^item> Using the @{method transfer} method. \ subsection \More library theories\ text \ Note: currently, most theories listed here are hardly separate entities since they import each other in various ways. Always inspect them to understand what you pull in if you want to import one. \<^descr>[Syntax] \<^descr>[\<^theory>\Word_Lib.Syntax_Bundles\] Bundles to provide alternative syntax for various bit operations. \<^descr>[\<^theory>\Word_Lib.Hex_Words\] Printing word numerals as hexadecimal numerals. \<^descr>[\<^theory>\Word_Lib.Type_Syntax\] Pretty type-sensitive syntax for cast operations. \<^descr>[\<^theory>\Word_Lib.Word_Syntax\] Specific ASCII syntax for prominent bit operations on word. \<^descr>[Proof tools] \<^descr>[\<^theory>\Word_Lib.Norm_Words\] Rewriting word numerals to normal forms. \<^descr>[\<^theory>\Word_Lib.Bitwise\] Method @{method word_bitwise} decomposes word equalities and inequalities into bit propositions. \<^descr>[\<^theory>\Word_Lib.Bitwise_Signed\] Method @{method word_bitwise_signed} decomposes word equalities and inequalities into bit propositions. \<^descr>[\<^theory>\Word_Lib.Word_EqI\] Method @{method word_eqI_solve} decomposes word equalities and inequalities into bit propositions. \<^descr>[Operations] \<^descr>[\<^theory>\Word_Lib.Signed_Division_Word\] Signed division on word: \<^item> @{term [source] \(sdiv) :: 'a::len word \ 'a word \ 'a word\} \<^item> @{term [source] \(smod) :: 'a::len word \ 'a word \ 'a word\} \<^descr>[\<^theory>\Word_Lib.Aligned\] \ \<^item> @{thm [mode=iff] is_aligned_iff_udvd [no_vars]} \<^descr>[\<^theory>\Word_Lib.Least_significant_bit\] The least significant bit as an alias: @{thm [mode=iff] lsb_odd [where ?'a = int, no_vars]} \<^descr>[\<^theory>\Word_Lib.Most_significant_bit\] The most significant bit: \<^item> @{thm [mode=iff] msb_int_def [of k]} \<^item> @{thm [mode=iff] word_msb_sint [no_vars]} \<^item> @{thm [mode=iff] msb_word_iff_sless_0 [no_vars]} \<^item> @{thm [mode=iff] msb_word_iff_bit [no_vars]} \<^descr>[\<^theory>\Word_Lib.Bit_Shifts_Infix_Syntax\] Bit shifts decorated with infix syntax: \<^item> @{thm Bit_Shifts_Infix_Syntax.shiftl_def [no_vars]} \<^item> @{thm Bit_Shifts_Infix_Syntax.shiftr_def [no_vars]} \<^item> @{thm Bit_Shifts_Infix_Syntax.sshiftr_def [no_vars]} \<^descr>[\<^theory>\Word_Lib.Next_and_Prev\] \ \<^item> @{thm word_next_unfold [no_vars]} \<^item> @{thm word_prev_unfold [no_vars]} \<^descr>[\<^theory>\Word_Lib.Enumeration_Word\] More on explicit enumeration of word types. \<^descr>[\<^theory>\Word_Lib.More_Word_Operations\] Even more operations on word. \<^descr>[Types] \<^descr>[\<^theory>\Word_Lib.Signed_Words\] Formal tagging of word types with a \<^text>\signed\ marker. \<^descr>[Lemmas] \<^descr>[\<^theory>\Word_Lib.More_Word\] More lemmas on words. \<^descr>[\<^theory>\Word_Lib.Word_Lemmas\] More lemmas on words, covering many other theories mentioned here. \<^descr>[Words of popular lengths]. \<^descr>[\<^theory>\Word_Lib.Word_8\] for 8-bit words. \<^descr>[\<^theory>\Word_Lib.Word_16\] for 16-bit words. \<^descr>[\<^theory>\Word_Lib.Word_32\] for 32-bit words. \<^descr>[\<^theory>\Word_Lib.Word_64\] for 64-bit words. This theory is not part of \<^text>\Word_Lib_Sumo\, because it shadows names from \<^theory>\Word_Lib.Word_32\. They can be used together, but then will have to use qualified names in applications. \<^descr>[\<^theory>\Word_Lib.Machine_Word_32\ and \<^theory>\Word_Lib.Machine_Word_64\] provide lemmas for 32-bit words and 64-bit words under the same name, which can help to organize applications relying on some form of genericity. \ subsection \More library sessions\ text \ \<^descr>[\<^text>\Native_Word\] Makes machine words and machine arithmetic available for code generation. It provides a common abstraction that hides the differences between the different target languages. The code generator maps these operations to the APIs of the target languages. \ subsection \Legacy theories\ text \ The following theories contain material which has been factored out since it is not recommended to use it in new applications, mostly because matters can be expressed succinctly using already existing operations. This section gives some indication how to migrate away from those theories. However theorem coverage may still be terse in some cases. \<^descr>[\<^theory>\Word_Lib.Word_Lib_Sumo\] An entry point importing any relevant theory in that session. Intended for backward compatibility: start importing this theory when migrating applications to Isabelle2021, and later sort out what you really need. You may need to include \<^theory>\Word_Lib.Word_64\ separately. \<^descr>[\<^theory>\Word_Lib.Generic_set_bit\] Kind of an alias: @{thm set_bit_eq [no_vars]} \<^descr>[\<^theory>\Word_Lib.Typedef_Morphisms\] A low-level extension to HOL typedef providing conversions along type morphisms. The @{method transfer} method seems to be sufficient for most applications though. \<^descr>[\<^theory>\Word_Lib.Bit_Comprehension\] Comprehension syntax for bit values over predicates - \<^typ>\nat \ bool\. For \<^typ>\'a::len word\, straightforward - alternatives exist; difficult to handle for \<^typ>\int\. + \<^typ>\nat \ bool\, for \<^typ>\'a::len word\; straightforward + alternatives exist. + + \<^descr>[\<^theory>\Word_Lib.Bit_Comprehension_Int\] + + Comprehension syntax for bit values over predicates + \<^typ>\nat \ bool\, for \<^typ>\int\; inherently non-computational. \<^descr>[\<^theory>\Word_Lib.Reversed_Bit_Lists\] Representation of bit values as explicit list in \<^emph>\reversed\ order. This should rarely be necessary: the \<^const>\bit\ projection should be sufficient in most cases. In case explicit lists are needed, existing operations can be used: @{thm [display] horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} \<^descr>[\<^theory>\Word_Lib.Many_More\] Collection of operations and theorems which are kept for backward compatibility and not used in other theories in session \<^text>\Word_Lib\. They are used in applications of \<^text>\Word_Lib\, but should be migrated to there. \ section \Changelog\ text \ \<^descr>[Changes since AFP 2022] ~ \<^item> Theory \<^text>\Word_Lib.Ancient_Numeral\ has been removed from session. + \<^item> Bit comprehension syntax for \<^typ>\int\ moved to separate theory + \<^theory>\Word_Lib.Bit_Comprehension_Int\. + \<^descr>[Changes since AFP 2021] ~ \<^item> Theory \<^text>\Word_Lib.Ancient_Numeral\ is not part of \<^theory>\Word_Lib.Word_Lib_Sumo\ any longer. \<^item> Infix syntax for \<^term>\(AND)\, \<^term>\(OR)\, \<^term>\(XOR)\ organized in syntax bundle \<^bundle>\bit_operations_syntax\. \<^item> Abbreviation \<^abbrev>\max_word\ moved from distribution into theory \<^theory>\Word_Lib.Legacy_Aliases\. \<^item> Operation \<^const>\test_bit\ replaced by input abbreviation \<^abbrev>\test_bit\. \<^item> Abbreviations \<^abbrev>\bin_nth\, \<^abbrev>\bin_last\, \<^abbrev>\bin_rest\, \<^abbrev>\bintrunc\, \<^abbrev>\sbintrunc\, \<^abbrev>\norm_sint\, \<^abbrev>\bin_cat\ moved into theory \<^theory>\Word_Lib.Legacy_Aliases\. \<^item> Operations \<^abbrev>\bshiftr1\, \<^abbrev>\setBit\, \<^abbrev>\clearBit\ moved from distribution into theory \<^theory>\Word_Lib.Legacy_Aliases\ and replaced by input abbreviations. \<^item> Operations \<^const>\shiftl1\, \<^const>\shiftr1\, \<^const>\sshiftr1\ moved here from distribution. \<^item> Operation \<^const>\complement\ replaced by input abbreviation \<^abbrev>\complement\. \ (*<*) end (*>*) diff --git a/thys/Word_Lib/Word_Lib_Sumo.thy b/thys/Word_Lib/Word_Lib_Sumo.thy --- a/thys/Word_Lib/Word_Lib_Sumo.thy +++ b/thys/Word_Lib/Word_Lib_Sumo.thy @@ -1,136 +1,137 @@ (* * Copyright Florian Haftmann * * SPDX-License-Identifier: BSD-2-Clause *) section \Ancient comprehensive Word Library\ theory Word_Lib_Sumo imports "HOL-Library.Word" Aligned Bit_Comprehension + Bit_Comprehension_Int Bit_Shifts_Infix_Syntax Bits_Int Bitwise_Signed Bitwise Enumeration_Word Generic_set_bit Hex_Words Least_significant_bit More_Arithmetic More_Divides More_Sublist Even_More_List More_Misc Strict_part_mono Legacy_Aliases Most_significant_bit Next_and_Prev Norm_Words Reversed_Bit_Lists Rsplit Signed_Words Syntax_Bundles Typedef_Morphisms Type_Syntax Word_EqI Word_Lemmas Word_8 Word_16 Word_32 Word_Syntax Signed_Division_Word Singleton_Bit_Shifts More_Word_Operations Many_More begin unbundle bit_operations_syntax unbundle bit_projection_infix_syntax declare word_induct2[induct type] declare word_nat_cases[cases type] declare signed_take_bit_Suc [simp] (* these generate take_bit terms, which we often don't want for concrete lengths *) lemmas of_int_and_nat = unsigned_of_nat unsigned_of_int signed_of_int signed_of_nat bundle no_take_bit begin declare of_int_and_nat[simp del] end lemmas bshiftr1_def = bshiftr1_eq lemmas is_down_def = is_down_eq lemmas is_up_def = is_up_eq lemmas mask_def = mask_eq lemmas scast_def = scast_eq lemmas shiftl1_def = shiftl1_eq lemmas shiftr1_def = shiftr1_eq lemmas sshiftr1_def = sshiftr1_eq lemmas sshiftr_def = sshiftr_eq_funpow_sshiftr1 lemmas to_bl_def = to_bl_eq lemmas ucast_def = ucast_eq lemmas unat_def = unat_eq_nat_uint lemmas word_cat_def = word_cat_eq lemmas word_reverse_def = word_reverse_eq_of_bl_rev_to_bl lemmas word_roti_def = word_roti_eq_word_rotr_word_rotl lemmas word_rotl_def = word_rotl_eq lemmas word_rotr_def = word_rotr_eq lemmas word_sle_def = word_sle_eq lemmas word_sless_def = word_sless_eq lemmas uint_0 = uint_nonnegative lemmas uint_lt = uint_bounded lemmas uint_mod_same = uint_idem lemmas of_nth_def = word_set_bits_def lemmas of_nat_word_eq_iff = word_of_nat_eq_iff lemmas of_nat_word_eq_0_iff = word_of_nat_eq_0_iff lemmas of_int_word_eq_iff = word_of_int_eq_iff lemmas of_int_word_eq_0_iff = word_of_int_eq_0_iff lemmas word_next_def = word_next_unfold lemmas word_prev_def = word_prev_unfold lemmas is_aligned_def = is_aligned_iff_dvd_nat lemmas word_and_max_simps = word8_and_max_simp word16_and_max_simp word32_and_max_simp lemma distinct_lemma: "f x \ f y \ x \ y" by auto lemmas and_bang = word_and_nth lemmas sdiv_int_def = signed_divide_int_def lemmas smod_int_def = signed_modulo_int_def (* shortcut for some specific lengths *) lemma word_fixed_sint_1[simp]: "sint (1::8 word) = 1" "sint (1::16 word) = 1" "sint (1::32 word) = 1" "sint (1::64 word) = 1" by (auto simp: sint_word_ariths) declare of_nat_diff [simp] (* Haskellish names/syntax *) notation (input) bit ("testBit") lemmas cast_simps = cast_simps ucast_down_bl (* shadows the slightly weaker Word.nth_ucast *) lemma nth_ucast: "(ucast (w::'a::len word)::'b::len word) !! n = (w !! n \ n < min LENGTH('a) LENGTH('b))" by (auto simp add: bit_simps not_le dest: bit_imp_le_length) end