author  haftmann 
Mon, 08 Feb 2010 15:25:00 +0100  
changeset 35040  e42e7f133d94 
child 35828  46cfc4b8112e 
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 

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

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

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

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

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

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

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

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

19 
apply (rule add_le_imp_le_left[of "a"], simp only: add_assoc[symmetric], simp)+ 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

21 

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

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

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

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

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

26 
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

27 
qed 
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 
end 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

30 

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

31 
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

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

33 

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

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

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

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

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

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

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

40 
apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+ 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

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

44 

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

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

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

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

48 
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

49 
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

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

51 

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

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

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

58 
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

59 

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

60 
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

61 

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

62 
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

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

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

65 
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

66 
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

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

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

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

70 
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

71 
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

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

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

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

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

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

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

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

79 

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

80 
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

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

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

83 
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

84 
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

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

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

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

88 
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

89 
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

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

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

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

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

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

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

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

97 

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

98 
lemma neg_inf_eq_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

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

100 

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

101 
lemma neg_sup_eq_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

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

103 

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

104 
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

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

106 
have "0 =  inf 0 (ab) + inf (ab) 0" 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

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

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

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

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

111 
thus ?thesis 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

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

113 

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

114 
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

115 

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

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

117 
nprt :: "'a \<Rightarrow> 'a" where 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

118 
"nprt x = inf x 0" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

119 

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

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

121 
pprt :: "'a \<Rightarrow> 'a" where 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

122 
"pprt x = sup x 0" 
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 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

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

126 
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

127 
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

128 
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

129 
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

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" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

140 
by (simp add: pprt_def nprt_def add_eq_inf_sup[symmetric]) 
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" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

143 
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

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" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

146 
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

147 

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

148 
lemma le_eq_neg: "a \<le>  b \<longleftrightarrow> a + b \<le> 0" (is "?l = ?r") 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

150 
have a: "?l \<longrightarrow> ?r" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

151 
apply (auto) 
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 _ "uminus b" _]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

153 
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

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

155 
have b: "?r \<longrightarrow> ?l" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

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

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

160 
from a b 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

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

162 

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

163 
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

164 
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

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_eq_id [simp, noatp]: "0 \<le> x \<Longrightarrow> pprt x = x" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

168 

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

169 
lemma nprt_eq_id [simp, noatp]: "x \<le> 0 \<Longrightarrow> nprt x = x" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

170 
by (simp add: nprt_def inf_aci inf_absorb1) 
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 pprt_eq_0 [simp, noatp]: "x \<le> 0 \<Longrightarrow> pprt x = 0" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

173 
by (simp add: pprt_def sup_aci sup_absorb2) 
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 
lemma nprt_eq_0 [simp, noatp]: "0 \<le> x \<Longrightarrow> nprt x = 0" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

177 

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

178 
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

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

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

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

182 
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

183 
hence "sup 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

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

185 
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

186 
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

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

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

189 
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

190 
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

191 
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

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

193 

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

194 
lemma inf_0_imp_0: "inf 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

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

196 
apply (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

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

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

199 

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

200 
lemma inf_0_eq_0 [simp, noatp]: "inf 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

201 
by (rule, erule inf_0_imp_0) simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

202 

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

203 
lemma sup_0_eq_0 [simp, noatp]: "sup 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

204 
by (rule, erule sup_0_imp_0) simp 
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 

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

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

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

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

224 
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

225 
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

226 
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

227 
then have 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

228 
show "a = 0" apply (rule antisym) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

229 
apply (unfold neg_le_iff_le [symmetric, of a]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

231 
unfolding zero_le_double_add_iff_zero_le_single_add [symmetric, of a] 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

232 
unfolding assm unfolding le_less apply simp_all done 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

234 
assume "a = 0" then show "a + 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

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

236 

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

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

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

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

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

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

242 
case False then show ?thesis (*FIXME tune proof*) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

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

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

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

248 
unfolding double_zero [symmetric, of a] apply simp 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

251 

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

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

253 
"a + a \<le> 0 \<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

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

255 
have "a + a \<le> 0 \<longleftrightarrow> 0 \<le>  (a + a)" by (subst le_minus_iff, simp) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

256 
moreover have "\<dots> \<longleftrightarrow> a \<le> 0" by (simp add: zero_le_double_add_iff_zero_le_single_add) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

257 
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

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

259 

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

260 
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

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

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

263 
have "a + a < 0 \<longleftrightarrow> 0 <  (a + a)" by (subst less_minus_iff, simp) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

264 
moreover have "\<dots> \<longleftrightarrow> a < 0" by (simp add: zero_less_double_add_iff_zero_less_single_add) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

265 
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

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

267 

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

268 
declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] 
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 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

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

272 
from add_le_cancel_left [of "uminus a" "plus a a" zero] 
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) = (a+a <= 0)" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

274 
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

275 
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

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

277 

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

278 
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

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

280 
from add_le_cancel_left [of "uminus a" zero "plus a a"] 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

282 
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

283 
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

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

285 

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

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

287 
unfolding le_iff_inf by (simp add: nprt_def inf_commute) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

