tuned laws for cancellation in divisions for fields.
authornipkow
Sun Jun 17 18:47:03 2007 +0200 (2007-06-17)
changeset 234135caa2710dd5b
parent 23412 aed08cd6adae
child 23414 927203ad4b3a
tuned laws for cancellation in divisions for fields.
src/HOL/Complex/ex/Sqrt.thy
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/Deriv.thy
src/HOL/Hyperreal/HDeriv.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Library/BigO.thy
src/HOL/Ring_and_Field.thy
src/HOL/SetInterval.thy
src/HOL/int_factor_simprocs.ML
     1.1 --- a/src/HOL/Complex/ex/Sqrt.thy	Sun Jun 17 13:39:50 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/Sqrt.thy	Sun Jun 17 18:47:03 2007 +0200
     1.3 @@ -44,8 +44,7 @@
     1.4    have "\<bar>x\<bar> = real ?k / real ?l"
     1.5    proof -
     1.6      from gcd have "real ?k / real ?l =
     1.7 -        real (?gcd * ?k) / real (?gcd * ?l)"
     1.8 -      by (simp add: mult_divide_cancel_left)
     1.9 +        real (?gcd * ?k) / real (?gcd * ?l)" by simp
    1.10      also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
    1.11      also from x_rat have "\<dots> = \<bar>x\<bar>" ..
    1.12      finally show ?thesis ..
     2.1 --- a/src/HOL/Finite_Set.thy	Sun Jun 17 13:39:50 2007 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Sun Jun 17 18:47:03 2007 +0200
     2.3 @@ -1469,13 +1469,7 @@
     2.4  lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
     2.5      (setprod f (A - {a}) :: 'a :: {field}) =
     2.6        (if a:A then setprod f A / f a else setprod f A)"
     2.7 -  apply (erule finite_induct)
     2.8 -   apply (auto simp add: insert_Diff_if)
     2.9 -  apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a")
    2.10 -  apply (erule ssubst)
    2.11 -  apply (subst times_divide_eq_right [THEN sym])
    2.12 -  apply (auto simp add: mult_ac times_divide_eq_right)
    2.13 -  done
    2.14 +by (erule finite_induct) (auto simp add: insert_Diff_if)
    2.15  
    2.16  lemma setprod_inversef: "finite A ==>
    2.17      ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==>
     3.1 --- a/src/HOL/Hyperreal/Deriv.thy	Sun Jun 17 13:39:50 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/Deriv.thy	Sun Jun 17 18:47:03 2007 +0200
     3.3 @@ -236,8 +236,7 @@
     3.4    show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
     3.5    proof (intro exI conjI)
     3.6      let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
     3.7 -    show "\<forall>z. f z - f x = ?g z * (z-x)"
     3.8 -      by (simp add: nonzero_mult_divide_cancel_right')
     3.9 +    show "\<forall>z. f z - f x = ?g z * (z-x)" by simp
    3.10      show "isCont ?g x" using der
    3.11        by (simp add: isCont_iff DERIV_iff diff_minus
    3.12                 cong: LIM_equal [rule_format])
    3.13 @@ -248,8 +247,7 @@
    3.14    then obtain g where
    3.15      "(\<forall>z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast
    3.16    thus "(DERIV f x :> l)"
    3.17 -     by (auto simp add: isCont_iff DERIV_iff nonzero_mult_divide_cancel_right'
    3.18 -              cong: LIM_cong)
    3.19 +     by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong)
    3.20  qed
    3.21  
    3.22  lemma DERIV_chain':
     4.1 --- a/src/HOL/Hyperreal/HDeriv.thy	Sun Jun 17 13:39:50 2007 +0200
     4.2 +++ b/src/HOL/Hyperreal/HDeriv.thy	Sun Jun 17 18:47:03 2007 +0200
     4.3 @@ -358,13 +358,13 @@
     4.4              del: inverse_mult_distrib inverse_minus_eq
     4.5                   minus_mult_left [symmetric] minus_mult_right [symmetric])
     4.6  apply (subst mult_commute, simp add: nonzero_mult_divide_cancel_right)
     4.7 -apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib
     4.8 +apply (simp (no_asm_simp) add: mult_assoc [symmetric] left_distrib
     4.9              del: minus_mult_left [symmetric] minus_mult_right [symmetric])
    4.10  apply (rule_tac y = "inverse (- (star_of x * star_of x))" in approx_trans)
    4.11  apply (rule inverse_add_Infinitesimal_approx2)
    4.12  apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal
    4.13              simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
    4.14 -apply (rule Infinitesimal_HFinite_mult2, auto)
    4.15 +apply (rule Infinitesimal_HFinite_mult, auto)
    4.16  done
    4.17  
    4.18  subsubsection {* Equivalence of NS and Standard definitions *}
     5.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Sun Jun 17 13:39:50 2007 +0200
     5.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Sun Jun 17 18:47:03 2007 +0200
     5.3 @@ -178,8 +178,6 @@
     5.4          (z + h) ^ q * z ^ (n - 2 - q))" (is "?lhs = ?rhs")
     5.5  apply (subgoal_tac "h * ?lhs = h * ?rhs", simp add: h)
     5.6  apply (simp add: right_diff_distrib diff_divide_distrib h)
     5.7 -apply (simp only: times_divide_eq_left [symmetric])
     5.8 -apply (simp add: divide_self [OF h])
     5.9  apply (simp add: mult_assoc [symmetric])
    5.10  apply (cases "n", simp)
    5.11  apply (simp add: lemma_realpow_diff_sumr2 h
     6.1 --- a/src/HOL/Library/BigO.thy	Sun Jun 17 13:39:50 2007 +0200
     6.2 +++ b/src/HOL/Library/BigO.thy	Sun Jun 17 18:47:03 2007 +0200
     6.3 @@ -698,11 +698,7 @@
     6.4    apply (subgoal_tac "f = (%x. 1 / c) * ((%x. c) * f)")
     6.5    apply (erule ssubst)
     6.6    apply (erule set_times_intro2)
     6.7 -  apply (simp add: func_times) 
     6.8 -  apply (rule ext)
     6.9 -  apply (subst times_divide_eq_left [symmetric])
    6.10 -  apply (subst divide_self)
    6.11 -  apply (assumption, simp)
    6.12 +  apply (simp add: func_times)
    6.13    done
    6.14  
    6.15  lemma bigo_fix: "(%x. f ((x::nat) + 1)) =o O(%x. h(x + 1)) ==> f 0 = 0 ==>
     7.1 --- a/src/HOL/Ring_and_Field.thy	Sun Jun 17 13:39:50 2007 +0200
     7.2 +++ b/src/HOL/Ring_and_Field.thy	Sun Jun 17 18:47:03 2007 +0200
     7.3 @@ -977,7 +977,11 @@
     7.4  
     7.5  subsection {* Calculations with fractions *}
     7.6  
     7.7 -lemma nonzero_mult_divide_cancel_left:
     7.8 +text{* There is a whole bunch of simp-rules just for class @{text
     7.9 +field} but none for class @{text field} and @{text nonzero_divides}
    7.10 +because the latter are covered by a simproc. *}
    7.11 +
    7.12 +lemma nonzero_mult_divide_mult_cancel_left[simp]:
    7.13    assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0" 
    7.14      shows "(c*a)/(c*b) = a/(b::'a::field)"
    7.15  proof -
    7.16 @@ -992,21 +996,22 @@
    7.17      by (simp add: divide_inverse)
    7.18  qed
    7.19  
    7.20 -lemma mult_divide_cancel_left:
    7.21 +lemma mult_divide_mult_cancel_left:
    7.22       "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
    7.23  apply (cases "b = 0")
    7.24 -apply (simp_all add: nonzero_mult_divide_cancel_left)
    7.25 +apply (simp_all add: nonzero_mult_divide_mult_cancel_left)
    7.26  done
    7.27  
    7.28 -lemma nonzero_mult_divide_cancel_right:
    7.29 +lemma nonzero_mult_divide_mult_cancel_right:
    7.30       "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (b*c) = a/(b::'a::field)"
    7.31 -by (simp add: mult_commute [of _ c] nonzero_mult_divide_cancel_left) 
    7.32 +by (simp add: mult_commute [of _ c] nonzero_mult_divide_mult_cancel_left) 
    7.33  
    7.34 -lemma mult_divide_cancel_right:
    7.35 +lemma mult_divide_mult_cancel_right:
    7.36       "c\<noteq>0 ==> (a*c) / (b*c) = a / (b::'a::{field,division_by_zero})"
    7.37  apply (cases "b = 0")
    7.38 -apply (simp_all add: nonzero_mult_divide_cancel_right)
    7.39 +apply (simp_all add: nonzero_mult_divide_mult_cancel_right)
    7.40  done
    7.41 +
    7.42  lemma divide_1 [simp]: "a/1 = (a::'a::field)"
    7.43    by (simp add: divide_inverse)
    7.44  
    7.45 @@ -1032,39 +1037,46 @@
    7.46    apply (erule ssubst)
    7.47    apply (rule add_divide_distrib [THEN sym])
    7.48    apply (subst mult_commute)
    7.49 -  apply (erule nonzero_mult_divide_cancel_left [THEN sym])
    7.50 +  apply (erule nonzero_mult_divide_mult_cancel_left [THEN sym])
    7.51    apply assumption
    7.52 -  apply (erule nonzero_mult_divide_cancel_right [THEN sym])
    7.53 +  apply (erule nonzero_mult_divide_mult_cancel_right [THEN sym])
    7.54    apply assumption
    7.55  done
    7.56  
    7.57  
    7.58 -lemma nonzero_mult_divide_cancel_right':
    7.59 -  "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
    7.60 -proof -
    7.61 -  assume b: "b \<noteq> 0"
    7.62 -  have "a * b / b = a * (b / b)" by (simp add: times_divide_eq_right)
    7.63 -  also have "\<dots> = a" by (simp add: divide_self b)
    7.64 -  finally show "a * b / b = a" .
    7.65 -qed
    7.66 -
    7.67 -lemma nonzero_mult_divide_cancel_left':
    7.68 -  "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
    7.69 -proof -
    7.70 -  assume b: "a \<noteq> 0"
    7.71 -  have "a * b / a = b * a / a" by (simp add: mult_commute)
    7.72 -  also have "\<dots> = b * (a / a)" by (simp add: times_divide_eq_right)
    7.73 -  also have "\<dots> = b" by (simp add: divide_self b)
    7.74 -  finally show "a * b / a = b" .
    7.75 -qed
    7.76 -
    7.77  subsubsection{*Special Cancellation Simprules for Division*}
    7.78  
    7.79 -(* FIXME need not be a simp-rule once "divide_cancel_factor" has been fixed *)
    7.80 -lemma mult_divide_cancel_left_if[simp]:
    7.81 +lemma mult_divide_mult_cancel_left_if[simp]:
    7.82    fixes c :: "'a :: {field,division_by_zero}"
    7.83    shows "(c*a) / (c*b) = (if c=0 then 0 else a/b)"
    7.84 -by (simp add: mult_divide_cancel_left)
    7.85 +by (simp add: mult_divide_mult_cancel_left)
    7.86 +
    7.87 +lemma nonzero_mult_divide_cancel_right[simp]:
    7.88 +  "b \<noteq> 0 \<Longrightarrow> a * b / b = (a::'a::field)"
    7.89 +using nonzero_mult_divide_mult_cancel_right[of 1 b a] by simp
    7.90 +
    7.91 +lemma nonzero_mult_divide_cancel_left[simp]:
    7.92 +  "a \<noteq> 0 \<Longrightarrow> a * b / a = (b::'a::field)"
    7.93 +using nonzero_mult_divide_mult_cancel_left[of 1 a b] by simp
    7.94 +
    7.95 +
    7.96 +lemma nonzero_divide_mult_cancel_right[simp]:
    7.97 +  "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> b / (a * b) = 1/(a::'a::field)"
    7.98 +using nonzero_mult_divide_mult_cancel_right[of a b 1] by simp
    7.99 +
   7.100 +lemma nonzero_divide_mult_cancel_left[simp]:
   7.101 +  "\<lbrakk> a\<noteq>0; b\<noteq>0 \<rbrakk> \<Longrightarrow> a / (a * b) = 1/(b::'a::field)"
   7.102 +using nonzero_mult_divide_mult_cancel_left[of b a 1] by simp
   7.103 +
   7.104 +
   7.105 +lemma nonzero_mult_divide_mult_cancel_left2[simp]:
   7.106 +     "[|b\<noteq>0; c\<noteq>0|] ==> (c*a) / (b*c) = a/(b::'a::field)"
   7.107 +using nonzero_mult_divide_mult_cancel_left[of b c a] by(simp add:mult_ac)
   7.108 +
   7.109 +lemma nonzero_mult_divide_mult_cancel_right2[simp]:
   7.110 +     "[|b\<noteq>0; c\<noteq>0|] ==> (a*c) / (c*b) = a/(b::'a::field)"
   7.111 +using nonzero_mult_divide_mult_cancel_right[of b c a] by(simp add:mult_ac)
   7.112 +
   7.113  
   7.114  (* Not needed anymore because now subsumed by simproc "divide_cancel_factor"
   7.115  lemma mult_divide_cancel_right_if:
   7.116 @@ -1113,6 +1125,7 @@
   7.117  by (simp add: times_divide_eq_left)
   7.118  *)
   7.119  
   7.120 +
   7.121  subsection {* Division and Unary Minus *}
   7.122  
   7.123  lemma nonzero_minus_divide_left: "b \<noteq> 0 ==> - (a/b) = (-a) / (b::'a::field)"
     8.1 --- a/src/HOL/SetInterval.thy	Sun Jun 17 13:39:50 2007 +0200
     8.2 +++ b/src/HOL/SetInterval.thy	Sun Jun 17 18:47:03 2007 +0200
     8.3 @@ -739,12 +739,11 @@
     8.4  lemma geometric_sum:
     8.5    "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) =
     8.6    (x ^ n - 1) / (x - 1::'a::{field, recpower})"
     8.7 -  apply (induct "n", auto)
     8.8 -  apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
     8.9 -  apply (auto simp add: mult_assoc left_distrib)
    8.10 -  apply (simp add: times_divide_eq_right [symmetric])
    8.11 -  apply (simp add: right_distrib diff_minus mult_commute power_Suc)
    8.12 -  done
    8.13 +apply (induct "n", auto)
    8.14 +apply (rule_tac c = "x - 1" in field_mult_cancel_right_lemma)
    8.15 +apply (auto simp add: mult_assoc left_distrib)
    8.16 +apply (simp add: right_distrib diff_minus mult_commute power_Suc)
    8.17 +done
    8.18  
    8.19  
    8.20  subsection {* The formula for arithmetic sums *}
     9.1 --- a/src/HOL/int_factor_simprocs.ML	Sun Jun 17 13:39:50 2007 +0200
     9.2 +++ b/src/HOL/int_factor_simprocs.ML	Sun Jun 17 18:47:03 2007 +0200
     9.3 @@ -62,7 +62,7 @@
     9.4    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
     9.5    val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
     9.6    val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
     9.7 -  val cancel = @{thm mult_divide_cancel_left} RS trans
     9.8 +  val cancel = @{thm mult_divide_mult_cancel_left} RS trans
     9.9    val neg_exchanges = false
    9.10  )
    9.11  
    9.12 @@ -257,7 +257,7 @@
    9.13    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    9.14    val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
    9.15    val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
    9.16 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_cancel_left_if}
    9.17 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm mult_divide_mult_cancel_left_if}
    9.18  );
    9.19  
    9.20  val cancel_factors =