author  haftmann 
Fri, 14 Jun 2019 08:34:27 +0000  
changeset 70344  050104f01bf9 
parent 70343  e54caaa38ad9 
child 70356  4a327c061870 
permissions  rwrr 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

1 
(* Title: HOL/Fields.thy 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

2 
Author: Gertrud Bauer 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

3 
Author: Steven Obua 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

4 
Author: Tobias Nipkow 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

5 
Author: Lawrence C Paulson 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

6 
Author: Markus Wenzel 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30961
diff
changeset

7 
Author: Jeremy Avigad 
14265
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

8 
*) 
95b42e69436c
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
paulson
parents:
diff
changeset

9 

60758  10 
section \<open>Fields\<close> 
25152  11 

35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35043
diff
changeset

12 
theory Fields 
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

13 
imports Nat 
25186  14 
begin 
14421
ee97b6463cb4
new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents:
14398
diff
changeset

15 

69502  16 
context idom 
17 
begin 

18 

19 
lemma inj_mult_left [simp]: \<open>inj ((*) a) \<longleftrightarrow> a \<noteq> 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>) 

20 
proof 

21 
assume ?P 

22 
show ?Q 

23 
proof 

24 
assume \<open>a = 0\<close> 

25 
with \<open>?P\<close> have "inj ((*) 0)" 

26 
by simp 

27 
moreover have "0 * 0 = 0 * 1" 

28 
by simp 

29 
ultimately have "0 = 1" 

30 
by (rule injD) 

31 
then show False 

32 
by simp 

33 
qed 

34 
next 

35 
assume ?Q then show ?P 

36 
by (auto intro: injI) 

37 
qed 

38 

39 
end 

40 

41 

60758  42 
subsection \<open>Division rings\<close> 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

43 

60758  44 
text \<open> 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

45 
A division ring is like a field, but without the commutativity requirement. 
60758  46 
\<close> 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

47 

60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59867
diff
changeset

48 
class inverse = divide + 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

49 
fixes inverse :: "'a \<Rightarrow> 'a" 
58776
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58512
diff
changeset

50 
begin 
60352
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59867
diff
changeset

51 

d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59867
diff
changeset

52 
abbreviation inverse_divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70) 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59867
diff
changeset

53 
where 
d46de31a50c4
separate class for division operator, with particular syntax added in more specific classes
haftmann
parents:
59867
diff
changeset

54 
"inverse_divide \<equiv> divide" 
58776
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58512
diff
changeset

55 

95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58512
diff
changeset

56 
end 
95e58e04e534
use NO_MATCHsimproc for distribution rules in field_simps, otherwise field_simps on '(a / (c + d)) * (e + f)' can be nonterminating
hoelzl
parents:
58512
diff
changeset

57 

62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

58 
text \<open>Setup for linear arithmetic prover\<close> 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

59 

69605  60 
ML_file \<open>~~/src/Provers/Arith/fast_lin_arith.ML\<close> 
61 
ML_file \<open>Tools/lin_arith.ML\<close> 

62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

62 
setup \<open>Lin_Arith.global_setup\<close> 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

63 
declaration \<open>K Lin_Arith.setup\<close> 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

64 

b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

65 
simproc_setup fast_arith_nat ("(m::nat) < n"  "(m::nat) \<le> n"  "(m::nat) = n") = 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

66 
\<open>K Lin_Arith.simproc\<close> 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

67 
(* Because of this simproc, the arithmetic solver is really only 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

68 
useful to detect inconsistencies among the premises for subgoals which are 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

69 
*not* themselves (in)equalities, because the latter activate 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

70 
fast_nat_arith_simproc anyway. However, it seems cheaper to activate the 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

71 
solver all the time rather than add the additional check. *) 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

72 

b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

73 
lemmas [arith_split] = nat_diff_split split_min split_max 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

74 

67969
83c8cafdebe8
Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

75 
context linordered_nonzero_semiring 
83c8cafdebe8
Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

76 
begin 
83c8cafdebe8
Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

77 
lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)" 
83c8cafdebe8
Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

78 
by (auto simp: max_def) 
83c8cafdebe8
Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

79 

83c8cafdebe8
Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

80 
lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)" 
83c8cafdebe8
Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

81 
by (auto simp: min_def) 
83c8cafdebe8
Syntax for the special cases Min(A`I) and Max (A`I)
paulson <lp15@cam.ac.uk>
parents:
67091
diff
changeset

82 
end 
62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

83 

61799  84 
text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close> 
56481  85 

57950  86 
named_theorems divide_simps "rewrite rules to eliminate divisions" 
56481  87 

44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

88 
class division_ring = ring_1 + inverse + 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

89 
assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

90 
assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

91 
assumes divide_inverse: "a / b = a * inverse b" 
59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59779
diff
changeset

92 
assumes inverse_zero [simp]: "inverse 0 = 0" 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

93 
begin 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

94 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

95 
subclass ring_1_no_zero_divisors 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

96 
proof 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

97 
fix a b :: 'a 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

98 
assume a: "a \<noteq> 0" and b: "b \<noteq> 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

99 
show "a * b \<noteq> 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

100 
proof 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

101 
assume ab: "a * b = 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

102 
hence "0 = inverse a * (a * b) * inverse b" by simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

103 
also have "\<dots> = (inverse a * a) * (b * inverse b)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

104 
by (simp only: mult.assoc) 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

105 
also have "\<dots> = 1" using a b by simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

106 
finally show False by simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

107 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

108 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

109 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

110 
lemma nonzero_imp_inverse_nonzero: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

111 
"a \<noteq> 0 \<Longrightarrow> inverse a \<noteq> 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

112 
proof 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

113 
assume ianz: "inverse a = 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

114 
assume "a \<noteq> 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

115 
hence "1 = a * inverse a" by simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

116 
also have "... = 0" by (simp add: ianz) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

117 
finally have "1 = 0" . 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

118 
thus False by (simp add: eq_commute) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

119 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

120 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

121 
lemma inverse_zero_imp_zero: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

122 
"inverse a = 0 \<Longrightarrow> a = 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

123 
apply (rule classical) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

124 
apply (drule nonzero_imp_inverse_nonzero) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

125 
apply auto 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

126 
done 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

127 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

128 
lemma inverse_unique: 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

129 
assumes ab: "a * b = 1" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

130 
shows "inverse a = b" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

131 
proof  
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

132 
have "a \<noteq> 0" using ab by (cases "a = 0") simp_all 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

133 
moreover have "inverse a * (a * b) = inverse a" by (simp add: ab) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

134 
ultimately show ?thesis by (simp add: mult.assoc [symmetric]) 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

135 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

136 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

137 
lemma nonzero_inverse_minus_eq: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

138 
"a \<noteq> 0 \<Longrightarrow> inverse ( a) =  inverse a" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

139 
by (rule inverse_unique) simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

140 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

141 
lemma nonzero_inverse_inverse_eq: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

142 
"a \<noteq> 0 \<Longrightarrow> inverse (inverse a) = a" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

143 
by (rule inverse_unique) simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

144 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

145 
lemma nonzero_inverse_eq_imp_eq: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

146 
assumes "inverse a = inverse b" and "a \<noteq> 0" and "b \<noteq> 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

147 
shows "a = b" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

148 
proof  
60758  149 
from \<open>inverse a = inverse b\<close> 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

150 
have "inverse (inverse a) = inverse (inverse b)" by (rule arg_cong) 
60758  151 
with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> show "a = b" 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

152 
by (simp add: nonzero_inverse_inverse_eq) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

153 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

154 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

155 
lemma inverse_1 [simp]: "inverse 1 = 1" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

156 
by (rule inverse_unique) simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

157 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

158 
lemma nonzero_inverse_mult_distrib: 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

159 
assumes "a \<noteq> 0" and "b \<noteq> 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

160 
shows "inverse (a * b) = inverse b * inverse a" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

161 
proof  
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

162 
have "a * (b * inverse b) * inverse a = 1" using assms by simp 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

163 
hence "a * b * (inverse b * inverse a) = 1" by (simp only: mult.assoc) 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

164 
thus ?thesis by (rule inverse_unique) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

165 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

166 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

167 
lemma division_ring_inverse_add: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

168 
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = inverse a * (a + b) * inverse b" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

169 
by (simp add: algebra_simps) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

170 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

171 
lemma division_ring_inverse_diff: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

172 
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a  inverse b = inverse a * (b  a) * inverse b" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

173 
by (simp add: algebra_simps) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

174 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

175 
lemma right_inverse_eq: "b \<noteq> 0 \<Longrightarrow> a / b = 1 \<longleftrightarrow> a = b" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

176 
proof 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

177 
assume neq: "b \<noteq> 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

178 
{ 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

179 
hence "a = (a / b) * b" by (simp add: divide_inverse mult.assoc) 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

180 
also assume "a / b = 1" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

181 
finally show "a = b" by simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

182 
next 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

183 
assume "a = b" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

184 
with neq show "a / b = 1" by (simp add: divide_inverse) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

185 
} 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

186 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

187 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

