author  wenzelm 
Thu, 09 Jul 2015 00:40:57 +0200  
changeset 60698  29e8bdc41f90 
parent 60500  903bb1495239 
child 61546  53bb4172c7f7 
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 

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 
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"]) 

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) 

34 
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

35 
apply (simp only: add.assoc [symmetric], simp) 
54230
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) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56228
diff
changeset

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

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

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 

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

53240  150 
proof 
151 
assume ?l 

152 
then show ?r 

153 
apply  

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

154 
apply (rule add_le_imp_le_right[of _ "uminus b" _]) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
56228
diff
changeset

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

156 
done 
53240  157 
next 
158 
assume ?r 

159 
then show ?l 

160 
apply  

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

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

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

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

165 

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

166 
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

167 
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

168 

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

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

171 

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

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

174 

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

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

177 

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

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

180 

60698  181 
lemma sup_0_imp_0: 
182 
assumes "sup a ( a) = 0" 

183 
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

184 
proof  
60698  185 
have p: "0 \<le> a" if "sup a ( a) = 0" for a :: 'a 
186 
proof  

187 
from that have "sup a ( a) + a = a" 

56228  188 
by simp 
189 
then have "sup (a + a) 0 = a" 

190 
by (simp add: add_sup_distrib_right) 

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

192 
by simp 

60698  193 
then show ?thesis 
56228  194 
by (blast intro: order_trans inf_sup_ord) 
60698  195 
qed 
196 
from assms have **: "sup (a) ((a)) = 0" 

56228  197 
by (simp add: sup_commute) 
60698  198 
from p[OF assms] p[OF **] show "a = 0" 
56228  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 

60698  220 
lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a" 
221 
(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

222 
proof 
60698  223 
show ?rhs if ?lhs 
224 
proof  

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

226 
by (simp add: inf_commute inf_absorb1) 

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

228 
by (simp add: add_sup_inf_distribs inf_aci) 

229 
then have "?l = 0 + inf a 0" 

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

231 
then have "inf a 0 = 0" 

232 
by (simp only: add_right_cancel) 

233 
then show ?thesis 

234 
unfolding le_iff_inf by (simp add: inf_commute) 

235 
qed 

236 
show ?lhs if ?rhs 

237 
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

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" 
60698  241 
(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

242 
proof 
60698  243 
show ?rhs if ?lhs 
244 
proof  

245 
from that have "a + a +  a =  a" 

246 
by simp 

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

248 
by (simp only: add.assoc) 

249 
then have a: " a = a" 

250 
by simp 

251 
show ?thesis 

252 
apply (rule antisym) 

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

254 
unfolding a 

255 
apply simp 

256 
unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a] 

257 
unfolding that 

258 
unfolding le_less 

259 
apply simp_all 

260 
done 

261 
qed 

262 
show ?lhs if ?rhs 

263 
using that by simp 

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

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

265 

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

267 
proof (cases "a = 0") 
53240  268 
case True 
269 
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

270 
next 
53240  271 
case False 
272 
then show ?thesis 

273 
unfolding less_le 

274 
apply simp 

275 
apply rule 

276 
apply clarify 

277 
apply rule 

278 
apply assumption 

279 
apply (rule notI) 

280 
unfolding double_zero [symmetric, of a] 

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

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

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

284 

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

286 
proof  
56228  287 
have "a + a \<le> 0 \<longleftrightarrow> 0 \<le>  (a + a)" 
60698  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 

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

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

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

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

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

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

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

304 

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

305 
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

306 

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

307 
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

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

309 
from add_le_cancel_left [of "uminus a" "plus a a" zero] 
56228  310 
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

311 
by (simp add: add.assoc[symmetric]) 
56228  312 
then show ?thesis 
313 
by simp 

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

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

315 

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

316 
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

317 
proof  
56228  318 
have " a \<le> a \<longleftrightarrow> 0 \<le> a + a" 
60698  319 
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

320 
by (simp add: add.assoc[symmetric]) 
56228  321 
then show ?thesis 
322 
by simp 

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

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

324 

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

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

327 

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

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

330 

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

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

333 

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

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

336 

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

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

339 

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

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

342 

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

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

344 

56228  345 
lemmas add_sup_inf_distribs = 
346 
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

347 

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

350 
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

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

352 

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

353 
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

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

355 
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

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

359 
show ?thesis 

360 
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

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

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

365 
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

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

367 
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

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

369 

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

370 
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

371 
proof 
60698  372 
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

373 
proof  
53240  374 
have a: "a \<le> \<bar>a\<bar>" and b: " a \<le> \<bar>a\<bar>" 
375 
by (auto simp add: abs_lattice) 

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

377 
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

378 
qed 
60698  379 
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

380 
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

381 
fix a b 
56228  382 
show "0 \<le> \<bar>a\<bar>" 
383 
by simp 

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

384 
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

385 
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

386 
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

387 
by (simp add: abs_lattice sup_commute) 
60698  388 
show " a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b" if "a \<le> b" 
389 
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

390 
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

391 
proof  
56228  392 
have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup ( a  b) (sup ( a + b) (a + ( b))))" 
60698  393 
(is "_ = sup ?m ?n") 
57862  394 
by (simp add: abs_lattice add_sup_inf_distribs ac_simps) 
56228  395 
have a: "a + b \<le> sup ?m ?n" 
396 
by simp 

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

398 
by simp 

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

400 
by simp 

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

402 
by (rule order_trans) 

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

404 
by simp 

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

53240  406 
apply  
407 
apply (drule abs_leI) 

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

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

411 
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

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

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

414 

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

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

416 

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

417 
lemma sup_eq_if: 
60698  418 
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

