author  haftmann 
Fri, 01 Nov 2013 18:51:14 +0100  
changeset 54230  b1d955791529 
parent 53240  07593a0a27f4 
child 54863  82acc20ded73 
permissions  rwrr 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

2 

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

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

4 

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

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

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

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

8 

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

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

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

11 

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

14 
apply (simp_all add: le_infI) 

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

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

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

18 

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

20 
proof  
53240  21 
have "c + inf a b = inf (c+a) (c+b)" 
22 
by (simp add: add_inf_distrib_left) 

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

23 
thus ?thesis by (simp add: add_commute) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

25 

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

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

27 

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

28 
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

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

30 

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

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

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

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

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

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

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

39 

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

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

42 
have "c + sup a b = sup (c+a) (c+b)" by (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

43 
thus ?thesis by (simp add: add_commute) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

45 

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

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

47 

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

48 
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

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

52 
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

53 

53240  54 
lemmas add_sup_inf_distribs = 
55 
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

56 

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

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

58 
proof (rule inf_unique) 
53240  59 
fix a b c :: 'a 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

61 
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

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

63 
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

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 
assume "a \<le> b" "a \<le> c" 
53240  67 
then show "a \<le>  sup (b) (c)" 
68 
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

69 
qed 
53240  70 

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

71 
lemma sup_eq_neg_inf: "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

72 
proof (rule sup_unique) 
53240  73 
fix a b c :: 'a 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

75 
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

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

77 
show "b \<le>  inf (a) (b)" 
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) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

80 
assume "a \<le> c" "b \<le> c" 
53240  81 
then show " inf (a) (b) \<le> c" 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

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

83 

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

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

86 

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

87 
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

88 
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

89 

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

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

92 

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

93 
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

94 
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

95 

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

96 
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

97 
proof  
53240  98 
have "0 =  inf 0 (ab) + inf (ab) 0" 
99 
by (simp add: inf_commute) 

100 
hence "0 = sup 0 (ba) + inf (ab) 0" 

101 
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

102 
hence "0 = (a + sup a b) + (inf a b + (b))" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

103 
by (simp only: add_sup_distrib_left add_inf_distrib_right) simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

104 
then show ?thesis 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

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

106 

53240  107 

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

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

109 

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

112 

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

115 

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

116 
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

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

118 
have "sup ( x) 0 = sup ( x) ( 0)" unfolding minus_zero .. 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

119 
also have "\<dots> =  inf x 0" unfolding neg_inf_eq_sup .. 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

120 
finally have "sup ( x) 0 =  inf x 0" . 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

123 

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

124 
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

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

126 
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

127 
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

128 
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

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

133 

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

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

136 

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

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

139 

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

140 
lemma le_eq_neg: "a \<le>  b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r") 
53240  141 
proof 
142 
assume ?l 

143 
then show ?r 

144 
apply  

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

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

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

147 
done 
53240  148 
next 
149 
assume ?r 

150 
then show ?l 

151 
apply  

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

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

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

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

156 

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

157 
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

158 
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

159 

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

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

162 

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

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

165 

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

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

168 

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

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

171 

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

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

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

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

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

176 
assume hyp: "sup a (a) = 0" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

177 
hence "sup a (a) + a = a" by (simp) 
53240  178 
hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

179 
hence "sup (a+a) 0 <= a" by (simp) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

180 
hence "0 <= a" by (blast intro: order_trans inf_sup_ord) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

183 
assume hyp:"sup a (a) = 0" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

184 
hence hyp2:"sup (a) ((a)) = 0" by (simp add: sup_commute) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

185 
from p[OF hyp] p[OF hyp2] show "a = 0" by simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

187 

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

188 
lemma inf_0_imp_0: "inf a (a) = 0 \<Longrightarrow> a = 0" 
53240  189 
apply (simp add: inf_eq_neg_sup) 
190 
apply (simp add: sup_commute) 

191 
apply (erule sup_0_imp_0) 

192 
done 

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

193 

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

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

197 
apply simp 

198 
done 

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

199 

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

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

203 
apply simp 

204 
done 

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

205 

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

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

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

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

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

210 
hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

211 
have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_") 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

213 
hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

214 
hence "inf a 0 = 0" by (simp only: add_right_cancel) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

215 
then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

217 
assume a: "0 <= a" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