188 
lemma nonzero_inverse_eq_divide: "a \<noteq> 0 \<Longrightarrow> inverse a = 1 / a" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

189 
by (simp add: divide_inverse) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

190 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

191 
lemma divide_self [simp]: "a \<noteq> 0 \<Longrightarrow> a / a = 1" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

192 
by (simp add: divide_inverse) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

193 

56481  194 
lemma inverse_eq_divide [field_simps, divide_simps]: "inverse a = 1 / a" 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

195 
by (simp add: divide_inverse) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

196 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

197 
lemma add_divide_distrib: "(a+b) / c = a/c + b/c" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

198 
by (simp add: divide_inverse algebra_simps) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

199 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

200 
lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

201 
by (simp add: divide_inverse mult.assoc) 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

202 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

203 
lemma minus_divide_left: " (a / b) = (a) / b" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

204 
by (simp add: divide_inverse) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

205 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

206 
lemma nonzero_minus_divide_right: "b \<noteq> 0 ==>  (a / b) = a / ( b)" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

207 
by (simp add: divide_inverse nonzero_inverse_minus_eq) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

208 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

209 
lemma nonzero_minus_divide_divide: "b \<noteq> 0 ==> (a) / (b) = a / b" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

210 
by (simp add: divide_inverse nonzero_inverse_minus_eq) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

211 

56479
91958d4b30f7
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents:
56445
diff
changeset

212 
lemma divide_minus_left [simp]: "(a) / b =  (a / b)" 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

213 
by (simp add: divide_inverse) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

214 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

215 
lemma diff_divide_distrib: "(a  b) / c = a / c  b / c" 
56479
91958d4b30f7
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents:
56445
diff
changeset

216 
using add_divide_distrib [of a " b" c] by simp 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

217 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

218 
lemma nonzero_eq_divide_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> a = b / c \<longleftrightarrow> a * c = b" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

219 
proof  
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

220 
assume [simp]: "c \<noteq> 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

221 
have "a = b / c \<longleftrightarrow> a * c = (b / c) * c" by simp 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

222 
also have "... \<longleftrightarrow> a * c = b" by (simp add: divide_inverse mult.assoc) 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

223 
finally show ?thesis . 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

224 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

225 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

226 
lemma nonzero_divide_eq_eq [field_simps]: "c \<noteq> 0 \<Longrightarrow> b / c = a \<longleftrightarrow> b = a * c" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

227 
proof  
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

228 
assume [simp]: "c \<noteq> 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

229 
have "b / c = a \<longleftrightarrow> (b / c) * c = a * c" by simp 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

230 
also have "... \<longleftrightarrow> b = a * c" by (simp add: divide_inverse mult.assoc) 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

231 
finally show ?thesis . 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

232 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

233 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

234 
lemma nonzero_neg_divide_eq_eq [field_simps]: "b \<noteq> 0 \<Longrightarrow>  (a / b) = c \<longleftrightarrow>  a = c * b" 
59535  235 
using nonzero_divide_eq_eq[of b "a" c] by simp 
56441  236 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

237 
lemma nonzero_neg_divide_eq_eq2 [field_simps]: "b \<noteq> 0 \<Longrightarrow> c =  (a / b) \<longleftrightarrow> c * b =  a" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

238 
using nonzero_neg_divide_eq_eq[of b a c] by auto 
56441  239 

44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

240 
lemma divide_eq_imp: "c \<noteq> 0 \<Longrightarrow> b = a * c \<Longrightarrow> b / c = a" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

241 
by (simp add: divide_inverse mult.assoc) 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

242 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

243 
lemma eq_divide_imp: "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

244 
by (drule sym) (simp add: divide_inverse mult.assoc) 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

245 

56445  246 
lemma add_divide_eq_iff [field_simps]: 
247 
"z \<noteq> 0 \<Longrightarrow> x + y / z = (x * z + y) / z" 

248 
by (simp add: add_divide_distrib nonzero_eq_divide_eq) 

249 

250 
lemma divide_add_eq_iff [field_simps]: 

251 
"z \<noteq> 0 \<Longrightarrow> x / z + y = (x + y * z) / z" 

252 
by (simp add: add_divide_distrib nonzero_eq_divide_eq) 

253 

254 
lemma diff_divide_eq_iff [field_simps]: 

255 
"z \<noteq> 0 \<Longrightarrow> x  y / z = (x * z  y) / z" 

256 
by (simp add: diff_divide_distrib nonzero_eq_divide_eq eq_diff_eq) 

257 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

258 
lemma minus_divide_add_eq_iff [field_simps]: 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

259 
"z \<noteq> 0 \<Longrightarrow>  (x / z) + y = ( x + y * z) / z" 
59535  260 
by (simp add: add_divide_distrib diff_divide_eq_iff) 
56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

261 

56445  262 
lemma divide_diff_eq_iff [field_simps]: 
263 
"z \<noteq> 0 \<Longrightarrow> x / z  y = (x  y * z) / z" 

264 
by (simp add: field_simps) 

265 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

266 
lemma minus_divide_diff_eq_iff [field_simps]: 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

267 
"z \<noteq> 0 \<Longrightarrow>  (x / z)  y = ( x  y * z) / z" 
59535  268 
by (simp add: divide_diff_eq_iff[symmetric]) 
56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

269 

60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

270 
lemma division_ring_divide_zero [simp]: 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

271 
"a / 0 = 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

272 
by (simp add: divide_inverse) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

273 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

274 
lemma divide_self_if [simp]: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

275 
"a / a = (if a = 0 then 0 else 1)" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

276 
by simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

277 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

278 
lemma inverse_nonzero_iff_nonzero [simp]: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

279 
"inverse a = 0 \<longleftrightarrow> a = 0" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

280 
by rule (fact inverse_zero_imp_zero, simp) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

281 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

282 
lemma inverse_minus_eq [simp]: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

283 
"inverse ( a) =  inverse a" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

284 
proof cases 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

285 
assume "a=0" thus ?thesis by simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

286 
next 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

287 
assume "a\<noteq>0" 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

288 
thus ?thesis by (simp add: nonzero_inverse_minus_eq) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

289 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

290 

5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

291 
lemma inverse_inverse_eq [simp]: 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

292 
"inverse (inverse a) = a" 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

293 
proof cases 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

294 
assume "a=0" thus ?thesis by simp 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

295 
next 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

296 
assume "a\<noteq>0" 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

297 
thus ?thesis by (simp add: nonzero_inverse_inverse_eq) 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

298 
qed 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

299 

44680  300 
lemma inverse_eq_imp_eq: 
301 
"inverse a = inverse b \<Longrightarrow> a = b" 

302 
by (drule arg_cong [where f="inverse"], simp) 

303 

304 
lemma inverse_eq_iff_eq [simp]: 

305 
"inverse a = inverse b \<longleftrightarrow> a = b" 

306 
by (force dest!: inverse_eq_imp_eq) 

307 

69791
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

308 
lemma mult_commute_imp_mult_inverse_commute: 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

309 
assumes "y * x = x * y" 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

310 
shows "inverse y * x = x * inverse y" 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

311 
proof (cases "y=0") 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

312 
case False 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

313 
hence "x * inverse y = inverse y * y * x * inverse y" 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

314 
by simp 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

315 
also have "\<dots> = inverse y * (x * y * inverse y)" 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

316 
by (simp add: mult.assoc assms) 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

317 
finally show ?thesis by (simp add: mult.assoc False) 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

318 
qed simp 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

319 

195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

320 
lemmas mult_inverse_of_nat_commute = 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

321 
mult_commute_imp_mult_inverse_commute[OF mult_of_nat_commute] 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

322 

195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

323 
lemma divide_divide_eq_left': 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

324 
"(a / b) / c = a / (c * b)" 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

325 
by (cases "b = 0 \<or> c = 0") 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

326 
(auto simp: divide_inverse mult.assoc nonzero_inverse_mult_distrib) 
195aeee8b30a
Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre)
Manuel Eberl <eberlm@in.tum.de>
parents:
69605
diff
changeset

327 

56481  328 
lemma add_divide_eq_if_simps [divide_simps]: 
329 
"a + b / z = (if z = 0 then a else (a * z + b) / z)" 

330 
"a / z + b = (if z = 0 then b else (a + b * z) / z)" 

331 
" (a / z) + b = (if z = 0 then b else (a + b * z) / z)" 

332 
"a  b / z = (if z = 0 then a else (a * z  b) / z)" 

333 
"a / z  b = (if z = 0 then b else (a  b * z) / z)" 

334 
" (a / z)  b = (if z = 0 then b else ( a  b * z) / z)" 

335 
by (simp_all add: add_divide_eq_iff divide_add_eq_iff diff_divide_eq_iff divide_diff_eq_iff 

336 
minus_divide_diff_eq_iff) 

337 

338 
lemma [divide_simps]: 

339 
shows divide_eq_eq: "b / c = a \<longleftrightarrow> (if c \<noteq> 0 then b = a * c else a = 0)" 

340 
and eq_divide_eq: "a = b / c \<longleftrightarrow> (if c \<noteq> 0 then a * c = b else a = 0)" 

