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 - div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+ + 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 - div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq)+ + 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/Parity.thy b/src/HOL/Parity.thy --- a/src/HOL/Parity.thy +++ b/src/HOL/Parity.thy @@ -1,1208 +1,1231 @@ (* 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]: \(\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 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_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]: \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) context fixes a assumes stable: \a div 2 = a\ begin lemma 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) 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) 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) 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) +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) +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: "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) end diff --git a/src/HOL/Transfer.thy b/src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy +++ b/src/HOL/Transfer.thy @@ -1,654 +1,666 @@ (* Title: HOL/Transfer.thy Author: Brian Huffman, TU Muenchen Author: Ondrej Kuncar, TU Muenchen *) section \Generic theorem transfer using relations\ theory Transfer imports Basic_BNF_LFPs Hilbert_Choice Metis begin subsection \Relator for function space\ bundle lifting_syntax begin notation rel_fun (infixr "===>" 55) notation map_fun (infixr "--->" 55) end context includes lifting_syntax begin lemma rel_funD2: assumes "rel_fun A B f g" and "A x x" shows "B (f x) (g x)" using assms by (rule rel_funD) lemma rel_funE: assumes "rel_fun A B f g" and "A x y" obtains "B (f x) (g y)" using assms by (simp add: rel_fun_def) lemmas rel_fun_eq = fun.rel_eq lemma rel_fun_eq_rel: shows "rel_fun (=) R = (\f g. \x. R (f x) (g x))" by (simp add: rel_fun_def) subsection \Transfer method\ text \Explicit tag for relation membership allows for backward proof methods.\ definition Rel :: "('a \ 'b \ bool) \ 'a \ 'b \ bool" where "Rel r \ r" text \Handling of equality relations\ definition is_equality :: "('a \ 'a \ bool) \ bool" where "is_equality R \ R = (=)" lemma is_equality_eq: "is_equality (=)" unfolding is_equality_def by simp text \Reverse implication for monotonicity rules\ definition rev_implies where "rev_implies x y \ (y \ x)" text \Handling of meta-logic connectives\ definition transfer_forall where "transfer_forall \ All" definition transfer_implies where "transfer_implies \ (\)" definition transfer_bforall :: "('a \ bool) \ ('a \ bool) \ bool" where "transfer_bforall \ (\P Q. \x. P x \ Q x)" lemma transfer_forall_eq: "(\x. P x) \ Trueprop (transfer_forall (\x. P x))" unfolding atomize_all transfer_forall_def .. lemma transfer_implies_eq: "(A \ B) \ Trueprop (transfer_implies A B)" unfolding atomize_imp transfer_implies_def .. lemma transfer_bforall_unfold: "Trueprop (transfer_bforall P (\x. Q x)) \ (\x. P x \ Q x)" unfolding transfer_bforall_def atomize_imp atomize_all .. lemma transfer_start: "\P; Rel (=) P Q\ \ Q" unfolding Rel_def by simp lemma transfer_start': "\P; Rel (\) P Q\ \ Q" unfolding Rel_def by simp lemma transfer_prover_start: "\x = x'; Rel R x' y\ \ Rel R x y" by simp lemma untransfer_start: "\Q; Rel (=) P Q\ \ P" unfolding Rel_def by simp lemma Rel_eq_refl: "Rel (=) x x" unfolding Rel_def .. lemma Rel_app: assumes "Rel (A ===> B) f g" and "Rel A x y" shows "Rel B (f x) (g y)" using assms unfolding Rel_def rel_fun_def by fast lemma Rel_abs: assumes "\x y. Rel A x y \ Rel B (f x) (g y)" shows "Rel (A ===> B) (\x. f x) (\y. g y)" using assms unfolding Rel_def rel_fun_def by fast subsection \Predicates on relations, i.e. ``class constraints''\ definition left_total :: "('a \ 'b \ bool) \ bool" where "left_total R \ (\x. \y. R x y)" definition left_unique :: "('a \ 'b \ bool) \ bool" where "left_unique R \ (\x y z. R x z \ R y z \ x = y)" definition right_total :: "('a \ 'b \ bool) \ bool" where "right_total R \ (\y. \x. R x y)" definition right_unique :: "('a \ 'b \ bool) \ bool" where "right_unique R \ (\x y z. R x y \ R x z \ y = z)" definition bi_total :: "('a \ 'b \ bool) \ bool" where "bi_total R \ (\x. \y. R x y) \ (\y. \x. R x y)" definition bi_unique :: "('a \ 'b \ bool) \ bool" where "bi_unique R \ (\x y z. R x y \ R x z \ y = z) \ (\x y z. R x z \ R y z \ x = y)" lemma left_uniqueI: "(\x y z. \ A x z; A y z \ \ x = y) \ left_unique A" unfolding left_unique_def by blast lemma left_uniqueD: "\ left_unique A; A x z; A y z \ \ x = y" unfolding left_unique_def by blast lemma left_totalI: "(\x. \y. R x y) \ left_total R" unfolding left_total_def by blast lemma left_totalE: assumes "left_total R" obtains "(\x. \y. R x y)" using assms unfolding left_total_def by blast lemma bi_uniqueDr: "\ bi_unique A; A x y; A x z \ \ y = z" by(simp add: bi_unique_def) lemma bi_uniqueDl: "\ bi_unique A; A x y; A z y \ \ x = z" by(simp add: bi_unique_def) lemma right_uniqueI: "(\x y z. \ A x y; A x z \ \ y = z) \ right_unique A" unfolding right_unique_def by fast lemma right_uniqueD: "\ right_unique A; A x y; A x z \ \ y = z" unfolding right_unique_def by fast lemma right_totalI: "(\y. \x. A x y) \ right_total A" by(simp add: right_total_def) lemma right_totalE: assumes "right_total A" obtains x where "A x y" using assms by(auto simp add: right_total_def) lemma right_total_alt_def2: "right_total R \ ((R ===> (\)) ===> (\)) All All" unfolding right_total_def rel_fun_def apply (rule iffI, fast) apply (rule allI) apply (drule_tac x="\x. True" in spec) apply (drule_tac x="\y. \x. R x y" in spec) apply fast done lemma right_unique_alt_def2: "right_unique R \ (R ===> R ===> (\)) (=) (=)" unfolding right_unique_def rel_fun_def by auto lemma bi_total_alt_def2: "bi_total R \ ((R ===> (=)) ===> (=)) All All" unfolding bi_total_def rel_fun_def apply (rule iffI, fast) apply safe apply (drule_tac x="\x. \y. R x y" in spec) apply (drule_tac x="\y. True" in spec) apply fast apply (drule_tac x="\x. True" in spec) apply (drule_tac x="\y. \x. R x y" in spec) apply fast done lemma bi_unique_alt_def2: "bi_unique R \ (R ===> R ===> (=)) (=) (=)" unfolding bi_unique_def rel_fun_def by auto lemma [simp]: shows left_unique_conversep: "left_unique A\\ \ right_unique A" and right_unique_conversep: "right_unique A\\ \ left_unique A" by(auto simp add: left_unique_def right_unique_def) lemma [simp]: shows left_total_conversep: "left_total A\\ \ right_total A" and right_total_conversep: "right_total A\\ \ left_total A" by(simp_all add: left_total_def right_total_def) lemma bi_unique_conversep [simp]: "bi_unique R\\ = bi_unique R" by(auto simp add: bi_unique_def) lemma bi_total_conversep [simp]: "bi_total R\\ = bi_total R" by(auto simp add: bi_total_def) lemma right_unique_alt_def: "right_unique R = (conversep R OO R \ (=))" unfolding right_unique_def by blast lemma left_unique_alt_def: "left_unique R = (R OO (conversep R) \ (=))" unfolding left_unique_def by blast lemma right_total_alt_def: "right_total R = (conversep R OO R \ (=))" unfolding right_total_def by blast lemma left_total_alt_def: "left_total R = (R OO conversep R \ (=))" unfolding left_total_def by blast lemma bi_total_alt_def: "bi_total A = (left_total A \ right_total A)" unfolding left_total_def right_total_def bi_total_def by blast lemma bi_unique_alt_def: "bi_unique A = (left_unique A \ right_unique A)" unfolding left_unique_def right_unique_def bi_unique_def by blast lemma bi_totalI: "left_total R \ right_total R \ bi_total R" unfolding bi_total_alt_def .. lemma bi_uniqueI: "left_unique R \ right_unique R \ bi_unique R" unfolding bi_unique_alt_def .. end lemma is_equality_lemma: "(\R. is_equality R \ PROP (P R)) \ PROP (P (=))" apply (unfold is_equality_def) apply (rule equal_intr_rule) apply (drule meta_spec) apply (erule meta_mp) apply (rule refl) apply simp done lemma Domainp_lemma: "(\R. Domainp T = R \ PROP (P R)) \ PROP (P (Domainp T))" apply (rule equal_intr_rule) apply (drule meta_spec) apply (erule meta_mp) apply (rule refl) apply simp done ML_file \Tools/Transfer/transfer.ML\ declare refl [transfer_rule] hide_const (open) Rel context includes lifting_syntax begin text \Handling of domains\ lemma Domainp_iff: "Domainp T x \ (\y. T x y)" by auto lemma Domainp_refl[transfer_domain_rule]: "Domainp T = Domainp T" .. lemma Domain_eq_top[transfer_domain_rule]: "Domainp (=) = top" by auto lemma Domainp_pred_fun_eq[relator_domain]: assumes "left_unique T" shows "Domainp (T ===> S) = pred_fun (Domainp T) (Domainp S)" using assms unfolding rel_fun_def Domainp_iff[abs_def] left_unique_def fun_eq_iff pred_fun_def apply safe apply blast apply (subst all_comm) apply (rule choice) apply blast done text \Properties are preserved by relation composition.\ lemma OO_def: "R OO S = (\x z. \y. R x y \ S y z)" by auto lemma bi_total_OO: "\bi_total A; bi_total B\ \ bi_total (A OO B)" unfolding bi_total_def OO_def by fast lemma bi_unique_OO: "\bi_unique A; bi_unique B\ \ bi_unique (A OO B)" unfolding bi_unique_def OO_def by blast lemma right_total_OO: "\right_total A; right_total B\ \ right_total (A OO B)" unfolding right_total_def OO_def by fast lemma right_unique_OO: "\right_unique A; right_unique B\ \ right_unique (A OO B)" unfolding right_unique_def OO_def by fast lemma left_total_OO: "left_total R \ left_total S \ left_total (R OO S)" unfolding left_total_def OO_def by fast lemma left_unique_OO: "left_unique R \ left_unique S \ left_unique (R OO S)" unfolding left_unique_def OO_def by blast subsection \Properties of relators\ lemma left_total_eq[transfer_rule]: "left_total (=)" unfolding left_total_def by blast lemma left_unique_eq[transfer_rule]: "left_unique (=)" unfolding left_unique_def by blast lemma right_total_eq [transfer_rule]: "right_total (=)" unfolding right_total_def by simp lemma right_unique_eq [transfer_rule]: "right_unique (=)" unfolding right_unique_def by simp lemma bi_total_eq[transfer_rule]: "bi_total (=)" unfolding bi_total_def by simp lemma bi_unique_eq[transfer_rule]: "bi_unique (=)" unfolding bi_unique_def by simp lemma left_total_fun[transfer_rule]: "\left_unique A; left_total B\ \ left_total (A ===> B)" unfolding left_total_def rel_fun_def apply (rule allI, rename_tac f) apply (rule_tac x="\y. SOME z. B (f (THE x. A x y)) z" in exI) apply clarify apply (subgoal_tac "(THE x. A x y) = x", simp) apply (rule someI_ex) apply (simp) apply (rule the_equality) apply assumption apply (simp add: left_unique_def) done lemma left_unique_fun[transfer_rule]: "\left_total A; left_unique B\ \ left_unique (A ===> B)" unfolding left_total_def left_unique_def rel_fun_def by (clarify, rule ext, fast) lemma right_total_fun [transfer_rule]: "\right_unique A; right_total B\ \ right_total (A ===> B)" unfolding right_total_def rel_fun_def apply (rule allI, rename_tac g) apply (rule_tac x="\x. SOME z. B z (g (THE y. A x y))" in exI) apply clarify apply (subgoal_tac "(THE y. A x y) = y", simp) apply (rule someI_ex) apply (simp) apply (rule the_equality) apply assumption apply (simp add: right_unique_def) done lemma right_unique_fun [transfer_rule]: "\right_total A; right_unique B\ \ right_unique (A ===> B)" unfolding right_total_def right_unique_def rel_fun_def by (clarify, rule ext, fast) lemma bi_total_fun[transfer_rule]: "\bi_unique A; bi_total B\ \ bi_total (A ===> B)" unfolding bi_unique_alt_def bi_total_alt_def by (blast intro: right_total_fun left_total_fun) lemma bi_unique_fun[transfer_rule]: "\bi_total A; bi_unique B\ \ bi_unique (A ===> B)" unfolding bi_unique_alt_def bi_total_alt_def by (blast intro: right_unique_fun left_unique_fun) end lemma if_conn: "(if P \ Q then t else e) = (if P then if Q then t else e else e)" "(if P \ Q then t else e) = (if P then t else if Q then t else e)" "(if P \ Q then t else e) = (if P then if Q then t else e else t)" "(if \ P then t else e) = (if P then e else t)" by auto ML_file \Tools/Transfer/transfer_bnf.ML\ ML_file \Tools/BNF/bnf_fp_rec_sugar_transfer.ML\ declare pred_fun_def [simp] declare rel_fun_eq [relator_eq] (* Delete the automated generated rule from the bnf command; we have a more general rule (Domainp_pred_fun_eq) that subsumes it. *) declare fun.Domainp_rel[relator_domain del] subsection \Transfer rules\ context includes lifting_syntax begin lemma Domainp_forall_transfer [transfer_rule]: assumes "right_total A" shows "((A ===> (=)) ===> (=)) (transfer_bforall (Domainp A)) transfer_forall" using assms unfolding right_total_def unfolding transfer_forall_def transfer_bforall_def rel_fun_def Domainp_iff by fast text \Transfer rules using implication instead of equality on booleans.\ lemma transfer_forall_transfer [transfer_rule]: "bi_total A \ ((A ===> (=)) ===> (=)) transfer_forall transfer_forall" "right_total A \ ((A ===> (=)) ===> implies) transfer_forall transfer_forall" "right_total A \ ((A ===> implies) ===> implies) transfer_forall transfer_forall" "bi_total A \ ((A ===> (=)) ===> rev_implies) transfer_forall transfer_forall" "bi_total A \ ((A ===> rev_implies) ===> rev_implies) transfer_forall transfer_forall" unfolding transfer_forall_def rev_implies_def rel_fun_def right_total_def bi_total_def by fast+ lemma transfer_implies_transfer [transfer_rule]: "((=) ===> (=) ===> (=) ) transfer_implies transfer_implies" "(rev_implies ===> implies ===> implies ) transfer_implies transfer_implies" "(rev_implies ===> (=) ===> implies ) transfer_implies transfer_implies" "((=) ===> implies ===> implies ) transfer_implies transfer_implies" "((=) ===> (=) ===> implies ) transfer_implies transfer_implies" "(implies ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" "(implies ===> (=) ===> rev_implies) transfer_implies transfer_implies" "((=) ===> rev_implies ===> rev_implies) transfer_implies transfer_implies" "((=) ===> (=) ===> rev_implies) transfer_implies transfer_implies" unfolding transfer_implies_def rev_implies_def rel_fun_def by auto lemma eq_imp_transfer [transfer_rule]: "right_unique A \ (A ===> A ===> (\)) (=) (=)" unfolding right_unique_alt_def2 . text \Transfer rules using equality.\ lemma left_unique_transfer [transfer_rule]: assumes "right_total A" assumes "right_total B" assumes "bi_unique A" shows "((A ===> B ===> (=)) ===> implies) left_unique left_unique" using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def by metis lemma eq_transfer [transfer_rule]: assumes "bi_unique A" shows "(A ===> A ===> (=)) (=) (=)" using assms unfolding bi_unique_def rel_fun_def by auto lemma right_total_Ex_transfer[transfer_rule]: assumes "right_total A" shows "((A ===> (=)) ===> (=)) (Bex (Collect (Domainp A))) Ex" using assms unfolding right_total_def Bex_def rel_fun_def Domainp_iff[abs_def] by fast lemma right_total_All_transfer[transfer_rule]: assumes "right_total A" shows "((A ===> (=)) ===> (=)) (Ball (Collect (Domainp A))) All" using assms unfolding right_total_def Ball_def rel_fun_def Domainp_iff[abs_def] by fast context includes lifting_syntax begin lemma right_total_fun_eq_transfer: assumes [transfer_rule]: "right_total A" "bi_unique B" shows "((A ===> B) ===> (A ===> B) ===> (=)) (\f g. \x\Collect(Domainp A). f x = g x) (=)" unfolding fun_eq_iff by transfer_prover end lemma All_transfer [transfer_rule]: assumes "bi_total A" shows "((A ===> (=)) ===> (=)) All All" using assms unfolding bi_total_def rel_fun_def by fast lemma Ex_transfer [transfer_rule]: assumes "bi_total A" shows "((A ===> (=)) ===> (=)) Ex Ex" using assms unfolding bi_total_def rel_fun_def by fast lemma Ex1_parametric [transfer_rule]: assumes [transfer_rule]: "bi_unique A" "bi_total A" shows "((A ===> (=)) ===> (=)) Ex1 Ex1" unfolding Ex1_def[abs_def] by transfer_prover declare If_transfer [transfer_rule] lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let" unfolding rel_fun_def by simp declare id_transfer [transfer_rule] declare comp_transfer [transfer_rule] lemma curry_transfer [transfer_rule]: "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry" unfolding curry_def by transfer_prover lemma fun_upd_transfer [transfer_rule]: assumes [transfer_rule]: "bi_unique A" shows "((A ===> B) ===> A ===> B ===> A ===> B) fun_upd fun_upd" unfolding fun_upd_def [abs_def] by transfer_prover lemma case_nat_transfer [transfer_rule]: "(A ===> ((=) ===> A) ===> (=) ===> A) case_nat case_nat" unfolding rel_fun_def by (simp split: nat.split) lemma rec_nat_transfer [transfer_rule]: "(A ===> ((=) ===> A ===> A) ===> (=) ===> A) rec_nat rec_nat" unfolding rel_fun_def by (clarsimp, rename_tac n, induct_tac n, simp_all) lemma funpow_transfer [transfer_rule]: "((=) ===> (A ===> A) ===> (A ===> A)) compow compow" unfolding funpow_def by transfer_prover lemma mono_transfer[transfer_rule]: assumes [transfer_rule]: "bi_total A" assumes [transfer_rule]: "(A ===> A ===> (=)) (\) (\)" assumes [transfer_rule]: "(B ===> B ===> (=)) (\) (\)" shows "((A ===> B) ===> (=)) mono mono" unfolding mono_def[abs_def] by transfer_prover lemma right_total_relcompp_transfer[transfer_rule]: assumes [transfer_rule]: "right_total B" shows "((A ===> B ===> (=)) ===> (B ===> C ===> (=)) ===> A ===> C ===> (=)) (\R S x z. \y\Collect (Domainp B). R x y \ S y z) (OO)" unfolding OO_def[abs_def] by transfer_prover lemma relcompp_transfer[transfer_rule]: assumes [transfer_rule]: "bi_total B" shows "((A ===> B ===> (=)) ===> (B ===> C ===> (=)) ===> A ===> C ===> (=)) (OO) (OO)" unfolding OO_def[abs_def] by transfer_prover lemma right_total_Domainp_transfer[transfer_rule]: assumes [transfer_rule]: "right_total B" shows "((A ===> B ===> (=)) ===> A ===> (=)) (\T x. \y\Collect(Domainp B). T x y) Domainp" apply(subst(2) Domainp_iff[abs_def]) by transfer_prover lemma Domainp_transfer[transfer_rule]: assumes [transfer_rule]: "bi_total B" shows "((A ===> B ===> (=)) ===> A ===> (=)) Domainp Domainp" unfolding Domainp_iff[abs_def] by transfer_prover lemma reflp_transfer[transfer_rule]: "bi_total A \ ((A ===> A ===> (=)) ===> (=)) reflp reflp" "right_total A \ ((A ===> A ===> implies) ===> implies) reflp reflp" "right_total A \ ((A ===> A ===> (=)) ===> implies) reflp reflp" "bi_total A \ ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp" "bi_total A \ ((A ===> A ===> (=)) ===> rev_implies) reflp reflp" unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def by fast+ lemma right_unique_transfer [transfer_rule]: "\ right_total A; right_total B; bi_unique B \ \ ((A ===> B ===> (=)) ===> implies) right_unique right_unique" unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def by metis lemma left_total_parametric [transfer_rule]: assumes [transfer_rule]: "bi_total A" "bi_total B" shows "((A ===> B ===> (=)) ===> (=)) left_total left_total" unfolding left_total_def[abs_def] by transfer_prover lemma right_total_parametric [transfer_rule]: assumes [transfer_rule]: "bi_total A" "bi_total B" shows "((A ===> B ===> (=)) ===> (=)) right_total right_total" unfolding right_total_def[abs_def] by transfer_prover lemma left_unique_parametric [transfer_rule]: assumes [transfer_rule]: "bi_unique A" "bi_total A" "bi_total B" shows "((A ===> B ===> (=)) ===> (=)) left_unique left_unique" unfolding left_unique_def[abs_def] by transfer_prover lemma prod_pred_parametric [transfer_rule]: "((A ===> (=)) ===> (B ===> (=)) ===> rel_prod A B ===> (=)) pred_prod pred_prod" unfolding prod.pred_set[abs_def] Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps by simp transfer_prover lemma apfst_parametric [transfer_rule]: "((A ===> B) ===> rel_prod A C ===> rel_prod B C) apfst apfst" unfolding apfst_def[abs_def] by transfer_prover lemma rel_fun_eq_eq_onp: "((=) ===> eq_onp P) = eq_onp (\f. \x. P(f x))" unfolding eq_onp_def rel_fun_def by auto lemma rel_fun_eq_onp_rel: shows "((eq_onp R) ===> S) = (\f g. \x. R x \ S (f x) (g x))" by (auto simp add: eq_onp_def rel_fun_def) lemma eq_onp_transfer [transfer_rule]: assumes [transfer_rule]: "bi_unique A" shows "((A ===> (=)) ===> A ===> A ===> (=)) eq_onp eq_onp" unfolding eq_onp_def[abs_def] by transfer_prover lemma rtranclp_parametric [transfer_rule]: assumes "bi_unique A" "bi_total A" shows "((A ===> A ===> (=)) ===> A ===> A ===> (=)) rtranclp rtranclp" proof(rule rel_funI iffI)+ fix R :: "'a \ 'a \ bool" and R' x y x' y' assume R: "(A ===> A ===> (=)) R R'" and "A x x'" { assume "R\<^sup>*\<^sup>* x y" "A y y'" thus "R'\<^sup>*\<^sup>* x' y'" proof(induction arbitrary: y') case base with \bi_unique A\ \A x x'\ have "x' = y'" by(rule bi_uniqueDr) thus ?case by simp next case (step y z z') from \bi_total A\ obtain y' where "A y y'" unfolding bi_total_def by blast hence "R'\<^sup>*\<^sup>* x' y'" by(rule step.IH) moreover from R \A y y'\ \A z z'\ \R y z\ have "R' y' z'" by(auto dest: rel_funD) ultimately show ?case .. qed next assume "R'\<^sup>*\<^sup>* x' y'" "A y y'" thus "R\<^sup>*\<^sup>* x y" proof(induction arbitrary: y) case base with \bi_unique A\ \A x x'\ have "x = y" by(rule bi_uniqueDl) thus ?case by simp next case (step y' z' z) from \bi_total A\ obtain y where "A y y'" unfolding bi_total_def by blast hence "R\<^sup>*\<^sup>* x y" by(rule step.IH) moreover from R \A y y'\ \A z z'\ \R' y' z'\ have "R y z" by(auto dest: rel_funD) ultimately show ?case .. qed } qed lemma right_unique_parametric [transfer_rule]: assumes [transfer_rule]: "bi_total A" "bi_unique B" "bi_total B" shows "((A ===> B ===> (=)) ===> (=)) right_unique right_unique" unfolding right_unique_def[abs_def] by transfer_prover lemma map_fun_parametric [transfer_rule]: "((A ===> B) ===> (C ===> D) ===> (B ===> C) ===> A ===> D) map_fun map_fun" unfolding map_fun_def[abs_def] by transfer_prover end -subsection \\<^const>\of_nat\\ +subsection \\<^const>\of_bool\ and \<^const>\of_nat\\ + +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 lemma transfer_rule_of_nat: - fixes R :: "'a::semiring_1 \ 'b::semiring_1 \ bool" - assumes [transfer_rule]: "R 0 0" "R 1 1" - "rel_fun R (rel_fun R R) plus plus" - shows "rel_fun HOL.eq R of_nat of_nat" + "((=) ===> (\)) of_nat of_nat" + if [transfer_rule]: \0 \ 0\ \1 \ 1\ + \((\) ===> (\) ===> (\)) (+) (+)\ + for R :: \'a::semiring_1 \ 'b::semiring_1 \ bool\ (infix \\\ 50) by (unfold of_nat_def [abs_def]) transfer_prover end + +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,728 +1,737 @@ (* 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 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_numeral [transfer_rule] + 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 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) 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) qed 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 have \of_bool (odd k) < (1 :: int) \ even k\ for k :: int by auto with triv that show ?thesis by (auto; transfer) simp_all next case take_bit_2 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) = 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) = take_bit LENGTH('a) k\ by simp 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 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 qed 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 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)\ 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 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 interpret bit_word: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: 'a word" proof show "a AND (b OR c) = a AND b OR a AND c" for a b c :: "'a word" by transfer (simp add: bit.conj_disj_distrib) show "a OR b AND c = (a OR b) AND (a OR c)" for a b c :: "'a word" by transfer (simp add: bit.disj_conj_distrib) qed (transfer; simp add: ac_simps)+ show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: 'a word)" by (fact bit_word.boolean_algebra_axioms) show "bit_word.xor = ((XOR) :: 'a word \ _)" proof (rule ext)+ fix a b :: "'a word" have "a XOR b = a AND NOT b OR NOT a AND b" by transfer (simp add: bit.xor_def) then show "bit_word.xor a b = a XOR b" by (simp add: bit_word.xor_def) qed qed end end