author  wenzelm 
Thu, 20 Mar 2014 15:38:49 +0100  
changeset 56228  0f6dc7512023 
parent 54863  82acc20ded73 
child 57512  cc97b347b301 
permissions  rwrr 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

1 
(* Author: Steven Obua, TU Muenchen *) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

2 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

3 
header {* Various algebraic structures combined with a lattice *} 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

4 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

5 
theory Lattice_Algebras 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

6 
imports Complex_Main 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

7 
begin 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

8 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

9 
class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

10 
begin 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

11 

53240  12 
lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)" 
13 
apply (rule antisym) 

14 
apply (simp_all add: le_infI) 

15 
apply (rule add_le_imp_le_left [of "uminus a"]) 

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

16 
apply (simp only: add_assoc [symmetric], simp add: diff_le_eq add.commute) 
53240  17 
done 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

18 

53240  19 
lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

20 
proof  
56228  21 
have "c + inf a b = inf (c + a) (c + b)" 
53240  22 
by (simp add: add_inf_distrib_left) 
56228  23 
then show ?thesis 
24 
by (simp add: add_commute) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

25 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

26 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

27 
end 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

28 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

29 
class semilattice_sup_ab_group_add = ordered_ab_group_add + semilattice_sup 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

30 
begin 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

31 

53240  32 
lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)" 
33 
apply (rule antisym) 

34 
apply (rule add_le_imp_le_left [of "uminus a"]) 

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

35 
apply (simp only: add_assoc [symmetric], simp) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

36 
apply (simp add: le_diff_eq add.commute) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

37 
apply (rule le_supI) 
53240  38 
apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+ 
39 
done 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

40 

56228  41 
lemma add_sup_distrib_right: "sup a b + c = sup (a + c) (b + c)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

42 
proof  
56228  43 
have "c + sup a b = sup (c+a) (c+b)" 
44 
by (simp add: add_sup_distrib_left) 

45 
then show ?thesis 

46 
by (simp add: add_commute) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

47 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

48 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

49 
end 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

50 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

51 
class lattice_ab_group_add = ordered_ab_group_add + lattice 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

52 
begin 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

53 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

54 
subclass semilattice_inf_ab_group_add .. 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

55 
subclass semilattice_sup_ab_group_add .. 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

56 

53240  57 
lemmas add_sup_inf_distribs = 
58 
add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

59 

56228  60 
lemma inf_eq_neg_sup: "inf a b =  sup ( a) ( b)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

61 
proof (rule inf_unique) 
53240  62 
fix a b c :: 'a 
56228  63 
show " sup ( a) ( b) \<le> a" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

64 
by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

65 
(simp, simp add: add_sup_distrib_left) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

66 
show " sup (a) (b) \<le> b" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

67 
by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

68 
(simp, simp add: add_sup_distrib_left) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

69 
assume "a \<le> b" "a \<le> c" 
53240  70 
then show "a \<le>  sup (b) (c)" 
71 
by (subst neg_le_iff_le [symmetric]) (simp add: le_supI) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

72 
qed 
53240  73 

56228  74 
lemma sup_eq_neg_inf: "sup a b =  inf ( a) ( b)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

75 
proof (rule sup_unique) 
53240  76 
fix a b c :: 'a 
56228  77 
show "a \<le>  inf ( a) ( b)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

78 
by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

79 
(simp, simp add: add_inf_distrib_left) 
56228  80 
show "b \<le>  inf ( a) ( b)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

81 
by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

82 
(simp, simp add: add_inf_distrib_left) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

83 
assume "a \<le> c" "b \<le> c" 
56228  84 
then show " inf ( a) ( b) \<le> c" 
85 
by (subst neg_le_iff_le [symmetric]) (simp add: le_infI) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

86 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

87 

56228  88 
lemma neg_inf_eq_sup: " inf a b = sup ( a) ( b)" 
53240  89 
by (simp add: inf_eq_neg_sup) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

90 

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

91 
lemma diff_inf_eq_sup: "a  inf b c = a + sup ( b) ( c)" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

