implicit partial divison operation in integral domains
authorhaftmann
Mon Jun 01 18:59:22 2015 +0200 (2015-06-01)
changeset 60353838025c6e278
parent 60352 d46de31a50c4
child 60356 2e1c1968b38e
implicit partial divison operation in integral domains
src/HOL/Divides.thy
src/HOL/Fields.thy
src/HOL/Groups_Big.thy
src/HOL/NSA/StarDef.thy
src/HOL/Nat.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Divides.thy	Mon Jun 01 18:59:21 2015 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Jun 01 18:59:22 2015 +0200
     1.3 @@ -31,7 +31,13 @@
     1.4      and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
     1.5  begin
     1.6  
     1.7 -subclass semiring_no_zero_divisors ..
     1.8 +subclass semidom_divide
     1.9 +proof
    1.10 +  fix b a
    1.11 +  assume "b \<noteq> 0"
    1.12 +  then show "a * b div b = a"
    1.13 +    using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
    1.14 +qed simp
    1.15  
    1.16  lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>
    1.17    "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
    1.18 @@ -107,11 +113,13 @@
    1.19    "(b * c + a) mod b = a mod b"
    1.20    by (simp add: add.commute)
    1.21  
    1.22 -lemma div_mult_self1_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
    1.23 -  using div_mult_self2 [of b 0 a] by simp
    1.24 -
    1.25 -lemma div_mult_self2_is_id [simp]: "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    1.26 -  using div_mult_self1 [of b 0 a] by simp
    1.27 +lemma div_mult_self1_is_id:
    1.28 +  "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
    1.29 +  by (fact nonzero_mult_divide_cancel_left)
    1.30 +
    1.31 +lemma div_mult_self2_is_id:
    1.32 +  "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
    1.33 +  by (fact nonzero_mult_divide_cancel_right)
    1.34  
    1.35  lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
    1.36    using mod_mult_self2 [of 0 b a] by simp
    1.37 @@ -439,21 +447,21 @@
    1.38  next
    1.39    assume "b div a = c"
    1.40    then have "b div a * a = c * a" by simp
    1.41 -  moreover from `a dvd b` have "b div a * a = b" by (simp add: dvd_div_mult_self)
    1.42 +  moreover from `a dvd b` have "b div a * a = b" by simp
    1.43    ultimately show "b = c * a" by simp
    1.44  qed
    1.45     
    1.46  lemma dvd_div_div_eq_mult:
    1.47    assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
    1.48    shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
    1.49 -  using assms by (auto simp add: mult.commute [of _ a] dvd_div_mult_self dvd_div_eq_mult div_mult_swap intro: sym)
    1.50 +  using assms by (auto simp add: mult.commute [of _ a] dvd_div_eq_mult div_mult_swap intro: sym)
    1.51  
    1.52  end
    1.53  
    1.54  class ring_div = comm_ring_1 + semiring_div
    1.55  begin
    1.56  
    1.57 -subclass idom ..
    1.58 +subclass idom_divide ..
    1.59  
    1.60  text {* Negation respects modular equivalence. *}
    1.61  
     2.1 --- a/src/HOL/Fields.thy	Mon Jun 01 18:59:21 2015 +0200
     2.2 +++ b/src/HOL/Fields.thy	Mon Jun 01 18:59:22 2015 +0200
     2.3 @@ -221,7 +221,7 @@
     2.4    "z \<noteq> 0 \<Longrightarrow> - (x / z) - y = (- x - y * z) / z"
     2.5    by (simp add: divide_diff_eq_iff[symmetric])
     2.6  
     2.7 -lemma divide_zero [simp]:
     2.8 +lemma division_ring_divide_zero [simp]:
     2.9    "a / 0 = 0"
    2.10    by (simp add: divide_inverse)
    2.11  
    2.12 @@ -300,18 +300,31 @@
    2.13      by (fact field_inverse_zero) 
    2.14  qed
    2.15  
    2.16 -subclass idom ..
    2.17 +subclass idom_divide
    2.18 +proof
    2.19 +  fix b a
    2.20 +  assume "b \<noteq> 0"
    2.21 +  then show "a * b / b = a"
    2.22 +    by (simp add: divide_inverse ac_simps)
    2.23 +next
    2.24 +  fix a
    2.25 +  show "a / 0 = 0"
    2.26 +    by (simp add: divide_inverse)
    2.27 +qed
    2.28  
    2.29  text{*There is no slick version using division by zero.*}
    2.30  lemma inverse_add:
    2.31 -  "[| a \<noteq> 0;  b \<noteq> 0 |]
    2.32 -   ==> inverse a + inverse b = (a + b) * inverse a * inverse b"
    2.33 -by (simp add: division_ring_inverse_add ac_simps)
    2.34 +  "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b"
    2.35 +  by (simp add: division_ring_inverse_add ac_simps)
    2.36  
    2.37  lemma nonzero_mult_divide_mult_cancel_left [simp]:
    2.38 -assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" shows "(c*a)/(c*b) = a/b"
    2.39 -proof -
    2.40 -  have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
    2.41 +  assumes [simp]: "c \<noteq> 0"
    2.42 +  shows "(c * a) / (c * b) = a / b"
    2.43 +proof (cases "b = 0")
    2.44 +  case True then show ?thesis by simp
    2.45 +next
    2.46 +  case False
    2.47 +  then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
    2.48      by (simp add: divide_inverse nonzero_inverse_mult_distrib)
    2.49    also have "... =  a * inverse b * (inverse c * c)"
    2.50      by (simp only: ac_simps)
    2.51 @@ -320,8 +333,8 @@
    2.52  qed
    2.53  
    2.54  lemma nonzero_mult_divide_mult_cancel_right [simp]:
    2.55 -  "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (b * c) = a / b"
    2.56 -by (simp add: mult.commute [of _ c])
    2.57 +  "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
    2.58 +  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
    2.59  
    2.60  lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c"
    2.61    by (simp add: divide_inverse ac_simps)
    2.62 @@ -340,33 +353,24 @@
    2.63  
    2.64  text{*Special Cancellation Simprules for Division*}
    2.65  
    2.66 -lemma nonzero_mult_divide_cancel_right [simp]:
    2.67 -  "b \<noteq> 0 \<Longrightarrow> a * b / b = a"
    2.68 -  using nonzero_mult_divide_mult_cancel_right [of 1 b a] by simp
    2.69 -
    2.70 -lemma nonzero_mult_divide_cancel_left [simp]:
    2.71 -  "a \<noteq> 0 \<Longrightarrow> a * b / a = b"
    2.72 -using nonzero_mult_divide_mult_cancel_left [of 1 a b] by simp
    2.73 -
    2.74  lemma nonzero_divide_mult_cancel_right [simp]:
    2.75 -  "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> b / (a * b) = 1 / a"
    2.76 -using nonzero_mult_divide_mult_cancel_right [of a b 1] by simp
    2.77 +  "b \<noteq> 0 \<Longrightarrow> b / (a * b) = 1 / a"
    2.78 +  using nonzero_mult_divide_mult_cancel_right [of b 1 a] by simp
    2.79  
    2.80  lemma nonzero_divide_mult_cancel_left [simp]:
    2.81 -  "\<lbrakk>a \<noteq> 0; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / (a * b) = 1 / b"
    2.82 -using nonzero_mult_divide_mult_cancel_left [of b a 1] by simp
    2.83 +  "a \<noteq> 0 \<Longrightarrow> a / (a * b) = 1 / b"
    2.84 +  using nonzero_mult_divide_mult_cancel_left [of a 1 b] by simp
    2.85  
    2.86  lemma nonzero_mult_divide_mult_cancel_left2 [simp]:
    2.87 -  "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (c * a) / (b * c) = a / b"
    2.88 -using nonzero_mult_divide_mult_cancel_left [of b c a] by (simp add: ac_simps)
    2.89 +  "c \<noteq> 0 \<Longrightarrow> (c * a) / (b * c) = a / b"
    2.90 +  using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps)
    2.91  
    2.92  lemma nonzero_mult_divide_mult_cancel_right2 [simp]:
    2.93 -  "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
    2.94 -using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
    2.95 +  "c \<noteq> 0 \<Longrightarrow> (a * c) / (c * b) = a / b"
    2.96 +  using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
    2.97  
    2.98  lemma diff_frac_eq:
    2.99    "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
   2.100 -  thm field_simps
   2.101    by (simp add: field_simps)
   2.102  
   2.103  lemma frac_eq_eq:
   2.104 @@ -427,7 +431,7 @@
   2.105  
   2.106  lemma mult_divide_mult_cancel_left_if [simp]:
   2.107    shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)"
   2.108 -  by (simp add: mult_divide_mult_cancel_left)
   2.109 +  by simp
   2.110  
   2.111  
   2.112  text {* Division and Unary Minus *}
     3.1 --- a/src/HOL/Groups_Big.thy	Mon Jun 01 18:59:21 2015 +0200
     3.2 +++ b/src/HOL/Groups_Big.thy	Mon Jun 01 18:59:22 2015 +0200
     3.3 @@ -1153,10 +1153,29 @@
     3.4    shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
     3.5    using assms by (induct A) (auto simp: no_zero_divisors)
     3.6  
     3.7 -lemma (in field) setprod_diff1:
     3.8 -  "finite A \<Longrightarrow> f a \<noteq> 0 \<Longrightarrow>
     3.9 -    (setprod f (A - {a})) = (if a \<in> A then setprod f A / f a else setprod f A)"
    3.10 -  by (induct A rule: finite_induct) (auto simp add: insert_Diff_if)
    3.11 +lemma (in semidom_divide) setprod_diff1:
    3.12 +  assumes "finite A" and "f a \<noteq> 0"
    3.13 +  shows "setprod f (A - {a}) = (if a \<in> A then divide (setprod f A) (f a) else setprod f A)"
    3.14 +proof (cases "a \<notin> A")
    3.15 +  case True then show ?thesis by simp
    3.16 +next
    3.17 +  case False with assms show ?thesis
    3.18 +  proof (induct A rule: finite_induct)
    3.19 +    case empty then show ?case by simp
    3.20 +  next
    3.21 +    case (insert b B)
    3.22 +    then show ?case
    3.23 +    proof (cases "a = b")
    3.24 +      case True with insert show ?thesis by simp
    3.25 +    next
    3.26 +      case False with insert have "a \<in> B" by simp
    3.27 +      def C \<equiv> "B - {a}"
    3.28 +      with `finite B` `a \<in> B`
    3.29 +        have *: "B = insert a C" "finite C" "a \<notin> C" by auto
    3.30 +      with insert show ?thesis by (auto simp add: insert_commute ac_simps)
    3.31 +    qed
    3.32 +  qed
    3.33 +qed
    3.34  
    3.35  lemma (in field) setprod_inversef: 
    3.36    "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = inverse (setprod f A)"
     4.1 --- a/src/HOL/NSA/StarDef.thy	Mon Jun 01 18:59:21 2015 +0200
     4.2 +++ b/src/HOL/NSA/StarDef.thy	Mon Jun 01 18:59:22 2015 +0200
     4.3 @@ -853,6 +853,13 @@
     4.4  instance star :: (ring_1) ring_1 ..
     4.5  instance star :: (comm_ring_1) comm_ring_1 ..
     4.6  instance star :: (semidom) semidom ..
     4.7 +instance star :: (semidom_divide) semidom_divide
     4.8 +proof
     4.9 +  show "\<And>b a :: 'a star. b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
    4.10 +    by transfer simp
    4.11 +  show "\<And>a :: 'a star. divide a 0 = 0"
    4.12 +    by transfer simp
    4.13 +qed
    4.14  instance star :: (semiring_div) semiring_div
    4.15  apply intro_classes
    4.16  apply(transfer, rule mod_div_equality)
    4.17 @@ -865,6 +872,7 @@
    4.18  instance star :: (ring_no_zero_divisors) ring_no_zero_divisors ..
    4.19  instance star :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors ..
    4.20  instance star :: (idom) idom .. 
    4.21 +instance star :: (idom_divide) idom_divide ..
    4.22  
    4.23  instance star :: (division_ring) division_ring
    4.24  apply (intro_classes)
     5.1 --- a/src/HOL/Nat.thy	Mon Jun 01 18:59:21 2015 +0200
     5.2 +++ b/src/HOL/Nat.thy	Mon Jun 01 18:59:22 2015 +0200
     5.3 @@ -1484,6 +1484,14 @@
     5.4  lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
     5.5    by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
     5.6  
     5.7 +lemma of_nat_neq_0 [simp]:
     5.8 +  "of_nat (Suc n) \<noteq> 0"
     5.9 +  unfolding of_nat_eq_0_iff by simp
    5.10 +
    5.11 +lemma of_nat_0_neq [simp]:
    5.12 +  "0 \<noteq> of_nat (Suc n)"
    5.13 +  unfolding of_nat_0_eq_iff by simp  
    5.14 +  
    5.15  end
    5.16  
    5.17  context linordered_semidom
     6.1 --- a/src/HOL/Rings.thy	Mon Jun 01 18:59:21 2015 +0200
     6.2 +++ b/src/HOL/Rings.thy	Mon Jun 01 18:59:22 2015 +0200
     6.3 @@ -415,33 +415,6 @@
     6.4  
     6.5  end
     6.6  
     6.7 -class divide =
     6.8 -  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     6.9 -
    6.10 -setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    6.11 -
    6.12 -context semiring
    6.13 -begin
    6.14 -
    6.15 -lemma [field_simps]:
    6.16 -  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
    6.17 -    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
    6.18 -  by (rule distrib_left distrib_right)+
    6.19 -
    6.20 -end
    6.21 -
    6.22 -context ring
    6.23 -begin
    6.24 -
    6.25 -lemma [field_simps]:
    6.26 -  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
    6.27 -    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
    6.28 -  by (rule left_diff_distrib right_diff_distrib)+
    6.29 -
    6.30 -end
    6.31 -
    6.32 -setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    6.33 -  
    6.34  class semiring_no_zero_divisors = semiring_0 +
    6.35    assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    6.36  begin
    6.37 @@ -585,6 +558,46 @@
    6.38    \end{itemize}
    6.39  *}
    6.40  
    6.41 +class divide =
    6.42 +  fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.43 +
    6.44 +setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    6.45 +
    6.46 +context semiring
    6.47 +begin
    6.48 +
    6.49 +lemma [field_simps]:
    6.50 +  shows distrib_left_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
    6.51 +    and distrib_right_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
    6.52 +  by (rule distrib_left distrib_right)+
    6.53 +
    6.54 +end
    6.55 +
    6.56 +context ring
    6.57 +begin
    6.58 +
    6.59 +lemma [field_simps]:
    6.60 +  shows left_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
    6.61 +    and right_diff_distrib_NO_MATCH: "NO_MATCH (divide x y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
    6.62 +  by (rule left_diff_distrib right_diff_distrib)+
    6.63 +
    6.64 +end
    6.65 +
    6.66 +setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::divide \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
    6.67 +
    6.68 +class semidom_divide = semidom + divide +
    6.69 +  assumes nonzero_mult_divide_cancel_right [simp]: "b \<noteq> 0 \<Longrightarrow> divide (a * b) b = a"
    6.70 +  assumes divide_zero [simp]: "divide a 0 = 0"
    6.71 +begin
    6.72 +
    6.73 +lemma nonzero_mult_divide_cancel_left [simp]:
    6.74 +  "a \<noteq> 0 \<Longrightarrow> divide (a * b) a = b"
    6.75 +  using nonzero_mult_divide_cancel_right [of a b] by (simp add: ac_simps)
    6.76 +
    6.77 +end
    6.78 +
    6.79 +class idom_divide = idom + semidom_divide
    6.80 +
    6.81  class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
    6.82    assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
    6.83    assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"