author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45548  3e2722d66169 
child 48556  62a3fbf9d35b 
permissions  rwrr 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35036
diff
changeset

1 
(* Title: HOL/Groups.thy 
29269
5c25a2012975
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
28823
diff
changeset

2 
Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad 
14738  3 
*) 
4 

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

5 
header {* Groups, also combined with orderings *} 
14738  6 

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

7 
theory Groups 
35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

8 
imports Orderings 
37986
3b3187adf292
use file names relative to master directory of theory source  Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);
wenzelm
parents:
37889
diff
changeset

9 
uses ("Tools/abel_cancel.ML") 
15131  10 
begin 
14738  11 

35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

12 
subsection {* Fact collections *} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

13 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

14 
ML {* 
45294  15 
structure Ac_Simps = Named_Thms 
16 
( 

17 
val name = @{binding ac_simps} 

36343  18 
val description = "associativity and commutativity simplification rules" 
19 
) 

20 
*} 

21 

22 
setup Ac_Simps.setup 

23 

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

24 
text{* The rewrites accumulated in @{text algebra_simps} deal with the 
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

25 
classical algebraic structures of groups, rings and family. They simplify 
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

26 
terms by multiplying everything out (in case of a ring) and bringing sums and 
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

27 
products into a canonical form (by ordered rewriting). As a result it decides 
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

28 
group and ring equalities but also helps with inequalities. 
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

29 

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

30 
Of course it also works for fields, but it knows nothing about multiplicative 
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

31 
inverses or division. This is catered for by @{text 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

32 

36343  33 
ML {* 
45294  34 
structure Algebra_Simps = Named_Thms 
35 
( 

36 
val name = @{binding algebra_simps} 

35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

37 
val description = "algebra simplification rules" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

38 
) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

39 
*} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

40 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

41 
setup Algebra_Simps.setup 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

42 

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

43 
text{* Lemmas @{text field_simps} multiply with denominators in (in)equations 
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

44 
if they can be proved to be nonzero (for equations) or positive/negative 
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

45 
(for inequations). Can be too aggressive and is therefore separate from the 
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

46 
more benign @{text algebra_simps}. *} 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

47 

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

48 
ML {* 
45294  49 
structure Field_Simps = Named_Thms 
50 
( 

51 
val name = @{binding field_simps} 

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

52 
val description = "algebra simplification rules for fields" 
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

53 
) 
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

54 
*} 
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

55 

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

56 
setup Field_Simps.setup 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

57 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

58 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

59 
subsection {* Abstract structures *} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

60 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

61 
text {* 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

62 
These locales provide basic structures for interpretation into 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

63 
bigger structures; extensions require careful thinking, otherwise 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

64 
undesired effects may occur due to interpretation. 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

65 
*} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

66 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

67 
locale semigroup = 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

68 
fixes f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

69 
assumes assoc [ac_simps]: "a * b * c = a * (b * c)" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

70 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

71 
locale abel_semigroup = semigroup + 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

72 
assumes commute [ac_simps]: "a * b = b * a" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

73 
begin 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

74 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

75 
lemma left_commute [ac_simps]: 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

76 
"b * (a * c) = a * (b * c)" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

77 
proof  
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

78 
have "(b * a) * c = (a * b) * c" 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

79 
by (simp only: commute) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

80 
then show ?thesis 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

81 
by (simp only: assoc) 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

82 
qed 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

83 

90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

84 
end 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

85 

35720  86 
locale monoid = semigroup + 
35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

87 
fixes z :: 'a ("1") 
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

88 
assumes left_neutral [simp]: "1 * a = a" 
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

89 
assumes right_neutral [simp]: "a * 1 = a" 
35720  90 

91 
locale comm_monoid = abel_semigroup + 

35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

92 
fixes z :: 'a ("1") 
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

93 
assumes comm_neutral: "a * 1 = a" 
35720  94 

95 
sublocale comm_monoid < monoid proof 

96 
qed (simp_all add: commute comm_neutral) 

97 

35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

98 

35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

99 
subsection {* Generic operations *} 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

100 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

101 
class zero = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

102 
fixes zero :: 'a ("0") 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

103 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

104 
class one = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

105 
fixes one :: 'a ("1") 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

106 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
35828
diff
changeset

107 
hide_const (open) zero one 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

108 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

109 
lemma Let_0 [simp]: "Let 0 f = f 0" 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

110 
unfolding Let_def .. 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

111 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

112 
lemma Let_1 [simp]: "Let 1 f = f 1" 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

113 
unfolding Let_def .. 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

114 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

115 
setup {* 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

116 
Reorient_Proc.add 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

117 
(fn Const(@{const_name Groups.zero}, _) => true 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

118 
 Const(@{const_name Groups.one}, _) => true 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

119 
 _ => false) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

120 
*} 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

121 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

122 
simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

123 
simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

124 

39134
917b4b6ba3d2
turned show_sorts/show_types into proper configuration options;
wenzelm
parents:
37986
diff
changeset

125 
typed_print_translation (advanced) {* 
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

126 
let 
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

127 
fun tr' c = (c, fn ctxt => fn T => fn ts => 
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

128 
if not (null ts) orelse T = dummyT 
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

129 
orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T 
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

130 
then raise Match 
42248  131 
else 
132 
Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $ 

133 
Syntax_Phases.term_of_typ ctxt T); 

42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

134 
in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end; 
35267
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

135 
*}  {* show types that are presumably too general *} 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

136 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

137 
class plus = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

138 
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

139 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

140 
class minus = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

141 
fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "" 65) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

142 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

143 
class uminus = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

144 
fixes uminus :: "'a \<Rightarrow> 'a" (" _" [81] 80) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

145 

8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

146 
class times = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

147 
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70) 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

148 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

149 

23085  150 
subsection {* Semigroups and Monoids *} 
14738  151 

22390  152 
class semigroup_add = plus + 
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

153 
assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)" 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

154 

35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

155 
sublocale semigroup_add < add!: semigroup plus proof 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

156 
qed (fact add_assoc) 
22390  157 

158 
class ab_semigroup_add = semigroup_add + 

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

159 
assumes add_commute [algebra_simps, field_simps]: "a + b = b + a" 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

160 

35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

161 
sublocale ab_semigroup_add < add!: abel_semigroup plus proof 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

162 
qed (fact add_commute) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

163 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

164 
context ab_semigroup_add 
25062  165 
begin 
14738  166 

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

167 
lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute 
25062  168 

169 
theorems add_ac = add_assoc add_commute add_left_commute 

170 

171 
end 

14738  172 

173 
theorems add_ac = add_assoc add_commute add_left_commute 

174 

22390  175 
class semigroup_mult = times + 
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

176 
assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

177 

35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

178 
sublocale semigroup_mult < mult!: semigroup times proof 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

179 
qed (fact mult_assoc) 
14738  180 

22390  181 
class ab_semigroup_mult = semigroup_mult + 
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

182 
assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a" 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

183 

35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

184 
sublocale ab_semigroup_mult < mult!: abel_semigroup times proof 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

185 
qed (fact mult_commute) 
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

186 

ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

187 
context ab_semigroup_mult 
23181  188 
begin 
14738  189 

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

190 
lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute 
25062  191 

192 
theorems mult_ac = mult_assoc mult_commute mult_left_commute 

23181  193 

194 
end 

14738  195 