341 
and minus_divide_eq_eq: " (b / c) = a \<longleftrightarrow> (if c \<noteq> 0 then  b = a * c else a = 0)" 

342 
and eq_minus_divide_eq: "a =  (b / c) \<longleftrightarrow> (if c \<noteq> 0 then a * c =  b else a = 0)" 

343 
by (auto simp add: field_simps) 

344 

44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

345 
end 
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

346 

60758  347 
subsection \<open>Fields\<close> 
44064
5bce8ff0d9ae
moved division ring stuff from Rings.thy to Fields.thy
huffman
parents:
42904
diff
changeset

348 

22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

349 
class field = comm_ring_1 + inverse + 
35084  350 
assumes field_inverse: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 
351 
assumes field_divide_inverse: "a / b = a * inverse b" 

59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59779
diff
changeset

352 
assumes field_inverse_zero: "inverse 0 = 0" 
25267  353 
begin 
20496
23eb6034c06d
added axclass division_ring (like field without commutativity; includes e.g. quaternions) and generalized some theorems from field to division_ring
huffman
parents:
19404
diff
changeset

354 

25267  355 
subclass division_ring 
28823  356 
proof 
22987
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

357 
fix a :: 'a 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

358 
assume "a \<noteq> 0" 
550709aa8e66
instance division_ring < no_zero_divisors; clean up field instance proofs
huffman
parents:
22842
diff
changeset

359 
thus "inverse a * a = 1" by (rule field_inverse) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

360 
thus "a * inverse a = 1" by (simp only: mult.commute) 
35084  361 
next 
362 
fix a b :: 'a 

363 
show "a / b = a * inverse b" by (rule field_divide_inverse) 

59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59779
diff
changeset

364 
next 
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59779
diff
changeset

365 
show "inverse 0 = 0" 
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59779
diff
changeset

366 
by (fact field_inverse_zero) 
14738  367 
qed 
25230  368 

60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

369 
subclass idom_divide 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

370 
proof 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

371 
fix b a 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

372 
assume "b \<noteq> 0" 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

373 
then show "a * b / b = a" 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

374 
by (simp add: divide_inverse ac_simps) 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

375 
next 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

376 
fix a 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

377 
show "a / 0 = 0" 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

378 
by (simp add: divide_inverse) 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

379 
qed 
25230  380 

60758  381 
text\<open>There is no slick version using division by zero.\<close> 
30630  382 
lemma inverse_add: 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

383 
"a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse a + inverse b = (a + b) * inverse a * inverse b" 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

384 
by (simp add: division_ring_inverse_add ac_simps) 
30630  385 

70147
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

386 
lemma nonzero_mult_divide_mult_cancel_left [simp]: 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

387 
assumes [simp]: "c \<noteq> 0" 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

388 
shows "(c * a) / (c * b) = a / b" 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

389 
proof (cases "b = 0") 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

390 
case True then show ?thesis by simp 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

391 
next 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

392 
case False 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

393 
then have "(c*a)/(c*b) = c * a * (inverse b * inverse c)" 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

394 
by (simp add: divide_inverse nonzero_inverse_mult_distrib) 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

395 
also have "... = a * inverse b * (inverse c * c)" 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

396 
by (simp only: ac_simps) 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

397 
also have "... = a * inverse b" by simp 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

398 
finally show ?thesis by (simp add: divide_inverse) 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

399 
qed 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

400 

1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

401 
lemma nonzero_mult_divide_mult_cancel_right [simp]: 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

402 
"c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b" 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

403 
using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps) 
1657688a6406
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
haftmann
parents:
70094
diff
changeset

404 

36304
6984744e6b34
less special treatment of times_divide_eq [simp]
haftmann
parents:
36301
diff
changeset

405 
lemma times_divide_eq_left [simp]: "(b / c) * a = (b * a) / c" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

406 
by (simp add: divide_inverse ac_simps) 
30630  407 

61238
e3d8a313a649
Useful facts about min/max, etc.
paulson <lp15@cam.ac.uk>
parents:
61076
diff
changeset

408 
lemma divide_inverse_commute: "a / b = inverse b * a" 
e3d8a313a649
Useful facts about min/max, etc.
paulson <lp15@cam.ac.uk>
parents:
61076
diff
changeset

409 
by (simp add: divide_inverse mult.commute) 
e3d8a313a649
Useful facts about min/max, etc.
paulson <lp15@cam.ac.uk>
parents:
61076
diff
changeset

410 

30630  411 
lemma add_frac_eq: 
412 
assumes "y \<noteq> 0" and "z \<noteq> 0" 

413 
shows "x / y + w / z = (x * z + w * y) / (y * z)" 

414 
proof  

415 
have "x / y + w / z = (x * z) / (y * z) + (y * w) / (y * z)" 

416 
using assms by simp 

417 
also have "\<dots> = (x * z + y * w) / (y * z)" 

418 
by (simp only: add_divide_distrib) 

419 
finally show ?thesis 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

420 
by (simp only: mult.commute) 
30630  421 
qed 
422 

60758  423 
text\<open>Special Cancellation Simprules for Division\<close> 
30630  424 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

425 
lemma nonzero_divide_mult_cancel_right [simp]: 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

426 
"b \<noteq> 0 \<Longrightarrow> b / (a * b) = 1 / a" 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

427 
using nonzero_mult_divide_mult_cancel_right [of b 1 a] by simp 
30630  428 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

429 
lemma nonzero_divide_mult_cancel_left [simp]: 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

430 
"a \<noteq> 0 \<Longrightarrow> a / (a * b) = 1 / b" 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

431 
using nonzero_mult_divide_mult_cancel_left [of a 1 b] by simp 
30630  432 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

433 
lemma nonzero_mult_divide_mult_cancel_left2 [simp]: 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

434 
"c \<noteq> 0 \<Longrightarrow> (c * a) / (b * c) = a / b" 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

435 
using nonzero_mult_divide_mult_cancel_left [of c a b] by (simp add: ac_simps) 
30630  436 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

437 
lemma nonzero_mult_divide_mult_cancel_right2 [simp]: 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

438 
"c \<noteq> 0 \<Longrightarrow> (a * c) / (c * b) = a / b" 
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

439 
using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps) 
30630  440 

441 
lemma diff_frac_eq: 

442 
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y  w / z = (x * z  w * y) / (y * z)" 

36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

443 
by (simp add: field_simps) 
30630  444 

445 
lemma frac_eq_eq: 

446 
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)" 

36348
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

447 
by (simp add: field_simps) 
89c54f51f55a
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
haftmann
parents:
36343
diff
changeset

448 

58512
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
57950
diff
changeset

449 
lemma divide_minus1 [simp]: "x /  1 =  x" 
dc4d76dfa8f0
moved lemmas out of Int.thy which have nothing to do with int
haftmann
parents:
57950
diff
changeset

450 
using nonzero_minus_divide_right [of "1" x] by simp 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

451 

60758  452 
text\<open>This version builds in division by zero while also reorienting 
453 
the righthand side.\<close> 

14270  454 
lemma inverse_mult_distrib [simp]: 
36409  455 
"inverse (a * b) = inverse a * inverse b" 
456 
proof cases 

67091  457 
assume "a \<noteq> 0 \<and> b \<noteq> 0" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

458 
thus ?thesis by (simp add: nonzero_inverse_mult_distrib ac_simps) 
36409  459 
next 
67091  460 
assume "\<not> (a \<noteq> 0 \<and> b \<noteq> 0)" 
36409  461 
thus ?thesis by force 
462 
qed 

14270  463 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

464 
lemma inverse_divide [simp]: 
36409  465 
"inverse (a / b) = b / a" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

466 
by (simp add: divide_inverse mult.commute) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

467 

23389  468 

60758  469 
text \<open>Calculations with fractions\<close> 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

470 

61799  471 
text\<open>There is a whole bunch of simprules just for class \<open>field\<close> but none for class \<open>field\<close> and \<open>nonzero_divides\<close> 
60758  472 
because the latter are covered by a simproc.\<close> 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

473 

68527
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
67969
diff
changeset

474 
lemmas mult_divide_mult_cancel_left = nonzero_mult_divide_mult_cancel_left 
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

475 

68527
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
67969
diff
changeset

476 
lemmas mult_divide_mult_cancel_right = nonzero_mult_divide_mult_cancel_right 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

477 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

478 
lemma divide_divide_eq_right [simp]: 
36409  479 
"a / (b / c) = (a * c) / b" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

480 
by (simp add: divide_inverse ac_simps) 
14288  481 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

482 
lemma divide_divide_eq_left [simp]: 
36409  483 
"(a / b) / c = a / (b * c)" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

484 
by (simp add: divide_inverse mult.assoc) 
14288  485 

56365
713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

486 
lemma divide_divide_times_eq: 
713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

487 
"(x / y) / (z / w) = (x * w) / (y * z)" 
713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

488 
by simp 
23389  489 

60758  490 
text \<open>Special Cancellation Simprules for Division\<close> 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

491 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

