author  wenzelm 
Fri, 14 Mar 2014 10:08:36 +0100  
changeset 56140  ed92ce2ac88e 
parent 55803  74d3fe9031d8 
child 56993  e5366291d6aa 
permissions  rwrr 
54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

1 
(* Title: HOL/Lattices_Big.thy 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

2 
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

3 
with contributions by Jeremy Avigad 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

4 
*) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

5 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

6 
header {* Big infimum (minimum) and supremum (maximum) over finite (nonempty) sets *} 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

7 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

8 
theory Lattices_Big 
55089
181751ad852f
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
blanchet
parents:
54868
diff
changeset

9 
imports Finite_Set Option 
54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

10 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

11 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

12 
subsection {* Generic lattice operations over a set *} 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

13 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

14 
no_notation times (infixl "*" 70) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

15 
no_notation Groups.one ("1") 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

16 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

17 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

18 
subsubsection {* Without neutral element *} 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

19 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

20 
locale semilattice_set = semilattice 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

21 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

22 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

23 
interpretation comp_fun_idem f 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

24 
by default (simp_all add: fun_eq_iff left_commute) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

25 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

26 
definition F :: "'a set \<Rightarrow> 'a" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

27 
where 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

28 
eq_fold': "F A = the (Finite_Set.fold (\<lambda>x y. Some (case y of None \<Rightarrow> x  Some z \<Rightarrow> f x z)) None A)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

29 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

30 
lemma eq_fold: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

31 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

32 
shows "F (insert x A) = Finite_Set.fold f x A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

33 
proof (rule sym) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

34 
let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x  Some z \<Rightarrow> f x z)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

35 
interpret comp_fun_idem "?f" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

36 
by default (simp_all add: fun_eq_iff commute left_commute split: option.split) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

37 
from assms show "Finite_Set.fold f x A = F (insert x A)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

38 
proof induct 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