196 
theorems mult_ac = mult_assoc mult_commute mult_left_commute 

197 

23085  198 
class monoid_add = zero + semigroup_add + 
35720  199 
assumes add_0_left: "0 + a = a" 
200 
and add_0_right: "a + 0 = a" 

201 

35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

202 
sublocale monoid_add < add!: monoid plus 0 proof 
35720  203 
qed (fact add_0_left add_0_right)+ 
23085  204 

26071  205 
lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0" 
29667  206 
by (rule eq_commute) 
26071  207 

22390  208 
class comm_monoid_add = zero + ab_semigroup_add + 
25062  209 
assumes add_0: "0 + a = a" 
23085  210 

35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

211 
sublocale comm_monoid_add < add!: comm_monoid plus 0 proof 
35720  212 
qed (insert add_0, simp add: ac_simps) 
25062  213 

35720  214 
subclass (in comm_monoid_add) monoid_add proof 
35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

215 
qed (fact add.left_neutral add.right_neutral)+ 
14738  216 

22390  217 
class monoid_mult = one + semigroup_mult + 
35720  218 
assumes mult_1_left: "1 * a = a" 
219 
and mult_1_right: "a * 1 = a" 

220 

35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

221 
sublocale monoid_mult < mult!: monoid times 1 proof 
35720  222 
qed (fact mult_1_left mult_1_right)+ 
14738  223 

26071  224 
lemma one_reorient: "1 = x \<longleftrightarrow> x = 1" 
29667  225 
by (rule eq_commute) 
26071  226 

22390  227 
class comm_monoid_mult = one + ab_semigroup_mult + 
25062  228 
assumes mult_1: "1 * a = a" 
14738  229 

35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

230 
sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof 
35720  231 
qed (insert mult_1, simp add: ac_simps) 
25062  232 

35720  233 
subclass (in comm_monoid_mult) monoid_mult proof 
35723
b6cf98f25c3f
tuned monoid locales and prefix of sublocale interpretations
haftmann
parents:
35720
diff
changeset

234 
qed (fact mult.left_neutral mult.right_neutral)+ 
14738  235 

22390  236 
class cancel_semigroup_add = semigroup_add + 
25062  237 
assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" 
238 
assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c" 

27474
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

239 
begin 
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

240 

a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

241 
lemma add_left_cancel [simp]: 
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

242 
"a + b = a + c \<longleftrightarrow> b = c" 
29667  243 
by (blast dest: add_left_imp_eq) 
27474
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

244 

a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

245 
lemma add_right_cancel [simp]: 
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

246 
"b + a = c + a \<longleftrightarrow> b = c" 
29667  247 
by (blast dest: add_right_imp_eq) 
27474
a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

248 

a89d755b029d
move proofs of add_left_cancel and add_right_cancel into the correct locale
huffman
parents:
27250
diff
changeset

249 
end 
14738  250 

22390  251 
class cancel_ab_semigroup_add = ab_semigroup_add + 
25062  252 
assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c" 
25267  253 
begin 
14738  254 

25267  255 
subclass cancel_semigroup_add 
28823  256 
proof 
22390  257 
fix a b c :: 'a 
258 
assume "a + b = a + c" 

259 
then show "b = c" by (rule add_imp_eq) 

260 
next 

14738  261 
fix a b c :: 'a 
262 
assume "b + a = c + a" 

22390  263 
then have "a + b = a + c" by (simp only: add_commute) 
264 
then show "b = c" by (rule add_imp_eq) 

14738  265 
qed 
266 

25267  267 
end 
268 

29904  269 
class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add 
270 

271 

23085  272 
subsection {* Groups *} 
273 

25762  274 
class group_add = minus + uminus + monoid_add + 
25062  275 
assumes left_minus [simp]: " a + a = 0" 
276 
assumes diff_minus: "a  b = a + ( b)" 

277 
begin 

23085  278 

34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

279 
lemma minus_unique: 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

280 
assumes "a + b = 0" shows " a = b" 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

281 
proof  
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

282 
have " a =  a + (a + b)" using assms by simp 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

283 
also have "\<dots> = b" by (simp add: add_assoc [symmetric]) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

284 
finally show ?thesis . 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

285 
qed 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

286 

319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

287 
lemmas equals_zero_I = minus_unique (* legacy name *) 
14738  288 

25062  289 
lemma minus_zero [simp]: " 0 = 0" 
14738  290 
proof  
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

291 
have "0 + 0 = 0" by (rule add_0_right) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

292 
thus " 0 = 0" by (rule minus_unique) 
14738  293 
qed 
294 

25062  295 
lemma minus_minus [simp]: " ( a) = a" 
23085  296 
proof  
34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

297 
have " a + a = 0" by (rule left_minus) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

298 
thus " ( a) = a" by (rule minus_unique) 
23085  299 
qed 
14738  300 

25062  301 
lemma right_minus [simp]: "a +  a = 0" 
14738  302 
proof  
25062  303 
have "a +  a =  ( a) +  a" by simp 
304 
also have "\<dots> = 0" by (rule left_minus) 

14738  305 
finally show ?thesis . 
306 
qed 

307 

40368
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

308 
subclass cancel_semigroup_add 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

309 
proof 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

310 
fix a b c :: 'a 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

311 
assume "a + b = a + c" 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

312 
then have " a + a + b =  a + a + c" 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

313 
unfolding add_assoc by simp 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

314 
then show "b = c" by simp 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

315 
next 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

316 
fix a b c :: 'a 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

317 
assume "b + a = c + a" 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

318 
then have "b + a +  a = c + a +  a" by simp 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

319 
then show "b = c" unfolding add_assoc by simp 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

320 
qed 
47c186c8577d
added class relation group_add < cancel_semigroup_add
haftmann
parents:
39134
diff
changeset

321 

34147
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

322 
lemma minus_add_cancel: " a + (a + b) = b" 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

323 
by (simp add: add_assoc [symmetric]) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

324 

319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

325 
lemma add_minus_cancel: "a + ( a + b) = b" 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

326 
by (simp add: add_assoc [symmetric]) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

327 

319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

328 
lemma minus_add: " (a + b) =  b +  a" 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

329 
proof  
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

330 
have "(a + b) + ( b +  a) = 0" 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

331 
by (simp add: add_assoc add_minus_cancel) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

332 
thus " (a + b) =  b +  a" 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

333 
by (rule minus_unique) 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

334 
qed 
319616f4eecf
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
huffman
parents:
34146
diff
changeset

335 

25062  336 
lemma right_minus_eq: "a  b = 0 \<longleftrightarrow> a = b" 
14738  337 
proof 
23085  338 
assume "a  b = 0" 
339 
have "a = (a  b) + b" by (simp add:diff_minus add_assoc) 

340 
also have "\<dots> = b" using `a  b = 0` by simp 

341 
finally show "a = b" . 

14738  342 
next 
23085  343 
assume "a = b" thus "a  b = 0" by (simp add: diff_minus) 
14738  344 
qed 
345 

25062  346 
lemma diff_self [simp]: "a  a = 0" 
29667  347 
by (simp add: diff_minus) 
14738  348 

25062  349 
lemma diff_0 [simp]: "0  a =  a" 
29667  350 
by (simp add: diff_minus) 
14738  351 

25062  352 
lemma diff_0_right [simp]: "a  0 = a" 
29667  353 
by (simp add: diff_minus) 
14738  354 

