author  haftmann 
Mon, 04 Nov 2013 20:10:09 +0100  
changeset 54250  7d2544dd3988 
parent 54230  b1d955791529 
child 54703  499f92dc6e45 
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 
15131  9 
begin 
14738  10 

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

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

12 

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

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

16 
val name = @{binding ac_simps} 

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

19 
*} 

20 

21 
setup Ac_Simps.setup 

22 

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

23 
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

24 
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

25 
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

26 
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

27 
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

28 

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

30 
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

31 

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

35 
val name = @{binding algebra_simps} 

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

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

37 
) 
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 
setup Algebra_Simps.setup 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

41 

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

42 
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

43 
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

44 
(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

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

46 

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

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

50 
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

51 
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

52 
) 
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 
setup Field_Simps.setup 
35301
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

56 

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 
subsection {* Abstract structures *} 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

59 

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

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

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

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

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

64 
*} 
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 
locale semigroup = 
90e42f9ba4d1
distributed theory Algebras to theories Groups and Lattices
haftmann
parents:
35267
diff
changeset

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

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

69 

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

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

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

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

73 

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

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

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

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

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

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

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

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

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

82 

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

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

84 

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

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

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

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

90 
locale comm_monoid = abel_semigroup + 

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

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

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

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

94 
sublocale comm_monoid < monoid 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

95 
by default (simp_all add: commute comm_neutral) 
35720  96 

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

97 

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

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

99 

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

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

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

102 

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

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

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

105 

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

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

107 

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

108 
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

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

110 

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

111 
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

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

113 

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

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

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

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

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

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

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

122 
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

123 

52143  124 
typed_print_translation {* 
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

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

126 
fun tr' c = (c, fn ctxt => fn T => fn ts => 
52210
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52143
diff
changeset

127 
if null ts andalso Printer.type_emphasis ctxt T then 
42248  128 
Syntax.const @{syntax_const "_constrain"} $ Syntax.const c $ 
52210
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52143
diff
changeset

129 
Syntax_Phases.term_of_typ ctxt T 
0226035df99d
more explicit Printer.type_emphasis, depending on show_type_emphasis;
wenzelm
parents:
52143
diff
changeset

130 
else raise Match); 
42247
12fe41a92cd5
typed_print_translation: discontinued show_sorts argument;
wenzelm
parents:
42245
diff
changeset

131 
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

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

133 

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

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

135 
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

136 

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

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

138 
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

139 

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

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

141 
fixes uminus :: "'a \<Rightarrow> 'a" (" _" [81] 80) 
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 times = 
8dfd816713c6
moved remaning class operations from Algebras.thy to Groups.thy
haftmann
parents:
35216
diff
changeset

144 
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

145 

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

146 

23085  147 
subsection {* Semigroups and Monoids *} 
14738  148 

22390  149 
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

150 
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

151 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

152 
sublocale semigroup_add < add!: semigroup plus 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

153 
by default (fact add_assoc) 
22390  154 

155 
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

156 
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

157 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

158 
sublocale ab_semigroup_add < add!: abel_semigroup plus 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

159 
by default (fact add_commute) 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

160 

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

161 
context ab_semigroup_add 
25062  162 
begin 
14738  163 

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

164 
lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute 
25062  165 

166 
theorems add_ac = add_assoc add_commute add_left_commute 

167 

168 
end 

14738  169 

170 
theorems add_ac = add_assoc add_commute add_left_commute 

171 

22390  172 
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

173 
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

174 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

175 
sublocale semigroup_mult < mult!: semigroup times 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

176 
by default (fact mult_assoc) 
14738  177 

22390  178 
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

179 
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

180 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

181 
sublocale ab_semigroup_mult < mult!: abel_semigroup times 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

182 
by default (fact mult_commute) 
34973
ae634fad947e
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
haftmann
parents:
34147
diff
changeset

183 

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

184 
context ab_semigroup_mult 
23181  185 
begin 
14738  186 

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

187 
lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute 
25062  188 

189 
theorems mult_ac = mult_assoc mult_commute mult_left_commute 

23181  190 

191 
end 

14738  192 

193 
theorems mult_ac = mult_assoc mult_commute mult_left_commute 

194 

23085  195 
class monoid_add = zero + semigroup_add + 
35720  196 
assumes add_0_left: "0 + a = a" 
197 
and add_0_right: "a + 0 = a" 

198 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

199 
sublocale monoid_add < add!: monoid plus 0 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

200 
by default (fact add_0_left add_0_right)+ 
23085  201 

26071  202 
lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0" 
29667  203 
by (rule eq_commute) 
26071  204 

22390  205 
class comm_monoid_add = zero + ab_semigroup_add + 
25062  206 
assumes add_0: "0 + a = a" 
23085  207 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

208 
sublocale comm_monoid_add < add!: comm_monoid plus 0 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

209 
by default (insert add_0, simp add: ac_simps) 
25062  210 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

211 
subclass (in comm_monoid_add) monoid_add 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

