tightended specification of class semiring_div
authorhaftmann
Thu Apr 16 10:11:34 2009 +0200 (2009-04-16)
changeset 3093011010e5f18f0
parent 30929 d9343c0aac11
child 30931 86ca651da03e
tightended specification of class semiring_div
NEWS
src/HOL/Divides.thy
src/HOL/IntDiv.thy
src/HOL/Library/Polynomial.thy
     1.1 --- a/NEWS	Wed Apr 15 15:52:37 2009 +0200
     1.2 +++ b/NEWS	Thu Apr 16 10:11:34 2009 +0200
     1.3 @@ -1,6 +1,14 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Class semiring_div now requires no_zero_divisors and proof of div_mult_mult1;
    1.10 +theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
    1.11 +div_mult_mult2 have been generalized to class semiring_div, subsuming former
    1.12 +theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
    1.13 +div_mult_mult1 is now [simp] by default.  INCOMPATIBILITY.
    1.14 +
    1.15  New in Isabelle2009 (April 2009)
    1.16  --------------------------------
    1.17  
     2.1 --- a/src/HOL/Divides.thy	Wed Apr 15 15:52:37 2009 +0200
     2.2 +++ b/src/HOL/Divides.thy	Thu Apr 16 10:11:34 2009 +0200
     2.3 @@ -19,11 +19,12 @@
     2.4  
     2.5  subsection {* Abstract division in commutative semirings. *}
     2.6  
     2.7 -class semiring_div = comm_semiring_1_cancel + div +
     2.8 +class semiring_div = comm_semiring_1_cancel + no_zero_divisors + div +
     2.9    assumes mod_div_equality: "a div b * b + a mod b = a"
    2.10      and div_by_0 [simp]: "a div 0 = 0"
    2.11      and div_0 [simp]: "0 div a = 0"
    2.12      and div_mult_self1 [simp]: "b \<noteq> 0 \<Longrightarrow> (a + c * b) div b = c + a div b"
    2.13 +    and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
    2.14  begin
    2.15  
    2.16  text {* @{const div} and @{const mod} *}
    2.17 @@ -296,21 +297,41 @@
    2.18    finally show ?thesis .
    2.19  qed
    2.20  
    2.21 -end
    2.22 -
    2.23 -lemma div_mult_div_if_dvd: "(y::'a::{semiring_div,no_zero_divisors}) dvd x \<Longrightarrow> 
    2.24 -  z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
    2.25 -unfolding dvd_def
    2.26 -  apply clarify
    2.27 -  apply (case_tac "y = 0")
    2.28 -  apply simp
    2.29 -  apply (case_tac "z = 0")
    2.30 -  apply simp
    2.31 -  apply (simp add: algebra_simps)
    2.32 +lemma div_mult_div_if_dvd:
    2.33 +  "y dvd x \<Longrightarrow> z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
    2.34 +  apply (cases "y = 0", simp)
    2.35 +  apply (cases "z = 0", simp)
    2.36 +  apply (auto elim!: dvdE simp add: algebra_simps)
    2.37    apply (subst mult_assoc [symmetric])
    2.38    apply (simp add: no_zero_divisors)
    2.39 -done
    2.40 +  done
    2.41 +
    2.42 +lemma div_mult_mult2 [simp]:
    2.43 +  "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
    2.44 +  by (drule div_mult_mult1) (simp add: mult_commute)
    2.45 +
    2.46 +lemma div_mult_mult1_if [simp]:
    2.47 +  "(c * a) div (c * b) = (if c = 0 then 0 else a div b)"
    2.48 +  by simp_all
    2.49  
    2.50 +lemma mod_mult_mult1:
    2.51 +  "(c * a) mod (c * b) = c * (a mod b)"
    2.52 +proof (cases "c = 0")
    2.53 +  case True then show ?thesis by simp
    2.54 +next
    2.55 +  case False
    2.56 +  from mod_div_equality
    2.57 +  have "((c * a) div (c * b)) * (c * b) + (c * a) mod (c * b) = c * a" .
    2.58 +  with False have "c * ((a div b) * b + a mod b) + (c * a) mod (c * b)
    2.59 +    = c * a + c * (a mod b)" by (simp add: algebra_simps)
    2.60 +  with mod_div_equality show ?thesis by simp 
    2.61 +qed
    2.62 +  
    2.63 +lemma mod_mult_mult2:
    2.64 +  "(a * c) mod (b * c) = (a mod b) * c"
    2.65 +  using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
    2.66 +
    2.67 +end
    2.68  
    2.69  lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow>
    2.70      (x div y)^n = x^n div y^n"
    2.71 @@ -566,18 +587,40 @@
    2.72    shows "m mod n = (m - n) mod n"
    2.73    using assms divmod_step divmod_div_mod by (cases "n = 0") simp_all
    2.74  
    2.75 -instance proof
    2.76 -  fix m n :: nat show "m div n * n + m mod n = m"
    2.77 -    using divmod_rel [of m n] by (simp add: divmod_rel_def)
    2.78 -next
    2.79 -  fix n :: nat show "n div 0 = 0"
    2.80 -    using divmod_zero divmod_div_mod [of n 0] by simp
    2.81 -next
    2.82 -  fix n :: nat show "0 div n = 0"
    2.83 -    using divmod_rel [of 0 n] by (cases n) (simp_all add: divmod_rel_def)
    2.84 -next
    2.85 -  fix m n q :: nat assume "n \<noteq> 0" then show "(q + m * n) div n = m + q div n"
    2.86 -    by (induct m) (simp_all add: le_div_geq)
    2.87 +instance proof -
    2.88 +  have [simp]: "\<And>n::nat. n div 0 = 0"
    2.89 +    by (simp add: div_nat_def divmod_zero)
    2.90 +  have [simp]: "\<And>n::nat. 0 div n = 0"
    2.91 +  proof -
    2.92 +    fix n :: nat
    2.93 +    show "0 div n = 0"
    2.94 +      by (cases "n = 0") simp_all
    2.95 +  qed
    2.96 +  show "OFCLASS(nat, semiring_div_class)" proof
    2.97 +    fix m n :: nat
    2.98 +    show "m div n * n + m mod n = m"
    2.99 +      using divmod_rel [of m n] by (simp add: divmod_rel_def)
   2.100 +  next
   2.101 +    fix m n q :: nat
   2.102 +    assume "n \<noteq> 0"
   2.103 +    then show "(q + m * n) div n = m + q div n"
   2.104 +      by (induct m) (simp_all add: le_div_geq)
   2.105 +  next
   2.106 +    fix m n q :: nat
   2.107 +    assume "m \<noteq> 0"
   2.108 +    then show "(m * n) div (m * q) = n div q"
   2.109 +    proof (cases "n \<noteq> 0 \<and> q \<noteq> 0")
   2.110 +      case False then show ?thesis by auto
   2.111 +    next
   2.112 +      case True with `m \<noteq> 0`
   2.113 +        have "m > 0" and "n > 0" and "q > 0" by auto
   2.114 +      then have "\<And>a b. divmod_rel n q (a, b) \<Longrightarrow> divmod_rel (m * n) (m * q) (a, m * b)"
   2.115 +        by (auto simp add: divmod_rel_def) (simp_all add: algebra_simps)
   2.116 +      moreover from divmod_rel have "divmod_rel n q (n div q, n mod q)" .
   2.117 +      ultimately have "divmod_rel (m * n) (m * q) (n div q, m * (n mod q))" .
   2.118 +      then show ?thesis by (simp add: div_eq)
   2.119 +    qed
   2.120 +  qed simp_all
   2.121  qed
   2.122  
   2.123  end
   2.124 @@ -744,23 +787,6 @@
   2.125    done
   2.126  
   2.127  
   2.128 -subsubsection{*Cancellation of Common Factors in Division*}
   2.129 -
   2.130 -lemma div_mult_mult_lemma:
   2.131 -    "[| (0::nat) < b;  0 < c |] ==> (c*a) div (c*b) = a div b"
   2.132 -by (auto simp add: div_mult2_eq)
   2.133 -
   2.134 -lemma div_mult_mult1 [simp]: "(0::nat) < c ==> (c*a) div (c*b) = a div b"
   2.135 -  apply (cases "b = 0")
   2.136 -  apply (auto simp add: linorder_neq_iff [of b] div_mult_mult_lemma)
   2.137 -  done
   2.138 -
   2.139 -lemma div_mult_mult2 [simp]: "(0::nat) < c ==> (a*c) div (b*c) = a div b"
   2.140 -  apply (drule div_mult_mult1)
   2.141 -  apply (auto simp add: mult_commute)
   2.142 -  done
   2.143 -
   2.144 -
   2.145  subsubsection{*Further Facts about Quotient and Remainder*}
   2.146  
   2.147  lemma div_1 [simp]: "m div Suc 0 = m"
     3.1 --- a/src/HOL/IntDiv.thy	Wed Apr 15 15:52:37 2009 +0200
     3.2 +++ b/src/HOL/IntDiv.thy	Thu Apr 16 10:11:34 2009 +0200
     3.3 @@ -711,6 +711,26 @@
     3.4    show "(a + c * b) div b = c + a div b"
     3.5      unfolding zdiv_zadd1_eq [of a "c * b"] using not0 
     3.6        by (simp add: zmod_zmult1_eq zmod_zdiv_trivial zdiv_zmult1_eq)
     3.7 +next
     3.8 +  fix a b c :: int
     3.9 +  assume "a \<noteq> 0"
    3.10 +  then show "(a * b) div (a * c) = b div c"
    3.11 +  proof (cases "b \<noteq> 0 \<and> c \<noteq> 0")
    3.12 +    case False then show ?thesis by auto
    3.13 +  next
    3.14 +    case True then have "b \<noteq> 0" and "c \<noteq> 0" by auto
    3.15 +    with `a \<noteq> 0`
    3.16 +    have "\<And>q r. divmod_rel b c (q, r) \<Longrightarrow> divmod_rel (a * b) (a * c) (q, a * r)"
    3.17 +      apply (auto simp add: divmod_rel_def) 
    3.18 +      apply (auto simp add: algebra_simps)
    3.19 +      apply (auto simp add: zero_less_mult_iff zero_le_mult_iff mult_le_0_iff)
    3.20 +      apply (simp_all add: mult_less_cancel_left_disj mult_commute [of _ a])
    3.21 +      done
    3.22 +    moreover with `c \<noteq> 0` divmod_rel_div_mod have "divmod_rel b c (b div c, b mod c)" by auto
    3.23 +    ultimately have "divmod_rel (a * b) (a * c) (b div c, a * (b mod c))" .
    3.24 +    moreover from  `a \<noteq> 0` `c \<noteq> 0` have "a * c \<noteq> 0" by simp
    3.25 +    ultimately show ?thesis by (rule divmod_rel_div)
    3.26 +  qed
    3.27  qed auto
    3.28  
    3.29  lemma posDivAlg_div_mod:
    3.30 @@ -808,52 +828,6 @@
    3.31  done
    3.32  
    3.33  
    3.34 -subsection{*Cancellation of Common Factors in div*}
    3.35 -
    3.36 -lemma zdiv_zmult_zmult1_aux1:
    3.37 -     "[| (0::int) < b;  c \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
    3.38 -by (subst zdiv_zmult2_eq, auto)
    3.39 -
    3.40 -lemma zdiv_zmult_zmult1_aux2:
    3.41 -     "[| b < (0::int);  c \<noteq> 0 |] ==> (c*a) div (c*b) = a div b"
    3.42 -apply (subgoal_tac " (c * (-a)) div (c * (-b)) = (-a) div (-b) ")
    3.43 -apply (rule_tac [2] zdiv_zmult_zmult1_aux1, auto)
    3.44 -done
    3.45 -
    3.46 -lemma zdiv_zmult_zmult1: "c \<noteq> (0::int) ==> (c*a) div (c*b) = a div b"
    3.47 -apply (case_tac "b = 0", simp)
    3.48 -apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
    3.49 -done
    3.50 -
    3.51 -lemma zdiv_zmult_zmult1_if[simp]:
    3.52 -  "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)"
    3.53 -by (simp add:zdiv_zmult_zmult1)
    3.54 -
    3.55 -
    3.56 -subsection{*Distribution of Factors over mod*}
    3.57 -
    3.58 -lemma zmod_zmult_zmult1_aux1:
    3.59 -     "[| (0::int) < b;  c \<noteq> 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
    3.60 -by (subst zmod_zmult2_eq, auto)
    3.61 -
    3.62 -lemma zmod_zmult_zmult1_aux2:
    3.63 -     "[| b < (0::int);  c \<noteq> 0 |] ==> (c*a) mod (c*b) = c * (a mod b)"
    3.64 -apply (subgoal_tac " (c * (-a)) mod (c * (-b)) = c * ((-a) mod (-b))")
    3.65 -apply (rule_tac [2] zmod_zmult_zmult1_aux1, auto)
    3.66 -done
    3.67 -
    3.68 -lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
    3.69 -apply (case_tac "b = 0", simp)
    3.70 -apply (case_tac "c = 0", simp)
    3.71 -apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
    3.72 -done
    3.73 -
    3.74 -lemma zmod_zmult_zmult2: "(a*c) mod (b*c) = (a mod b) * (c::int)"
    3.75 -apply (cut_tac c = c in zmod_zmult_zmult1)
    3.76 -apply (auto simp add: mult_commute)
    3.77 -done
    3.78 -
    3.79 -
    3.80  subsection {*Splitting Rules for div and mod*}
    3.81  
    3.82  text{*The proofs of the two lemmas below are essentially identical*}
    3.83 @@ -937,7 +911,7 @@
    3.84                    right_distrib) 
    3.85    thus ?thesis
    3.86      by (subst zdiv_zadd1_eq,
    3.87 -        simp add: zdiv_zmult_zmult1 zmod_zmult_zmult1 one_less_a2
    3.88 +        simp add: mod_mult_mult1 one_less_a2
    3.89                    div_pos_pos_trivial)
    3.90  qed
    3.91  
    3.92 @@ -961,7 +935,7 @@
    3.93             then number_of v div (number_of w)     
    3.94             else (number_of v + (1::int)) div (number_of w))"
    3.95  apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) 
    3.96 -apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
    3.97 +apply (simp add: pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
    3.98  done
    3.99  
   3.100  
   3.101 @@ -977,7 +951,7 @@
   3.102  apply (auto simp add: add_commute [of 1] mult_commute add1_zle_eq 
   3.103                        pos_mod_bound)
   3.104  apply (subst mod_add_eq)
   3.105 -apply (simp add: zmod_zmult_zmult2 mod_pos_pos_trivial)
   3.106 +apply (simp add: mod_mult_mult2 mod_pos_pos_trivial)
   3.107  apply (rule mod_pos_pos_trivial)
   3.108  apply (auto simp add: mod_pos_pos_trivial ring_distribs)
   3.109  apply (subgoal_tac "0 \<le> b mod a", arith, simp)
   3.110 @@ -998,7 +972,7 @@
   3.111       "number_of (Int.Bit0 v) mod number_of (Int.Bit0 w) =  
   3.112        (2::int) * (number_of v mod number_of w)"
   3.113  apply (simp only: number_of_eq numeral_simps) 
   3.114 -apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
   3.115 +apply (simp add: mod_mult_mult1 pos_zmod_mult_2 
   3.116                   neg_zmod_mult_2 add_ac)
   3.117  done
   3.118  
   3.119 @@ -1008,7 +982,7 @@
   3.120                  then 2 * (number_of v mod number_of w) + 1     
   3.121                  else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
   3.122  apply (simp only: number_of_eq numeral_simps) 
   3.123 -apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
   3.124 +apply (simp add: mod_mult_mult1 pos_zmod_mult_2 
   3.125                   neg_zmod_mult_2 add_ac)
   3.126  done
   3.127  
   3.128 @@ -1090,9 +1064,7 @@
   3.129  done
   3.130  
   3.131  lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
   3.132 -  apply (simp add: dvd_def)
   3.133 -  apply (auto simp add: zmod_zmult_zmult1)
   3.134 -  done
   3.135 +  by (auto elim!: dvdE simp add: mod_mult_mult1)
   3.136  
   3.137  lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
   3.138    apply (subgoal_tac "k dvd n * (m div n) + m mod n")
   3.139 @@ -1247,9 +1219,9 @@
   3.140  lemmas zmod_simps =
   3.141    mod_add_left_eq  [symmetric]
   3.142    mod_add_right_eq [symmetric]
   3.143 -  IntDiv.zmod_zmult1_eq     [symmetric]
   3.144 -  mod_mult_left_eq          [symmetric]
   3.145 -  IntDiv.zpower_zmod
   3.146 +  zmod_zmult1_eq   [symmetric]
   3.147 +  mod_mult_left_eq [symmetric]
   3.148 +  zpower_zmod
   3.149    zminus_zmod zdiff_zmod_left zdiff_zmod_right
   3.150  
   3.151  text {* Distributive laws for function @{text nat}. *}
     4.1 --- a/src/HOL/Library/Polynomial.thy	Wed Apr 15 15:52:37 2009 +0200
     4.2 +++ b/src/HOL/Library/Polynomial.thy	Thu Apr 16 10:11:34 2009 +0200
     4.3 @@ -987,6 +987,30 @@
     4.4      by (simp add: pdivmod_rel_def left_distrib)
     4.5    thus "(x + z * y) div y = z + x div y"
     4.6      by (rule div_poly_eq)
     4.7 +next
     4.8 +  fix x y z :: "'a poly"
     4.9 +  assume "x \<noteq> 0"
    4.10 +  show "(x * y) div (x * z) = y div z"
    4.11 +  proof (cases "y \<noteq> 0 \<and> z \<noteq> 0")
    4.12 +    have "\<And>x::'a poly. pdivmod_rel x 0 0 x"
    4.13 +      by (rule pdivmod_rel_by_0)
    4.14 +    then have [simp]: "\<And>x::'a poly. x div 0 = 0"
    4.15 +      by (rule div_poly_eq)
    4.16 +    have "\<And>x::'a poly. pdivmod_rel 0 x 0 0"
    4.17 +      by (rule pdivmod_rel_0)
    4.18 +    then have [simp]: "\<And>x::'a poly. 0 div x = 0"
    4.19 +      by (rule div_poly_eq)
    4.20 +    case False then show ?thesis by auto
    4.21 +  next
    4.22 +    case True then have "y \<noteq> 0" and "z \<noteq> 0" by auto
    4.23 +    with `x \<noteq> 0`
    4.24 +    have "\<And>q r. pdivmod_rel y z q r \<Longrightarrow> pdivmod_rel (x * y) (x * z) q (x * r)"
    4.25 +      by (auto simp add: pdivmod_rel_def algebra_simps)
    4.26 +        (rule classical, simp add: degree_mult_eq)
    4.27 +    moreover from pdivmod_rel have "pdivmod_rel y z (y div z) (y mod z)" .
    4.28 +    ultimately have "pdivmod_rel (x * y) (x * z) (y div z) (x * (y mod z))" .
    4.29 +    then show ?thesis by (simp add: div_poly_eq)
    4.30 +  qed
    4.31  qed
    4.32  
    4.33  end