25062  355 
lemma diff_minus_eq_add [simp]: "a   b = a + b" 
29667  356 
by (simp add: diff_minus) 
14738  357 

25062  358 
lemma neg_equal_iff_equal [simp]: 
359 
" a =  b \<longleftrightarrow> a = b" 

14738  360 
proof 
361 
assume " a =  b" 

29667  362 
hence " ( a) =  ( b)" by simp 
25062  363 
thus "a = b" by simp 
14738  364 
next 
25062  365 
assume "a = b" 
366 
thus " a =  b" by simp 

14738  367 
qed 
368 

25062  369 
lemma neg_equal_0_iff_equal [simp]: 
370 
" a = 0 \<longleftrightarrow> a = 0" 

29667  371 
by (subst neg_equal_iff_equal [symmetric], simp) 
14738  372 

25062  373 
lemma neg_0_equal_iff_equal [simp]: 
374 
"0 =  a \<longleftrightarrow> 0 = a" 

29667  375 
by (subst neg_equal_iff_equal [symmetric], simp) 
14738  376 

377 
text{*The next two equations can make the simplifier loop!*} 

378 

25062  379 
lemma equation_minus_iff: 
380 
"a =  b \<longleftrightarrow> b =  a" 

14738  381 
proof  
25062  382 
have " ( a) =  b \<longleftrightarrow>  a = b" by (rule neg_equal_iff_equal) 
383 
thus ?thesis by (simp add: eq_commute) 

384 
qed 

385 

386 
lemma minus_equation_iff: 

387 
" a = b \<longleftrightarrow>  b = a" 

388 
proof  

389 
have " a =  ( b) \<longleftrightarrow> a = b" by (rule neg_equal_iff_equal) 

14738  390 
thus ?thesis by (simp add: eq_commute) 
391 
qed 

392 

28130
32b4185bfdc7
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
huffman
parents:
27516
diff
changeset

393 
lemma diff_add_cancel: "a  b + b = a" 
29667  394 
by (simp add: diff_minus add_assoc) 
28130
32b4185bfdc7
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
huffman
parents:
27516
diff
changeset

395 

32b4185bfdc7
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
huffman
parents:
27516
diff
changeset

396 
lemma add_diff_cancel: "a + b  b = a" 
29667  397 
by (simp add: diff_minus add_assoc) 
398 

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

399 
declare diff_minus[symmetric, algebra_simps, field_simps] 
28130
32b4185bfdc7
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
huffman
parents:
27516
diff
changeset

400 

29914
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

401 
lemma eq_neg_iff_add_eq_0: "a =  b \<longleftrightarrow> a + b = 0" 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

402 
proof 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

403 
assume "a =  b" then show "a + b = 0" by simp 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

404 
next 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

405 
assume "a + b = 0" 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

406 
moreover have "a + (b +  b) = (a + b) +  b" 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

407 
by (simp only: add_assoc) 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

408 
ultimately show "a =  b" by simp 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

409 
qed 
c9ced4f54e82
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
huffman
parents:
29904
diff
changeset

410 

44348  411 
lemma add_eq_0_iff: "x + y = 0 \<longleftrightarrow> y =  x" 
412 
unfolding eq_neg_iff_add_eq_0 [symmetric] 

413 
by (rule equation_minus_iff) 

414 

45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

415 
lemma minus_diff_eq [simp]: " (a  b) = b  a" 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

416 
by (simp add: diff_minus minus_add) 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

417 

3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

418 
lemma add_diff_eq[algebra_simps, field_simps]: "a + (b  c) = (a + b)  c" 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

419 
by (simp add: diff_minus add_assoc) 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

420 

3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

421 
lemma diff_eq_eq[algebra_simps, field_simps]: "a  b = c \<longleftrightarrow> a = c + b" 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

422 
by (auto simp add: diff_minus add_assoc) 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

423 

3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

424 
lemma eq_diff_eq[algebra_simps, field_simps]: "a = c  b \<longleftrightarrow> a + b = c" 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

425 
by (auto simp add: diff_minus add_assoc) 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

426 

3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

427 
lemma diff_diff_eq2[algebra_simps, field_simps]: "a  (b  c) = (a + c)  b" 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

428 
by (simp add: diff_minus minus_add add_assoc) 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

429 

3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

430 
lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a  b = 0" 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

431 
by (fact right_minus_eq [symmetric]) 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

432 

3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

433 
lemma diff_eq_diff_eq: 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

434 
"a  b = c  d \<Longrightarrow> a = b \<longleftrightarrow> c = d" 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

435 
by (simp add: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d]) 
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

436 

25062  437 
end 
438 

25762  439 
class ab_group_add = minus + uminus + comm_monoid_add + 
25062  440 
assumes ab_left_minus: " a + a = 0" 
441 
assumes ab_diff_minus: "a  b = a + ( b)" 

25267  442 
begin 
25062  443 

25267  444 
subclass group_add 
28823  445 
proof qed (simp_all add: ab_left_minus ab_diff_minus) 
25062  446 

29904  447 
subclass cancel_comm_monoid_add 
28823  448 
proof 
25062  449 
fix a b c :: 'a 
450 
assume "a + b = a + c" 

451 
then have " a + a + b =  a + a + c" 

452 
unfolding add_assoc by simp 

453 
then show "b = c" by simp 

454 
qed 

455 

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

456 
lemma uminus_add_conv_diff[algebra_simps, field_simps]: 
25062  457 
" a + b = b  a" 
29667  458 
by (simp add:diff_minus add_commute) 
25062  459 

460 
lemma minus_add_distrib [simp]: 

461 
" (a + b) =  a +  b" 

34146
14595e0c27e8
rename equals_zero_I to minus_unique (keep old name too)
huffman
parents:
33364
diff
changeset

462 
by (rule minus_unique) (simp add: add_ac) 
25062  463 

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

464 
lemma diff_add_eq[algebra_simps, field_simps]: "(a  b) + c = (a + c)  b" 
29667  465 
by (simp add: diff_minus add_ac) 
25077  466 

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

467 
lemma diff_diff_eq[algebra_simps, field_simps]: "(a  b)  c = a  (b + c)" 
29667  468 
by (simp add: diff_minus add_ac) 
25077  469 

35216  470 
(* FIXME: duplicates right_minus_eq from class group_add *) 
471 
(* but only this one is declared as a simp rule. *) 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35723
diff
changeset

472 
lemma diff_eq_0_iff_eq [simp, no_atp]: "a  b = 0 \<longleftrightarrow> a = b" 
44348  473 
by (rule right_minus_eq) 
30629  474 

25062  475 
end 
14738  476 

37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

477 

14738  478 
subsection {* (Partially) Ordered Groups *} 
479 

35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