218 
show "0 <= a + a" by (simp add: add_mono[OF a a, simplified]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

220 

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

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

223 
assume assm: "a + a = 0" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

224 
then have "a + a +  a =  a" by simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

225 
then have "a + (a +  a) =  a" by (simp only: add_assoc) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

226 
then have a: " a = a" by simp 
53240  227 
show "a = 0" 
228 
apply (rule antisym) 

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

230 
unfolding a 

231 
apply simp 

232 
unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a] 

233 
unfolding assm 

234 
unfolding le_less 

235 
apply simp_all 

236 
done 

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

237 
next 
53240  238 
assume "a = 0" 
239 
then show "a + a = 0" by simp 

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

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

241 

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

243 
proof (cases "a = 0") 
53240  244 
case True 
245 
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

246 
next 
53240  247 
case False 
248 
then show ?thesis 

249 
unfolding less_le 

250 
apply simp 

251 
apply rule 

252 
apply clarify 

253 
apply rule 

254 
apply assumption 

255 
apply (rule notI) 

256 
unfolding double_zero [symmetric, of a] 

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

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

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

260 

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

261 
lemma double_add_le_zero_iff_single_add_le_zero [simp]: 
53240  262 
"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

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

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

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

266 
by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

269 

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

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

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

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

273 
have "a + a < 0 \<longleftrightarrow> 0 <  (a + a)" by (subst less_minus_iff, simp) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

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

275 
by (simp only: minus_add_distrib zero_less_double_add_iff_zero_less_single_add) simp 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

278 

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

279 
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

280 

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

281 
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

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

283 
from add_le_cancel_left [of "uminus a" "plus a a" zero] 
53240  284 
have "(a <= a) = (a+a <= 0)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

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

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

291 
from add_le_cancel_left [of "uminus a" zero "plus a a"] 
53240  292 
have "(a <= a) = (0 <= a+a)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

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

296 

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

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

299 

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

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

302 

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

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

305 

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

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

308 

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

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

311 

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

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

314 

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

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

316 

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

317 
lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right 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

318 

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

319 

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

320 
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

321 
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

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

323 

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

324 
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

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

326 
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

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

328 
have a: "a \<le> \<bar>a\<bar>" and b: " a \<le> \<bar>a\<bar>" 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

329 
show ?thesis by (rule add_mono [OF a b, simplified]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

331 
then have "0 \<le> sup a ( a)" unfolding abs_lattice . 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

332 
then have "sup (sup a ( a)) 0 = sup a ( a)" by (rule sup_absorb1) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

334 
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

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

336 

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

337 
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

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

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

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

341 
fix a b 
53240  342 
have a: "a \<le> \<bar>a\<bar>" and b: " a \<le> \<bar>a\<bar>" 
343 
by (auto simp add: abs_lattice) 

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

345 
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

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

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

348 
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

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

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

351 
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

352 
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

353 
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

354 
by (simp add: abs_lattice sup_commute) 
53240  355 
{ 
356 
assume "a \<le> b" 

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

358 
by (rule abs_leI) 

359 
} 

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

360 
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

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

362 
have g:"abs a + abs b = sup (a+b) (sup (ab) (sup (a+b) (a + (b))))" (is "_=sup ?m ?n") 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

363 
by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps) 
53240  364 
have a: "a + b <= sup ?m ?n" by simp 
365 
have b: " a  b <= ?n" by simp 

366 
have c: "?n <= sup ?m ?n" by simp 

367 
from b c have d: "ab <= sup ?m ?n" by (rule order_trans) 

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

368 
have e:"ab = (a+b)" by simp 
53240  369 
from a d e have "abs(a+b) <= sup ?m ?n" 
370 
apply  

371 
apply (drule abs_leI) 

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

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

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

375 
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

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

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

378 

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

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

380 

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

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

382 
fixes a :: "'a\<Colon>{lattice_ab_group_add, linorder}" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

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

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

387 
then show ?thesis by (auto simp: sup_max min_max.sup_absorb1 min_max.sup_absorb2) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

389 

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

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

391 
fixes a :: "'a\<Colon>{lattice_ab_group_add_abs, linorder}" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

394 

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

395 
lemma estimate_by_abs: 
53240  396 
"a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

398 
assume "a+b <= c" 
37884
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36976
diff
changeset

399 
then have "a <= c+(b)" by (simp add: algebra_simps) 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36976
diff
changeset

400 
have "(b) <= abs b" by (rule abs_ge_minus_self) 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36976
diff
changeset

401 
then have "c + ( b) \<le> c + \<bar>b\<bar>" by (rule add_left_mono) 
314a88278715
discontinued pretending that abel_cancel is logicindependent; cleaned up junk
haftmann
parents:
36976
diff
changeset