92 
using neg_inf_eq_sup [of b c, symmetric] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

93 

56228  94 
lemma neg_sup_eq_inf: " sup a b = inf ( a) ( b)" 
53240  95 
by (simp add: sup_eq_neg_inf) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

96 

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

97 
lemma diff_sup_eq_inf: "a  sup b c = a + inf ( b) ( c)" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

98 
using neg_sup_eq_inf [of b c, symmetric] by simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

99 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

100 
lemma add_eq_inf_sup: "a + b = sup a b + inf a b" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

101 
proof  
56228  102 
have "0 =  inf 0 (a  b) + inf (a  b) 0" 
53240  103 
by (simp add: inf_commute) 
56228  104 
then have "0 = sup 0 (b  a) + inf (a  b) 0" 
53240  105 
by (simp add: inf_eq_neg_sup) 
56228  106 
then have "0 = ( a + sup a b) + (inf a b + ( b))" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

107 
by (simp only: add_sup_distrib_left add_inf_distrib_right) simp 
56228  108 
then show ?thesis 
109 
by (simp add: algebra_simps) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

110 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

111 

53240  112 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

113 
subsection {* Positive Part, Negative Part, Absolute Value *} 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

114 

53240  115 
definition nprt :: "'a \<Rightarrow> 'a" 
116 
where "nprt x = inf x 0" 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

117 

53240  118 
definition pprt :: "'a \<Rightarrow> 'a" 
119 
where "pprt x = sup x 0" 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

120 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

121 
lemma pprt_neg: "pprt ( x) =  nprt x" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

122 
proof  
56228  123 
have "sup ( x) 0 = sup ( x) ( 0)" 
124 
unfolding minus_zero .. 

125 
also have "\<dots> =  inf x 0" 

126 
unfolding neg_inf_eq_sup .. 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

127 
finally have "sup ( x) 0 =  inf x 0" . 
56228  128 
then show ?thesis 
129 
unfolding pprt_def nprt_def . 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

130 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

131 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

132 
lemma nprt_neg: "nprt ( x) =  pprt x" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

133 
proof  
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

134 
from pprt_neg have "pprt ( ( x)) =  nprt ( x)" . 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

135 
then have "pprt x =  nprt ( x)" by simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

136 
then show ?thesis by simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

137 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

138 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

139 
lemma prts: "a = pprt a + nprt a" 
53240  140 
by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric]) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

141 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

142 
lemma zero_le_pprt[simp]: "0 \<le> pprt a" 
53240  143 
by (simp add: pprt_def) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

144 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

145 
lemma nprt_le_zero[simp]: "nprt a \<le> 0" 
53240  146 
by (simp add: nprt_def) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

147 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

148 
lemma le_eq_neg: "a \<le>  b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r") 
53240  149 
proof 
150 
assume ?l 

151 
then show ?r 

152 
apply  

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

