author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 61546  53bb4172c7f7 
child 68406  6beb45f6cf67 
permissions  rwrr 
61546  1 
(* Author: Steven Obua, TU Muenchen *) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

2 

60500  3 
section \<open>Various algebraic structures combined with a lattice\<close> 
35040
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 
65151  6 
imports Complex_Main 
35040
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) 

65151  14 
apply (simp_all add: le_infI) 
53240  15 
apply (rule add_le_imp_le_left [of "uminus a"]) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56228
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 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56228
diff
changeset

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) 

65151  34 
apply (rule add_le_imp_le_left [of "uminus a"]) 
35 
apply (simp only: add.assoc [symmetric], simp) 

36 
apply (simp add: le_diff_eq add.commute) 

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

37 
apply (rule le_supI) 
65151  38 
apply (rule add_le_imp_le_left [of "a"], simp only: add.assoc[symmetric], simp)+ 
53240  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 

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

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) 
65151  83 
show " inf ( a) ( b) \<le> c" if "a \<le> c" "b \<le> c" 
84 
using that 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

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

86 

56228  87 
lemma neg_inf_eq_sup: " inf a b = sup ( a) ( b)" 
53240  88 
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

89 

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

90 
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

91 
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

92 

56228  93 
lemma neg_sup_eq_inf: " sup a b = inf ( a) ( b)" 
53240  94 
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

95 

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

96 
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

97 
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

98 

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

99 
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

100 
proof  
56228  101 
have "0 =  inf 0 (a  b) + inf (a  b) 0" 
53240  102 
by (simp add: inf_commute) 
56228  103 
then have "0 = sup 0 (b  a) + inf (a  b) 0" 
53240  104 
by (simp add: inf_eq_neg_sup) 
56228  105 
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

106 
by (simp only: add_sup_distrib_left add_inf_distrib_right) simp 
56228  107 
then show ?thesis 
108 
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

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

110 

53240  111 

60500  112 
subsection \<open>Positive Part, Negative Part, Absolute Value\<close> 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

113 

53240  114 
definition nprt :: "'a \<Rightarrow> 'a" 
115 
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

116 

53240  117 
definition pprt :: "'a \<Rightarrow> 'a" 
118 
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

119 

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

120 
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

