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,1150 +1,1176 @@ (* 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) -lemma [transfer_rule]: - "rel_fun (=) (rel_fun pcr_integer pcr_integer) (push_bit :: _ \ _ \ int) (push_bit :: _ \ _ \ integer)" - by (unfold push_bit_eq_mult [abs_def]) transfer_prover +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_split_eq bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div)+ + +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 -lemma [transfer_rule]: - "rel_fun (=) (rel_fun pcr_integer pcr_integer) (drop_bit :: _ \ _ \ int) (drop_bit :: _ \ _ \ integer)" - by (unfold drop_bit_eq_div [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 -lemma [transfer_rule]: - "rel_fun (=) (rel_fun pcr_natural pcr_natural) (push_bit :: _ \ _ \ nat) (push_bit :: _ \ _ \ natural)" - by (unfold push_bit_eq_mult [abs_def]) transfer_prover +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_split_eq bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div)+ + +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 -lemma [transfer_rule]: - "rel_fun (=) (rel_fun pcr_natural pcr_natural) (drop_bit :: _ \ _ \ nat) (drop_bit :: _ \ _ \ natural)" - by (unfold drop_bit_eq_div [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,1104 +1,1216 @@ (* 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 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\ class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring + assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n" and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1" and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a" begin lemma division_segment_eq_iff: "a = b" if "division_segment a = division_segment b" and "euclidean_size a = euclidean_size b" using that division_segment_euclidean_size [of a] by simp lemma euclidean_size_of_nat [simp]: "euclidean_size (of_nat n) = n" proof - have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n" by (fact division_segment_euclidean_size) then show ?thesis by simp qed lemma of_nat_euclidean_size: "of_nat (euclidean_size a) = a div division_segment a" proof - have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a" by (subst nonzero_mult_div_cancel_left) simp_all also have "\ = a div division_segment a" by simp finally show ?thesis . qed lemma division_segment_1 [simp]: "division_segment 1 = 1" using division_segment_of_nat [of 1] by simp lemma division_segment_numeral [simp]: "division_segment (numeral k) = 1" using division_segment_of_nat [of "numeral k"] by simp lemma euclidean_size_1 [simp]: "euclidean_size 1 = 1" using euclidean_size_of_nat [of 1] by simp lemma euclidean_size_numeral [simp]: "euclidean_size (numeral k) = numeral k" using euclidean_size_of_nat [of "numeral k"] by simp lemma of_nat_dvd_iff: "of_nat m dvd of_nat n \ m dvd n" (is "?P \ ?Q") proof (cases "m = 0") case True then show ?thesis by simp next case False show ?thesis proof assume ?Q then show ?P by auto next assume ?P with False have "of_nat n = of_nat n div of_nat m * of_nat m" by simp then have "of_nat n = of_nat (n div m * m)" by (simp add: of_nat_div) then have "n = n div m * m" by (simp only: of_nat_eq_iff) then have "n = m * (n div m)" by (simp add: ac_simps) then show ?Q .. qed qed lemma of_nat_mod: "of_nat (m mod n) = of_nat m mod of_nat n" proof - have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m" by (simp add: div_mult_mod_eq) also have "of_nat m = of_nat (m div n * n + m mod n)" by simp finally show ?thesis by (simp only: of_nat_div of_nat_mult of_nat_add) simp qed lemma one_div_two_eq_zero [simp]: "1 div 2 = 0" proof - from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0" by (simp only:) simp then show ?thesis by simp qed lemma one_mod_two_eq_one [simp]: "1 mod 2 = 1" proof - from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1" by (simp only:) simp then show ?thesis by simp qed 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 one_mod_2_pow_eq [simp]: "1 mod (2 ^ n) = of_bool (n > 0)" proof - have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))" using of_nat_mod [of 1 "2 ^ n"] by simp also have "\ = of_bool (n > 0)" by simp finally show ?thesis . qed lemma one_div_2_pow_eq [simp]: "1 div (2 ^ n) = of_bool (n = 0)" using div_mult_mod_eq [of 1 "2 ^ n"] by auto 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) lemma div_mult2_eq': "a div (of_nat m * of_nat n) = a div of_nat m div of_nat n" proof (cases a "of_nat m * of_nat n" rule: divmod_cases) case (divides q) then show ?thesis using nonzero_mult_div_cancel_right [of "of_nat m" "q * of_nat n"] by (simp add: ac_simps) next case (remainder q r) then have "division_segment r = 1" using division_segment_of_nat [of "m * n"] by simp with division_segment_euclidean_size [of r] have "of_nat (euclidean_size r) = r" by simp have "a mod (of_nat m * of_nat n) div (of_nat m * of_nat n) = 0" by simp with remainder(6) have "r div (of_nat m * of_nat n) = 0" by simp with \of_nat (euclidean_size r) = r\ have "of_nat (euclidean_size r) div (of_nat m * of_nat n) = 0" by simp then have "of_nat (euclidean_size r div (m * n)) = 0" by (simp add: of_nat_div) then have "of_nat (euclidean_size r div m div n) = 0" by (simp add: div_mult2_eq) with \of_nat (euclidean_size r) = r\ have "r div of_nat m div of_nat n = 0" by (simp add: of_nat_div) with remainder(1) have "q = (r div of_nat m + q * of_nat n * of_nat m div of_nat m) div of_nat n" by simp with remainder(5) remainder(7) show ?thesis using div_plus_div_distrib_dvd_right [of "of_nat m" "q * (of_nat m * of_nat n)" r] by (simp add: ac_simps) next case by0 then show ?thesis by auto qed lemma mod_mult2_eq': "a mod (of_nat m * of_nat n) = of_nat m * (a div of_nat m mod of_nat n) + a mod of_nat m" proof - have "a div (of_nat m * of_nat n) * (of_nat m * of_nat n) + a mod (of_nat m * of_nat n) = a div of_nat m div of_nat n * of_nat n * of_nat m + (a div of_nat m mod of_nat n * of_nat m + a mod of_nat m)" by (simp add: combine_common_factor div_mult_mod_eq) moreover have "a div of_nat m div of_nat n * of_nat n * of_nat m = of_nat n * of_nat m * (a div of_nat m div of_nat n)" by (simp add: ac_simps) ultimately show ?thesis by (simp add: div_mult2_eq' mult_commute) qed lemma div_mult2_numeral_eq: "a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B") proof - have "?A = a div of_nat (numeral k) div of_nat (numeral l)" by simp also have "\ = a div (of_nat (numeral k) * of_nat (numeral l))" by (fact div_mult2_eq' [symmetric]) also have "\ = ?B" by simp finally show ?thesis . qed lemma numeral_Bit0_div_2: "numeral (num.Bit0 n) div 2 = numeral n" proof - have "numeral (num.Bit0 n) = numeral n + numeral n" by (simp only: numeral.simps) also have "\ = numeral n * 2" by (simp add: mult_2_right) finally have "numeral (num.Bit0 n) div 2 = numeral n * 2 div 2" by simp also have "\ = numeral n" by (rule nonzero_mult_div_cancel_right) simp finally show ?thesis . qed lemma numeral_Bit1_div_2: "numeral (num.Bit1 n) div 2 = numeral n" proof - have "numeral (num.Bit1 n) = numeral n + numeral n + 1" by (simp only: numeral.simps) also have "\ = numeral n * 2 + 1" by (simp add: mult_2_right) finally have "numeral (num.Bit1 n) div 2 = (numeral n * 2 + 1) div 2" by simp also have "\ = numeral n * 2 div 2 + 1 div 2" using dvd_triv_right by (rule div_plus_div_distrib_dvd_left) also have "\ = numeral n * 2 div 2" by simp also have "\ = numeral n" by (rule nonzero_mult_div_cancel_right) simp finally show ?thesis . qed end class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_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 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 - 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\\ instance int :: unique_euclidean_ring_with_nat by standard (simp_all add: dvd_eq_mod_eq_0 divide_int_def division_segment_int_def) 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]) + +subsection \Abstract bit shifts\ + +class semiring_bits = semiring_parity + + assumes bit_split_eq: \\a. of_bool (odd a) + 2 * (a div 2) = a\ + and bit_eq_rec: \\a b. a = b \ (even a = even b) \ a div 2 = b div 2\ + and 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\ + +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 \of_bool (odd n) + 2 * (n div 2) = n\ + for n :: nat + by simp + show \m = n \ (even m \ even n) \ m div 2 = n div 2\ + for m n :: nat + by (auto dest: odd_two_times_div_two_succ) + 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 +qed + 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 \of_bool (odd k) + 2 * (k div 2) = k\ + for k :: int + by (auto elim: oddE) + show \k = l \ (even k \ even l) \ k div 2 = l div 2\ + for k l :: int + by (auto dest: odd_two_times_div_two_succ) + 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 +qed -subsection \Abstract bit operations\ - -context semiring_parity +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 -text \The primary purpose of the following operations is - to avoid ad-hoc simplification of concrete expressions \<^term>\2 ^ n\\ +definition take_bit :: \nat \ 'a \ 'a\ + where take_bit_eq_mod: \take_bit n a = a mod 2 ^ n\ -definition push_bit :: "nat \ 'a \ 'a" - where push_bit_eq_mult: "push_bit n a = a * 2 ^ n" - -definition take_bit :: "nat \ 'a \ 'a" - where take_bit_eq_mod: "take_bit n a = a mod 2 ^ n" - -definition drop_bit :: "nat \ 'a \ 'a" - where drop_bit_eq_div: "drop_bit n a = a div 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. +\ end -context unique_euclidean_semiring_with_nat +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 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 take_bit_take_bit [simp]: "take_bit m (take_bit n a) = take_bit (min m n) a" proof (cases "m \ n") case True then show ?thesis by (simp add: take_bit_eq_mod not_le min_def mod_mod_cancel le_imp_power_dvd) next case False then have "n < m" and "min m n = n" by simp_all then have "2 ^ m = of_nat (2 ^ n) * of_nat (2 ^ (m - n))" by (simp add: power_add [symmetric]) then have "a mod 2 ^ n mod 2 ^ m = a mod 2 ^ n mod (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))" by simp also have "\ = of_nat (2 ^ n) * (a mod 2 ^ n div of_nat (2 ^ n) mod of_nat (2 ^ (m - n))) + a mod 2 ^ n mod of_nat (2 ^ n)" by (simp only: mod_mult2_eq') finally show ?thesis using \min m n = n\ by (simp add: take_bit_eq_mod) qed lemma drop_bit_drop_bit [simp]: "drop_bit m (drop_bit n a) = drop_bit (m + n) a" proof - have "a div (2 ^ m * 2 ^ n) = a div (of_nat (2 ^ n) * of_nat (2 ^ m))" by (simp add: ac_simps) also have "\ = a div of_nat (2 ^ n) div of_nat (2 ^ m)" by (simp only: div_mult2_eq') finally show ?thesis by (simp add: drop_bit_eq_div power_add) qed lemma push_bit_take_bit: "push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)" by (simp add: push_bit_eq_mult take_bit_eq_mod power_add mult_mod_right ac_simps) 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 by (simp_all add: push_bit_eq_mult take_bit_eq_mod mod_eq_0_iff_dvd dvd_power_le) 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)" using mod_mult2_eq' [of a "2 ^ n" "2 ^ m"] by (simp add: drop_bit_eq_div take_bit_eq_mod power_add ac_simps) 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 have "a mod 2 ^ n div 2 ^ m = a mod 2 ^ n div 2 ^ (n + (m - n))" by simp also have "\ = a mod 2 ^ n div (2 ^ n * 2 ^ (m - n))" by (simp add: power_add) also have "\ = a mod 2 ^ n div (of_nat (2 ^ n) * of_nat (2 ^ (m - n)))" by simp also have "\ = a mod 2 ^ n div of_nat (2 ^ n) div of_nat (2 ^ (m - n))" by (simp only: div_mult2_eq') finally show ?thesis using False by (simp add: take_bit_eq_mod drop_bit_eq_div) qed 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_eq_0_iff [simp]: "push_bit n a = 0 \ a = 0" by (simp add: push_bit_eq_mult) 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 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_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 "1 + 2 * (a div 2) mod (2 * 2 ^ n) = (a div 2 * 2 + a mod 2) mod (2 * 2 ^ n)" if "odd a" using that mod_mult2_eq' [of "1 + 2 * (a div 2)" 2 "2 ^ n"] by (simp add: ac_simps odd_iff_mod_2_eq_one mult_mod_right) also have "\ = a mod (2 * 2 ^ n)" by (simp only: div_mult_mod_eq) finally show ?thesis by (simp add: take_bit_eq_mod algebra_simps mult_mod_right) 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 (simp add: take_bit_eq_mod) 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 even_take_bit_eq [simp]: "even (take_bit n a) \ n = 0 \ even a" by (cases n) (simp_all add: take_bit_eq_mod dvd_mod_iff) 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_0 [simp]: "drop_bit 0 = id" by (simp add: fun_eq_iff drop_bit_eq_div) 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_Suc [simp]: "drop_bit (Suc n) a = drop_bit n (a div 2)" proof (cases "even a") case True then obtain b where "a = 2 * b" .. moreover have "drop_bit (Suc n) (2 * b) = drop_bit n b" by (simp add: drop_bit_eq_div) ultimately show ?thesis by simp next case False then obtain b where "a = 2 * b + 1" .. moreover have "drop_bit (Suc n) (2 * b + 1) = drop_bit n b" using div_mult2_eq' [of "1 + b * 2" 2 "2 ^ n"] by (auto simp add: drop_bit_eq_div ac_simps) ultimately show ?thesis by simp qed 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 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/Set_Interval.thy b/src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy +++ b/src/HOL/Set_Interval.thy @@ -1,2490 +1,2490 @@ (* Title: HOL/Set_Interval.thy Author: Tobias Nipkow, Clemens Ballarin, Jeremy Avigad lessThan, greaterThan, atLeast, atMost and two-sided intervals Modern convention: Ixy stands for an interval where x and y describe the lower and upper bound and x,y : {c,o,i} where c = closed, o = open, i = infinite. Examples: Ico = {_ ..< _} and Ici = {_ ..} *) section \Set intervals\ theory Set_Interval imports Divides begin context ord begin definition lessThan :: "'a => 'a set" ("(1{..<_})") where "{.. 'a set" ("(1{.._})") where "{..u} == {x. x \ u}" definition greaterThan :: "'a => 'a set" ("(1{_<..})") where "{l<..} == {x. l 'a set" ("(1{_..})") where "{l..} == {x. l\x}" definition greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where "{l<.. 'a => 'a set" ("(1{_..<_})") where "{l.. 'a => 'a set" ("(1{_<.._})") where "{l<..u} == {l<..} Int {..u}" definition atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where "{l..u} == {l..} Int {..u}" end text\A note of warning when using \<^term>\{.. on type \<^typ>\nat\: it is equivalent to \<^term>\{0::nat.. but some lemmas involving \<^term>\{m.. may not exist in \<^term>\{..-form as well.\ syntax (ASCII) "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10) "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10) "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10) "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10) syntax (latex output) "_UNION_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10) "_UNION_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10) "_INTER_le" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ \ _)/ _)" [0, 0, 10] 10) "_INTER_less" :: "'a \ 'a => 'b set => 'b set" ("(3\(\unbreakable\_ < _)/ _)" [0, 0, 10] 10) syntax "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10) "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10) "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\_\_./ _)" [0, 0, 10] 10) "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\_<_./ _)" [0, 0, 10] 10) translations "\i\n. A" \ "\i\{..n}. A" "\i "\i\{..i\n. A" \ "\i\{..n}. A" "\i "\i\{..Various equivalences\ lemma (in ord) lessThan_iff [iff]: "(i \ lessThan k) = (i greaterThan k) = (k atLeast k) = (k<=i)" by (simp add: atLeast_def) lemma Compl_atLeast [simp]: "!!k:: 'a::linorder. -atLeast k = lessThan k" by (auto simp add: lessThan_def atLeast_def) lemma (in ord) atMost_iff [iff]: "(i \ atMost k) = (i<=k)" by (simp add: atMost_def) lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" by (blast intro: order_antisym) lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \ { b <..} = { max a b <..}" by auto lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \ {..< b} = {..< min a b}" by auto subsection \Logical Equivalences for Set Inclusion and Equality\ lemma atLeast_empty_triv [simp]: "{{}..} = UNIV" by auto lemma atMost_UNIV_triv [simp]: "{..UNIV} = UNIV" by auto lemma atLeast_subset_iff [iff]: "(atLeast x \ atLeast y) = (y \ (x::'a::preorder))" by (blast intro: order_trans) lemma atLeast_eq_iff [iff]: "(atLeast x = atLeast y) = (x = (y::'a::order))" by (blast intro: order_antisym order_trans) lemma greaterThan_subset_iff [iff]: "(greaterThan x \ greaterThan y) = (y \ (x::'a::linorder))" unfolding greaterThan_def by (auto simp: linorder_not_less [symmetric]) lemma greaterThan_eq_iff [iff]: "(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" by (auto simp: elim!: equalityE) lemma atMost_subset_iff [iff]: "(atMost x \ atMost y) = (x \ (y::'a::preorder))" by (blast intro: order_trans) lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::order))" by (blast intro: order_antisym order_trans) lemma lessThan_subset_iff [iff]: "(lessThan x \ lessThan y) = (x \ (y::'a::linorder))" unfolding lessThan_def by (auto simp: linorder_not_less [symmetric]) lemma lessThan_eq_iff [iff]: "(lessThan x = lessThan y) = (x = (y::'a::linorder))" by (auto simp: elim!: equalityE) lemma lessThan_strict_subset_iff: fixes m n :: "'a::linorder" shows "{.. m < n" by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq) lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \ {b <..} \ b < a" by auto lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \ {..< b} \ a < b" by auto lemma (in preorder) Ioi_le_Ico: "{a <..} \ {a ..}" by (auto intro: less_imp_le) subsection \Two-sided intervals\ context ord begin lemma greaterThanLessThan_iff [simp]: "(i \ {l<.. i < u)" by (simp add: greaterThanLessThan_def) lemma atLeastLessThan_iff [simp]: "(i \ {l.. i \ i < u)" by (simp add: atLeastLessThan_def) lemma greaterThanAtMost_iff [simp]: "(i \ {l<..u}) = (l < i \ i \ u)" by (simp add: greaterThanAtMost_def) lemma atLeastAtMost_iff [simp]: "(i \ {l..u}) = (l \ i \ i \ u)" by (simp add: atLeastAtMost_def) text \The above four lemmas could be declared as iffs. Unfortunately this breaks many proofs. Since it only helps blast, it is better to leave them alone.\ lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \ {..< b }" by auto lemma (in order) atLeastLessThan_eq_atLeastAtMost_diff: "{a..Emptyness, singletons, subset\ context preorder begin lemma atLeastatMost_empty_iff[simp]: "{a..b} = {} \ (\ a \ b)" by auto (blast intro: order_trans) lemma atLeastatMost_empty_iff2[simp]: "{} = {a..b} \ (\ a \ b)" by auto (blast intro: order_trans) lemma atLeastLessThan_empty_iff[simp]: "{a.. (\ a < b)" by auto (blast intro: le_less_trans) lemma atLeastLessThan_empty_iff2[simp]: "{} = {a.. (\ a < b)" by auto (blast intro: le_less_trans) lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \ \ k < l" by auto (blast intro: less_le_trans) lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \ \ k < l" by auto (blast intro: less_le_trans) lemma atLeastatMost_subset_iff[simp]: "{a..b} \ {c..d} \ (\ a \ b) \ c \ a \ b \ d" unfolding atLeastAtMost_def atLeast_def atMost_def by (blast intro: order_trans) lemma atLeastatMost_psubset_iff: "{a..b} < {c..d} \ ((\ a \ b) \ c \ a \ b \ d \ (c < a \ b < d)) \ c \ d" by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) lemma atLeastAtMost_subseteq_atLeastLessThan_iff: "{a..b} \ {c ..< d} \ (a \ b \ c \ a \ b < d)" by auto (blast intro: local.order_trans local.le_less_trans elim: )+ lemma Icc_subset_Ici_iff[simp]: "{l..h} \ {l'..} = (\ l\h \ l\l')" by(auto simp: subset_eq intro: order_trans) lemma Icc_subset_Iic_iff[simp]: "{l..h} \ {..h'} = (\ l\h \ h\h')" by(auto simp: subset_eq intro: order_trans) lemma not_Ici_eq_empty[simp]: "{l..} \ {}" by(auto simp: set_eq_iff) lemma not_Iic_eq_empty[simp]: "{..h} \ {}" by(auto simp: set_eq_iff) lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric] lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric] end context order begin lemma atLeastatMost_empty[simp]: "b < a \ {a..b} = {}" by(auto simp: atLeastAtMost_def atLeast_def atMost_def) lemma atLeastLessThan_empty[simp]: "b \ a \ {a.. k ==> {k<..l} = {}" by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) lemma greaterThanLessThan_empty[simp]:"l \ k ==> {k<.. {a .. b} = {a}" by simp lemma Icc_eq_Icc[simp]: "{l..h} = {l'..h'} = (l=l' \ h=h' \ \ l\h \ \ l'\h')" by(simp add: order_class.eq_iff)(auto intro: order_trans) lemma atLeastAtMost_singleton_iff[simp]: "{a .. b} = {c} \ a = b \ b = c" proof assume "{a..b} = {c}" hence *: "\ (\ a \ b)" unfolding atLeastatMost_empty_iff[symmetric] by simp with \{a..b} = {c}\ have "c \ a \ b \ c" by auto with * show "a = b \ b = c" by auto qed simp end context no_top begin (* also holds for no_bot but no_top should suffice *) lemma not_UNIV_le_Icc[simp]: "\ UNIV \ {l..h}" using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) lemma not_UNIV_le_Iic[simp]: "\ UNIV \ {..h}" using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) lemma not_Ici_le_Icc[simp]: "\ {l..} \ {l'..h'}" using gt_ex[of h'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) lemma not_Ici_le_Iic[simp]: "\ {l..} \ {..h'}" using gt_ex[of h'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) end context no_bot begin lemma not_UNIV_le_Ici[simp]: "\ UNIV \ {l..}" using lt_ex[of l] by(auto simp: subset_eq less_le_not_le) lemma not_Iic_le_Icc[simp]: "\ {..h} \ {l'..h'}" using lt_ex[of l'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) lemma not_Iic_le_Ici[simp]: "\ {..h} \ {l'..}" using lt_ex[of l'] by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) end context no_top begin (* also holds for no_bot but no_top should suffice *) lemma not_UNIV_eq_Icc[simp]: "\ UNIV = {l'..h'}" using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric] lemma not_UNIV_eq_Iic[simp]: "\ UNIV = {..h'}" using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric] lemma not_Icc_eq_Ici[simp]: "\ {l..h} = {l'..}" unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric] (* also holds for no_bot but no_top should suffice *) lemma not_Iic_eq_Ici[simp]: "\ {..h} = {l'..}" using not_Ici_le_Iic[of l' h] by blast lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric] end context no_bot begin lemma not_UNIV_eq_Ici[simp]: "\ UNIV = {l'..}" using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le) lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric] lemma not_Icc_eq_Iic[simp]: "\ {l..h} = {..h'}" unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric] end context dense_linorder begin lemma greaterThanLessThan_empty_iff[simp]: "{ a <..< b } = {} \ b \ a" using dense[of a b] by (cases "a < b") auto lemma greaterThanLessThan_empty_iff2[simp]: "{} = { a <..< b } \ b \ a" using dense[of a b] by (cases "a < b") auto lemma atLeastLessThan_subseteq_atLeastAtMost_iff: "{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)" using dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: "{a <.. b} \ { c .. d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: "{a <..< b} \ { c .. d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_greaterThanLessThan: "{a <..< b} \ {c <..< d} \ (a < b \ a \ c \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: "{a <.. b} \ { c ..< d } \ (a < b \ c \ a \ b < d)" using dense[of "a" "min c b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: "{a <..< b} \ { c ..< d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff: "{a <..< b} \ { c <.. d } \ (a < b \ c \ a \ b \ d)" using dense[of "a" "min c b"] dense[of "max a d" "b"] by (force simp: subset_eq Ball_def not_less[symmetric]) end context no_top begin lemma greaterThan_non_empty[simp]: "{x <..} \ {}" using gt_ex[of x] by auto end context no_bot begin lemma lessThan_non_empty[simp]: "{..< x} \ {}" using lt_ex[of x] by auto end lemma (in linorder) atLeastLessThan_subset_iff: "{a.. {c.. b \ a \ c\a \ b\d" apply (auto simp:subset_eq Ball_def not_le) apply(frule_tac x=a in spec) apply(erule_tac x=d in allE) apply (auto simp: ) done lemma atLeastLessThan_inj: fixes a b c d :: "'a::linorder" assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d" shows "a = c" "b = d" using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le antisym_conv2 subset_refl)+ lemma atLeastLessThan_eq_iff: fixes a b c d :: "'a::linorder" assumes "a < b" "c < d" shows "{a ..< b} = {c ..< d} \ a = c \ b = d" using atLeastLessThan_inj assms by auto lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \ (b \ a \ d \ c) \ a = c \ b = d" by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le) lemma (in order) Iio_Int_singleton: "{.. {x} = (if x < k then {x} else {})" by auto lemma (in linorder) Ioc_subset_iff: "{a<..b} \ {c<..d} \ (b \ a \ c \ a \ b \ d)" by (auto simp: subset_eq Ball_def) (metis less_le not_less) lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \ x = bot" by (auto simp: set_eq_iff intro: le_bot) lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \ x = top" by (auto simp: set_eq_iff intro: top_le) lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff: "{x..y} = UNIV \ (x = bot \ y = top)" by (auto simp: set_eq_iff intro: top_le le_bot) lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \ n = bot" by (auto simp: set_eq_iff not_less le_bot) lemma lessThan_empty_iff: "{..< n::nat} = {} \ n = 0" by (simp add: Iio_eq_empty_iff bot_nat_def) lemma mono_image_least: assumes f_mono: "mono f" and f_img: "f ` {m ..< n} = {m' ..< n'}" "m < n" shows "f m = m'" proof - from f_img have "{m' ..< n'} \ {}" by (metis atLeastLessThan_empty_iff image_is_empty) with f_img have "m' \ f ` {m ..< n}" by auto then obtain k where "f k = m'" "m \ k" by auto moreover have "m' \ f m" using f_img by auto ultimately show "f m = m'" using f_mono by (auto elim: monoE[where x=m and y=k]) qed subsection \Infinite intervals\ context dense_linorder begin lemma infinite_Ioo: assumes "a < b" shows "\ finite {a<.. {}" using \a < b\ by auto ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b" using Max_in[of "{a <..< b}"] by auto then obtain x where "Max {a <..< b} < x" "x < b" using dense[of "Max {a<.. {a <..< b}" using \a < Max {a <..< b}\ by auto then have "x \ Max {a <..< b}" using fin by auto with \Max {a <..< b} < x\ show False by auto qed lemma infinite_Icc: "a < b \ \ finite {a .. b}" using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b] by (auto dest: finite_subset) lemma infinite_Ico: "a < b \ \ finite {a ..< b}" using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b] by (auto dest: finite_subset) lemma infinite_Ioc: "a < b \ \ finite {a <.. b}" using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b] by (auto dest: finite_subset) lemma infinite_Ioo_iff [simp]: "infinite {a<.. a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioo) lemma infinite_Icc_iff [simp]: "infinite {a .. b} \ a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Icc) lemma infinite_Ico_iff [simp]: "infinite {a.. a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ico) lemma infinite_Ioc_iff [simp]: "infinite {a<..b} \ a < b" using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioc) end lemma infinite_Iio: "\ finite {..< a :: 'a :: {no_bot, linorder}}" proof assume "finite {..< a}" then have *: "\x. x < a \ Min {..< a} \ x" by auto obtain x where "x < a" using lt_ex by auto obtain y where "y < Min {..< a}" using lt_ex by auto also have "Min {..< a} \ x" using \x < a\ by fact also note \x < a\ finally have "Min {..< a} \ y" by fact with \y < Min {..< a}\ show False by auto qed lemma infinite_Iic: "\ finite {.. a :: 'a :: {no_bot, linorder}}" using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"] by (auto simp: subset_eq less_imp_le) lemma infinite_Ioi: "\ finite {a :: 'a :: {no_top, linorder} <..}" proof assume "finite {a <..}" then have *: "\x. a < x \ x \ Max {a <..}" by auto obtain y where "Max {a <..} < y" using gt_ex by auto obtain x where x: "a < x" using gt_ex by auto also from x have "x \ Max {a <..}" by fact also note \Max {a <..} < y\ finally have "y \ Max { a <..}" by fact with \Max {a <..} < y\ show False by auto qed lemma infinite_Ici: "\ finite {a :: 'a :: {no_top, linorder} ..}" using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"] by (auto simp: subset_eq less_imp_le) subsubsection \Intersection\ context linorder begin lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}" by auto lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}" by auto lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}" by auto lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}" by auto lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}" by auto lemma Int_atLeastLessThan[simp]: "{a.. {..b} = {.. min a b}" by (auto simp: min_def) lemma Ioc_disjoint: "{a<..b} \ {c<..d} = {} \ b \ a \ d \ c \ b \ c \ d \ a" by auto end context complete_lattice begin lemma shows Sup_atLeast[simp]: "Sup {x ..} = top" and Sup_greaterThanAtLeast[simp]: "x < top \ Sup {x <..} = top" and Sup_atMost[simp]: "Sup {.. y} = y" and Sup_atLeastAtMost[simp]: "x \ y \ Sup { x .. y} = y" and Sup_greaterThanAtMost[simp]: "x < y \ Sup { x <.. y} = y" by (auto intro!: Sup_eqI) lemma shows Inf_atMost[simp]: "Inf {.. x} = bot" and Inf_atMostLessThan[simp]: "top < x \ Inf {..< x} = bot" and Inf_atLeast[simp]: "Inf {x ..} = x" and Inf_atLeastAtMost[simp]: "x \ y \ Inf { x .. y} = x" and Inf_atLeastLessThan[simp]: "x < y \ Inf { x ..< y} = x" by (auto intro!: Inf_eqI) end lemma fixes x y :: "'a :: {complete_lattice, dense_linorder}" shows Sup_lessThan[simp]: "Sup {..< y} = y" and Sup_atLeastLessThan[simp]: "x < y \ Sup { x ..< y} = y" and Sup_greaterThanLessThan[simp]: "x < y \ Sup { x <..< y} = y" and Inf_greaterThan[simp]: "Inf {x <..} = x" and Inf_greaterThanAtMost[simp]: "x < y \ Inf { x <.. y} = x" and Inf_greaterThanLessThan[simp]: "x < y \ Inf { x <..< y} = x" by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded) subsection \Intervals of natural numbers\ subsubsection \The Constant \<^term>\lessThan\\ lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" by (simp add: lessThan_def) lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" by (simp add: lessThan_def less_Suc_eq, blast) text \The following proof is convenient in induction proofs where new elements get indices at the beginning. So it is used to transform \<^term>\{.. to \<^term>\0::nat\ and \<^term>\{..< n}\.\ lemma zero_notin_Suc_image [simp]: "0 \ Suc ` A" by auto lemma lessThan_Suc_eq_insert_0: "{..m::nat. lessThan m) = UNIV" by blast subsubsection \The Constant \<^term>\greaterThan\\ lemma greaterThan_0: "greaterThan 0 = range Suc" unfolding greaterThan_def by (blast dest: gr0_conv_Suc [THEN iffD1]) lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}" unfolding greaterThan_def by (auto elim: linorder_neqE) lemma INT_greaterThan_UNIV: "(\m::nat. greaterThan m) = {}" by blast subsubsection \The Constant \<^term>\atLeast\\ lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" by (unfold atLeast_def UNIV_def, simp) lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}" unfolding atLeast_def by (auto simp: order_le_less Suc_le_eq) lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) lemma UN_atLeast_UNIV: "(\m::nat. atLeast m) = UNIV" by blast subsubsection \The Constant \<^term>\atMost\\ lemma atMost_0 [simp]: "atMost (0::nat) = {0}" by (simp add: atMost_def) lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" unfolding atMost_def by (auto simp add: less_Suc_eq order_le_less) lemma UN_atMost_UNIV: "(\m::nat. atMost m) = UNIV" by blast subsubsection \The Constant \<^term>\atLeastLessThan\\ text\The orientation of the following 2 rules is tricky. The lhs is defined in terms of the rhs. Hence the chosen orientation makes sense in this theory --- the reverse orientation complicates proofs (eg nontermination). But outside, when the definition of the lhs is rarely used, the opposite orientation seems preferable because it reduces a specific concept to a more general one.\ lemma atLeast0LessThan [code_abbrev]: "{0::nat..The Constant \<^term>\atLeastAtMost\\ lemma Icc_eq_insert_lb_nat: "m \ n \ {m..n} = insert m {Suc m..n}" by auto lemma atLeast0_atMost_Suc: "{0..Suc n} = insert (Suc n) {0..n}" by (simp add: atLeast0AtMost atMost_Suc) lemma atLeast0_atMost_Suc_eq_insert_0: "{0..Suc n} = insert 0 (Suc ` {0..n})" by (simp add: atLeast0AtMost atMost_Suc_eq_insert_0) subsubsection \Intervals of nats with \<^term>\Suc\\ text\Not a simprule because the RHS is too messy.\ lemma atLeastLessThanSuc: "{m.. n then insert n {m.. Suc n \ {m..Suc n} = insert (Suc n) {m..n}" by (auto simp add: atLeastAtMost_def) lemma atLeastAtMost_insertL: "m \ n \ insert m {Suc m..n} = {m ..n}" by auto text \The analogous result is useful on \<^typ>\int\:\ (* here, because we don't have an own int section *) lemma atLeastAtMostPlus1_int_conv: "m \ 1+n \ {m..1+n} = insert (1+n) {m..n::int}" by (auto intro: set_eqI) lemma atLeastLessThan_add_Un: "i \ j \ {i.. {j..Intervals and numerals\ lemma lessThan_nat_numeral: \ \Evaluation for specific numerals\ "lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))" by (simp add: numeral_eq_Suc lessThan_Suc) lemma atMost_nat_numeral: \ \Evaluation for specific numerals\ "atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))" by (simp add: numeral_eq_Suc atMost_Suc) lemma atLeastLessThan_nat_numeral: \ \Evaluation for specific numerals\ "atLeastLessThan m (numeral k :: nat) = (if m \ (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k)) else {})" by (simp add: numeral_eq_Suc atLeastLessThanSuc) subsubsection \Image\ context linordered_semidom begin lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}" proof - have "n = k + (n - k)" if "i + k \ n" for n proof - have "n = (n - (k + i)) + (k + i)" using that by (metis add_commute le_add_diff_inverse) then show "n = k + (n - k)" by (metis local.add_diff_cancel_left' add_assoc add_commute) qed then show ?thesis by (fastforce simp: add_le_imp_le_diff add.commute) qed lemma image_add_atLeastAtMost [simp]: "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B") proof show "?A \ ?B" by (auto simp add: ac_simps) next show "?B \ ?A" proof fix n assume "n \ ?B" then have "i \ n - k" by (simp add: add_le_imp_le_diff) have "n = n - k + k" proof - from \n \ ?B\ have "n = n - (i + k) + (i + k)" by simp also have "\ = n - k - i + i + k" by (simp add: algebra_simps) also have "\ = n - k + k" using \i \ n - k\ by simp finally show ?thesis . qed moreover have "n - k \ {i..j}" using \n \ ?B\ by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le) ultimately show "n \ ?A" by (simp add: ac_simps) qed qed lemma image_add_atLeastAtMost' [simp]: "(\n. n + k) ` {i..j} = {i + k..j + k}" by (simp add: add.commute [of _ k]) lemma image_add_atLeastLessThan [simp]: "plus k ` {i..n. n + k) ` {i.. uminus ` {x<..}" by (rule imageI) (simp add: *) thus "y \ uminus ` {x<..}" by simp next fix y assume "y \ -x" have "- (-y) \ uminus ` {x..}" by (rule imageI) (insert \y \ -x\[THEN le_imp_neg_le], simp) thus "y \ uminus ` {x..}" by simp qed simp_all lemma fixes x :: 'a shows image_uminus_lessThan[simp]: "uminus ` {.. = {c - b<..c - a}" by simp finally show ?thesis by simp qed lemma image_minus_const_greaterThanAtMost[simp]: fixes a b c::"'a::linordered_idom" shows "(-) c ` {a<..b} = {c - b.. = {c - b.. = {..c - a}" by simp finally show ?thesis by simp qed lemma image_minus_const_AtMost[simp]: fixes b c::"'a::linordered_idom" shows "(-) c ` {..b} = {c - b..}" proof - have "(-) c ` {..b} = (+) c ` uminus ` {..b}" unfolding image_image by simp also have "\ = {c - b..}" by simp finally show ?thesis by simp qed lemma image_minus_const_atLeastAtMost' [simp]: "(\t. t-d)`{a..b} = {a-d..b-d}" for d::"'a::linordered_idom" by (metis (no_types, lifting) diff_conv_add_uminus image_add_atLeastAtMost' image_cong) context linordered_field begin lemma image_mult_atLeastAtMost [simp]: "((*) d ` {a..b}) = {d*a..d*b}" if "d>0" using that by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x]) lemma image_divide_atLeastAtMost [simp]: "((\c. c / d) ` {a..b}) = {a/d..b/d}" if "d>0" proof - from that have "inverse d > 0" by simp with image_mult_atLeastAtMost [of "inverse d" a b] have "(*) (inverse d) ` {a..b} = {inverse d * a..inverse d * b}" by blast moreover have "(*) (inverse d) = (\c. c / d)" by (simp add: fun_eq_iff field_simps) ultimately show ?thesis by simp qed lemma image_mult_atLeastAtMost_if: "(*) c ` {x .. y} = (if c > 0 then {c * x .. c * y} else if x \ y then {c * y .. c * x} else {})" proof (cases "c = 0 \ x > y") case True then show ?thesis by auto next case False then have "x \ y" by auto from False consider "c < 0"| "c > 0" by (auto simp add: neq_iff) then show ?thesis proof cases case 1 have "(*) c ` {x..y} = {c * y..c * x}" proof (rule set_eqI) fix d from 1 have "inj (\z. z / c)" by (auto intro: injI) then have "d \ (*) c ` {x..y} \ d / c \ (\z. z div c) ` (*) c ` {x..y}" by (subst inj_image_mem_iff) simp_all also have "\ \ d / c \ {x..y}" using 1 by (simp add: image_image) also have "\ \ d \ {c * y..c * x}" by (auto simp add: field_simps 1) finally show "d \ (*) c ` {x..y} \ d \ {c * y..c * x}" . qed with \x \ y\ show ?thesis by auto qed (simp add: mult_left_mono_neg) qed lemma image_mult_atLeastAtMost_if': "(\x. x * c) ` {x..y} = (if x \ y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})" using image_mult_atLeastAtMost_if [of c x y] by (auto simp add: ac_simps) lemma image_affinity_atLeastAtMost: "((\x. m * x + c) ` {a..b}) = (if {a..b} = {} then {} else if 0 \ m then {m * a + c .. m * b + c} else {m * b + c .. m * a + c})" proof - have *: "(\x. m * x + c) = ((\x. x + c) \ (*) m)" by (simp add: fun_eq_iff) show ?thesis by (simp only: * image_comp [symmetric] image_mult_atLeastAtMost_if) (auto simp add: mult_le_cancel_left) qed lemma image_affinity_atLeastAtMost_diff: "((\x. m*x - c) ` {a..b}) = (if {a..b}={} then {} else if 0 \ m then {m*a - c .. m*b - c} else {m*b - c .. m*a - c})" using image_affinity_atLeastAtMost [of m "-c" a b] by simp lemma image_affinity_atLeastAtMost_div: "((\x. x/m + c) ` {a..b}) = (if {a..b}={} then {} else if 0 \ m then {a/m + c .. b/m + c} else {b/m + c .. a/m + c})" using image_affinity_atLeastAtMost [of "inverse m" c a b] by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide) lemma image_affinity_atLeastAtMost_div_diff: "((\x. x/m - c) ` {a..b}) = (if {a..b}={} then {} else if 0 \ m then {a/m - c .. b/m - c} else {b/m - c .. a/m - c})" using image_affinity_atLeastAtMost_diff [of "inverse m" c a b] by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide) end lemma atLeast1_lessThan_eq_remove0: "{Suc 0..x. x + (l::int)) ` {0..i. i - c) ` {x ..< y} = (if c < y then {x - c ..< y - c} else if x < y then {0} else {})" (is "_ = ?right") proof safe fix a assume a: "a \ ?right" show "a \ (\i. i - c) ` {x ..< y}" proof cases assume "c < y" with a show ?thesis by (auto intro!: image_eqI[of _ _ "a + c"]) next assume "\ c < y" with a show ?thesis by (auto intro!: image_eqI[of _ _ x] split: if_split_asm) qed qed auto lemma image_int_atLeastLessThan: "int ` {a..Finiteness\ lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..A bounded set of natural numbers is finite.\ lemma bounded_nat_set_is_finite: "(\i\N. i < (n::nat)) \ finite N" by (rule finite_subset [OF _ finite_lessThan]) auto text \A set of natural numbers is finite iff it is bounded.\ lemma finite_nat_set_iff_bounded: "finite(N::nat set) = (\m. \n\N. n?F\, simplified less_Suc_eq_le[symmetric]] by blast next assume ?B show ?F using \?B\ by(blast intro:bounded_nat_set_is_finite) qed lemma finite_nat_set_iff_bounded_le: "finite(N::nat set) = (\m. \n\N. n\m)" unfolding finite_nat_set_iff_bounded by (blast dest:less_imp_le_nat le_imp_less_Suc) lemma finite_less_ub: "!!f::nat=>nat. (!!n. n \ f n) ==> finite {n. f n \ u}" by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) lemma bounded_Max_nat: fixes P :: "nat \ bool" assumes x: "P x" and M: "\x. P x \ x \ M" obtains m where "P m" "\x. P x \ x \ m" proof - have "finite {x. P x}" using M finite_nat_set_iff_bounded_le by auto then have "Max {x. P x} \ {x. P x}" using Max_in x by auto then show ?thesis by (simp add: \finite {x. P x}\ that) qed text\Any subset of an interval of natural numbers the size of the subset is exactly that interval.\ lemma subset_card_intvl_is_intvl: assumes "A \ {k.. A" by auto with insert have "A \ {k..Proving Inclusions and Equalities between Unions\ lemma UN_le_eq_Un0: "(\i\n::nat. M i) = (\i\{1..n}. M i) \ M 0" (is "?A = ?B") proof show "?A \ ?B" proof fix x assume "x \ ?A" then obtain i where i: "i\n" "x \ M i" by auto show "x \ ?B" proof(cases i) case 0 with i show ?thesis by simp next case (Suc j) with i show ?thesis by auto qed qed next show "?B \ ?A" by fastforce qed lemma UN_le_add_shift: "(\i\n::nat. M(i+k)) = (\i\{k..n+k}. M i)" (is "?A = ?B") proof show "?A \ ?B" by fastforce next show "?B \ ?A" proof fix x assume "x \ ?B" then obtain i where i: "i \ {k..n+k}" "x \ M(i)" by auto hence "i-k\n \ x \ M((i-k)+k)" by auto thus "x \ ?A" by blast qed qed lemma UN_le_add_shift_strict: "(\ii\{k.. ?A" proof fix x assume "x \ ?B" then obtain i where i: "i \ {k.. M(i)" by auto then have "i - k < n \ x \ M((i-k) + k)" by auto then show "x \ ?A" using UN_le_add_shift by blast qed qed (fastforce) lemma UN_UN_finite_eq: "(\n::nat. \i\{0..n. A n)" by (auto simp add: atLeast0LessThan) lemma UN_finite_subset: "(\n::nat. (\i\{0.. C) \ (\n. A n) \ C" by (subst UN_UN_finite_eq [symmetric]) blast lemma UN_finite2_subset: assumes "\n::nat. (\i\{0.. (\i\{0..n. A n) \ (\n. B n)" proof (rule UN_finite_subset, rule) fix n and a from assms have "(\i\{0.. (\i\{0.. (\i\{0.. (\i\{0.. (\i. B i)" by (auto simp add: UN_UN_finite_eq) qed lemma UN_finite2_eq: "(\n::nat. (\i\{0..i\{0.. (\n. A n) = (\n. B n)" apply (rule subset_antisym [OF UN_finite_subset UN_finite2_subset]) apply auto apply (force simp add: atLeastLessThan_add_Un [of 0])+ done subsubsection \Cardinality\ lemma card_lessThan [simp]: "card {..x. x + l) ` {.. {0.. {0..n}" shows "finite N" using assms finite_atLeastAtMost by (rule finite_subset) lemma ex_bij_betw_nat_finite: "finite M \ \h. bij_betw h {0.. \h. bij_betw h M {0.. finite B \ card A = card B \ \h. bij_betw h A B" apply(drule ex_bij_betw_finite_nat) apply(drule ex_bij_betw_nat_finite) apply(auto intro!:bij_betw_trans) done lemma ex_bij_betw_nat_finite_1: "finite M \ \h. bij_betw h {1 .. card M} M" by (rule finite_same_card_bij) auto lemma bij_betw_iff_card: assumes "finite A" "finite B" shows "(\f. bij_betw f A B) \ (card A = card B)" proof assume "card A = card B" moreover obtain f where "bij_betw f A {0 ..< card A}" using assms ex_bij_betw_finite_nat by blast moreover obtain g where "bij_betw g {0 ..< card B} B" using assms ex_bij_betw_nat_finite by blast ultimately have "bij_betw (g \ f) A B" by (auto simp: bij_betw_trans) thus "(\f. bij_betw f A B)" by blast qed (auto simp: bij_betw_same_card) lemma subset_eq_atLeast0_lessThan_card: fixes n :: nat assumes "N \ {0.. n" proof - from assms finite_lessThan have "card N \ card {0..Relational version of @{thm [source] card_inj_on_le}:\ lemma card_le_if_inj_on_rel: assumes "finite B" "\a. a \ A \ \b. b\B \ r a b" "\a1 a2 b. \ a1 \ A; a2 \ A; b \ B; r a1 b; r a2 b \ \ a1 = a2" shows "card A \ card B" proof - let ?P = "\a b. b \ B \ r a b" let ?f = "\a. SOME b. ?P a b" have 1: "?f ` A \ B" by (auto intro: someI2_ex[OF assms(2)]) have "inj_on ?f A" proof (auto simp: inj_on_def) fix a1 a2 assume asms: "a1 \ A" "a2 \ A" "?f a1 = ?f a2" have 0: "?f a1 \ B" using "1" \a1 \ A\ by blast have 1: "r a1 (?f a1)" using someI_ex[OF assms(2)[OF \a1 \ A\]] by blast have 2: "r a2 (?f a1)" using someI_ex[OF assms(2)[OF \a2 \ A\]] asms(3) by auto show "a1 = a2" using assms(3)[OF asms(1,2) 0 1 2] . qed with 1 show ?thesis using card_inj_on_le[of ?f A B] assms(1) by simp qed subsection \Intervals of integers\ lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..Finiteness\ lemma image_atLeastZeroLessThan_int: "0 \ u ==> {(0::int).. u") case True then show ?thesis by (auto simp: image_atLeastZeroLessThan_int) qed auto lemma finite_atLeastLessThan_int [iff]: "finite {l..Cardinality\ lemma card_atLeastZeroLessThan_int: "card {(0::int).. u") case True then show ?thesis by (auto simp: image_atLeastZeroLessThan_int card_image inj_on_def) qed auto lemma card_atLeastLessThan_int [simp]: "card {l.. k < (i::nat)}" proof - have "{k. P k \ k < i} \ {.. M" shows "card {k \ M. k < Suc i} \ 0" proof - from zero_in_M have "{k \ M. k < Suc i} \ {}" by auto with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff) qed lemma card_less_Suc2: assumes "0 \ M" shows "card {k. Suc k \ M \ k < i} = card {k \ M. k < Suc i}" proof - have *: "\j \ M; j < Suc i\ \ j - Suc 0 < i \ Suc (j - Suc 0) \ M \ Suc 0 \ j" for j by (cases j) (use assms in auto) show ?thesis proof (rule card_bij_eq) show "inj_on Suc {k. Suc k \ M \ k < i}" by force show "inj_on (\x. x - Suc 0) {k \ M. k < Suc i}" by (rule inj_on_diff_nat) (use * in blast) qed (use * in auto) qed lemma card_less_Suc: assumes "0 \ M" shows "Suc (card {k. Suc k \ M \ k < i}) = card {k \ M. k < Suc i}" proof - have "Suc (card {k. Suc k \ M \ k < i}) = Suc (card {k. Suc k \ M - {0} \ k < i})" by simp also have "\ = Suc (card {k \ M - {0}. k < Suc i})" apply (subst card_less_Suc2) using assms by auto also have "\ = Suc (card ({k \ M. k < Suc i} - {0}))" by (force intro: arg_cong [where f=card]) also have "\ = card (insert 0 ({k \ M. k < Suc i} - {0}))" by (simp add: card_insert) also have "... = card {k \ M. k < Suc i}" using assms by (force simp add: intro: arg_cong [where f=card]) finally show ?thesis. qed subsection \Lemmas useful with the summation operator sum\ text \For examples, see Algebra/poly/UnivPoly2.thy\ subsubsection \Disjoint Unions\ text \Singletons and open intervals\ lemma ivl_disj_un_singleton: "{l::'a::linorder} Un {l<..} = {l..}" "{.. {l} Un {l<.. {l<.. u ==> {l} Un {l<..u} = {l..u}" "(l::'a::linorder) \ u ==> {l..One- and two-sided intervals\ lemma ivl_disj_un_one: "(l::'a::linorder) < u ==> {..l} Un {l<.. u ==> {.. u ==> {..l} Un {l<..u} = {..u}" "(l::'a::linorder) \ u ==> {.. u ==> {l<..u} Un {u<..} = {l<..}" "(l::'a::linorder) < u ==> {l<.. u ==> {l..u} Un {u<..} = {l..}" "(l::'a::linorder) \ u ==> {l..Two- and two-sided intervals\ lemma ivl_disj_un_two: "[| (l::'a::linorder) < m; m \ u |] ==> {l<.. m; m < u |] ==> {l<..m} Un {m<.. m; m \ u |] ==> {l.. m; m < u |] ==> {l..m} Un {m<.. u |] ==> {l<.. m; m \ u |] ==> {l<..m} Un {m<..u} = {l<..u}" "[| (l::'a::linorder) \ m; m \ u |] ==> {l.. m; m \ u |] ==> {l..m} Un {m<..u} = {l..u}" by auto lemma ivl_disj_un_two_touch: "[| (l::'a::linorder) < m; m < u |] ==> {l<..m} Un {m.. m; m < u |] ==> {l..m} Un {m.. u |] ==> {l<..m} Un {m..u} = {l<..u}" "[| (l::'a::linorder) \ m; m \ u |] ==> {l..m} Un {m..u} = {l..u}" by auto lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two ivl_disj_un_two_touch subsubsection \Disjoint Intersections\ text \One- and two-sided intervals\ lemma ivl_disj_int_one: "{..l::'a::order} Int {l<..Two- and two-sided intervals\ lemma ivl_disj_int_two: "{l::'a::order<..Some Differences\ lemma ivl_diff[simp]: "i \ n \ {i..Some Subset Conditions\ lemma ivl_subset [simp]: "({i.. {m.. i \ m \ i \ j \ (n::'a::linorder))" using linorder_class.le_less_linear[of i n] apply (auto simp: linorder_not_le) apply (force intro: leI)+ done subsection \Generic big monoid operation over intervals\ context semiring_char_0 begin lemma inj_on_of_nat [simp]: "inj_on of_nat N" by rule simp lemma bij_betw_of_nat [simp]: "bij_betw of_nat N A \ of_nat ` N = A" by (simp add: bij_betw_def) end context comm_monoid_set begin lemma atLeastLessThan_reindex: "F g {h m.. h) {m.. h) {m..n}" if "bij_betw h {m..n} {h m..h n}" for m n ::nat proof - from that have "inj_on h {m..n}" and "h ` {m..n} = {h m..h n}" by (simp_all add: bij_betw_def) then show ?thesis using reindex [of h "{m..n}" g] by simp qed lemma atLeastLessThan_shift_bounds: "F g {m + k.. plus k) {m.. plus k) {m..n}" for m n k :: nat using atLeastAtMost_reindex [of "plus k" m n g] by (simp add: ac_simps) lemma atLeast_Suc_lessThan_Suc_shift: "F g {Suc m.. Suc) {m.. Suc) {m..n}" using atLeastAtMost_shift_bounds [of _ _ 1] by (simp add: plus_1_eq_Suc) lemma atLeast_int_lessThan_int_shift: "F g {int m.. int) {m.. int) {m..n}" by (rule atLeastAtMost_reindex) (simp add: image_int_atLeastAtMost) lemma atLeast0_lessThan_Suc: "F g {0..* g n" by (simp add: atLeast0_lessThan_Suc ac_simps) lemma atLeast0_atMost_Suc: "F g {0..Suc n} = F g {0..n} \<^bold>* g (Suc n)" by (simp add: atLeast0_atMost_Suc ac_simps) lemma atLeast0_lessThan_Suc_shift: "F g {0..* F (g \ Suc) {0..* F (g \ Suc) {0..n}" by (simp add: atLeast0_atMost_Suc_eq_insert_0 atLeast_Suc_atMost_Suc_shift) lemma atLeast_Suc_lessThan: "F g {m..* F g {Suc m..* F g {Suc m..n}" if "m \ n" proof - from that have "{m..n} = insert m {Suc m..n}" by auto then show ?thesis by simp qed lemma ivl_cong: "a = c \ b = d \ (\x. c \ x \ x < d \ g x = h x) \ F g {a.. plus m) {0.. n") simp_all lemma atLeastAtMost_shift_0: fixes m n p :: nat assumes "m \ n" shows "F g {m..n} = F (g \ plus m) {0..n - m}" using assms atLeastAtMost_shift_bounds [of g 0 m "n - m"] by simp lemma atLeastLessThan_concat: fixes m n p :: nat shows "m \ n \ n \ p \ F g {m..* F g {n..i. g (m + n - Suc i)) {n..i. g (m + n - i)) {n..m}" by (rule reindex_bij_witness [where i="\i. m + n - i" and j="\i. m + n - i"]) auto lemma atLeastLessThan_rev_at_least_Suc_atMost: "F g {n..i. g (m + n - i)) {Suc n..m}" unfolding atLeastLessThan_rev [of g n m] by (cases m) (simp_all add: atLeast_Suc_atMost_Suc_shift atLeastLessThanSuc_atLeastAtMost) end subsection \Summation indexed over intervals\ syntax (ASCII) "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<_./ _)" [0,0,10] 10) "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(SUM _<=_./ _)" [0,0,10] 10) syntax (latex_sum output) "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ = _\<^latex>\}^{\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ = _\<^latex>\}^{<\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ < _\<^latex>\}$\ _)" [0,0,10] 10) "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\sum_{\_ \ _\<^latex>\}$\ _)" [0,0,10] 10) syntax "_from_to_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) "_from_upto_sum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) "_upt_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_sum" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) translations "\x=a..b. t" == "CONST sum (\x. t) {a..b}" "\x=a..x. t) {a..i\n. t" == "CONST sum (\i. t) {..n}" "\ii. t) {..The above introduces some pretty alternative syntaxes for summation over intervals: \begin{center} \begin{tabular}{lll} Old & New & \LaTeX\\ @{term[source]"\x\{a..b}. e"} & \<^term>\\x=a..b. e\ & @{term[mode=latex_sum]"\x=a..b. e"}\\ @{term[source]"\x\{a..\\x=a.. & @{term[mode=latex_sum]"\x=a..x\{..b}. e"} & \<^term>\\x\b. e\ & @{term[mode=latex_sum]"\x\b. e"}\\ @{term[source]"\x\{..\\x & @{term[mode=latex_sum]"\xlatex_sum\ (e.g.\ via \mode = latex_sum\ in antiquotations). It is not the default \LaTeX\ output because it only works well with italic-style formulae, not tt-style. Note that for uniformity on \<^typ>\nat\ it is better to use \<^term>\\x::nat=0.. rather than \\x: \sum\ may not provide all lemmas available for \<^term>\{m.. also in the special form for \<^term>\{...\ text\This congruence rule should be used for sums over intervals as the standard theorem @{text[source]sum.cong} does not work well with the simplifier who adds the unsimplified premise \<^term>\x\B\ to the context.\ context comm_monoid_set begin lemma zero_middle: assumes "1 \ p" "k \ p" shows "F (\j. if j < k then g j else if j = k then \<^bold>1 else h (j - Suc 0)) {..p} = F (\j. if j < k then g j else h j) {..p - Suc 0}" (is "?lhs = ?rhs") proof - have [simp]: "{..p - Suc 0} \ {j. j < k} = {.. - {j. j < k} = {k..p - Suc 0}" using assms by auto have "?lhs = F g {..* F (\j. if j = k then \<^bold>1 else h (j - Suc 0)) {k..p}" using union_disjoint [of "{.. = F g {..* F (\j. h (j - Suc 0)) {Suc k..p}" by (simp add: atLeast_Suc_atMost [of k p] assms) also have "\ = F g {..* F h {k .. p - Suc 0}" using reindex [of Suc "{k..p - Suc 0}"] assms by simp also have "\ = ?rhs" by (simp add: If_cases) finally show ?thesis . qed lemma atMost_Suc [simp]: "F g {..Suc n} = F g {..n} \<^bold>* g (Suc n)" by (simp add: atMost_Suc ac_simps) lemma lessThan_Suc [simp]: "F g {..* g n" by (simp add: lessThan_Suc ac_simps) lemma cl_ivl_Suc [simp]: "F g {m..Suc n} = (if Suc n < m then \<^bold>1 else F g {m..n} \<^bold>* g(Suc n))" by (auto simp: ac_simps atLeastAtMostSuc_conv) lemma op_ivl_Suc [simp]: "F g {m..1 else F g {m..* g(n))" by (auto simp: ac_simps atLeastLessThanSuc) lemma head: fixes n :: nat assumes mn: "m \ n" shows "F g {m..n} = g m \<^bold>* F g {m<..n}" (is "?lhs = ?rhs") proof - from mn have "{m..n} = {m} \ {m<..n}" by (auto intro: ivl_disj_un_singleton) hence "?lhs = F g ({m} \ {m<..n})" by (simp add: atLeast0LessThan) also have "\ = ?rhs" by simp finally show ?thesis . qed lemma ub_add_nat: assumes "(m::nat) \ n + 1" shows "F g {m..n + p} = F g {m..n} \<^bold>* F g {n + 1..n + p}" proof- have "{m .. n+p} = {m..n} \ {n+1..n+p}" using \m \ n+1\ by auto thus ?thesis by (auto simp: ivl_disj_int union_disjoint atLeastSucAtMost_greaterThanAtMost) qed lemma nat_group: fixes k::nat shows "F (\m. F g {m * k ..< m*k + k}) {.. 0" by auto then show ?thesis by (induct n) (simp_all add: atLeastLessThan_concat add.commute atLeast0LessThan[symmetric]) qed auto lemma triangle_reindex: fixes n :: nat shows "F (\(i,j). g i j) {(i,j). i+j < n} = F (\k. F (\i. g i (k - i)) {..k}) {..(i,j). g i j) {(i,j). i+j \ n} = F (\k. F (\i. g i (k - i)) {..k}) {..n}" using triangle_reindex [of g "Suc n"] by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost) lemma nat_diff_reindex: "F (\i. g (n - Suc i)) {..i. g(i + k)){m..i. g(i + k)){m..n::nat}" by (rule reindex_bij_witness[where i="\i. i + k" and j="\i. i - k"]) auto corollary shift_bounds_cl_Suc_ivl: "F g {Suc m..Suc n} = F (\i. g(Suc i)){m..n}" by (simp add: shift_bounds_cl_nat_ivl[where k="Suc 0", simplified]) corollary shift_bounds_Suc_ivl: "F g {Suc m..i. g(Suc i)){m..* F (\i. g (Suc i)) {..n}" proof (induct n) case 0 show ?case by simp next case (Suc n) note IH = this have "F g {..Suc (Suc n)} = F g {..Suc n} \<^bold>* g (Suc (Suc n))" by (rule atMost_Suc) also have "F g {..Suc n} = g 0 \<^bold>* F (\i. g (Suc i)) {..n}" by (rule IH) also have "g 0 \<^bold>* F (\i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)) = g 0 \<^bold>* (F (\i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)))" by (rule assoc) also have "F (\i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)) = F (\i. g (Suc i)) {..Suc n}" by (rule atMost_Suc [symmetric]) finally show ?case . qed lemma lessThan_Suc_shift: "F g {..* F (\i. g (Suc i)) {..* F (\i. g (Suc i)) {.. n \ F g {m..n} = g n \<^bold>* F g {m..i. F (\j. a i j) {0..j. F (\i. a i j) {Suc j..n}) {0..i. F (\j. a i j) {..j. F (\i. a i j) {Suc j..n}) {..k. g (Suc k)) {.. = F (\k. g (Suc k)) {.. b \ F g {a..* g b" by (simp add: atLeastLessThanSuc commute) lemma nat_ivl_Suc': assumes "m \ Suc n" shows "F g {m..Suc n} = g (Suc n) \<^bold>* F g {m..n}" proof - from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto also have "F g \ = g (Suc n) \<^bold>* F g {m..n}" by simp finally show ?thesis . qed lemma in_pairs: "F g {2*m..Suc(2*n)} = F (\i. g(2*i) \<^bold>* g(Suc(2*i))) {m..n}" proof (induction n) case 0 show ?case by (cases "m=0") auto next case (Suc n) then show ?case by (auto simp: assoc split: if_split_asm) qed lemma in_pairs_0: "F g {..Suc(2*n)} = F (\i. g(2*i) \<^bold>* g(Suc(2*i))) {..n}" using in_pairs [of _ 0 n] by (simp add: atLeast0AtMost) end lemma sum_natinterval_diff: fixes f:: "nat \ ('a::ab_group_add)" shows "sum (\k. f k - f(k + 1)) {(m::nat) .. n} = (if m \ n then f m - f(n + 1) else 0)" by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) lemma sum_diff_nat_ivl: fixes f :: "nat \ 'a::ab_group_add" shows "\ m \ n; n \ p \ \ sum f {m..x. Q x \ P x \ (\xxxk = 0..k = 0..k = Suc 0..k = Suc 0..k = 0..Shifting bounds\ context comm_monoid_add begin context fixes f :: "nat \ 'a" assumes "f 0 = 0" begin lemma sum_shift_lb_Suc0_0_upt: "sum f {Suc 0..f 0 = 0\ by simp qed lemma sum_shift_lb_Suc0_0: "sum f {Suc 0..k} = sum f {0..k}" proof (cases k) case 0 with \f 0 = 0\ show ?thesis by simp next case (Suc k) moreover have "{0..Suc k} = insert 0 {Suc 0..Suc k}" by auto ultimately show ?thesis using \f 0 = 0\ by simp qed end end lemma sum_Suc_diff: fixes f :: "nat \ 'a::ab_group_add" assumes "m \ Suc n" shows "(\i = m..n. f(Suc i) - f i) = f (Suc n) - f m" using assms by (induct n) (auto simp: le_Suc_eq) lemma sum_Suc_diff': fixes f :: "nat \ 'a::ab_group_add" assumes "m \ n" shows "(\i = m..Telescoping\ lemma sum_telescope: fixes f::"nat \ 'a::ab_group_add" shows "sum (\i. f i - f (Suc i)) {.. i} = f 0 - f (Suc i)" by (induct i) simp_all lemma sum_telescope'': assumes "m \ n" shows "(\k\{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)" by (rule dec_induct[OF assms]) (simp_all add: algebra_simps) lemma sum_lessThan_telescope: "(\nnThe formula for geometric sums\ lemma sum_power2: "(\i=0.. 1" shows "(\i 0" by simp_all moreover have "(\iy \ 0\) ultimately show ?thesis by simp qed lemma diff_power_eq_sum: fixes y :: "'a::{comm_ring,monoid_mult}" shows "x ^ (Suc n) - y ^ (Suc n) = (x - y) * (\pppp \\COMPLEX_POLYFUN\ in HOL Light\ fixes x :: "'a::{comm_ring,monoid_mult}" shows "x^n - y^n = (x - y) * (\i 0 \ x^n - 1 = (x - 1) * (\i 0 \ 1 - x^n = (1 - x) * (\i 0 \ 1 - x^n = (1 - x) * (\ii\n. x^i) = 1 - x^Suc n" by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost) lemma sum_power_shift: fixes x :: "'a::{comm_ring,monoid_mult}" assumes "m \ n" shows "(\i=m..n. x^i) = x^m * (\i\n-m. x^i)" proof - have "(\i=m..n. x^i) = x^m * (\i=m..n. x^(i-m))" by (simp add: sum_distrib_left power_add [symmetric]) also have "(\i=m..n. x^(i-m)) = (\i\n-m. x^i)" using \m \ n\ by (intro sum.reindex_bij_witness[where j="\i. i - m" and i="\i. i + m"]) auto finally show ?thesis . qed lemma sum_gp_multiplied: fixes x :: "'a::{comm_ring,monoid_mult}" assumes "m \ n" shows "(1 - x) * (\i=m..n. x^i) = x^m - x^Suc n" proof - have "(1 - x) * (\i=m..n. x^i) = x^m * (1 - x) * (\i\n-m. x^i)" by (metis mult.assoc mult.commute assms sum_power_shift) also have "... =x^m * (1 - x^Suc(n-m))" by (metis mult.assoc sum_gp_basic) also have "... = x^m - x^Suc n" using assms by (simp add: algebra_simps) (metis le_add_diff_inverse power_add) finally show ?thesis . qed lemma sum_gp: fixes x :: "'a::{comm_ring,division_ring}" shows "(\i=m..n. x^i) = (if n < m then 0 else if x = 1 then of_nat((n + 1) - m) else (x^m - x^Suc n) / (1 - x))" using sum_gp_multiplied [of m n x] apply auto by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq) subsubsection\Geometric progressions\ lemma sum_gp0: fixes x :: "'a::{comm_ring,division_ring}" shows "(\i\n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))" using sum_gp_basic[of x n] by (simp add: mult.commute field_split_simps) lemma sum_power_add: fixes x :: "'a::{comm_ring,monoid_mult}" shows "(\i\I. x^(m+i)) = x^m * (\i\I. x^i)" by (simp add: sum_distrib_left power_add) lemma sum_gp_offset: fixes x :: "'a::{comm_ring,division_ring}" shows "(\i=m..m+n. x^i) = (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))" using sum_gp [of x m "m+n"] by (auto simp: power_add algebra_simps) lemma sum_gp_strict: fixes x :: "'a::{comm_ring,division_ring}" shows "(\iThe formulae for arithmetic sums\ context comm_semiring_1 begin lemma double_gauss_sum: "2 * (\i = 0..n. of_nat i) = of_nat n * (of_nat n + 1)" by (induct n) (simp_all add: sum.atLeast0_atMost_Suc algebra_simps left_add_twice) lemma double_gauss_sum_from_Suc_0: "2 * (\i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1)" proof - have "sum of_nat {Suc 0..n} = sum of_nat (insert 0 {Suc 0..n})" by simp also have "\ = sum of_nat {0..n}" by (cases n) (simp_all add: atLeast0_atMost_Suc_eq_insert_0) finally show ?thesis by (simp add: double_gauss_sum) qed lemma double_arith_series: "2 * (\i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d)" proof - have "(\i = 0..n. a + of_nat i * d) = ((\i = 0..n. a) + (\i = 0..n. of_nat i * d))" by (rule sum.distrib) also have "\ = (of_nat (Suc n) * a + d * (\i = 0..n. of_nat i))" by (simp add: sum_distrib_left algebra_simps) finally show ?thesis by (simp add: algebra_simps double_gauss_sum left_add_twice) qed end context unique_euclidean_semiring_with_nat begin lemma gauss_sum: "(\i = 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2" using double_gauss_sum [of n, symmetric] by simp lemma gauss_sum_from_Suc_0: "(\i = Suc 0..n. of_nat i) = of_nat n * (of_nat n + 1) div 2" using double_gauss_sum_from_Suc_0 [of n, symmetric] by simp lemma arith_series: "(\i = 0..n. a + of_nat i * d) = (of_nat n + 1) * (2 * a + of_nat n * d) div 2" using double_arith_series [of a d n, symmetric] by simp end lemma gauss_sum_nat: "\{0..n} = (n * Suc n) div 2" using gauss_sum [of n, where ?'a = nat] by simp lemma arith_series_nat: "(\i = 0..n. a + i * d) = Suc n * (2 * a + n * d) div 2" using arith_series [of a d n] by simp lemma Sum_Icc_int: "\{m..n} = (n * (n + 1) - m * (m - 1)) div 2" if "m \ n" for m n :: int using that proof (induct i \ "nat (n - m)" arbitrary: m n) case 0 then have "m = n" by arith then show ?case by (simp add: algebra_simps mult_2 [symmetric]) next case (Suc i) have 0: "i = nat((n-1) - m)" "m \ n-1" using Suc(2,3) by arith+ have "\ {m..n} = \ {m..1+(n-1)}" by simp also have "\ = \ {m..n-1} + n" using \m \ n\ by(subst atLeastAtMostPlus1_int_conv) simp_all also have "\ = ((n-1)*(n-1+1) - m*(m-1)) div 2 + n" by(simp add: Suc(1)[OF 0]) also have "\ = ((n-1)*(n-1+1) - m*(m-1) + 2*n) div 2" by simp also have "\ = (n*(n+1) - m*(m-1)) div 2" by (simp add: algebra_simps mult_2_right) finally show ?case . qed lemma Sum_Icc_nat: "\{m..n} = (n * (n + 1) - m * (m - 1)) div 2" for m n :: nat proof (cases "m \ n") case True then have *: "m * (m - 1) \ n * (n + 1)" by (meson diff_le_self order_trans le_add1 mult_le_mono) have "int (\{m..n}) = (\{int m..int n})" by (simp add: sum.atLeast_int_atMost_int_shift) also have "\ = (int n * (int n + 1) - int m * (int m - 1)) div 2" using \m \ n\ by (simp add: Sum_Icc_int) also have "\ = int ((n * (n + 1) - m * (m - 1)) div 2)" using le_square * by (simp add: algebra_simps of_nat_div of_nat_diff) finally show ?thesis by (simp only: of_nat_eq_iff) next case False then show ?thesis by (auto dest: less_imp_Suc_add simp add: not_le algebra_simps) qed lemma Sum_Ico_nat: "\{m..Division remainder\ lemma range_mod: fixes n :: nat assumes "n > 0" shows "range (\m. m mod n) = {0.. ?A \ m \ ?B" proof assume "m \ ?A" with assms show "m \ ?B" by auto next assume "m \ ?B" moreover have "m mod n \ ?A" by (rule rangeI) ultimately show "m \ ?A" by simp qed qed subsection \Products indexed over intervals\ syntax (ASCII) "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10) "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10) "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<_./ _)" [0,0,10] 10) "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(PROD _<=_./ _)" [0,0,10] 10) syntax (latex_prod output) "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{<\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ < _\<^latex>\}$\ _)" [0,0,10] 10) "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\<^latex>\$\\prod_{\_ \ _\<^latex>\}$\ _)" [0,0,10] 10) syntax "_from_to_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) "_from_upto_prod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _..<_./ _)" [0,0,0,10] 10) "_upt_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_<_./ _)" [0,0,10] 10) "_upto_prod" :: "idt \ 'a \ 'b \ 'b" ("(3\_\_./ _)" [0,0,10] 10) translations "\x=a..b. t" \ "CONST prod (\x. t) {a..b}" "\x=a.. "CONST prod (\x. t) {a..i\n. t" \ "CONST prod (\i. t) {..n}" "\i "CONST prod (\i. t) {..{int i..int (i+j)}" by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv) lemma prod_int_eq: "prod int {i..j} = \{int i..int j}" proof (cases "i \ j") case True then show ?thesis by (metis le_iff_add prod_int_plus_eq) next case False then show ?thesis by auto qed subsection \Efficient folding over intervals\ function fold_atLeastAtMost_nat where [simp del]: "fold_atLeastAtMost_nat f a (b::nat) acc = (if a > b then acc else fold_atLeastAtMost_nat f (a+1) b (f a acc))" by pat_completeness auto termination by (relation "measure (\(_,a,b,_). Suc b - a)") auto lemma fold_atLeastAtMost_nat: assumes "comp_fun_commute f" shows "fold_atLeastAtMost_nat f a b acc = Finite_Set.fold f acc {a..b}" using assms proof (induction f a b acc rule: fold_atLeastAtMost_nat.induct, goal_cases) case (1 f a b acc) interpret comp_fun_commute f by fact show ?case proof (cases "a > b") case True thus ?thesis by (subst fold_atLeastAtMost_nat.simps) auto next case False with 1 show ?thesis by (subst fold_atLeastAtMost_nat.simps) (auto simp: atLeastAtMost_insertL[symmetric] fold_fun_left_comm) qed qed lemma sum_atLeastAtMost_code: "sum f {a..b} = fold_atLeastAtMost_nat (\a acc. f a + acc) a b 0" proof - have "comp_fun_commute (\a. (+) (f a))" by unfold_locales (auto simp: o_def add_ac) thus ?thesis by (simp add: sum.eq_fold fold_atLeastAtMost_nat o_def) qed lemma prod_atLeastAtMost_code: "prod f {a..b} = fold_atLeastAtMost_nat (\a acc. f a * acc) a b 1" proof - have "comp_fun_commute (\a. (*) (f a))" by unfold_locales (auto simp: o_def mult_ac) thus ?thesis by (simp add: prod.eq_fold fold_atLeastAtMost_nat o_def) qed (* TODO: Add support for folding over more kinds of intervals here *) end diff --git a/src/HOL/String.thy b/src/HOL/String.thy --- a/src/HOL/String.thy +++ b/src/HOL/String.thy @@ -1,743 +1,743 @@ (* Author: Tobias Nipkow, Florian Haftmann, TU Muenchen *) section \Character and string types\ theory String imports Enum begin subsection \Strings as list of bytes\ text \ When modelling strings, we follow the approach given in \<^url>\https://utf8everywhere.org/\: \<^item> Strings are a list of bytes (8 bit). \<^item> Byte values from 0 to 127 are US-ASCII. \<^item> Byte values from 128 to 255 are uninterpreted blobs. \ subsubsection \Bytes as datatype\ datatype char = Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool) (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool) context comm_semiring_1 begin definition of_char :: "char \ 'a" where "of_char c = ((((((of_bool (digit7 c) * 2 + of_bool (digit6 c)) * 2 + of_bool (digit5 c)) * 2 + of_bool (digit4 c)) * 2 + of_bool (digit3 c)) * 2 + of_bool (digit2 c)) * 2 + of_bool (digit1 c)) * 2 + of_bool (digit0 c)" lemma of_char_Char [simp]: "of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) = foldr (\b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0" by (simp add: of_char_def ac_simps) end -context unique_euclidean_semiring_with_nat +context unique_euclidean_semiring_with_bit_shifts begin definition char_of :: "'a \ char" where "char_of n = Char (odd n) (odd (drop_bit 1 n)) (odd (drop_bit 2 n)) (odd (drop_bit 3 n)) (odd (drop_bit 4 n)) (odd (drop_bit 5 n)) (odd (drop_bit 6 n)) (odd (drop_bit 7 n))" lemma char_of_char [simp]: "char_of (of_char c) = c" proof (cases c) have **: "drop_bit n (q * 2 + of_bool d) = drop_bit (n - 1) q + drop_bit n (of_bool d)" if "n > 0" for q :: 'a and n :: nat and d :: bool using that by (cases n) simp_all case (Char d0 d1 d2 d3 d4 d5 d6 d7) then show ?thesis by (simp only: of_char_def char_of_def char.simps char.sel drop_bit_of_bool **) simp qed lemma char_of_comp_of_char [simp]: "char_of \ of_char = id" by (simp add: fun_eq_iff) lemma inj_of_char: "inj of_char" proof (rule injI) fix c d assume "of_char c = of_char d" then have "char_of (of_char c) = char_of (of_char d)" by simp then show "c = d" by simp qed lemma of_char_eq_iff [simp]: "of_char c = of_char d \ c = d" by (simp add: inj_eq inj_of_char) lemma of_char_of [simp]: "of_char (char_of a) = a mod 256" proof - have *: "{0::nat..<8} = {0, 1, 2, 3, 4, 5, 6, 7}" by auto have "of_char (char_of (take_bit 8 a)) = (\k\{0, 1, 2, 3, 4, 5, 6, 7}. push_bit k (of_bool (odd (drop_bit k a))))" by (simp add: of_char_def char_of_def push_bit_of_1 drop_bit_take_bit) also have "\ = take_bit 8 a" using * take_bit_sum [of 8 a] by simp also have "char_of(take_bit 8 a) = char_of a" by (simp add: char_of_def drop_bit_take_bit) finally show ?thesis by (simp add: take_bit_eq_mod) qed lemma char_of_mod_256 [simp]: "char_of (n mod 256) = char_of n" by (metis char_of_char of_char_of) lemma of_char_mod_256 [simp]: "of_char c mod 256 = of_char c" by (metis char_of_char of_char_of) lemma char_of_quasi_inj [simp]: "char_of m = char_of n \ m mod 256 = n mod 256" by (metis char_of_mod_256 of_char_of) lemma char_of_nat_eq_iff: "char_of n = c \ take_bit 8 n = of_char c" by (simp add: take_bit_eq_mod) (use of_char_eq_iff in fastforce) lemma char_of_nat [simp]: "char_of (of_nat n) = char_of n" by (simp add: char_of_def String.char_of_def drop_bit_of_nat) end lemma inj_on_char_of_nat [simp]: "inj_on char_of {0::nat..<256}" by (rule inj_onI) simp lemma nat_of_char_less_256 [simp]: "of_char c < (256 :: nat)" proof - have "of_char c mod (256 :: nat) < 256" by arith then show ?thesis by simp qed lemma range_nat_of_char: "range of_char = {0::nat..<256}" proof (rule; rule) fix n :: nat assume "n \ range of_char" then show "n \ {0..<256}" by auto next fix n :: nat assume "n \ {0..<256}" then have "n = of_char (char_of n)" by simp then show "n \ range of_char" by (rule range_eqI) qed lemma UNIV_char_of_nat: "UNIV = char_of ` {0::nat..<256}" proof - have "range (of_char :: char \ nat) = of_char ` char_of ` {0::nat..<256}" by (auto simp add: range_nat_of_char intro!: image_eqI) with inj_of_char [where ?'a = nat] show ?thesis by (simp add: inj_image_eq_iff) qed lemma card_UNIV_char: "card (UNIV :: char set) = 256" by (auto simp add: UNIV_char_of_nat card_image) context includes lifting_syntax integer.lifting natural.lifting begin lemma [transfer_rule]: "(pcr_integer ===> (=)) (char_of :: int \ char) (char_of :: integer \ char)" by (unfold char_of_def [abs_def]) transfer_prover lemma [transfer_rule]: "((=) ===> pcr_integer) (of_char :: char \ int) (of_char :: char \ integer)" by (unfold of_char_def [abs_def]) transfer_prover lemma [transfer_rule]: "(pcr_natural ===> (=)) (char_of :: nat \ char) (char_of :: natural \ char)" by (unfold char_of_def [abs_def]) transfer_prover lemma [transfer_rule]: "((=) ===> pcr_natural) (of_char :: char \ nat) (of_char :: char \ natural)" by (unfold of_char_def [abs_def]) transfer_prover end lifting_update integer.lifting lifting_forget integer.lifting lifting_update natural.lifting lifting_forget natural.lifting syntax "_Char" :: "str_position \ char" ("CHR _") "_Char_ord" :: "num_const \ char" ("CHR _") type_synonym string = "char list" syntax "_String" :: "str_position \ string" ("_") ML_file \Tools/string_syntax.ML\ instantiation char :: enum begin definition "Enum.enum = [ CHR 0x00, CHR 0x01, CHR 0x02, CHR 0x03, CHR 0x04, CHR 0x05, CHR 0x06, CHR 0x07, CHR 0x08, CHR 0x09, CHR ''\'', CHR 0x0B, CHR 0x0C, CHR 0x0D, CHR 0x0E, CHR 0x0F, CHR 0x10, CHR 0x11, CHR 0x12, CHR 0x13, CHR 0x14, CHR 0x15, CHR 0x16, CHR 0x17, CHR 0x18, CHR 0x19, CHR 0x1A, CHR 0x1B, CHR 0x1C, CHR 0x1D, CHR 0x1E, CHR 0x1F, CHR '' '', CHR ''!'', CHR 0x22, CHR ''#'', CHR ''$'', CHR ''%'', CHR ''&'', CHR 0x27, CHR ''('', CHR '')'', CHR ''*'', CHR ''+'', CHR '','', CHR ''-'', CHR ''.'', CHR ''/'', CHR ''0'', CHR ''1'', CHR ''2'', CHR ''3'', CHR ''4'', CHR ''5'', CHR ''6'', CHR ''7'', CHR ''8'', CHR ''9'', CHR '':'', CHR '';'', CHR ''<'', CHR ''='', CHR ''>'', CHR ''?'', CHR ''@'', CHR ''A'', CHR ''B'', CHR ''C'', CHR ''D'', CHR ''E'', CHR ''F'', CHR ''G'', CHR ''H'', CHR ''I'', CHR ''J'', CHR ''K'', CHR ''L'', CHR ''M'', CHR ''N'', CHR ''O'', CHR ''P'', CHR ''Q'', CHR ''R'', CHR ''S'', CHR ''T'', CHR ''U'', CHR ''V'', CHR ''W'', CHR ''X'', CHR ''Y'', CHR ''Z'', CHR ''['', CHR 0x5C, CHR '']'', CHR ''^'', CHR ''_'', CHR 0x60, CHR ''a'', CHR ''b'', CHR ''c'', CHR ''d'', CHR ''e'', CHR ''f'', CHR ''g'', CHR ''h'', CHR ''i'', CHR ''j'', CHR ''k'', CHR ''l'', CHR ''m'', CHR ''n'', CHR ''o'', CHR ''p'', CHR ''q'', CHR ''r'', CHR ''s'', CHR ''t'', CHR ''u'', CHR ''v'', CHR ''w'', CHR ''x'', CHR ''y'', CHR ''z'', CHR ''{'', CHR ''|'', CHR ''}'', CHR ''~'', CHR 0x7F, CHR 0x80, CHR 0x81, CHR 0x82, CHR 0x83, CHR 0x84, CHR 0x85, CHR 0x86, CHR 0x87, CHR 0x88, CHR 0x89, CHR 0x8A, CHR 0x8B, CHR 0x8C, CHR 0x8D, CHR 0x8E, CHR 0x8F, CHR 0x90, CHR 0x91, CHR 0x92, CHR 0x93, CHR 0x94, CHR 0x95, CHR 0x96, CHR 0x97, CHR 0x98, CHR 0x99, CHR 0x9A, CHR 0x9B, CHR 0x9C, CHR 0x9D, CHR 0x9E, CHR 0x9F, CHR 0xA0, CHR 0xA1, CHR 0xA2, CHR 0xA3, CHR 0xA4, CHR 0xA5, CHR 0xA6, CHR 0xA7, CHR 0xA8, CHR 0xA9, CHR 0xAA, CHR 0xAB, CHR 0xAC, CHR 0xAD, CHR 0xAE, CHR 0xAF, CHR 0xB0, CHR 0xB1, CHR 0xB2, CHR 0xB3, CHR 0xB4, CHR 0xB5, CHR 0xB6, CHR 0xB7, CHR 0xB8, CHR 0xB9, CHR 0xBA, CHR 0xBB, CHR 0xBC, CHR 0xBD, CHR 0xBE, CHR 0xBF, CHR 0xC0, CHR 0xC1, CHR 0xC2, CHR 0xC3, CHR 0xC4, CHR 0xC5, CHR 0xC6, CHR 0xC7, CHR 0xC8, CHR 0xC9, CHR 0xCA, CHR 0xCB, CHR 0xCC, CHR 0xCD, CHR 0xCE, CHR 0xCF, CHR 0xD0, CHR 0xD1, CHR 0xD2, CHR 0xD3, CHR 0xD4, CHR 0xD5, CHR 0xD6, CHR 0xD7, CHR 0xD8, CHR 0xD9, CHR 0xDA, CHR 0xDB, CHR 0xDC, CHR 0xDD, CHR 0xDE, CHR 0xDF, CHR 0xE0, CHR 0xE1, CHR 0xE2, CHR 0xE3, CHR 0xE4, CHR 0xE5, CHR 0xE6, CHR 0xE7, CHR 0xE8, CHR 0xE9, CHR 0xEA, CHR 0xEB, CHR 0xEC, CHR 0xED, CHR 0xEE, CHR 0xEF, CHR 0xF0, CHR 0xF1, CHR 0xF2, CHR 0xF3, CHR 0xF4, CHR 0xF5, CHR 0xF6, CHR 0xF7, CHR 0xF8, CHR 0xF9, CHR 0xFA, CHR 0xFB, CHR 0xFC, CHR 0xFD, CHR 0xFE, CHR 0xFF]" definition "Enum.enum_all P \ list_all P (Enum.enum :: char list)" definition "Enum.enum_ex P \ list_ex P (Enum.enum :: char list)" lemma enum_char_unfold: "Enum.enum = map char_of [0..<256]" proof - have "map (of_char :: char \ nat) Enum.enum = [0..<256]" by (simp add: enum_char_def of_char_def upt_conv_Cons_Cons numeral_2_eq_2 [symmetric]) then have "map char_of (map (of_char :: char \ nat) Enum.enum) = map char_of [0..<256]" by simp then show ?thesis by simp qed instance proof show UNIV: "UNIV = set (Enum.enum :: char list)" by (simp add: enum_char_unfold UNIV_char_of_nat atLeast0LessThan) show "distinct (Enum.enum :: char list)" by (auto simp add: enum_char_unfold distinct_map intro: inj_onI) show "\P. Enum.enum_all P \ Ball (UNIV :: char set) P" by (simp add: UNIV enum_all_char_def list_all_iff) show "\P. Enum.enum_ex P \ Bex (UNIV :: char set) P" by (simp add: UNIV enum_ex_char_def list_ex_iff) qed end lemma linorder_char: "class.linorder (\c d. of_char c \ (of_char d :: nat)) (\c d. of_char c < (of_char d :: nat))" by standard auto text \Optimized version for execution\ definition char_of_integer :: "integer \ char" where [code_abbrev]: "char_of_integer = char_of" definition integer_of_char :: "char \ integer" where [code_abbrev]: "integer_of_char = of_char" lemma char_of_integer_code [code]: "char_of_integer k = (let (q0, b0) = bit_cut_integer k; (q1, b1) = bit_cut_integer q0; (q2, b2) = bit_cut_integer q1; (q3, b3) = bit_cut_integer q2; (q4, b4) = bit_cut_integer q3; (q5, b5) = bit_cut_integer q4; (q6, b6) = bit_cut_integer q5; (_, b7) = bit_cut_integer q6 in Char b0 b1 b2 b3 b4 b5 b6 b7)" by (simp add: bit_cut_integer_def char_of_integer_def char_of_def div_mult2_numeral_eq odd_iff_mod_2_eq_one drop_bit_eq_div) lemma integer_of_char_code [code]: "integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) = ((((((of_bool b7 * 2 + of_bool b6) * 2 + of_bool b5) * 2 + of_bool b4) * 2 + of_bool b3) * 2 + of_bool b2) * 2 + of_bool b1) * 2 + of_bool b0" by (simp only: integer_of_char_def of_char_def char.sel) subsection \Strings as dedicated type for target language code generation\ subsubsection \Logical specification\ context begin qualified definition ascii_of :: "char \ char" where "ascii_of c = Char (digit0 c) (digit1 c) (digit2 c) (digit3 c) (digit4 c) (digit5 c) (digit6 c) False" qualified lemma ascii_of_Char [simp]: "ascii_of (Char b0 b1 b2 b3 b4 b5 b6 b7) = Char b0 b1 b2 b3 b4 b5 b6 False" by (simp add: ascii_of_def) qualified lemma not_digit7_ascii_of [simp]: "\ digit7 (ascii_of c)" by (simp add: ascii_of_def) qualified lemma ascii_of_idem: "ascii_of c = c" if "\ digit7 c" using that by (cases c) simp qualified lemma char_of_ascii_of [simp]: "of_char (ascii_of c) = take_bit 7 (of_char c :: nat)" by (cases c) (simp add: numeral_3_eq_3 [symmetric] numeral_2_eq_2 [symmetric]) qualified typedef literal = "{cs. \c\set cs. \ digit7 c}" morphisms explode Abs_literal proof show "[] \ {cs. \c\set cs. \ digit7 c}" by simp qed qualified setup_lifting type_definition_literal qualified lift_definition implode :: "string \ literal" is "map ascii_of" by auto qualified lemma implode_explode_eq [simp]: "String.implode (String.explode s) = s" proof transfer fix cs show "map ascii_of cs = cs" if "\c\set cs. \ digit7 c" using that by (induction cs) (simp_all add: ascii_of_idem) qed qualified lemma explode_implode_eq [simp]: "String.explode (String.implode cs) = map ascii_of cs" by transfer rule end subsubsection \Syntactic representation\ text \ Logical ground representations for literals are: \<^enum> \0\ for the empty literal; \<^enum> \Literal b0 \ b6 s\ for a literal starting with one character and continued by another literal. Syntactic representations for literals are: \<^enum> Printable text as string prefixed with \STR\; \<^enum> A single ascii value as numerical hexadecimal value prefixed with \STR\. \ instantiation String.literal :: zero begin context begin qualified lift_definition zero_literal :: String.literal is Nil by simp instance .. end end context begin qualified abbreviation (output) empty_literal :: String.literal where "empty_literal \ 0" qualified lift_definition Literal :: "bool \ bool \ bool \ bool \ bool \ bool \ bool \ String.literal \ String.literal" is "\b0 b1 b2 b3 b4 b5 b6 cs. Char b0 b1 b2 b3 b4 b5 b6 False # cs" by auto qualified lemma Literal_eq_iff [simp]: "Literal b0 b1 b2 b3 b4 b5 b6 s = Literal c0 c1 c2 c3 c4 c5 c6 t \ (b0 \ c0) \ (b1 \ c1) \ (b2 \ c2) \ (b3 \ c3) \ (b4 \ c4) \ (b5 \ c5) \ (b6 \ c6) \ s = t" by transfer simp qualified lemma empty_neq_Literal [simp]: "empty_literal \ Literal b0 b1 b2 b3 b4 b5 b6 s" by transfer simp qualified lemma Literal_neq_empty [simp]: "Literal b0 b1 b2 b3 b4 b5 b6 s \ empty_literal" by transfer simp end code_datatype "0 :: String.literal" String.Literal syntax "_Literal" :: "str_position \ String.literal" ("STR _") "_Ascii" :: "num_const \ String.literal" ("STR _") ML_file \Tools/literal.ML\ subsubsection \Operations\ instantiation String.literal :: plus begin context begin qualified lift_definition plus_literal :: "String.literal \ String.literal \ String.literal" is "(@)" by auto instance .. end end instance String.literal :: monoid_add by (standard; transfer) simp_all instantiation String.literal :: size begin context includes literal.lifting begin lift_definition size_literal :: "String.literal \ nat" is length . end instance .. end instantiation String.literal :: equal begin context begin qualified lift_definition equal_literal :: "String.literal \ String.literal \ bool" is HOL.equal . instance by (standard; transfer) (simp add: equal) end end instantiation String.literal :: linorder begin context begin qualified lift_definition less_eq_literal :: "String.literal \ String.literal \ bool" is "ord.lexordp_eq (\c d. of_char c < (of_char d :: nat))" . qualified lift_definition less_literal :: "String.literal \ String.literal \ bool" is "ord.lexordp (\c d. of_char c < (of_char d :: nat))" . instance proof - from linorder_char interpret linorder "ord.lexordp_eq (\c d. of_char c < (of_char d :: nat))" "ord.lexordp (\c d. of_char c < (of_char d :: nat)) :: string \ string \ bool" by (rule linorder.lexordp_linorder) show "PROP ?thesis" by (standard; transfer) (simp_all add: less_le_not_le linear) qed end end lemma infinite_literal: "infinite (UNIV :: String.literal set)" proof - define S where "S = range (\n. replicate n CHR ''A'')" have "inj_on String.implode S" proof (rule inj_onI) fix cs ds assume "String.implode cs = String.implode ds" then have "String.explode (String.implode cs) = String.explode (String.implode ds)" by simp moreover assume "cs \ S" and "ds \ S" ultimately show "cs = ds" by (auto simp add: S_def) qed moreover have "infinite S" by (auto simp add: S_def dest: finite_range_imageI [of _ length]) ultimately have "infinite (String.implode ` S)" by (simp add: finite_image_iff) then show ?thesis by (auto intro: finite_subset) qed subsubsection \Executable conversions\ context begin qualified lift_definition asciis_of_literal :: "String.literal \ integer list" is "map of_char" . qualified lemma asciis_of_zero [simp, code]: "asciis_of_literal 0 = []" by transfer simp qualified lemma asciis_of_Literal [simp, code]: "asciis_of_literal (String.Literal b0 b1 b2 b3 b4 b5 b6 s) = of_char (Char b0 b1 b2 b3 b4 b5 b6 False) # asciis_of_literal s " by transfer simp qualified lift_definition literal_of_asciis :: "integer list \ String.literal" is "map (String.ascii_of \ char_of)" by auto qualified lemma literal_of_asciis_Nil [simp, code]: "literal_of_asciis [] = 0" by transfer simp qualified lemma literal_of_asciis_Cons [simp, code]: "literal_of_asciis (k # ks) = (case char_of k of Char b0 b1 b2 b3 b4 b5 b6 b7 \ String.Literal b0 b1 b2 b3 b4 b5 b6 (literal_of_asciis ks))" by (simp add: char_of_def) (transfer, simp add: char_of_def) qualified lemma literal_of_asciis_of_literal [simp]: "literal_of_asciis (asciis_of_literal s) = s" proof transfer fix cs assume "\c\set cs. \ digit7 c" then show "map (String.ascii_of \ char_of) (map of_char cs) = cs" by (induction cs) (simp_all add: String.ascii_of_idem) qed qualified lemma explode_code [code]: "String.explode s = map char_of (asciis_of_literal s)" by transfer simp qualified lemma implode_code [code]: "String.implode cs = literal_of_asciis (map of_char cs)" by transfer simp qualified lemma equal_literal [code]: "HOL.equal (String.Literal b0 b1 b2 b3 b4 b5 b6 s) (String.Literal a0 a1 a2 a3 a4 a5 a6 r) \ (b0 \ a0) \ (b1 \ a1) \ (b2 \ a2) \ (b3 \ a3) \ (b4 \ a4) \ (b5 \ a5) \ (b6 \ a6) \ (s = r)" by (simp add: equal) end subsubsection \Technical code generation setup\ text \Alternative constructor for generated computations\ context begin qualified definition Literal' :: "bool \ bool \ bool \ bool \ bool \ bool \ bool \ String.literal \ String.literal" where [simp]: "Literal' = String.Literal" lemma [code]: "Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis [foldr (\b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0] + s" unfolding Literal'_def by transfer (simp add: char_of_def) lemma [code_computation_unfold]: "String.Literal = Literal'" by simp end code_reserved SML string String Char List code_reserved OCaml string String Char List code_reserved Haskell Prelude code_reserved Scala string code_printing type_constructor String.literal \ (SML) "string" and (OCaml) "string" and (Haskell) "String" and (Scala) "String" | constant "STR ''''" \ (SML) "\"\"" and (OCaml) "\"\"" and (Haskell) "\"\"" and (Scala) "\"\"" setup \ fold Literal.add_code ["SML", "OCaml", "Haskell", "Scala"] \ code_printing constant "(+) :: String.literal \ String.literal \ String.literal" \ (SML) infixl 18 "^" and (OCaml) infixr 6 "^" and (Haskell) infixr 5 "++" and (Scala) infixl 7 "+" | constant String.literal_of_asciis \ (SML) "!(String.implode/ o List.map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))" and (OCaml) "!(let xs = _ and chr k = let l = Z.to'_int k in if 0 <= l && l < 128 then Char.chr l else failwith \"Non-ASCII character in literal\" in String.init (List.length xs) (List.nth (List.map chr xs)))" and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)" and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))" | constant String.asciis_of_literal \ (SML) "!(List.map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)" and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (String.get s i) in if k < 128 then Z.of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (String.length s - 1) [])" and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))" and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))" | class_instance String.literal :: equal \ (Haskell) - | constant "HOL.equal :: String.literal \ String.literal \ bool" \ (SML) "!((_ : string) = _)" and (OCaml) "!((_ : string) = _)" and (Haskell) infix 4 "==" and (Scala) infixl 5 "==" | constant "(\) :: String.literal \ String.literal \ bool" \ (SML) "!((_ : string) <= _)" and (OCaml) "!((_ : string) <= _)" and (Haskell) infix 4 "<=" \ \Order operations for \<^typ>\String.literal\ work in Haskell only if no type class instance needs to be generated, because String = [Char] in Haskell and \<^typ>\char list\ need not have the same order as \<^typ>\String.literal\.\ and (Scala) infixl 4 "<=" and (Eval) infixl 6 "<=" | constant "(<) :: String.literal \ String.literal \ bool" \ (SML) "!((_ : string) < _)" and (OCaml) "!((_ : string) < _)" and (Haskell) infix 4 "<" and (Scala) infixl 4 "<" and (Eval) infixl 6 "<" subsubsection \Code generation utility\ setup \Sign.map_naming (Name_Space.mandatory_path "Code")\ definition abort :: "String.literal \ (unit \ 'a) \ 'a" where [simp]: "abort _ f = f ()" declare [[code drop: Code.abort]] lemma abort_cong: "msg = msg' \ Code.abort msg f = Code.abort msg' f" by simp setup \Sign.map_naming Name_Space.parent_path\ setup \Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong})\ code_printing constant Code.abort \ (SML) "!(raise/ Fail/ _)" and (OCaml) "failwith" and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)" and (Scala) "!{/ sys.error((_));/ ((_)).apply(())/ }" subsubsection \Finally\ lifting_update literal.lifting lifting_forget literal.lifting end diff --git a/src/HOL/ex/Bit_Lists.thy b/src/HOL/ex/Bit_Lists.thy --- a/src/HOL/ex/Bit_Lists.thy +++ b/src/HOL/ex/Bit_Lists.thy @@ -1,368 +1,367 @@ (* Author: Florian Haftmann, TUM *) section \Proof(s) of concept for algebraically founded lists of bits\ theory Bit_Lists imports Bit_Operations begin subsection \Fragments of algebraic bit representations\ context comm_semiring_1 begin primrec radix_value :: "('b \ 'a) \ 'a \ 'b list \ 'a" where "radix_value f b [] = 0" | "radix_value f b (a # as) = f a + radix_value f b as * b" abbreviation (input) unsigned_of_bits :: "bool list \ 'a" where "unsigned_of_bits \ radix_value of_bool 2" lemma unsigned_of_bits_replicate_False [simp]: "unsigned_of_bits (replicate n False) = 0" by (induction n) simp_all end -context unique_euclidean_semiring_with_nat +context unique_euclidean_semiring_with_bit_shifts begin lemma unsigned_of_bits_append [simp]: "unsigned_of_bits (bs @ cs) = unsigned_of_bits bs + push_bit (length bs) (unsigned_of_bits cs)" by (induction bs) (simp_all add: push_bit_double, simp_all add: algebra_simps) lemma unsigned_of_bits_take [simp]: "unsigned_of_bits (take n bs) = Parity.take_bit n (unsigned_of_bits bs)" proof (induction bs arbitrary: n) case Nil then show ?case by simp next case (Cons b bs) then show ?case by (cases n) (simp_all add: ac_simps) qed lemma unsigned_of_bits_drop [simp]: "unsigned_of_bits (drop n bs) = Parity.drop_bit n (unsigned_of_bits bs)" proof (induction bs arbitrary: n) case Nil then show ?case by simp next case (Cons b bs) then show ?case by (cases n) simp_all qed primrec n_bits_of :: "nat \ 'a \ bool list" where "n_bits_of 0 a = []" | "n_bits_of (Suc n) a = odd a # n_bits_of n (a div 2)" lemma n_bits_of_eq_iff: "n_bits_of n a = n_bits_of n b \ Parity.take_bit n a = Parity.take_bit n b" apply (induction n arbitrary: a b) apply (auto elim!: evenE oddE) apply (metis dvd_triv_right even_plus_one_iff) apply (metis dvd_triv_right even_plus_one_iff) done lemma take_n_bits_of [simp]: "take m (n_bits_of n a) = n_bits_of (min m n) a" proof - define q and v and w where "q = min m n" and "v = m - q" and "w = n - q" then have "v = 0 \ w = 0" by auto then have "take (q + v) (n_bits_of (q + w) a) = n_bits_of q a" by (induction q arbitrary: a) auto with q_def v_def w_def show ?thesis by simp qed lemma unsigned_of_bits_n_bits_of [simp]: "unsigned_of_bits (n_bits_of n a) = Parity.take_bit n a" by (induction n arbitrary: a) (simp_all add: ac_simps) end subsection \Syntactic bit representation\ class bit_representation = fixes bits_of :: "'a \ bool list" and of_bits :: "bool list \ 'a" assumes of_bits_of [simp]: "of_bits (bits_of a) = a" text \Unclear whether a \<^typ>\bool\ instantiation is needed or not\ instantiation nat :: bit_representation begin fun bits_of_nat :: "nat \ bool list" where "bits_of (n::nat) = (if n = 0 then [] else odd n # bits_of (n div 2))" lemma bits_of_nat_simps [simp]: "bits_of (0::nat) = []" "n > 0 \ bits_of n = odd n # bits_of (n div 2)" for n :: nat by simp_all declare bits_of_nat.simps [simp del] definition of_bits_nat :: "bool list \ nat" where [simp]: "of_bits_nat = unsigned_of_bits" \ \remove simp\ instance proof show "of_bits (bits_of n) = n" for n :: nat by (induction n rule: nat_bit_induct) simp_all qed end lemma bits_of_Suc_0 [simp]: "bits_of (Suc 0) = [True]" by simp lemma bits_of_1_nat [simp]: "bits_of (1 :: nat) = [True]" by simp lemma bits_of_nat_numeral_simps [simp]: "bits_of (numeral Num.One :: nat) = [True]" (is ?One) "bits_of (numeral (Num.Bit0 n) :: nat) = False # bits_of (numeral n :: nat)" (is ?Bit0) "bits_of (numeral (Num.Bit1 n) :: nat) = True # bits_of (numeral n :: nat)" (is ?Bit1) proof - show ?One by simp define m :: nat where "m = numeral n" then have "m > 0" and *: "numeral n = m" "numeral (Num.Bit0 n) = 2 * m" "numeral (Num.Bit1 n) = Suc (2 * m)" by simp_all from \m > 0\ show ?Bit0 ?Bit1 by (simp_all add: *) qed lemma unsigned_of_bits_of_nat [simp]: "unsigned_of_bits (bits_of n) = n" for n :: nat using of_bits_of [of n] by simp instantiation int :: bit_representation begin fun bits_of_int :: "int \ bool list" where "bits_of_int k = odd k # (if k = 0 \ k = - 1 then [] else bits_of_int (k div 2))" lemma bits_of_int_simps [simp]: "bits_of (0 :: int) = [False]" "bits_of (- 1 :: int) = [True]" "k \ 0 \ k \ - 1 \ bits_of k = odd k # bits_of (k div 2)" for k :: int by simp_all lemma bits_of_not_Nil [simp]: "bits_of k \ []" for k :: int by simp declare bits_of_int.simps [simp del] definition of_bits_int :: "bool list \ int" where "of_bits_int bs = (if bs = [] \ \ last bs then unsigned_of_bits bs else unsigned_of_bits bs - 2 ^ length bs)" lemma of_bits_int_simps [simp]: "of_bits [] = (0 :: int)" "of_bits [False] = (0 :: int)" "of_bits [True] = (- 1 :: int)" "of_bits (bs @ [b]) = (unsigned_of_bits bs :: int) - (2 ^ length bs) * of_bool b" "of_bits (False # bs) = 2 * (of_bits bs :: int)" "bs \ [] \ of_bits (True # bs) = 1 + 2 * (of_bits bs :: int)" by (simp_all add: of_bits_int_def push_bit_of_1) instance proof show "of_bits (bits_of k) = k" for k :: int by (induction k rule: int_bit_induct) simp_all qed lemma bits_of_1_int [simp]: "bits_of (1 :: int) = [True, False]" by simp lemma bits_of_int_numeral_simps [simp]: "bits_of (numeral Num.One :: int) = [True, False]" (is ?One) "bits_of (numeral (Num.Bit0 n) :: int) = False # bits_of (numeral n :: int)" (is ?Bit0) "bits_of (numeral (Num.Bit1 n) :: int) = True # bits_of (numeral n :: int)" (is ?Bit1) "bits_of (- numeral (Num.Bit0 n) :: int) = False # bits_of (- numeral n :: int)" (is ?nBit0) "bits_of (- numeral (Num.Bit1 n) :: int) = True # bits_of (- numeral (Num.inc n) :: int)" (is ?nBit1) proof - show ?One by simp define k :: int where "k = numeral n" then have "k > 0" and *: "numeral n = k" "numeral (Num.Bit0 n) = 2 * k" "numeral (Num.Bit1 n) = 2 * k + 1" "numeral (Num.inc n) = k + 1" by (simp_all add: add_One) have "- (2 * k) div 2 = - k" "(- (2 * k) - 1) div 2 = - k - 1" by simp_all with \k > 0\ show ?Bit0 ?Bit1 ?nBit0 ?nBit1 by (simp_all add: *) qed lemma of_bits_append [simp]: "of_bits (bs @ cs) = of_bits bs + push_bit (length bs) (of_bits cs :: int)" if "bs \ []" "\ last bs" using that proof (induction bs rule: list_nonempty_induct) case (single b) then show ?case by simp next case (cons b bs) then show ?case by (cases b) (simp_all add: push_bit_double) qed lemma of_bits_replicate_False [simp]: "of_bits (replicate n False) = (0 :: int)" by (auto simp add: of_bits_int_def) lemma of_bits_drop [simp]: "of_bits (drop n bs) = Parity.drop_bit n (of_bits bs :: int)" if "n < length bs" using that proof (induction bs arbitrary: n) case Nil then show ?case by simp next case (Cons b bs) show ?case proof (cases n) case 0 then show ?thesis by simp next case (Suc n) with Cons.prems have "bs \ []" by auto with Suc Cons.IH [of n] Cons.prems show ?thesis by (cases b) simp_all qed qed end lemma unsigned_of_bits_eq_of_bits: "unsigned_of_bits bs = (of_bits (bs @ [False]) :: int)" by (simp add: of_bits_int_def) instantiation word :: (len) bit_representation begin lift_definition bits_of_word :: "'a word \ bool list" is "n_bits_of LENGTH('a)" by (simp add: n_bits_of_eq_iff) lift_definition of_bits_word :: "bool list \ 'a word" is unsigned_of_bits . instance proof fix a :: "'a word" show "of_bits (bits_of a) = a" by transfer simp qed end subsection \Bit representations with bit operations\ class semiring_bit_representation = semiring_bit_operations + bit_representation + assumes and_eq: "length bs = length cs \ of_bits bs AND of_bits cs = of_bits (map2 (\) bs cs)" and or_eq: "length bs = length cs \ of_bits bs OR of_bits cs = of_bits (map2 (\) bs cs)" and xor_eq: "length bs = length cs \ of_bits bs XOR of_bits cs = of_bits (map2 (\) bs cs)" - and shift_bit_eq: "shift_bit n a = of_bits (replicate n False @ bits_of a)" + and push_bit_eq: "push_bit n a = of_bits (replicate n False @ bits_of a)" and drop_bit_eq: "n < length (bits_of a) \ drop_bit n a = of_bits (drop n (bits_of a))" class ring_bit_representation = ring_bit_operations + semiring_bit_representation + assumes not_eq: "not = of_bits \ map Not \ bits_of" context zip_nat begin lemma of_bits: "of_bits bs \<^bold>\ of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: nat)" if "length bs = length cs" for bs cs using that proof (induction bs cs rule: list_induct2) case Nil then show ?case by simp next case (Cons b bs c cs) then show ?case by (cases "of_bits bs = (0::nat) \ of_bits cs = (0::nat)") (auto simp add: ac_simps end_of_bits rec [of "Suc 0"]) qed end instance nat :: semiring_bit_representation apply standard apply (simp_all only: and_nat.of_bits or_nat.of_bits xor_nat.of_bits) - apply (simp_all add: drop_bit_eq_div Parity.drop_bit_eq_div shift_bit_eq_mult push_bit_eq_mult) + apply simp_all done context zip_int begin lemma of_bits: "of_bits bs \<^bold>\ of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: int)" if "length bs = length cs" and "\ False \<^bold>* False" for bs cs using \length bs = length cs\ proof (induction bs cs rule: list_induct2) case Nil then show ?case using \\ False \<^bold>* False\ by (auto simp add: False_False_imp_True_True split: bool.splits) next case (Cons b bs c cs) show ?case proof (cases "bs = []") case True with Cons show ?thesis using \\ False \<^bold>* False\ by (cases b; cases c) (auto simp add: ac_simps split: bool.splits) next case False with Cons.hyps have "cs \ []" by auto with \bs \ []\ have "map2 (\<^bold>*) bs cs \ []" by (simp add: zip_eq_Nil_iff) from \bs \ []\ \cs \ []\ \map2 (\<^bold>*) bs cs \ []\ Cons show ?thesis by (cases b; cases c) (auto simp add: \\ False \<^bold>* False\ ac_simps rec [of "of_bits bs * 2"] rec [of "of_bits cs * 2"] rec [of "1 + of_bits bs * 2"]) qed qed end instance int :: ring_bit_representation proof show "(not :: int \ _) = of_bits \ map Not \ bits_of" proof (rule sym, rule ext) fix k :: int show "(of_bits \ map Not \ bits_of) k = NOT k" by (induction k rule: int_bit_induct) (simp_all add: not_int_def) qed - show "shift_bit n k = of_bits (replicate n False @ bits_of k)" + show "push_bit n k = of_bits (replicate n False @ bits_of k)" for k :: int and n :: nat - by (cases "n = 0") (simp_all add: shift_bit_eq_push_bit) -qed (simp_all add: and_int.of_bits or_int.of_bits xor_int.of_bits - drop_bit_eq_drop_bit) + by (cases "n = 0") simp_all +qed (simp_all add: and_int.of_bits or_int.of_bits xor_int.of_bits) end diff --git a/src/HOL/ex/Bit_Operations.thy b/src/HOL/ex/Bit_Operations.thy --- a/src/HOL/ex/Bit_Operations.thy +++ b/src/HOL/ex/Bit_Operations.thy @@ -1,1033 +1,790 @@ (* Author: Florian Haftmann, TUM *) section \Proof of concept for purely algebraically founded lists of bits\ theory Bit_Operations imports "HOL-Library.Boolean_Algebra" Word begin -hide_const (open) drop_bit take_bit - -subsection \Algebraic structures with bits\ - -class semiring_bits = semiring_parity + - assumes bit_split_eq: \\a. of_bool (odd a) + 2 * (a div 2) = a\ - and bit_eq_rec: \\a b. a = b \ (even a = even b) \ a div 2 = b div 2\ - and 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\ - - -subsubsection \Instance \<^typ>\nat\\ - -instance nat :: semiring_bits -proof - show \of_bool (odd n) + 2 * (n div 2) = n\ - for n :: nat - by simp - show \m = n \ (even m \ even n) \ m div 2 = n div 2\ - for m n :: nat - by (auto dest: odd_two_times_div_two_succ) - 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 -qed - - -subsubsection \Instance \<^typ>\int\\ - -instance int :: semiring_bits -proof - show \of_bool (odd k) + 2 * (k div 2) = k\ - for k :: int - by (auto elim: oddE) - show \k = l \ (even k \ even l) \ k div 2 = l div 2\ - for k l :: int - by (auto dest: odd_two_times_div_two_succ) - 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 -qed - - -subsubsection \Instance \<^typ>\'a word\\ - -instance word :: (len) semiring_bits -proof - show \of_bool (odd a) + 2 * (a div 2) = a\ - for a :: \'a word\ - apply (cases \even a\; simp, transfer; cases rule: length_cases [where ?'a = 'a]) - apply auto - apply (auto simp add: take_bit_eq_mod) - apply (metis add.commute even_take_bit_eq len_not_eq_0 mod_mod_trivial odd_two_times_div_two_succ take_bit_eq_mod) - done - show \a = b \ (even a \ even b) \ a div 2 = b div 2\ - for a b :: \'a word\ - apply transfer - apply (cases rule: length_cases [where ?'a = 'a]) - apply auto - apply (metis even_take_bit_eq len_not_eq_0) - apply (metis even_take_bit_eq len_not_eq_0) - apply (metis (no_types, hide_lams) diff_add_cancel dvd_div_mult_self even_take_bit_eq mult_2_right take_bit_add take_bit_minus) - apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod) - done - 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 -qed - - -subsection \Bit shifts in suitable algebraic structures\ - -class semiring_bit_shifts = semiring_bits + - fixes shift_bit :: \nat \ 'a \ 'a\ - assumes shift_bit_eq_mult: \shift_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>\shift_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. -\ - -end - -subsubsection \Instance \<^typ>\nat\\ - -instantiation nat :: semiring_bit_shifts -begin - -definition shift_bit_nat :: \nat \ nat \ nat\ - where \shift_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 \shift_bit n m = m * 2 ^ n\ for n m :: nat - by (simp add: shift_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 - - -subsubsection \Instance \<^typ>\int\\ - -instantiation int :: semiring_bit_shifts -begin - -definition shift_bit_int :: \nat \ int \ int\ - where \shift_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 \shift_bit n k = k * 2 ^ n\ for n :: nat and k :: int - by (simp add: shift_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 - -lemma shift_bit_eq_push_bit: - \shift_bit = (push_bit :: nat \ int \ int)\ - by (simp add: fun_eq_iff push_bit_eq_mult shift_bit_eq_mult) - -lemma drop_bit_eq_drop_bit: - \drop_bit = (Parity.drop_bit :: nat \ int \ int)\ - by (simp add: fun_eq_iff drop_bit_eq_div Parity.drop_bit_eq_div) - -lemma take_bit_eq_take_bit: - \take_bit = (Parity.take_bit :: nat \ int \ int)\ - by (simp add: fun_eq_iff take_bit_eq_mod Parity.take_bit_eq_mod) - - -subsubsection \Instance \<^typ>\'a word\\ - -instantiation word :: (len) semiring_bit_shifts -begin - -lift_definition shift_bit_word :: \nat \ 'a word \ 'a word\ - is shift_bit -proof - - show \Parity.take_bit LENGTH('a) (shift_bit n k) = Parity.take_bit LENGTH('a) (shift_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: shift_bit_eq_push_bit 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 Parity.take_bit_eq_mod) - -instance proof - show \shift_bit n a = a * 2 ^ n\ for n :: nat and a :: "'a word" - by transfer (simp add: shift_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: Parity.take_bit_eq_mod 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: Parity.take_bit_eq_mod take_bit_eq_mod drop_bit_eq_div power_add zdiv_zmult2_eq) - qed -qed - -end - - subsection \Bit operations in suitable algebraic structures\ class semiring_bit_operations = semiring_bit_shifts + fixes "and" :: "'a \ 'a \ 'a" (infixr "AND" 64) and or :: "'a \ 'a \ 'a" (infixr "OR" 59) and xor :: "'a \ 'a \ 'a" (infixr "XOR" 59) begin text \ We want the bitwise operations to bind slightly weaker - than \+\ and \-\, but \~~\ to - bind slightly stronger than \*\. + than \+\ and \-\. For the sake of code generation the operations \<^const>\and\, \<^const>\or\ and \<^const>\xor\ are specified as definitional class operations. \ definition bit :: \'a \ nat \ bool\ where \bit a n \ odd (drop_bit n a)\ definition map_bit :: \nat \ (bool \ bool) \ 'a \ 'a\ - where \map_bit n f a = take_bit n a + shift_bit n (of_bool (f (bit a n)) + drop_bit (Suc n) a)\ + where \map_bit n f a = take_bit n a + push_bit n (of_bool (f (bit a n)) + drop_bit (Suc n) a)\ definition set_bit :: \nat \ 'a \ 'a\ where \set_bit n = map_bit n top\ definition unset_bit :: \nat \ 'a \ 'a\ where \unset_bit n = map_bit n bot\ definition flip_bit :: \nat \ 'a \ 'a\ where \flip_bit n = map_bit n Not\ text \ The logical core are \<^const>\bit\ and \<^const>\map_bit\; having <^const>\set_bit\, \<^const>\unset_bit\ and \<^const>\flip_bit\ as separate operations allows to implement them using bit masks later. \ end class ring_bit_operations = semiring_bit_operations + ring_parity + fixes not :: \'a \ 'a\ (\NOT\) assumes boolean_algebra: \boolean_algebra (AND) (OR) NOT 0 (- 1)\ and boolean_algebra_xor_eq: \boolean_algebra.xor (AND) (OR) NOT = (XOR)\ begin sublocale bit: boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ rewrites \bit.xor = (XOR)\ proof - interpret bit: boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ by (fact boolean_algebra) show \boolean_algebra (AND) (OR) NOT 0 (- 1)\ by standard show \boolean_algebra.xor (AND) (OR) NOT = (XOR)\ by (fact boolean_algebra_xor_eq) qed text \ For the sake of code generation \<^const>\not\ is specified as definitional class operation. Note that \<^const>\not\ has no sensible definition for unlimited but only positive bit strings (type \<^typ>\nat\). \ end subsubsection \Instance \<^typ>\nat\\ locale zip_nat = single: abel_semigroup f for f :: "bool \ bool \ bool" (infixl "\<^bold>*" 70) + assumes end_of_bits: "\ False \<^bold>* False" begin lemma False_P_imp: "False \<^bold>* True \ P" if "False \<^bold>* P" using that end_of_bits by (cases P) simp_all function F :: "nat \ nat \ nat" (infixl "\<^bold>\" 70) where "m \<^bold>\ n = (if m = 0 \ n = 0 then 0 else of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2)" by auto termination by (relation "measure (case_prod (+))") auto lemma zero_left_eq: "0 \<^bold>\ n = of_bool (False \<^bold>* True) * n" by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits) lemma zero_right_eq: "m \<^bold>\ 0 = of_bool (True \<^bold>* False) * m" by (induction m rule: nat_bit_induct) (simp_all add: end_of_bits) lemma simps [simp]: "0 \<^bold>\ 0 = 0" "0 \<^bold>\ n = of_bool (False \<^bold>* True) * n" "m \<^bold>\ 0 = of_bool (True \<^bold>* False) * m" "m > 0 \ n > 0 \ m \<^bold>\ n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2" by (simp_all only: zero_left_eq zero_right_eq) simp lemma rec: "m \<^bold>\ n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\ (n div 2) * 2" by (cases "m = 0 \ n = 0") (auto simp add: end_of_bits) declare F.simps [simp del] sublocale abel_semigroup F proof show "m \<^bold>\ n \<^bold>\ q = m \<^bold>\ (n \<^bold>\ q)" for m n q :: nat proof (induction m arbitrary: n q rule: nat_bit_induct) case zero show ?case by simp next case (even m) with rec [of "2 * m"] rec [of _ q] show ?case by (cases "even n") (auto dest: False_P_imp) next case (odd m) with rec [of "Suc (2 * m)"] rec [of _ q] show ?case by (cases "even n"; cases "even q") (auto dest: False_P_imp simp add: ac_simps) qed show "m \<^bold>\ n = n \<^bold>\ m" for m n :: nat proof (induction m arbitrary: n rule: nat_bit_induct) case zero show ?case by (simp add: ac_simps) next case (even m) with rec [of "2 * m" n] rec [of n "2 * m"] show ?case by (simp add: ac_simps) next case (odd m) with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case by (simp add: ac_simps) qed qed lemma self [simp]: "n \<^bold>\ n = of_bool (True \<^bold>* True) * n" by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits) lemma even_iff [simp]: "even (m \<^bold>\ n) \ \ (odd m \<^bold>* odd n)" proof (induction m arbitrary: n rule: nat_bit_induct) case zero show ?case by (cases "even n") (simp_all add: end_of_bits) next case (even m) then show ?case by (simp add: rec [of "2 * m"]) next case (odd m) then show ?case by (simp add: rec [of "Suc (2 * m)"]) qed end instantiation nat :: semiring_bit_operations begin global_interpretation and_nat: zip_nat "(\)" defines and_nat = and_nat.F by standard auto global_interpretation and_nat: semilattice "(AND) :: nat \ nat \ nat" proof (rule semilattice.intro, fact and_nat.abel_semigroup_axioms, standard) show "n AND n = n" for n :: nat by (simp add: and_nat.self) qed declare and_nat.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ lemma zero_nat_and_eq [simp]: "0 AND n = 0" for n :: nat by simp lemma and_zero_nat_eq [simp]: "n AND 0 = 0" for n :: nat by simp global_interpretation or_nat: zip_nat "(\)" defines or_nat = or_nat.F by standard auto global_interpretation or_nat: semilattice "(OR) :: nat \ nat \ nat" proof (rule semilattice.intro, fact or_nat.abel_semigroup_axioms, standard) show "n OR n = n" for n :: nat by (simp add: or_nat.self) qed declare or_nat.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ lemma zero_nat_or_eq [simp]: "0 OR n = n" for n :: nat by simp lemma or_zero_nat_eq [simp]: "n OR 0 = n" for n :: nat by simp global_interpretation xor_nat: zip_nat "(\)" defines xor_nat = xor_nat.F by standard auto declare xor_nat.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ lemma zero_nat_xor_eq [simp]: "0 XOR n = n" for n :: nat by simp lemma xor_zero_nat_eq [simp]: "n XOR 0 = n" for n :: nat by simp instance .. end global_interpretation or_nat: semilattice_neutr "(OR)" "0 :: nat" by standard simp global_interpretation xor_nat: comm_monoid "(XOR)" "0 :: nat" by standard simp lemma Suc_0_and_eq [simp]: "Suc 0 AND n = n mod 2" by (cases n) auto lemma and_Suc_0_eq [simp]: "n AND Suc 0 = n mod 2" using Suc_0_and_eq [of n] by (simp add: ac_simps) lemma Suc_0_or_eq [simp]: "Suc 0 OR n = n + of_bool (even n)" by (cases n) (simp_all add: ac_simps) lemma or_Suc_0_eq [simp]: "n OR Suc 0 = n + of_bool (even n)" using Suc_0_or_eq [of n] by (simp add: ac_simps) lemma Suc_0_xor_eq [simp]: "Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)" by (cases n) (simp_all add: ac_simps) lemma xor_Suc_0_eq [simp]: "n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)" using Suc_0_xor_eq [of n] by (simp add: ac_simps) subsubsection \Instance \<^typ>\int\\ abbreviation (input) complement :: "int \ int" where "complement k \ - k - 1" lemma complement_half: "complement (k * 2) div 2 = complement k" by simp lemma complement_div_2: "complement (k div 2) = complement k div 2" by linarith locale zip_int = single: abel_semigroup f for f :: "bool \ bool \ bool" (infixl "\<^bold>*" 70) begin lemma False_False_imp_True_True: "True \<^bold>* True" if "False \<^bold>* False" proof (rule ccontr) assume "\ True \<^bold>* True" with that show False using single.assoc [of False True True] by (cases "False \<^bold>* True") simp_all qed function F :: "int \ int \ int" (infixl "\<^bold>\" 70) where "k \<^bold>\ l = (if k \ {0, - 1} \ l \ {0, - 1} then - of_bool (odd k \<^bold>* odd l) else of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2)" by auto termination by (relation "measure (\(k, l). nat (\k\ + \l\))") auto lemma zero_left_eq: "0 \<^bold>\ l = (case (False \<^bold>* False, False \<^bold>* True) of (False, False) \ 0 | (False, True) \ l | (True, False) \ complement l | (True, True) \ - 1)" by (induction l rule: int_bit_induct) (simp_all split: bool.split) lemma minus_left_eq: "- 1 \<^bold>\ l = (case (True \<^bold>* False, True \<^bold>* True) of (False, False) \ 0 | (False, True) \ l | (True, False) \ complement l | (True, True) \ - 1)" by (induction l rule: int_bit_induct) (simp_all split: bool.split) lemma zero_right_eq: "k \<^bold>\ 0 = (case (False \<^bold>* False, False \<^bold>* True) of (False, False) \ 0 | (False, True) \ k | (True, False) \ complement k | (True, True) \ - 1)" by (induction k rule: int_bit_induct) (simp_all add: ac_simps split: bool.split) lemma minus_right_eq: "k \<^bold>\ - 1 = (case (True \<^bold>* False, True \<^bold>* True) of (False, False) \ 0 | (False, True) \ k | (True, False) \ complement k | (True, True) \ - 1)" by (induction k rule: int_bit_induct) (simp_all add: ac_simps split: bool.split) lemma simps [simp]: "0 \<^bold>\ 0 = - of_bool (False \<^bold>* False)" "- 1 \<^bold>\ 0 = - of_bool (True \<^bold>* False)" "0 \<^bold>\ - 1 = - of_bool (False \<^bold>* True)" "- 1 \<^bold>\ - 1 = - of_bool (True \<^bold>* True)" "0 \<^bold>\ l = (case (False \<^bold>* False, False \<^bold>* True) of (False, False) \ 0 | (False, True) \ l | (True, False) \ complement l | (True, True) \ - 1)" "- 1 \<^bold>\ l = (case (True \<^bold>* False, True \<^bold>* True) of (False, False) \ 0 | (False, True) \ l | (True, False) \ complement l | (True, True) \ - 1)" "k \<^bold>\ 0 = (case (False \<^bold>* False, False \<^bold>* True) of (False, False) \ 0 | (False, True) \ k | (True, False) \ complement k | (True, True) \ - 1)" "k \<^bold>\ - 1 = (case (True \<^bold>* False, True \<^bold>* True) of (False, False) \ 0 | (False, True) \ k | (True, False) \ complement k | (True, True) \ - 1)" "k \ 0 \ k \ - 1 \ l \ 0 \ l \ - 1 \ k \<^bold>\ l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2" by simp_all[4] (simp_all only: zero_left_eq minus_left_eq zero_right_eq minus_right_eq, simp) declare F.simps [simp del] lemma rec: "k \<^bold>\ l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\ (l div 2) * 2" by (cases "k \ {0, - 1} \ l \ {0, - 1}") (auto simp add: ac_simps F.simps [of k l] split: bool.split) sublocale abel_semigroup F proof show "k \<^bold>\ l \<^bold>\ r = k \<^bold>\ (l \<^bold>\ r)" for k l r :: int proof (induction k arbitrary: l r rule: int_bit_induct) case zero have "complement l \<^bold>\ r = complement (l \<^bold>\ r)" if "False \<^bold>* False" "\ False \<^bold>* True" proof (induction l arbitrary: r rule: int_bit_induct) case zero from that show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case minus from that show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case (even l) with that rec [of _ r] show ?case by (cases "even r") (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits) next case (odd l) moreover have "- l - 1 = - 1 - l" by simp ultimately show ?case using that rec [of _ r] by (cases "even r") (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) qed then show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case minus have "complement l \<^bold>\ r = complement (l \<^bold>\ r)" if "\ True \<^bold>* True" "False \<^bold>* True" proof (induction l arbitrary: r rule: int_bit_induct) case zero from that show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case minus from that show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case (even l) with that rec [of _ r] show ?case by (cases "even r") (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits) next case (odd l) moreover have "- l - 1 = - 1 - l" by simp ultimately show ?case using that rec [of _ r] by (cases "even r") (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) qed then show ?case by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits) next case (even k) with rec [of "k * 2"] rec [of _ r] show ?case by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True) next case (odd k) with rec [of "1 + k * 2"] rec [of _ r] show ?case by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True) qed show "k \<^bold>\ l = l \<^bold>\ k" for k l :: int proof (induction k arbitrary: l rule: int_bit_induct) case zero show ?case by simp next case minus show ?case by simp next case (even k) with rec [of "k * 2" l] rec [of l "k * 2"] show ?case by (simp add: ac_simps) next case (odd k) with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case by (simp add: ac_simps) qed qed lemma self [simp]: "k \<^bold>\ k = (case (False \<^bold>* False, True \<^bold>* True) of (False, False) \ 0 | (False, True) \ k | (True, True) \ - 1)" by (induction k rule: int_bit_induct) (auto simp add: False_False_imp_True_True split: bool.split) lemma even_iff [simp]: "even (k \<^bold>\ l) \ \ (odd k \<^bold>* odd l)" proof (induction k arbitrary: l rule: int_bit_induct) case zero show ?case by (cases "even l") (simp_all split: bool.splits) next case minus show ?case by (cases "even l") (simp_all split: bool.splits) next case (even k) then show ?case by (simp add: rec [of "k * 2"]) next case (odd k) then show ?case by (simp add: rec [of "1 + k * 2"]) qed end instantiation int :: ring_bit_operations begin definition not_int :: "int \ int" where "not_int = complement" global_interpretation and_int: zip_int "(\)" defines and_int = and_int.F by standard declare and_int.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ global_interpretation and_int: semilattice "(AND) :: int \ int \ int" proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard) show "k AND k = k" for k :: int by (simp add: and_int.self) qed lemma zero_int_and_eq [simp]: "0 AND k = 0" for k :: int by simp lemma and_zero_int_eq [simp]: "k AND 0 = 0" for k :: int by simp lemma minus_int_and_eq [simp]: "- 1 AND k = k" for k :: int by simp lemma and_minus_int_eq [simp]: "k AND - 1 = k" for k :: int by simp global_interpretation or_int: zip_int "(\)" defines or_int = or_int.F by standard declare or_int.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ global_interpretation or_int: semilattice "(OR) :: int \ int \ int" proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard) show "k OR k = k" for k :: int by (simp add: or_int.self) qed lemma zero_int_or_eq [simp]: "0 OR k = k" for k :: int by simp lemma and_zero_or_eq [simp]: "k OR 0 = k" for k :: int by simp lemma minus_int_or_eq [simp]: "- 1 OR k = - 1" for k :: int by simp lemma or_minus_int_eq [simp]: "k OR - 1 = - 1" for k :: int by simp global_interpretation xor_int: zip_int "(\)" defines xor_int = xor_int.F by standard declare xor_int.simps [simp] \ \inconsistent declaration handling by \global_interpretation\ in \instantiation\\ lemma zero_int_xor_eq [simp]: "0 XOR k = k" for k :: int by simp lemma and_zero_xor_eq [simp]: "k XOR 0 = k" for k :: int by simp lemma minus_int_xor_eq [simp]: "- 1 XOR k = complement k" for k :: int by simp lemma xor_minus_int_eq [simp]: "k XOR - 1 = complement k" for k :: int by simp lemma not_div_2: "NOT k div 2 = NOT (k div 2)" for k :: int by (simp add: complement_div_2 not_int_def) lemma not_int_simps [simp]: "NOT 0 = (- 1 :: int)" "NOT (- 1) = (0 :: int)" "k \ 0 \ k \ - 1 \ NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int by (auto simp add: not_int_def elim: oddE) lemma not_one_int [simp]: "NOT 1 = (- 2 :: int)" by simp lemma even_not_iff [simp]: "even (NOT k) \ odd k" for k :: int by (simp add: not_int_def) instance proof interpret bit_int: boolean_algebra "(AND)" "(OR)" NOT 0 "- 1 :: int" proof show "k AND (l OR r) = k AND l OR k AND r" for k l r :: int proof (induction k arbitrary: l r rule: int_bit_induct) case zero show ?case by simp next case minus show ?case by simp next case (even k) then show ?case by (simp add: and_int.rec [of "k * 2"] or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of l]) next case (odd k) then show ?case by (simp add: and_int.rec [of "1 + k * 2"] or_int.rec [of "(k AND l div 2) * 2"] or_int.rec [of "1 + (k AND l div 2) * 2"] or_int.rec [of l]) qed show "k OR l AND r = (k OR l) AND (k OR r)" for k l r :: int proof (induction k arbitrary: l r rule: int_bit_induct) case zero then show ?case by simp next case minus then show ?case by simp next case (even k) then show ?case by (simp add: or_int.rec [of "k * 2"] and_int.rec [of "(k OR l div 2) * 2"] and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l]) next case (odd k) then show ?case by (simp add: or_int.rec [of "1 + k * 2"] and_int.rec [of "1 + (k OR l div 2) * 2"] and_int.rec [of l]) qed show "k AND NOT k = 0" for k :: int by (induction k rule: int_bit_induct) (simp_all add: not_int_def complement_half minus_diff_commute [of 1]) show "k OR NOT k = - 1" for k :: int by (induction k rule: int_bit_induct) (simp_all add: not_int_def complement_half minus_diff_commute [of 1]) qed (simp_all add: and_int.assoc or_int.assoc, simp_all add: and_int.commute or_int.commute) show "boolean_algebra (AND) (OR) NOT 0 (- 1 :: int)" by (fact bit_int.boolean_algebra_axioms) show "bit_int.xor = ((XOR) :: int \ _)" proof (rule ext)+ fix k l :: int have "k XOR l = k AND NOT l OR NOT k AND l" proof (induction k arbitrary: l rule: int_bit_induct) case zero show ?case by simp next case minus show ?case by (simp add: not_int_def) next case (even k) then show ?case by (simp add: xor_int.rec [of "k * 2"] and_int.rec [of "k * 2"] or_int.rec [of _ "1 + 2 * NOT k AND l"] not_div_2) (simp add: and_int.rec [of _ l]) next case (odd k) then show ?case by (simp add: xor_int.rec [of "1 + k * 2"] and_int.rec [of "1 + k * 2"] or_int.rec [of _ "2 * NOT k AND l"] not_div_2) (simp add: and_int.rec [of _ l]) qed then show "bit_int.xor k l = k XOR l" by (simp add: bit_int.xor_def) qed qed end lemma one_and_int_eq [simp]: "1 AND k = k mod 2" for k :: int using and_int.rec [of 1] by (simp add: mod2_eq_if) lemma and_one_int_eq [simp]: "k AND 1 = k mod 2" for k :: int using one_and_int_eq [of 1] by (simp add: ac_simps) lemma one_or_int_eq [simp]: "1 OR k = k + of_bool (even k)" for k :: int using or_int.rec [of 1] by (auto elim: oddE) lemma or_one_int_eq [simp]: "k OR 1 = k + of_bool (even k)" for k :: int using one_or_int_eq [of k] by (simp add: ac_simps) lemma one_xor_int_eq [simp]: "1 XOR k = k + of_bool (even k) - of_bool (odd k)" for k :: int using xor_int.rec [of 1] by (auto elim: oddE) lemma xor_one_int_eq [simp]: "k XOR 1 = k + of_bool (even k) - of_bool (odd k)" for k :: int using one_xor_int_eq [of k] by (simp add: ac_simps) lemma take_bit_complement_iff: "Parity.take_bit n (complement k) = Parity.take_bit n (complement l) \ Parity.take_bit n k = Parity.take_bit n l" for k l :: int by (simp add: Parity.take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute) lemma take_bit_not_iff: "Parity.take_bit n (NOT k) = Parity.take_bit n (NOT l) \ Parity.take_bit n k = Parity.take_bit n l" for k l :: int by (simp add: not_int_def take_bit_complement_iff) lemma take_bit_and [simp]: "Parity.take_bit n (k AND l) = Parity.take_bit n k AND Parity.take_bit n l" for k l :: int apply (induction n arbitrary: k l) apply simp apply (subst and_int.rec) apply (subst (2) and_int.rec) apply simp done lemma take_bit_or [simp]: "Parity.take_bit n (k OR l) = Parity.take_bit n k OR Parity.take_bit n l" for k l :: int apply (induction n arbitrary: k l) apply simp apply (subst or_int.rec) apply (subst (2) or_int.rec) apply simp done lemma take_bit_xor [simp]: "Parity.take_bit n (k XOR l) = Parity.take_bit n k XOR Parity.take_bit n l" for k l :: int apply (induction n arbitrary: k l) apply simp apply (subst xor_int.rec) apply (subst (2) xor_int.rec) apply simp done subsubsection \Instance \<^typ>\'a word\\ 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 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,565 +1,652 @@ (* Author: Florian Haftmann, TUM *) section \Proof of concept for algebraically founded bit word types\ theory Word imports Main "HOL-Library.Type_Length" begin subsection \Preliminaries\ 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] transfer_rule_of_nat [transfer_rule] transfer_rule_of_int [transfer_rule] begin 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: 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 +subsubsection \Instance \<^typ>\'a word\\ + +instance word :: (len) semiring_bits +proof + show \of_bool (odd a) + 2 * (a div 2) = a\ + for a :: \'a word\ + apply (cases \even a\; simp, transfer; cases rule: length_cases [where ?'a = 'a]) + apply auto + apply (auto simp add: take_bit_eq_mod) + apply (metis add.commute even_take_bit_eq len_not_eq_0 mod_mod_trivial odd_two_times_div_two_succ take_bit_eq_mod) + done + show \a = b \ (even a \ even b) \ a div 2 = b div 2\ + for a b :: \'a word\ + apply transfer + apply (cases rule: length_cases [where ?'a = 'a]) + apply auto + apply (metis even_take_bit_eq len_not_eq_0) + apply (metis even_take_bit_eq len_not_eq_0) + apply (metis (no_types, hide_lams) diff_add_cancel dvd_div_mult_self even_take_bit_eq mult_2_right take_bit_add take_bit_minus) + apply (metis bit_ident drop_bit_eq_div drop_bit_half even_take_bit_eq even_two_times_div_two mod_div_trivial odd_two_times_div_two_succ take_bit_eq_mod) + done + 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 +qed + + +subsubsection \Instance \<^typ>\'a word\\ + +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 + +end