480 
text {* 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

481 
The theory of partially ordered groups is taken from the books: 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

482 
\begin{itemize} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

483 
\item \emph{Lattice Theory} by Garret Birkhoff, American Mathematical Society 1979 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

484 
\item \emph{Partially Ordered Algebraic Systems}, Pergamon Press 1963 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

485 
\end{itemize} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

486 
Most of the used notions can also be looked up in 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

487 
\begin{itemize} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

488 
\item \url{http://www.mathworld.com} by Eric Weisstein et. al. 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

489 
\item \emph{Algebra I} by van der Waerden, Springer. 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

490 
\end{itemize} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

491 
*} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

492 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

493 
class ordered_ab_semigroup_add = order + ab_semigroup_add + 
25062  494 
assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b" 
495 
begin 

24380
c215e256beca
moved ordered_ab_semigroup_add to OrderedGroup.thy
haftmann
parents:
24286
diff
changeset

496 

25062  497 
lemma add_right_mono: 
498 
"a \<le> b \<Longrightarrow> a + c \<le> b + c" 

29667  499 
by (simp add: add_commute [of _ c] add_left_mono) 
14738  500 

501 
text {* nonstrict, in both arguments *} 

502 
lemma add_mono: 

25062  503 
"a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c \<le> b + d" 
14738  504 
apply (erule add_right_mono [THEN order_trans]) 
505 
apply (simp add: add_commute add_left_mono) 

506 
done 

507 

25062  508 
end 
509 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

510 
class ordered_cancel_ab_semigroup_add = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

511 
ordered_ab_semigroup_add + cancel_ab_semigroup_add 
25062  512 
begin 
513 

14738  514 
lemma add_strict_left_mono: 
25062  515 
"a < b \<Longrightarrow> c + a < c + b" 
29667  516 
by (auto simp add: less_le add_left_mono) 
14738  517 

518 
lemma add_strict_right_mono: 

25062  519 
"a < b \<Longrightarrow> a + c < b + c" 
29667  520 
by (simp add: add_commute [of _ c] add_strict_left_mono) 
14738  521 

522 
text{*Strict monotonicity in both arguments*} 

25062  523 
lemma add_strict_mono: 
524 
"a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" 

525 
apply (erule add_strict_right_mono [THEN less_trans]) 

14738  526 
apply (erule add_strict_left_mono) 
527 
done 

528 

529 
lemma add_less_le_mono: 

25062  530 
"a < b \<Longrightarrow> c \<le> d \<Longrightarrow> a + c < b + d" 
531 
apply (erule add_strict_right_mono [THEN less_le_trans]) 

532 
apply (erule add_left_mono) 

14738  533 
done 
534 

535 
lemma add_le_less_mono: 

25062  536 
"a \<le> b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" 
537 
apply (erule add_right_mono [THEN le_less_trans]) 

14738  538 
apply (erule add_strict_left_mono) 
539 
done 

540 

25062  541 
end 
542 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

543 
class ordered_ab_semigroup_add_imp_le = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

544 
ordered_cancel_ab_semigroup_add + 
25062  545 
assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b" 
546 
begin 

547 

14738  548 
lemma add_less_imp_less_left: 
29667  549 
assumes less: "c + a < c + b" shows "a < b" 
14738  550 
proof  
551 
from less have le: "c + a <= c + b" by (simp add: order_le_less) 

552 
have "a <= b" 

553 
apply (insert le) 

554 
apply (drule add_le_imp_le_left) 

555 
by (insert le, drule add_le_imp_le_left, assumption) 

556 
moreover have "a \<noteq> b" 

557 
proof (rule ccontr) 

558 
assume "~(a \<noteq> b)" 

559 
then have "a = b" by simp 

560 
then have "c + a = c + b" by simp 

561 
with less show "False"by simp 

562 
qed 

563 
ultimately show "a < b" by (simp add: order_le_less) 

564 
qed 

565 

566 
lemma add_less_imp_less_right: 

25062  567 
"a + c < b + c \<Longrightarrow> a < b" 
14738  568 
apply (rule add_less_imp_less_left [of c]) 
569 
apply (simp add: add_commute) 

570 
done 

571 

572 
lemma add_less_cancel_left [simp]: 

25062  573 
"c + a < c + b \<longleftrightarrow> a < b" 
29667  574 
by (blast intro: add_less_imp_less_left add_strict_left_mono) 
14738  575 

576 
lemma add_less_cancel_right [simp]: 

25062  577 
"a + c < b + c \<longleftrightarrow> a < b" 
29667  578 
by (blast intro: add_less_imp_less_right add_strict_right_mono) 
14738  579 

580 
lemma add_le_cancel_left [simp]: 

25062  581 
"c + a \<le> c + b \<longleftrightarrow> a \<le> b" 
29667  582 
by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
14738  583 

584 
lemma add_le_cancel_right [simp]: 

25062  585 
"a + c \<le> b + c \<longleftrightarrow> a \<le> b" 
29667  586 
by (simp add: add_commute [of a c] add_commute [of b c]) 
14738  587 

588 
lemma add_le_imp_le_right: 

25062  589 
"a + c \<le> b + c \<Longrightarrow> a \<le> b" 
29667  590 
by simp 
25062  591 

25077  592 
lemma max_add_distrib_left: 
593 
"max x y + z = max (x + z) (y + z)" 

594 
unfolding max_def by auto 

595 

596 
lemma min_add_distrib_left: 

597 
"min x y + z = min (x + z) (y + z)" 

598 
unfolding min_def by auto 

599 

44848
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

600 
lemma max_add_distrib_right: 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

601 
"x + max y z = max (x + y) (x + z)" 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

602 
unfolding max_def by auto 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

603 

f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

604 
lemma min_add_distrib_right: 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

605 
"x + min y z = min (x + y) (x + z)" 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

606 
unfolding min_def by auto 
f4d0b060c7ca
remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}
huffman
parents:
44433
diff
changeset

607 

25062  608 
end 
609 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

610 
subsection {* Support for reasoning about signs *} 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

611 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

612 
class ordered_comm_monoid_add = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

613 
ordered_cancel_ab_semigroup_add + comm_monoid_add 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

614 
begin 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

615 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

616 
lemma add_pos_nonneg: 
29667  617 
assumes "0 < a" and "0 \<le> b" shows "0 < a + b" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

618 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

619 
have "0 + 0 < a + b" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