153 
apply (rule add_le_imp_le_right[of _ "uminus b" _]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

154 
apply (simp add: add_assoc) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

155 
done 
53240  156 
next 
157 
assume ?r 

158 
then show ?l 

159 
apply  

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

160 
apply (rule add_le_imp_le_right[of _ "b" _]) 
53240  161 
apply simp 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

162 
done 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

163 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

164 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

165 
lemma pprt_0[simp]: "pprt 0 = 0" by (simp add: pprt_def) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

166 
lemma nprt_0[simp]: "nprt 0 = 0" by (simp add: nprt_def) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

167 

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

168 
lemma pprt_eq_id [simp, no_atp]: "0 \<le> x \<Longrightarrow> pprt x = x" 
46986  169 
by (simp add: pprt_def sup_absorb1) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

170 

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

171 
lemma nprt_eq_id [simp, no_atp]: "x \<le> 0 \<Longrightarrow> nprt x = x" 
46986  172 
by (simp add: nprt_def inf_absorb1) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

173 

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

174 
lemma pprt_eq_0 [simp, no_atp]: "x \<le> 0 \<Longrightarrow> pprt x = 0" 
46986  175 
by (simp add: pprt_def sup_absorb2) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

176 

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

177 
lemma nprt_eq_0 [simp, no_atp]: "0 \<le> x \<Longrightarrow> nprt x = 0" 
46986  178 
by (simp add: nprt_def inf_absorb2) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

179 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

180 
lemma sup_0_imp_0: "sup a ( a) = 0 \<Longrightarrow> a = 0" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

181 
proof  
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

182 
{ 
56228  183 
fix a :: 'a 
184 
assume hyp: "sup a ( a) = 0" 

185 
then have "sup a ( a) + a = a" 

186 
by simp 

187 
then have "sup (a + a) 0 = a" 

188 
by (simp add: add_sup_distrib_right) 

189 
then have "sup (a + a) 0 \<le> a" 

190 
by simp 

191 
then have "0 \<le> a" 

192 
by (blast intro: order_trans inf_sup_ord) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

193 
} 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

194 
note p = this 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

195 
assume hyp:"sup a (a) = 0" 
56228  196 
then have hyp2:"sup (a) ((a)) = 0" 
197 
by (simp add: sup_commute) 

198 
from p[OF hyp] p[OF hyp2] show "a = 0" 

199 
by simp 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

200 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

201 

56228  202 
lemma inf_0_imp_0: "inf a ( a) = 0 \<Longrightarrow> a = 0" 
53240  203 
apply (simp add: inf_eq_neg_sup) 
204 
apply (simp add: sup_commute) 

205 
apply (erule sup_0_imp_0) 

206 
done 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

207 

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

208 
lemma inf_0_eq_0 [simp, no_atp]: "inf a ( a) = 0 \<longleftrightarrow> a = 0" 
53240  209 
apply rule 
210 
apply (erule inf_0_imp_0) 

211 
apply simp 

212 
done 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

213 

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

214 
lemma sup_0_eq_0 [simp, no_atp]: "sup a ( a) = 0 \<longleftrightarrow> a = 0" 
53240  215 
apply rule 
216 
apply (erule sup_0_imp_0) 

217 
apply simp 

218 
done 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

219 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

220 
lemma zero_le_double_add_iff_zero_le_single_add [simp]: 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

221 
"0 \<le> a + a \<longleftrightarrow> 0 \<le> a" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

222 
proof 
56228  223 
assume "0 \<le> a + a" 
224 
then have a: "inf (a + a) 0 = 0" 

225 
by (simp add: inf_commute inf_absorb1) 

226 
have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a" (is "?l=_") 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

227 
by (simp add: add_sup_inf_distribs inf_aci) 
56228  228 
then have "?l = 0 + inf a 0" 
229 
by (simp add: a, simp add: inf_commute) 

230 
then have "inf a 0 = 0" 

231 
by (simp only: add_right_cancel) 

232 
then show "0 \<le> a" 

233 
unfolding le_iff_inf by (simp add: inf_commute) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

234 
next 
56228  235 
assume a: "0 \<le> a" 
236 
show "0 \<le> a + a" 

237 
by (simp add: add_mono[OF a a, simplified]) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

238 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

239 

53240  240 
lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

241 
proof 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

242 
assume assm: "a + a = 0" 
56228  243 
then have "a + a +  a =  a" 
244 
by simp 

245 
then have "a + (a +  a) =  a" 

246 
by (simp only: add_assoc) 

247 
then have a: " a = a" 

248 
by simp 

53240  249 
show "a = 0" 
250 
apply (rule antisym) 

251 
apply (unfold neg_le_iff_le [symmetric, of a]) 

252 
unfolding a 

253 
apply simp 

254 
unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a] 

255 
unfolding assm 

256 
unfolding le_less 

257 
apply simp_all 

258 
done 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

259 
next 
53240  260 
assume "a = 0" 
56228  261 
then show "a + a = 0" 
262 
by simp 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

263 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

264 

53240  265 
lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

266 
proof (cases "a = 0") 
53240  267 
case True 
268 
then show ?thesis by auto 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

269 
next 
53240  270 
case False 
271 
then show ?thesis 

272 
unfolding less_le 

273 
apply simp 