212 
by default (fact add.left_neutral add.right_neutral)+ 
14738  213 

49388  214 
class comm_monoid_diff = comm_monoid_add + minus + 
215 
assumes diff_zero [simp]: "a  0 = a" 

216 
and zero_diff [simp]: "0  a = 0" 

217 
and add_diff_cancel_left [simp]: "(c + a)  (c + b) = a  b" 

218 
and diff_diff_add: "a  b  c = a  (b + c)" 

219 
begin 

220 

221 
lemma add_diff_cancel_right [simp]: 

222 
"(a + c)  (b + c) = a  b" 

223 
using add_diff_cancel_left [symmetric] by (simp add: add.commute) 

224 

225 
lemma add_diff_cancel_left' [simp]: 

226 
"(b + a)  b = a" 

227 
proof  

228 
have "(b + a)  (b + 0) = a" by (simp only: add_diff_cancel_left diff_zero) 

229 
then show ?thesis by simp 

230 
qed 

231 

232 
lemma add_diff_cancel_right' [simp]: 

233 
"(a + b)  b = a" 

234 
using add_diff_cancel_left' [symmetric] by (simp add: add.commute) 

235 

236 
lemma diff_add_zero [simp]: 

237 
"a  (a + b) = 0" 

238 
proof  

239 
have "a  (a + b) = (a + 0)  (a + b)" by simp 

240 
also have "\<dots> = 0" by (simp only: add_diff_cancel_left zero_diff) 

241 
finally show ?thesis . 

242 
qed 

243 

244 
lemma diff_cancel [simp]: 

245 
"a  a = 0" 

246 
proof  

247 
have "(a + 0)  (a + 0) = 0" by (simp only: add_diff_cancel_left diff_zero) 

248 
then show ?thesis by simp 

249 
qed 

250 

251 
lemma diff_right_commute: 

252 
"a  c  b = a  b  c" 

253 
by (simp add: diff_diff_add add.commute) 

254 

255 
lemma add_implies_diff: 

256 
assumes "c + b = a" 

257 
shows "c = a  b" 

258 
proof  

259 
from assms have "(b + c)  (b + 0) = a  b" by (simp add: add.commute) 

260 
then show "c = a  b" by simp 

261 
qed 

262 

263 
end 

264 

22390  265 
class monoid_mult = one + semigroup_mult + 
35720  266 
assumes mult_1_left: "1 * a = a" 
267 
and mult_1_right: "a * 1 = a" 

268 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

269 
sublocale monoid_mult < mult!: monoid times 1 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

270 
by default (fact mult_1_left mult_1_right)+ 
14738  271 

26071  272 
lemma one_reorient: "1 = x \<longleftrightarrow> x = 1" 
29667  273 
by (rule eq_commute) 
26071  274 

22390  275 
class comm_monoid_mult = one + ab_semigroup_mult + 
25062  276 
assumes mult_1: "1 * a = a" 
14738  277 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

278 
sublocale comm_monoid_mult < mult!: comm_monoid times 1 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

279 
by default (insert mult_1, simp add: ac_simps) 
25062  280 

51546
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

281 
subclass (in comm_monoid_mult) monoid_mult 
2e26df807dc7
more uniform style for interpretation and sublocale declarations
haftmann
parents:
49690
diff
changeset

282 
by default (fact mult.left_neutral mult.right_neutral)+ 
14738  283 

22390  284 
class cancel_semigroup_add = semigroup_add + 
25062  285 
assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" 
286 
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

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

288 

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

289 
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

290 
"a + b = a + c \<longleftrightarrow> b = c" 
29667  291 
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

292 

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

293 
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

294 
"b + a = c + a \<longleftrightarrow> b = c" 
29667  295 
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

296 

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

297 
end 
14738  298 

22390  299 
class cancel_ab_semigroup_add = ab_semigroup_add + 
25062  300 
assumes add_imp_eq: "a + b = a + c \<Longrightarrow> b = c" 
25267  301 
begin 
14738  302 

25267  303 
subclass cancel_semigroup_add 
28823  304 
proof 
22390  305 
fix a b c :: 'a 
306 
assume "a + b = a + c" 

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

308 
next 

14738  309 
fix a b c :: 'a 
310 
assume "b + a = c + a" 

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

14738  313 
qed 
314 

25267  315 
end 
316 

29904  317 
class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add 
318 

319 

23085  320 
subsection {* Groups *} 
321 

25762  322 
class group_add = minus + uminus + monoid_add + 
25062  323 
assumes left_minus [simp]: " a + a = 0" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

324 
assumes add_uminus_conv_diff [simp]: "a + ( b) = a  b" 
25062  325 
begin 
23085  326 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

327 
lemma diff_conv_add_uminus: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

328 
"a  b = a + ( b)" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

329 
by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

330 

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

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

332 
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

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

334 
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

335 
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

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

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

338 

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

341 
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

342 
thus " 0 = 0" by (rule minus_unique) 
14738  343 
qed 
344 

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

