src/HOL/Divides.thy
changeset 61275 053ec04ea866
parent 61201 94efa2688ff6
child 61433 a4c0de1df3d8
     1.1 --- a/src/HOL/Divides.thy	Sun Sep 27 10:11:14 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sun Sep 27 10:11:15 2015 +0200
     1.3 @@ -567,6 +567,16 @@
     1.4      and mod_mult2_eq: "0 \<le> c \<Longrightarrow> a mod (b * c) = b * (a div b mod c) + a mod b"
     1.5      and div_mult2_eq: "0 \<le> c \<Longrightarrow> a div (b * c) = a div b div c"
     1.6    assumes discrete: "a < b \<longleftrightarrow> a + 1 \<le> b"
     1.7 +  fixes divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
     1.8 +    and divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
     1.9 +  assumes divmod_def: "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
    1.10 +    and divmod_step_def: "divmod_step l qr = (let (q, r) = qr
    1.11 +    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
    1.12 +    else (2 * q, r))"
    1.13 +    -- \<open>These are conceptually definitions but force generated code
    1.14 +    to be monomorphic wrt. particular instances of this class which
    1.15 +    yields a significant speedup.\<close>
    1.16 +
    1.17  begin
    1.18  
    1.19  lemma mult_div_cancel:
    1.20 @@ -650,10 +660,6 @@
    1.21      by (simp_all add: div mod)
    1.22  qed
    1.23  
    1.24 -definition divmod :: "num \<Rightarrow> num \<Rightarrow> 'a \<times> 'a"
    1.25 -where
    1.26 -  "divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
    1.27 -
    1.28  lemma fst_divmod:
    1.29    "fst (divmod m n) = numeral m div numeral n"
    1.30    by (simp add: divmod_def)
    1.31 @@ -662,12 +668,6 @@
    1.32    "snd (divmod m n) = numeral m mod numeral n"
    1.33    by (simp add: divmod_def)
    1.34  
    1.35 -definition divmod_step :: "num \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<times> 'a"
    1.36 -where
    1.37 -  "divmod_step l qr = (let (q, r) = qr
    1.38 -    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
    1.39 -    else (2 * q, r))"
    1.40 -
    1.41  text \<open>
    1.42    This is a formulation of one step (referring to one digit position)
    1.43    in school-method division: compare the dividend at the current
    1.44 @@ -675,7 +675,7 @@
    1.45    and evaluate accordingly.
    1.46  \<close>
    1.47  
    1.48 -lemma divmod_step_eq [code, simp]:
    1.49 +lemma divmod_step_eq [simp]:
    1.50    "divmod_step l (q, r) = (if numeral l \<le> r
    1.51      then (2 * q + 1, r - numeral l) else (2 * q, r))"
    1.52    by (simp add: divmod_step_def)
    1.53 @@ -735,7 +735,7 @@
    1.54  
    1.55  text \<open>The division rewrite proper -- first, trivial results involving @{text 1}\<close>
    1.56  
    1.57 -lemma divmod_trivial [simp, code]:
    1.58 +lemma divmod_trivial [simp]:
    1.59    "divmod Num.One Num.One = (numeral Num.One, 0)"
    1.60    "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
    1.61    "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
    1.62 @@ -745,7 +745,7 @@
    1.63  
    1.64  text \<open>Division by an even number is a right-shift\<close>
    1.65  
    1.66 -lemma divmod_cancel [simp, code]:
    1.67 +lemma divmod_cancel [simp]:
    1.68    "divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
    1.69    "divmod (Num.Bit1 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r + 1))" (is ?Q)
    1.70  proof -
    1.71 @@ -761,7 +761,7 @@
    1.72  
    1.73  text \<open>The really hard work\<close>
    1.74  
    1.75 -lemma divmod_steps [simp, code]:
    1.76 +lemma divmod_steps [simp]:
    1.77    "divmod (num.Bit0 m) (num.Bit1 n) =
    1.78        (if m \<le> n then (0, numeral (num.Bit0 m))
    1.79         else divmod_step (num.Bit1 n)
    1.80 @@ -774,6 +774,8 @@
    1.81                 (num.Bit0 (num.Bit1 n))))"
    1.82    by (simp_all add: divmod_divmod_step)
    1.83  
    1.84 +lemmas divmod_algorithm_code = divmod_step_eq divmod_trivial divmod_cancel divmod_steps  
    1.85 +
    1.86  text \<open>Special case: divisibility\<close>
    1.87  
    1.88  definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
    1.89 @@ -1177,9 +1179,26 @@
    1.90  lemma mod_mult2_eq: "a mod (b * c) = b * (a div b mod c) + a mod (b::nat)"
    1.91  by (auto simp add: mult.commute divmod_nat_rel [THEN divmod_nat_rel_mult2_eq, THEN mod_nat_unique])
    1.92  
    1.93 -instance nat :: semiring_numeral_div
    1.94 -  by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)
    1.95 -
    1.96 +instantiation nat :: semiring_numeral_div
    1.97 +begin
    1.98 +
    1.99 +definition divmod_nat :: "num \<Rightarrow> num \<Rightarrow> nat \<times> nat"
   1.100 +where
   1.101 +  divmod'_nat_def: "divmod_nat m n = (numeral m div numeral n, numeral m mod numeral n)"
   1.102 +
   1.103 +definition divmod_step_nat :: "num \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
   1.104 +where
   1.105 +  "divmod_step_nat l qr = (let (q, r) = qr
   1.106 +    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   1.107 +    else (2 * q, r))"
   1.108 +
   1.109 +instance
   1.110 +  by standard (auto intro: div_positive simp add: divmod'_nat_def divmod_step_nat_def mod_mult2_eq div_mult2_eq)
   1.111 +
   1.112 +end
   1.113 +
   1.114 +declare divmod_algorithm_code [where ?'a = nat, code]
   1.115 +  
   1.116  
   1.117  subsubsection \<open>Further Facts about Quotient and Remainder\<close>
   1.118  
   1.119 @@ -2304,12 +2323,26 @@
   1.120  
   1.121  subsubsection \<open>Computation of Division and Remainder\<close>
   1.122  
   1.123 -instance int :: semiring_numeral_div
   1.124 -  by intro_classes (auto intro: zmod_le_nonneg_dividend
   1.125 -    simp add:
   1.126 -    zmult_div_cancel
   1.127 -    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial
   1.128 -    zmod_zmult2_eq zdiv_zmult2_eq)
   1.129 +instantiation int :: semiring_numeral_div
   1.130 +begin
   1.131 +
   1.132 +definition divmod_int :: "num \<Rightarrow> num \<Rightarrow> int \<times> int"
   1.133 +where
   1.134 +  "divmod_int m n = (numeral m div numeral n, numeral m mod numeral n)"
   1.135 +
   1.136 +definition divmod_step_int :: "num \<Rightarrow> int \<times> int \<Rightarrow> int \<times> int"
   1.137 +where
   1.138 +  "divmod_step_int l qr = (let (q, r) = qr
   1.139 +    in if r \<ge> numeral l then (2 * q + 1, r - numeral l)
   1.140 +    else (2 * q, r))"
   1.141 +
   1.142 +instance
   1.143 +  by standard (auto intro: zmod_le_nonneg_dividend simp add: divmod_int_def divmod_step_int_def
   1.144 +    pos_imp_zdiv_pos_iff div_pos_pos_trivial mod_pos_pos_trivial zmod_zmult2_eq zdiv_zmult2_eq)
   1.145 +
   1.146 +end
   1.147 +
   1.148 +declare divmod_algorithm_code [where ?'a = int, code]
   1.149  
   1.150  context
   1.151  begin