274 
apply rule 

275 
apply clarify 

276 
apply rule 

277 
apply assumption 

278 
apply (rule notI) 

279 
unfolding double_zero [symmetric, of a] 

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

280 
apply blast 
53240  281 
done 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

282 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

283 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

284 
lemma double_add_le_zero_iff_single_add_le_zero [simp]: 
53240  285 
"a + a \<le> 0 \<longleftrightarrow> a \<le> 0" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

286 
proof  
56228  287 
have "a + a \<le> 0 \<longleftrightarrow> 0 \<le>  (a + a)" 
288 
by (subst le_minus_iff, simp) 

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

289 
moreover have "\<dots> \<longleftrightarrow> a \<le> 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

290 
by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp 
56228  291 
ultimately show ?thesis 
292 
by blast 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

293 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

294 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

295 
lemma double_add_less_zero_iff_single_less_zero [simp]: 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

296 
"a + a < 0 \<longleftrightarrow> a < 0" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

297 
proof  
56228  298 
have "a + a < 0 \<longleftrightarrow> 0 <  (a + a)" 
299 
by (subst less_minus_iff) simp 

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

300 
moreover have "\<dots> \<longleftrightarrow> a < 0" 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

301 
by (simp only: minus_add_distrib zero_less_double_add_iff_zero_less_single_add) simp 
56228  302 
ultimately show ?thesis 
303 
by blast 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

304 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

305 

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

306 
declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] diff_inf_eq_sup [simp] diff_sup_eq_inf [simp] 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

307 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

308 
lemma le_minus_self_iff: "a \<le>  a \<longleftrightarrow> a \<le> 0" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

309 
proof  
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

310 
from add_le_cancel_left [of "uminus a" "plus a a" zero] 
56228  311 
have "a \<le>  a \<longleftrightarrow> a + a \<le> 0" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

312 
by (simp add: add_assoc[symmetric]) 
56228  313 
then show ?thesis 
314 
by simp 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

315 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

316 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

317 
lemma minus_le_self_iff: " a \<le> a \<longleftrightarrow> 0 \<le> a" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

318 
proof  
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

319 
from add_le_cancel_left [of "uminus a" zero "plus a a"] 
56228  320 
have " a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

321 
by (simp add: add_assoc[symmetric]) 
56228  322 
then show ?thesis 
323 
by simp 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

324 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

325 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

326 
lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0" 
53240  327 
unfolding le_iff_inf by (simp add: nprt_def inf_commute) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

328 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

329 
lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0" 
53240  330 
unfolding le_iff_sup by (simp add: pprt_def sup_commute) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

331 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

332 
lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a" 
53240  333 
unfolding le_iff_sup by (simp add: pprt_def sup_commute) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

334 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

335 
lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a" 
53240  336 
unfolding le_iff_inf by (simp add: nprt_def inf_commute) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

337 

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

338 
lemma pprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b" 
53240  339 
unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a]) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

340 

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

341 
lemma nprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b" 
53240  342 
unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a]) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

343 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

344 
end 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

345 

56228  346 
lemmas add_sup_inf_distribs = 
347 
add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

348 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

349 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

350 
class lattice_ab_group_add_abs = lattice_ab_group_add + abs + 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

351 
assumes abs_lattice: "\<bar>a\<bar> = sup a ( a)" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

352 
begin 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

353 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

354 
lemma abs_prts: "\<bar>a\<bar> = pprt a  nprt a" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

355 
proof  
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

356 
have "0 \<le> \<bar>a\<bar>" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

357 
proof  
56228  358 
have a: "a \<le> \<bar>a\<bar>" and b: " a \<le> \<bar>a\<bar>" 
359 
by (auto simp add: abs_lattice) 

360 
show ?thesis 

361 
by (rule add_mono [OF a b, simplified]) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

362 
qed 
56228  363 
then have "0 \<le> sup a ( a)" 
364 
unfolding abs_lattice . 

365 
then have "sup (sup a ( a)) 0 = sup a ( a)" 

366 
by (rule sup_absorb1) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

