# HG changeset patch # User haftmann # Date 1443341475 -7200 # Node ID 053ec04ea8661aed53f0e7f47605cb2a226ef15c # Parent 0261eec37233e4f9c1259483e23e21eed255b97a monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime diff -r 0261eec37233 -r 053ec04ea866 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sun Sep 27 10:11:14 2015 +0200 +++ b/src/HOL/Code_Numeral.thy Sun Sep 27 10:11:15 2015 +0200 @@ -147,6 +147,25 @@ "int_of_integer (Num.sub k l) = Num.sub k l" by transfer rule +lift_definition integer_of_num :: "num \ integer" + is "numeral :: num \ int" + . + +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 (transfer, simp only: numeral.simps Let_def)+ + +lemma numeral_unfold_integer_of_num: + "numeral = integer_of_num" + by (simp add: integer_of_num_def map_fun_def fun_eq_iff) + +lemma integer_of_num_triv: + "integer_of_num Num.One = 1" + "integer_of_num (Num.Bit0 Num.One) = 2" + by (transfer, simp)+ + instantiation integer :: "{ring_div, equal, linordered_idom}" begin @@ -215,18 +234,43 @@ "of_nat (nat_of_integer k) = max 0 k" by transfer auto -instance integer :: semiring_numeral_div - by intro_classes (transfer, - fact le_add_diff_inverse2 - semiring_numeral_div_class.div_less - semiring_numeral_div_class.mod_less - semiring_numeral_div_class.div_positive - semiring_numeral_div_class.mod_less_eq_dividend - semiring_numeral_div_class.pos_mod_bound - semiring_numeral_div_class.pos_mod_sign - semiring_numeral_div_class.mod_mult2_eq - semiring_numeral_div_class.div_mult2_eq - semiring_numeral_div_class.discrete)+ +instantiation integer :: semiring_numeral_div +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 + semiring_numeral_div_class.div_less + semiring_numeral_div_class.mod_less + semiring_numeral_div_class.div_positive + semiring_numeral_div_class.mod_less_eq_dividend + semiring_numeral_div_class.pos_mod_bound + semiring_numeral_div_class.pos_mod_sign + semiring_numeral_div_class.mod_mult2_eq + semiring_numeral_div_class.div_mult2_eq + semiring_numeral_div_class.discrete)+ + +end + +declare divmod_algorithm_code [where ?'a = integer, + unfolded numeral_unfold_integer_of_num, unfolded integer_of_num_triv, + code] lemma integer_of_nat_0: "integer_of_nat 0 = 0" by transfer simp @@ -440,16 +484,6 @@ "Neg k < Neg l \ l < k" by simp_all -lift_definition integer_of_num :: "num \ integer" - is "numeral :: num \ int" - . - -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 (transfer, simp only: numeral.simps Let_def)+ - lift_definition num_of_integer :: "integer \ num" is "num_of_nat \ nat" . diff -r 0261eec37233 -r 053ec04ea866 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Sun Sep 27 10:11:14 2015 +0200 +++ b/src/HOL/Divides.thy Sun Sep 27 10:11:15 2015 +0200 @@ -567,6 +567,16 @@ and mod_mult2_eq: "0 \ c \ a mod (b * c) = b * (a div b mod c) + a mod b" and div_mult2_eq: "0 \ c \ a div (b * c) = a div b div c" assumes discrete: "a < b \ a + 1 \ b" + fixes divmod :: "num \ num \ 'a \ 'a" + and divmod_step :: "num \ 'a \ 'a \ 'a \ 'a" + assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)" + and divmod_step_def: "divmod_step l qr = (let (q, r) = qr + in if r \ numeral l then (2 * q + 1, r - numeral l) + else (2 * q, r))" + -- \These are conceptually definitions but force generated code + to be monomorphic wrt. particular instances of this class which + yields a significant speedup.\ + begin lemma mult_div_cancel: @@ -650,10 +660,6 @@ by (simp_all add: div mod) qed -definition divmod :: "num \ num \ 'a \ 'a" -where - "divmod m n = (numeral m div numeral n, numeral m mod numeral n)" - lemma fst_divmod: "fst (divmod m n) = numeral m div numeral n" by (simp add: divmod_def) @@ -662,12 +668,6 @@ "snd (divmod m n) = numeral m mod numeral n" by (simp add: divmod_def) -definition divmod_step :: "num \ 'a \ 'a \ 'a \ 'a" -where - "divmod_step l qr = (let (q, r) = qr - in if r \ numeral l then (2 * q + 1, r - numeral l) - else (2 * q, r))" - text \ This is a formulation of one step (referring to one digit position) in school-method division: compare the dividend at the current @@ -675,7 +675,7 @@ and evaluate accordingly. \ -lemma divmod_step_eq [code, simp]: +lemma divmod_step_eq [simp]: "divmod_step l (q, r) = (if numeral l \ r then (2 * q + 1, r - numeral l) else (2 * q, r))" by (simp add: divmod_step_def) @@ -735,7 +735,7 @@ text \The division rewrite proper -- first, trivial results involving @{text 1}\ -lemma divmod_trivial [simp, code]: +lemma divmod_trivial [simp]: "divmod Num.One Num.One = (numeral Num.One, 0)" "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)" "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)" @@ -745,7 +745,7 @@ text \Division by an even number is a right-shift\ -lemma divmod_cancel [simp, code]: +lemma divmod_cancel [simp]: "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \ (q, 2 * r))" (is ?P) "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \ (q, 2 * r + 1))" (is ?Q) proof - @@ -761,7 +761,7 @@ text \The really hard work\ -lemma divmod_steps [simp, code]: +lemma divmod_steps [simp]: "divmod (num.Bit0 m) (num.Bit1 n) = (if m \ n then (0, numeral (num.Bit0 m)) else divmod_step (num.Bit1 n) @@ -774,6 +774,8 @@ (num.Bit0 (num.Bit1 n))))" by (simp_all add: divmod_divmod_step) +lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps + text \Special case: divisibility\ definition divides_aux :: "'a \ 'a \ bool" @@ -1177,9 +1179,26 @@ lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)" by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique]) -instance nat :: semiring_numeral_div - by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq) - +instantiation nat :: semiring_numeral_div +begin + +definition divmod_nat :: "num \ num \ nat \ nat" +where + divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)" + +definition divmod_step_nat :: "num \ nat \ nat \ nat \ nat" +where + "divmod_step_nat l qr = (let (q, r) = qr + in if r \ numeral l then (2 * q + 1, r - numeral l) + else (2 * q, r))" + +instance + by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq) + +end + +declare divmod_algorithm_code [where ?'a = nat, code] + subsubsection \Further Facts about Quotient and Remainder\ @@ -2304,12 +2323,26 @@ subsubsection \Computation of Division and Remainder\ -instance int :: semiring_numeral_div - by intro_classes (auto intro: zmod_le_nonneg_dividend - simp add: - zmult_div_cancel - pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial - zmod_zmult2_eq zdiv_zmult2_eq) +instantiation int :: semiring_numeral_div +begin + +definition divmod_int :: "num \ num \ int \ int" +where + "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)" + +definition divmod_step_int :: "num \ int \ int \ int \ int" +where + "divmod_step_int l qr = (let (q, r) = qr + in if r \ numeral l then (2 * q + 1, r - numeral l) + else (2 * q, r))" + +instance + by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def + pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq) + +end + +declare divmod_algorithm_code [where ?'a = int, code] context begin diff -r 0261eec37233 -r 053ec04ea866 src/HOL/Library/Code_Target_Int.thy --- a/src/HOL/Library/Code_Target_Int.thy Sun Sep 27 10:11:14 2015 +0200 +++ b/src/HOL/Library/Code_Target_Int.thy Sun Sep 27 10:11:15 2015 +0200 @@ -79,6 +79,11 @@ by simp lemma [code]: + "divmod m n = map_prod int_of_integer int_of_integer (divmod m n)" + unfolding prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv + by transfer simp + +lemma [code]: "HOL.equal k l = HOL.equal (of_int k :: integer) (of_int l)" by transfer (simp add: equal) diff -r 0261eec37233 -r 053ec04ea866 src/HOL/Library/Code_Target_Nat.thy --- a/src/HOL/Library/Code_Target_Nat.thy Sun Sep 27 10:11:14 2015 +0200 +++ b/src/HOL/Library/Code_Target_Nat.thy Sun Sep 27 10:11:15 2015 +0200 @@ -85,6 +85,12 @@ by (fact divmod_nat_div_mod) lemma [code]: + "divmod m n = map_prod nat_of_integer nat_of_integer (divmod m n)" + by (simp only: prod_eq_iff divmod_def map_prod_def case_prod_beta fst_conv snd_conv) + (transfer, simp_all only: nat_div_distrib nat_mod_distrib + zero_le_numeral nat_numeral) + +lemma [code]: "HOL.equal m n = HOL.equal (of_nat m :: integer) (of_nat n)" by transfer (simp add: equal) diff -r 0261eec37233 -r 053ec04ea866 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Sun Sep 27 10:11:14 2015 +0200 +++ b/src/HOL/NSA/StarDef.thy Sun Sep 27 10:11:15 2015 +0200 @@ -1009,18 +1009,42 @@ apply(transfer, rule zero_not_eq_two) done -instance star :: (semiring_numeral_div) semiring_numeral_div -apply intro_classes -apply(transfer, fact semiring_numeral_div_class.div_less) -apply(transfer, fact semiring_numeral_div_class.mod_less) -apply(transfer, fact semiring_numeral_div_class.div_positive) -apply(transfer, fact semiring_numeral_div_class.mod_less_eq_dividend) -apply(transfer, fact semiring_numeral_div_class.pos_mod_bound) -apply(transfer, fact semiring_numeral_div_class.pos_mod_sign) -apply(transfer, fact semiring_numeral_div_class.mod_mult2_eq) -apply(transfer, fact semiring_numeral_div_class.div_mult2_eq) -apply(transfer, fact discrete) -done +instantiation star :: (semiring_numeral_div) semiring_numeral_div +begin + +definition divmod_star :: "num \ num \ 'a star \ 'a star" +where + divmod_star_def: "divmod_star m n = (numeral m div numeral n, numeral m mod numeral n)" + +definition divmod_step_star :: "num \ 'a star \ 'a star \ 'a star \ 'a star" +where + "divmod_step_star 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 :: 'a star, numeral m mod numeral n)" + for m n by (fact divmod_star_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 :: "'a star \ 'a star" + by (fact divmod_step_star_def) +qed (transfer, + fact + semiring_numeral_div_class.div_less + semiring_numeral_div_class.mod_less + semiring_numeral_div_class.div_positive + semiring_numeral_div_class.mod_less_eq_dividend + semiring_numeral_div_class.pos_mod_bound + semiring_numeral_div_class.pos_mod_sign + semiring_numeral_div_class.mod_mult2_eq + semiring_numeral_div_class.div_mult2_eq + semiring_numeral_div_class.discrete)+ + +end + +declare divmod_algorithm_code [where ?'a = "'a::semiring_numeral_div star", code] + subsection {* Finite class *}