492 
lemma mult_divide_mult_cancel_left_if [simp]: 
36409  493 
shows "(c * a) / (c * b) = (if c = 0 then 0 else a / b)" 
60353
838025c6e278
implicit partial divison operation in integral domains
haftmann
parents:
60352
diff
changeset

494 
by simp 
23413
5caa2710dd5b
tuned laws for cancellation in divisions for fields.
nipkow
parents:
23406
diff
changeset

495 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

496 

60758  497 
text \<open>Division and Unary Minus\<close> 
14293  498 

36409  499 
lemma minus_divide_right: 
500 
" (a / b) = a /  b" 

501 
by (simp add: divide_inverse) 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

502 

56479
91958d4b30f7
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents:
56445
diff
changeset

503 
lemma divide_minus_right [simp]: 
36409  504 
"a /  b =  (a / b)" 
505 
by (simp add: divide_inverse) 

30630  506 

56479
91958d4b30f7
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents:
56445
diff
changeset

507 
lemma minus_divide_divide: 
36409  508 
"( a) / ( b) = a / b" 
68527
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
67969
diff
changeset

509 
by (cases "b=0") (simp_all add: nonzero_minus_divide_divide) 
14293  510 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

511 
lemma inverse_eq_1_iff [simp]: 
36409  512 
"inverse x = 1 \<longleftrightarrow> x = 1" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

513 
by (insert inverse_eq_iff_eq [of x 1], simp) 
23389  514 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

515 
lemma divide_eq_0_iff [simp]: 
36409  516 
"a / b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" 
517 
by (simp add: divide_inverse) 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

518 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

519 
lemma divide_cancel_right [simp]: 
36409  520 
"a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b" 
68527
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
67969
diff
changeset

521 
by (cases "c=0") (simp_all add: divide_inverse) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

522 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

523 
lemma divide_cancel_left [simp]: 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

524 
"c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b" 
68527
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
67969
diff
changeset

525 
by (cases "c=0") (simp_all add: divide_inverse) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

526 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

527 
lemma divide_eq_1_iff [simp]: 
36409  528 
"a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b" 
68527
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
67969
diff
changeset

529 
by (cases "b=0") (simp_all add: right_inverse_eq) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

530 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

531 
lemma one_eq_divide_iff [simp]: 
36409  532 
"1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b" 
533 
by (simp add: eq_commute [of 1]) 

534 

65057
799bbbb3a395
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
paulson <lp15@cam.ac.uk>
parents:
64591
diff
changeset

535 
lemma divide_eq_minus_1_iff: 
799bbbb3a395
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
paulson <lp15@cam.ac.uk>
parents:
64591
diff
changeset

536 
"(a / b =  1) \<longleftrightarrow> b \<noteq> 0 \<and> a =  b" 
799bbbb3a395
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
paulson <lp15@cam.ac.uk>
parents:
64591
diff
changeset

537 
using divide_eq_1_iff by fastforce 
799bbbb3a395
Some new lemmas thanks to Lukas Bulwahn. Also, NEWS.
paulson <lp15@cam.ac.uk>
parents:
64591
diff
changeset

538 

36719  539 
lemma times_divide_times_eq: 
540 
"(x / y) * (z / w) = (x * z) / (y * w)" 

541 
by simp 

542 

543 
lemma add_frac_num: 

544 
"y \<noteq> 0 \<Longrightarrow> x / y + z = (x + z * y) / y" 

545 
by (simp add: add_divide_distrib) 

546 

547 
lemma add_num_frac: 

548 
"y \<noteq> 0 \<Longrightarrow> z + x / y = (x + z * y) / y" 

549 
by (simp add: add_divide_distrib add.commute) 

550 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64329
diff
changeset

551 
lemma dvd_field_iff: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64329
diff
changeset

552 
"a dvd b \<longleftrightarrow> (a = 0 \<longrightarrow> b = 0)" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64329
diff
changeset

553 
proof (cases "a = 0") 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64329
diff
changeset

554 
case False 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64329
diff
changeset

555 
then have "b = a * (b / a)" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64329
diff
changeset

556 
by (simp add: field_simps) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64329
diff
changeset

557 
then have "a dvd b" .. 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64329
diff
changeset

558 
with False show ?thesis 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64329
diff
changeset

559 
by simp 
68527
2f4e2aab190a
Generalising and renaming some basic results
paulson <lp15@cam.ac.uk>
parents:
67969
diff
changeset

560 
qed simp 
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64329
diff
changeset

561 

69502  562 
lemma inj_divide_right [simp]: 
563 
"inj (\<lambda>b. b / a) \<longleftrightarrow> a \<noteq> 0" 

564 
proof  

565 
have "(\<lambda>b. b / a) = (*) (inverse a)" 

566 
by (simp add: field_simps fun_eq_iff) 

567 
then have "inj (\<lambda>y. y / a) \<longleftrightarrow> inj ((*) (inverse a))" 

568 
by simp 

569 
also have "\<dots> \<longleftrightarrow> inverse a \<noteq> 0" 

570 
by simp 

571 
also have "\<dots> \<longleftrightarrow> a \<noteq> 0" 

572 
by simp 

573 
finally show ?thesis 

574 
by simp 

575 
qed 

576 

36409  577 
end 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

578 

62481
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

579 
class field_char_0 = field + ring_char_0 
b5d8e57826df
tuned bootstrap order to provide type classes in a more sensible order
haftmann
parents:
62347
diff
changeset

580 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

581 

60758  582 
subsection \<open>Ordered fields\<close> 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

583 

64290  584 
class field_abs_sgn = field + idom_abs_sgn 
585 
begin 

586 

587 
lemma sgn_inverse [simp]: 

588 
"sgn (inverse a) = inverse (sgn a)" 

589 
proof (cases "a = 0") 

590 
case True then show ?thesis by simp 

591 
next 

592 
case False 

593 
then have "a * inverse a = 1" 

594 
by simp 

595 
then have "sgn (a * inverse a) = sgn 1" 

596 
by simp 

597 
then have "sgn a * sgn (inverse a) = 1" 

598 
by (simp add: sgn_mult) 

599 
then have "inverse (sgn a) * (sgn a * sgn (inverse a)) = inverse (sgn a) * 1" 

600 
by simp 

601 
then have "(inverse (sgn a) * sgn a) * sgn (inverse a) = inverse (sgn a)" 

602 
by (simp add: ac_simps) 

603 
with False show ?thesis 

604 
by (simp add: sgn_eq_0_iff) 

605 
qed 

606 

607 
lemma abs_inverse [simp]: 

608 
"\<bar>inverse a\<bar> = inverse \<bar>a\<bar>" 

609 
proof  

610 
from sgn_mult_abs [of "inverse a"] sgn_mult_abs [of a] 

611 
have "inverse (sgn a) * \<bar>inverse a\<bar> = inverse (sgn a * \<bar>a\<bar>)" 

612 
by simp 

613 
then show ?thesis by (auto simp add: sgn_eq_0_iff) 

614 
qed 

615 

616 
lemma sgn_divide [simp]: 

617 
"sgn (a / b) = sgn a / sgn b" 

618 
unfolding divide_inverse sgn_mult by simp 

619 

620 
lemma abs_divide [simp]: 

621 
"\<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>" 

622 
unfolding divide_inverse abs_mult by simp 

623 

624 
end 

625 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

626 
class linordered_field = field + linordered_idom 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

627 
begin 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

628 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

629 
lemma positive_imp_inverse_positive: 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

630 
assumes a_gt_0: "0 < a" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

631 
shows "0 < inverse a" 
23482  632 
proof  
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

633 
have "0 < a * inverse a" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

634 
by (simp add: a_gt_0 [THEN less_imp_not_eq2]) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

635 
thus "0 < inverse a" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

636 
by (simp add: a_gt_0 [THEN less_not_sym] zero_less_mult_iff) 
23482  637 
qed 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

638 

14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

639 
lemma negative_imp_inverse_negative: 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

640 
"a < 0 \<Longrightarrow> inverse a < 0" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

641 
by (insert positive_imp_inverse_positive [of "a"], 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

642 
simp add: nonzero_inverse_minus_eq less_imp_not_eq) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

643 

5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

644 
lemma inverse_le_imp_le: 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

645 
assumes invle: "inverse a \<le> inverse b" and apos: "0 < a" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

646 
shows "b \<le> a" 
23482  647 
proof (rule classical) 
67091  648 
assume "\<not> b \<le> a" 
23482  649 
hence "a < b" by (simp add: linorder_not_le) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

650 
hence bpos: "0 < b" by (blast intro: apos less_trans) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

651 
hence "a * inverse a \<le> a * inverse b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

652 
by (simp add: apos invle less_imp_le mult_left_mono) 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

653 
hence "(a * inverse a) * b \<le> (a * inverse b) * b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

654 
by (simp add: bpos less_imp_le mult_right_mono) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

655 
thus "b \<le> a" by (simp add: mult.assoc apos bpos less_imp_not_eq2) 
23482  656 
qed 
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
14267
diff
changeset

657 

14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

658 
lemma inverse_positive_imp_positive: 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