367 
then show ?thesis 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

368 
by (simp add: add_sup_inf_distribs ac_simps pprt_def nprt_def abs_lattice) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

369 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

370 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

371 
subclass ordered_ab_group_add_abs 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

372 
proof 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

373 
have abs_ge_zero [simp]: "\<And>a. 0 \<le> \<bar>a\<bar>" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

374 
proof  
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

375 
fix a b 
53240  376 
have a: "a \<le> \<bar>a\<bar>" and b: " a \<le> \<bar>a\<bar>" 
377 
by (auto simp add: abs_lattice) 

378 
show "0 \<le> \<bar>a\<bar>" 

379 
by (rule add_mono [OF a b, simplified]) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

380 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

381 
have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow>  a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

382 
by (simp add: abs_lattice le_supI) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

383 
fix a b 
56228  384 
show "0 \<le> \<bar>a\<bar>" 
385 
by simp 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

386 
show "a \<le> \<bar>a\<bar>" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

387 
by (auto simp add: abs_lattice) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

388 
show "\<bar>a\<bar> = \<bar>a\<bar>" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

389 
by (simp add: abs_lattice sup_commute) 
53240  390 
{ 
391 
assume "a \<le> b" 

392 
then show " a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" 

393 
by (rule abs_leI) 

394 
} 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

395 
show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

396 
proof  
56228  397 
have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup ( a  b) (sup ( a + b) (a + ( b))))" 
398 
(is "_=sup ?m ?n") 

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

399 
by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps) 
56228  400 
have a: "a + b \<le> sup ?m ?n" 
401 
by simp 

402 
have b: " a  b \<le> ?n" 

403 
by simp 

404 
have c: "?n \<le> sup ?m ?n" 

405 
by simp 

406 
from b c have d: " a  b \<le> sup ?m ?n" 

407 
by (rule order_trans) 

408 
have e: " a  b =  (a + b)" 

409 
by simp 

410 
from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n" 

53240  411 
apply  
412 
apply (drule abs_leI) 

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

413 
apply (simp_all only: algebra_simps ac_simps minus_add) 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

414 
apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff) 
53240  415 
done 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

416 
with g[symmetric] show ?thesis by simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

417 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

418 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

419 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

420 
end 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

421 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

422 
lemma sup_eq_if: 
56228  423 
fixes a :: "'a::{lattice_ab_group_add, linorder}" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

424 
shows "sup a ( a) = (if a < 0 then  a else a)" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

425 
proof  
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

426 
note add_le_cancel_right [of a a " a", symmetric, simplified] 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

427 
moreover note add_le_cancel_right [of "a" a a, symmetric, simplified] 
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54230
diff
changeset

428 
then show ?thesis by (auto simp: sup_max max.absorb1 max.absorb2) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

429 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

430 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

431 
lemma abs_if_lattice: 
56228  432 
fixes a :: "'a::{lattice_ab_group_add_abs, linorder}" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

433 
shows "\<bar>a\<bar> = (if a < 0 then  a else a)" 
53240  434 
by auto 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

435 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

436 
lemma estimate_by_abs: 
56228  437 
fixes a b c :: "'a::lattice_ab_group_add_abs" 
438 
shows "a + b \<le> c \<Longrightarrow> a \<le> c + \<bar>b\<bar>" 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

439 
proof  
56228  440 
assume "a + b \<le> c" 
441 
then have "a \<le> c + ( b)" 

442 
by (simp add: algebra_simps) 

443 
have " b \<le> \<bar>b\<bar>" 

444 
by (rule abs_ge_minus_self) 

445 
then have "c + ( b) \<le> c + \<bar>b\<bar>" 

446 
by (rule add_left_mono) 

447 
with `a \<le> c + ( b)` show ?thesis 

448 
by (rule order_trans) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

449 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

450 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

451 
class lattice_ring = ordered_ring + lattice_ab_group_add_abs 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

452 
begin 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

453 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

454 
subclass semilattice_inf_ab_group_add .. 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

455 
subclass semilattice_sup_ab_group_add .. 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

456 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