402 
with `a \<le> c + ( b)` show ?thesis 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

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

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

409 
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

410 

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

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

412 

53240  413 
lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lattice_ring))" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

415 
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

416 
let ?y = "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

417 
have a: "(abs a) * (abs b) = ?x" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

420 
fix u v :: 'a 
53240  421 
have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
422 
u * v = pprt a * pprt b + pprt a * nprt b + 

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

423 
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

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

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

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

428 
note b = this[OF refl[of a] refl[of b]] 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

429 
have xy: " ?x <= ?y" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

430 
apply simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

431 
apply (metis (full_types) add_increasing add_uminus_conv_diff lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg 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

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

433 
have yx: "?y <= ?x" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

434 
apply simp 
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

435 
apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos 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 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

437 
have i1: "a*b <= abs a * abs b" by (simp only: a b yx) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

438 
have i2: " (abs a * abs b) <= a*b" by (simp only: a b xy) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

440 
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

441 
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

442 
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

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

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

445 

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

446 
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

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

448 
fix a b :: "'a\<Colon> lattice_ring" 
41528  449 
assume a: "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)" 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

450 
show "abs (a*b) = abs a * abs b" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

452 
have s: "(0 <= a*b)  (a*b <= 0)" 
53240  453 
apply (auto) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

455 
apply (rule_tac contrapos_np[of "a*b <= 0"]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

457 
apply (rule_tac split_mult_neg_le) 
41528  458 
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

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

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

461 
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

462 
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

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

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

465 
assume "0 <= a * b" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

467 
apply (simp_all add: mulprts abs_prts) 
41528  468 
apply (insert a) 
53240  469 
apply (auto simp add: 
470 
algebra_simps 

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

471 
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

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

473 
apply(drule (1) mult_nonneg_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

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

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

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

477 
assume "~(0 <= a*b)" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

478 
with s have "a*b <= 0" by simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

482 
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

483 
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

484 
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

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

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

487 
qed 
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 
lemma mult_le_prts: 
53240  491 
assumes "a1 <= (a::'a::lattice_ring)" 
492 
and "a <= a2" 

493 
and "b1 <= b" 

494 
and "b <= b2" 

495 
shows "a * b <= 

496 
pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1" 

497 
proof  

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

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

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

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

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

502 
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

503 
by (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

504 
moreover have "pprt a * pprt b <= pprt a2 * pprt b2" 
41528  505 
by (simp_all add: assms mult_mono) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

508 
have "pprt a * nprt b <= pprt a * nprt b2" 
41528  509 
by (simp add: mult_left_mono assms) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

510 
moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2" 
41528  511 
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

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

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

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

515 
moreover have "nprt a * pprt b <= nprt a2 * pprt b1" 
53240  516 
proof  
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

517 
have "nprt a * pprt b <= nprt a2 * pprt b" 
41528  518 
by (simp add: mult_right_mono assms) 
35040
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

519 
moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1" 
41528  520 
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

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

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

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

524 
moreover have "nprt a * nprt b <= nprt a1 * nprt b1" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

526 
have "nprt a * nprt b <= nprt a * nprt b1" 
41528  527 
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

528 
moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1" 
41528  529 
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

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

531 
by simp 
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 
ultimately show ?thesis 
53240  534 
apply  
535 
apply (rule add_mono  simp)+ 

536 
done 

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: 
53240  540 
assumes "a1 <= (a::'a::lattice_ring)" 
541 
and "a <= a2" 

542 
and "b1 <= b" 

543 
and "b <= b2" 

544 
shows "a * b >= 

545 
nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1" 

546 
proof  

547 
from assms have a1:" a2 <= a" 

548 
by auto 

549 
from assms have a2: "a <= a1" 

550 
by auto 

551 
from mult_le_prts[of "a2" "a" "a1" "b1" b "b2", OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg] 

552 
have le: " (a * b) <=  nprt a1 * pprt b2 +  nprt a2 * nprt b2 +  pprt a1 * pprt b1 +  pprt a2 * nprt b1" 

553 
by simp 

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

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

555 
by (simp only: minus_le_iff) 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53240
diff
changeset

556 
then show ?thesis 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

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

558 

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

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

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

562 
show "abs k = sup k ( k)" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

563 
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

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

565 

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

566 
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

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

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

569 
show "abs a = sup a ( a)" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

570 
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

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

572 

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

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

574 