659 
assumes inv_gt_0: "0 < inverse a" and nz: "a \<noteq> 0" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

660 
shows "0 < a" 
23389  661 
proof  
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

662 
have "0 < inverse (inverse a)" 
23389  663 
using inv_gt_0 by (rule positive_imp_inverse_positive) 
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

664 
thus "0 < a" 
23389  665 
using nz by (simp add: nonzero_inverse_inverse_eq) 
666 
qed 

14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

667 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

668 
lemma inverse_negative_imp_negative: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

669 
assumes inv_less_0: "inverse a < 0" and nz: "a \<noteq> 0" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

670 
shows "a < 0" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

671 
proof  
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

672 
have "inverse (inverse a) < 0" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

673 
using inv_less_0 by (rule negative_imp_inverse_negative) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

674 
thus "a < 0" using nz by (simp add: nonzero_inverse_inverse_eq) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

675 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

676 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

677 
lemma linordered_field_no_lb: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

678 
"\<forall>x. \<exists>y. y < x" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

679 
proof 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

680 
fix x::'a 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

681 
have m1: " (1::'a) < 0" by simp 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

682 
from add_strict_right_mono[OF m1, where c=x] 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

683 
have "( 1) + x < x" by simp 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

684 
thus "\<exists>y. y < x" by blast 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

685 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

686 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

687 
lemma linordered_field_no_ub: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

688 
"\<forall> x. \<exists>y. y > x" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

689 
proof 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

690 
fix x::'a 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

691 
have m1: " (1::'a) > 0" by simp 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

692 
from add_strict_right_mono[OF m1, where c=x] 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

693 
have "1 + x > x" by simp 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

694 
thus "\<exists>y. y > x" by blast 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

695 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

696 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

697 
lemma less_imp_inverse_less: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

698 
assumes less: "a < b" and apos: "0 < a" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

699 
shows "inverse b < inverse a" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

700 
proof (rule ccontr) 
67091  701 
assume "\<not> inverse b < inverse a" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

702 
hence "inverse a \<le> inverse b" by simp 
67091  703 
hence "\<not> (a < b)" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

704 
by (simp add: not_less inverse_le_imp_le [OF _ apos]) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

705 
thus False by (rule notE [OF _ less]) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

706 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

707 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

708 
lemma inverse_less_imp_less: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

709 
"inverse a < inverse b \<Longrightarrow> 0 < a \<Longrightarrow> b < a" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

710 
apply (simp add: less_le [of "inverse a"] less_le [of "b"]) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

711 
apply (force dest!: inverse_le_imp_le nonzero_inverse_eq_imp_eq) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

712 
done 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

713 

60758  714 
text\<open>Both premises are essential. Consider 1 and 1.\<close> 
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

715 
lemma inverse_less_iff_less [simp]: 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

716 
"0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

717 
by (blast intro: less_imp_inverse_less dest: inverse_less_imp_less) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

718 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

719 
lemma le_imp_inverse_le: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

720 
"a \<le> b \<Longrightarrow> 0 < a \<Longrightarrow> inverse b \<le> inverse a" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

721 
by (force simp add: le_less less_imp_inverse_less) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

722 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

723 
lemma inverse_le_iff_le [simp]: 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

724 
"0 < a \<Longrightarrow> 0 < b \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

725 
by (blast intro: le_imp_inverse_le dest: inverse_le_imp_le) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

726 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

727 

60758  728 
text\<open>These results refer to both operands being negative. The oppositesign 
729 
case is trivial, since inverse preserves signs.\<close> 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

730 
lemma inverse_le_imp_le_neg: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

731 
"inverse a \<le> inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b \<le> a" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

732 
apply (rule classical) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

733 
apply (subgoal_tac "a < 0") 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

734 
prefer 2 apply force 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

735 
apply (insert inverse_le_imp_le [of "b" "a"]) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

736 
apply (simp add: nonzero_inverse_minus_eq) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

737 
done 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

738 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

739 
lemma less_imp_inverse_less_neg: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

740 
"a < b \<Longrightarrow> b < 0 \<Longrightarrow> inverse b < inverse a" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

741 
apply (subgoal_tac "a < 0") 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

742 
prefer 2 apply (blast intro: less_trans) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

743 
apply (insert less_imp_inverse_less [of "b" "a"]) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

744 
apply (simp add: nonzero_inverse_minus_eq) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

745 
done 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

746 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

747 
lemma inverse_less_imp_less_neg: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

748 
"inverse a < inverse b \<Longrightarrow> b < 0 \<Longrightarrow> b < a" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

749 
apply (rule classical) 
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

750 
apply (subgoal_tac "a < 0") 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

751 
prefer 2 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

752 
apply force 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

753 
apply (insert inverse_less_imp_less [of "b" "a"]) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

754 
apply (simp add: nonzero_inverse_minus_eq) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

755 
done 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

756 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

757 
lemma inverse_less_iff_less_neg [simp]: 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

758 
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a < inverse b \<longleftrightarrow> b < a" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

759 
apply (insert inverse_less_iff_less [of "b" "a"]) 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

760 
apply (simp del: inverse_less_iff_less 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

761 
add: nonzero_inverse_minus_eq) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

762 
done 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

763 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

764 
lemma le_imp_inverse_le_neg: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

765 
"a \<le> b \<Longrightarrow> b < 0 ==> inverse b \<le> inverse a" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

766 
by (force simp add: le_less less_imp_inverse_less_neg) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

767 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

768 
lemma inverse_le_iff_le_neg [simp]: 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

769 
"a < 0 \<Longrightarrow> b < 0 \<Longrightarrow> inverse a \<le> inverse b \<longleftrightarrow> b \<le> a" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

770 
by (blast intro: le_imp_inverse_le_neg dest: inverse_le_imp_le_neg) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

771 

36774  772 
lemma one_less_inverse: 
773 
"0 < a \<Longrightarrow> a < 1 \<Longrightarrow> 1 < inverse a" 

774 
using less_imp_inverse_less [of a 1, unfolded inverse_1] . 

775 

776 
lemma one_le_inverse: 

777 
"0 < a \<Longrightarrow> a \<le> 1 \<Longrightarrow> 1 \<le> inverse a" 

778 
using le_imp_inverse_le [of a 1, unfolded inverse_1] . 

779 

59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

780 
lemma pos_le_divide_eq [field_simps]: 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

781 
assumes "0 < c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

782 
shows "a \<le> b / c \<longleftrightarrow> a * c \<le> b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

783 
proof  
59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

784 
from assms have "a \<le> b / c \<longleftrightarrow> a * c \<le> (b / c) * c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

785 
using mult_le_cancel_right [of a c "b * inverse c"] by (auto simp add: field_simps) 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

786 
also have "... \<longleftrightarrow> a * c \<le> b" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

787 
by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

788 
finally show ?thesis . 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

789 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

790 

59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

791 
lemma pos_less_divide_eq [field_simps]: 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

792 
assumes "0 < c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

793 
shows "a < b / c \<longleftrightarrow> a * c < b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

794 
proof  
59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

795 
from assms have "a < b / c \<longleftrightarrow> a * c < (b / c) * c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

796 
using mult_less_cancel_right [of a c "b / c"] by auto 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

797 
also have "... = (a*c < b)" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

798 
by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

799 
finally show ?thesis . 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

800 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

801 

59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

802 
lemma neg_less_divide_eq [field_simps]: 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

803 
assumes "c < 0" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

804 
shows "a < b / c \<longleftrightarrow> b < a * c" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

805 
proof  
59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

806 
from assms have "a < b / c \<longleftrightarrow> (b / c) * c < a * c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

807 
using mult_less_cancel_right [of "b / c" c a] by auto 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

808 
also have "... \<longleftrightarrow> b < a * c" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

809 
by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

810 
finally show ?thesis . 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

811 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

812 

59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

813 
lemma neg_le_divide_eq [field_simps]: 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

814 
assumes "c < 0" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

815 
shows "a \<le> b / c \<longleftrightarrow> b \<le> a * c" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

816 
proof  
59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

817 
from assms have "a \<le> b / c \<longleftrightarrow> (b / c) * c \<le> a * c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

818 
using mult_le_cancel_right [of "b * inverse c" c a] by (auto simp add: field_simps) 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

819 
also have "... \<longleftrightarrow> b \<le> a * c" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

820 
by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

821 
finally show ?thesis . 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

822 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

823 

59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

824 
lemma pos_divide_le_eq [field_simps]: 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

825 
assumes "0 < c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

826 
shows "b / c \<le> a \<longleftrightarrow> b \<le> a * c" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

827 
proof  
59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

828 
from assms have "b / c \<le> a \<longleftrightarrow> (b / c) * c \<le> a * c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

829 
using mult_le_cancel_right [of "b / c" c a] by auto 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

830 
also have "... \<longleftrightarrow> b \<le> a * c" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

831 
by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

832 
finally show ?thesis . 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

833 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

834 

59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

835 
lemma pos_divide_less_eq [field_simps]: 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

836 
assumes "0 < c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

837 
shows "b / c < a \<longleftrightarrow> b < a * c" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