39 
case empty then show ?case by (simp add: eq_fold') 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

40 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

41 
case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold') 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

42 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

43 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

44 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

45 
lemma singleton [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

46 
"F {x} = x" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

47 
by (simp add: eq_fold) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

48 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

49 
lemma insert_not_elem: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

50 
assumes "finite A" and "x \<notin> A" and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

51 
shows "F (insert x A) = x * F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

52 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

53 
from `A \<noteq> {}` obtain b where "b \<in> A" by blast 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

54 
then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

55 
with `finite A` and `x \<notin> A` 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

56 
have "finite (insert x B)" and "b \<notin> insert x B" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

57 
then have "F (insert b (insert x B)) = x * F (insert b B)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

58 
by (simp add: eq_fold) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

59 
then show ?thesis by (simp add: * insert_commute) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

60 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

61 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

62 
lemma in_idem: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

63 
assumes "finite A" and "x \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

64 
shows "x * F A = F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

65 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

66 
from assms have "A \<noteq> {}" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

67 
with `finite A` show ?thesis using `x \<in> A` 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

68 
by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

69 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

70 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

71 
lemma insert [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

72 
assumes "finite A" and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

73 
shows "F (insert x A) = x * F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

74 
using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

75 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

76 
lemma union: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

77 
assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

78 
shows "F (A \<union> B) = F A * F B" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

79 
using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

80 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

81 
lemma remove: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

82 
assumes "finite A" and "x \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

83 
shows "F A = (if A  {x} = {} then x else x * F (A  {x}))" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

84 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

85 
from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

86 
with assms show ?thesis by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

87 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

88 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

89 
lemma insert_remove: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

90 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

91 
shows "F (insert x A) = (if A  {x} = {} then x else x * F (A  {x}))" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

92 
using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

93 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

94 
lemma subset: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

95 
assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

96 
shows "F B * F A = F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

97 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

98 
from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

99 
with assms show ?thesis by (simp add: union [symmetric] Un_absorb1) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

100 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

101 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

102 
lemma closed: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

103 
assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

104 
shows "F A \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

105 
using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

106 
case singleton then show ?case by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

107 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

108 
case insert with elem show ?case by force 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

109 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

110 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

111 
lemma hom_commute: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

112 
assumes hom: "\<And>x y. h (x * y) = h x * h y" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

113 
and N: "finite N" "N \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

114 
shows "h (F N) = F (h ` N)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

115 
using N proof (induct rule: finite_ne_induct) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

116 
case singleton thus ?case by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

117 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

118 
case (insert n N) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

119 
then have "h (F (insert n N)) = h (n * F N)" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

120 
also have "\<dots> = h n * h (F N)" by (rule hom) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

121 
also have "h (F N) = F (h ` N)" by (rule insert) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

122 
also have "h n * \<dots> = F (insert (h n) (h ` N))" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

123 
using insert by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

124 
also have "insert (h n) (h ` N) = h ` insert n N" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

125 
finally show ?case . 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

126 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

127 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

128 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

129 

54745  130 
locale semilattice_order_set = binary?: semilattice_order + semilattice_set 
54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

131 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

132 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

133 
lemma bounded_iff: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

134 
assumes "finite A" and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

135 
shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

136 
using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

137 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

138 
lemma boundedI: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

139 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

140 
assumes "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

141 
assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

142 
shows "x \<preceq> F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

143 
using assms by (simp add: bounded_iff) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

144 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

145 
lemma boundedE: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

146 
assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

147 
obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

148 
using assms by (simp add: bounded_iff) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

149 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

150 
lemma coboundedI: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

151 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

152 
and "a \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

153 
shows "F A \<preceq> a" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

154 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

155 
from assms have "A \<noteq> {}" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

156 
from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

157 
proof (induct rule: finite_ne_induct) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

158 
case singleton thus ?case by (simp add: refl) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

159 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

160 
case (insert x B) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

161 
from insert have "a = x \<or> a \<in> B" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

162 
then show ?case using insert by (auto intro: coboundedI2) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

163 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

164 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

165 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

166 
lemma antimono: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

167 
assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

168 
shows "F B \<preceq> F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

169 
proof (cases "A = B") 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

170 
case True then show ?thesis by (simp add: refl) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

171 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

172 
case False 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

173 
have B: "B = A \<union> (B  A)" using `A \<subseteq> B` by blast 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

174 
then have "F B = F (A \<union> (B  A))" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

175 
also have "\<dots> = F A * F (B  A)" using False assms by (subst union) (auto intro: finite_subset) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

176 
also have "\<dots> \<preceq> F A" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

177 
finally show ?thesis . 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

178 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

179 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

180 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

181 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

182 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

183 
subsubsection {* With neutral element *} 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

184 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

185 
locale semilattice_neutr_set = semilattice_neutr 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

186 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

187 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

188 
interpretation comp_fun_idem f 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

189 
by default (simp_all add: fun_eq_iff left_commute) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

190 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

191 
definition F :: "'a set \<Rightarrow> 'a" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

192 
where 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

193 
eq_fold: "F A = Finite_Set.fold f 1 A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

194 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

195 
lemma infinite [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

196 
"\<not> finite A \<Longrightarrow> F A = 1" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

197 
by (simp add: eq_fold) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

198 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

199 
lemma empty [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

200 
"F {} = 1" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

201 
by (simp add: eq_fold) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

202 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

203 
lemma insert [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

204 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

205 
shows "F (insert x A) = x * F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

206 
using assms by (simp add: eq_fold) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

207 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

208 
lemma in_idem: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

209 
assumes "finite A" and "x \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

210 
shows "x * F A = F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

211 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

212 
from assms have "A \<noteq> {}" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

213 
with `finite A` show ?thesis using `x \<in> A` 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

214 
by (induct A rule: finite_ne_induct) (auto simp add: ac_simps) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

215 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

216 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

217 
lemma union: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

218 
assumes "finite A" and "finite B" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

219 
shows "F (A \<union> B) = F A * F B" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

220 
using assms by (induct A) (simp_all add: ac_simps) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

221 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

222 
lemma remove: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

223 
assumes "finite A" and "x \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

224 
shows "F A = x * F (A  {x})" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

225 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

226 
from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

227 
with assms show ?thesis by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

228 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

229 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

230 
lemma insert_remove: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

231 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

232 
shows "F (insert x A) = x * F (A  {x})" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

233 
using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

234 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

235 
lemma subset: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

236 
assumes "finite A" and "B \<subseteq> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

237 
shows "F B * F A = F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

238 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

239 
from assms have "finite B" by (auto dest: finite_subset) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

240 
with assms show ?thesis by (simp add: union [symmetric] Un_absorb1) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

241 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

242 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

243 
lemma closed: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

244 
assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

245 
shows "F A \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

246 
using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

247 
case singleton then show ?case by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

248 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

249 
case insert with elem show ?case by force 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

250 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

251 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

252 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

253 

54745  254 
locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set 
54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

255 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

256 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

257 
lemma bounded_iff: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

258 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

259 
shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

260 
using assms by (induct A) (simp_all add: bounded_iff) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

261 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

262 
lemma boundedI: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

263 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

264 
assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

265 
shows "x \<preceq> F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

266 
using assms by (simp add: bounded_iff) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

267 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

268 
lemma boundedE: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

269 
assumes "finite A" and "x \<preceq> F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

270 
obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

271 
using assms by (simp add: bounded_iff) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

272 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

273 
lemma coboundedI: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

274 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

275 
and "a \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

276 
shows "F A \<preceq> a" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

277 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

278 
from assms have "A \<noteq> {}" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

279 
from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

280 
proof (induct rule: finite_ne_induct) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

281 
case singleton thus ?case by (simp add: refl) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

282 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

283 
case (insert x B) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

284 
from insert have "a = x \<or> a \<in> B" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

285 
then show ?case using insert by (auto intro: coboundedI2) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

286 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

287 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

288 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

289 
lemma antimono: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

290 
assumes "A \<subseteq> B" and "finite B" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

291 
shows "F B \<preceq> F A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

292 
proof (cases "A = B") 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

293 
case True then show ?thesis by (simp add: refl) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

294 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

295 
case False 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

296 
have B: "B = A \<union> (B  A)" using `A \<subseteq> B` by blast 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

297 
then have "F B = F (A \<union> (B  A))" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

298 
also have "\<dots> = F A * F (B  A)" using False assms by (subst union) (auto intro: finite_subset) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

299 
also have "\<dots> \<preceq> F A" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

300 
finally show ?thesis . 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

301 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

302 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

303 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

304 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

305 
notation times (infixl "*" 70) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

306 
notation Groups.one ("1") 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

307 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

308 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

309 
subsection {* Lattice operations on finite sets *} 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

310 

54868  311 
context semilattice_inf 
312 
begin 

313 

314 
definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) 

54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

315 
where 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

316 
"Inf_fin = semilattice_set.F inf" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

317 

54868  318 
sublocale Inf_fin!: semilattice_order_set inf less_eq less 
54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

319 
where 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

320 
"semilattice_set.F inf = Inf_fin" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

321 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

322 
show "semilattice_order_set inf less_eq less" .. 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

323 
then interpret Inf_fin!: semilattice_order_set inf less_eq less . 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

324 
from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

325 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

326 

54868  327 
end 
328 

329 
context semilattice_sup 

330 
begin 

331 

332 
definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) 

333 
where 

334 
"Sup_fin = semilattice_set.F sup" 

335 

336 
sublocale Sup_fin!: semilattice_order_set sup greater_eq greater 

54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

337 
where 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

338 
"semilattice_set.F sup = Sup_fin" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

339 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

340 
show "semilattice_order_set sup greater_eq greater" .. 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

341 
then interpret Sup_fin!: semilattice_order_set sup greater_eq greater . 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

342 
from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

343 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

344 

54868  345 
end 
346 

54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

347 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

348 
subsection {* Infimum and Supremum over nonempty sets *} 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

349 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

350 
context lattice 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

351 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

352 

54745  353 
lemma Inf_fin_le_Sup_fin [simp]: 
354 
assumes "finite A" and "A \<noteq> {}" 

355 
shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" 

356 
proof  

357 
from `A \<noteq> {}` obtain a where "a \<in> A" by blast 

358 
with `finite A` have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI) 

359 
moreover from `finite A` `a \<in> A` have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI) 

360 
ultimately show ?thesis by (rule order_trans) 

361 
qed 

54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

362 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

363 
lemma sup_Inf_absorb [simp]: 
54745  364 
"finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a" 
365 
by (rule sup_absorb2) (rule Inf_fin.coboundedI) 

54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

366 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

367 
lemma inf_Sup_absorb [simp]: 
54745  368 
"finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a" 
369 
by (rule inf_absorb1) (rule Sup_fin.coboundedI) 

54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

370 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

371 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

372 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

373 
context distrib_lattice 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

374 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

375 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

376 
lemma sup_Inf1_distrib: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

377 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

378 
and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

379 
shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x aa. a \<in> A}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

380 
using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

381 
(rule arg_cong [where f="Inf_fin"], blast) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

382 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

383 
lemma sup_Inf2_distrib: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

384 
assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

385 
shows "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a ba b. a \<in> A \<and> b \<in> B}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

386 
using A proof (induct rule: finite_ne_induct) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

387 
case singleton then show ?case 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

388 
by (simp add: sup_Inf1_distrib [OF B]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

389 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

390 
case (insert x A) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

391 
have finB: "finite {sup x b b. b \<in> B}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

392 
by (rule finite_surj [where f = "sup x", OF B(1)], auto) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

393 
have finAB: "finite {sup a b a b. a \<in> A \<and> b \<in> B}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

394 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

395 
have "{sup a b a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

396 
by blast 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

397 
thus ?thesis by(simp add: insert(1) B(1)) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

398 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

399 
have ne: "{sup a b a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

400 
have "sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB) = sup (inf x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA)) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

401 
using insert by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

402 
also have "\<dots> = inf (sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB)) (sup (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nB))" by(rule sup_inf_distrib2) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

403 
also have "\<dots> = inf (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x bb. b \<in> B}) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a ba b. a \<in> A \<and> b \<in> B})" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

404 
using insert by(simp add:sup_Inf1_distrib[OF B]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

405 
also have "\<dots> = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n({sup x b b. b \<in> B} \<union> {sup a b a b. a \<in> A \<and> b \<in> B})" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

406 
(is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M") 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

407 
using B insert 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

408 
by (simp add: Inf_fin.union [OF finB _ finAB ne]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

409 
also have "?M = {sup a b a b. a \<in> insert x A \<and> b \<in> B}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

410 
by blast 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

411 
finally show ?case . 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

412 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

413 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

414 
lemma inf_Sup1_distrib: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

415 
assumes "finite A" and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

416 
shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x aa. a \<in> A}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

417 
using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

418 
(rule arg_cong [where f="Sup_fin"], blast) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

419 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

420 
lemma inf_Sup2_distrib: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

421 
assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

422 
shows "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a ba b. a \<in> A \<and> b \<in> B}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

423 
using A proof (induct rule: finite_ne_induct) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

424 
case singleton thus ?case 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

425 
by(simp add: inf_Sup1_distrib [OF B]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

426 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

427 
case (insert x A) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

428 
have finB: "finite {inf x b b. b \<in> B}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

429 
by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

430 
have finAB: "finite {inf a b a b. a \<in> A \<and> b \<in> B}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

431 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

432 
have "{inf a b a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

433 
by blast 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

434 
thus ?thesis by(simp add: insert(1) B(1)) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

435 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

436 
have ne: "{inf a b a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

437 
have "inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB) = inf (sup x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA)) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

438 
using insert by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

439 
also have "\<dots> = sup (inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB)) (inf (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) (\<Squnion>\<^sub>f\<^sub>i\<^sub>nB))" by(rule inf_sup_distrib2) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

440 
also have "\<dots> = sup (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x bb. b \<in> B}) (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a ba b. a \<in> A \<and> b \<in> B})" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

441 
using insert by(simp add:inf_Sup1_distrib[OF B]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

442 
also have "\<dots> = \<Squnion>\<^sub>f\<^sub>i\<^sub>n({inf x b b. b \<in> B} \<union> {inf a b a b. a \<in> A \<and> b \<in> B})" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

443 
(is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M") 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

444 
using B insert 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

445 
by (simp add: Sup_fin.union [OF finB _ finAB ne]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

446 
also have "?M = {inf a b a b. a \<in> insert x A \<and> b \<in> B}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

447 
by blast 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

448 
finally show ?case . 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

449 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

450 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

451 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

452 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

453 
context complete_lattice 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

454 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

455 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

456 
lemma Inf_fin_Inf: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

457 
assumes "finite A" and "A \<noteq> {}" 
54868  458 
shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = \<Sqinter>A" 
54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

459 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

460 
from assms obtain b B where "A = insert b B" and "finite B" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

461 
then show ?thesis 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

462 
by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

463 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

464 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

465 
lemma Sup_fin_Sup: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

466 
assumes "finite A" and "A \<noteq> {}" 
54868  467 
shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = \<Squnion>A" 
54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

468 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

469 
from assms obtain b B where "A = insert b B" and "finite B" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

470 
then show ?thesis 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

471 
by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

472 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

473 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

474 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

475 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

476 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

477 
subsection {* Minimum and Maximum over nonempty sets *} 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

478 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

479 
context linorder 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

480 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

481 

54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

482 
definition Min :: "'a set \<Rightarrow> 'a" 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

483 
where 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

484 
"Min = semilattice_set.F min" 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

485 

a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

486 
definition Max :: "'a set \<Rightarrow> 'a" 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

487 
where 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

488 
"Max = semilattice_set.F max" 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

489 

a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

490 
sublocale Min!: semilattice_order_set min less_eq less 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

491 
+ Max!: semilattice_order_set max greater_eq greater 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

492 
where 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

493 
"semilattice_set.F min = Min" 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

494 
and "semilattice_set.F max = Max" 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

495 
proof  
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

496 
show "semilattice_order_set min less_eq less" by default (auto simp add: min_def) 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

497 
then interpret Min!: semilattice_order_set min less_eq less . 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

498 
show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def) 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

499 
then interpret Max!: semilattice_order_set max greater_eq greater . 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

500 
from Min_def show "semilattice_set.F min = Min" by rule 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

501 
from Max_def show "semilattice_set.F max = Max" by rule 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

502 
qed 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

503 

a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

504 
end 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

505 

a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

506 
text {* An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *} 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

507 

a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

508 
lemma Inf_fin_Min: 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

509 
"Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)" 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

510 
by (simp add: Inf_fin_def Min_def inf_min) 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

511 

a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

512 
lemma Sup_fin_Max: 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

513 
"Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)" 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

514 
by (simp add: Sup_fin_def Max_def sup_max) 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

515 

a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

516 
context linorder 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

517 
begin 
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset

518 

54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

519 
lemma dual_min: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

520 
"ord.min greater_eq = max" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

521 
by (auto simp add: ord.min_def max_def fun_eq_iff) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

522 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

523 
lemma dual_max: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

524 
"ord.max greater_eq = min" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

525 
by (auto simp add: ord.max_def min_def fun_eq_iff) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

526 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

527 
lemma dual_Min: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

528 
"linorder.Min greater_eq = Max" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

529 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

530 
interpret dual!: linorder greater_eq greater by (fact dual_linorder) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

531 
show ?thesis by (simp add: dual.Min_def dual_min Max_def) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

532 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

533 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

534 
lemma dual_Max: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

535 
"linorder.Max greater_eq = Min" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

536 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

537 
interpret dual!: linorder greater_eq greater by (fact dual_linorder) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

538 
show ?thesis by (simp add: dual.Max_def dual_max Min_def) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

539 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

540 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

541 
lemmas Min_singleton = Min.singleton 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

542 
lemmas Max_singleton = Max.singleton 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

543 
lemmas Min_insert = Min.insert 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

544 
lemmas Max_insert = Max.insert 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

545 
lemmas Min_Un = Min.union 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

546 
lemmas Max_Un = Max.union 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

547 
lemmas hom_Min_commute = Min.hom_commute 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

548 
lemmas hom_Max_commute = Max.hom_commute 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

549 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

550 
lemma Min_in [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

551 
assumes "finite A" and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

552 
shows "Min A \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

553 
using assms by (auto simp add: min_def Min.closed) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

554 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

555 
lemma Max_in [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

556 
assumes "finite A" and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

557 
shows "Max A \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

558 
using assms by (auto simp add: max_def Max.closed) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

559 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

560 
lemma Min_le [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

561 
assumes "finite A" and "x \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

562 
shows "Min A \<le> x" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

563 
using assms by (fact Min.coboundedI) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

564 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

565 
lemma Max_ge [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

566 
assumes "finite A" and "x \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

567 
shows "x \<le> Max A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

568 
using assms by (fact Max.coboundedI) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

569 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

570 
lemma Min_eqI: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

571 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

572 
assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

573 
and "x \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

574 
shows "Min A = x" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

575 
proof (rule antisym) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

576 
from `x \<in> A` have "A \<noteq> {}" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

577 
with assms show "Min A \<ge> x" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

578 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

579 
from assms show "x \<ge> Min A" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

580 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

581 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

582 
lemma Max_eqI: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

583 
assumes "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

584 
assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

585 
and "x \<in> A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

586 
shows "Max A = x" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

587 
proof (rule antisym) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

588 
from `x \<in> A` have "A \<noteq> {}" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

589 
with assms show "Max A \<le> x" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

590 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

591 
from assms show "x \<le> Max A" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

592 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

593 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

594 
context 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

595 
fixes A :: "'a set" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

596 
assumes fin_nonempty: "finite A" "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

597 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

598 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

599 
lemma Min_ge_iff [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

600 
"x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

601 
using fin_nonempty by (fact Min.bounded_iff) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

602 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

603 
lemma Max_le_iff [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

604 
"Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

605 
using fin_nonempty by (fact Max.bounded_iff) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

606 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

607 
lemma Min_gr_iff [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

608 
"x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

609 
using fin_nonempty by (induct rule: finite_ne_induct) simp_all 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

610 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

611 
lemma Max_less_iff [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

612 
"Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

613 
using fin_nonempty by (induct rule: finite_ne_induct) simp_all 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

614 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

615 
lemma Min_le_iff: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

616 
"Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

617 
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

618 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

619 
lemma Max_ge_iff: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

620 
"x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

621 
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

622 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

623 
lemma Min_less_iff: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

624 
"Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

625 
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

626 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

627 
lemma Max_gr_iff: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

628 
"x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

629 
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

630 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

631 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

632 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

633 
lemma Min_antimono: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

634 
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

635 
shows "Min N \<le> Min M" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

636 
using assms by (fact Min.antimono) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

637 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

638 
lemma Max_mono: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

639 
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

640 
shows "Max M \<le> Max N" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

641 
using assms by (fact Max.antimono) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

642 

56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
55803
diff
changeset

643 
end 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
55803
diff
changeset

644 

ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
55803
diff
changeset

645 
context linorder (* FIXME *) 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
55803
diff
changeset

646 
begin 
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
55803
diff
changeset

647 

54744
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

648 
lemma mono_Min_commute: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

649 
assumes "mono f" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

650 
assumes "finite A" and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

651 
shows "f (Min A) = Min (f ` A)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

652 
proof (rule linorder_class.Min_eqI [symmetric]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

653 
from `finite A` show "finite (f ` A)" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

654 
from assms show "f (Min A) \<in> f ` A" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

655 
fix x 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

656 
assume "x \<in> f ` A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

657 
then obtain y where "y \<in> A" and "x = f y" .. 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

658 
with assms have "Min A \<le> y" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

659 
with `mono f` have "f (Min A) \<le> f y" by (rule monoE) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

660 
with `x = f y` show "f (Min A) \<le> x" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

661 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

662 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

663 
lemma mono_Max_commute: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

664 
assumes "mono f" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

665 
assumes "finite A" and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

666 
shows "f (Max A) = Max (f ` A)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

667 
proof (rule linorder_class.Max_eqI [symmetric]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

668 
from `finite A` show "finite (f ` A)" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

669 
from assms show "f (Max A) \<in> f ` A" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

670 
fix x 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

671 
assume "x \<in> f ` A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

672 
then obtain y where "y \<in> A" and "x = f y" .. 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

673 
with assms have "y \<le> Max A" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

674 
with `mono f` have "f y \<le> f (Max A)" by (rule monoE) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

675 
with `x = f y` show "x \<le> f (Max A)" by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

676 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

677 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

678 
lemma finite_linorder_max_induct [consumes 1, case_names empty insert]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

679 
assumes fin: "finite A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

680 
and empty: "P {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

681 
and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

682 
shows "P A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

683 
using fin empty insert 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

684 
proof (induct rule: finite_psubset_induct) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

685 
case (psubset A) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

686 
have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

687 
have fin: "finite A" by fact 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

688 
have empty: "P {}" by fact 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

689 
have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

690 
show "P A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

691 
proof (cases "A = {}") 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

692 
assume "A = {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

693 
then show "P A" using `P {}` by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

694 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

695 
let ?B = "A  {Max A}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

696 
let ?A = "insert (Max A) ?B" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

697 
have "finite ?B" using `finite A` by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

698 
assume "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

699 
with `finite A` have "Max A : A" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

700 
then have A: "?A = A" using insert_Diff_single insert_absorb by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

701 
then have "P ?B" using `P {}` step IH [of ?B] by blast 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

702 
moreover 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

703 
have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

704 
ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

705 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

706 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

707 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

708 
lemma finite_linorder_min_induct [consumes 1, case_names empty insert]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

709 
"\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

710 
by (rule linorder.finite_linorder_max_induct [OF dual_linorder]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

711 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

712 
lemma Least_Min: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

713 
assumes "finite {a. P a}" and "\<exists>a. P a" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

714 
shows "(LEAST a. P a) = Min {a. P a}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

715 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

716 
{ fix A :: "'a set" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

717 
assume A: "finite A" "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

718 
have "(LEAST a. a \<in> A) = Min A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

719 
using A proof (induct A rule: finite_ne_induct) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

720 
case singleton show ?case by (rule Least_equality) simp_all 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

721 
next 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

722 
case (insert a A) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

723 
have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

724 
by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

725 
with insert show ?case by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

726 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

727 
} from this [of "{a. P a}"] assms show ?thesis by simp 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

728 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

729 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

730 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

731 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

732 
context linordered_ab_semigroup_add 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

733 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

734 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

735 
lemma add_Min_commute: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

736 
fixes k 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

737 
assumes "finite N" and "N \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

738 
shows "k + Min N = Min {k + m  m. m \<in> N}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

739 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

740 
have "\<And>x y. k + min x y = min (k + x) (k + y)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

741 
by (simp add: min_def not_le) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

742 
(blast intro: antisym less_imp_le add_left_mono) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

743 
with assms show ?thesis 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

744 
using hom_Min_commute [of "plus k" N] 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

745 
by simp (blast intro: arg_cong [where f = Min]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

746 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

747 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

748 
lemma add_Max_commute: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

749 
fixes k 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

750 
assumes "finite N" and "N \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

751 
shows "k + Max N = Max {k + m  m. m \<in> N}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

752 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

753 
have "\<And>x y. k + max x y = max (k + x) (k + y)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

754 
by (simp add: max_def not_le) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

755 
(blast intro: antisym less_imp_le add_left_mono) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

756 
with assms show ?thesis 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

757 
using hom_Max_commute [of "plus k" N] 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

758 
by simp (blast intro: arg_cong [where f = Max]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

759 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

760 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

761 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

762 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

763 
context linordered_ab_group_add 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

764 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

765 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

766 
lemma minus_Max_eq_Min [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

767 
"finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow>  Max S = Min (uminus ` S)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

768 
by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

769 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

770 
lemma minus_Min_eq_Max [simp]: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

771 
"finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow>  Min S = Max (uminus ` S)" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

772 
by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

773 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

774 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

775 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

776 
context complete_linorder 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

777 
begin 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

778 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

779 
lemma Min_Inf: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

780 
assumes "finite A" and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

781 
shows "Min A = Inf A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

782 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

783 
from assms obtain b B where "A = insert b B" and "finite B" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

784 
then show ?thesis 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

785 
by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

786 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

787 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

788 
lemma Max_Sup: 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

789 
assumes "finite A" and "A \<noteq> {}" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

790 
shows "Max A = Sup A" 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

791 
proof  
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

792 
from assms obtain b B where "A = insert b B" and "finite B" by auto 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

793 
then show ?thesis 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

794 
by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b]) 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

795 
qed 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

796 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

797 
end 
1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

798 

1e7f2d296e19
more algebraic terminology for theories about big operators
haftmann
parents:
diff
changeset

799 
end 