419 
shows "sup a ( a) = (if a < 0 then  a else a)" 
60698  420 
using add_le_cancel_right [of a a " a", symmetric, simplified] 
421 
and add_le_cancel_right [of "a" a a, symmetric, simplified] 

422 
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

423 

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

424 
lemma abs_if_lattice: 
60698  425 
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

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

428 

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

429 
lemma estimate_by_abs: 
56228  430 
fixes a b c :: "'a::lattice_ab_group_add_abs" 
60698  431 
assumes "a + b \<le> c" 
432 
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

433 
proof  
60698  434 
from assms have "a \<le> c + ( b)" 
56228  435 
by (simp add: algebra_simps) 
436 
have " b \<le> \<bar>b\<bar>" 

437 
by (rule abs_ge_minus_self) 

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

439 
by (rule add_left_mono) 

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

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

443 

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

444 
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

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

446 

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

447 
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

448 
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

449 

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

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

451 

56228  452 
lemma abs_le_mult: 
453 
fixes a b :: "'a::lattice_ring" 

454 
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

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

456 
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

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

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

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

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

464 
apply (simp add: algebra_simps) 

465 
done 

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

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

468 
apply simp 
56228  469 
apply (metis (full_types) add_increasing add_uminus_conv_diff 
470 
lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg 

471 
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

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

474 
apply simp 
56228  475 
apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff 
476 
lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos 

477 
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

478 
done 
56228  479 
have i1: "a * b \<le> \<bar>a\<bar> * \<bar>b\<bar>" 
480 
by (simp only: a b yx) 

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

482 
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

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

484 
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

485 
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

486 
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

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

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

489 

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

490 
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

491 
proof 
56228  492 
fix a b :: "'a::lattice_ring" 
41528  493 
assume a: "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)" 
56228  494 
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

495 
proof  
56228  496 
have s: "(0 \<le> a * b) \<or> (a * b \<le> 0)" 
497 
apply auto 

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

498 
apply (rule_tac split_mult_pos_le) 
56228  499 
apply (rule_tac contrapos_np[of "a * b \<le> 0"]) 
500 
apply simp 

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

501 
apply (rule_tac split_mult_neg_le) 
56228  502 
using a 
503 
apply blast 

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

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

505 
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

506 
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

507 
show ?thesis 
56228  508 
proof (cases "0 \<le> a * b") 
509 
case True 

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

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

511 
apply (simp_all add: mulprts abs_prts) 
56228  512 
using a 
53240  513 
apply (auto simp add: 
514 
algebra_simps 

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

515 
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

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

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

520 
next 
56228  521 
case False 
522 
with s have "a * b \<le> 0" 

523 
by simp 

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

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

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

527 
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

528 
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

529 
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

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

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

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

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

534 

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

535 
lemma mult_le_prts: 
56228  536 
fixes a b :: "'a::lattice_ring" 
537 
assumes "a1 \<le> a" 

538 
and "a \<le> a2" 

539 
and "b1 \<le> b" 

540 
and "b \<le> b2" 

541 
shows "a * b \<le> 

53240  542 
pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1" 
543 
proof  

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

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

546 
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

547 
by (simp add: algebra_simps) 
56228  548 
moreover have "pprt a * pprt b \<le> pprt a2 * pprt b2" 
41528  549 
by (simp_all add: assms mult_mono) 
56228  550 
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

551 
proof  
56228  552 
have "pprt a * nprt b \<le> pprt a * nprt b2" 
41528  553 
by (simp add: mult_left_mono assms) 
56228  554 
moreover have "pprt a * nprt b2 \<le> pprt a1 * nprt b2" 
41528  555 
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

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

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

558 
qed 
56228  559 
moreover have "nprt a * pprt b \<le> nprt a2 * pprt b1" 
53240  560 
proof  
56228  561 
have "nprt a * pprt b \<le> nprt a2 * pprt b" 
41528  562 
by (simp add: mult_right_mono assms) 
56228  563 
moreover have "nprt a2 * pprt b \<le> nprt a2 * pprt b1" 
41528  564 
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

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

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

567 
qed 
56228  568 
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

569 
proof  
56228  570 
have "nprt a * nprt b \<le> nprt a * nprt b1" 
41528  571 
by (simp add: mult_left_mono_neg assms) 
56228  572 
moreover have "nprt a * nprt b1 \<le> nprt a1 * nprt b1" 
41528  573 
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

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

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

576 
qed 
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 
60698  578 
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

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

580 

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

581 
lemma mult_ge_prts: 
56228  582 
fixes a b :: "'a::lattice_ring" 
583 
assumes "a1 \<le> a" 

584 
and "a \<le> a2" 

585 
and "b1 \<le> b" 

586 
and "b \<le> b2" 

587 
shows "a * b \<ge> 

53240  588 
nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1" 
589 
proof  

56228  590 
from assms have a1: " a2 \<le> a" 
53240  591 
by auto 
56228  592 
from assms have a2: " a \<le> a1" 
53240  593 
by auto 
56228  594 
from mult_le_prts[of " a2" " a" " a1" "b1" b "b2", 
595 
OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg] 

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

56228  598 
 pprt a1 * pprt b1 +  pprt a2 * nprt b1" 
53240  599 
by simp 
56228  600 
then have " ( nprt a1 * pprt b2 +  nprt a2 * nprt b2 + 
601 
 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

602 
by (simp only: minus_le_iff) 
56228  603 
then show ?thesis 
604 
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

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

606 

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

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

609 
fix k :: int 
56228  610 
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

611 
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

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

613 

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

614 
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

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

616 
fix a :: real 
56228  617 
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

618 
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

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

620 

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

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

622 