288 

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

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

290 
unfolding le_iff_sup by (simp add: pprt_def sup_commute) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

291 

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

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

293 
unfolding le_iff_sup by (simp add: pprt_def sup_commute) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

294 

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

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

296 
unfolding le_iff_inf by (simp add: nprt_def inf_commute) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

297 

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

298 
lemma pprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> pprt a \<le> pprt b" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

299 
unfolding le_iff_sup by (simp add: pprt_def sup_aci sup_assoc [symmetric, of a]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

300 

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

301 
lemma nprt_mono [simp, noatp]: "a \<le> b \<Longrightarrow> nprt a \<le> nprt b" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

302 
unfolding le_iff_inf by (simp add: nprt_def inf_aci inf_assoc [symmetric, of a]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

303 

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

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

307 

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

308 

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

309 
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

310 
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

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

312 

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

313 
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

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

315 
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

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

317 
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

318 
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

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

320 
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

321 
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

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

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

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

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

326 

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

327 
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

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

329 
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

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

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

332 
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

333 
show "0 \<le> \<bar>a\<bar>" 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

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

335 
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

336 
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

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

338 
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

339 
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

340 
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

341 
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

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

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

344 
show "\<bar>a + 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

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

346 
have g:"abs a + abs b = sup (a+b) (sup (ab) (sup (a+b) (a + (b))))" (is "_=sup ?m ?n") 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

348 
have a:"a+b <= sup ?m ?n" by (simp) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

349 
have b:"ab <= ?n" by (simp) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

350 
have c:"?n <= sup ?m ?n" by (simp) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

351 
from b c have d: "ab <= sup ?m ?n" by(rule order_trans) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

352 
have e:"ab = (a+b)" by (simp add: diff_minus) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

353 
from a d e have "abs(a+b) <= sup ?m ?n" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

354 
by (drule_tac abs_leI, auto) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

355 
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

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

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

358 

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

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

360 

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

361 
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

362 
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

363 
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

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

365 
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

366 
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

367 
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

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

371 
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

372 
shows "\<bar>a\<bar> = (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

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

374 

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

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

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

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

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

379 
hence 2: "a <= c+(b)" 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

380 
have 3: "(b) <= abs b" by (rule abs_ge_minus_self) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

381 
show ?thesis by (rule le_add_right_mono[OF 2 3]) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

383 

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

384 
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

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

386 

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

387 
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

388 
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

389 

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

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

391 

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

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

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

394 
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

395 
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

396 
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

397 
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

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

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

400 
have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow> 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

402 
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

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

404 
apply (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

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

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

407 
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

408 
note addm = add_mono[of "0::'a" _ "0::'a", simplified] 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

409 
note addm2 = add_mono[of _ "0::'a" _ "0::'a", simplified] 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

410 
have xy: " ?x <= ?y" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

412 
apply (rule_tac y="0::'a" in order_trans) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

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

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

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

418 
have yx: "?y <= ?x" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

420 
apply (rule_tac y=0 in order_trans) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

421 
apply (rule addm2, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

422 
apply (rule addm, (simp add: mult_nonneg_nonpos mult_nonneg_nonpos2)+) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

424 
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

425 
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

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

427 
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

428 
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

429 
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

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

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

432 

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

433 
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

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

435 
fix a b :: "'a\<Colon> lattice_ring" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

437 
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

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

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

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

441 
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

442 
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

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

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

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

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

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

448 
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

449 
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

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

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

452 
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

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

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

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

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

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

458 
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

459 
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

460 
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

461 
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

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

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

464 
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

465 
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

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) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

469 
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

470 
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

471 
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

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

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

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

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

476 

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

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

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

479 
"a1 <= (a::'a::lattice_ring)" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

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

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

484 
"a * b <= pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + 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

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

486 
have "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

487 
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

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

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

490 
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

491 
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

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

493 
by (simp_all add: prems mult_mono) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

494 
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

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

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

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

498 
moreover have "pprt a * nprt b2 <= 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

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

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

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

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

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

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

505 
have "nprt a * pprt b <= nprt a2 * pprt 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: mult_right_mono prems) 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

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

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

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

512 
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

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

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

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

516 
moreover have "nprt a * nprt b1 <= 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

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

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

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

520 
qed 
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  (rule add_mono  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 

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

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

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

527 
"a1 <= (a::'a::lattice_ring)" 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

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

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

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

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

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

534 
from prems have a1:" a2 <= a" by auto 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

535 
from prems have a2: "a <= a1" by auto 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

536 
from mult_le_prts[of "a2" "a" "a1" "b1" b "b2", OF a1 a2 prems(3) prems(4), simplified nprt_neg pprt_neg] 
e42e7f133d94
separate library theory for type classes combining lattices with various algebraic structures; c.f. cs. 7efe662e41b4
haftmann
parents:
diff
changeset

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

538 
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

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

540 
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

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

542 

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

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

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

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

546 
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

547 
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

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

549 

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

550 
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

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

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

553 
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

554 
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

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

556 

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

557 
end 