838 
proof  
59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

839 
from assms have "b / c < a \<longleftrightarrow> (b / c) * c < a * c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

840 
using mult_less_cancel_right [of "b / c" c a] by auto 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

841 
also have "... \<longleftrightarrow> b < a * c" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

842 
by (simp add: less_imp_not_eq2 [OF assms] divide_inverse mult.assoc) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

843 
finally show ?thesis . 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

844 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

845 

59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

846 
lemma neg_divide_le_eq [field_simps]: 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

847 
assumes "c < 0" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

848 
shows "b / c \<le> a \<longleftrightarrow> a * c \<le> b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

849 
proof  
59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

850 
from assms have "b / c \<le> a \<longleftrightarrow> a * c \<le> (b / c) * c" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

851 
using mult_le_cancel_right [of a c "b / c"] by auto 
59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

852 
also have "... \<longleftrightarrow> a * c \<le> b" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

853 
by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

854 
finally show ?thesis . 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

855 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

856 

59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

857 
lemma neg_divide_less_eq [field_simps]: 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

858 
assumes "c < 0" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

859 
shows "b / c < a \<longleftrightarrow> a * c < b" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

860 
proof  
59546
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

861 
from assms have "b / c < a \<longleftrightarrow> a * c < b / c * c" 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

862 
using mult_less_cancel_right [of a c "b / c"] by auto 
3850a2d20f19
times_divide_eq rules are already [simp] despite of comment
haftmann
parents:
59535
diff
changeset

863 
also have "... \<longleftrightarrow> a * c < b" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

864 
by (simp add: less_imp_not_eq [OF assms] divide_inverse mult.assoc) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

865 
finally show ?thesis . 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

866 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

867 

61799  868 
text\<open>The following \<open>field_simps\<close> rules are necessary, as minus is always moved atop of 
60758  869 
division but we want to get rid of division.\<close> 
56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

870 

093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

871 
lemma pos_le_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a \<le>  (b / c) \<longleftrightarrow> a * c \<le>  b" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

872 
unfolding minus_divide_left by (rule pos_le_divide_eq) 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

873 

093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

874 
lemma neg_le_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a \<le>  (b / c) \<longleftrightarrow>  b \<le> a * c" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

875 
unfolding minus_divide_left by (rule neg_le_divide_eq) 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

876 

093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

877 
lemma pos_less_minus_divide_eq [field_simps]: "0 < c \<Longrightarrow> a <  (b / c) \<longleftrightarrow> a * c <  b" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

878 
unfolding minus_divide_left by (rule pos_less_divide_eq) 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

879 

093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

880 
lemma neg_less_minus_divide_eq [field_simps]: "c < 0 \<Longrightarrow> a <  (b / c) \<longleftrightarrow>  b < a * c" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

881 
unfolding minus_divide_left by (rule neg_less_divide_eq) 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

882 

093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

883 
lemma pos_minus_divide_less_eq [field_simps]: "0 < c \<Longrightarrow>  (b / c) < a \<longleftrightarrow>  b < a * c" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

884 
unfolding minus_divide_left by (rule pos_divide_less_eq) 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

885 

093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

886 
lemma neg_minus_divide_less_eq [field_simps]: "c < 0 \<Longrightarrow>  (b / c) < a \<longleftrightarrow> a * c <  b" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

887 
unfolding minus_divide_left by (rule neg_divide_less_eq) 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

888 

093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

889 
lemma pos_minus_divide_le_eq [field_simps]: "0 < c \<Longrightarrow>  (b / c) \<le> a \<longleftrightarrow>  b \<le> a * c" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

890 
unfolding minus_divide_left by (rule pos_divide_le_eq) 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

891 

093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

892 
lemma neg_minus_divide_le_eq [field_simps]: "c < 0 \<Longrightarrow>  (b / c) \<le> a \<longleftrightarrow> a * c \<le>  b" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

893 
unfolding minus_divide_left by (rule neg_divide_le_eq) 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

894 

56365
713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

895 
lemma frac_less_eq: 
713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

896 
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y < w / z \<longleftrightarrow> (x * z  w * y) / (y * z) < 0" 
713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

897 
by (subst less_iff_diff_less_0) (simp add: diff_frac_eq ) 
713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

898 

713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

899 
lemma frac_le_eq: 
713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

900 
"y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y \<le> w / z \<longleftrightarrow> (x * z  w * y) / (y * z) \<le> 0" 
713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

901 
by (subst le_iff_diff_le_0) (simp add: diff_frac_eq ) 
713f9b9a7e51
New theorems for extracting quotients
paulson <lp15@cam.ac.uk>
parents:
55718
diff
changeset

902 

56541  903 
lemma divide_pos_pos[simp]: 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

904 
"0 < x ==> 0 < y ==> 0 < x / y" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

905 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

906 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

907 
lemma divide_nonneg_pos: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

908 
"0 <= x ==> 0 < y ==> 0 <= x / y" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

909 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

910 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

911 
lemma divide_neg_pos: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

912 
"x < 0 ==> 0 < y ==> x / y < 0" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

913 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

914 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

915 
lemma divide_nonpos_pos: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

916 
"x <= 0 ==> 0 < y ==> x / y <= 0" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

917 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

918 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

919 
lemma divide_pos_neg: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

920 
"0 < x ==> y < 0 ==> x / y < 0" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

921 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

922 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

923 
lemma divide_nonneg_neg: 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

924 
"0 <= x ==> y < 0 ==> x / y <= 0" 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

925 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

926 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

927 
lemma divide_neg_neg: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

928 
"x < 0 ==> y < 0 ==> 0 < x / y" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

929 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

930 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

931 
lemma divide_nonpos_neg: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

932 
"x <= 0 ==> y < 0 ==> 0 <= x / y" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

933 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

934 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

935 
lemma divide_strict_right_mono: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

936 
"[a < b; 0 < c] ==> a / c < b / c" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

937 
by (simp add: less_imp_not_eq2 divide_inverse mult_strict_right_mono 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

938 
positive_imp_inverse_positive) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

939 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

940 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

941 
lemma divide_strict_right_mono_neg: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

942 
"[b < a; c < 0] ==> a / c < b / c" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

943 
apply (drule divide_strict_right_mono [of _ _ "c"], simp) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

944 
apply (simp add: less_imp_not_eq nonzero_minus_divide_right [symmetric]) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

945 
done 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

946 

69593  947 
text\<open>The last premise ensures that \<^term>\<open>a\<close> and \<^term>\<open>b\<close> 
60758  948 
have the same sign\<close> 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

949 
lemma divide_strict_left_mono: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

950 
"[b < a; 0 < c; 0 < a*b] ==> c / a < c / b" 
44921  951 
by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

952 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

953 
lemma divide_left_mono: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

954 
"[b \<le> a; 0 \<le> c; 0 < a*b] ==> c / a \<le> c / b" 
44921  955 
by (auto simp: field_simps zero_less_mult_iff mult_right_mono) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

956 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

957 
lemma divide_strict_left_mono_neg: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

958 
"[a < b; c < 0; 0 < a*b] ==> c / a < c / b" 
44921  959 
by (auto simp: field_simps zero_less_mult_iff mult_strict_right_mono_neg) 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

960 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

961 
lemma mult_imp_div_pos_le: "0 < y ==> x <= z * y ==> 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

962 
x / y <= z" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

963 
by (subst pos_divide_le_eq, assumption+) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

964 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

965 
lemma mult_imp_le_div_pos: "0 < y ==> z * y <= x ==> 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

966 
z <= x / y" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

967 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

968 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

969 
lemma mult_imp_div_pos_less: "0 < y ==> x < z * y ==> 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

970 
x / y < z" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

971 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

972 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

973 
lemma mult_imp_less_div_pos: "0 < y ==> z * y < x ==> 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

974 
z < x / y" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

