diff --git a/src/HOL/Code_Numeral.thy b/src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy +++ b/src/HOL/Code_Numeral.thy @@ -1,1180 +1,1180 @@ (* Title: HOL/Code_Numeral.thy Author: Florian Haftmann, TU Muenchen *) section \Numeric types for code generation onto target language numerals only\ theory Code_Numeral imports Divides Lifting begin subsection \Type of target language integers\ typedef integer = "UNIV :: int set" morphisms int_of_integer integer_of_int .. setup_lifting type_definition_integer lemma integer_eq_iff: "k = l \ int_of_integer k = int_of_integer l" by transfer rule lemma integer_eqI: "int_of_integer k = int_of_integer l \ k = l" using integer_eq_iff [of k l] by simp lemma int_of_integer_integer_of_int [simp]: "int_of_integer (integer_of_int k) = k" by transfer rule lemma integer_of_int_int_of_integer [simp]: "integer_of_int (int_of_integer k) = k" by transfer rule instantiation integer :: ring_1 begin lift_definition zero_integer :: integer is "0 :: int" . declare zero_integer.rep_eq [simp] lift_definition one_integer :: integer is "1 :: int" . declare one_integer.rep_eq [simp] lift_definition plus_integer :: "integer \ integer \ integer" is "plus :: int \ int \ int" . declare plus_integer.rep_eq [simp] lift_definition uminus_integer :: "integer \ integer" is "uminus :: int \ int" . declare uminus_integer.rep_eq [simp] lift_definition minus_integer :: "integer \ integer \ integer" is "minus :: int \ int \ int" . declare minus_integer.rep_eq [simp] lift_definition times_integer :: "integer \ integer \ integer" is "times :: int \ int \ int" . declare times_integer.rep_eq [simp] instance proof qed (transfer, simp add: algebra_simps)+ end instance integer :: Rings.dvd .. context includes lifting_syntax notes transfer_rule_numeral [transfer_rule] begin lemma [transfer_rule]: "(pcr_integer ===> pcr_integer ===> (\)) (dvd) (dvd)" by (unfold dvd_def) transfer_prover lemma [transfer_rule]: "((\) ===> pcr_integer) of_bool of_bool" by (unfold of_bool_def [abs_def]) transfer_prover lemma [transfer_rule]: "((=) ===> pcr_integer) int of_nat" by (rule transfer_rule_of_nat) transfer_prover+ lemma [transfer_rule]: "((=) ===> pcr_integer) (\k. k) of_int" proof - have "((=) ===> pcr_integer) of_int of_int" by (rule transfer_rule_of_int) transfer_prover+ then show ?thesis by (simp add: id_def) qed lemma [transfer_rule]: "((=) ===> pcr_integer) numeral numeral" by transfer_prover lemma [transfer_rule]: "((=) ===> (=) ===> pcr_integer) Num.sub Num.sub" by (unfold Num.sub_def [abs_def]) transfer_prover lemma [transfer_rule]: "(pcr_integer ===> (=) ===> pcr_integer) (^) (^)" by (unfold power_def [abs_def]) transfer_prover end lemma int_of_integer_of_nat [simp]: "int_of_integer (of_nat n) = of_nat n" by transfer rule lift_definition integer_of_nat :: "nat \ integer" is "of_nat :: nat \ int" . lemma integer_of_nat_eq_of_nat [code]: "integer_of_nat = of_nat" by transfer rule lemma int_of_integer_integer_of_nat [simp]: "int_of_integer (integer_of_nat n) = of_nat n" by transfer rule lift_definition nat_of_integer :: "integer \ nat" is Int.nat . lemma nat_of_integer_of_nat [simp]: "nat_of_integer (of_nat n) = n" by transfer simp lemma int_of_integer_of_int [simp]: "int_of_integer (of_int k) = k" by transfer simp lemma nat_of_integer_integer_of_nat [simp]: "nat_of_integer (integer_of_nat n) = n" by transfer simp lemma integer_of_int_eq_of_int [simp, code_abbrev]: "integer_of_int = of_int" by transfer (simp add: fun_eq_iff) lemma of_int_integer_of [simp]: "of_int (int_of_integer k) = (k :: integer)" by transfer rule lemma int_of_integer_numeral [simp]: "int_of_integer (numeral k) = numeral k" by transfer rule lemma int_of_integer_sub [simp]: "int_of_integer (Num.sub k l) = Num.sub k l" by transfer rule definition integer_of_num :: "num \ integer" where [simp]: "integer_of_num = numeral" lemma integer_of_num [code]: "integer_of_num Num.One = 1" "integer_of_num (Num.Bit0 n) = (let k = integer_of_num n in k + k)" "integer_of_num (Num.Bit1 n) = (let k = integer_of_num n in k + k + 1)" by (simp_all only: integer_of_num_def numeral.simps Let_def) lemma integer_of_num_triv: "integer_of_num Num.One = 1" "integer_of_num (Num.Bit0 Num.One) = 2" by simp_all instantiation integer :: "{linordered_idom, equal}" begin lift_definition abs_integer :: "integer \ integer" is "abs :: int \ int" . declare abs_integer.rep_eq [simp] lift_definition sgn_integer :: "integer \ integer" is "sgn :: int \ int" . declare sgn_integer.rep_eq [simp] lift_definition less_eq_integer :: "integer \ integer \ bool" is "less_eq :: int \ int \ bool" . lemma integer_less_eq_iff: "k \ l \ int_of_integer k \ int_of_integer l" by (fact less_eq_integer.rep_eq) lift_definition less_integer :: "integer \ integer \ bool" is "less :: int \ int \ bool" . lemma integer_less_iff: "k < l \ int_of_integer k < int_of_integer l" by (fact less_integer.rep_eq) lift_definition equal_integer :: "integer \ integer \ bool" is "HOL.equal :: int \ int \ bool" . instance by standard (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] mult_strict_right_mono linear)+ end lemma [transfer_rule]: "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (min :: _ \ _ \ int) (min :: _ \ _ \ integer)" by (unfold min_def [abs_def]) transfer_prover lemma [transfer_rule]: "rel_fun pcr_integer (rel_fun pcr_integer pcr_integer) (max :: _ \ _ \ int) (max :: _ \ _ \ integer)" by (unfold max_def [abs_def]) transfer_prover lemma int_of_integer_min [simp]: "int_of_integer (min k l) = min (int_of_integer k) (int_of_integer l)" by transfer rule lemma int_of_integer_max [simp]: "int_of_integer (max k l) = max (int_of_integer k) (int_of_integer l)" by transfer rule lemma nat_of_integer_non_positive [simp]: "k \ 0 \ nat_of_integer k = 0" by transfer simp lemma of_nat_of_integer [simp]: "of_nat (nat_of_integer k) = max 0 k" by transfer auto instantiation integer :: unique_euclidean_ring begin lift_definition divide_integer :: "integer \ integer \ integer" is "divide :: int \ int \ int" . declare divide_integer.rep_eq [simp] lift_definition modulo_integer :: "integer \ integer \ integer" is "modulo :: int \ int \ int" . declare modulo_integer.rep_eq [simp] lift_definition euclidean_size_integer :: "integer \ nat" is "euclidean_size :: int \ nat" . declare euclidean_size_integer.rep_eq [simp] lift_definition division_segment_integer :: "integer \ integer" is "division_segment :: int \ int" . declare division_segment_integer.rep_eq [simp] instance by (standard; transfer) (use mult_le_mono2 [of 1] in \auto simp add: sgn_mult_abs abs_mult sgn_mult abs_mod_less sgn_mod nat_mult_distrib division_segment_mult division_segment_mod intro: div_eqI\) end lemma [code]: "euclidean_size = nat_of_integer \ abs" by (simp add: fun_eq_iff nat_of_integer.rep_eq) lemma [code]: "division_segment (k :: integer) = (if k \ 0 then 1 else - 1)" by transfer (simp add: division_segment_int_def) instance integer :: unique_euclidean_ring_with_nat by (standard; transfer) (simp_all add: of_nat_div division_segment_int_def) instantiation integer :: semiring_bit_shifts begin lift_definition push_bit_integer :: \nat \ integer \ integer\ is \push_bit\ . lift_definition drop_bit_integer :: \nat \ integer \ integer\ is \drop_bit\ . instance by (standard; transfer) - (fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div - bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2 + (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div + bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2 exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+ end lemma [transfer_rule]: "rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \ _ \ int) (take_bit :: _ \ _ \ integer)" by (unfold take_bit_eq_mod [abs_def]) transfer_prover instance integer :: unique_euclidean_semiring_with_bit_shifts .. lemma [code]: \push_bit n k = k * 2 ^ n\ \drop_bit n k = k div 2 ^ n\ for k :: integer by (fact push_bit_eq_mult drop_bit_eq_div)+ instantiation integer :: unique_euclidean_semiring_numeral begin definition divmod_integer :: "num \ num \ integer \ integer" where divmod_integer'_def: "divmod_integer m n = (numeral m div numeral n, numeral m mod numeral n)" definition divmod_step_integer :: "num \ integer \ integer \ integer \ integer" where "divmod_step_integer l qr = (let (q, r) = qr in if r \ numeral l then (2 * q + 1, r - numeral l) else (2 * q, r))" instance proof show "divmod m n = (numeral m div numeral n :: integer, numeral m mod numeral n)" for m n by (fact divmod_integer'_def) show "divmod_step l qr = (let (q, r) = qr in if r \ numeral l then (2 * q + 1, r - numeral l) else (2 * q, r))" for l and qr :: "integer \ integer" by (fact divmod_step_integer_def) qed (transfer, fact le_add_diff_inverse2 unique_euclidean_semiring_numeral_class.div_less unique_euclidean_semiring_numeral_class.mod_less unique_euclidean_semiring_numeral_class.div_positive unique_euclidean_semiring_numeral_class.mod_less_eq_dividend unique_euclidean_semiring_numeral_class.pos_mod_bound unique_euclidean_semiring_numeral_class.pos_mod_sign unique_euclidean_semiring_numeral_class.mod_mult2_eq unique_euclidean_semiring_numeral_class.div_mult2_eq unique_euclidean_semiring_numeral_class.discrete)+ end declare divmod_algorithm_code [where ?'a = integer, folded integer_of_num_def, unfolded integer_of_num_triv, code] lemma integer_of_nat_0: "integer_of_nat 0 = 0" by transfer simp lemma integer_of_nat_1: "integer_of_nat 1 = 1" by transfer simp lemma integer_of_nat_numeral: "integer_of_nat (numeral n) = numeral n" by transfer simp subsection \Code theorems for target language integers\ text \Constructors\ definition Pos :: "num \ integer" where [simp, code_post]: "Pos = numeral" lemma [transfer_rule]: "rel_fun HOL.eq pcr_integer numeral Pos" by simp transfer_prover lemma Pos_fold [code_unfold]: "numeral Num.One = Pos Num.One" "numeral (Num.Bit0 k) = Pos (Num.Bit0 k)" "numeral (Num.Bit1 k) = Pos (Num.Bit1 k)" by simp_all definition Neg :: "num \ integer" where [simp, code_abbrev]: "Neg n = - Pos n" lemma [transfer_rule]: "rel_fun HOL.eq pcr_integer (\n. - numeral n) Neg" by (simp add: Neg_def [abs_def]) transfer_prover code_datatype "0::integer" Pos Neg text \A further pair of constructors for generated computations\ context begin qualified definition positive :: "num \ integer" where [simp]: "positive = numeral" qualified definition negative :: "num \ integer" where [simp]: "negative = uminus \ numeral" lemma [code_computation_unfold]: "numeral = positive" "Pos = positive" "Neg = negative" by (simp_all add: fun_eq_iff) end text \Auxiliary operations\ lift_definition dup :: "integer \ integer" is "\k::int. k + k" . lemma dup_code [code]: "dup 0 = 0" "dup (Pos n) = Pos (Num.Bit0 n)" "dup (Neg n) = Neg (Num.Bit0 n)" by (transfer, simp only: numeral_Bit0 minus_add_distrib)+ lift_definition sub :: "num \ num \ integer" is "\m n. numeral m - numeral n :: int" . lemma sub_code [code]: "sub Num.One Num.One = 0" "sub (Num.Bit0 m) Num.One = Pos (Num.BitM m)" "sub (Num.Bit1 m) Num.One = Pos (Num.Bit0 m)" "sub Num.One (Num.Bit0 n) = Neg (Num.BitM n)" "sub Num.One (Num.Bit1 n) = Neg (Num.Bit0 n)" "sub (Num.Bit0 m) (Num.Bit0 n) = dup (sub m n)" "sub (Num.Bit1 m) (Num.Bit1 n) = dup (sub m n)" "sub (Num.Bit1 m) (Num.Bit0 n) = dup (sub m n) + 1" "sub (Num.Bit0 m) (Num.Bit1 n) = dup (sub m n) - 1" by (transfer, simp add: dbl_def dbl_inc_def dbl_dec_def)+ text \Implementations\ lemma one_integer_code [code, code_unfold]: "1 = Pos Num.One" by simp lemma plus_integer_code [code]: "k + 0 = (k::integer)" "0 + l = (l::integer)" "Pos m + Pos n = Pos (m + n)" "Pos m + Neg n = sub m n" "Neg m + Pos n = sub n m" "Neg m + Neg n = Neg (m + n)" by (transfer, simp)+ lemma uminus_integer_code [code]: "uminus 0 = (0::integer)" "uminus (Pos m) = Neg m" "uminus (Neg m) = Pos m" by simp_all lemma minus_integer_code [code]: "k - 0 = (k::integer)" "0 - l = uminus (l::integer)" "Pos m - Pos n = sub m n" "Pos m - Neg n = Pos (m + n)" "Neg m - Pos n = Neg (m + n)" "Neg m - Neg n = sub n m" by (transfer, simp)+ lemma abs_integer_code [code]: "\k\ = (if (k::integer) < 0 then - k else k)" by simp lemma sgn_integer_code [code]: "sgn k = (if k = 0 then 0 else if (k::integer) < 0 then - 1 else 1)" by simp lemma times_integer_code [code]: "k * 0 = (0::integer)" "0 * l = (0::integer)" "Pos m * Pos n = Pos (m * n)" "Pos m * Neg n = Neg (m * n)" "Neg m * Pos n = Neg (m * n)" "Neg m * Neg n = Pos (m * n)" by simp_all definition divmod_integer :: "integer \ integer \ integer \ integer" where "divmod_integer k l = (k div l, k mod l)" lemma fst_divmod_integer [simp]: "fst (divmod_integer k l) = k div l" by (simp add: divmod_integer_def) lemma snd_divmod_integer [simp]: "snd (divmod_integer k l) = k mod l" by (simp add: divmod_integer_def) definition divmod_abs :: "integer \ integer \ integer \ integer" where "divmod_abs k l = (\k\ div \l\, \k\ mod \l\)" lemma fst_divmod_abs [simp]: "fst (divmod_abs k l) = \k\ div \l\" by (simp add: divmod_abs_def) lemma snd_divmod_abs [simp]: "snd (divmod_abs k l) = \k\ mod \l\" by (simp add: divmod_abs_def) lemma divmod_abs_code [code]: "divmod_abs (Pos k) (Pos l) = divmod k l" "divmod_abs (Neg k) (Neg l) = divmod k l" "divmod_abs (Neg k) (Pos l) = divmod k l" "divmod_abs (Pos k) (Neg l) = divmod k l" "divmod_abs j 0 = (0, \j\)" "divmod_abs 0 j = (0, 0)" by (simp_all add: prod_eq_iff) lemma divmod_integer_eq_cases: "divmod_integer k l = (if k = 0 then (0, 0) else if l = 0 then (0, k) else (apsnd \ times \ sgn) l (if sgn k = sgn l then divmod_abs k l else (let (r, s) = divmod_abs k l in if s = 0 then (- r, 0) else (- r - 1, \l\ - s))))" proof - have *: "sgn k = sgn l \ k = 0 \ l = 0 \ 0 < l \ 0 < k \ l < 0 \ k < 0" for k l :: int by (auto simp add: sgn_if) have **: "- k = l * q \ k = - (l * q)" for k l q :: int by auto show ?thesis by (simp add: divmod_integer_def divmod_abs_def) (transfer, auto simp add: * ** not_less zdiv_zminus1_eq_if zmod_zminus1_eq_if div_minus_right mod_minus_right) qed lemma divmod_integer_code [code]: \<^marker>\contributor \René Thiemann\\ \<^marker>\contributor \Akihisa Yamada\\ "divmod_integer k l = (if k = 0 then (0, 0) else if l > 0 then (if k > 0 then Code_Numeral.divmod_abs k l else case Code_Numeral.divmod_abs k l of (r, s) \ if s = 0 then (- r, 0) else (- r - 1, l - s)) else if l = 0 then (0, k) else apsnd uminus (if k < 0 then Code_Numeral.divmod_abs k l else case Code_Numeral.divmod_abs k l of (r, s) \ if s = 0 then (- r, 0) else (- r - 1, - l - s)))" by (cases l "0 :: integer" rule: linorder_cases) (auto split: prod.splits simp add: divmod_integer_eq_cases) lemma div_integer_code [code]: "k div l = fst (divmod_integer k l)" by simp lemma mod_integer_code [code]: "k mod l = snd (divmod_integer k l)" by simp definition bit_cut_integer :: "integer \ integer \ bool" where "bit_cut_integer k = (k div 2, odd k)" lemma bit_cut_integer_code [code]: "bit_cut_integer k = (if k = 0 then (0, False) else let (r, s) = Code_Numeral.divmod_abs k 2 in (if k > 0 then r else - r - s, s = 1))" proof - have "bit_cut_integer k = (let (r, s) = divmod_integer k 2 in (r, s = 1))" by (simp add: divmod_integer_def bit_cut_integer_def odd_iff_mod_2_eq_one) then show ?thesis by (simp add: divmod_integer_code) (auto simp add: split_def) qed lemma equal_integer_code [code]: "HOL.equal 0 (0::integer) \ True" "HOL.equal 0 (Pos l) \ False" "HOL.equal 0 (Neg l) \ False" "HOL.equal (Pos k) 0 \ False" "HOL.equal (Pos k) (Pos l) \ HOL.equal k l" "HOL.equal (Pos k) (Neg l) \ False" "HOL.equal (Neg k) 0 \ False" "HOL.equal (Neg k) (Pos l) \ False" "HOL.equal (Neg k) (Neg l) \ HOL.equal k l" by (simp_all add: equal) lemma equal_integer_refl [code nbe]: "HOL.equal (k::integer) k \ True" by (fact equal_refl) lemma less_eq_integer_code [code]: "0 \ (0::integer) \ True" "0 \ Pos l \ True" "0 \ Neg l \ False" "Pos k \ 0 \ False" "Pos k \ Pos l \ k \ l" "Pos k \ Neg l \ False" "Neg k \ 0 \ True" "Neg k \ Pos l \ True" "Neg k \ Neg l \ l \ k" by simp_all lemma less_integer_code [code]: "0 < (0::integer) \ False" "0 < Pos l \ True" "0 < Neg l \ False" "Pos k < 0 \ False" "Pos k < Pos l \ k < l" "Pos k < Neg l \ False" "Neg k < 0 \ True" "Neg k < Pos l \ True" "Neg k < Neg l \ l < k" by simp_all lift_definition num_of_integer :: "integer \ num" is "num_of_nat \ nat" . lemma num_of_integer_code [code]: "num_of_integer k = (if k \ 1 then Num.One else let (l, j) = divmod_integer k 2; l' = num_of_integer l; l'' = l' + l' in if j = 0 then l'' else l'' + Num.One)" proof - { assume "int_of_integer k mod 2 = 1" then have "nat (int_of_integer k mod 2) = nat 1" by simp moreover assume *: "1 < int_of_integer k" ultimately have **: "nat (int_of_integer k) mod 2 = 1" by (simp add: nat_mod_distrib) have "num_of_nat (nat (int_of_integer k)) = num_of_nat (2 * (nat (int_of_integer k) div 2) + nat (int_of_integer k) mod 2)" by simp then have "num_of_nat (nat (int_of_integer k)) = num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + nat (int_of_integer k) mod 2)" by (simp add: mult_2) with ** have "num_of_nat (nat (int_of_integer k)) = num_of_nat (nat (int_of_integer k) div 2 + nat (int_of_integer k) div 2 + 1)" by simp } note aux = this show ?thesis by (auto simp add: num_of_integer_def nat_of_integer_def Let_def case_prod_beta not_le integer_eq_iff less_eq_integer_def nat_mult_distrib nat_div_distrib num_of_nat_One num_of_nat_plus_distrib mult_2 [where 'a=nat] aux add_One) qed lemma nat_of_integer_code [code]: "nat_of_integer k = (if k \ 0 then 0 else let (l, j) = divmod_integer k 2; l' = nat_of_integer l; l'' = l' + l' in if j = 0 then l'' else l'' + 1)" proof - obtain j where k: "k = integer_of_int j" proof show "k = integer_of_int (int_of_integer k)" by simp qed have *: "nat j mod 2 = nat_of_integer (of_int j mod 2)" if "j \ 0" using that by transfer (simp add: nat_mod_distrib) from k show ?thesis by (auto simp add: split_def Let_def nat_of_integer_def nat_div_distrib mult_2 [symmetric] minus_mod_eq_mult_div [symmetric] *) qed lemma int_of_integer_code [code]: "int_of_integer k = (if k < 0 then - (int_of_integer (- k)) else if k = 0 then 0 else let (l, j) = divmod_integer k 2; l' = 2 * int_of_integer l in if j = 0 then l' else l' + 1)" by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric]) lemma integer_of_int_code [code]: "integer_of_int k = (if k < 0 then - (integer_of_int (- k)) else if k = 0 then 0 else let l = 2 * integer_of_int (k div 2); j = k mod 2 in if j = 0 then l else l + 1)" by (auto simp add: split_def Let_def integer_eq_iff minus_mod_eq_mult_div [symmetric]) hide_const (open) Pos Neg sub dup divmod_abs subsection \Serializer setup for target language integers\ code_reserved Eval int Integer abs code_printing type_constructor integer \ (SML) "IntInf.int" and (OCaml) "Z.t" and (Haskell) "Integer" and (Scala) "BigInt" and (Eval) "int" | class_instance integer :: equal \ (Haskell) - code_printing constant "0::integer" \ (SML) "!(0/ :/ IntInf.int)" and (OCaml) "Z.zero" and (Haskell) "!(0/ ::/ Integer)" and (Scala) "BigInt(0)" setup \ fold (fn target => Numeral.add_code \<^const_name>\Code_Numeral.Pos\ I Code_Printer.literal_numeral target #> Numeral.add_code \<^const_name>\Code_Numeral.Neg\ (~) Code_Printer.literal_numeral target) ["SML", "OCaml", "Haskell", "Scala"] \ code_printing constant "plus :: integer \ _ \ _" \ (SML) "IntInf.+ ((_), (_))" and (OCaml) "Z.add" and (Haskell) infixl 6 "+" and (Scala) infixl 7 "+" and (Eval) infixl 8 "+" | constant "uminus :: integer \ _" \ (SML) "IntInf.~" and (OCaml) "Z.neg" and (Haskell) "negate" and (Scala) "!(- _)" and (Eval) "~/ _" | constant "minus :: integer \ _" \ (SML) "IntInf.- ((_), (_))" and (OCaml) "Z.sub" and (Haskell) infixl 6 "-" and (Scala) infixl 7 "-" and (Eval) infixl 8 "-" | constant Code_Numeral.dup \ (SML) "IntInf.*/ (2,/ (_))" and (OCaml) "Z.shift'_left/ _/ 1" and (Haskell) "!(2 * _)" and (Scala) "!(2 * _)" and (Eval) "!(2 * _)" | constant Code_Numeral.sub \ (SML) "!(raise/ Fail/ \"sub\")" and (OCaml) "failwith/ \"sub\"" and (Haskell) "error/ \"sub\"" and (Scala) "!sys.error(\"sub\")" | constant "times :: integer \ _ \ _" \ (SML) "IntInf.* ((_), (_))" and (OCaml) "Z.mul" and (Haskell) infixl 7 "*" and (Scala) infixl 8 "*" and (Eval) infixl 9 "*" | constant Code_Numeral.divmod_abs \ (SML) "IntInf.divMod/ (IntInf.abs _,/ IntInf.abs _)" and (OCaml) "!(fun k l ->/ if Z.equal Z.zero l then/ (Z.zero, l) else/ Z.div'_rem/ (Z.abs k)/ (Z.abs l))" and (Haskell) "divMod/ (abs _)/ (abs _)" and (Scala) "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))" and (Eval) "Integer.div'_mod/ (abs _)/ (abs _)" | constant "HOL.equal :: integer \ _ \ bool" \ (SML) "!((_ : IntInf.int) = _)" and (OCaml) "Z.equal" and (Haskell) infix 4 "==" and (Scala) infixl 5 "==" and (Eval) infixl 6 "=" | constant "less_eq :: integer \ _ \ bool" \ (SML) "IntInf.<= ((_), (_))" and (OCaml) "Z.leq" and (Haskell) infix 4 "<=" and (Scala) infixl 4 "<=" and (Eval) infixl 6 "<=" | constant "less :: integer \ _ \ bool" \ (SML) "IntInf.< ((_), (_))" and (OCaml) "Z.lt" and (Haskell) infix 4 "<" and (Scala) infixl 4 "<" and (Eval) infixl 6 "<" | constant "abs :: integer \ _" \ (SML) "IntInf.abs" and (OCaml) "Z.abs" and (Haskell) "Prelude.abs" and (Scala) "_.abs" and (Eval) "abs" code_identifier code_module Code_Numeral \ (SML) Arith and (OCaml) Arith and (Haskell) Arith subsection \Type of target language naturals\ typedef natural = "UNIV :: nat set" morphisms nat_of_natural natural_of_nat .. setup_lifting type_definition_natural lemma natural_eq_iff [termination_simp]: "m = n \ nat_of_natural m = nat_of_natural n" by transfer rule lemma natural_eqI: "nat_of_natural m = nat_of_natural n \ m = n" using natural_eq_iff [of m n] by simp lemma nat_of_natural_of_nat_inverse [simp]: "nat_of_natural (natural_of_nat n) = n" by transfer rule lemma natural_of_nat_of_natural_inverse [simp]: "natural_of_nat (nat_of_natural n) = n" by transfer rule instantiation natural :: "{comm_monoid_diff, semiring_1}" begin lift_definition zero_natural :: natural is "0 :: nat" . declare zero_natural.rep_eq [simp] lift_definition one_natural :: natural is "1 :: nat" . declare one_natural.rep_eq [simp] lift_definition plus_natural :: "natural \ natural \ natural" is "plus :: nat \ nat \ nat" . declare plus_natural.rep_eq [simp] lift_definition minus_natural :: "natural \ natural \ natural" is "minus :: nat \ nat \ nat" . declare minus_natural.rep_eq [simp] lift_definition times_natural :: "natural \ natural \ natural" is "times :: nat \ nat \ nat" . declare times_natural.rep_eq [simp] instance proof qed (transfer, simp add: algebra_simps)+ end instance natural :: Rings.dvd .. lemma [transfer_rule]: "rel_fun pcr_natural (rel_fun pcr_natural HOL.iff) Rings.dvd Rings.dvd" unfolding dvd_def by transfer_prover lemma [transfer_rule]: "rel_fun (=) pcr_natural (of_bool :: bool \ nat) (of_bool :: bool \ natural)" by (unfold of_bool_def [abs_def]) transfer_prover lemma [transfer_rule]: "rel_fun HOL.eq pcr_natural (\n::nat. n) (of_nat :: nat \ natural)" proof - have "rel_fun HOL.eq pcr_natural (of_nat :: nat \ nat) (of_nat :: nat \ natural)" by (unfold of_nat_def [abs_def]) transfer_prover then show ?thesis by (simp add: id_def) qed lemma [transfer_rule]: "rel_fun HOL.eq pcr_natural (numeral :: num \ nat) (numeral :: num \ natural)" proof - have "rel_fun HOL.eq pcr_natural (numeral :: num \ nat) (\n. of_nat (numeral n))" by transfer_prover then show ?thesis by simp qed lemma [transfer_rule]: "rel_fun pcr_natural (rel_fun (=) pcr_natural) (power :: _ \ _ \ nat) (power :: _ \ _ \ natural)" by (unfold power_def [abs_def]) transfer_prover lemma nat_of_natural_of_nat [simp]: "nat_of_natural (of_nat n) = n" by transfer rule lemma natural_of_nat_of_nat [simp, code_abbrev]: "natural_of_nat = of_nat" by transfer rule lemma of_nat_of_natural [simp]: "of_nat (nat_of_natural n) = n" by transfer rule lemma nat_of_natural_numeral [simp]: "nat_of_natural (numeral k) = numeral k" by transfer rule instantiation natural :: "{linordered_semiring, equal}" begin lift_definition less_eq_natural :: "natural \ natural \ bool" is "less_eq :: nat \ nat \ bool" . declare less_eq_natural.rep_eq [termination_simp] lift_definition less_natural :: "natural \ natural \ bool" is "less :: nat \ nat \ bool" . declare less_natural.rep_eq [termination_simp] lift_definition equal_natural :: "natural \ natural \ bool" is "HOL.equal :: nat \ nat \ bool" . instance proof qed (transfer, simp add: algebra_simps equal less_le_not_le [symmetric] linear)+ end lemma [transfer_rule]: "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (min :: _ \ _ \ nat) (min :: _ \ _ \ natural)" by (unfold min_def [abs_def]) transfer_prover lemma [transfer_rule]: "rel_fun pcr_natural (rel_fun pcr_natural pcr_natural) (max :: _ \ _ \ nat) (max :: _ \ _ \ natural)" by (unfold max_def [abs_def]) transfer_prover lemma nat_of_natural_min [simp]: "nat_of_natural (min k l) = min (nat_of_natural k) (nat_of_natural l)" by transfer rule lemma nat_of_natural_max [simp]: "nat_of_natural (max k l) = max (nat_of_natural k) (nat_of_natural l)" by transfer rule instantiation natural :: unique_euclidean_semiring begin lift_definition divide_natural :: "natural \ natural \ natural" is "divide :: nat \ nat \ nat" . declare divide_natural.rep_eq [simp] lift_definition modulo_natural :: "natural \ natural \ natural" is "modulo :: nat \ nat \ nat" . declare modulo_natural.rep_eq [simp] lift_definition euclidean_size_natural :: "natural \ nat" is "euclidean_size :: nat \ nat" . declare euclidean_size_natural.rep_eq [simp] lift_definition division_segment_natural :: "natural \ natural" is "division_segment :: nat \ nat" . declare division_segment_natural.rep_eq [simp] instance by (standard; transfer) (auto simp add: algebra_simps unit_factor_nat_def gr0_conv_Suc) end lemma [code]: "euclidean_size = nat_of_natural" by (simp add: fun_eq_iff) lemma [code]: "division_segment (n::natural) = 1" by (simp add: natural_eq_iff) instance natural :: linordered_semidom by (standard; transfer) simp_all instance natural :: unique_euclidean_semiring_with_nat by (standard; transfer) simp_all instantiation natural :: semiring_bit_shifts begin lift_definition push_bit_natural :: \nat \ natural \ natural\ is \push_bit\ . lift_definition drop_bit_natural :: \nat \ natural \ natural\ is \drop_bit\ . instance by (standard; transfer) - (fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div - bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2 + (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div + bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2 exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+ end lemma [transfer_rule]: "rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \ _ \ nat) (take_bit :: _ \ _ \ natural)" by (unfold take_bit_eq_mod [abs_def]) transfer_prover instance natural :: unique_euclidean_semiring_with_bit_shifts .. lemma [code]: \push_bit n m = m * 2 ^ n\ \drop_bit n m = m div 2 ^ n\ for m :: natural by (fact push_bit_eq_mult drop_bit_eq_div)+ lift_definition natural_of_integer :: "integer \ natural" is "nat :: int \ nat" . lift_definition integer_of_natural :: "natural \ integer" is "of_nat :: nat \ int" . lemma natural_of_integer_of_natural [simp]: "natural_of_integer (integer_of_natural n) = n" by transfer simp lemma integer_of_natural_of_integer [simp]: "integer_of_natural (natural_of_integer k) = max 0 k" by transfer auto lemma int_of_integer_of_natural [simp]: "int_of_integer (integer_of_natural n) = of_nat (nat_of_natural n)" by transfer rule lemma integer_of_natural_of_nat [simp]: "integer_of_natural (of_nat n) = of_nat n" by transfer rule lemma [measure_function]: "is_measure nat_of_natural" by (rule is_measure_trivial) subsection \Inductive representation of target language naturals\ lift_definition Suc :: "natural \ natural" is Nat.Suc . declare Suc.rep_eq [simp] old_rep_datatype "0::natural" Suc by (transfer, fact nat.induct nat.inject nat.distinct)+ lemma natural_cases [case_names nat, cases type: natural]: fixes m :: natural assumes "\n. m = of_nat n \ P" shows P using assms by transfer blast instantiation natural :: size begin definition size_nat where [simp, code]: "size_nat = nat_of_natural" instance .. end lemma natural_decr [termination_simp]: "n \ 0 \ nat_of_natural n - Nat.Suc 0 < nat_of_natural n" by transfer simp lemma natural_zero_minus_one: "(0::natural) - 1 = 0" by (rule zero_diff) lemma Suc_natural_minus_one: "Suc n - 1 = n" by transfer simp hide_const (open) Suc subsection \Code refinement for target language naturals\ lift_definition Nat :: "integer \ natural" is nat . lemma [code_post]: "Nat 0 = 0" "Nat 1 = 1" "Nat (numeral k) = numeral k" by (transfer, simp)+ lemma [code abstype]: "Nat (integer_of_natural n) = n" by transfer simp lemma [code]: "natural_of_nat n = natural_of_integer (integer_of_nat n)" by transfer simp lemma [code abstract]: "integer_of_natural (natural_of_integer k) = max 0 k" by simp lemma [code_abbrev]: "natural_of_integer (Code_Numeral.Pos k) = numeral k" by transfer simp lemma [code abstract]: "integer_of_natural 0 = 0" by transfer simp lemma [code abstract]: "integer_of_natural 1 = 1" by transfer simp lemma [code abstract]: "integer_of_natural (Code_Numeral.Suc n) = integer_of_natural n + 1" by transfer simp lemma [code]: "nat_of_natural = nat_of_integer \ integer_of_natural" by transfer (simp add: fun_eq_iff) lemma [code, code_unfold]: "case_natural f g n = (if n = 0 then f else g (n - 1))" by (cases n rule: natural.exhaust) (simp_all, simp add: Suc_def) declare natural.rec [code del] lemma [code abstract]: "integer_of_natural (m + n) = integer_of_natural m + integer_of_natural n" by transfer simp lemma [code abstract]: "integer_of_natural (m - n) = max 0 (integer_of_natural m - integer_of_natural n)" by transfer simp lemma [code abstract]: "integer_of_natural (m * n) = integer_of_natural m * integer_of_natural n" by transfer simp lemma [code abstract]: "integer_of_natural (m div n) = integer_of_natural m div integer_of_natural n" by transfer (simp add: zdiv_int) lemma [code abstract]: "integer_of_natural (m mod n) = integer_of_natural m mod integer_of_natural n" by transfer (simp add: zmod_int) lemma [code]: "HOL.equal m n \ HOL.equal (integer_of_natural m) (integer_of_natural n)" by transfer (simp add: equal) lemma [code nbe]: "HOL.equal n (n::natural) \ True" by (rule equal_class.equal_refl) lemma [code]: "m \ n \ integer_of_natural m \ integer_of_natural n" by transfer simp lemma [code]: "m < n \ integer_of_natural m < integer_of_natural n" by transfer simp hide_const (open) Nat lifting_update integer.lifting lifting_forget integer.lifting lifting_update natural.lifting lifting_forget natural.lifting code_reflect Code_Numeral datatypes natural functions "Code_Numeral.Suc" "0 :: natural" "1 :: natural" "plus :: natural \ _" "minus :: natural \ _" "times :: natural \ _" "divide :: natural \ _" "modulo :: natural \ _" integer_of_natural natural_of_integer end diff --git a/src/HOL/Library/Type_Length.thy b/src/HOL/Library/Type_Length.thy --- a/src/HOL/Library/Type_Length.thy +++ b/src/HOL/Library/Type_Length.thy @@ -1,106 +1,110 @@ (* Title: HOL/Library/Type_Length.thy Author: John Matthews, Galois Connections, Inc., Copyright 2006 *) section \Assigning lengths to types by type classes\ theory Type_Length imports Numeral_Type begin text \ The aim of this is to allow any type as index type, but to provide a default instantiation for numeral types. This independence requires some duplication with the definitions in \<^file>\Numeral_Type.thy\. \ class len0 = fixes len_of :: "'a itself \ nat" syntax "_type_length" :: "type \ nat" (\(1LENGTH/(1'(_')))\) translations "LENGTH('a)" \ "CONST len_of (CONST Pure.type :: 'a itself)" print_translation \ let fun len_of_itself_tr' ctxt [Const (\<^const_syntax>\Pure.type\, Type (_, [T]))] = Syntax.const \<^syntax_const>\_type_length\ $ Syntax_Phases.term_of_typ ctxt T in [(\<^const_syntax>\len_of\, len_of_itself_tr')] end \ text \Some theorems are only true on words with length greater 0.\ class len = len0 + assumes len_gt_0 [iff]: "0 < LENGTH('a)" begin lemma len_not_eq_0 [simp]: "LENGTH('a) \ 0" by simp end instantiation num0 and num1 :: len0 begin definition len_num0: "len_of (_ :: num0 itself) = 0" definition len_num1: "len_of (_ :: num1 itself) = 1" instance .. end instantiation bit0 and bit1 :: (len0) len0 begin definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * LENGTH('a)" definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * LENGTH('a) + 1" instance .. end lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1 instance num1 :: len by standard simp instance bit0 :: (len) len by standard simp instance bit1 :: (len0) len by standard simp instantiation Enum.finite_1 :: len begin definition "len_of_finite_1 (x :: Enum.finite_1 itself) \ (1 :: nat)" instance by standard (auto simp: len_of_finite_1_def) end instantiation Enum.finite_2 :: len begin definition "len_of_finite_2 (x :: Enum.finite_2 itself) \ (2 :: nat)" instance by standard (auto simp: len_of_finite_2_def) end instantiation Enum.finite_3 :: len begin definition "len_of_finite_3 (x :: Enum.finite_3 itself) \ (4 :: nat)" instance by standard (auto simp: len_of_finite_3_def) end +lemma length_not_greater_eq_2_iff [simp]: + \\ 2 \ LENGTH('a::len) \ LENGTH('a) = 1\ + by (auto simp add: not_le dest: less_2_cases) + end diff --git a/src/HOL/Parity.thy b/src/HOL/Parity.thy --- a/src/HOL/Parity.thy +++ b/src/HOL/Parity.thy @@ -1,1231 +1,1262 @@ (* Title: HOL/Parity.thy Author: Jeremy Avigad Author: Jacques D. Fleuriot *) section \Parity in rings and semirings\ theory Parity imports Euclidean_Division begin subsection \Ring structures with parity and \even\/\odd\ predicates\ class semiring_parity = comm_semiring_1 + semiring_modulo + assumes even_iff_mod_2_eq_zero: "2 dvd a \ a mod 2 = 0" and odd_iff_mod_2_eq_one: "\ 2 dvd a \ a mod 2 = 1" and odd_one [simp]: "\ 2 dvd 1" begin abbreviation even :: "'a \ bool" where "even a \ 2 dvd a" abbreviation odd :: "'a \ bool" where "odd a \ \ 2 dvd a" lemma parity_cases [case_names even odd]: assumes "even a \ a mod 2 = 0 \ P" assumes "odd a \ a mod 2 = 1 \ P" shows P using assms by (cases "even a") (simp_all add: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric]) lemma odd_of_bool_self [simp]: \odd (of_bool p) \ p\ by (cases p) simp_all lemma not_mod_2_eq_0_eq_1 [simp]: "a mod 2 \ 0 \ a mod 2 = 1" by (cases a rule: parity_cases) simp_all lemma not_mod_2_eq_1_eq_0 [simp]: "a mod 2 \ 1 \ a mod 2 = 0" by (cases a rule: parity_cases) simp_all lemma mod2_eq_if: "a mod 2 = (if 2 dvd a then 0 else 1)" by (simp add: even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one) lemma evenE [elim?]: assumes "even a" obtains b where "a = 2 * b" using assms by (rule dvdE) lemma oddE [elim?]: assumes "odd a" obtains b where "a = 2 * b + 1" proof - have "a = 2 * (a div 2) + a mod 2" by (simp add: mult_div_mod_eq) with assms have "a = 2 * (a div 2) + 1" by (simp add: odd_iff_mod_2_eq_one) then show ?thesis .. qed lemma mod_2_eq_odd: "a mod 2 = of_bool (odd a)" by (auto elim: oddE simp add: even_iff_mod_2_eq_zero) lemma of_bool_odd_eq_mod_2: "of_bool (odd a) = a mod 2" by (simp add: mod_2_eq_odd) lemma even_zero [simp]: "even 0" by (fact dvd_0_right) lemma odd_even_add: "even (a + b)" if "odd a" and "odd b" proof - from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1" by (blast elim: oddE) then have "a + b = 2 * c + 2 * d + (1 + 1)" by (simp only: ac_simps) also have "\ = 2 * (c + d + 1)" by (simp add: algebra_simps) finally show ?thesis .. qed lemma even_add [simp]: "even (a + b) \ (even a \ even b)" by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add) lemma odd_add [simp]: "odd (a + b) \ \ (odd a \ odd b)" by simp lemma even_plus_one_iff [simp]: "even (a + 1) \ odd a" by (auto simp add: dvd_add_right_iff intro: odd_even_add) lemma even_mult_iff [simp]: "even (a * b) \ even a \ even b" (is "?P \ ?Q") proof assume ?Q then show ?P by auto next assume ?P show ?Q proof (rule ccontr) assume "\ (even a \ even b)" then have "odd a" and "odd b" by auto then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1" by (blast elim: oddE) then have "a * b = (2 * r + 1) * (2 * s + 1)" by simp also have "\ = 2 * (2 * r * s + r + s) + 1" by (simp add: algebra_simps) finally have "odd (a * b)" by simp with \?P\ show False by auto qed qed lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))" proof - have "even (2 * numeral n)" unfolding even_mult_iff by simp then have "even (numeral n + numeral n)" unfolding mult_2 . then show ?thesis unfolding numeral.simps . qed lemma odd_numeral [simp]: "odd (numeral (Num.Bit1 n))" proof assume "even (numeral (num.Bit1 n))" then have "even (numeral n + numeral n + 1)" unfolding numeral.simps . then have "even (2 * numeral n + 1)" unfolding mult_2 . then have "2 dvd numeral n * 2 + 1" by (simp add: ac_simps) then have "2 dvd 1" using dvd_add_times_triv_left_iff [of 2 "numeral n" 1] by simp then show False by simp qed lemma even_power [simp]: "even (a ^ n) \ even a \ n > 0" by (induct n) auto end class ring_parity = ring + semiring_parity begin subclass comm_ring_1 .. lemma even_minus: "even (- a) \ even a" by (fact dvd_minus_iff) lemma even_diff [simp]: "even (a - b) \ even (a + b)" using even_add [of a "- b"] by simp end subsection \Special case: euclidean rings containing the natural numbers\ context unique_euclidean_semiring_with_nat begin subclass semiring_parity proof show "2 dvd a \ a mod 2 = 0" for a by (fact dvd_eq_mod_eq_0) show "\ 2 dvd a \ a mod 2 = 1" for a proof assume "a mod 2 = 1" then show "\ 2 dvd a" by auto next assume "\ 2 dvd a" have eucl: "euclidean_size (a mod 2) = 1" proof (rule order_antisym) show "euclidean_size (a mod 2) \ 1" using mod_size_less [of 2 a] by simp show "1 \ euclidean_size (a mod 2)" using \\ 2 dvd a\ by (simp add: Suc_le_eq dvd_eq_mod_eq_0) qed from \\ 2 dvd a\ have "\ of_nat 2 dvd division_segment a * of_nat (euclidean_size a)" by simp then have "\ of_nat 2 dvd of_nat (euclidean_size a)" by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment) then have "\ 2 dvd euclidean_size a" using of_nat_dvd_iff [of 2] by simp then have "euclidean_size a mod 2 = 1" by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0) then have "of_nat (euclidean_size a mod 2) = of_nat 1" by simp then have "of_nat (euclidean_size a) mod 2 = 1" by (simp add: of_nat_mod) from \\ 2 dvd a\ eucl show "a mod 2 = 1" by (auto intro: division_segment_eq_iff simp add: division_segment_mod) qed show "\ is_unit 2" proof (rule notI) assume "is_unit 2" then have "of_nat 2 dvd of_nat 1" by simp then have "is_unit (2::nat)" by (simp only: of_nat_dvd_iff) then show False by simp qed qed lemma even_of_nat [simp]: "even (of_nat a) \ even a" proof - have "even (of_nat a) \ of_nat 2 dvd of_nat a" by simp also have "\ \ even a" by (simp only: of_nat_dvd_iff) finally show ?thesis . qed lemma even_succ_div_two [simp]: "even a \ (a + 1) div 2 = a div 2" by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero) lemma odd_succ_div_two [simp]: "odd a \ (a + 1) div 2 = a div 2 + 1" by (auto elim!: oddE simp add: add.assoc) lemma even_two_times_div_two: "even a \ 2 * (a div 2) = a" by (fact dvd_mult_div_cancel) lemma odd_two_times_div_two_succ [simp]: "odd a \ 2 * (a div 2) + 1 = a" using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero) lemma coprime_left_2_iff_odd [simp]: "coprime 2 a \ odd a" proof assume "odd a" show "coprime 2 a" proof (rule coprimeI) fix b assume "b dvd 2" "b dvd a" then have "b dvd a mod 2" by (auto intro: dvd_mod) with \odd a\ show "is_unit b" by (simp add: mod_2_eq_odd) qed next assume "coprime 2 a" show "odd a" proof (rule notI) assume "even a" then obtain b where "a = 2 * b" .. with \coprime 2 a\ have "coprime 2 (2 * b)" by simp moreover have "\ coprime 2 (2 * b)" by (rule not_coprimeI [of 2]) simp_all ultimately show False by blast qed qed lemma coprime_right_2_iff_odd [simp]: "coprime a 2 \ odd a" using coprime_left_2_iff_odd [of a] by (simp add: ac_simps) end context unique_euclidean_ring_with_nat begin subclass ring_parity .. lemma minus_1_mod_2_eq [simp]: "- 1 mod 2 = 1" by (simp add: mod_2_eq_odd) lemma minus_1_div_2_eq [simp]: "- 1 div 2 = - 1" proof - from div_mult_mod_eq [of "- 1" 2] have "- 1 div 2 * 2 = - 1 * 2" using add_implies_diff by fastforce then show ?thesis using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp qed end subsection \Instance for \<^typ>\nat\\ instance nat :: unique_euclidean_semiring_with_nat by standard (simp_all add: dvd_eq_mod_eq_0) lemma even_Suc_Suc_iff [simp]: "even (Suc (Suc n)) \ even n" using dvd_add_triv_right_iff [of 2 n] by simp lemma even_Suc [simp]: "even (Suc n) \ odd n" using even_plus_one_iff [of n] by simp lemma even_diff_nat [simp]: "even (m - n) \ m < n \ even (m + n)" for m n :: nat proof (cases "n \ m") case True then have "m - n + n * 2 = m + n" by (simp add: mult_2_right) moreover have "even (m - n) \ even (m - n + n * 2)" by simp ultimately have "even (m - n) \ even (m + n)" by (simp only:) then show ?thesis by auto next case False then show ?thesis by simp qed lemma odd_pos: "odd n \ 0 < n" for n :: nat by (auto elim: oddE) lemma Suc_double_not_eq_double: "Suc (2 * m) \ 2 * n" proof assume "Suc (2 * m) = 2 * n" moreover have "odd (Suc (2 * m))" and "even (2 * n)" by simp_all ultimately show False by simp qed lemma double_not_eq_Suc_double: "2 * m \ Suc (2 * n)" using Suc_double_not_eq_double [of n m] by simp lemma odd_Suc_minus_one [simp]: "odd n \ Suc (n - Suc 0) = n" by (auto elim: oddE) lemma even_Suc_div_two [simp]: "even n \ Suc n div 2 = n div 2" using even_succ_div_two [of n] by simp lemma odd_Suc_div_two [simp]: "odd n \ Suc n div 2 = Suc (n div 2)" using odd_succ_div_two [of n] by simp lemma odd_two_times_div_two_nat [simp]: assumes "odd n" shows "2 * (n div 2) = n - (1 :: nat)" proof - from assms have "2 * (n div 2) + 1 = n" by (rule odd_two_times_div_two_succ) then have "Suc (2 * (n div 2)) - 1 = n - 1" by simp then show ?thesis by simp qed lemma not_mod2_eq_Suc_0_eq_0 [simp]: "n mod 2 \ Suc 0 \ n mod 2 = 0" using not_mod_2_eq_1_eq_0 [of n] by simp lemma odd_card_imp_not_empty: \A \ {}\ if \odd (card A)\ using that by auto lemma nat_induct2 [case_names 0 1 step]: assumes "P 0" "P 1" and step: "\n::nat. P n \ P (n + 2)" shows "P n" proof (induct n rule: less_induct) case (less n) show ?case proof (cases "n < Suc (Suc 0)") case True then show ?thesis using assms by (auto simp: less_Suc_eq) next case False then obtain k where k: "n = Suc (Suc k)" by (force simp: not_less nat_le_iff_add) then have "kParity and powers\ context ring_1 begin lemma power_minus_even [simp]: "even n \ (- a) ^ n = a ^ n" by (auto elim: evenE) lemma power_minus_odd [simp]: "odd n \ (- a) ^ n = - (a ^ n)" by (auto elim: oddE) lemma uminus_power_if: "(- a) ^ n = (if even n then a ^ n else - (a ^ n))" by auto lemma neg_one_even_power [simp]: "even n \ (- 1) ^ n = 1" by simp lemma neg_one_odd_power [simp]: "odd n \ (- 1) ^ n = - 1" by simp lemma neg_one_power_add_eq_neg_one_power_diff: "k \ n \ (- 1) ^ (n + k) = (- 1) ^ (n - k)" by (cases "even (n + k)") auto lemma minus_one_power_iff: "(- 1) ^ n = (if even n then 1 else - 1)" by (induct n) auto end context linordered_idom begin lemma zero_le_even_power: "even n \ 0 \ a ^ n" by (auto elim: evenE) lemma zero_le_odd_power: "odd n \ 0 \ a ^ n \ 0 \ a" by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE) lemma zero_le_power_eq: "0 \ a ^ n \ even n \ odd n \ 0 \ a" by (auto simp add: zero_le_even_power zero_le_odd_power) lemma zero_less_power_eq: "0 < a ^ n \ n = 0 \ even n \ a \ 0 \ odd n \ 0 < a" proof - have [simp]: "0 = a ^ n \ a = 0 \ n > 0" unfolding power_eq_0_iff [of a n, symmetric] by blast show ?thesis unfolding less_le zero_le_power_eq by auto qed lemma power_less_zero_eq [simp]: "a ^ n < 0 \ odd n \ a < 0" unfolding not_le [symmetric] zero_le_power_eq by auto lemma power_le_zero_eq: "a ^ n \ 0 \ n > 0 \ (odd n \ a \ 0 \ even n \ a = 0)" unfolding not_less [symmetric] zero_less_power_eq by auto lemma power_even_abs: "even n \ \a\ ^ n = a ^ n" using power_abs [of a n] by (simp add: zero_le_even_power) lemma power_mono_even: assumes "even n" and "\a\ \ \b\" shows "a ^ n \ b ^ n" proof - have "0 \ \a\" by auto with \\a\ \ \b\\ have "\a\ ^ n \ \b\ ^ n" by (rule power_mono) with \even n\ show ?thesis by (simp add: power_even_abs) qed lemma power_mono_odd: assumes "odd n" and "a \ b" shows "a ^ n \ b ^ n" proof (cases "b < 0") case True with \a \ b\ have "- b \ - a" and "0 \ - b" by auto then have "(- b) ^ n \ (- a) ^ n" by (rule power_mono) with \odd n\ show ?thesis by simp next case False then have "0 \ b" by auto show ?thesis proof (cases "a < 0") case True then have "n \ 0" and "a \ 0" using \odd n\ [THEN odd_pos] by auto then have "a ^ n \ 0" unfolding power_le_zero_eq using \odd n\ by auto moreover from \0 \ b\ have "0 \ b ^ n" by auto ultimately show ?thesis by auto next case False then have "0 \ a" by auto with \a \ b\ show ?thesis using power_mono by auto qed qed text \Simplify, when the exponent is a numeral\ lemma zero_le_power_eq_numeral [simp]: "0 \ a ^ numeral w \ even (numeral w :: nat) \ odd (numeral w :: nat) \ 0 \ a" by (fact zero_le_power_eq) lemma zero_less_power_eq_numeral [simp]: "0 < a ^ numeral w \ numeral w = (0 :: nat) \ even (numeral w :: nat) \ a \ 0 \ odd (numeral w :: nat) \ 0 < a" by (fact zero_less_power_eq) lemma power_le_zero_eq_numeral [simp]: "a ^ numeral w \ 0 \ (0 :: nat) < numeral w \ (odd (numeral w :: nat) \ a \ 0 \ even (numeral w :: nat) \ a = 0)" by (fact power_le_zero_eq) lemma power_less_zero_eq_numeral [simp]: "a ^ numeral w < 0 \ odd (numeral w :: nat) \ a < 0" by (fact power_less_zero_eq) lemma power_even_abs_numeral [simp]: "even (numeral w :: nat) \ \a\ ^ numeral w = a ^ numeral w" by (fact power_even_abs) end subsection \Instance for \<^typ>\int\\ lemma even_diff_iff: "even (k - l) \ even (k + l)" for k l :: int by (fact even_diff) lemma even_abs_add_iff: "even (\k\ + l) \ even (k + l)" for k l :: int by simp lemma even_add_abs_iff: "even (k + \l\) \ even (k + l)" for k l :: int by simp lemma even_nat_iff: "0 \ k \ even (nat k) \ even k" by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric]) lemma zdiv_zmult2_eq: \a div (b * c) = (a div b) div c\ if \c \ 0\ for a b c :: int proof (cases \b \ 0\) case True with that show ?thesis using div_mult2_eq' [of a \nat b\ \nat c\] by simp next case False with that show ?thesis using div_mult2_eq' [of \- a\ \nat (- b)\ \nat c\] by simp qed lemma zmod_zmult2_eq: \a mod (b * c) = b * (a div b mod c) + a mod b\ if \c \ 0\ for a b c :: int proof (cases \b \ 0\) case True with that show ?thesis using mod_mult2_eq' [of a \nat b\ \nat c\] by simp next case False with that show ?thesis using mod_mult2_eq' [of \- a\ \nat (- b)\ \nat c\] by simp qed subsection \Abstract bit structures\ class semiring_bits = semiring_parity + - assumes bit_induct [case_names stable rec]: + assumes bits_induct [case_names stable rec]: \(\a. a div 2 = a \ P a) \ (\a b. P a \ (of_bool b + 2 * a) div 2 = a \ P (of_bool b + 2 * a)) \ P a\ assumes bits_div_0 [simp]: \0 div a = 0\ and bits_div_by_1 [simp]: \a div 1 = a\ - and bit_mod_div_trivial [simp]: \a mod b div b = 0\ + and bits_mod_div_trivial [simp]: \a mod b div b = 0\ and even_succ_div_2 [simp]: \even a \ (1 + a) div 2 = a div 2\ and exp_div_exp_eq: \2 ^ m div 2 ^ n = of_bool (2 ^ m \ 0 \ m \ n) * 2 ^ (m - n)\ and div_exp_eq: \a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\ and mod_exp_eq: \a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\ and mult_exp_mod_exp_eq: \m \ n \ (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\ and div_exp_mod_exp_eq: \a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\ begin +lemma bits_div_by_0 [simp]: + \a div 0 = 0\ + by (metis add_cancel_right_right bits_mod_div_trivial mod_mult_div_eq mult_not_zero) + lemma bits_1_div_2 [simp]: \1 div 2 = 0\ using even_succ_div_2 [of 0] by simp lemma bits_1_div_exp [simp]: \1 div 2 ^ n = of_bool (n = 0)\ using div_exp_eq [of 1 1] by (cases n) simp_all lemma even_succ_div_exp [simp]: \(1 + a) div 2 ^ n = a div 2 ^ n\ if \even a\ and \n > 0\ proof (cases n) case 0 with that show ?thesis by simp next case (Suc n) with \even a\ have \(1 + a) div 2 ^ Suc n = a div 2 ^ Suc n\ proof (induction n) case 0 then show ?case by simp next case (Suc n) then show ?case using div_exp_eq [of _ 1 \Suc n\, symmetric] by simp qed with Suc show ?thesis by simp qed lemma even_succ_mod_exp [simp]: \(1 + a) mod 2 ^ n = 1 + (a mod 2 ^ n)\ if \even a\ and \n > 0\ using div_mult_mod_eq [of \1 + a\ \2 ^ n\] that apply simp by (metis local.add.left_commute local.add_left_cancel local.div_mult_mod_eq) lemma bits_mod_by_1 [simp]: \a mod 1 = 0\ using div_mult_mod_eq [of a 1] by simp lemma bits_mod_0 [simp]: \0 mod a = 0\ using div_mult_mod_eq [of 0 a] by simp -lemma one_mod_two_eq_one [simp]: +lemma bits_one_mod_two_eq_one [simp]: \1 mod 2 = 1\ by (simp add: mod2_eq_if) definition bit :: \'a \ nat \ bool\ where \bit a n \ odd (a div 2 ^ n)\ lemma bit_0 [simp]: \bit a 0 \ odd a\ by (simp add: bit_def) lemma bit_Suc [simp]: \bit a (Suc n) \ bit (a div 2) n\ using div_exp_eq [of a 1 n] by (simp add: bit_def) +lemma bit_0_eq [simp]: + \bit 0 = bot\ + by (simp add: fun_eq_iff bit_def) + context fixes a assumes stable: \a div 2 = a\ begin -lemma stable_imp_add_self: +lemma bits_stable_imp_add_self: \a + a mod 2 = 0\ proof - have \a div 2 * 2 + a mod 2 = a\ by (fact div_mult_mod_eq) then have \a * 2 + a mod 2 = a\ by (simp add: stable) then show ?thesis by (simp add: mult_2_right ac_simps) qed lemma stable_imp_bit_iff_odd: \bit a n \ odd a\ by (induction n) (simp_all add: stable) end lemma bit_iff_idd_imp_stable: \a div 2 = a\ if \\n. bit a n \ odd a\ -using that proof (induction a rule: bit_induct) +using that proof (induction a rule: bits_induct) case (stable a) then show ?case by simp next case (rec a b) from rec.prems [of 1] have [simp]: \b = odd a\ by (simp add: rec.hyps) from rec.hyps have hyp: \(of_bool (odd a) + 2 * a) div 2 = a\ by simp have \bit a n \ odd a\ for n using rec.prems [of \Suc n\] by (simp add: hyp) then have \a div 2 = a\ by (rule rec.IH) then have \of_bool (odd a) + 2 * a = 2 * (a div 2) + of_bool (odd a)\ by (simp add: ac_simps) also have \\ = a\ using mult_div_mod_eq [of 2 a] by (simp add: of_bool_odd_eq_mod_2) finally show ?case using \a div 2 = a\ by (simp add: hyp) qed lemma bit_eqI: \a = b\ if \\n. bit a n \ bit b n\ -using that proof (induction a arbitrary: b rule: bit_induct) +using that proof (induction a arbitrary: b rule: bits_induct) case (stable a) from stable(2) [of 0] have **: \even b \ even a\ by simp have \b div 2 = b\ proof (rule bit_iff_idd_imp_stable) fix n from stable have *: \bit b n \ bit a n\ by simp also have \bit a n \ odd a\ using stable by (simp add: stable_imp_bit_iff_odd) finally show \bit b n \ odd b\ by (simp add: **) qed from ** have \a mod 2 = b mod 2\ by (simp add: mod2_eq_if) then have \a mod 2 + (a + b) = b mod 2 + (a + b)\ by simp then have \a + a mod 2 + b = b + b mod 2 + a\ by (simp add: ac_simps) with \a div 2 = a\ \b div 2 = b\ show ?case - by (simp add: stable_imp_add_self) + by (simp add: bits_stable_imp_add_self) next case (rec a p) from rec.prems [of 0] have [simp]: \p = odd b\ by simp from rec.hyps have \bit a n \ bit (b div 2) n\ for n using rec.prems [of \Suc n\] by simp then have \a = b div 2\ by (rule rec.IH) then have \2 * a = 2 * (b div 2)\ by simp then have \b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)\ by simp also have \\ = b\ by (fact mod_mult_div_eq) finally show ?case by (auto simp add: mod2_eq_if) qed lemma bit_eq_iff: \a = b \ (\n. bit a n \ bit b n)\ by (auto intro: bit_eqI) lemma bit_eq_rec: \a = b \ (even a \ even b) \ a div 2 = b div 2\ apply (simp add: bit_eq_iff) apply auto using bit_0 apply blast using bit_0 apply blast using bit_Suc apply blast using bit_Suc apply blast apply (metis bit_eq_iff local.even_iff_mod_2_eq_zero local.mod_div_mult_eq) apply (metis bit_eq_iff local.even_iff_mod_2_eq_zero local.mod_div_mult_eq) apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq) apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq) done lemma bit_exp_iff: \bit (2 ^ m) n \ 2 ^ m \ 0 \ m = n\ by (auto simp add: bit_def exp_div_exp_eq) end lemma nat_bit_induct [case_names zero even odd]: "P n" if zero: "P 0" and even: "\n. P n \ n > 0 \ P (2 * n)" and odd: "\n. P n \ P (Suc (2 * n))" proof (induction n rule: less_induct) case (less n) show "P n" proof (cases "n = 0") case True with zero show ?thesis by simp next case False with less have hyp: "P (n div 2)" by simp show ?thesis proof (cases "even n") case True then have "n \ 1" by auto with \n \ 0\ have "n div 2 > 0" by simp with \even n\ hyp even [of "n div 2"] show ?thesis by simp next case False with hyp odd [of "n div 2"] show ?thesis by simp qed qed qed instance nat :: semiring_bits proof show \P n\ if stable: \\n. n div 2 = n \ P n\ and rec: \\n b. P n \ (of_bool b + 2 * n) div 2 = n \ P (of_bool b + 2 * n)\ for P and n :: nat proof (induction n rule: nat_bit_induct) case zero from stable [of 0] show ?case by simp next case (even n) with rec [of n False] show ?case by simp next case (odd n) with rec [of n True] show ?case by simp qed show \q mod 2 ^ m mod 2 ^ n = q mod 2 ^ min m n\ for q m n :: nat apply (auto simp add: less_iff_Suc_add power_add mod_mod_cancel split: split_min_lin) apply (metis div_mult2_eq mod_div_trivial mod_eq_self_iff_div_eq_0 mod_mult_self2_is_0 power_commutes) done show \(q * 2 ^ m) mod (2 ^ n) = (q mod 2 ^ (n - m)) * 2 ^ m\ if \m \ n\ for q m n :: nat using that apply (auto simp add: mod_mod_cancel div_mult2_eq power_add mod_mult2_eq le_iff_add split: split_min_lin) apply (simp add: mult.commute) done qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff) lemma int_bit_induct [case_names zero minus even odd]: "P k" if zero_int: "P 0" and minus_int: "P (- 1)" and even_int: "\k. P k \ k \ 0 \ P (k * 2)" and odd_int: "\k. P k \ k \ - 1 \ P (1 + (k * 2))" for k :: int proof (cases "k \ 0") case True define n where "n = nat k" with True have "k = int n" by simp then show "P k" proof (induction n arbitrary: k rule: nat_bit_induct) case zero then show ?case by (simp add: zero_int) next case (even n) have "P (int n * 2)" by (rule even_int) (use even in simp_all) with even show ?case by (simp add: ac_simps) next case (odd n) have "P (1 + (int n * 2))" by (rule odd_int) (use odd in simp_all) with odd show ?case by (simp add: ac_simps) qed next case False define n where "n = nat (- k - 1)" with False have "k = - int n - 1" by simp then show "P k" proof (induction n arbitrary: k rule: nat_bit_induct) case zero then show ?case by (simp add: minus_int) next case (even n) have "P (1 + (- int (Suc n) * 2))" by (rule odd_int) (use even in \simp_all add: algebra_simps\) also have "\ = - int (2 * n) - 1" by (simp add: algebra_simps) finally show ?case using even by simp next case (odd n) have "P (- int (Suc n) * 2)" by (rule even_int) (use odd in \simp_all add: algebra_simps\) also have "\ = - int (Suc (2 * n)) - 1" by (simp add: algebra_simps) finally show ?case using odd by simp qed qed instance int :: semiring_bits proof show \P k\ if stable: \\k. k div 2 = k \ P k\ and rec: \\k b. P k \ (of_bool b + 2 * k) div 2 = k \ P (of_bool b + 2 * k)\ for P and k :: int proof (induction k rule: int_bit_induct) case zero from stable [of 0] show ?case by simp next case minus from stable [of \- 1\] show ?case by simp next case (even k) with rec [of k False] show ?case by (simp add: ac_simps) next case (odd k) with rec [of k True] show ?case by (simp add: ac_simps) qed show \(2::int) ^ m div 2 ^ n = of_bool ((2::int) ^ m \ 0 \ n \ m) * 2 ^ (m - n)\ for m n :: nat proof (cases \m < n\) case True then have \n = m + (n - m)\ by simp then have \(2::int) ^ m div 2 ^ n = (2::int) ^ m div 2 ^ (m + (n - m))\ by simp also have \\ = (2::int) ^ m div (2 ^ m * 2 ^ (n - m))\ by (simp add: power_add) also have \\ = (2::int) ^ m div 2 ^ m div 2 ^ (n - m)\ by (simp add: zdiv_zmult2_eq) finally show ?thesis using \m < n\ by simp next case False then show ?thesis by (simp add: power_diff) qed show \k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n\ for m n :: nat and k :: int using mod_exp_eq [of \nat k\ m n] apply (auto simp add: mod_mod_cancel zdiv_zmult2_eq power_add zmod_zmult2_eq le_iff_add split: split_min_lin) apply (auto simp add: less_iff_Suc_add mod_mod_cancel power_add) apply (simp only: flip: mult.left_commute [of \2 ^ m\]) apply (subst zmod_zmult2_eq) apply simp_all done show \(k * 2 ^ m) mod (2 ^ n) = (k mod 2 ^ (n - m)) * 2 ^ m\ if \m \ n\ for m n :: nat and k :: int using that apply (auto simp add: power_add zmod_zmult2_eq le_iff_add split: split_min_lin) apply (simp add: ac_simps) done qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le) class semiring_bit_shifts = semiring_bits + fixes push_bit :: \nat \ 'a \ 'a\ assumes push_bit_eq_mult: \push_bit n a = a * 2 ^ n\ fixes drop_bit :: \nat \ 'a \ 'a\ assumes drop_bit_eq_div: \drop_bit n a = a div 2 ^ n\ begin definition take_bit :: \nat \ 'a \ 'a\ where take_bit_eq_mod: \take_bit n a = a mod 2 ^ n\ text \ Logically, \<^const>\push_bit\, \<^const>\drop_bit\ and \<^const>\take_bit\ are just aliases; having them as separate operations makes proofs easier, otherwise proof automation would fiddle with concrete expressions \<^term>\2 ^ n\ in a way obfuscating the basic algebraic relationships between those operations. Having \<^const>\push_bit\ and \<^const>\drop_bit\ as definitional class operations takes into account that specific instances of these can be implemented differently wrt. code generation. \ -lemma bit_ident: +lemma bits_ident: "push_bit n (drop_bit n a) + take_bit n a = a" using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div) lemma push_bit_push_bit [simp]: "push_bit m (push_bit n a) = push_bit (m + n) a" by (simp add: push_bit_eq_mult power_add ac_simps) lemma push_bit_0_id [simp]: "push_bit 0 = id" by (simp add: fun_eq_iff push_bit_eq_mult) lemma push_bit_of_0 [simp]: "push_bit n 0 = 0" by (simp add: push_bit_eq_mult) lemma push_bit_of_1: "push_bit n 1 = 2 ^ n" by (simp add: push_bit_eq_mult) lemma push_bit_Suc [simp]: "push_bit (Suc n) a = push_bit n (a * 2)" by (simp add: push_bit_eq_mult ac_simps) lemma push_bit_double: "push_bit n (a * 2) = push_bit n a * 2" by (simp add: push_bit_eq_mult ac_simps) lemma push_bit_add: "push_bit n (a + b) = push_bit n a + push_bit n b" by (simp add: push_bit_eq_mult algebra_simps) lemma take_bit_0 [simp]: "take_bit 0 a = 0" by (simp add: take_bit_eq_mod) lemma take_bit_Suc [simp]: \take_bit (Suc n) a = take_bit n (a div 2) * 2 + of_bool (odd a)\ proof - have \take_bit (Suc n) (a div 2 * 2 + of_bool (odd a)) = take_bit n (a div 2) * 2 + of_bool (odd a)\ using even_succ_mod_exp [of \2 * (a div 2)\ \Suc n\] mult_exp_mod_exp_eq [of 1 \Suc n\ \a div 2\] by (auto simp add: take_bit_eq_mod ac_simps) then show ?thesis using div_mult_mod_eq [of a 2] by (simp add: mod_2_eq_odd) qed lemma take_bit_of_0 [simp]: "take_bit n 0 = 0" by (simp add: take_bit_eq_mod) lemma take_bit_of_1 [simp]: "take_bit n 1 = of_bool (n > 0)" by (cases n) simp_all lemma drop_bit_of_0 [simp]: "drop_bit n 0 = 0" by (simp add: drop_bit_eq_div) lemma drop_bit_of_1 [simp]: "drop_bit n 1 = of_bool (n = 0)" by (simp add: drop_bit_eq_div) lemma drop_bit_0 [simp]: "drop_bit 0 = id" by (simp add: fun_eq_iff drop_bit_eq_div) lemma drop_bit_Suc [simp]: "drop_bit (Suc n) a = drop_bit n (a div 2)" using div_exp_eq [of a 1] by (simp add: drop_bit_eq_div) lemma drop_bit_half: "drop_bit n (a div 2) = drop_bit n a div 2" by (induction n arbitrary: a) simp_all lemma drop_bit_of_bool [simp]: "drop_bit n (of_bool d) = of_bool (n = 0 \ d)" by (cases n) simp_all lemma take_bit_eq_0_imp_dvd: "take_bit n a = 0 \ 2 ^ n dvd a" by (simp add: take_bit_eq_mod mod_0_imp_dvd) lemma even_take_bit_eq [simp]: \even (take_bit n a) \ n = 0 \ even a\ by (cases n) simp_all lemma take_bit_take_bit [simp]: "take_bit m (take_bit n a) = take_bit (min m n) a" by (simp add: take_bit_eq_mod mod_exp_eq ac_simps) lemma drop_bit_drop_bit [simp]: "drop_bit m (drop_bit n a) = drop_bit (m + n) a" by (simp add: drop_bit_eq_div power_add div_exp_eq ac_simps) lemma push_bit_take_bit: "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)" apply (simp add: push_bit_eq_mult take_bit_eq_mod power_add ac_simps) using mult_exp_mod_exp_eq [of m \m + n\ a] apply (simp add: ac_simps power_add) done lemma take_bit_push_bit: "take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)" proof (cases "m \ n") case True then show ?thesis apply (simp add:) apply (simp_all add: push_bit_eq_mult take_bit_eq_mod) apply (auto dest!: le_Suc_ex simp add: power_add ac_simps) using mult_exp_mod_exp_eq [of m m \a * 2 ^ n\ for n] apply (simp add: ac_simps) done next case False then show ?thesis using push_bit_take_bit [of n "m - n" a] by simp qed lemma take_bit_drop_bit: "take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)" by (simp add: drop_bit_eq_div take_bit_eq_mod ac_simps div_exp_mod_exp_eq) lemma drop_bit_take_bit: "drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)" proof (cases "m \ n") case True then show ?thesis using take_bit_drop_bit [of "n - m" m a] by simp next case False then obtain q where \m = n + q\ by (auto simp add: not_le dest: less_imp_Suc_add) then have \drop_bit m (take_bit n a) = 0\ using div_exp_eq [of \a mod 2 ^ n\ n q] by (simp add: take_bit_eq_mod drop_bit_eq_div) with False show ?thesis by simp qed lemma bit_drop_bit_eq: \bit (drop_bit n a) = bit a \ (+) n\ by (simp add: bit_def fun_eq_iff ac_simps flip: drop_bit_eq_div) lemma bit_take_bit_iff: \bit (take_bit m a) n \ n < m \ bit a n\ by (simp add: bit_def drop_bit_take_bit not_le flip: drop_bit_eq_div) end instantiation nat :: semiring_bit_shifts begin definition push_bit_nat :: \nat \ nat \ nat\ where \push_bit_nat n m = m * 2 ^ n\ definition drop_bit_nat :: \nat \ nat \ nat\ where \drop_bit_nat n m = m div 2 ^ n\ instance proof show \push_bit n m = m * 2 ^ n\ for n m :: nat by (simp add: push_bit_nat_def) show \drop_bit n m = m div 2 ^ n\ for n m :: nat by (simp add: drop_bit_nat_def) qed end instantiation int :: semiring_bit_shifts begin definition push_bit_int :: \nat \ int \ int\ where \push_bit_int n k = k * 2 ^ n\ definition drop_bit_int :: \nat \ int \ int\ where \drop_bit_int n k = k div 2 ^ n\ instance proof show \push_bit n k = k * 2 ^ n\ for n :: nat and k :: int by (simp add: push_bit_int_def) show \drop_bit n k = k div 2 ^ n\ for n :: nat and k :: int by (simp add: drop_bit_int_def) qed end class unique_euclidean_semiring_with_bit_shifts = unique_euclidean_semiring_with_nat + semiring_bit_shifts begin lemma take_bit_of_exp [simp]: \take_bit m (2 ^ n) = of_bool (n < m) * 2 ^ n\ by (simp add: take_bit_eq_mod exp_mod_exp) lemma take_bit_of_2 [simp]: \take_bit n 2 = of_bool (2 \ n) * 2\ using take_bit_of_exp [of n 1] by simp lemma push_bit_eq_0_iff [simp]: "push_bit n a = 0 \ a = 0" by (simp add: push_bit_eq_mult) lemma push_bit_numeral [simp]: "push_bit (numeral l) (numeral k) = push_bit (pred_numeral l) (numeral (Num.Bit0 k))" by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric]) (simp add: ac_simps) lemma push_bit_of_nat: "push_bit n (of_nat m) = of_nat (push_bit n m)" by (simp add: push_bit_eq_mult Parity.push_bit_eq_mult) lemma take_bit_add: "take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)" by (simp add: take_bit_eq_mod mod_simps) lemma take_bit_eq_0_iff: "take_bit n a = 0 \ 2 ^ n dvd a" by (simp add: take_bit_eq_mod mod_eq_0_iff_dvd) lemma take_bit_of_1_eq_0_iff [simp]: "take_bit n 1 = 0 \ n = 0" by (simp add: take_bit_eq_mod) lemma take_bit_numeral_bit0 [simp]: "take_bit (numeral l) (numeral (Num.Bit0 k)) = take_bit (pred_numeral l) (numeral k) * 2" by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] take_bit_Suc ac_simps even_mult_iff nonzero_mult_div_cancel_right [OF numeral_neq_zero]) simp lemma take_bit_numeral_bit1 [simp]: "take_bit (numeral l) (numeral (Num.Bit1 k)) = take_bit (pred_numeral l) (numeral k) * 2 + 1" by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] take_bit_Suc ac_simps even_add even_mult_iff div_mult_self1 [OF numeral_neq_zero]) (simp add: ac_simps) lemma take_bit_of_nat: "take_bit n (of_nat m) = of_nat (take_bit n m)" by (simp add: take_bit_eq_mod Parity.take_bit_eq_mod of_nat_mod [of m "2 ^ n"]) lemma drop_bit_numeral_bit0 [simp]: "drop_bit (numeral l) (numeral (Num.Bit0 k)) = drop_bit (pred_numeral l) (numeral k)" by (simp only: numeral_eq_Suc power_Suc numeral_Bit0 [of k] mult_2 [symmetric] drop_bit_Suc nonzero_mult_div_cancel_left [OF numeral_neq_zero]) lemma drop_bit_numeral_bit1 [simp]: "drop_bit (numeral l) (numeral (Num.Bit1 k)) = drop_bit (pred_numeral l) (numeral k)" by (simp only: numeral_eq_Suc power_Suc numeral_Bit1 [of k] mult_2 [symmetric] drop_bit_Suc div_mult_self4 [OF numeral_neq_zero]) simp lemma drop_bit_of_nat: "drop_bit n (of_nat m) = of_nat (drop_bit n m)" by (simp add: drop_bit_eq_div Parity.drop_bit_eq_div of_nat_div [of m "2 ^ n"]) end instance nat :: unique_euclidean_semiring_with_bit_shifts .. instance int :: unique_euclidean_semiring_with_bit_shifts .. lemma push_bit_of_Suc_0 [simp]: "push_bit n (Suc 0) = 2 ^ n" using push_bit_of_1 [where ?'a = nat] by simp lemma take_bit_of_Suc_0 [simp]: "take_bit n (Suc 0) = of_bool (0 < n)" using take_bit_of_1 [where ?'a = nat] by simp lemma drop_bit_of_Suc_0 [simp]: "drop_bit n (Suc 0) = of_bool (n = 0)" using drop_bit_of_1 [where ?'a = nat] by simp lemma take_bit_eq_self: \take_bit n m = m\ if \m < 2 ^ n\ for n m :: nat using that by (simp add: take_bit_eq_mod) lemma push_bit_minus_one: "push_bit n (- 1 :: int) = - (2 ^ n)" by (simp add: push_bit_eq_mult) +lemma minus_1_div_exp_eq_int: + \- 1 div (2 :: int) ^ n = - 1\ + by (induction n) (use div_exp_eq [symmetric, of \- 1 :: int\ 1] in \simp_all add: ac_simps\) + +lemma drop_bit_minus_one [simp]: + \drop_bit n (- 1 :: int) = - 1\ + by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int) + +lemma take_bit_uminus: + "take_bit n (- (take_bit n k)) = take_bit n (- k)" + for k :: int + by (simp add: take_bit_eq_mod mod_minus_eq) + +lemma take_bit_minus: + "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)" + for k l :: int + by (simp add: take_bit_eq_mod mod_diff_eq) + +lemma take_bit_nonnegative [simp]: + "take_bit n k \ 0" + for k :: int + by (simp add: take_bit_eq_mod) + end diff --git a/src/HOL/ex/Bit_Operations.thy b/src/HOL/ex/Bit_Operations.thy --- a/src/HOL/ex/Bit_Operations.thy +++ b/src/HOL/ex/Bit_Operations.thy @@ -1,801 +1,791 @@ (* Author: Florian Haftmann, TUM *) section \Proof of concept for purely algebraically founded lists of bits\ theory Bit_Operations imports "HOL-Library.Boolean_Algebra" Main begin -lemma minus_1_div_exp_eq_int [simp]: - \- 1 div (2 :: int) ^ n = - 1\ - for n :: nat - by (induction n) (use div_exp_eq [symmetric, of \- 1 :: int\ 1] in \simp_all add: ac_simps\) - context semiring_bits begin -lemma bits_div_by_0 [simp]: - \a div 0 = 0\ - by (metis local.add_cancel_right_right local.bit_mod_div_trivial local.mod_mult_div_eq local.mult_not_zero) - -lemma bit_0_eq [simp]: - \bit 0 = bot\ - by (simp add: fun_eq_iff bit_def) - end context semiring_bit_shifts begin end subsection \Bit operations in suitable algebraic structures\ class semiring_bit_operations = semiring_bit_shifts + fixes "and" :: \'a \ 'a \ 'a\ (infixr "AND" 64) and or :: \'a \ 'a \ 'a\ (infixr "OR" 59) and xor :: \'a \ 'a \ 'a\ (infixr "XOR" 59) assumes bit_and_iff: \\n. bit (a AND b) n \ bit a n \ bit b n\ and bit_or_iff: \\n. bit (a OR b) n \ bit a n \ bit b n\ and bit_xor_iff: \\n. bit (a XOR b) n \ bit a n \ bit b n\ begin text \ We want the bitwise operations to bind slightly weaker than \+\ and \-\. For the sake of code generation the operations \<^const>\and\, \<^const>\or\ and \<^const>\xor\ are specified as definitional class operations. - \ definition map_bit :: \nat \ (bool \ bool) \ 'a \ 'a\ where \map_bit n f a = take_bit n a + push_bit n (of_bool (f (bit a n)) + 2 * drop_bit (Suc n) a)\ definition set_bit :: \nat \ 'a \ 'a\ where \set_bit n = map_bit n top\ definition unset_bit :: \nat \ 'a \ 'a\ where \unset_bit n = map_bit n bot\ definition flip_bit :: \nat \ 'a \ 'a\ where \flip_bit n = map_bit n Not\ text \ Having \<^const>\set_bit\, \<^const>\unset_bit\ and \<^const>\flip_bit\ as separate operations allows to implement them using bit masks later. \ lemma stable_imp_drop_eq: \drop_bit n a = a\ if \a div 2 = a\ by (induction n) (simp_all add: that) lemma map_bit_0 [simp]: \map_bit 0 f a = of_bool (f (odd a)) + 2 * (a div 2)\ by (simp add: map_bit_def) lemma map_bit_Suc [simp]: \map_bit (Suc n) f a = a mod 2 + 2 * map_bit n f (a div 2)\ by (auto simp add: map_bit_def algebra_simps mod2_eq_if push_bit_add mult_2 elim: evenE oddE) lemma set_bit_0 [simp]: \set_bit 0 a = 1 + 2 * (a div 2)\ by (simp add: set_bit_def) lemma set_bit_Suc [simp]: \set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\ by (simp add: set_bit_def) lemma unset_bit_0 [simp]: \unset_bit 0 a = 2 * (a div 2)\ by (simp add: unset_bit_def) lemma unset_bit_Suc [simp]: \unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\ by (simp add: unset_bit_def) lemma flip_bit_0 [simp]: \flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\ by (simp add: flip_bit_def) lemma flip_bit_Suc [simp]: \flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\ by (simp add: flip_bit_def) end class ring_bit_operations = semiring_bit_operations + ring_parity + fixes not :: \'a \ 'a\ (\NOT\) assumes bits_even_minus_1_div_exp_iff [simp]: \even (- 1 div 2 ^ n) \ 2 ^ n = 0\ assumes bit_not_iff: \\n. bit (NOT a) n \ 2 ^ n \ 0 \ \ bit a n\ begin lemma bits_minus_1_mod_2_eq [simp]: \(- 1) mod 2 = 1\ by (simp add: mod_2_eq_odd) lemma bit_minus_1_iff [simp]: \bit (- 1) n \ 2 ^ n \ 0\ by (simp add: bit_def) sublocale bit: boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ rewrites \bit.xor = (XOR)\ proof - interpret bit: boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ apply standard apply (auto simp add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff) apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) done show \boolean_algebra (AND) (OR) NOT 0 (- 1)\ by standard show \boolean_algebra.xor (AND) (OR) NOT = (XOR)\ apply (auto simp add: fun_eq_iff bit.xor_def bit_eq_iff bit_and_iff bit_or_iff bit_not_iff bit_xor_iff) apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) done qed text \ For the sake of code generation \<^const>\not\ is specified as definitional class operation. Note that \<^const>\not\ has no sensible definition for unlimited but only positive bit strings (type \<^typ>\nat\). \ end subsubsection \Instance \<^typ>\nat\\ locale zip_nat = single: abel_semigroup f for f :: "bool \ bool \ bool" (infixl "\<^bold>*" 70) + assumes end_of_bits: "\ False \<^bold>* False" begin lemma False_P_imp: "False \<^bold>* True \ P" if "False \<^bold>* P" using that end_of_bits by (cases P) simp_all function F :: "nat \ nat \ nat" (infixl "\<^bold>\" 70) where "m \<^bold>\ n = (if m = 0 \ n = 0 then 0 else of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2)" by auto termination by (relation "measure (case_prod (+))") auto lemma zero_left_eq: "0 \<^bold>\ n = of_bool (False \<^bold>* True) * n" by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits) lemma zero_right_eq: "m \<^bold>\ 0 = of_bool (True \<^bold>* False) * m" by (induction m rule: nat_bit_induct) (simp_all add: end_of_bits) lemma simps [simp]: "0 \<^bold>\ 0 = 0" "0 \<^bold>\ n = of_bool (False \<^bold>* True) * n" "m \<^bold>\ 0 = of_bool (True \<^bold>* False) * m" "m > 0 \ n > 0 \ m \<^bold>\ n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2" by (simp_all only: zero_left_eq zero_right_eq) simp lemma rec: "m \<^bold>\ n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2" by (cases "m = 0 \ n = 0") (auto simp add: end_of_bits) declare F.simps [simp del] sublocale abel_semigroup F proof show "m \<^bold>\ n \<^bold>\ q = m \<^bold>\ (n \<^bold>\ q)" for m n q :: nat proof (induction m arbitrary: n q rule: nat_bit_induct) case zero show ?case by simp next case (even m) with rec [of "2 * m"] rec [of _ q] show ?case by (cases "even n") (auto simp add: ac_simps dest: False_P_imp) next case (odd m) with rec [of "Suc (2 * m)"] rec [of _ q] show ?case by (cases "even n"; cases "even q") (auto dest: False_P_imp simp add: ac_simps) qed show "m \<^bold>\ n = n \<^bold>\ m" for m n :: nat proof (induction m arbitrary: n rule: nat_bit_induct) case zero show ?case by (simp add: ac_simps) next case (even m) with rec [of "2 * m" n] rec [of n "2 * m"] show ?case by (simp add: ac_simps) next case (odd m) with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case by (simp add: ac_simps) qed qed lemma self [simp]: "n \<^bold>\ n = of_bool (True \<^bold>* True) * n" by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits) lemma even_iff [simp]: "even (m \<^bold>\ n) \ \ (odd m \<^bold>* odd n)" proof (induction m arbitrary: n rule: nat_bit_induct) case zero show ?case by (cases "even n") (simp_all add: end_of_bits) next case (even m) then show ?case by (simp add: rec [of "2 * m"]) next case (odd m) then show ?case by (simp add: rec [of "Suc (2 * m)"]) qed end instantiation nat :: semiring_bit_operations begin global_interpretation and_nat: zip_nat "(\)" defines and_nat = and_nat.F by standard auto global_interpretation and_nat: semilattice "(AND) :: nat \ nat \ nat" proof (rule semilattice.intro, fact and_nat.abel_semigroup_axioms, standard) show "n AND n = n" for n :: nat by (simp add: and_nat.self) qed declare and_nat.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ lemma zero_nat_and_eq [simp]: "0 AND n = 0" for n :: nat by simp lemma and_zero_nat_eq [simp]: "n AND 0 = 0" for n :: nat by simp global_interpretation or_nat: zip_nat "(\)" defines or_nat = or_nat.F by standard auto global_interpretation or_nat: semilattice "(OR) :: nat \ nat \ nat" proof (rule semilattice.intro, fact or_nat.abel_semigroup_axioms, standard) show "n OR n = n" for n :: nat by (simp add: or_nat.self) qed declare or_nat.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ lemma zero_nat_or_eq [simp]: "0 OR n = n" for n :: nat by simp lemma or_zero_nat_eq [simp]: "n OR 0 = n" for n :: nat by simp global_interpretation xor_nat: zip_nat "(\)" defines xor_nat = xor_nat.F by standard auto declare xor_nat.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ lemma zero_nat_xor_eq [simp]: "0 XOR n = n" for n :: nat by simp lemma xor_zero_nat_eq [simp]: "n XOR 0 = n" for n :: nat by simp instance proof fix m n q :: nat show \bit (m AND n) q \ bit m q \ bit n q\ proof (rule sym, induction q arbitrary: m n) case 0 then show ?case by (simp add: and_nat.even_iff) next case (Suc q) with and_nat.rec [of m n] show ?case by simp qed show \bit (m OR n) q \ bit m q \ bit n q\ proof (rule sym, induction q arbitrary: m n) case 0 then show ?case by (simp add: or_nat.even_iff) next case (Suc q) with or_nat.rec [of m n] show ?case by simp qed show \bit (m XOR n) q \ bit m q \ bit n q\ proof (rule sym, induction q arbitrary: m n) case 0 then show ?case by (simp add: xor_nat.even_iff) next case (Suc q) with xor_nat.rec [of m n] show ?case by simp qed qed end global_interpretation or_nat: semilattice_neutr "(OR)" "0 :: nat" by standard simp global_interpretation xor_nat: comm_monoid "(XOR)" "0 :: nat" by standard simp lemma Suc_0_and_eq [simp]: "Suc 0 AND n = n mod 2" by (cases n) auto lemma and_Suc_0_eq [simp]: "n AND Suc 0 = n mod 2" using Suc_0_and_eq [of n] by (simp add: ac_simps) lemma Suc_0_or_eq [simp]: "Suc 0 OR n = n + of_bool (even n)" by (cases n) (simp_all add: ac_simps) lemma or_Suc_0_eq [simp]: "n OR Suc 0 = n + of_bool (even n)" using Suc_0_or_eq [of n] by (simp add: ac_simps) lemma Suc_0_xor_eq [simp]: "Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)" by (cases n) (simp_all add: ac_simps) lemma xor_Suc_0_eq [simp]: "n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)" using Suc_0_xor_eq [of n] by (simp add: ac_simps) subsubsection \Instance \<^typ>\int\\ abbreviation (input) complement :: "int \ int" where "complement k \ - k - 1" lemma complement_half: "complement (k * 2) div 2 = complement k" by simp lemma complement_div_2: "complement (k div 2) = complement k div 2" by linarith locale zip_int = single: abel_semigroup f for f :: "bool \ bool \ bool" (infixl "\<^bold>*" 70) begin lemma False_False_imp_True_True: "True \<^bold>* True" if "False \<^bold>* False" proof (rule ccontr) assume "\ True \<^bold>* True" with that show False using single.assoc [of False True True] by (cases "False \<^bold>* True") simp_all qed function F :: "int \ int \ int" (infixl "\<^bold>\" 70) where "k \<^bold>\ l = (if k \ {0, - 1} \ l \ {0, - 1} then - of_bool (odd k \<^bold>* odd l) else of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2)" by auto termination by (relation "measure (\(k, l). nat (\k\ + \l\))") auto lemma zero_left_eq: "0 \<^bold>\ l = (case (False \<^bold>* False, False \<^bold>* True) of (False, False) \ 0 | (False, True) \ l | (True, False) \ complement l | (True, True) \ - 1)" by (induction l rule: int_bit_induct) (simp_all split: bool.split) lemma minus_left_eq: "- 1 \<^bold>\ l = (case (True \<^bold>* False, True \<^bold>* True) of (False, False) \ 0 | (False, True) \ l | (True, False) \ complement l | (True, True) \ - 1)" by (induction l rule: int_bit_induct) (simp_all split: bool.split) lemma zero_right_eq: "k \<^bold>\ 0 = (case (False \<^bold>* False, False \<^bold>* True) of (False, False) \ 0 | (False, True) \ k | (True, False) \ complement k | (True, True) \ - 1)" by (induction k rule: int_bit_induct) (simp_all add: ac_simps split: bool.split) lemma minus_right_eq: "k \<^bold>\ - 1 = (case (True \<^bold>* False, True \<^bold>* True) of (False, False) \ 0 | (False, True) \ k | (True, False) \ complement k | (True, True) \ - 1)" by (induction k rule: int_bit_induct) (simp_all add: ac_simps split: bool.split) lemma simps [simp]: "0 \<^bold>\ 0 = - of_bool (False \<^bold>* False)" "- 1 \<^bold>\ 0 = - of_bool (True \<^bold>* False)" "0 \<^bold>\ - 1 = - of_bool (False \<^bold>* True)" "- 1 \<^bold>\ - 1 = - of_bool (True \<^bold>* True)" "0 \<^bold>\ l = (case (False \<^bold>* False, False \<^bold>* True) of (False, False) \ 0 | (False, True) \ l | (True, False) \ complement l | (True, True) \ - 1)" "- 1 \<^bold>\ l = (case (True \<^bold>* False, True \<^bold>* True) of (False, False) \ 0 | (False, True) \ l | (True, False) \ complement l | (True, True) \ - 1)" "k \<^bold>\ 0 = (case (False \<^bold>* False, False \<^bold>* True) of (False, False) \ 0 | (False, True) \ k | (True, False) \ complement k | (True, True) \ - 1)" "k \<^bold>\ - 1 = (case (True \<^bold>* False, True \<^bold>* True) of (False, False) \ 0 | (False, True) \ k | (True, False) \ complement k | (True, True) \ - 1)" "k \ 0 \ k \ - 1 \ l \ 0 \ l \ - 1 \ k \<^bold>\ l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2" by simp_all[4] (simp_all only: zero_left_eq minus_left_eq zero_right_eq minus_right_eq, simp) declare F.simps [simp del] lemma rec: "k \<^bold>\ l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2" by (cases "k \ {0, - 1} \ l \ {0, - 1}") (auto simp add: ac_simps F.simps [of k l] split: bool.split) sublocale abel_semigroup F proof show "k \<^bold>\ l \<^bold>\ r = k \<^bold>\ (l \<^bold>\ r)" for k l r :: int proof (induction k arbitrary: l r rule: int_bit_induct) case zero have "complement l \<^bold>\ r = complement (l \<^bold>\ r)" if "False \<^bold>* False" "\ False \<^bold>* True" proof (induction l arbitrary: r rule: int_bit_induct) case zero from that show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case minus from that show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case (even l) with that rec [of _ r] show ?case by (cases "even r") (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits) next case (odd l) moreover have "- l - 1 = - 1 - l" by simp ultimately show ?case using that rec [of _ r] by (cases "even r") (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) qed then show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case minus have "complement l \<^bold>\ r = complement (l \<^bold>\ r)" if "\ True \<^bold>* True" "False \<^bold>* True" proof (induction l arbitrary: r rule: int_bit_induct) case zero from that show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case minus from that show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case (even l) with that rec [of _ r] show ?case by (cases "even r") (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits) next case (odd l) moreover have "- l - 1 = - 1 - l" by simp ultimately show ?case using that rec [of _ r] by (cases "even r") (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) qed then show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case (even k) with rec [of "k * 2"] rec [of _ r] show ?case by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True) next case (odd k) with rec [of "1 + k * 2"] rec [of _ r] show ?case by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True) qed show "k \<^bold>\ l = l \<^bold>\ k" for k l :: int proof (induction k arbitrary: l rule: int_bit_induct) case zero show ?case by simp next case minus show ?case by simp next case (even k) with rec [of "k * 2" l] rec [of l "k * 2"] show ?case by (simp add: ac_simps) next case (odd k) with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case by (simp add: ac_simps) qed qed lemma self [simp]: "k \<^bold>\ k = (case (False \<^bold>* False, True \<^bold>* True) of (False, False) \ 0 | (False, True) \ k | (True, True) \ - 1)" by (induction k rule: int_bit_induct) (auto simp add: False_False_imp_True_True split: bool.split) lemma even_iff [simp]: "even (k \<^bold>\ l) \ \ (odd k \<^bold>* odd l)" proof (induction k arbitrary: l rule: int_bit_induct) case zero show ?case by (cases "even l") (simp_all split: bool.splits) next case minus show ?case by (cases "even l") (simp_all split: bool.splits) next case (even k) then show ?case by (simp add: rec [of "k * 2"]) next case (odd k) then show ?case by (simp add: rec [of "1 + k * 2"]) qed end instantiation int :: ring_bit_operations begin definition not_int :: "int \ int" where "not_int = complement" global_interpretation and_int: zip_int "(\)" defines and_int = and_int.F by standard declare and_int.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ global_interpretation and_int: semilattice "(AND) :: int \ int \ int" proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard) show "k AND k = k" for k :: int by (simp add: and_int.self) qed lemma zero_int_and_eq [simp]: "0 AND k = 0" for k :: int by simp lemma and_zero_int_eq [simp]: "k AND 0 = 0" for k :: int by simp lemma minus_int_and_eq [simp]: "- 1 AND k = k" for k :: int by simp lemma and_minus_int_eq [simp]: "k AND - 1 = k" for k :: int by simp global_interpretation or_int: zip_int "(\)" defines or_int = or_int.F by standard declare or_int.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ global_interpretation or_int: semilattice "(OR) :: int \ int \ int" proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard) show "k OR k = k" for k :: int by (simp add: or_int.self) qed lemma zero_int_or_eq [simp]: "0 OR k = k" for k :: int by simp lemma and_zero_or_eq [simp]: "k OR 0 = k" for k :: int by simp lemma minus_int_or_eq [simp]: "- 1 OR k = - 1" for k :: int by simp lemma or_minus_int_eq [simp]: "k OR - 1 = - 1" for k :: int by simp global_interpretation xor_int: zip_int "(\)" defines xor_int = xor_int.F by standard declare xor_int.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ lemma zero_int_xor_eq [simp]: "0 XOR k = k" for k :: int by simp lemma and_zero_xor_eq [simp]: "k XOR 0 = k" for k :: int by simp lemma minus_int_xor_eq [simp]: "- 1 XOR k = complement k" for k :: int by simp lemma xor_minus_int_eq [simp]: "k XOR - 1 = complement k" for k :: int by simp lemma not_div_2: "NOT k div 2 = NOT (k div 2)" for k :: int by (simp add: complement_div_2 not_int_def) lemma not_int_simps [simp]: "NOT 0 = (- 1 :: int)" "NOT (- 1) = (0 :: int)" "k \ 0 \ k \ - 1 \ NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int by (auto simp add: not_int_def elim: oddE) lemma not_one_int [simp]: "NOT 1 = (- 2 :: int)" by simp lemma even_not_iff [simp]: "even (NOT k) \ odd k" for k :: int by (simp add: not_int_def) lemma bit_not_iff_int: \bit (NOT k) n \ \ bit k n\ for k :: int by (induction n arbitrary: k) (simp_all add: not_int_def flip: complement_div_2) - instance proof fix k l :: int and n :: nat show \bit (k AND l) n \ bit k n \ bit l n\ proof (rule sym, induction n arbitrary: k l) case 0 then show ?case by (simp add: and_int.even_iff) next case (Suc n) with and_int.rec [of k l] show ?case by simp qed show \bit (k OR l) n \ bit k n \ bit l n\ proof (rule sym, induction n arbitrary: k l) case 0 then show ?case by (simp add: or_int.even_iff) next case (Suc n) with or_int.rec [of k l] show ?case by simp qed show \bit (k XOR l) n \ bit k n \ bit l n\ proof (rule sym, induction n arbitrary: k l) case 0 then show ?case by (simp add: xor_int.even_iff) next case (Suc n) with xor_int.rec [of k l] show ?case by simp qed -qed (simp_all add: bit_not_iff_int) +qed (simp_all add: minus_1_div_exp_eq_int bit_not_iff_int) end lemma one_and_int_eq [simp]: "1 AND k = k mod 2" for k :: int using and_int.rec [of 1] by (simp add: mod2_eq_if) lemma and_one_int_eq [simp]: "k AND 1 = k mod 2" for k :: int using one_and_int_eq [of 1] by (simp add: ac_simps) lemma one_or_int_eq [simp]: "1 OR k = k + of_bool (even k)" for k :: int using or_int.rec [of 1] by (auto elim: oddE) lemma or_one_int_eq [simp]: "k OR 1 = k + of_bool (even k)" for k :: int using one_or_int_eq [of k] by (simp add: ac_simps) lemma one_xor_int_eq [simp]: "1 XOR k = k + of_bool (even k) - of_bool (odd k)" for k :: int using xor_int.rec [of 1] by (auto elim: oddE) lemma xor_one_int_eq [simp]: "k XOR 1 = k + of_bool (even k) - of_bool (odd k)" for k :: int using one_xor_int_eq [of k] by (simp add: ac_simps) lemma take_bit_complement_iff: - "Parity.take_bit n (complement k) = Parity.take_bit n (complement l) \ Parity.take_bit n k = Parity.take_bit n l" + "take_bit n (complement k) = take_bit n (complement l) \ take_bit n k = take_bit n l" for k l :: int - by (simp add: Parity.take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute) + by (simp add: take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute) lemma take_bit_not_iff: - "Parity.take_bit n (NOT k) = Parity.take_bit n (NOT l) \ Parity.take_bit n k = Parity.take_bit n l" + "take_bit n (NOT k) = take_bit n (NOT l) \ take_bit n k = take_bit n l" for k l :: int by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff_int) +lemma take_bit_not_take_bit: + \take_bit n (NOT (take_bit n k)) = take_bit n (NOT k)\ + for k :: int + by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff) + lemma take_bit_and [simp]: - "Parity.take_bit n (k AND l) = Parity.take_bit n k AND Parity.take_bit n l" + "take_bit n (k AND l) = take_bit n k AND take_bit n l" for k l :: int by (auto simp add: bit_eq_iff bit_take_bit_iff bit_and_iff) lemma take_bit_or [simp]: - "Parity.take_bit n (k OR l) = Parity.take_bit n k OR Parity.take_bit n l" + "take_bit n (k OR l) = take_bit n k OR take_bit n l" for k l :: int by (auto simp add: bit_eq_iff bit_take_bit_iff bit_or_iff) lemma take_bit_xor [simp]: - "Parity.take_bit n (k XOR l) = Parity.take_bit n k XOR Parity.take_bit n l" + "take_bit n (k XOR l) = take_bit n k XOR take_bit n l" for k l :: int by (auto simp add: bit_eq_iff bit_take_bit_iff bit_xor_iff) end diff --git a/src/HOL/ex/Word.thy b/src/HOL/ex/Word.thy --- a/src/HOL/ex/Word.thy +++ b/src/HOL/ex/Word.thy @@ -1,769 +1,692 @@ (* Author: Florian Haftmann, TUM *) section \Proof of concept for algebraically founded bit word types\ theory Word imports Main "HOL-Library.Type_Length" "HOL-ex.Bit_Operations" begin -context - includes lifting_syntax -begin - -lemma transfer_rule_of_bool: - \((\) ===> (\)) of_bool of_bool\ - if [transfer_rule]: \0 \ 0\ \1 \ 1\ - for R :: \'a::zero_neq_one \ 'b::zero_neq_one \ bool\ (infix \\\ 50) - by (unfold of_bool_def [abs_def]) transfer_prover - -end - - subsection \Preliminaries\ -lemma length_not_greater_eq_2_iff [simp]: - \\ 2 \ LENGTH('a::len) \ LENGTH('a) = 1\ - by (auto simp add: not_le dest: less_2_cases) - -lemma take_bit_uminus: - "take_bit n (- (take_bit n k)) = take_bit n (- k)" for k :: int - by (simp add: take_bit_eq_mod mod_minus_eq) - -lemma take_bit_minus: - "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)" for k l :: int - by (simp add: take_bit_eq_mod mod_diff_eq) - -lemma take_bit_nonnegative [simp]: - "take_bit n k \ 0" for k :: int - by (simp add: take_bit_eq_mod) - definition signed_take_bit :: "nat \ int \ int" where signed_take_bit_eq_take_bit: "signed_take_bit n k = take_bit (Suc n) (k + 2 ^ n) - 2 ^ n" lemma signed_take_bit_eq_take_bit': "signed_take_bit (n - Suc 0) k = take_bit n (k + 2 ^ (n - 1)) - 2 ^ (n - 1)" if "n > 0" using that by (simp add: signed_take_bit_eq_take_bit) lemma signed_take_bit_0 [simp]: "signed_take_bit 0 k = - (k mod 2)" proof (cases "even k") case True then have "odd (k + 1)" by simp then have "(k + 1) mod 2 = 1" by (simp add: even_iff_mod_2_eq_zero) with True show ?thesis by (simp add: signed_take_bit_eq_take_bit) next case False then show ?thesis by (simp add: signed_take_bit_eq_take_bit odd_iff_mod_2_eq_one) qed lemma signed_take_bit_Suc [simp]: "signed_take_bit (Suc n) k = signed_take_bit n (k div 2) * 2 + k mod 2" by (simp add: odd_iff_mod_2_eq_one signed_take_bit_eq_take_bit algebra_simps) lemma signed_take_bit_of_0 [simp]: "signed_take_bit n 0 = 0" by (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod) lemma signed_take_bit_of_minus_1 [simp]: "signed_take_bit n (- 1) = - 1" by (induct n) simp_all lemma signed_take_bit_eq_iff_take_bit_eq: "signed_take_bit (n - Suc 0) k = signed_take_bit (n - Suc 0) l \ take_bit n k = take_bit n l" (is "?P \ ?Q") if "n > 0" proof - from that obtain m where m: "n = Suc m" by (cases n) auto show ?thesis proof assume ?Q have "take_bit (Suc m) (k + 2 ^ m) = take_bit (Suc m) (take_bit (Suc m) k + take_bit (Suc m) (2 ^ m))" by (simp only: take_bit_add) also have "\ = take_bit (Suc m) (take_bit (Suc m) l + take_bit (Suc m) (2 ^ m))" by (simp only: \?Q\ m [symmetric]) also have "\ = take_bit (Suc m) (l + 2 ^ m)" by (simp only: take_bit_add) finally show ?P by (simp only: signed_take_bit_eq_take_bit m) simp next assume ?P with that have "(k + 2 ^ (n - Suc 0)) mod 2 ^ n = (l + 2 ^ (n - Suc 0)) mod 2 ^ n" by (simp add: signed_take_bit_eq_take_bit' take_bit_eq_mod) then have "(i + (k + 2 ^ (n - Suc 0))) mod 2 ^ n = (i + (l + 2 ^ (n - Suc 0))) mod 2 ^ n" for i by (metis mod_add_eq) then have "k mod 2 ^ n = l mod 2 ^ n" by (metis add_diff_cancel_right' uminus_add_conv_diff) then show ?Q by (simp add: take_bit_eq_mod) qed qed subsection \Bit strings as quotient type\ subsubsection \Basic properties\ quotient_type (overloaded) 'a word = int / "\k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len0) l" by (auto intro!: equivpI reflpI sympI transpI) instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}" begin lift_definition zero_word :: "'a word" is 0 . lift_definition one_word :: "'a word" is 1 . lift_definition plus_word :: "'a word \ 'a word \ 'a word" is plus by (subst take_bit_add [symmetric]) (simp add: take_bit_add) lift_definition uminus_word :: "'a word \ 'a word" is uminus by (subst take_bit_uminus [symmetric]) (simp add: take_bit_uminus) lift_definition minus_word :: "'a word \ 'a word \ 'a word" is minus by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus) lift_definition times_word :: "'a word \ 'a word \ 'a word" is times by (auto simp add: take_bit_eq_mod intro: mod_mult_cong) instance by standard (transfer; simp add: algebra_simps)+ end instance word :: (len) comm_ring_1 by standard (transfer; simp)+ quickcheck_generator word constructors: "zero_class.zero :: ('a::len0) word", "numeral :: num \ ('a::len0) word", "uminus :: ('a::len0) word \ ('a::len0) word" context includes lifting_syntax notes power_transfer [transfer_rule] begin lemma power_transfer_word [transfer_rule]: \(pcr_word ===> (=) ===> pcr_word) (^) (^)\ by transfer_prover end subsubsection \Conversions\ context includes lifting_syntax notes transfer_rule_of_bool [transfer_rule] transfer_rule_numeral [transfer_rule] transfer_rule_of_nat [transfer_rule] transfer_rule_of_int [transfer_rule] begin lemma [transfer_rule]: "((=) ===> (pcr_word :: int \ 'a::len word \ bool)) of_bool of_bool" by transfer_prover lemma [transfer_rule]: "((=) ===> (pcr_word :: int \ 'a::len word \ bool)) numeral numeral" by transfer_prover lemma [transfer_rule]: "((=) ===> pcr_word) int of_nat" by transfer_prover lemma [transfer_rule]: "((=) ===> pcr_word) (\k. k) of_int" proof - have "((=) ===> pcr_word) of_int of_int" by transfer_prover then show ?thesis by (simp add: id_def) qed end lemma abs_word_eq: "abs_word = of_int" by (rule ext) (transfer, rule) context semiring_1 begin lift_definition unsigned :: "'b::len0 word \ 'a" is "of_nat \ nat \ take_bit LENGTH('b)" by simp lemma unsigned_0 [simp]: "unsigned 0 = 0" by transfer simp end context semiring_char_0 begin lemma word_eq_iff_unsigned: "a = b \ unsigned a = unsigned b" by safe (transfer; simp add: eq_nat_nat_iff) end instantiation word :: (len0) equal begin definition equal_word :: "'a word \ 'a word \ bool" where "equal_word a b \ (unsigned a :: int) = unsigned b" instance proof fix a b :: "'a word" show "HOL.equal a b \ a = b" using word_eq_iff_unsigned [of a b] by (auto simp add: equal_word_def) qed end context ring_1 begin lift_definition signed :: "'b::len word \ 'a" is "of_int \ signed_take_bit (LENGTH('b) - 1)" by (simp add: signed_take_bit_eq_iff_take_bit_eq [symmetric]) lemma signed_0 [simp]: "signed 0 = 0" by transfer simp end lemma unsigned_of_nat [simp]: "unsigned (of_nat n :: 'a word) = take_bit LENGTH('a::len) n" by transfer (simp add: nat_eq_iff take_bit_eq_mod zmod_int) lemma of_nat_unsigned [simp]: "of_nat (unsigned a) = a" by transfer simp lemma of_int_unsigned [simp]: "of_int (unsigned a) = a" by transfer simp lemma unsigned_nat_less: \unsigned a < (2 ^ LENGTH('a) :: nat)\ for a :: \'a::len0 word\ by transfer (simp add: take_bit_eq_mod) lemma unsigned_int_less: \unsigned a < (2 ^ LENGTH('a) :: int)\ for a :: \'a::len0 word\ by transfer (simp add: take_bit_eq_mod) context ring_char_0 begin lemma word_eq_iff_signed: "a = b \ signed a = signed b" by safe (transfer; auto simp add: signed_take_bit_eq_iff_take_bit_eq) end lemma signed_of_int [simp]: "signed (of_int k :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) k" by transfer simp lemma of_int_signed [simp]: "of_int (signed a) = a" by transfer (simp add: signed_take_bit_eq_take_bit take_bit_eq_mod mod_simps) subsubsection \Properties\ -lemma length_cases: \ \TODO get rid of\ - obtains (triv) "LENGTH('a::len) = 1" "take_bit LENGTH('a) 2 = (0 :: int)" - | (take_bit_2) "take_bit LENGTH('a) 2 = (2 :: int)" -proof (cases "LENGTH('a) \ 2") - case False - then have "LENGTH('a) = 1" - by (auto simp add: not_le dest: less_2_cases) - then have "take_bit LENGTH('a) 2 = (0 :: int)" - by simp - with \LENGTH('a) = 1\ triv show ?thesis - by simp -next - case True - then obtain n where "LENGTH('a) = Suc (Suc n)" - by (auto dest: le_Suc_ex) - then have "take_bit LENGTH('a) 2 = (2 :: int)" - by simp - with take_bit_2 show ?thesis - by simp -qed - subsubsection \Division\ instantiation word :: (len0) modulo begin lift_definition divide_word :: "'a word \ 'a word \ 'a word" is "\a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b" by simp lift_definition modulo_word :: "'a word \ 'a word \ 'a word" is "\a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b" by simp instance .. end lemma zero_word_div_eq [simp]: \0 div a = 0\ for a :: \'a::len0 word\ by transfer simp lemma div_zero_word_eq [simp]: \a div 0 = 0\ for a :: \'a::len0 word\ by transfer simp -(*lemma - \a div a = of_bool (a \ 0)\ for a :: \'a::len word\ - by transfer simp*) - context includes lifting_syntax begin lemma [transfer_rule]: "(pcr_word ===> (\)) even ((dvd) 2 :: 'a::len word \ bool)" proof - have even_word_unfold: "even k \ (\l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \ ?Q") for k :: int proof assume ?P then show ?Q by auto next assume ?Q then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" .. then have "even (take_bit LENGTH('a) k)" by simp then show ?P by simp qed show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def]) transfer_prover qed end instance word :: (len) semiring_modulo proof show "a div b * b + a mod b = a" for a b :: "'a word" proof transfer fix k l :: int define r :: int where "r = 2 ^ LENGTH('a)" then have r: "take_bit LENGTH('a) k = k mod r" for k by (simp add: take_bit_eq_mod) have "k mod r = ((k mod r) div (l mod r) * (l mod r) + (k mod r) mod (l mod r)) mod r" by (simp add: div_mult_mod_eq) also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r + (k mod r) mod (l mod r)) mod r" by (simp add: mod_add_left_eq) also have "... = (((k mod r) div (l mod r) * l) mod r + (k mod r) mod (l mod r)) mod r" by (simp add: mod_mult_right_eq) finally have "k mod r = ((k mod r) div (l mod r) * l + (k mod r) mod (l mod r)) mod r" by (simp add: mod_simps) with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k" by simp qed qed instance word :: (len) semiring_parity proof show "\ 2 dvd (1::'a word)" by transfer simp show even_iff_mod_2_eq_0: "2 dvd a \ a mod 2 = 0" for a :: "'a word" - by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd) + by transfer (simp_all add: mod_2_eq_odd) show "\ 2 dvd a \ a mod 2 = 1" for a :: "'a word" - by (transfer; cases rule: length_cases [where ?'a = 'a]) (simp_all add: mod_2_eq_odd) + by transfer (simp_all add: mod_2_eq_odd) qed -(*lemma - \2 ^ n = (0 :: 'a word) \ LENGTH('a::len) \ n\ - apply transfer*) - - subsubsection \Orderings\ instantiation word :: (len0) linorder begin lift_definition less_eq_word :: "'a word \ 'a word \ bool" is "\a b. take_bit LENGTH('a) a \ take_bit LENGTH('a) b" by simp lift_definition less_word :: "'a word \ 'a word \ bool" is "\a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b" by simp instance by standard (transfer; auto)+ end context linordered_semidom begin lemma word_less_eq_iff_unsigned: "a \ b \ unsigned a \ unsigned b" by (transfer fixing: less_eq) (simp add: nat_le_eq_zle) lemma word_less_iff_unsigned: "a < b \ unsigned a < unsigned b" by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative]) end lemma word_greater_zero_iff: \a > 0 \ a \ 0\ for a :: \'a::len0 word\ by transfer (simp add: less_le) lemma of_nat_word_eq_iff: \of_nat m = (of_nat n :: 'a::len word) \ take_bit LENGTH('a) m = take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) lemma of_nat_word_less_eq_iff: \of_nat m \ (of_nat n :: 'a::len word) \ take_bit LENGTH('a) m \ take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) lemma of_nat_word_less_iff: \of_nat m < (of_nat n :: 'a::len word) \ take_bit LENGTH('a) m < take_bit LENGTH('a) n\ by transfer (simp add: take_bit_of_nat) lemma of_nat_word_eq_0_iff: \of_nat n = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd n\ using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) lemma of_int_word_eq_iff: \of_int k = (of_int l :: 'a::len word) \ take_bit LENGTH('a) k = take_bit LENGTH('a) l\ by transfer rule lemma of_int_word_less_eq_iff: \of_int k \ (of_int l :: 'a::len word) \ take_bit LENGTH('a) k \ take_bit LENGTH('a) l\ by transfer rule lemma of_int_word_less_iff: \of_int k < (of_int l :: 'a::len word) \ take_bit LENGTH('a) k < take_bit LENGTH('a) l\ by transfer rule lemma of_int_word_eq_0_iff: \of_int k = (0 :: 'a::len word) \ 2 ^ LENGTH('a) dvd k\ using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) subsection \Bit structure on \<^typ>\'a word\\ lemma word_bit_induct [case_names zero even odd]: \P a\ if word_zero: \P 0\ and word_even: \\a. P a \ 0 < a \ a < 2 ^ (LENGTH('a) - 1) \ P (2 * a)\ and word_odd: \\a. P a \ a < 2 ^ (LENGTH('a) - 1) \ P (1 + 2 * a)\ for P and a :: \'a::len word\ proof - define m :: nat where \m = LENGTH('a) - 1\ then have l: \LENGTH('a) = Suc m\ by simp define n :: nat where \n = unsigned a\ then have \n < 2 ^ LENGTH('a)\ by (simp add: unsigned_nat_less) then have \n < 2 * 2 ^ m\ by (simp add: l) then have \P (of_nat n)\ proof (induction n rule: nat_bit_induct) case zero show ?case by simp (rule word_zero) next case (even n) then have \n < 2 ^ m\ by simp with even.IH have \P (of_nat n)\ by simp moreover from \n < 2 ^ m\ even.hyps have \0 < (of_nat n :: 'a word)\ by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l) moreover from \n < 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\ using of_nat_word_less_iff [where ?'a = 'a, of n \2 ^ m\] by (cases \m = 0\) (simp_all add: not_less take_bit_eq_self ac_simps l) ultimately have \P (2 * of_nat n)\ by (rule word_even) then show ?case by simp next case (odd n) then have \Suc n \ 2 ^ m\ by simp with odd.IH have \P (of_nat n)\ by simp moreover from \Suc n \ 2 ^ m\ have \(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\ using of_nat_word_less_iff [where ?'a = 'a, of n \2 ^ m\] by (cases \m = 0\) (simp_all add: not_less take_bit_eq_self ac_simps l) ultimately have \P (1 + 2 * of_nat n)\ by (rule word_odd) then show ?case by simp qed then show ?thesis by (simp add: n_def) qed lemma bit_word_half_eq: \(of_bool b + a * 2) div 2 = a\ if \a < 2 ^ (LENGTH('a) - Suc 0)\ for a :: \'a::len word\ -proof (cases rule: length_cases [where ?'a = 'a]) - case triv +proof (cases \2 \ LENGTH('a::len)\) + case False have \of_bool (odd k) < (1 :: int) \ even k\ for k :: int by auto - with triv that show ?thesis + with False that show ?thesis by (auto; transfer) simp_all next - case take_bit_2 + case True obtain n where length: \LENGTH('a) = Suc n\ by (cases \LENGTH('a)\) simp_all show ?thesis proof (cases b) case False moreover have \a * 2 div 2 = a\ using that proof transfer fix k :: int from length have \k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\ by simp moreover assume \take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\ with \LENGTH('a) = Suc n\ have \k mod 2 ^ LENGTH('a) = k mod 2 ^ n\ by (simp add: take_bit_eq_mod divmod_digit_0) ultimately have \take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\ by (simp add: take_bit_eq_mod) - with take_bit_2 show \take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2) + with True show \take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2) = take_bit LENGTH('a) k\ by simp qed ultimately show ?thesis by simp next case True moreover have \(1 + a * 2) div 2 = a\ using that proof transfer fix k :: int from length have \(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\ using pos_zmod_mult_2 [of \2 ^ n\ k] by (simp add: ac_simps) moreover assume \take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\ with \LENGTH('a) = Suc n\ have \k mod 2 ^ LENGTH('a) = k mod 2 ^ n\ by (simp add: take_bit_eq_mod divmod_digit_0) ultimately have \take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\ by (simp add: take_bit_eq_mod) - with take_bit_2 show \take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2) + with True show \take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2) = take_bit LENGTH('a) k\ - by simp + by auto qed ultimately show ?thesis by simp qed qed instance word :: (len) semiring_bits proof show \P a\ if stable: \\a. a div 2 = a \ P a\ and rec: \\a b. P a \ (of_bool b + 2 * a) div 2 = a \ P (of_bool b + 2 * a)\ for P and a :: \'a word\ proof (induction a rule: word_bit_induct) case zero from stable [of 0] show ?case by simp next case (even a) with rec [of a False] show ?case using bit_word_half_eq [of a False] by (simp add: ac_simps) next case (odd a) with rec [of a True] show ?case using bit_word_half_eq [of a True] by (simp add: ac_simps) qed show \0 div a = 0\ for a :: \'a word\ by transfer simp show \a div 1 = a\ for a :: \'a word\ by transfer simp show \a mod b div b = 0\ for a b :: \'a word\ apply transfer apply (simp add: take_bit_eq_mod) apply (subst (3) mod_pos_pos_trivial [of _ \2 ^ LENGTH('a)\]) apply simp_all apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power) using pos_mod_bound [of \2 ^ LENGTH('a)\] apply simp proof - fix aa :: int and ba :: int have f1: "\i n. (i::int) mod 2 ^ n = 0 \ 0 < i mod 2 ^ n" by (metis le_less take_bit_eq_mod take_bit_nonnegative) have "(0::int) < 2 ^ len_of (TYPE('a)::'a itself) \ ba mod 2 ^ len_of (TYPE('a)::'a itself) \ 0 \ aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)" by (metis (no_types) mod_by_0 unique_euclidean_semiring_numeral_class.pos_mod_bound zero_less_numeral zero_less_power) then show "aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)" using f1 by (meson le_less less_le_trans unique_euclidean_semiring_numeral_class.pos_mod_bound) qed show \(1 + a) div 2 = a div 2\ if \even a\ for a :: \'a word\ using that by transfer (auto dest: le_Suc_ex) show \(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \ 0 \ n \ m) * 2 ^ (m - n)\ for m n :: nat by transfer (simp, simp add: exp_div_exp_eq) show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)" for a :: "'a word" and m n :: nat apply transfer apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div) apply (simp add: drop_bit_take_bit) done show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n" for a :: "'a word" and m n :: nat - apply transfer - apply (auto simp flip: take_bit_eq_mod) - apply (simp add: ac_simps) - done + by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps) show \a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\ if \m \ n\ for a :: "'a word" and m n :: nat using that apply transfer apply (auto simp flip: take_bit_eq_mod) apply (auto simp flip: push_bit_eq_mult simp add: push_bit_take_bit split: split_min_lin) done show \a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\ for a :: "'a word" and m n :: nat - apply transfer - apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin) - done + by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin) qed context includes lifting_syntax begin lemma transfer_rule_bit_word [transfer_rule]: \((pcr_word :: int \ 'a::len word \ bool) ===> (=)) (\k n. n < LENGTH('a) \ bit k n) bit\ proof - let ?t = \\a n. odd (take_bit LENGTH('a) a div take_bit LENGTH('a) ((2::int) ^ n))\ have \((pcr_word :: int \ 'a word \ bool) ===> (=)) ?t bit\ by (unfold bit_def) transfer_prover also have \?t = (\k n. n < LENGTH('a) \ bit k n)\ by (simp add: fun_eq_iff bit_take_bit_iff flip: bit_def) finally show ?thesis . qed end instantiation word :: (len) semiring_bit_shifts begin lift_definition push_bit_word :: \nat \ 'a word \ 'a word\ is push_bit proof - - show \Parity.take_bit LENGTH('a) (push_bit n k) = Parity.take_bit LENGTH('a) (push_bit n l)\ - if \Parity.take_bit LENGTH('a) k = Parity.take_bit LENGTH('a) l\ for k l :: int and n :: nat + show \take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\ + if \take_bit LENGTH('a) k = take_bit LENGTH('a) l\ for k l :: int and n :: nat proof - from that - have \Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) k) - = Parity.take_bit (LENGTH('a) - n) (Parity.take_bit LENGTH('a) l)\ + have \take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k) + = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\ by simp moreover have \min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\ by simp ultimately show ?thesis by (simp add: take_bit_push_bit) qed qed lift_definition drop_bit_word :: \nat \ 'a word \ 'a word\ is \\n. drop_bit n \ take_bit LENGTH('a)\ by (simp add: take_bit_eq_mod) instance proof show \push_bit n a = a * 2 ^ n\ for n :: nat and a :: "'a word" by transfer (simp add: push_bit_eq_mult) show \drop_bit n a = a div 2 ^ n\ for n :: nat and a :: "'a word" - proof (cases \n < LENGTH('a)\) - case True - then show ?thesis - by transfer - (simp add: take_bit_eq_mod drop_bit_eq_div) - next - case False - then obtain m where n: \n = LENGTH('a) + m\ - by (auto simp add: not_less dest: le_Suc_ex) - then show ?thesis - by transfer - (simp add: take_bit_eq_mod drop_bit_eq_div power_add zdiv_zmult2_eq) - qed + by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit) qed end instantiation word :: (len) ring_bit_operations begin lift_definition not_word :: "'a word \ 'a word" is not by (simp add: take_bit_not_iff) lift_definition and_word :: "'a word \ 'a word \ 'a word" is "and" by simp lift_definition or_word :: "'a word \ 'a word \ 'a word" is or by simp lift_definition xor_word :: "'a word \ 'a word \ 'a word" is xor by simp instance proof fix a b :: \'a word\ and n :: nat show \even (- 1 div (2 :: 'a word) ^ n) \ (2 :: 'a word) ^ n = 0\ - by transfer - (simp flip: drop_bit_eq_div add: drop_bit_take_bit, simp add: drop_bit_eq_div) + by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit) show \bit (NOT a) n \ (2 :: 'a word) ^ n \ 0 \ \ bit a n\ by transfer (simp add: bit_not_iff) show \bit (a AND b) n \ bit a n \ bit b n\ by transfer (auto simp add: bit_and_iff) show \bit (a OR b) n \ bit a n \ bit b n\ by transfer (auto simp add: bit_or_iff) show \bit (a XOR b) n \ bit a n \ bit b n\ by transfer (auto simp add: bit_xor_iff) qed end end