457 
end 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

458 

56228  459 
lemma abs_le_mult: 
460 
fixes a b :: "'a::lattice_ring" 

461 
shows "\<bar>a * b\<bar> \<le> \<bar>a\<bar> * \<bar>b\<bar>" 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

462 
proof  
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

463 
let ?x = "pprt a * pprt b  pprt a * nprt b  nprt a * pprt b + nprt a * nprt b" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

464 
let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" 
56228  465 
have a: "\<bar>a\<bar> * \<bar>b\<bar> = ?x" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

466 
by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

467 
{ 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

468 
fix u v :: 'a 
56228  469 
have bh: "u = a \<Longrightarrow> v = b \<Longrightarrow> 
53240  470 
u * v = pprt a * pprt b + pprt a * nprt b + 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

471 
nprt a * pprt b + nprt a * nprt b" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

472 
apply (subst prts[of u], subst prts[of v]) 
53240  473 
apply (simp add: algebra_simps) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

474 
done 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

475 
} 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

476 
note b = this[OF refl[of a] refl[of b]] 
56228  477 
have xy: " ?x \<le> ?y" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

478 
apply simp 
56228  479 
apply (metis (full_types) add_increasing add_uminus_conv_diff 
480 
lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg 

481 
mult_nonpos_nonpos nprt_le_zero zero_le_pprt) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

482 
done 
56228  483 
have yx: "?y \<le> ?x" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

484 
apply simp 
56228  485 
apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff 
486 
lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos 

487 
mult_nonpos_nonneg nprt_le_zero zero_le_pprt) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

488 
done 
56228  489 
have i1: "a * b \<le> \<bar>a\<bar> * \<bar>b\<bar>" 
490 
by (simp only: a b yx) 

491 
have i2: " (\<bar>a\<bar> * \<bar>b\<bar>) \<le> a * b" 

492 
by (simp only: a b xy) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

493 
show ?thesis 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

494 
apply (rule abs_leI) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

495 
apply (simp add: i1) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

496 
apply (simp add: i2[simplified minus_le_iff]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

497 
done 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

498 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

499 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

500 
instance lattice_ring \<subseteq> ordered_ring_abs 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

501 
proof 
56228  502 
fix a b :: "'a::lattice_ring" 
41528  503 
assume a: "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)" 
56228  504 
show "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

505 
proof  
56228  506 
have s: "(0 \<le> a * b) \<or> (a * b \<le> 0)" 
507 
apply auto 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

508 
apply (rule_tac split_mult_pos_le) 
56228  509 
apply (rule_tac contrapos_np[of "a * b \<le> 0"]) 
510 
apply simp 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

511 
apply (rule_tac split_mult_neg_le) 
56228  512 
using a 
513 
apply blast 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

514 
done 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

515 
have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

516 
by (simp add: prts[symmetric]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

517 
show ?thesis 
56228  518 
proof (cases "0 \<le> a * b") 
519 
case True 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

520 
then show ?thesis 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

521 
apply (simp_all add: mulprts abs_prts) 
56228  522 
using a 
53240  523 
apply (auto simp add: 
524 
algebra_simps 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

525 
iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt] 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

526 
iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id]) 
56228  527 
apply(drule (1) mult_nonneg_nonpos[of a b], simp) 
528 
apply(drule (1) mult_nonneg_nonpos2[of b a], simp) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

529 
done 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

530 
next 
56228  531 
case False 
532 
with s have "a * b \<le> 0" 

533 
by simp 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

534 
then show ?thesis 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

535 
apply (simp_all add: mulprts abs_prts) 
41528  536 
apply (insert a) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

537 
apply (auto simp add: algebra_simps) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

538 
apply(drule (1) mult_nonneg_nonneg[of a b],simp) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

539 
apply(drule (1) mult_nonpos_nonpos[of a b],simp) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

540 
done 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

541 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

542 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

543 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

544 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

545 
lemma mult_le_prts: 
56228  546 
fixes a b :: "'a::lattice_ring" 
547 
assumes "a1 \<le> a" 