620 
using assms by (rule add_less_le_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

621 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

622 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

623 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

624 
lemma add_pos_pos: 
29667  625 
assumes "0 < a" and "0 < b" shows "0 < a + b" 
626 
by (rule add_pos_nonneg) (insert assms, auto) 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

627 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

628 
lemma add_nonneg_pos: 
29667  629 
assumes "0 \<le> a" and "0 < b" shows "0 < a + b" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

630 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

631 
have "0 + 0 < a + b" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

632 
using assms by (rule add_le_less_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

633 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

634 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

635 

36977
71c8973a604b
declare add_nonneg_nonneg [simp]; remove nowredundant lemmas realpow_two_le_order(2)
huffman
parents:
36348
diff
changeset

636 
lemma add_nonneg_nonneg [simp]: 
29667  637 
assumes "0 \<le> a" and "0 \<le> b" shows "0 \<le> a + b" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

638 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

639 
have "0 + 0 \<le> a + b" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

640 
using assms by (rule add_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

641 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

642 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

643 

30691  644 
lemma add_neg_nonpos: 
29667  645 
assumes "a < 0" and "b \<le> 0" shows "a + b < 0" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

646 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

647 
have "a + b < 0 + 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

648 
using assms by (rule add_less_le_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

649 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

650 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

651 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

652 
lemma add_neg_neg: 
29667  653 
assumes "a < 0" and "b < 0" shows "a + b < 0" 
654 
by (rule add_neg_nonpos) (insert assms, auto) 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

655 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

656 
lemma add_nonpos_neg: 
29667  657 
assumes "a \<le> 0" and "b < 0" shows "a + b < 0" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

658 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

659 
have "a + b < 0 + 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

660 
using assms by (rule add_le_less_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

661 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

662 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

663 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

664 
lemma add_nonpos_nonpos: 
29667  665 
assumes "a \<le> 0" and "b \<le> 0" shows "a + b \<le> 0" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

666 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

667 
have "a + b \<le> 0 + 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

668 
using assms by (rule add_mono) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

669 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

670 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

671 

30691  672 
lemmas add_sign_intros = 
673 
add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg 

674 
add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos 

675 

29886  676 
lemma add_nonneg_eq_0_iff: 
677 
assumes x: "0 \<le> x" and y: "0 \<le> y" 

678 
shows "x + y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" 

679 
proof (intro iffI conjI) 

680 
have "x = x + 0" by simp 

681 
also have "x + 0 \<le> x + y" using y by (rule add_left_mono) 

682 
also assume "x + y = 0" 

683 
also have "0 \<le> x" using x . 

684 
finally show "x = 0" . 

685 
next 

686 
have "y = 0 + y" by simp 

687 
also have "0 + y \<le> x + y" using x by (rule add_right_mono) 

688 
also assume "x + y = 0" 

689 
also have "0 \<le> y" using y . 

690 
finally show "y = 0" . 

691 
next 

692 
assume "x = 0 \<and> y = 0" 

693 
then show "x + y = 0" by simp 

694 
qed 

695 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

696 
end 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

697 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

698 
class ordered_ab_group_add = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

699 
ab_group_add + ordered_ab_semigroup_add 
25062  700 
begin 
701 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

702 
subclass ordered_cancel_ab_semigroup_add .. 
25062  703 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

704 
subclass ordered_ab_semigroup_add_imp_le 
28823  705 
proof 
25062  706 
fix a b c :: 'a 
707 
assume "c + a \<le> c + b" 

708 
hence "(c) + (c + a) \<le> (c) + (c + b)" by (rule add_left_mono) 

709 
hence "((c) + c) + a \<le> ((c) + c) + b" by (simp only: add_assoc) 

710 
thus "a \<le> b" by simp 

711 
qed 

712 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

713 
subclass ordered_comm_monoid_add .. 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

714 

25077  715 
lemma max_diff_distrib_left: 
716 
shows "max x y  z = max (x  z) (y  z)" 

29667  717 
by (simp add: diff_minus, rule max_add_distrib_left) 
25077  718 

719 
lemma min_diff_distrib_left: 

720 
shows "min x y  z = min (x  z) (y  z)" 

29667  721 
by (simp add: diff_minus, rule min_add_distrib_left) 
25077  722 

723 
lemma le_imp_neg_le: 

29667  724 
assumes "a \<le> b" shows "b \<le> a" 
25077  725 
proof  
29667  726 
have "a+a \<le> a+b" using `a \<le> b` by (rule add_left_mono) 
727 
hence "0 \<le> a+b" by simp 

728 
hence "0 + (b) \<le> (a + b) + (b)" by (rule add_right_mono) 

729 
thus ?thesis by (simp add: add_assoc) 

25077  730 
qed 
731 

732 
lemma neg_le_iff_le [simp]: " b \<le>  a \<longleftrightarrow> a \<le> b" 

733 
proof 

734 
assume " b \<le>  a" 

29667  735 
hence " ( a) \<le>  ( b)" by (rule le_imp_neg_le) 
25077  736 
thus "a\<le>b" by simp 
737 
next 

738 
assume "a\<le>b" 

739 
thus "b \<le> a" by (rule le_imp_neg_le) 

740 
qed 

741 

742 
lemma neg_le_0_iff_le [simp]: " a \<le> 0 \<longleftrightarrow> 0 \<le> a" 

29667  743 
by (subst neg_le_iff_le [symmetric], simp) 
25077  744 

745 
lemma neg_0_le_iff_le [simp]: "0 \<le>  a \<longleftrightarrow> a \<le> 0" 

29667  746 
by (subst neg_le_iff_le [symmetric], simp) 
25077  747 

748 
lemma neg_less_iff_less [simp]: " b <  a \<longleftrightarrow> a < b" 

29667  749 
by (force simp add: less_le) 
25077  750 

751 
lemma neg_less_0_iff_less [simp]: " a < 0 \<longleftrightarrow> 0 < a" 

29667  752 
by (subst neg_less_iff_less [symmetric], simp) 
25077  753 

754 
lemma neg_0_less_iff_less [simp]: "0 <  a \<longleftrightarrow> a < 0" 

29667  755 
by (subst neg_less_iff_less [symmetric], simp) 
25077  756 

757 
text{*The next several equations can make the simplifier loop!*} 

758 

759 
lemma less_minus_iff: "a <  b \<longleftrightarrow> b <  a" 

760 
proof  

761 
have "( (a) <  b) = (b <  a)" by (rule neg_less_iff_less) 

762 
thus ?thesis by simp 

763 
qed 

764 

765 
lemma minus_less_iff: " a < b \<longleftrightarrow>  b < a" 

766 
proof  

767 
have "( a <  (b)) = ( b < a)" by (rule neg_less_iff_less) 

768 
thus ?thesis by simp 

769 
qed 

770 

771 
lemma le_minus_iff: "a \<le>  b \<longleftrightarrow> b \<le>  a" 

772 
proof  

773 
have mm: "!! a (b::'a). ((a)) < b \<Longrightarrow> (b) < a" by (simp only: minus_less_iff) 

774 
have "( ( a) <= b) = (b <=  a)" 

775 
apply (auto simp only: le_less) 

776 
apply (drule mm) 

777 
apply (simp_all) 

778 
apply (drule mm[simplified], assumption) 

779 
done 

780 
then show ?thesis by simp 

781 
qed 

782 

783 
lemma minus_le_iff: " a \<le> b \<longleftrightarrow>  b \<le> a" 

29667  784 
by (auto simp add: le_less minus_less_iff) 
25077  785 

37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

786 
lemma diff_less_0_iff_less [simp, no_atp]: 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

787 
"a  b < 0 \<longleftrightarrow> a < b" 
25077  788 
proof  
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

789 
have "a  b < 0 \<longleftrightarrow> a + ( b) < b + ( b)" by (simp add: diff_minus) 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

790 
also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right) 
25077  791 
finally show ?thesis . 
792 
qed 

793 

37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

794 
lemmas less_iff_diff_less_0 = diff_less_0_iff_less [symmetric] 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

795 

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

796 
lemma diff_less_eq[algebra_simps, field_simps]: "a  b < c \<longleftrightarrow> a < c + b" 
25077  797 
apply (subst less_iff_diff_less_0 [of a]) 
798 
apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) 

799 
apply (simp add: diff_minus add_ac) 

800 
done 

801 

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

802 
lemma less_diff_eq[algebra_simps, field_simps]: "a < c  b \<longleftrightarrow> a + b < c" 
36302  803 
apply (subst less_iff_diff_less_0 [of "a + b"]) 
25077  804 
apply (subst less_iff_diff_less_0 [of a]) 
805 
apply (simp add: diff_minus add_ac) 

806 
done 

807 

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

808 
lemma diff_le_eq[algebra_simps, field_simps]: "a  b \<le> c \<longleftrightarrow> a \<le> c + b" 
29667  809 
by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel) 
25077  810 

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

811 
lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c  b \<longleftrightarrow> a + b \<le> c" 
29667  812 
by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel) 
25077  813 

37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

814 
lemma diff_le_0_iff_le [simp, no_atp]: 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

815 
"a  b \<le> 0 \<longleftrightarrow> a \<le> b" 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

816 
by (simp add: algebra_simps) 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

817 

314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

818 
lemmas le_iff_diff_le_0 = diff_le_0_iff_le [symmetric] 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

819 

314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

820 
lemma diff_eq_diff_less: 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

821 
"a  b = c  d \<Longrightarrow> a < b \<longleftrightarrow> c < d" 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

822 
by (auto simp only: less_iff_diff_less_0 [of a b] less_iff_diff_less_0 [of c d]) 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

823 

37889
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

824 
lemma diff_eq_diff_less_eq: 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

825 
"a  b = c  d \<Longrightarrow> a \<le> b \<longleftrightarrow> c \<le> d" 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

826 
by (auto simp only: le_iff_diff_le_0 [of a b] le_iff_diff_le_0 [of c d]) 
25077  827 

828 
end 

829 

37986
3b3187adf292
use file names relative to master directory of theory source  Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);
wenzelm
parents:
37889
diff
changeset