347 
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

348 
thus " ( a) = a" by (rule minus_unique) 
23085  349 
qed 
14738  350 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

351 
lemma right_minus: "a +  a = 0" 
14738  352 
proof  
25062  353 
have "a +  a =  ( a) +  a" by simp 
354 
also have "\<dots> = 0" by (rule left_minus) 

14738  355 
finally show ?thesis . 
356 
qed 

357 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

358 
lemma diff_self [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

359 
"a  a = 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

360 
using right_minus [of a] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

361 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

375 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

376 
lemma minus_add_cancel [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

377 
" a + (a + b) = b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

378 
by (simp add: add_assoc [symmetric]) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

379 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

380 
lemma add_minus_cancel [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

381 
"a + ( a + b) = b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

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

383 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

384 
lemma diff_add_cancel [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

385 
"a  b + b = a" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

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

387 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

388 
lemma add_diff_cancel [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

389 
"a + b  b = a" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

390 
by (simp only: diff_conv_add_uminus add_assoc) simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

391 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

392 
lemma minus_add: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

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

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

395 
have "(a + b) + ( b +  a) = 0" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

396 
by (simp only: add_assoc add_minus_cancel) simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

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

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

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

400 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

401 
lemma right_minus_eq [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

402 
"a  b = 0 \<longleftrightarrow> a = b" 
14738  403 
proof 
23085  404 
assume "a  b = 0" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

405 
have "a = (a  b) + b" by (simp add: add_assoc) 
23085  406 
also have "\<dots> = b" using `a  b = 0` by simp 
407 
finally show "a = b" . 

14738  408 
next 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

409 
assume "a = b" thus "a  b = 0" by simp 
14738  410 
qed 
411 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

412 
lemma eq_iff_diff_eq_0: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

413 
"a = b \<longleftrightarrow> a  b = 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

414 
by (fact right_minus_eq [symmetric]) 
14738  415 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

416 
lemma diff_0 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

417 
"0  a =  a" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

418 
by (simp only: diff_conv_add_uminus add_0_left) 
14738  419 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

420 
lemma diff_0_right [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

421 
"a  0 = a" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

422 
by (simp only: diff_conv_add_uminus minus_zero add_0_right) 
14738  423 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

424 
lemma diff_minus_eq_add [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

425 
"a   b = a + b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

426 
by (simp only: diff_conv_add_uminus minus_minus) 
14738  427 

25062  428 
lemma neg_equal_iff_equal [simp]: 
429 
" a =  b \<longleftrightarrow> a = b" 

14738  430 
proof 
431 
assume " a =  b" 

29667  432 
hence " ( a) =  ( b)" by simp 
25062  433 
thus "a = b" by simp 
14738  434 
next 
25062  435 
assume "a = b" 
436 
thus " a =  b" by simp 

14738  437 
qed 
438 

25062  439 
lemma neg_equal_0_iff_equal [simp]: 
440 
" a = 0 \<longleftrightarrow> a = 0" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

441 
by (subst neg_equal_iff_equal [symmetric]) simp 
14738  442 

25062  443 
lemma neg_0_equal_iff_equal [simp]: 
444 
"0 =  a \<longleftrightarrow> 0 = a" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

445 
by (subst neg_equal_iff_equal [symmetric]) simp 
14738  446 

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

448 

25062  449 
lemma equation_minus_iff: 
450 
"a =  b \<longleftrightarrow> b =  a" 

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

454 
qed 

455 

456 
lemma minus_equation_iff: 

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

458 
proof  

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

14738  460 
thus ?thesis by (simp add: eq_commute) 
461 
qed 

462 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

463 
lemma eq_neg_iff_add_eq_0: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

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

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

466 
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

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

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

469 
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

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

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

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

473 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

474 
lemma add_eq_0_iff2: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

475 
"a + b = 0 \<longleftrightarrow> a =  b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

476 
by (fact eq_neg_iff_add_eq_0 [symmetric]) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

477 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

478 
lemma neg_eq_iff_add_eq_0: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

479 
" a = b \<longleftrightarrow> a + b = 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

480 
by (auto simp add: add_eq_0_iff2) 
44348  481 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

482 
lemma add_eq_0_iff: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

483 
"a + b = 0 \<longleftrightarrow> b =  a" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

484 
by (auto simp add: neg_eq_iff_add_eq_0 [symmetric]) 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

485 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

486 
lemma minus_diff_eq [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

487 
" (a  b) = b  a" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

488 
by (simp only: neg_eq_iff_add_eq_0 diff_conv_add_uminus add_assoc minus_add_cancel) simp 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

489 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

490 
lemma add_diff_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

491 
"a + (b  c) = (a + b)  c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

492 
by (simp only: diff_conv_add_uminus add_assoc) 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

493 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

494 
lemma diff_add_eq_diff_diff_swap: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

495 
"a  (b + c) = a  c  b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

496 
by (simp only: diff_conv_add_uminus add_assoc minus_add) 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

497 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

498 
lemma diff_eq_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

499 
"a  b = c \<longleftrightarrow> a = c + b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

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

501 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

502 
lemma eq_diff_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

503 
"a = c  b \<longleftrightarrow> a + b = c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

504 
by auto 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

505 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

506 
lemma diff_diff_eq2 [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

507 
"a  (b  c) = (a + c)  b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

508 
by (simp only: diff_conv_add_uminus add_assoc) simp 
45548
3e2722d66169
Groups.thy: generalize several lemmas from class ab_group_add to class group_add
huffman
parents:
45294
diff
changeset

509 

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

510 
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

511 
"a  b = c  d \<Longrightarrow> a = b \<longleftrightarrow> c = d" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

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

513 

25062  514 
end 
515 

25762  516 
class ab_group_add = minus + uminus + comm_monoid_add + 
25062  517 
assumes ab_left_minus: " a + a = 0" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

518 
assumes ab_add_uminus_conv_diff: "a  b = a + ( b)" 
25267  519 
begin 
25062  520 

25267  521 
subclass group_add 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

522 
proof qed (simp_all add: ab_left_minus ab_add_uminus_conv_diff) 
25062  523 

29904  524 
subclass cancel_comm_monoid_add 
28823  525 
proof 
25062  526 
fix a b c :: 'a 
527 
assume "a + b = a + c" 

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

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

529 
by (simp only: add_assoc) 
25062  530 
then show "b = c" by simp 
531 
qed 

532 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

533 
lemma uminus_add_conv_diff [simp]: 
25062  534 
" a + b = b  a" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

535 
by (simp add: add_commute) 
25062  536 

537 
lemma minus_add_distrib [simp]: 

538 
" (a + b) =  a +  b" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

539 
by (simp add: algebra_simps) 
25062  540 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

541 
lemma diff_add_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

542 
"(a  b) + c = (a + c)  b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

543 
by (simp add: algebra_simps) 
25077  544 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

545 
lemma diff_diff_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

546 
"(a  b)  c = a  (b + c)" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

547 
by (simp add: algebra_simps) 
30629  548 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

549 
lemma diff_add_eq_diff_diff: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

550 
"a  (b + c) = a  b  c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

551 
using diff_add_eq_diff_diff_swap [of a c b] by (simp add: add.commute) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

552 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

553 
lemma add_diff_cancel_left [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

554 
"(c + a)  (c + b) = a  b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

555 
by (simp add: algebra_simps) 
48556
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

556 

25062  557 
end 
14738  558 

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

559 

14738  560 
subsection {* (Partially) Ordered Groups *} 
561 

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

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

563 
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

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

565 
\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

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

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

568 
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

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

570 
\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

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

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

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

574 

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

575 
class ordered_ab_semigroup_add = order + ab_semigroup_add + 
25062  576 
assumes add_left_mono: "a \<le> b \<Longrightarrow> c + a \<le> c + b" 
577 
begin 

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

578 

25062  579 
lemma add_right_mono: 
580 
"a \<le> b \<Longrightarrow> a + c \<le> b + c" 

29667  581 
by (simp add: add_commute [of _ c] add_left_mono) 
14738  582 

583 
text {* nonstrict, in both arguments *} 

584 
lemma add_mono: 

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

588 
done 

589 

25062  590 
end 
591 

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

592 
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

593 
ordered_ab_semigroup_add + cancel_ab_semigroup_add 
25062  594 
begin 
595 

14738  596 
lemma add_strict_left_mono: 
25062  597 
"a < b \<Longrightarrow> c + a < c + b" 
29667  598 
by (auto simp add: less_le add_left_mono) 
14738  599 

600 
lemma add_strict_right_mono: 

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

604 
text{*Strict monotonicity in both arguments*} 

25062  605 
lemma add_strict_mono: 
606 
"a < b \<Longrightarrow> c < d \<Longrightarrow> a + c < b + d" 

607 
apply (erule add_strict_right_mono [THEN less_trans]) 

14738  608 
apply (erule add_strict_left_mono) 
609 
done 

610 

611 
lemma add_less_le_mono: 

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

614 
apply (erule add_left_mono) 

14738  615 
done 
616 

617 
lemma add_le_less_mono: 

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

14738  620 
apply (erule add_strict_left_mono) 
621 
done 

622 

25062  623 
end 
624 

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

625 
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

626 
ordered_cancel_ab_semigroup_add + 
25062  627 
assumes add_le_imp_le_left: "c + a \<le> c + b \<Longrightarrow> a \<le> b" 
628 
begin 

629 

14738  630 
lemma add_less_imp_less_left: 
29667  631 
assumes less: "c + a < c + b" shows "a < b" 
14738  632 
proof  
633 
from less have le: "c + a <= c + b" by (simp add: order_le_less) 

634 
have "a <= b" 

635 
apply (insert le) 

636 
apply (drule add_le_imp_le_left) 

637 
by (insert le, drule add_le_imp_le_left, assumption) 

638 
moreover have "a \<noteq> b" 

639 
proof (rule ccontr) 

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

641 
then have "a = b" by simp 

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

643 
with less show "False"by simp 

644 
qed 

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

646 
qed 

647 

648 
lemma add_less_imp_less_right: 

25062  649 
"a + c < b + c \<Longrightarrow> a < b" 
14738  650 
apply (rule add_less_imp_less_left [of c]) 
651 
apply (simp add: add_commute) 

652 
done 

653 

654 
lemma add_less_cancel_left [simp]: 

25062  655 
"c + a < c + b \<longleftrightarrow> a < b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

656 
by (blast intro: add_less_imp_less_left add_strict_left_mono) 
14738  657 

658 
lemma add_less_cancel_right [simp]: 

25062  659 
"a + c < b + c \<longleftrightarrow> a < b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

660 
by (blast intro: add_less_imp_less_right add_strict_right_mono) 
14738  661 

662 
lemma add_le_cancel_left [simp]: 

25062  663 
"c + a \<le> c + b \<longleftrightarrow> a \<le> b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

664 
by (auto, drule add_le_imp_le_left, simp_all add: add_left_mono) 
14738  665 

666 
lemma add_le_cancel_right [simp]: 

25062  667 
"a + c \<le> b + c \<longleftrightarrow> a \<le> b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

668 
by (simp add: add_commute [of a c] add_commute [of b c]) 
14738  669 

670 
lemma add_le_imp_le_right: 

25062  671 
"a + c \<le> b + c \<Longrightarrow> a \<le> b" 
29667  672 
by simp 
25062  673 

25077  674 
lemma max_add_distrib_left: 
675 
"max x y + z = max (x + z) (y + z)" 

676 
unfolding max_def by auto 

677 

678 
lemma min_add_distrib_left: 

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

680 
unfolding min_def by auto 

681 

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

682 
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

683 
"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

684 
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

685 

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

686 
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

687 
"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

688 
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

689 

25062  690 
end 
691 

52289  692 
class ordered_cancel_comm_monoid_diff = comm_monoid_diff + ordered_ab_semigroup_add_imp_le + 
693 
assumes le_iff_add: "a \<le> b \<longleftrightarrow> (\<exists>c. b = a + c)" 

694 
begin 

695 

696 
context 

697 
fixes a b 

698 
assumes "a \<le> b" 

699 
begin 

700 

701 
lemma add_diff_inverse: 

702 
"a + (b  a) = b" 

703 
using `a \<le> b` by (auto simp add: le_iff_add) 

704 

705 
lemma add_diff_assoc: 

706 
"c + (b  a) = c + b  a" 

707 
using `a \<le> b` by (auto simp add: le_iff_add add_left_commute [of c]) 

708 

709 
lemma add_diff_assoc2: 

710 
"b  a + c = b + c  a" 

711 
using `a \<le> b` by (auto simp add: le_iff_add add_assoc) 

712 

713 
lemma diff_add_assoc: 

714 
"c + b  a = c + (b  a)" 

715 
using `a \<le> b` by (simp add: add_commute add_diff_assoc) 

716 

717 
lemma diff_add_assoc2: 

718 
"b + c  a = b  a + c" 

719 
using `a \<le> b`by (simp add: add_commute add_diff_assoc) 

720 

721 
lemma diff_diff_right: 

722 
"c  (b  a) = c + a  b" 

723 
by (simp add: add_diff_inverse add_diff_cancel_left [of a c "b  a", symmetric] add_commute) 

724 

725 
lemma diff_add: 

726 
"b  a + a = b" 

727 
by (simp add: add_commute add_diff_inverse) 

728 

729 
lemma le_add_diff: 

730 
"c \<le> b + c  a" 

731 
by (auto simp add: add_commute diff_add_assoc2 le_iff_add) 

732 

733 
lemma le_imp_diff_is_add: 

734 
"a \<le> b \<Longrightarrow> b  a = c \<longleftrightarrow> b = c + a" 

735 
by (auto simp add: add_commute add_diff_inverse) 

736 

737 
lemma le_diff_conv2: 

738 
"c \<le> b  a \<longleftrightarrow> c + a \<le> b" (is "?P \<longleftrightarrow> ?Q") 

739 
proof 

740 
assume ?P 

741 
then have "c + a \<le> b  a + a" by (rule add_right_mono) 

742 
then show ?Q by (simp add: add_diff_inverse add_commute) 

743 
next 

744 
assume ?Q 

745 
then have "a + c \<le> a + (b  a)" by (simp add: add_diff_inverse add_commute) 

746 
then show ?P by simp 

747 
qed 

748 

749 
end 

750 

751 
end 

752 

753 

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

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

755 

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

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

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

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

759 

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

760 
lemma add_pos_nonneg: 
29667  761 
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

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

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

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

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

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

767 

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

768 
lemma add_pos_pos: 
29667  769 
assumes "0 < a" and "0 < b" shows "0 < a + b" 
770 
by (rule add_pos_nonneg) (insert assms, auto) 

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

771 

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

772 
lemma add_nonneg_pos: 
29667  773 
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

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

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

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

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

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

779 

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

780 
lemma add_nonneg_nonneg [simp]: 
29667  781 
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

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

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

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

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

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

787 

30691  788 
lemma add_neg_nonpos: 
29667  789 
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

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

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

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

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

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

795 

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

796 
lemma add_neg_neg: 
29667  797 
assumes "a < 0" and "b < 0" shows "a + b < 0" 
798 
by (rule add_neg_nonpos) (insert assms, auto) 

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

799 

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

800 
lemma add_nonpos_neg: 
29667  801 
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

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

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

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

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

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

807 

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

808 
lemma add_nonpos_nonpos: 
29667  809 
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

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

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

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

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

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

815 

30691  816 
lemmas add_sign_intros = 
817 
add_pos_nonneg add_pos_pos add_nonneg_pos add_nonneg_nonneg 

818 
add_neg_nonpos add_neg_neg add_nonpos_neg add_nonpos_nonpos 

819 

29886  820 
lemma add_nonneg_eq_0_iff: 
821 
assumes x: "0 \<le> x" and y: "0 \<le> y" 

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

823 
proof (intro iffI conjI) 

824 
have "x = x + 0" by simp 

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

826 
also assume "x + y = 0" 

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

828 
finally show "x = 0" . 

829 
next 

830 
have "y = 0 + y" by simp 

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

832 
also assume "x + y = 0" 

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

834 
finally show "y = 0" . 

835 
next 

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

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

838 
qed 

839 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

840 
lemma add_increasing: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

841 
"0 \<le> a \<Longrightarrow> b \<le> c \<Longrightarrow> b \<le> a + c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

842 
by (insert add_mono [of 0 a b c], simp) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

843 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

844 
lemma add_increasing2: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

845 
"0 \<le> c \<Longrightarrow> b \<le> a \<Longrightarrow> b \<le> a + c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

846 
by (simp add: add_increasing add_commute [of a]) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

847 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

848 
lemma add_strict_increasing: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

849 
"0 < a \<Longrightarrow> b \<le> c \<Longrightarrow> b < a + c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

850 
by (insert add_less_le_mono [of 0 a b c], simp) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

851 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

852 
lemma add_strict_increasing2: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

853 
"0 \<le> a \<Longrightarrow> b < c \<Longrightarrow> b < a + c" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

854 
by (insert add_le_less_mono [of 0 a b c], simp) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

855 

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

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

857 

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

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

859 
ab_group_add + ordered_ab_semigroup_add 
25062  860 
begin 
861 

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

862 
subclass ordered_cancel_ab_semigroup_add .. 
25062  863 

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

864 
subclass ordered_ab_semigroup_add_imp_le 
28823  865 
proof 
25062  866 
fix a b c :: 'a 
867 
assume "c + a \<le> c + b" 

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

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

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

871 
qed 

872 

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

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

874 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

875 
lemma add_less_same_cancel1 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

876 
"b + a < b \<longleftrightarrow> a < 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

877 
using add_less_cancel_left [of _ _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

878 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

879 
lemma add_less_same_cancel2 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

880 
"a + b < b \<longleftrightarrow> a < 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

881 
using add_less_cancel_right [of _ _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

882 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

883 
lemma less_add_same_cancel1 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

884 
"a < a + b \<longleftrightarrow> 0 < b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

885 
using add_less_cancel_left [of _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

886 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

887 
lemma less_add_same_cancel2 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

888 
"a < b + a \<longleftrightarrow> 0 < b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

889 
using add_less_cancel_right [of 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

890 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

891 
lemma add_le_same_cancel1 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

892 
"b + a \<le> b \<longleftrightarrow> a \<le> 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

893 
using add_le_cancel_left [of _ _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

894 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

895 
lemma add_le_same_cancel2 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

896 
"a + b \<le> b \<longleftrightarrow> a \<le> 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

897 
using add_le_cancel_right [of _ _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

898 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

899 
lemma le_add_same_cancel1 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

900 
"a \<le> a + b \<longleftrightarrow> 0 \<le> b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

901 
using add_le_cancel_left [of _ 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

902 

b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

903 
lemma le_add_same_cancel2 [simp]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

904 
"a \<le> b + a \<longleftrightarrow> 0 \<le> b" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

905 
using add_le_cancel_right [of 0] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

906 

25077  907 
lemma max_diff_distrib_left: 
908 
shows "max x y  z = max (x  z) (y  z)" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

909 
using max_add_distrib_left [of x y " z"] by simp 
25077  910 

911 
lemma min_diff_distrib_left: 

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

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

913 
using min_add_distrib_left [of x y " z"] by simp 
25077  914 

915 
lemma le_imp_neg_le: 

29667  916 
assumes "a \<le> b" shows "b \<le> a" 
25077  917 
proof  
29667  918 
have "a+a \<le> a+b" using `a \<le> b` by (rule add_left_mono) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

919 
then have "0 \<le> a+b" by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

920 
then have "0 + (b) \<le> (a + b) + (b)" by (rule add_right_mono) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

921 
then show ?thesis by (simp add: algebra_simps) 
25077  922 
qed 
923 

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

925 
proof 

926 
assume " b \<le>  a" 

29667  927 
hence " ( a) \<le>  ( b)" by (rule le_imp_neg_le) 
25077  928 
thus "a\<le>b" by simp 
929 
next 

930 
assume "a\<le>b" 

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

932 
qed 

933 

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

29667  935 
by (subst neg_le_iff_le [symmetric], simp) 
25077  936 

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

29667  938 
by (subst neg_le_iff_le [symmetric], simp) 
25077  939 

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

29667  941 
by (force simp add: less_le) 
25077  942 

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

29667  944 
by (subst neg_less_iff_less [symmetric], simp) 
25077  945 

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

29667  947 
by (subst neg_less_iff_less [symmetric], simp) 
25077  948 

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

950 

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

952 
proof  

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

954 
thus ?thesis by simp 

955 
qed 

956 

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

958 
proof  

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

960 
thus ?thesis by simp 

961 
qed 

962 

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

964 
proof  

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

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

967 
apply (auto simp only: le_less) 

968 
apply (drule mm) 

969 
apply (simp_all) 

970 
apply (drule mm[simplified], assumption) 

971 
done 

972 
then show ?thesis by simp 

973 
qed 

974 

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

29667  976 
by (auto simp add: le_less minus_less_iff) 
25077  977 

54148  978 
lemma diff_less_0_iff_less [simp]: 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

979 
"a  b < 0 \<longleftrightarrow> a < b" 
25077  980 
proof  
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

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

982 
also have "... \<longleftrightarrow> a < b" by (simp only: add_less_cancel_right) 
25077  983 
finally show ?thesis . 
984 
qed 

985 

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

986 
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

987 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

988 
lemma diff_less_eq [algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

989 
"a  b < c \<longleftrightarrow> a < c + b" 
25077  990 
apply (subst less_iff_diff_less_0 [of a]) 
991 
apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

992 
apply (simp add: algebra_simps) 
25077  993 
done 
994 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

995 
lemma less_diff_eq[algebra_simps, field_simps]: 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

996 
"a < c  b \<longleftrightarrow> a + b < c" 
36302  997 
apply (subst less_iff_diff_less_0 [of "a + b"]) 
25077  998 
apply (subst less_iff_diff_less_0 [of a]) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

999 
apply (simp add: algebra_simps) 
25077  1000 
done 
1001 

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

1002 
lemma diff_le_eq[algebra_simps, field_simps]: "a  b \<le> c \<longleftrightarrow> a \<le> c + b" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

1003 
by (auto simp add: le_less diff_less_eq ) 
25077  1004 

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

1005 
lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c  b \<longleftrightarrow> a + b \<le> c" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
54148
diff
changeset

1006 
by (auto simp add: le_less less_diff_eq) 
25077  1007 

54148  1008 
lemma diff_le_0_iff_le [simp]: 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

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

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

1011 

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

1012 
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

1013 

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

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

1015 
"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

1016 
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

1017 

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

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

1019 
"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

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

1022 
end 

1023 

48891  1024 
ML_file "Tools/group_cancel.ML" 
48556
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1025 

62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1026 
simproc_setup group_cancel_add ("a + b::'a::ab_group_add") = 
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1027 
{* fn phi => fn ss => try Group_Cancel.cancel_add_conv *} 
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1028 

62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1029 
simproc_setup group_cancel_diff ("a  b::'a::ab_group_add") = 
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1030 
{* fn phi => fn ss => try Group_Cancel.cancel_diff_conv *} 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1031 

48556
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1032 
simproc_setup group_cancel_eq ("a = (b::'a::ab_group_add)") = 
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1033 
{* fn phi => fn ss => try Group_Cancel.cancel_eq_conv *} 
37889
0d8058e0c270
keep explicit diff_def as legacy theorem; modernized abel_cancel simproc setup
haftmann
parents:
37884
diff
changeset

1034 

48556
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1035 
simproc_setup group_cancel_le ("a \<le> (b::'a::ordered_ab_group_add)") = 
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1036 
{* fn phi => fn ss => try Group_Cancel.cancel_le_conv *} 
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1037 

62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1038 
simproc_setup group_cancel_less ("a < (b::'a::ordered_ab_group_add)") = 
62a3fbf9d35b
replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
huffman
parents:
45548
diff
changeset

1039 
{* fn phi => fn ss => try Group_Cancel.cancel_less_conv *} 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36977
diff
changeset

1040 

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

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

1042 
linorder + ordered_ab_semigroup_add 
25062  1043 

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

1044 
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

1045 
linorder + ordered_cancel_ab_semigroup_add 
25267  1046 
begin 
25062  1047 

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

1048 
subclass linordered_ab_semigroup_add .. 
25062  1049 

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

1050 
subclass ordered_ab_semigroup_add_imp_le 
28823  1051 
proof 
25062  1052 
fix a b c :: 'a 
1053 
assume le: "c + a <= c + b" 

1054 
show "a <= b" 

1055 
proof (rule ccontr) 

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

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

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

1059 
have "a = b" 

1060 
apply (insert le) 

1061 
apply (insert le2) 

1062 
apply (drule antisym, simp_all) 

1063 
done 

1064 
with w show False 

1065 
by (simp add: linorder_not_le [symmetric]) 

1066 
qed 

1067 
qed 

1068 

25267  1069 
end 
1070 

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

1071 
class linordered_ab_group_add = linorder + ordered_ab_group_add 
25267  1072 
begin 
25230  1073 

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

1074 
subclass linordered_cancel_ab_semigroup_add .. 
25230  1075 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1092 

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

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

1094 
" 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

1095 
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

1096 

54250  1097 
lemma neg_less_eq_nonneg [simp]: 
1098 
" a \<le> a \<longleftrightarrow> 0 \<le> a" 

1099 
proof 

1100 
assume A: " a \<le> a" show "0 \<le> a" 

1101 
proof (rule classical) 

1102 
assume "\<not> 0 \<le> a" 

1103 
then have "a < 0" by auto 

1104 
with A have " a < 0" by (rule le_less_trans) 

1105 
then show ?thesis by auto 

1106 
qed 

1107 
next 

1108 
assume A: "0 \<le> a" show " a \<le> a" 

1109 
proof (rule order_trans) 

1110 
show " a \<le> 0" using A by (simp add: minus_le_iff) 

1111 
next 

1112 
show "0 \<le> a" using A . 

1113 
qed 

1114 
qed 

1115 

1116 
lemma neg_less_pos [simp]: 

1117 
" a < a \<longleftrightarrow> 0 < a" 

1118 
by (auto simp add: less_le) 

1119 

1120 
lemma less_eq_neg_nonpos [simp]: 

1121 
"a \<le>  a \<longleftrightarrow> a \<le> 0" 

1122 
using neg_less_eq_nonneg [of " a"] by simp 

1123 

1124 
lemma less_neg_neg [simp]: 

1125 
"a <  a \<longleftrightarrow> a < 0" 

1126 
using neg_less_pos [of " a"] by simp 

1127 

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

1128 
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

1129 
"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

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

1131 
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

1132 
then have a: " a = a" by (rule minus_unique) 
35216  1133 
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

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

1135 

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

1136 
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

1137 
"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

1138 
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

1139 

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

1140 
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

1141 
"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

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

1143 
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

1144 
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

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

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

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

1149 
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

1150 
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

1151 
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

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

1153 

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

1154 
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

1155 
"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

1156 
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

1157 

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

1158 
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

1159 
"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

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

1161 
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

1162 
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

1163 
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

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

1165 

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

1166 
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

1167 
"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

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

1169 
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

1170 
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

1171 
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

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

1173 

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

1174 
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

1175 
" 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

1176 
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

1177 

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

1178 
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

1179 
" 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

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

1181 

25267  1182 
end 
1183 

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

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

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

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

1187 

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

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

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

1190 

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

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

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

1193 

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

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

1195 

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

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

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

1198 

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

1199 
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

1200 
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

1201 

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

1202 
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

1203 
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

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

1205 

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

1206 
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

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

1208 

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

1209 
end 
14738  1210 

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

1211 
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

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

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

1214 
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

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

1216 
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

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

1218 

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

1221 

1222 
lemma abs_of_nonneg [simp]: 

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

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

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

1228 
qed (rule abs_ge_self) 

1229 

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

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

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

1235 
proof  

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

1237 
proof (rule antisym) 

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

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

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

36302  1241 
with abs_ge_self [of " a"] have " a \<le> 0" by auto 
25307  1242 
with neg_le_0_iff_le show "0 \<le> a" by auto 
1243 
qed 

1244 
then show ?thesis by auto 

1245 
qed 

1246 

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

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

1249 

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

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

1252 
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

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

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

1255 

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

1256 
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

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

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

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

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

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

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

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

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

1265 

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

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

1268 

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

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

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

1271 
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

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

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

1274 

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

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

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

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

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

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

1280 

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

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

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

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

1284 
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

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

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

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

1288 

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

1289 
lemma abs_of_pos: "0 < a \<Longrightarrow> \<bar>a\<bar> = a" 
29667  1290 
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

1291 

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

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

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

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

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

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

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

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

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

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

1302 

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

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

1305 

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

1306 
lemma abs_le_D1: "\<bar>a\<bar> \<le> b \<Longrightarrow> a \<le> b" 
29667  1307 
by (insert abs_ge_self, blast intro: order_trans) 
25303
0699e20feabd
renamed lo 