src/HOL/Ring_and_Field.thy
 changeset 14277 ad66687ece6e parent 14272 5efbb548107d child 14284 f1abe67c448a
```     1.1 --- a/src/HOL/Ring_and_Field.thy	Fri Dec 05 12:58:18 2003 +0100
1.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Dec 05 18:10:59 2003 +0100
1.3 @@ -187,6 +187,9 @@
1.4    }
1.5  qed
1.6
1.7 +lemma nonzero_inverse_eq_divide: "a \<noteq> 0 ==> inverse (a::'a::field) = 1/a"
1.9 +
1.10  lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
1.12
1.13 @@ -534,6 +537,8 @@
1.14  apply (blast dest: zero_less_mult_pos)
1.15  done
1.16
1.17 +text{*A field has no "zero divisors", so this theorem should hold without the
1.18 +      assumption of an ordering.  See @{text field_mult_eq_0_iff} below.*}
1.19  lemma mult_eq_0_iff [simp]: "(a*b = (0::'a::ordered_ring)) = (a = 0 | b = 0)"
1.20  apply (case_tac "a < 0")
1.21  apply (auto simp add: linorder_not_less order_le_less linorder_neq_iff)
1.22 @@ -685,6 +690,17 @@
1.23
1.24  subsection {* Fields *}
1.25
1.26 +lemma divide_inverse_zero: "a/b = a * inverse(b::'a::{field,division_by_zero})"
1.27 +apply (case_tac "b = 0")
1.29 +done
1.30 +
1.31 +lemma divide_zero_left [simp]: "0/a = (0::'a::{field,division_by_zero})"
1.33 +
1.34 +lemma inverse_eq_divide: "inverse (a::'a::{field,division_by_zero}) = 1/a"
1.36 +
1.37  text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement
1.38        of an ordering.*}
1.39  lemma field_mult_eq_0_iff: "(a*b = (0::'a::field)) = (a = 0 | b = 0)"
1.40 @@ -735,6 +751,9 @@
1.41    thus False by (simp add: eq_commute)
1.42    qed
1.43
1.44 +
1.45 +subsection{*Basic Properties of @{term inverse}*}
1.46 +
1.47  lemma inverse_zero_imp_zero: "inverse a = 0 ==> a = (0::'a::field)"
1.48  apply (rule ccontr)
1.49  apply (blast dest: nonzero_imp_inverse_nonzero)
1.50 @@ -855,10 +874,37 @@
1.52  done
1.53
1.54 +lemma nonzero_mult_divide_cancel_left:
1.55 +  assumes [simp]: "b\<noteq>0" and [simp]: "c\<noteq>0"
1.56 +    shows "(c*a)/(c*b) = a/(b::'a::field)"
1.57 +proof -
1.58 +  have "(c*a)/(c*b) = c * a * (inverse b * inverse c)"
1.59 +    by (simp add: field_mult_eq_0_iff divide_inverse
1.60 +                  nonzero_inverse_mult_distrib)
1.61 +  also have "... =  a * inverse b * (inverse c * c)"
1.62 +    by (simp only: mult_ac)
1.63 +  also have "... =  a * inverse b"
1.64 +    by simp
1.65 +    finally show ?thesis
1.66 +    by (simp add: divide_inverse)
1.67 +qed
1.68 +
1.69 +lemma mult_divide_cancel_left:
1.70 +     "c\<noteq>0 ==> (c*a) / (c*b) = a / (b::'a::{field,division_by_zero})"
1.71 +apply (case_tac "b = 0")
1.73 +done
1.74 +
1.75 +(*For ExtractCommonTerm*)
1.76 +lemma mult_divide_cancel_eq_if:
1.77 +     "(c*a) / (c*b) =
1.78 +      (if c=0 then 0 else a / (b::'a::{field,division_by_zero}))"
1.79 +  by (simp add: mult_divide_cancel_left)
1.80 +
1.81
1.82  subsection {* Ordered Fields *}
1.83
1.84 -lemma inverse_gt_0:
1.85 +lemma positive_imp_inverse_positive:
1.86        assumes a_gt_0: "0 < a"  shows "0 < inverse (a::'a::ordered_field)"
1.87    proof -
1.88    have "0 < a * inverse a"
1.89 @@ -867,9 +913,9 @@
1.90      by (simp add: a_gt_0 [THEN order_less_not_sym] zero_less_mult_iff)
1.91    qed
1.92
1.93 -lemma inverse_less_0:
1.94 +lemma negative_imp_inverse_negative:
1.95       "a < 0 ==> inverse a < (0::'a::ordered_field)"
1.96 -  by (insert inverse_gt_0 [of "-a"],
1.97 +  by (insert positive_imp_inverse_positive [of "-a"],
1.99
1.100  lemma inverse_le_imp_le:
1.101 @@ -890,6 +936,51 @@
1.102      by (simp add: mult_assoc apos bpos order_less_imp_not_eq2)
1.103    qed
1.104
1.105 +lemma inverse_positive_imp_positive:
1.106 +      assumes inv_gt_0: "0 < inverse a"
1.107 +          and [simp]:   "a \<noteq> 0"
1.108 +        shows "0 < (a::'a::ordered_field)"
1.109 +  proof -
1.110 +  have "0 < inverse (inverse a)"
1.111 +    by (rule positive_imp_inverse_positive)
1.112 +  thus "0 < a"
1.113 +    by (simp add: nonzero_inverse_inverse_eq)
1.114 +  qed
1.115 +
1.116 +lemma inverse_positive_iff_positive [simp]:
1.117 +      "(0 < inverse a) = (0 < (a::'a::{ordered_field,division_by_zero}))"
1.118 +apply (case_tac "a = 0", simp)
1.119 +apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive)
1.120 +done
1.121 +
1.122 +lemma inverse_negative_imp_negative:
1.123 +      assumes inv_less_0: "inverse a < 0"
1.124 +          and [simp]:   "a \<noteq> 0"
1.125 +        shows "a < (0::'a::ordered_field)"
1.126 +  proof -
1.127 +  have "inverse (inverse a) < 0"
1.128 +    by (rule negative_imp_inverse_negative)
1.129 +  thus "a < 0"
1.130 +    by (simp add: nonzero_inverse_inverse_eq)
1.131 +  qed
1.132 +
1.133 +lemma inverse_negative_iff_negative [simp]:
1.134 +      "(inverse a < 0) = (a < (0::'a::{ordered_field,division_by_zero}))"
1.135 +apply (case_tac "a = 0", simp)
1.136 +apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative)
1.137 +done
1.138 +
1.139 +lemma inverse_nonnegative_iff_nonnegative [simp]:
1.140 +      "(0 \<le> inverse a) = (0 \<le> (a::'a::{ordered_field,division_by_zero}))"
1.141 +by (simp add: linorder_not_less [symmetric])
1.142 +
1.143 +lemma inverse_nonpositive_iff_nonpositive [simp]:
1.144 +      "(inverse a \<le> 0) = (a \<le> (0::'a::{ordered_field,division_by_zero}))"
1.145 +by (simp add: linorder_not_less [symmetric])
1.146 +
1.147 +
1.148 +subsection{*Anti-Monotonicity of @{term inverse}*}
1.149 +
1.150  lemma less_imp_inverse_less:
1.151        assumes less: "a < b"
1.152  	  and apos:  "0 < a"
1.153 @@ -972,4 +1063,30 @@
1.154        ==> (inverse a \<le> inverse b) = (b \<le> (a::'a::ordered_field))"
1.155  by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg)
1.156
1.157 +
1.158 +subsection{*Division and Signs*}
1.159 +
1.160 +lemma zero_less_divide_iff:
1.161 +     "((0::'a::{ordered_field,division_by_zero}) < a/b) = (0 < a & 0 < b | a < 0 & b < 0)"
1.162 +by (simp add: divide_inverse_zero zero_less_mult_iff)
1.163 +
1.164 +lemma divide_less_0_iff:
1.165 +     "(a/b < (0::'a::{ordered_field,division_by_zero})) =
1.166 +      (0 < a & b < 0 | a < 0 & 0 < b)"
1.167 +by (simp add: divide_inverse_zero mult_less_0_iff)
1.168 +
1.169 +lemma zero_le_divide_iff:
1.170 +     "((0::'a::{ordered_field,division_by_zero}) \<le> a/b) =
1.171 +      (0 \<le> a & 0 \<le> b | a \<le> 0 & b \<le> 0)"
1.172 +by (simp add: divide_inverse_zero zero_le_mult_iff)
1.173 +
1.174 +lemma divide_le_0_iff:
1.175 +     "(a/b \<le> (0::'a::{ordered_field,division_by_zero})) = (0 \<le> a & b \<le> 0 | a \<le> 0 & 0 \<le> b)"
1.176 +by (simp add: divide_inverse_zero mult_le_0_iff)
1.177 +
1.178 +lemma divide_eq_0_iff [simp]:
1.179 +     "(a/b = 0) = (a=0 | b=(0::'a::{field,division_by_zero}))"
1.180 +by (simp add: divide_inverse_zero field_mult_eq_0_iff)
1.181 +
1.182 +
1.183  end
```