121 
proof  
56228  122 
have "sup ( x) 0 = sup ( x) ( 0)" 
65151  123 
by (simp only: minus_zero) 
56228  124 
also have "\<dots> =  inf x 0" 
65151  125 
by (simp only: 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

126 
finally have "sup ( x) 0 =  inf x 0" . 
56228  127 
then show ?thesis 
65151  128 
by (simp only: 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

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

130 

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

131 
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

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

133 
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

134 
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

135 
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

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

137 

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

138 
lemma prts: "a = pprt a + nprt a" 
53240  139 
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

140 

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

141 
lemma zero_le_pprt[simp]: "0 \<le> pprt a" 
53240  142 
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

143 

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

144 
lemma nprt_le_zero[simp]: "nprt a \<le> 0" 
53240  145 
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

146 

60698  147 
lemma le_eq_neg: "a \<le>  b \<longleftrightarrow> a + b \<le> 0" 
65151  148 
(is "?lhs = ?rhs") 
53240  149 
proof 
65151  150 
assume ?lhs 
151 
show ?rhs 

152 
by (rule add_le_imp_le_right[of _ "uminus b" _]) (simp add: add.assoc \<open>?lhs\<close>) 

53240  153 
next 
65151  154 
assume ?rhs 
155 
show ?lhs 

156 
by (rule add_le_imp_le_right[of _ "b" _]) (simp add: \<open>?rhs\<close>) 

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

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

158 

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

159 
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

160 
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

161 

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

162 
lemma pprt_eq_id [simp, no_atp]: "0 \<le> x \<Longrightarrow> pprt x = x" 
46986  163 
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

164 

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

165 
lemma nprt_eq_id [simp, no_atp]: "x \<le> 0 \<Longrightarrow> nprt x = x" 
46986  166 
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

167 

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

168 
lemma pprt_eq_0 [simp, no_atp]: "x \<le> 0 \<Longrightarrow> pprt x = 0" 
46986  169 
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

170 

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

171 
lemma nprt_eq_0 [simp, no_atp]: "0 \<le> x \<Longrightarrow> nprt x = 0" 
46986  172 
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

173 

60698  174 
lemma sup_0_imp_0: 
175 
assumes "sup a ( a) = 0" 

176 
shows "a = 0" 

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

177 
proof  
65151  178 
have pos: "0 \<le> a" if "sup a ( a) = 0" for a :: 'a 
60698  179 
proof  
180 
from that have "sup a ( a) + a = a" 

56228  181 
by simp 
182 
then have "sup (a + a) 0 = a" 

183 
by (simp add: add_sup_distrib_right) 

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

185 
by simp 

60698  186 
then show ?thesis 
56228  187 
by (blast intro: order_trans inf_sup_ord) 
60698  188 
qed 
189 
from assms have **: "sup (a) ((a)) = 0" 

56228  190 
by (simp add: sup_commute) 
65151  191 
from pos[OF assms] pos[OF **] show "a = 0" 
56228  192 
by simp 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

194 

56228  195 
lemma inf_0_imp_0: "inf a ( a) = 0 \<Longrightarrow> a = 0" 
53240  196 
apply (simp add: inf_eq_neg_sup) 
197 
apply (simp add: sup_commute) 

198 
apply (erule sup_0_imp_0) 

199 
done 

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

200 

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

201 
lemma inf_0_eq_0 [simp, no_atp]: "inf a ( a) = 0 \<longleftrightarrow> a = 0" 
65151  202 
apply (rule iffI) 
203 
apply (erule inf_0_imp_0) 

53240  204 
apply simp 
205 
done 

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

206 

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

207 
lemma sup_0_eq_0 [simp, no_atp]: "sup a ( a) = 0 \<longleftrightarrow> a = 0" 
65151  208 
apply (rule iffI) 
209 
apply (erule sup_0_imp_0) 

53240  210 
apply simp 
211 
done 

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

212 

60698  213 
lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a" 
214 
(is "?lhs \<longleftrightarrow> ?rhs") 

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

215 
proof 
60698  216 
show ?rhs if ?lhs 
217 
proof  

218 
from that have a: "inf (a + a) 0 = 0" 

219 
by (simp add: inf_commute inf_absorb1) 

61546  220 
have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a" (is "?l = _") 
60698  221 
by (simp add: add_sup_inf_distribs inf_aci) 
222 
then have "?l = 0 + inf a 0" 

223 
by (simp add: a, simp add: inf_commute) 

224 
then have "inf a 0 = 0" 

225 
by (simp only: add_right_cancel) 

226 
then show ?thesis 

227 
unfolding le_iff_inf by (simp add: inf_commute) 

228 
qed 

229 
show ?lhs if ?rhs 

230 
by (simp add: add_mono[OF that that, simplified]) 

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

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

232 

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

235 

53240  236 
lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a" 
65151  237 
by (meson le_less_trans less_add_same_cancel2 less_le_not_le 
238 
zero_le_double_add_iff_zero_le_single_add) 

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

239 

60698  240 
lemma double_add_le_zero_iff_single_add_le_zero [simp]: "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

241 
proof  
56228  242 
have "a + a \<le> 0 \<longleftrightarrow> 0 \<le>  (a + a)" 
60698  243 
by (subst le_minus_iff) simp 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

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

245 
by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp 
56228  246 
ultimately show ?thesis 
247 
by blast 

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

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

249 

60698  250 
lemma double_add_less_zero_iff_single_less_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

251 
proof  
56228  252 
have "a + a < 0 \<longleftrightarrow> 0 <  (a + a)" 
253 
by (subst less_minus_iff) simp 

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

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

255 
by (simp only: minus_add_distrib zero_less_double_add_iff_zero_less_single_add) simp 
56228  256 
ultimately show ?thesis 
257 
by blast 

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

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

259 

65151  260 
declare neg_inf_eq_sup [simp] 
261 
and neg_sup_eq_inf [simp] 

262 
and diff_inf_eq_sup [simp] 

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

264 

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

265 
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

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

267 
from add_le_cancel_left [of "uminus a" "plus a a" zero] 
56228  268 
have "a \<le>  a \<longleftrightarrow> a + a \<le> 0" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56228
diff
changeset

269 
by (simp add: add.assoc[symmetric]) 
56228  270 
then show ?thesis 
271 
by simp 

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

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

273 

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

274 
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

275 
proof  
56228  276 
have " a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
60698  277 
using add_le_cancel_left [of "uminus a" zero "plus a a"] 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56228
diff
changeset

278 
by (simp add: add.assoc[symmetric]) 
56228  279 
then show ?thesis 
280 
by simp 

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

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

282 

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

283 
lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0" 
53240  284 
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

285 

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

286 
lemma le_zero_iff_zero_pprt: "a \<le> 0 \<longleftrightarrow> pprt a = 0" 
53240  287 
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

288 

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

289 
lemma le_zero_iff_pprt_id: "0 \<le> a \<longleftrightarrow> pprt a = a" 
53240  290 
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

291 

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

292 
lemma zero_le_iff_nprt_id: "a \<le> 0 \<longleftrightarrow> nprt a = a" 
53240  293 
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

294 

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

295 
lemma pprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b" 
53240  296 
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

297 

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

298 
lemma nprt_mono [simp, no_atp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b" 
53240  299 
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

300 

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

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

302 

56228  303 
lemmas add_sup_inf_distribs = 
304 
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

305 

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

306 

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

307 
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

308 
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

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

310 

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

311 
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

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

313 
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

314 
proof  
56228  315 
have a: "a \<le> \<bar>a\<bar>" and b: " a \<le> \<bar>a\<bar>" 
316 
by (auto simp add: abs_lattice) 

317 
show ?thesis 

318 
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

319 
qed 
56228  320 
then have "0 \<le> sup a ( a)" 
321 
unfolding abs_lattice . 

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

323 
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

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

325 
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

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

327 

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

328 
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

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

331 
proof  
53240  332 
have a: "a \<le> \<bar>a\<bar>" and b: " a \<le> \<bar>a\<bar>" 
333 
by (auto simp add: abs_lattice) 

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

335 
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

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

338 
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

339 
fix a b 
56228  340 
show "0 \<le> \<bar>a\<bar>" 
341 
by simp 

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

342 
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

343 
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

344 
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

345 
by (simp add: abs_lattice sup_commute) 
60698  346 
show " a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" if "a \<le> b" 
347 
using that by (rule abs_leI) 

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

348 
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

349 
proof  
56228  350 
have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup ( a  b) (sup ( a + b) (a + ( b))))" 
60698  351 
(is "_ = sup ?m ?n") 
57862  352 
by (simp add: abs_lattice add_sup_inf_distribs ac_simps) 
56228  353 
have a: "a + b \<le> sup ?m ?n" 
354 
by simp 

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

356 
by simp 

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

358 
by simp 

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

360 
by (rule order_trans) 

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

362 
by simp 

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

53240  364 
apply  
365 
apply (drule abs_leI) 

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

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

369 
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

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

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

372 

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

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

374 

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

375 
lemma sup_eq_if: 
60698  376 
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

377 
shows "sup a ( a) = (if a < 0 then  a else a)" 
60698  378 
using add_le_cancel_right [of a a " a", symmetric, simplified] 
379 
and add_le_cancel_right [of "a" a a, symmetric, simplified] 

380 
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

381 

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

382 
lemma abs_if_lattice: 
60698  383 
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

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

386 

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

387 
lemma estimate_by_abs: 
56228  388 
fixes a b c :: "'a::lattice_ab_group_add_abs" 
60698  389 
assumes "a + b \<le> c" 
390 
shows "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

391 
proof  
60698  392 
from assms have "a \<le> c + ( b)" 
56228  393 
by (simp add: algebra_simps) 
394 
have " b \<le> \<bar>b\<bar>" 

395 
by (rule abs_ge_minus_self) 

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

397 
by (rule add_left_mono) 

60500  398 
with \<open>a \<le> c + ( b)\<close> show ?thesis 
56228  399 
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

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

401 

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

402 
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

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

404 

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

405 
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

406 
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

407 

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

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

409 

56228  410 
lemma abs_le_mult: 
411 
fixes a b :: "'a::lattice_ring" 

412 
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

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

414 
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

415 
let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b" 
56228  416 
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

417 
by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps) 
60698  418 
have bh: "u = a \<Longrightarrow> v = b \<Longrightarrow> 
419 
u * v = pprt a * pprt b + pprt a * nprt b + 

420 
nprt a * pprt b + nprt a * nprt b" for u v :: 'a 

421 
apply (subst prts[of u], subst prts[of v]) 

422 
apply (simp add: algebra_simps) 

423 
done 

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

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

426 
apply simp 
56228  427 
apply (metis (full_types) add_increasing add_uminus_conv_diff 
428 
lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg 

429 
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

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

432 
apply simp 
56228  433 
apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff 
434 
lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos 

435 
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

436 
done 
56228  437 
have i1: "a * b \<le> \<bar>a\<bar> * \<bar>b\<bar>" 
438 
by (simp only: a b yx) 

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

440 
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

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

442 
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

443 
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

444 
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

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

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

447 

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

448 
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

449 
proof 
56228  450 
fix a b :: "'a::lattice_ring" 
41528  451 
assume a: "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)" 
56228  452 
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

453 
proof  
56228  454 
have s: "(0 \<le> a * b) \<or> (a * b \<le> 0)" 
455 
apply auto 

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

456 
apply (rule_tac split_mult_pos_le) 
56228  457 
apply (rule_tac contrapos_np[of "a * b \<le> 0"]) 
458 
apply simp 

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

459 
apply (rule_tac split_mult_neg_le) 
56228  460 
using a 
461 
apply blast 

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

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

463 
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

464 
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

465 
show ?thesis 
56228  466 
proof (cases "0 \<le> a * b") 
467 
case True 

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

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

469 
apply (simp_all add: mulprts abs_prts) 
56228  470 
using a 
53240  471 
apply (auto simp add: 
472 
algebra_simps 

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

473 
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

474 
iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id]) 
56228  475 
apply(drule (1) mult_nonneg_nonpos[of a b], simp) 
476 
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

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

478 
next 
56228  479 
case False 
480 
with s have "a * b \<le> 0" 

481 
by simp 

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

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

483 
apply (simp_all add: mulprts abs_prts) 
41528  484 
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

485 
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

486 
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

487 
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

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

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

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

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

492 

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

493 
lemma mult_le_prts: 
56228  494 
fixes a b :: "'a::lattice_ring" 
495 
assumes "a1 \<le> a" 

496 
and "a \<le> a2" 

497 
and "b1 \<le> b" 

498 
and "b \<le> b2" 

499 
shows "a * b \<le> 

53240  500 
pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1" 
501 
proof  

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

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

504 
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

505 
by (simp add: algebra_simps) 
56228  506 
moreover have "pprt a * pprt b \<le> pprt a2 * pprt b2" 
41528  507 
by (simp_all add: assms mult_mono) 
56228  508 
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

509 
proof  
56228  510 
have "pprt a * nprt b \<le> pprt a * nprt b2" 
41528  511 
by (simp add: mult_left_mono assms) 
56228  512 
moreover have "pprt a * nprt b2 \<le> pprt a1 * nprt b2" 
41528  513 
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

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

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

516 
qed 
56228  517 
moreover have "nprt a * pprt b \<le> nprt a2 * pprt b1" 
53240  518 
proof  
56228  519 
have "nprt a * pprt b \<le> nprt a2 * pprt b" 
41528  520 
by (simp add: mult_right_mono assms) 
56228  521 
moreover have "nprt a2 * pprt b \<le> nprt a2 * pprt b1" 
41528  522 
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

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

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

525 
qed 
56228  526 
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

527 
proof  
56228  528 
have "nprt a * nprt b \<le> nprt a * nprt b1" 
41528  529 
by (simp add: mult_left_mono_neg assms) 
56228  530 
moreover have "nprt a * nprt b1 \<le> nprt a1 * nprt b1" 
41528  531 
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

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

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

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

535 
ultimately show ?thesis 
60698  536 
by  (rule add_mono  simp)+ 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

538 

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

539 
lemma mult_ge_prts: 
56228  540 
fixes a b :: "'a::lattice_ring" 
541 
assumes "a1 \<le> a" 

542 
and "a \<le> a2" 

543 
and "b1 \<le> b" 

544 
and "b \<le> b2" 

545 
shows "a * b \<ge> 

53240  546 
nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1" 
547 
proof  

56228  548 
from assms have a1: " a2 \<le> a" 
53240  549 
by auto 
56228  550 
from assms have a2: " a \<le> a1" 
53240  551 
by auto 
56228  552 
from mult_le_prts[of " a2" " a" " a1" "b1" b "b2", 
553 
OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg] 

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

56228  556 
 pprt a1 * pprt b1 +  pprt a2 * nprt b1" 
53240  557 
by simp 
56228  558 
then have " ( nprt a1 * pprt b2 +  nprt a2 * nprt b2 + 
559 
 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

560 
by (simp only: minus_le_iff) 
56228  561 
then show ?thesis 
562 
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

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

564 

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

565 
instance int :: lattice_ring 
53240  566 
proof 
65151  567 
show "\<bar>k\<bar> = sup k ( k)" for k :: int 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

568 
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

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

570 

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

571 
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

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

574 
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

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

576 

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

577 
end 