548 
and "a \<le> a2" 

549 
and "b1 \<le> b" 

550 
and "b \<le> b2" 

551 
shows "a * b \<le> 

53240  552 
pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1" 
553 
proof  

554 
have "a * b = (pprt a + nprt a) * (pprt b + nprt b)" 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

555 
apply (subst prts[symmetric])+ 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

556 
apply simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

557 
done 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

558 
then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

559 
by (simp add: algebra_simps) 
56228  560 
moreover have "pprt a * pprt b \<le> pprt a2 * pprt b2" 
41528  561 
by (simp_all add: assms mult_mono) 
56228  562 
moreover have "pprt a * nprt b \<le> pprt a1 * nprt b2" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

563 
proof  
56228  564 
have "pprt a * nprt b \<le> pprt a * nprt b2" 
41528  565 
by (simp add: mult_left_mono assms) 
56228  566 
moreover have "pprt a * nprt b2 \<le> pprt a1 * nprt b2" 
41528  567 
by (simp add: mult_right_mono_neg assms) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

568 
ultimately show ?thesis 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

569 
by simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

570 
qed 
56228  571 
moreover have "nprt a * pprt b \<le> nprt a2 * pprt b1" 
53240  572 
proof  
56228  573 
have "nprt a * pprt b \<le> nprt a2 * pprt b" 
41528  574 
by (simp add: mult_right_mono assms) 
56228  575 
moreover have "nprt a2 * pprt b \<le> nprt a2 * pprt b1" 
41528  576 
by (simp add: mult_left_mono_neg assms) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

577 
ultimately show ?thesis 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

578 
by simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

579 
qed 
56228  580 
moreover have "nprt a * nprt b \<le> nprt a1 * nprt b1" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

581 
proof  
56228  582 
have "nprt a * nprt b \<le> nprt a * nprt b1" 
41528  583 
by (simp add: mult_left_mono_neg assms) 
56228  584 
moreover have "nprt a * nprt b1 \<le> nprt a1 * nprt b1" 
41528  585 
by (simp add: mult_right_mono_neg assms) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

586 
ultimately show ?thesis 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

587 
by simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

588 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

589 
ultimately show ?thesis 
53240  590 
apply  
591 
apply (rule add_mono  simp)+ 

592 
done 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

593 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

594 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

595 
lemma mult_ge_prts: 
56228  596 
fixes a b :: "'a::lattice_ring" 
597 
assumes "a1 \<le> a" 

598 
and "a \<le> a2" 

599 
and "b1 \<le> b" 

600 
and "b \<le> b2" 

601 
shows "a * b \<ge> 

53240  602 
nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1" 
603 
proof  

56228  604 
from assms have a1: " a2 \<le> a" 
53240  605 
by auto 
56228  606 
from assms have a2: " a \<le> a1" 
53240  607 
by auto 
56228  608 
from mult_le_prts[of " a2" " a" " a1" "b1" b "b2", 
609 
OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg] 

610 
have le: " (a * b) \<le>  nprt a1 * pprt b2 +  nprt a2 * nprt b2 + 

611 
 pprt a1 * pprt b1 +  pprt a2 * nprt b1" 

53240  612 
by simp 
56228  613 
then have " ( nprt a1 * pprt b2 +  nprt a2 * nprt b2 + 
614 
 pprt a1 * pprt b1 +  pprt a2 * nprt b1) \<le> a * b" 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

615 
by (simp only: minus_le_iff) 
56228  616 
then show ?thesis 
617 
by (simp add: algebra_simps) 

35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

618 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

619 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

620 
instance int :: lattice_ring 
53240  621 
proof 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

622 
fix k :: int 
56228  623 
show "\<bar>k\<bar> = sup k ( k)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

624 
by (auto simp add: sup_int_def) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

625 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

626 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

627 
instance real :: lattice_ring 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

628 
proof 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

629 
fix a :: real 
56228  630 
show "\<bar>a\<bar> = sup a ( a)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

631 
by (auto simp add: sup_real_def) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

632 
qed 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

633 

e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

634 
end 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

635 