830 
use "Tools/abel_cancel.ML" 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

831 

37889
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

832 
simproc_setup abel_cancel_sum 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

833 
("a + b::'a::ab_group_add"  "a  b::'a::ab_group_add") = 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

834 
{* fn phi => Abel_Cancel.sum_proc *} 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

835 

0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

836 
simproc_setup abel_cancel_relation 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

837 
("a < (b::'a::ordered_ab_group_add)"  "a \<le> (b::'a::ordered_ab_group_add)"  "c = (d::'b::ab_group_add)") = 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

838 
{* fn phi => Abel_Cancel.rel_proc *} 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

839 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

840 
class linordered_ab_semigroup_add = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

841 
linorder + ordered_ab_semigroup_add 
25062  842 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

843 
class linordered_cancel_ab_semigroup_add = 
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

844 
linorder + ordered_cancel_ab_semigroup_add 
25267  845 
begin 
25062  846 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

847 
subclass linordered_ab_semigroup_add .. 
25062  848 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

849 
subclass ordered_ab_semigroup_add_imp_le 
28823  850 
proof 
25062  851 
fix a b c :: 'a 
852 
assume le: "c + a <= c + b" 

853 
show "a <= b" 

854 
proof (rule ccontr) 

855 
assume w: "~ a \<le> b" 

856 
hence "b <= a" by (simp add: linorder_not_le) 

857 
hence le2: "c + b <= c + a" by (rule add_left_mono) 

858 
have "a = b" 

859 
apply (insert le) 

860 
apply (insert le2) 

861 
apply (drule antisym, simp_all) 

862 
done 

863 
with w show False 

864 
by (simp add: linorder_not_le [symmetric]) 

865 
qed 

866 
qed 

867 

25267  868 
end 
869 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

870 
class linordered_ab_group_add = linorder + ordered_ab_group_add 
25267  871 
begin 
25230  872 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

873 
subclass linordered_cancel_ab_semigroup_add .. 
25230  874 

35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

875 
lemma neg_less_eq_nonneg [simp]: 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

876 
" a \<le> a \<longleftrightarrow> 0 \<le> a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

877 
proof 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

878 
assume A: " a \<le> a" show "0 \<le> a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

879 
proof (rule classical) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

880 
assume "\<not> 0 \<le> a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

881 
then have "a < 0" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

