diff --git a/thys/Native_Word/Code_Symbolic_Int_Bit.thy b/thys/Native_Word/Code_Symbolic_Int_Bit.thy --- a/thys/Native_Word/Code_Symbolic_Int_Bit.thy +++ b/thys/Native_Word/Code_Symbolic_Int_Bit.thy @@ -1,130 +1,104 @@ (* Title: Code_Symbolic_Int_Bit.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Symbolic implementation of bit operations on int\ theory Code_Symbolic_Int_Bit imports - "Word_Lib.Least_significant_bit" - "Word_Lib.Generic_set_bit" - "Word_Lib.Bit_Comprehension" + Main begin section \Implementations of bit operations on \<^typ>\int\ operating on symbolic representation\ context includes bit_operations_syntax begin lemma test_bit_int_code [code]: "bit (0::int) n = False" "bit (Int.Neg num.One) n = True" "bit (Int.Pos num.One) 0 = True" "bit (Int.Pos (num.Bit0 m)) 0 = False" "bit (Int.Pos (num.Bit1 m)) 0 = True" "bit (Int.Neg (num.Bit0 m)) 0 = False" "bit (Int.Neg (num.Bit1 m)) 0 = True" "bit (Int.Pos num.One) (Suc n) = False" "bit (Int.Pos (num.Bit0 m)) (Suc n) = bit (Int.Pos m) n" "bit (Int.Pos (num.Bit1 m)) (Suc n) = bit (Int.Pos m) n" "bit (Int.Neg (num.Bit0 m)) (Suc n) = bit (Int.Neg m) n" "bit (Int.Neg (num.Bit1 m)) (Suc n) = bit (Int.Neg (Num.inc m)) n" by (simp_all add: Num.add_One bit_0 bit_Suc) lemma int_not_code [code]: "NOT (0 :: int) = -1" "NOT (Int.Pos n) = Int.Neg (Num.inc n)" "NOT (Int.Neg n) = Num.sub n num.One" by (simp_all add: Num.add_One not_int_def) lemma int_and_code [code]: fixes i j :: int shows "0 AND j = 0" "i AND 0 = 0" "Int.Pos n AND Int.Pos m = (case and_num n m of None \ 0 | Some n' \ Int.Pos n')" "Int.Neg n AND Int.Neg m = NOT (Num.sub n num.One OR Num.sub m num.One)" "Int.Pos n AND Int.Neg num.One = Int.Pos n" "Int.Pos n AND Int.Neg (num.Bit0 m) = Num.sub (or_not_num_neg (Num.BitM m) n) num.One" "Int.Pos n AND Int.Neg (num.Bit1 m) = Num.sub (or_not_num_neg (num.Bit0 m) n) num.One" "Int.Neg num.One AND Int.Pos m = Int.Pos m" "Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (or_not_num_neg (Num.BitM n) m) num.One" "Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (or_not_num_neg (num.Bit0 n) m) num.One" - apply (simp_all add: and_num_eq_None_iff [where ?'a = int] and_num_eq_Some_iff [where ?'a = int] + apply (auto simp add: and_num_eq_None_iff [where ?'a = int] and_num_eq_Some_iff [where ?'a = int] split: option.split) apply (simp_all only: sub_one_eq_not_neg numeral_or_not_num_eq minus_minus and_not_numerals bit.de_Morgan_disj bit.double_compl and_not_num_eq_None_iff and_not_num_eq_Some_iff ac_simps) - apply auto done lemma int_or_code [code]: fixes i j :: int shows "0 OR j = j" "i OR 0 = i" "Int.Pos n OR Int.Pos m = Int.Pos (or_num n m)" "Int.Neg n OR Int.Neg m = NOT (Num.sub n num.One AND Num.sub m num.One)" "Int.Pos n OR Int.Neg num.One = Int.Neg num.One" "Int.Pos n OR Int.Neg (num.Bit0 m) = (case and_not_num (Num.BitM m) n of None \ -1 | Some n' \ Int.Neg (Num.inc n'))" "Int.Pos n OR Int.Neg (num.Bit1 m) = (case and_not_num (num.Bit0 m) n of None \ -1 | Some n' \ Int.Neg (Num.inc n'))" "Int.Neg num.One OR Int.Pos m = Int.Neg num.One" "Int.Neg (num.Bit0 n) OR Int.Pos m = (case and_not_num (Num.BitM n) m of None \ -1 | Some n' \ Int.Neg (Num.inc n'))" "Int.Neg (num.Bit1 n) OR Int.Pos m = (case and_not_num (num.Bit0 n) m of None \ -1 | Some n' \ Int.Neg (Num.inc n'))" apply (auto simp add: numeral_or_num_eq split: option.splits) apply (simp_all only: and_not_num_eq_None_iff and_not_num_eq_Some_iff and_not_numerals numeral_or_not_num_eq or_int_def bit.double_compl ac_simps flip: numeral_eq_iff [where ?'a = int]) apply simp_all done lemma int_xor_code [code]: fixes i j :: int shows "0 XOR j = j" "i XOR 0 = i" "Int.Pos n XOR Int.Pos m = (case xor_num n m of None \ 0 | Some n' \ Int.Pos n')" "Int.Neg n XOR Int.Neg m = Num.sub n num.One XOR Num.sub m num.One" "Int.Neg n XOR Int.Pos m = NOT (Num.sub n num.One XOR Int.Pos m)" "Int.Pos n XOR Int.Neg m = NOT (Int.Pos n XOR Num.sub m num.One)" by (simp_all add: xor_num_eq_None_iff [where ?'a = int] xor_num_eq_Some_iff [where ?'a = int] split: option.split) -lemma bin_rest_code: "i div 2 = drop_bit 1 i" for i :: int - by (simp add: drop_bit_eq_div) - -lemma set_bits_code [code]: - "set_bits = Code.abort (STR ''set_bits is unsupported on type int'') (\_. set_bits :: _ \ int)" - by simp - -lemma fixes i :: int - shows int_set_bit_True_conv_OR [code]: "Generic_set_bit.set_bit i n True = i OR push_bit n 1" - and int_set_bit_False_conv_NAND [code]: "Generic_set_bit.set_bit i n False = i AND NOT (push_bit n 1)" - and int_set_bit_conv_ops: "Generic_set_bit.set_bit i n b = (if b then i OR (push_bit n 1) else i AND NOT (push_bit n 1))" - by (simp_all add: bit_eq_iff) (auto simp add: bit_simps) - declare [[code drop: \drop_bit :: nat \ int \ int\]] lemma drop_bit_int_code [code]: fixes i :: int shows "drop_bit 0 i = i" "drop_bit (Suc n) 0 = (0 :: int)" "drop_bit (Suc n) (Int.Pos num.One) = 0" "drop_bit (Suc n) (Int.Pos (num.Bit0 m)) = drop_bit n (Int.Pos m)" "drop_bit (Suc n) (Int.Pos (num.Bit1 m)) = drop_bit n (Int.Pos m)" "drop_bit (Suc n) (Int.Neg num.One) = - 1" "drop_bit (Suc n) (Int.Neg (num.Bit0 m)) = drop_bit n (Int.Neg m)" "drop_bit (Suc n) (Int.Neg (num.Bit1 m)) = drop_bit n (Int.Neg (Num.inc m))" by (simp_all add: drop_bit_Suc add_One) declare [[code drop: \push_bit :: nat \ int \ int\]] lemma push_bit_int_code [code]: "push_bit 0 i = i" "push_bit (Suc n) i = push_bit n (Int.dup i)" by (simp_all add: ac_simps) -lemma int_lsb_code [code]: - "lsb (0 :: int) = False" - "lsb (Int.Pos num.One) = True" - "lsb (Int.Pos (num.Bit0 w)) = False" - "lsb (Int.Pos (num.Bit1 w)) = True" - "lsb (Int.Neg num.One) = True" - "lsb (Int.Neg (num.Bit0 w)) = False" - "lsb (Int.Neg (num.Bit1 w)) = True" - by simp_all - end end 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,679 +1,683 @@ (* Title: Code_Target_Integer_Bit.thy Author: Andreas Lochbihler, ETH Zurich *) chapter \Bit operations for target language integers\ -theory Code_Target_Integer_Bit imports - "Word_Lib.Bit_Comprehension" - Code_Int_Integer_Conversion - Code_Symbolic_Int_Bit +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 (simp add: int_set_bit_False_conv_NAND int_set_bit_True_conv_OR) + 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/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,428 +1,398 @@ (* 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" - "Word_Lib.Bit_Comprehension" -begin - -text \More lemmas\ - -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 - -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) - -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) - -context - includes bit_operations_syntax +theory Code_Target_Word_Base + imports + "HOL-Library.Word" + "Word_Lib.Signed_Division_Word" + "Word_Lib.More_Word" begin -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 - -end - - -text \Division on @{typ "'a word"} is unsigned, but Scala and OCaml only have signed division and modulus.\ - -lemmas word_sdiv_def = sdiv_word_def -lemmas word_smod_def = smod_word_def - -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. -\ +subsection \More on conversions\ -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: push_bit_of_1 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 push_bit_of_1 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 +lemma int_of_integer_unsigned_eq [simp]: + \int_of_integer (unsigned w) = uint w\ + by transfer simp - -text \More implementations tailored towards target-language implementations\ +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(simp add: word_of_integer.rep_eq) - -end - -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) - -context - 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 + by (fact word_of_integer.rep_eq) end -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 push_bit_of_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 push_bit_of_1 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 push_bit_of_1) - moreover - have "overflow \ i' - shift \ False" using \i' < shift\ unfolding assms - by(cases "LENGTH('a)")(auto simp add: not_le push_bit_of_1 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 push_bit_of_1 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 push_bit_of_1 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 +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) -text \Quickcheck conversion functions\ +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/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,341 +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" - Code_Target_Word_Base + "Word_Lib.Bit_Comprehension" + "Code_Target_Word_Base" begin -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 - -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) - - 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 word_of_numeral) + 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 word_of_numeral) + 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 word_of_numeral) + 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 word_of_numeral) + 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 word_of_numeral) + 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_numeral word_of_0) + 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 word_of_numeral even_iff_word_of word_of_mod even_iff_mod_2_eq_zero) + 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 push_bit_of_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 word_of_numeral + 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 push_bit_of_1) + 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 word_of_numeral) + 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_numeral word_of_integer.rep_eq) + by (simp add: eq_iff_word_of word_of_integer_eq word_of_integer.rep_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_numeral word_of_integer.rep_eq) + by (simp add: eq_iff_word_of word_of_integer_eq word_of_minus word_of_integer.rep_eq) 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) = Code_Target_Word_Base.set_bits_aux P n (word_of 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 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,251 +1,299 @@ (* * 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/Generic_set_bit.thy b/thys/Word_Lib/Generic_set_bit.thy --- a/thys/Word_Lib/Generic_set_bit.thy +++ b/thys/Word_Lib/Generic_set_bit.thy @@ -1,124 +1,136 @@ (* * Copyright Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) (* Author: Jeremy Dawson, NICTA *) section \Operation variant for setting and unsetting bits\ theory Generic_set_bit imports "HOL-Library.Word" Most_significant_bit begin class set_bit = semiring_bits + fixes set_bit :: \'a \ nat \ bool \ 'a\ assumes bit_set_bit_iff_2n: \bit (set_bit a m b) n \ (if m = n then b else bit a n) \ 2 ^ n \ 0\ lemmas bit_set_bit_iff[bit_simps] = bit_set_bit_iff_2n[simplified fold_possible_bit simp_thms] lemma set_bit_eq: \set_bit a n b = (if b then Bit_Operations.set_bit else unset_bit) n a\ for a :: \'a::{ring_bit_operations, set_bit}\ by (rule bit_eqI) (simp add: bit_simps) instantiation int :: set_bit begin definition set_bit_int :: \int \ nat \ bool \ int\ where \set_bit_int i n b = (if b then Bit_Operations.set_bit else Bit_Operations.unset_bit) n i\ instance by standard (simp_all add: set_bit_int_def bit_simps) end +context + includes bit_operations_syntax +begin + +lemma fixes i :: int + shows int_set_bit_True_conv_OR [code]: "Generic_set_bit.set_bit i n True = i OR push_bit n 1" + and int_set_bit_False_conv_NAND [code]: "Generic_set_bit.set_bit i n False = i AND NOT (push_bit n 1)" + and int_set_bit_conv_ops: "Generic_set_bit.set_bit i n b = (if b then i OR (push_bit n 1) else i AND NOT (push_bit n 1))" + by (simp_all add: bit_eq_iff) (auto simp add: bit_simps) + +end + instantiation word :: (len) set_bit begin definition set_bit_word :: \'a word \ nat \ bool \ 'a word\ where set_bit_unfold: \set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)\ for w :: \'a::len word\ instance by standard (auto simp add: set_bit_unfold bit_simps dest: bit_imp_le_length) end lemma bit_set_bit_word_iff [bit_simps]: \bit (set_bit w m b) n \ (if m = n then n < LENGTH('a) \ b else bit w n)\ for w :: \'a::len word\ by (auto simp add: bit_simps dest: bit_imp_le_length) lemma test_bit_set_gen: "bit (set_bit w n x) m \ (if m = n then n < size w \ x else bit w m)" for w :: "'a::len word" by (simp add: bit_set_bit_word_iff word_size) lemma test_bit_set: "bit (set_bit w n x) n \ n < size w \ x" for w :: "'a::len word" by (auto simp add: bit_simps word_size) lemma word_set_nth: "set_bit w n (bit w n) = w" for w :: "'a::len word" by (rule bit_word_eqI) (simp add: bit_simps) lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y" for w :: "'a::len word" by (rule word_eqI) (simp add : test_bit_set_gen word_size) lemma word_set_set_diff: fixes w :: "'a::len word" assumes "m \ n" shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms) lemma word_set_nth_iff: "set_bit w n b = w \ bit w n = b \ n \ size w" for w :: "'a::len word" apply (rule iffI) apply (rule disjCI) apply (drule word_eqD) apply (erule sym [THEN trans]) apply (simp add: test_bit_set) apply (erule disjE) apply clarsimp apply (rule word_eqI) apply (clarsimp simp add : test_bit_set_gen) apply (auto simp add: word_size) apply (rule bit_eqI) apply (simp add: bit_simps) done lemma word_clr_le: "w \ set_bit w n False" for w :: "'a::len word" apply (simp add: set_bit_unfold) apply transfer apply (simp add: take_bit_unset_bit_eq unset_bit_less_eq) done lemma word_set_ge: "w \ set_bit w n True" for w :: "'a::len word" apply (simp add: set_bit_unfold) apply transfer apply (simp add: take_bit_set_bit_eq set_bit_greater_eq) done lemma set_bit_beyond: "size x \ n \ set_bit x n b = x" for x :: "'a :: len word" by (simp add: word_set_nth_iff) lemma one_bit_shiftl: "set_bit 0 n True = (1 :: 'a :: len word) << n" apply (rule word_eqI) apply (auto simp add: word_size bit_simps) done lemma one_bit_pow: "set_bit 0 n True = (2 :: 'a :: len word) ^ n" by (simp add: one_bit_shiftl shiftl_def) end diff --git a/thys/Word_Lib/Many_More.thy b/thys/Word_Lib/Many_More.thy --- a/thys/Word_Lib/Many_More.thy +++ b/thys/Word_Lib/Many_More.thy @@ -1,690 +1,693 @@ (* * Copyright Data61, CSIRO (ABN 41 687 119 230) * * SPDX-License-Identifier: BSD-2-Clause *) theory Many_More imports Main "HOL-Library.Word" More_Word Even_More_List begin lemma nat_less_mult_monoish: "\ a < b; c < (d :: nat) \ \ (a + 1) * (c + 1) <= b * d" apply (drule Suc_leI)+ apply (drule(1) mult_le_mono) apply simp done context includes bit_operations_syntax begin lemma if_and_helper: "(If x v v') AND v'' = If x (v AND v'') (v' AND v'')" by (rule if_distrib) end lemma eq_eqI: "a = b \ (a = x) = (b = x)" by simp lemma map2_Cons_2_3: "(map2 f xs (y # ys) = (z # zs)) = (\x xs'. xs = x # xs' \ f x y = z \ map2 f xs' ys = zs)" by (case_tac xs, simp_all) lemma map2_xor_replicate_False: "map2 (\x y. x \ \ y) xs (replicate n False) = take n xs" apply (induct xs arbitrary: n, simp) apply (case_tac n; simp) done lemma plus_Collect_helper: "(+) x ` {xa. P (xa :: 'a :: len word)} = {xa. P (xa - x)}" by (fastforce simp add: image_def) lemma plus_Collect_helper2: "(+) (- x) ` {xa. P (xa :: 'a :: len word)} = {xa. P (x + xa)}" using plus_Collect_helper [of "- x" P] by (simp add: ac_simps) lemma range_subset_eq2: "{a :: 'a :: len word .. b} \ {} \ ({a .. b} \ {c .. d}) = (c \ a \ b \ d)" by simp lemma nat_mod_power_lem: fixes a :: nat shows "1 < a \ a ^ n mod a ^ m = (if m \ n then 0 else a ^ n)" apply (clarsimp) apply (clarsimp simp add: le_iff_add power_add) done lemma i_hate_words_helper: "i \ (j - k :: nat) \ i \ j" by simp lemma i_hate_words: "unat (a :: 'a word) \ unat (b :: 'a :: len word) - Suc 0 \ a \ -1" apply (frule i_hate_words_helper) apply (subst(asm) word_le_nat_alt[symmetric]) apply (clarsimp simp only: word_minus_one_le) apply (simp only: linorder_not_less[symmetric]) apply (erule notE) apply (rule diff_Suc_less) apply (subst neq0_conv[symmetric]) apply (subst unat_eq_0) apply (rule notI, drule arg_cong[where f="(+) 1"]) apply simp done lemma If_eq_obvious: "x \ z \ ((if P then x else y) = z) = (\ P \ y = z)" by simp lemma Some_to_the: "v = Some x \ x = the v" by simp lemma dom_if_Some: "dom (\x. if P x then Some (f x) else g x) = {x. P x} \ dom g" by fastforce lemma dom_insert_absorb: "x \ dom f \ insert x (dom f) = dom f" by (fact insert_absorb) lemma emptyE2: "\ S = {}; x \ S \ \ P" by simp lemma ptr_add_image_multI: "\ \x y. (x * val = y * val') = (x * val'' = y); x * val'' \ S \ \ ptr_add ptr (x * val) \ (\p. ptr_add ptr (p * val')) ` S" by (auto simp add: image_iff) metis lemmas map_prod_split_imageI' = map_prod_imageI[where f="case_prod f" and g="case_prod g" and a="(a, b)" and b="(c, d)" for a b c d f g] lemmas map_prod_split_imageI = map_prod_split_imageI'[simplified] lemma dom_if: "dom (\a. if a \ addrs then Some (f a) else g a) = addrs \ dom g" by (auto simp: dom_def split: if_split) lemmas arg_cong_Not = arg_cong [where f=Not] lemma drop_append_miracle: "n = length xs \ drop n (xs @ ys) = ys" by simp lemma foldr_does_nothing_to_xf: "\ \x s. x \ set xs \ xf (f x s) = xf s \ \ xf (foldr f xs s) = xf s" by (induct xs, simp_all) lemma mod_mod_power_int: fixes k :: int shows "k mod 2 ^ m mod 2 ^ n = k mod 2 ^ (min m n)" by (fact mod_exp_eq) lemma le_step_down_nat:"\(i::nat) \ n; i = n \ P; i \ n - 1 \ P\ \ P" by arith lemma le_step_down_int:"\(i::int) \ n; i = n \ P; i \ n - 1 \ P\ \ P" by arith lemma replicate_numeral [simp]: "replicate (numeral k) x = x # replicate (pred_numeral k) x" by (simp add: numeral_eq_Suc) lemma list_exhaust_size_gt0: assumes "\a list. y = a # list \ P" shows "0 < length y \ P" apply (cases y) apply simp apply (rule assms) apply fastforce done lemma list_exhaust_size_eq0: assumes "y = [] \ P" shows "length y = 0 \ P" apply (cases y) apply (rule assms) apply simp apply simp done lemma size_Cons_lem_eq: "y = xa # list \ size y = Suc k \ size list = k" by auto lemma takeWhile_take_has_property: "n \ length (takeWhile P xs) \ \x \ set (take n xs). P x" by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all) lemma takeWhile_take_has_property_nth: "\ n < length (takeWhile P xs) \ \ P (xs ! n)" by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all) lemma takeWhile_replicate: "takeWhile f (replicate len x) = (if f x then replicate len x else [])" by (induct_tac len) auto lemma takeWhile_replicate_empty: "\ f x \ takeWhile f (replicate len x) = []" by (simp add: takeWhile_replicate) lemma takeWhile_replicate_id: "f x \ takeWhile f (replicate len x) = replicate len x" by (simp add: takeWhile_replicate) lemma nth_rev: "n < length xs \ rev xs ! n = xs ! (length xs - 1 - n)" using rev_nth by simp lemma nth_rev_alt: "n < length ys \ ys ! n = rev ys ! (length ys - Suc n)" by (simp add: nth_rev) lemma hd_butlast: "length xs > 1 \ hd (butlast xs) = hd xs" by (cases xs) auto lemma split_upt_on_n: "n < m \ [0 ..< m] = [0 ..< n] @ [n] @ [Suc n ..< m]" by (metis append_Cons append_Nil less_Suc_eq_le less_imp_le_nat upt_add_eq_append' upt_rec zero_less_Suc) lemma drop_eq_mono: assumes le: "m \ n" assumes drop: "drop m xs = drop m ys" shows "drop n xs = drop n ys" proof - have ex: "\p. n = p + m" by (rule exI[of _ "n - m"]) (simp add: le) then obtain p where p: "n = p + m" by blast show ?thesis unfolding p drop_drop[symmetric] drop by simp qed lemma drop_Suc_nth: "n < length xs \ drop n xs = xs!n # drop (Suc n) xs" by (simp add: Cons_nth_drop_Suc) lemma and_len: "xs = ys \ xs = ys \ length xs = length ys" by auto lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)" by auto lemma hd_if: "hd (if p then xs else ys) = (if p then hd xs else hd ys)" by auto lemma if_single: "(if xc then [xab] else [an]) = [if xc then xab else an]" by auto \ \note -- \if_Cons\ can cause blowup in the size, if \p\ is complex, so make a simproc\ lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys" by auto lemma list_of_false: "True \ set xs \ xs = replicate (length xs) False" by (induct xs, simp_all) lemma list_all2_induct [consumes 1, case_names Nil Cons]: assumes lall: "list_all2 Q xs ys" and nilr: "P [] []" and consr: "\x xs y ys. \list_all2 Q xs ys; Q x y; P xs ys\ \ P (x # xs) (y # ys)" shows "P xs ys" using lall proof (induct rule: list_induct2 [OF list_all2_lengthD [OF lall]]) case 1 then show ?case by auto fact+ next case (2 x xs y ys) show ?case proof (rule consr) from "2.prems" show "list_all2 Q xs ys" and "Q x y" by simp_all then show "P xs ys" by (intro "2.hyps") qed qed lemma replicate_minus: "k < n \ replicate n False = replicate (n - k) False @ replicate k False" by (subst replicate_add [symmetric]) simp lemma cart_singleton_empty: "(S \ {e} = {}) = (S = {})" by blast lemma MinI: assumes fa: "finite A" and ne: "A \ {}" and xv: "m \ A" and min: "\y \ A. m \ y" shows "Min A = m" using fa ne xv min proof (induct A arbitrary: m rule: finite_ne_induct) case singleton then show ?case by simp next case (insert y F) from insert.prems have yx: "m \ y" and fx: "\y \ F. m \ y" by auto have "m \ insert y F" by fact then show ?case proof assume mv: "m = y" have mlt: "m \ Min F" by (rule iffD2 [OF Min_ge_iff [OF insert.hyps(1) insert.hyps(2)] fx]) show ?case apply (subst Min_insert [OF insert.hyps(1) insert.hyps(2)]) apply (subst mv [symmetric]) apply (auto simp: min_def mlt) done next assume "m \ F" then have mf: "Min F = m" by (rule insert.hyps(4) [OF _ fx]) show ?case apply (subst Min_insert [OF insert.hyps(1) insert.hyps(2)]) apply (subst mf) apply (rule iffD2 [OF _ yx]) apply (auto simp: min_def) done qed qed lemma power_numeral: "a ^ numeral k = a * a ^ (pred_numeral k)" by (simp add: numeral_eq_Suc) lemma funpow_numeral [simp]: "f ^^ numeral k = f \ f ^^ (pred_numeral k)" by (simp add: numeral_eq_Suc) lemma funpow_minus_simp: "0 < n \ f ^^ n = f \ f ^^ (n - 1)" by (auto dest: gr0_implies_Suc) lemma rco_alt: "(f \ g) ^^ n \ f = f \ (g \ f) ^^ n" apply (rule ext) apply (induct n) apply (simp_all add: o_def) done lemma union_sub: "\B \ A; C \ B\ \ (A - B) \ (B - C) = (A - C)" by fastforce lemma insert_sub: "x \ xs \ (insert x (xs - ys)) = (xs - (ys - {x}))" by blast lemma ran_upd: "\ inj_on f (dom f); f y = Some z \ \ ran (\x. if x = y then None else f x) = ran f - {z}" unfolding ran_def apply (rule set_eqI) apply simp by (metis domI inj_on_eq_iff option.sel) lemma if_apply_def2: "(if P then F else G) = (\x. (P \ F x) \ (\ P \ G x))" by simp lemma case_bool_If: "case_bool P Q b = (if b then P else Q)" by simp lemma if_f: "(if a then f b else f c) = f (if a then b else c)" by simp lemma size_if: "size (if p then xs else ys) = (if p then size xs else size ys)" by (fact if_distrib) lemma if_Not_x: "(if p then \ x else x) = (p = (\ x))" by auto lemma if_x_Not: "(if p then x else \ x) = (p = x)" by auto lemma if_same_and: "(If p x y \ If p u v) = (if p then x \ u else y \ v)" by auto lemma if_same_eq: "(If p x y = (If p u v)) = (if p then x = u else y = v)" by auto lemma if_same_eq_not: "(If p x y = (\ If p u v)) = (if p then x = (\ u) else y = (\ v))" by auto lemma the_elemI: "y = {x} \ the_elem y = x" by simp lemma nonemptyE: "S \ {} \ (\x. x \ S \ R) \ R" by auto lemmas xtr1 = xtrans(1) lemmas xtr2 = xtrans(2) lemmas xtr3 = xtrans(3) lemmas xtr4 = xtrans(4) lemmas xtr5 = xtrans(5) lemmas xtr6 = xtrans(6) lemmas xtr7 = xtrans(7) lemmas xtr8 = xtrans(8) lemmas if_fun_split = if_apply_def2 lemma not_empty_eq: "(S \ {}) = (\x. x \ S)" by auto lemma range_subset_lower: fixes c :: "'a ::linorder" shows "\ {a..b} \ {c..d}; x \ {a..b} \ \ c \ a" apply (frule (1) subsetD) apply (rule classical) apply clarsimp done lemma range_subset_upper: fixes c :: "'a ::linorder" shows "\ {a..b} \ {c..d}; x \ {a..b} \ \ b \ d" apply (frule (1) subsetD) apply (rule classical) apply clarsimp done lemma range_subset_eq: fixes a::"'a::linorder" assumes non_empty: "a \ b" shows "({a..b} \ {c..d}) = (c \ a \ b \ d)" apply (insert non_empty) apply (rule iffI) apply (frule range_subset_lower [where x=a], simp) apply (drule range_subset_upper [where x=a], simp) apply simp apply auto done lemma range_eq: fixes a::"'a::linorder" assumes non_empty: "a \ b" shows "({a..b} = {c..d}) = (a = c \ b = d)" by (metis atLeastatMost_subset_iff eq_iff non_empty) lemma range_strict_subset_eq: fixes a::"'a::linorder" assumes non_empty: "a \ b" shows "({a..b} \ {c..d}) = (c \ a \ b \ d \ (a = c \ b \ d))" apply (insert non_empty) apply (subst psubset_eq) apply (subst range_subset_eq, assumption+) apply (subst range_eq, assumption+) apply simp done lemma range_subsetI: fixes x :: "'a :: order" assumes xX: "X \ x" and yY: "y \ Y" shows "{x .. y} \ {X .. Y}" using xX yY by auto lemma set_False [simp]: "(set bs \ {False}) = (True \ set bs)" by auto lemma int_not_emptyD: "A \ B \ {} \ \x. x \ A \ x \ B" by (erule contrapos_np, clarsimp simp: disjoint_iff_not_equal) definition sum_map :: "('a \ 'b) \ ('c \ 'd) \ 'a + 'c \ 'b + 'd" where "sum_map f g x \ case x of Inl v \ Inl (f v) | Inr v' \ Inr (g v')" lemma sum_map_simps[simp]: "sum_map f g (Inl v) = Inl (f v)" "sum_map f g (Inr w) = Inr (g w)" by (simp add: sum_map_def)+ lemma if_Some_None_eq_None: "((if P then Some v else None) = None) = (\ P)" by simp lemma CollectPairFalse [iff]: "{(a,b). False} = {}" by (simp add: split_def) lemma if_conj_dist: "((if b then w else x) \ (if b then y else z) \ X) = ((if b then w \ y else x \ z) \ X)" by simp lemma if_P_True1: "Q \ (if P then True else Q)" by simp lemma if_P_True2: "Q \ (if P then Q else True)" by simp lemmas nat_simps = diff_add_inverse2 diff_add_inverse lemmas nat_iffs = le_add1 le_add2 lemma nat_min_simps: "(a::nat) \ b \ min b a = a" "a \ b \ min a b = a" by simp_all lemmas zadd_diff_inverse = trans [OF diff_add_cancel [symmetric] add.commute] lemmas add_diff_cancel2 = add.commute [THEN diff_eq_eq [THEN iffD2]] lemmas mcl = mult_cancel_left [THEN iffD1, THEN make_pos_rule] lemma pl_pl_rels: "a + b = c + d \ a \ c \ b \ d \ a \ c \ b \ d" for a b c d :: nat by arith lemmas pl_pl_rels' = add.commute [THEN [2] trans, THEN pl_pl_rels] lemma iszero_minus: \iszero (- z) \ iszero z\ by (simp add: iszero_def) lemma diff_le_eq': "a - b \ c \ a \ b + c" for a b c :: int by arith lemma zless2: "0 < (2 :: int)" by (fact zero_less_numeral) lemma zless2p: "0 < (2 ^ n :: int)" by arith lemma zle2p: "0 \ (2 ^ n :: int)" by arith lemma ex_eq_or: "(\m. n = Suc m \ (m = k \ P m)) \ n = Suc k \ (\m. n = Suc m \ P m)" by auto lemma power_minus_simp: "0 < n \ a ^ n = a * a ^ (n - 1)" by (auto dest: gr0_implies_Suc) lemma n2s_ths: \2 + n = Suc (Suc n)\ \n + 2 = Suc (Suc n)\ by (fact add_2_eq_Suc add_2_eq_Suc')+ lemma s2n_ths: \Suc (Suc n) = 2 + n\ \Suc (Suc n) = n + 2\ by simp_all lemma gt_or_eq_0: "0 < y \ 0 = y" for y :: nat by arith lemma sum_imp_diff: "j = k + i \ j - i = k" for k :: nat by simp lemma le_diff_eq': "a \ c - b \ b + a \ c" for a b c :: int by arith lemma less_diff_eq': "a < c - b \ b + a < c" for a b c :: int by arith lemma diff_less_eq': "a - b < c \ a < b + c" for a b c :: int by arith lemma axxbyy: "a + m + m = b + n + n \ a = 0 \ a = 1 \ b = 0 \ b = 1 \ a = b \ m = n" for a b m n :: int by arith lemma minus_eq: "m - k = m \ k = 0 \ m = 0" for k m :: nat by arith lemma pl_pl_mm: "a + b = c + d \ a - c = d - b" for a b c d :: nat by arith lemmas pl_pl_mm' = add.commute [THEN [2] trans, THEN pl_pl_mm] lemma less_le_mult': "w * c < b * c \ 0 \ c \ (w + 1) * c \ b * c" for b c w :: int apply (rule mult_right_mono) apply (rule zless_imp_add1_zle) apply (erule (1) mult_right_less_imp_less) apply assumption done lemma less_le_mult: "w * c < b * c \ 0 \ c \ w * c + c \ b * c" for b c w :: int using less_le_mult' [of w c b] by (simp add: algebra_simps) lemmas less_le_mult_minus = iffD2 [OF le_diff_eq less_le_mult, simplified left_diff_distrib] lemma gen_minus: "0 < n \ f n = f (Suc (n - 1))" by auto lemma mpl_lem: "j \ i \ k < j \ i - j + k < i" for i j k :: nat by arith lemmas dme = div_mult_mod_eq lemmas dtle = div_times_less_eq_dividend lemmas th2 = order_trans [OF order_refl [THEN [2] mult_le_mono] div_times_less_eq_dividend] lemmas sdl = div_nat_eqI lemma given_quot: "f > 0 \ (f * l + (f - 1)) div f = l" for f l :: nat by (rule div_nat_eqI) (simp_all) lemma given_quot_alt: "f > 0 \ (l * f + f - Suc 0) div f = l" for f l :: nat apply (frule given_quot) apply (rule trans) prefer 2 apply (erule asm_rl) apply (rule_tac f="\n. n div f" in arg_cong) apply (simp add : ac_simps) done lemma x_power_minus_1: fixes x :: "'a :: {ab_group_add, power, numeral, one}" shows "x + (2::'a) ^ n - (1::'a) = x + (2 ^ n - 1)" by simp lemma nat_diff_add: fixes i :: nat shows "\ i + j = k \ \ i = k - j" by arith lemma pow_2_gt: "n \ 2 \ (2::int) < 2 ^ n" by (induct n) auto lemma sum_to_zero: "(a :: 'a :: ring) + b = 0 \ a = (- b)" by (drule arg_cong[where f="\ x. x - a"], simp) lemma arith_is_1: "\ x \ Suc 0; x > 0 \ \ x = 1" by arith lemma suc_le_pow_2: "1 < (n::nat) \ Suc n < 2 ^ n" by (induct n; clarsimp) (case_tac "n = 1"; clarsimp) lemma nat_le_Suc_less_imp: "x < y \ x \ y - Suc 0" by arith lemma power_sub_int: "\ m \ n; 0 < b \ \ b ^ n div b ^ m = (b ^ (n - m) :: int)" apply (subgoal_tac "\n'. n = m + n'") apply (clarsimp simp: power_add) apply (rule exI[where x="n - m"]) apply simp done lemma nat_Suc_less_le_imp: "(k::nat) < Suc n \ k \ n" by auto lemma nat_add_less_by_max: "\ (x::nat) \ xmax ; y < k - xmax \ \ x + y < k" by simp lemma nat_le_Suc_less: "0 < y \ (x \ y - Suc 0) = (x < y)" by arith lemma nat_power_minus_less: "a < 2 ^ (x - n) \ (a :: nat) < 2 ^ x" by (erule order_less_le_trans) simp lemma less_le_mult_nat': "w * c < b * c ==> 0 \ c ==> Suc w * c \ b * (c::nat)" apply (rule mult_right_mono) apply (rule Suc_leI) apply (erule (1) mult_right_less_imp_less) apply assumption done lemma less_le_mult_nat: \0 < c \ w < b \ c + w * c \ b * c\ for b c w :: nat using less_le_mult_nat' [of w c b] by simp lemma p_assoc_help: fixes p :: "'a::{ring,power,numeral,one}" shows "p + 2^sz - 1 = p + (2^sz - 1)" by simp lemma pow_mono_leq_imp_lt: "x \ y \ x < 2 ^ y" by (simp add: le_less_trans) lemma small_powers_of_2: "x \ 3 \ x < 2 ^ (x - 1)" by (induct x; simp add: suc_le_pow_2) lemma nat_less_power_trans2: fixes n :: nat shows "\n < 2 ^ (m - k); k \ m\ \ n * 2 ^ k < 2 ^ m" by (subst mult.commute, erule (1) nat_less_power_trans) lemma nat_move_sub_le: "(a::nat) + b \ c \ a \ c - b" by arith lemma plus_minus_one_rewrite: "v + (- 1 :: ('a :: {ring, one, uminus})) \ v - 1" by (simp add: field_simps) lemma Suc_0_lt_2p_len_of: "Suc 0 < 2 ^ LENGTH('a :: len)" by (metis One_nat_def len_gt_0 lessI numeral_2_eq_2 one_less_power) +lemma bin_rest_code: "i div 2 = drop_bit 1 i" for i :: int + by (simp add: drop_bit_eq_div) + end