src/HOL/Ring_and_Field.thy
changeset 24286 7619080e49f0
parent 23879 4776af8be741
child 24422 c0b5ff9e9e4d
     1.1 --- a/src/HOL/Ring_and_Field.thy	Wed Aug 15 09:02:11 2007 +0200
     1.2 +++ b/src/HOL/Ring_and_Field.thy	Wed Aug 15 12:52:56 2007 +0200
     1.3 @@ -660,7 +660,7 @@
     1.4  qed  
     1.5  
     1.6  text{*Cancellation of equalities with a common factor*}
     1.7 -lemma mult_cancel_right [simp]:
     1.8 +lemma mult_cancel_right [simp,noatp]:
     1.9    fixes a b c :: "'a::ring_no_zero_divisors"
    1.10    shows "(a * c = b * c) = (c = 0 \<or> a = b)"
    1.11  proof -
    1.12 @@ -670,7 +670,7 @@
    1.13      by (simp add: disj_commute)
    1.14  qed
    1.15  
    1.16 -lemma mult_cancel_left [simp]:
    1.17 +lemma mult_cancel_left [simp,noatp]:
    1.18    fixes a b c :: "'a::ring_no_zero_divisors"
    1.19    shows "(c * a = c * b) = (c = 0 \<or> a = b)"
    1.20  proof -
    1.21 @@ -1029,11 +1029,11 @@
    1.22  
    1.23  lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
    1.24  
    1.25 -lemma divide_divide_eq_right [simp]:
    1.26 +lemma divide_divide_eq_right [simp,noatp]:
    1.27    "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
    1.28  by (simp add: divide_inverse mult_ac)
    1.29  
    1.30 -lemma divide_divide_eq_left [simp]:
    1.31 +lemma divide_divide_eq_left [simp,noatp]:
    1.32    "(a / b) / (c::'a::{field,division_by_zero}) = a / (b*c)"
    1.33  by (simp add: divide_inverse mult_assoc)
    1.34  
    1.35 @@ -1309,7 +1309,7 @@
    1.36  done
    1.37  
    1.38  text{*Both premises are essential. Consider -1 and 1.*}
    1.39 -lemma inverse_less_iff_less [simp]:
    1.40 +lemma inverse_less_iff_less [simp,noatp]:
    1.41    "[|0 < a; 0 < b|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
    1.42  by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
    1.43  
    1.44 @@ -1317,7 +1317,7 @@
    1.45    "[|a \<le> b; 0 < a|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
    1.46  by (force simp add: order_le_less less_imp_inverse_less)
    1.47  
    1.48 -lemma inverse_le_iff_le [simp]:
    1.49 +lemma inverse_le_iff_le [simp,noatp]:
    1.50   "[|0 < a; 0 < b|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
    1.51  by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
    1.52  
    1.53 @@ -1351,7 +1351,7 @@
    1.54  apply (simp add: order_less_imp_not_eq nonzero_inverse_minus_eq) 
    1.55  done
    1.56  
    1.57 -lemma inverse_less_iff_less_neg [simp]:
    1.58 +lemma inverse_less_iff_less_neg [simp,noatp]:
    1.59    "[|a < 0; b < 0|] ==> (inverse a < inverse b) = (b < (a::'a::ordered_field))"
    1.60  apply (insert inverse_less_iff_less [of "-b" "-a"])
    1.61  apply (simp del: inverse_less_iff_less 
    1.62 @@ -1362,7 +1362,7 @@
    1.63    "[|a \<le> b; b < 0|] ==> inverse b \<le> inverse (a::'a::ordered_field)"
    1.64  by (force simp add: order_le_less less_imp_inverse_less_neg)
    1.65  
    1.66 -lemma inverse_le_iff_le_neg [simp]:
    1.67 +lemma inverse_le_iff_le_neg [simp,noatp]:
    1.68   "[|a < 0; b < 0|] ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
    1.69  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
    1.70  
    1.71 @@ -1585,7 +1585,7 @@
    1.72        (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
    1.73  by (simp add: divide_inverse mult_le_0_iff)
    1.74  
    1.75 -lemma divide_eq_0_iff [simp]:
    1.76 +lemma divide_eq_0_iff [simp,noatp]:
    1.77       "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
    1.78  by (simp add: divide_inverse)
    1.79  
    1.80 @@ -1625,13 +1625,13 @@
    1.81  
    1.82  subsection{*Cancellation Laws for Division*}
    1.83  
    1.84 -lemma divide_cancel_right [simp]:
    1.85 +lemma divide_cancel_right [simp,noatp]:
    1.86       "(a/c = b/c) = (c = 0 | a = (b::'a::{field,division_by_zero}))"
    1.87  apply (cases "c=0", simp)
    1.88  apply (simp add: divide_inverse)
    1.89  done
    1.90  
    1.91 -lemma divide_cancel_left [simp]:
    1.92 +lemma divide_cancel_left [simp,noatp]:
    1.93       "(c/a = c/b) = (c = 0 | a = (b::'a::{field,division_by_zero}))" 
    1.94  apply (cases "c=0", simp)
    1.95  apply (simp add: divide_inverse)
    1.96 @@ -1641,23 +1641,23 @@
    1.97  subsection {* Division and the Number One *}
    1.98  
    1.99  text{*Simplify expressions equated with 1*}
   1.100 -lemma divide_eq_1_iff [simp]:
   1.101 +lemma divide_eq_1_iff [simp,noatp]:
   1.102       "(a/b = 1) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
   1.103  apply (cases "b=0", simp)
   1.104  apply (simp add: right_inverse_eq)
   1.105  done
   1.106  
   1.107 -lemma one_eq_divide_iff [simp]:
   1.108 +lemma one_eq_divide_iff [simp,noatp]:
   1.109       "(1 = a/b) = (b \<noteq> 0 & a = (b::'a::{field,division_by_zero}))"
   1.110  by (simp add: eq_commute [of 1])
   1.111  
   1.112 -lemma zero_eq_1_divide_iff [simp]:
   1.113 +lemma zero_eq_1_divide_iff [simp,noatp]:
   1.114       "((0::'a::{ordered_field,division_by_zero}) = 1/a) = (a = 0)"
   1.115  apply (cases "a=0", simp)
   1.116  apply (auto simp add: nonzero_eq_divide_eq)
   1.117  done
   1.118  
   1.119 -lemma one_divide_eq_0_iff [simp]:
   1.120 +lemma one_divide_eq_0_iff [simp,noatp]:
   1.121       "(1/a = (0::'a::{ordered_field,division_by_zero})) = (a = 0)"
   1.122  apply (cases "a=0", simp)
   1.123  apply (insert zero_neq_one [THEN not_sym])
   1.124 @@ -1671,9 +1671,9 @@
   1.125  lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
   1.126  
   1.127  declare zero_less_divide_1_iff [simp]
   1.128 -declare divide_less_0_1_iff [simp]
   1.129 +declare divide_less_0_1_iff [simp,noatp]
   1.130  declare zero_le_divide_1_iff [simp]
   1.131 -declare divide_le_0_1_iff [simp]
   1.132 +declare divide_le_0_1_iff [simp,noatp]
   1.133  
   1.134  
   1.135  subsection {* Ordering Rules for Division *}
   1.136 @@ -1722,22 +1722,22 @@
   1.137  
   1.138  text{*Simplify quotients that are compared with the value 1.*}
   1.139  
   1.140 -lemma le_divide_eq_1:
   1.141 +lemma le_divide_eq_1 [noatp]:
   1.142    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.143    shows "(1 \<le> b / a) = ((0 < a & a \<le> b) | (a < 0 & b \<le> a))"
   1.144  by (auto simp add: le_divide_eq)
   1.145  
   1.146 -lemma divide_le_eq_1:
   1.147 +lemma divide_le_eq_1 [noatp]:
   1.148    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.149    shows "(b / a \<le> 1) = ((0 < a & b \<le> a) | (a < 0 & a \<le> b) | a=0)"
   1.150  by (auto simp add: divide_le_eq)
   1.151  
   1.152 -lemma less_divide_eq_1:
   1.153 +lemma less_divide_eq_1 [noatp]:
   1.154    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.155    shows "(1 < b / a) = ((0 < a & a < b) | (a < 0 & b < a))"
   1.156  by (auto simp add: less_divide_eq)
   1.157  
   1.158 -lemma divide_less_eq_1:
   1.159 +lemma divide_less_eq_1 [noatp]:
   1.160    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.161    shows "(b / a < 1) = ((0 < a & b < a) | (a < 0 & a < b) | a=0)"
   1.162  by (auto simp add: divide_less_eq)
   1.163 @@ -1745,52 +1745,52 @@
   1.164  
   1.165  subsection{*Conditional Simplification Rules: No Case Splits*}
   1.166  
   1.167 -lemma le_divide_eq_1_pos [simp]:
   1.168 +lemma le_divide_eq_1_pos [simp,noatp]:
   1.169    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.170    shows "0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)"
   1.171  by (auto simp add: le_divide_eq)
   1.172  
   1.173 -lemma le_divide_eq_1_neg [simp]:
   1.174 +lemma le_divide_eq_1_neg [simp,noatp]:
   1.175    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.176    shows "a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)"
   1.177  by (auto simp add: le_divide_eq)
   1.178  
   1.179 -lemma divide_le_eq_1_pos [simp]:
   1.180 +lemma divide_le_eq_1_pos [simp,noatp]:
   1.181    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.182    shows "0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)"
   1.183  by (auto simp add: divide_le_eq)
   1.184  
   1.185 -lemma divide_le_eq_1_neg [simp]:
   1.186 +lemma divide_le_eq_1_neg [simp,noatp]:
   1.187    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.188    shows "a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)"
   1.189  by (auto simp add: divide_le_eq)
   1.190  
   1.191 -lemma less_divide_eq_1_pos [simp]:
   1.192 +lemma less_divide_eq_1_pos [simp,noatp]:
   1.193    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.194    shows "0 < a \<Longrightarrow> (1 < b/a) = (a < b)"
   1.195  by (auto simp add: less_divide_eq)
   1.196  
   1.197 -lemma less_divide_eq_1_neg [simp]:
   1.198 +lemma less_divide_eq_1_neg [simp,noatp]:
   1.199    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.200    shows "a < 0 \<Longrightarrow> (1 < b/a) = (b < a)"
   1.201  by (auto simp add: less_divide_eq)
   1.202  
   1.203 -lemma divide_less_eq_1_pos [simp]:
   1.204 +lemma divide_less_eq_1_pos [simp,noatp]:
   1.205    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.206    shows "0 < a \<Longrightarrow> (b/a < 1) = (b < a)"
   1.207  by (auto simp add: divide_less_eq)
   1.208  
   1.209 -lemma divide_less_eq_1_neg [simp]:
   1.210 +lemma divide_less_eq_1_neg [simp,noatp]:
   1.211    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.212    shows "a < 0 \<Longrightarrow> b/a < 1 <-> a < b"
   1.213  by (auto simp add: divide_less_eq)
   1.214  
   1.215 -lemma eq_divide_eq_1 [simp]:
   1.216 +lemma eq_divide_eq_1 [simp,noatp]:
   1.217    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.218    shows "(1 = b/a) = ((a \<noteq> 0 & a = b))"
   1.219  by (auto simp add: eq_divide_eq)
   1.220  
   1.221 -lemma divide_eq_eq_1 [simp]:
   1.222 +lemma divide_eq_eq_1 [simp,noatp]:
   1.223    fixes a :: "'a :: {ordered_field,division_by_zero}"
   1.224    shows "(b/a = 1) = ((a \<noteq> 0 & a = b))"
   1.225  by (auto simp add: divide_eq_eq)