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.8 +by (simp add: divide_inverse)
     1.9 +
    1.10  lemma divide_self [simp]: "a \<noteq> 0 ==> a / (a::'a::field) = 1"
    1.11    by (simp add: divide_inverse)
    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.28 +apply (simp_all add: divide_inverse)
    1.29 +done
    1.30 +
    1.31 +lemma divide_zero_left [simp]: "0/a = (0::'a::{field,division_by_zero})"
    1.32 +by (simp add: divide_inverse_zero)
    1.33 +
    1.34 +lemma inverse_eq_divide: "inverse (a::'a::{field,division_by_zero}) = 1/a"
    1.35 +by (simp add: divide_inverse_zero)
    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.51  apply (simp add: mult_assoc [symmetric] add_commute)
    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.72 +apply (simp_all add: nonzero_mult_divide_cancel_left)
    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.98        simp add: nonzero_inverse_minus_eq order_less_imp_not_eq) 
    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