882 
with A have " a < 0" by (rule le_less_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

883 
then show ?thesis by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

884 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

885 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

886 
assume A: "0 \<le> a" show " a \<le> a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

887 
proof (rule order_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

888 
show " a \<le> 0" using A by (simp add: minus_le_iff) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

889 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

890 
show "0 \<le> a" using A . 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

891 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

892 
qed 
35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

893 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

894 
lemma neg_less_nonneg [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

895 
" a < a \<longleftrightarrow> 0 < a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

896 
proof 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

897 
assume A: " a < a" show "0 < a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

898 
proof (rule classical) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

899 
assume "\<not> 0 < a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

900 
then have "a \<le> 0" by auto 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

901 
with A have " a < 0" by (rule less_le_trans) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

902 
then show ?thesis by auto 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

903 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

904 
next 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

905 
assume A: "0 < a" show " a < a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

906 
proof (rule less_trans) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

907 
show " a < 0" using A by (simp add: minus_le_iff) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

908 
next 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

909 
show "0 < a" using A . 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

910 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

911 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

912 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

913 
lemma less_eq_neg_nonpos [simp]: 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

914 
"a \<le>  a \<longleftrightarrow> a \<le> 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

915 
proof 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

916 
assume A: "a \<le>  a" show "a \<le> 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

917 
proof (rule classical) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

918 
assume "\<not> a \<le> 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

919 
then have "0 < a" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

920 
then have "0 <  a" using A by (rule less_le_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

921 
then show ?thesis by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

922 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

923 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

924 
assume A: "a \<le> 0" show "a \<le>  a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

925 
proof (rule order_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

926 
show "0 \<le>  a" using A by (simp add: minus_le_iff) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

927 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

928 
show "a \<le> 0" using A . 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

929 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

930 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

931 

35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

932 
lemma equal_neg_zero [simp]: 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

933 
"a =  a \<longleftrightarrow> a = 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

934 
proof 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

935 
assume "a = 0" then show "a =  a" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

936 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

937 
assume A: "a =  a" show "a = 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

938 
proof (cases "0 \<le> a") 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

939 
case True with A have "0 \<le>  a" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

940 
with le_minus_iff have "a \<le> 0" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

941 
with True show ?thesis by (auto intro: order_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

942 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

943 
case False then have B: "a \<le> 0" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

944 
with A have " a \<le> 0" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

945 
with B show ?thesis by (auto intro: order_trans) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

946 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

947 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

948 

35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

949 
lemma neg_equal_zero [simp]: 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

950 
" a = a \<longleftrightarrow> a = 0" 
35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

951 
by (auto dest: sym) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

952 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

953 
lemma double_zero [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

954 
"a + a = 0 \<longleftrightarrow> a = 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

955 
proof 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

956 
assume assm: "a + a = 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

957 
then have a: " a = a" by (rule minus_unique) 
35216  958 
then show "a = 0" by (simp only: neg_equal_zero) 
35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

959 
qed simp 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

960 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

961 
lemma double_zero_sym [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

962 
"0 = a + a \<longleftrightarrow> a = 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

963 
by (rule, drule sym) simp_all 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

964 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

965 
lemma zero_less_double_add_iff_zero_less_single_add [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

966 
"0 < a + a \<longleftrightarrow> 0 < a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

967 
proof 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

968 
assume "0 < a + a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

969 
then have "0  a < a" by (simp only: diff_less_eq) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

970 
then have " a < a" by simp 
35216  971 
then show "0 < a" by (simp only: neg_less_nonneg) 
35036
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

972 
next 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

973 
assume "0 < a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

974 
with this have "0 + 0 < a + a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

975 
by (rule add_strict_mono) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

976 
then show "0 < a + a" by simp 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

977 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

978 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

979 
lemma zero_le_double_add_iff_zero_le_single_add [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

980 
"0 \<le> a + a \<longleftrightarrow> 0 \<le> a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

981 
by (auto simp add: le_less) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

982 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

983 
lemma double_add_less_zero_iff_single_add_less_zero [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

984 
"a + a < 0 \<longleftrightarrow> a < 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

985 
proof  
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

986 
have "\<not> a + a < 0 \<longleftrightarrow> \<not> a < 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

987 
by (simp add: not_less) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

988 
then show ?thesis by simp 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

989 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

990 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

991 
lemma double_add_le_zero_iff_single_add_le_zero [simp]: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

992 
"a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

993 
proof  
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

994 
have "\<not> a + a \<le> 0 \<longleftrightarrow> \<not> a \<le> 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

995 
by (simp add: not_le) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

996 
then show ?thesis by simp 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

997 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

998 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

999 
lemma le_minus_self_iff: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1000 
"a \<le>  a \<longleftrightarrow> a \<le> 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1001 
proof  
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1002 
from add_le_cancel_left [of " a" "a + a" 0] 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1003 
have "a \<le>  a \<longleftrightarrow> a + a \<le> 0" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1004 
by (simp add: add_assoc [symmetric]) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1005 
thus ?thesis by simp 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1006 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1007 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1008 
lemma minus_le_self_iff: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1009 
" a \<le> a \<longleftrightarrow> 0 \<le> a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1010 
proof  
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1011 
from add_le_cancel_left [of " a" 0 "a + a"] 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1012 
have " a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1013 
by (simp add: add_assoc [symmetric]) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1014 
thus ?thesis by simp 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1015 
qed 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1016 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1017 
lemma minus_max_eq_min: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1018 
" max x y = min (x) (y)" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1019 
by (auto simp add: max_def min_def) 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1020 

b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1021 
lemma minus_min_eq_max: 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1022 
" min x y = max (x) (y)" 
b8c8d01cc20d
separate library theory for type classes combining lattices with various algebraic structures; more simp rules
haftmann
parents:
35028
diff
changeset

1023 
by (auto simp add: max_def min_def) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1024 

25267  1025 
end 
1026 

36302  1027 
context ordered_comm_monoid_add 
1028 
begin 

14738  1029 

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

1030 
lemma add_increasing: 
36302  1031 
"0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c" 
1032 
by (insert add_mono [of 0 a b c], simp) 

14738  1033 

15539  1034 
lemma add_increasing2: 
36302  1035 
"0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c" 
1036 
by (simp add: add_increasing add_commute [of a]) 

15539  1037 

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

1038 
lemma add_strict_increasing: 
36302  1039 
"0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c" 
1040 
by (insert add_less_le_mono [of 0 a b c], simp) 

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

1041 

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

1042 
lemma add_strict_increasing2: 
36302  1043 
"0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c" 
1044 
by (insert add_le_less_mono [of 0 a b c], simp) 

1045 

1046 
end 

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

1047 

35092
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1048 
class abs = 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1049 
fixes abs :: "'a \<Rightarrow> 'a" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1050 
begin 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1051 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1052 
notation (xsymbols) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1053 
abs ("\<bar>_\<bar>") 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1054 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1055 
notation (HTML output) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1056 
abs ("\<bar>_\<bar>") 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1057 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1058 
end 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1059 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1060 
class sgn = 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1061 
fixes sgn :: "'a \<Rightarrow> 'a" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1062 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1063 
class abs_if = minus + uminus + ord + zero + abs + 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1064 
assumes abs_if: "\<bar>a\<bar> = (if a < 0 then  a else a)" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1065 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1066 
class sgn_if = minus + uminus + zero + one + ord + sgn + 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1067 
assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else  1)" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1068 
begin 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1069 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1070 
lemma sgn0 [simp]: "sgn 0 = 0" 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1071 
by (simp add:sgn_if) 
cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1072 

cfe605c54e50
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
haftmann
parents:
35050
diff
changeset

1073 
end 
14738  1074 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1075 
class ordered_ab_group_add_abs = ordered_ab_group_add + abs + 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1076 
assumes abs_ge_zero [simp]: "\<bar>a\<bar> \<ge> 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1077 
and abs_ge_self: "a \<le> \<bar>a\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1078 
and abs_leI: "a \<le> b \<Longrightarrow>  a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1079 
and abs_minus_cancel [simp]: "\<bar>a\<bar> = \<bar>a\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1080 
and abs_triangle_ineq: "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1081 
begin 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1082 

25307  1083 
lemma abs_minus_le_zero: " \<bar>a\<bar> \<le> 0" 
1084 
unfolding neg_le_0_iff_le by simp 

1085 

1086 
lemma abs_of_nonneg [simp]: 

29667  1087 
assumes nonneg: "0 \<le> a" shows "\<bar>a\<bar> = a" 
25307  1088 
proof (rule antisym) 
1089 
from nonneg le_imp_neg_le have " a \<le> 0" by simp 

1090 
from this nonneg have " a \<le> a" by (rule order_trans) 

1091 
then show "\<bar>a\<bar> \<le> a" by (auto intro: abs_leI) 

1092 
qed (rule abs_ge_self) 

1093 

1094 
lemma abs_idempotent [simp]: "\<bar>\<bar>a\<bar>\<bar> = \<bar>a\<bar>" 

29667  1095 
by (rule antisym) 
36302  1096 
(auto intro!: abs_ge_self abs_leI order_trans [of " \<bar>a\<bar>" 0 "\<bar>a\<bar>"]) 
25307  1097 

1098 
lemma abs_eq_0 [simp]: "\<bar>a\<bar> = 0 \<longleftrightarrow> a = 0" 

1099 
proof  

1100 
have "\<bar>a\<bar> = 0 \<Longrightarrow> a = 0" 

1101 
proof (rule antisym) 

1102 
assume zero: "\<bar>a\<bar> = 0" 

1103 
with abs_ge_self show "a \<le> 0" by auto 

1104 
from zero have "\<bar>a\<bar> = 0" by simp 

36302  1105 
with abs_ge_self [of " a"] have " a \<le> 0" by auto 
25307  1106 
with neg_le_0_iff_le show "0 \<le> a" by auto 
1107 
qed 

1108 
then show ?thesis by auto 

1109 
qed 

1110 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1111 
lemma abs_zero [simp]: "\<bar>0\<bar> = 0" 
29667  1112 
by simp 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1113 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35723
diff
changeset

1114 
lemma abs_0_eq [simp, no_atp]: "0 = \<bar>a\<bar> \<longleftrightarrow> a = 0" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1115 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1116 
have "0 = \<bar>a\<bar> \<longleftrightarrow> \<bar>a\<bar> = 0" by (simp only: eq_ac) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1117 
thus ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1118 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1119 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1120 
lemma abs_le_zero_iff [simp]: "\<bar>a\<bar> \<le> 0 \<longleftrightarrow> a = 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1121 
proof 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1122 
assume "\<bar>a\<bar> \<le> 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1123 
then have "\<bar>a\<bar> = 0" by (rule antisym) simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1124 
thus "a = 0" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1125 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1126 
assume "a = 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1127 
thus "\<bar>a\<bar> \<le> 0" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1128 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1129 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1130 
lemma zero_less_abs_iff [simp]: "0 < \<bar>a\<bar> \<longleftrightarrow> a \<noteq> 0" 
29667  1131 
by (simp add: less_le) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1132 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1133 
lemma abs_not_less_zero [simp]: "\<not> \<bar>a\<bar> < 0" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1134 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1135 
have a: "\<And>x y. x \<le> y \<Longrightarrow> \<not> y < x" by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1136 
show ?thesis by (simp add: a) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1137 
qed 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1138 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1139 
lemma abs_ge_minus_self: " a \<le> \<bar>a\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1140 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1141 
have " a \<le> \<bar>a\<bar>" by (rule abs_ge_self) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1142 
then show ?thesis by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1143 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1144 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1145 
lemma abs_minus_commute: 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1146 
"\<bar>a  b\<bar> = \<bar>b  a\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1147 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1148 
have "\<bar>a  b\<bar> = \<bar> (a  b)\<bar>" by (simp only: abs_minus_cancel) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1149 
also have "... = \<bar>b  a\<bar>" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1150 
finally show ?thesis . 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1151 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1152 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1153 
lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a" 
29667  1154 
by (rule abs_of_nonneg, rule less_imp_le) 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1155 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1156 
lemma abs_of_nonpos [simp]: 
29667  1157 
assumes "a \<le> 0" shows "\<bar>a\<bar> =  a" 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1158 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1159 
let ?b = " a" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1160 
have " ?b \<le> 0 \<Longrightarrow> \<bar> ?b\<bar> =  ( ?b)" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1161 
unfolding abs_minus_cancel [of "?b"] 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1162 
unfolding neg_le_0_iff_le [of "?b"] 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1163 
unfolding minus_minus by (erule abs_of_nonneg) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1164 
then show ?thesis using assms by auto 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1165 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1166 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1167 
lemma abs_of_neg: "a < 0 \<Longrightarrow> \<bar>a\<bar> =  a" 
29667  1168 
by (rule abs_of_nonpos, rule less_imp_le) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1169 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1170 
lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b" 
29667  1171 
by (insert abs_ge_self, blast intro: order_trans) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1172 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1173 
lemma abs_le_D2: "\<bar>a\<bar> \<le> b \<Longrightarrow>  a \<le> b" 
36302  1174 
by (insert abs_le_D1 [of " a"], simp) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1175 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1176 
lemma abs_le_iff: "\<bar>a\<bar> \<le> b \<longleftrightarrow> a \<le> b \<and>  a \<le> b" 
29667  1177 
by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1178 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1179 
lemma abs_triangle_ineq2: "\<bar>a\<bar>  \<bar>b\<bar> \<le> \<bar>a  b\<bar>" 
36302  1180 
proof  
1181 
have "\<bar>a\<bar> = \<bar>b + (a  b)\<bar>" 

1182 
by (simp add: algebra_simps add_diff_cancel) 

1183 
then have "\<bar>a\<bar> \<le> \<bar>b\<bar> + \<bar>a  b\<bar>" 

1184 
by (simp add: abs_triangle_ineq) 

1185 
then show ?thesis 

1186 
by (simp add: algebra_simps) 

1187 
qed 

1188 

1189 
lemma abs_triangle_ineq2_sym: "\<bar>a\<bar>  \<bar>b\<bar> \<le> \<bar>b  a\<bar>" 

1190 
by (simp only: abs_minus_commute [of b] abs_triangle_ineq2) 

16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1191 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1192 
lemma abs_triangle_ineq3: "\<bar>\<bar>a\<bar>  \<bar>b\<bar>\<bar> \<le> \<bar>a  b\<bar>" 
36302  1193 
by (simp add: abs_le_iff abs_triangle_ineq2 abs_triangle_ineq2_sym) 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1194 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1195 
lemma abs_triangle_ineq4: "\<bar>a  b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1196 
proof  
36302  1197 
have "\<bar>a  b\<bar> = \<bar>a +  b\<bar>" by (subst diff_minus, rule refl) 
1198 
also have "... \<le> \<bar>a\<bar> + \<bar> b\<bar>" by (rule abs_triangle_ineq) 

29667  1199 
finally show ?thesis by simp 
25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1200 
qed 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1201 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1202 
lemma abs_diff_triangle_ineq: "\<bar>a + b  (c + d)\<bar> \<le> \<bar>a  c\<bar> + \<bar>b  d\<bar>" 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1203 
proof  
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1204 
have "\<bar>a + b  (c+d)\<bar> = \<bar>(ac) + (bd)\<bar>" by (simp add: diff_minus add_ac) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1205 
also have "... \<le> \<bar>ac\<bar> + \<bar>bd\<bar>" by (rule abs_triangle_ineq) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1206 
finally show ?thesis . 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1207 
qed 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16417
diff
changeset

1208 

25303
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1209 
lemma abs_add_abs [simp]: 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1210 
"\<bar>\<bar>a\<bar> + \<bar>b\<bar>\<bar> = \<bar>a\<bar> + \<bar>b\<bar>" (is "?L = ?R") 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1211 
proof (rule antisym) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1212 
show "?L \<ge> ?R" by(rule abs_ge_self) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1213 
next 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1214 
have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq) 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1215 
also have "\<dots> = ?R" by simp 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1216 
finally show "?L \<le> ?R" . 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1217 
qed 
0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1218 

0699e20feabd
renamed lordered_*_* to lordered_*_add_*; further localization
haftmann
parents:
25267
diff
changeset

1219 
end 
14738  1220 

15178  1221 

25090  1222 
subsection {* Tools setup *} 
1223 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35723
diff
changeset

1224 
lemma add_mono_thms_linordered_semiring [no_atp]: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1225 
fixes i j k :: "'a\<Colon>ordered_ab_semigroup_add" 
25077  1226 
shows "i \<le> j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" 
1227 
and "i = j \<and> k \<le> l \<Longrightarrow> i + k \<le> j + l" 

1228 
and "i \<le> j \<and> k = l \<Longrightarrow> i + k \<le> j + l" 

1229 
and "i = j \<and> k = l \<Longrightarrow> i + k = j + l" 

1230 
by (rule add_mono, clarify+)+ 

1231 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35723
diff
changeset

1232 
lemma add_mono_thms_linordered_field [no_atp]: 
35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34973
diff
changeset

1233 
fixes i j k :: "'a\<Colon>ordered_cancel_ab_semigroup_add" 
25077  1234 
shows "i < j \<and> k = l \<Longrightarrow> i + k < j + l" 
1235 
and "i = j \<and> k < l \<Longrightarrow> i + k < j + l" 

1236 
and "i < j \<and> k \<le> l \<Longrightarrow> i + k < j + l" 

1237 
and "i \<le> j \<and> k < l \<Longrightarrow> i + k < j + l" 

1238 
and "i < j \<and> k < l \<Longrightarrow> i + k < j + l" 

1239 
by (auto intro: add_strict_right_mono add_strict_left_mono 

1240 
add_less_le_mono add_le_less_mono add_strict_mono) 

1241 

33364  1242 
code_modulename SML 
35050
9f841f20dca6
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
haftmann
parents:
35036
diff
changeset

1243 
Groups Arith 
33364  1244 

1245 
code_modulename OCaml 

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

1246 
Groups Arith 
33364  1247 

1248 
code_modulename Haskell 

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

1249 
Groups Arith 
33364  1250 

37889
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

1251 

0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

1252 
text {* Legacy *} 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

1253 

0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

1254 
lemmas diff_def = diff_minus 
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

1255 

14738  1256 
end 