975 
by(simp add:field_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

976 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

977 
lemma frac_le: "0 <= x ==> 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

978 
x <= y ==> 0 < w ==> w <= z ==> x / z <= y / w" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

979 
apply (rule mult_imp_div_pos_le) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

980 
apply simp 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

981 
apply (subst times_divide_eq_left) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

982 
apply (rule mult_imp_le_div_pos, assumption) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

983 
apply (rule mult_mono) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

984 
apply simp_all 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

985 
done 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

986 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

987 
lemma frac_less: "0 <= x ==> 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

988 
x < y ==> 0 < w ==> w <= z ==> x / z < y / w" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

989 
apply (rule mult_imp_div_pos_less) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

990 
apply simp 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

991 
apply (subst times_divide_eq_left) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

992 
apply (rule mult_imp_less_div_pos, assumption) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

993 
apply (erule mult_less_le_imp_less) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

994 
apply simp_all 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

995 
done 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

996 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

997 
lemma frac_less2: "0 < x ==> 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

998 
x <= y ==> 0 < w ==> w < z ==> x / z < y / w" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

999 
apply (rule mult_imp_div_pos_less) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1000 
apply simp_all 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1001 
apply (rule mult_imp_less_div_pos, assumption) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1002 
apply (erule mult_le_less_imp_less) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1003 
apply simp_all 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1004 
done 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1005 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1006 
lemma less_half_sum: "a < b ==> a < (a+b) / (1+1)" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1007 
by (simp add: field_simps zero_less_two) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1008 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1009 
lemma gt_half_sum: "a < b ==> (a+b)/(1+1) < b" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1010 
by (simp add: field_simps zero_less_two) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1011 

53215
5e47c31c6f7c
renamed typeclass dense_linorder to unbounded_dense_linorder
hoelzl
parents:
52435
diff
changeset

1012 
subclass unbounded_dense_linorder 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1013 
proof 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1014 
fix x y :: 'a 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

1015 
from less_add_one show "\<exists>y. x < y" .. 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1016 
from less_add_one have "x + ( 1) < (x + 1) + ( 1)" by (rule add_strict_right_mono) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54147
diff
changeset

1017 
then have "x  1 < x + 1  1" by simp 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1018 
then have "x  1 < x" by (simp add: algebra_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1019 
then show "\<exists>y. y < x" .. 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1020 
show "x < y \<Longrightarrow> \<exists>z>x. z < y" by (blast intro!: less_half_sum gt_half_sum) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1021 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1022 

64290  1023 
subclass field_abs_sgn .. 
1024 

64329  1025 
lemma inverse_sgn [simp]: 
1026 
"inverse (sgn a) = sgn a" 

1027 
by (cases a 0 rule: linorder_cases) simp_all 

1028 

1029 
lemma divide_sgn [simp]: 

1030 
"a / sgn b = a * sgn b" 

1031 
by (cases b 0 rule: linorder_cases) simp_all 

1032 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1033 
lemma nonzero_abs_inverse: 
64290  1034 
"a \<noteq> 0 ==> \<bar>inverse a\<bar> = inverse \<bar>a\<bar>" 
1035 
by (rule abs_inverse) 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1036 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1037 
lemma nonzero_abs_divide: 
64290  1038 
"b \<noteq> 0 ==> \<bar>a / b\<bar> = \<bar>a\<bar> / \<bar>b\<bar>" 
1039 
by (rule abs_divide) 

36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1040 

72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1041 
lemma field_le_epsilon: 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1042 
assumes e: "\<And>e. 0 < e \<Longrightarrow> x \<le> y + e" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1043 
shows "x \<le> y" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1044 
proof (rule dense_le) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1045 
fix t assume "t < x" 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1046 
hence "0 < x  t" by (simp add: less_diff_eq) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1047 
from e [OF this] have "x + 0 \<le> x + (y  t)" by (simp add: algebra_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1048 
then have "0 \<le> y  t" by (simp only: add_le_cancel_left) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1049 
then show "t \<le> y" by (simp add: algebra_simps) 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1050 
qed 
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1051 

14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1052 
lemma inverse_positive_iff_positive [simp]: 
36409  1053 
"(0 < inverse a) = (0 < a)" 
21328  1054 
apply (cases "a = 0", simp) 
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1055 
apply (blast intro: inverse_positive_imp_positive positive_imp_inverse_positive) 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1056 
done 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1057 

ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1058 
lemma inverse_negative_iff_negative [simp]: 
36409  1059 
"(inverse a < 0) = (a < 0)" 
21328  1060 
apply (cases "a = 0", simp) 
14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1061 
apply (blast intro: inverse_negative_imp_negative negative_imp_inverse_negative) 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1062 
done 
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1063 

ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1064 
lemma inverse_nonnegative_iff_nonnegative [simp]: 
36409  1065 
"0 \<le> inverse a \<longleftrightarrow> 0 \<le> a" 
1066 
by (simp add: not_less [symmetric]) 

14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1067 

ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1068 
lemma inverse_nonpositive_iff_nonpositive [simp]: 
36409  1069 
"inverse a \<le> 0 \<longleftrightarrow> a \<le> 0" 
1070 
by (simp add: not_less [symmetric]) 

14277
ad66687ece6e
more field division lemmas transferred from Real to Ring_and_Field
paulson
parents:
14272
diff
changeset

1071 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1072 
lemma one_less_inverse_iff: "1 < inverse x \<longleftrightarrow> 0 < x \<and> x < 1" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1073 
using less_trans[of 1 x 0 for x] 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1074 
by (cases x 0 rule: linorder_cases) (auto simp add: field_simps) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

1075 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1076 
lemma one_le_inverse_iff: "1 \<le> inverse x \<longleftrightarrow> 0 < x \<and> x \<le> 1" 
36409  1077 
proof (cases "x = 1") 
1078 
case True then show ?thesis by simp 

1079 
next 

1080 
case False then have "inverse x \<noteq> 1" by simp 

1081 
then have "1 \<noteq> inverse x" by blast 

1082 
then have "1 \<le> inverse x \<longleftrightarrow> 1 < inverse x" by (simp add: le_less) 

1083 
with False show ?thesis by (auto simp add: one_less_inverse_iff) 

1084 
qed 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

1085 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1086 
lemma inverse_less_1_iff: "inverse x < 1 \<longleftrightarrow> x \<le> 0 \<or> 1 < x" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

1087 
by (simp add: not_le [symmetric] one_le_inverse_iff) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

1088 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1089 
lemma inverse_le_1_iff: "inverse x \<le> 1 \<longleftrightarrow> x \<le> 0 \<or> 1 \<le> x" 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

1090 
by (simp add: not_less [symmetric] one_less_inverse_iff) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset

1091 

56481  1092 
lemma [divide_simps]: 
56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1093 
shows le_divide_eq: "a \<le> b / c \<longleftrightarrow> (if 0 < c then a * c \<le> b else if c < 0 then b \<le> a * c else a \<le> 0)" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1094 
and divide_le_eq: "b / c \<le> a \<longleftrightarrow> (if 0 < c then b \<le> a * c else if c < 0 then a * c \<le> b else 0 \<le> a)" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1095 
and less_divide_eq: "a < b / c \<longleftrightarrow> (if 0 < c then a * c < b else if c < 0 then b < a * c else a < 0)" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1096 
and divide_less_eq: "b / c < a \<longleftrightarrow> (if 0 < c then b < a * c else if c < 0 then a * c < b else 0 < a)" 
56481  1097 
and le_minus_divide_eq: "a \<le>  (b / c) \<longleftrightarrow> (if 0 < c then a * c \<le>  b else if c < 0 then  b \<le> a * c else a \<le> 0)" 
1098 
and minus_divide_le_eq: " (b / c) \<le> a \<longleftrightarrow> (if 0 < c then  b \<le> a * c else if c < 0 then a * c \<le>  b else 0 \<le> a)" 

1099 
and less_minus_divide_eq: "a <  (b / c) \<longleftrightarrow> (if 0 < c then a * c <  b else if c < 0 then  b < a * c else a < 0)" 

1100 
and minus_divide_less_eq: " (b / c) < a \<longleftrightarrow> (if 0 < c then  b < a * c else if c < 0 then a * c <  b else 0 < a)" 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1101 
by (auto simp: field_simps not_less dest: antisym) 
14288  1102 

60758  1103 
text \<open>Division and Signs\<close> 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1104 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1105 
lemma 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1106 
shows zero_less_divide_iff: "0 < a / b \<longleftrightarrow> 0 < a \<and> 0 < b \<or> a < 0 \<and> b < 0" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1107 
and divide_less_0_iff: "a / b < 0 \<longleftrightarrow> 0 < a \<and> b < 0 \<or> a < 0 \<and> 0 < b" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1108 
and zero_le_divide_iff: "0 \<le> a / b \<longleftrightarrow> 0 \<le> a \<and> 0 \<le> b \<or> a \<le> 0 \<and> b \<le> 0" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1109 
and divide_le_0_iff: "a / b \<le> 0 \<longleftrightarrow> 0 \<le> a \<and> b \<le> 0 \<or> a \<le> 0 \<and> 0 \<le> b" 
56481  1110 
by (auto simp add: divide_simps) 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1111 

60758  1112 
text \<open>Division and the Number One\<close> 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset

1113 

60758  1114 
text\<open>Simplify expressions equated with 1\<close> 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset

1115 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1116 
lemma zero_eq_1_divide_iff [simp]: "0 = 1 / a \<longleftrightarrow> a = 0" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1117 
by (cases "a = 0") (auto simp: field_simps) 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset

1118 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1119 
lemma one_divide_eq_0_iff [simp]: "1 / a = 0 \<longleftrightarrow> a = 0" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1120 
using zero_eq_1_divide_iff[of a] by simp 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset

1121 

61799  1122 
text\<open>Simplify expressions such as \<open>0 < 1/x\<close> to \<open>0 < x\<close>\<close> 
36423  1123 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1124 
lemma zero_le_divide_1_iff [simp]: 
36423  1125 
"0 \<le> 1 / a \<longleftrightarrow> 0 \<le> a" 
1126 
by (simp add: zero_le_divide_iff) 

17085  1127 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1128 
lemma zero_less_divide_1_iff [simp]: 
36423  1129 
"0 < 1 / a \<longleftrightarrow> 0 < a" 
1130 
by (simp add: zero_less_divide_iff) 

1131 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1132 
lemma divide_le_0_1_iff [simp]: 
36423  1133 
"1 / a \<le> 0 \<longleftrightarrow> a \<le> 0" 
1134 
by (simp add: divide_le_0_iff) 

1135 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1136 
lemma divide_less_0_1_iff [simp]: 
36423  1137 
"1 / a < 0 \<longleftrightarrow> a < 0" 
1138 
by (simp add: divide_less_0_iff) 

14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset

1139 

14293  1140 
lemma divide_right_mono: 
36409  1141 
"[a \<le> b; 0 \<le> c] ==> a/c \<le> b/c" 
1142 
by (force simp add: divide_strict_right_mono le_less) 

14293  1143 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

1144 
lemma divide_right_mono_neg: "a <= b 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1145 
==> c <= 0 ==> b / c <= a / c" 
23482  1146 
apply (drule divide_right_mono [of _ _ " c"]) 
56479
91958d4b30f7
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
hoelzl
parents:
56445
diff
changeset

1147 
apply auto 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1148 
done 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1149 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

1150 
lemma divide_left_mono_neg: "a <= b 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1151 
==> c <= 0 ==> 0 < a * b ==> c / a <= c / b" 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1152 
apply (drule divide_left_mono [of _ _ " c"]) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56571
diff
changeset

1153 
apply (auto simp add: mult.commute) 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1154 
done 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1155 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1156 
lemma inverse_le_iff: "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)" 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1157 
by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases]) 
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1158 
(auto simp add: field_simps zero_less_mult_iff mult_le_0_iff) 
42904  1159 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1160 
lemma inverse_less_iff: "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)" 
42904  1161 
by (subst less_le) (auto simp: inverse_le_iff) 
1162 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1163 
lemma divide_le_cancel: "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)" 
42904  1164 
by (simp add: divide_inverse mult_le_cancel_right) 
1165 

56480
093ea91498e6
field_simps: better support for negation and division, and power
hoelzl
parents:
56479
diff
changeset

1166 
lemma divide_less_cancel: "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0" 
42904  1167 
by (auto simp add: divide_inverse mult_less_cancel_right) 
1168 

60758  1169 
text\<open>Simplify quotients that are compared with the value 1.\<close> 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1170 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1171 
lemma le_divide_eq_1: 
67091  1172 
"(1 \<le> b / a) = ((0 < a \<and> a \<le> b) \<or> (a < 0 \<and> b \<le> a))" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1173 
by (auto simp add: le_divide_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1174 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1175 
lemma divide_le_eq_1: 
67091  1176 
"(b / a \<le> 1) = ((0 < a \<and> b \<le> a) \<or> (a < 0 \<and> a \<le> b) \<or> a=0)" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1177 
by (auto simp add: divide_le_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1178 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1179 
lemma less_divide_eq_1: 
67091  1180 
"(1 < b / a) = ((0 < a \<and> a < b) \<or> (a < 0 \<and> b < a))" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1181 
by (auto simp add: less_divide_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1182 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1183 
lemma divide_less_eq_1: 
67091  1184 
"(b / a < 1) = ((0 < a \<and> b < a) \<or> (a < 0 \<and> a < b) \<or> a=0)" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1185 
by (auto simp add: divide_less_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1186 

56571
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1187 
lemma divide_nonneg_nonneg [simp]: 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1188 
"0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x / y" 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1189 
by (auto simp add: divide_simps) 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1190 

f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1191 
lemma divide_nonpos_nonpos: 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1192 
"x \<le> 0 \<Longrightarrow> y \<le> 0 \<Longrightarrow> 0 \<le> x / y" 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1193 
by (auto simp add: divide_simps) 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1194 

f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1195 
lemma divide_nonneg_nonpos: 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1196 
"0 \<le> x \<Longrightarrow> y \<le> 0 \<Longrightarrow> x / y \<le> 0" 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1197 
by (auto simp add: divide_simps) 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1198 

f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1199 
lemma divide_nonpos_nonneg: 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1200 
"x \<le> 0 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x / y \<le> 0" 
f4635657d66f
added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents:
56541
diff
changeset

1201 
by (auto simp add: divide_simps) 
23389  1202 

60758  1203 
text \<open>Conditional Simplification Rules: No Case Splits\<close> 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1204 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1205 
lemma le_divide_eq_1_pos [simp]: 
36409  1206 
"0 < a \<Longrightarrow> (1 \<le> b/a) = (a \<le> b)" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1207 
by (auto simp add: le_divide_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1208 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1209 
lemma le_divide_eq_1_neg [simp]: 
36409  1210 
"a < 0 \<Longrightarrow> (1 \<le> b/a) = (b \<le> a)" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1211 
by (auto simp add: le_divide_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1212 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1213 
lemma divide_le_eq_1_pos [simp]: 
36409  1214 
"0 < a \<Longrightarrow> (b/a \<le> 1) = (b \<le> a)" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1215 
by (auto simp add: divide_le_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1216 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1217 
lemma divide_le_eq_1_neg [simp]: 
36409  1218 
"a < 0 \<Longrightarrow> (b/a \<le> 1) = (a \<le> b)" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1219 
by (auto simp add: divide_le_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1220 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1221 
lemma less_divide_eq_1_pos [simp]: 
36409  1222 
"0 < a \<Longrightarrow> (1 < b/a) = (a < b)" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1223 
by (auto simp add: less_divide_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1224 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1225 
lemma less_divide_eq_1_neg [simp]: 
36409  1226 
"a < 0 \<Longrightarrow> (1 < b/a) = (b < a)" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1227 
by (auto simp add: less_divide_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1228 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1229 
lemma divide_less_eq_1_pos [simp]: 
36409  1230 
"0 < a \<Longrightarrow> (b/a < 1) = (b < a)" 
18649
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset

1231 
by (auto simp add: divide_less_eq) 
bb99c2e705ca
tidied, and added missing thm divide_less_eq_1_neg
paulson
parents:
18623
diff
changeset

1232 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1233 
lemma divide_less_eq_1_neg [simp]: 
61941  1234 
"a < 0 \<Longrightarrow> b/a < 1 \<longleftrightarrow> a < b" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1235 
by (auto simp add: divide_less_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1236 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1237 
lemma eq_divide_eq_1 [simp]: 
67091  1238 
"(1 = b/a) = ((a \<noteq> 0 \<and> a = b))" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1239 
by (auto simp add: eq_divide_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1240 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

1241 
lemma divide_eq_eq_1 [simp]: 
67091  1242 
"(b/a = 1) = ((a \<noteq> 0 \<and> a = b))" 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1243 
by (auto simp add: divide_eq_eq) 
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1244 

59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
59557
diff
changeset

1245 
lemma abs_div_pos: "0 < y ==> 
36301
72f4d079ebf8
more localization; factored out lemmas for division_ring
haftmann
parents:
35828
diff
changeset

1246 
\<bar>x\<bar> / y = \<bar>x / y\<bar>" 
25304
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1247 
apply (subst abs_divide) 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1248 
apply (simp add: order_less_imp_le) 
7491c00f0915
removed subclass edge ordered_ring < lordered_ring
haftmann
parents:
25267
diff
changeset

1249 
done 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16568
diff
changeset

1250 

67091  1251 
lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / \<bar>b\<bar>) = (0 \<le> a \<or> b = 0)" 
55718
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
54230
diff
changeset

1252 
by (auto simp: zero_le_divide_iff) 
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
54230
diff
changeset

1253 

67091  1254 
lemma divide_le_0_abs_iff [simp]: "(a / \<bar>b\<bar> \<le> 0) = (a \<le> 0 \<or> b = 0)" 
55718
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
54230
diff
changeset

1255 
by (auto simp: divide_le_0_iff) 
34618f031ba9
A few lemmas about summations, etc.
paulson <lp15@cam.ac.uk>
parents:
54230
diff
changeset

1256 

35579
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35216
diff
changeset

1257 
lemma field_le_mult_one_interval: 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35216
diff
changeset

1258 
assumes *: "\<And>z. \<lbrakk> 0 < z ; z < 1 \<rbrakk> \<Longrightarrow> z * x \<le> y" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35216
diff
changeset

1259 
shows "x \<le> y" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35216
diff
changeset

1260 
proof (cases "0 < x") 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35216
diff
changeset

1261 
assume "0 < x" 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35216
diff
changeset

1262 
thus ?thesis 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35216
diff
changeset

1263 
using dense_le_bounded[of 0 1 "y/x"] * 
60758  1264 
unfolding le_divide_eq if_P[OF \<open>0 < x\<close>] by simp 
35579
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35216
diff
changeset

1265 
next 
cc9a5a0ab5ea
Add dense_le, dense_le_bounded, field_le_mult_one_interval.
hoelzl
parents:
35216
diff
changeset

1266 
assume "\<not>0 < x" hence "x \<le> 0" by simp 
61076  1267 
obtain s::'a where s: "0 < s" "s < 1" using dense[of 0 "1::'a"] by auto 