# HG changeset patch # User haftmann # Date 1178785306 -7200 # Node ID 3c56b12fd9467e79e31412dbe119600ac40fd283 # Parent 8caf6da610e29d3ce51a3607f92f514ffe1a6a43 localized Min/Max diff -r 8caf6da610e2 -r 3c56b12fd946 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Thu May 10 10:21:44 2007 +0200 +++ b/src/HOL/Finite_Set.thy Thu May 10 10:21:46 2007 +0200 @@ -457,19 +457,14 @@ subsubsection {* Commutative monoids *} +(*FIXME integrate with Orderings.thy/OrderedGroup.thy*) locale ACf = fixes f :: "'a => 'a => 'a" (infixl "\" 70) assumes commute: "x \ y = y \ x" and assoc: "(x \ y) \ z = x \ (y \ z)" - -locale ACe = ACf + - fixes e :: 'a - assumes ident [simp]: "x \ e = x" - -locale ACIf = ACf + - assumes idem: "x \ x = x" - -lemma (in ACf) left_commute: "x \ (y \ z) = y \ (x \ z)" +begin + +lemma left_commute: "x \ (y \ z) = y \ (x \ z)" proof - have "x \ (y \ z) = (y \ z) \ x" by (simp only: commute) also have "... = y \ (z \ x)" by (simp only: assoc) @@ -477,30 +472,38 @@ finally show ?thesis . qed -lemmas (in ACf) AC = assoc commute left_commute - -lemma (in ACe) left_ident [simp]: "e \ x = x" +lemmas AC = assoc commute left_commute + +end + +locale ACe = ACf + + fixes e :: 'a + assumes ident [simp]: "x \ e = x" +begin + +lemma left_ident [simp]: "e \ x = x" proof - have "x \ e = x" by (rule ident) thus ?thesis by (subst commute) qed -lemma (in ACIf) idem2: "x \ (x \ y) = x \ y" +end + +locale ACIf = ACf + + assumes idem: "x \ x = x" +begin + +lemma idem2: "x \ (x \ y) = x \ y" proof - have "x \ (x \ y) = (x \ x) \ y" by(simp add:assoc) also have "\ = x \ y" by(simp add:idem) finally show ?thesis . qed -lemmas (in ACIf) ACI = AC idem idem2 - -text{* Interpretation of locales: *} - -interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"] - by unfold_locales (auto intro: add_assoc add_commute) - -interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"] - by unfold_locales (auto intro: mult_assoc mult_commute) +lemmas ACI = AC idem idem2 + +end + subsubsection{*From @{term foldSet} to @{term fold}*} @@ -791,6 +794,15 @@ done +text{* Interpretation of locales -- see OrderedGroup.thy *} + +interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"] + by unfold_locales (auto intro: add_assoc add_commute) + +interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"] + by unfold_locales (auto intro: mult_assoc mult_commute) + + subsection {* Generalized summation over a set *} constdefs @@ -1657,9 +1669,6 @@ subsubsection {* Cardinality of unions *} -lemma of_nat_id[simp]: "(of_nat n :: nat) = n" -by(induct n) auto - lemma card_UN_disjoint: "finite I ==> (ALL i:I. finite (A i)) ==> (ALL i:I. ALL j:I. i \ j --> A i Int A j = {}) ==> @@ -1796,9 +1805,8 @@ "fold1 f A == THE x. fold1Set f A x" lemma fold1Set_nonempty: - "fold1Set f A x \ A \ {}" -by(erule fold1Set.cases, simp_all) - + "fold1Set f A x \ A \ {}" + by(erule fold1Set.cases, simp_all) inductive_cases2 empty_fold1SetE [elim!]: "fold1Set f {} x" @@ -1808,7 +1816,7 @@ lemma fold1Set_sing [iff]: "(fold1Set f {a} b) = (a = b)" by (blast intro: foldSet.intros elim: foldSet.cases) -lemma fold1_singleton[simp]: "fold1 f {a} = a" +lemma fold1_singleton [simp]: "fold1 f {a} = a" by (unfold fold1_def) blast lemma finite_nonempty_imp_fold1Set: @@ -1914,18 +1922,34 @@ qed qed +lemma (in ACIf) hom_fold1_commute: +assumes hom: "!!x y. h(f x y) = f (h x) (h y)" +and N: "finite N" "N \ {}" shows "h(fold1 f N) = fold1 f (h ` N)" +using N proof (induct rule: finite_ne_induct) + case singleton thus ?case by simp +next + case (insert n N) + then have "h(fold1 f (insert n N)) = h(f n (fold1 f N))" by simp + also have "\ = f (h n) (h(fold1 f N))" by(rule hom) + also have "h(fold1 f N) = fold1 f (h ` N)" by(rule insert) + also have "f (h n) \ = fold1 f (insert (h n) (h ` N))" + using insert by(simp) + also have "insert (h n) (h ` N) = h ` insert n N" by simp + finally show ?case . +qed + text{* Now the recursion rules for definitions: *} -lemma fold1_singleton_def: "g \ fold1 f \ g {a} = a" +lemma fold1_singleton_def: "g = fold1 f \ g {a} = a" by(simp add:fold1_singleton) lemma (in ACf) fold1_insert_def: - "\ g \ fold1 f; finite A; x \ A; A \ {} \ \ g(insert x A) = x \ (g A)" + "\ g = fold1 f; finite A; x \ A; A \ {} \ \ g (insert x A) = x \ (g A)" by(simp add:fold1_insert) lemma (in ACIf) fold1_insert_idem_def: - "\ g \ fold1 f; finite A; A \ {} \ \ g(insert x A) = x \ (g A)" + "\ g = fold1 f; finite A; A \ {} \ \ g (insert x A) = x \ (g A)" by(simp add:fold1_insert_idem) subsubsection{* Determinacy for @{term fold1Set} *} @@ -1977,22 +2001,38 @@ empty_fold1SetE [rule del] insert_fold1SetE [rule del] -- {* No more proofs involve these relations. *} + subsubsection{* Semi-Lattices *} -(*FIXME integrate with Orderings.thy/OrderedGroup.thy*) -locale ACIfSL = ACIf + - fixes below :: "'a \ 'a \ bool" (infixl "\" 50) - and strict_below :: "'a \ 'a \ bool" (infixl "\" 50) - assumes below_def: "(x \ y) = (x\y = x)" - defines strict_below_def: "(x \ y) \ (x \ y \ x \ y)" - -locale ACIfSLlin = ACIfSL + - assumes lin: "x\y \ {x,y}" - -lemma (in ACIfSL) below_refl[simp]: "x \ x" -by(simp add: below_def idem) - -lemma (in ACIfSL) below_f_conv[simp]: "x \ y \ z = (x \ y \ x \ z)" +locale ACIfSL = ord + ACIf + + assumes below_def: "x \ y \ x \ y = x" + and strict_below_def: "x \ y \ x \ y \ x \ y" +begin + +lemma below_refl [simp]: "x \<^loc>\ x" + by (simp add: below_def idem) + +lemma below_antisym: + assumes xy: "x \<^loc>\ y" and yx: "y \<^loc>\ x" + shows "x = y" + using xy [unfolded below_def, symmetric] + yx [unfolded below_def commute] + by (rule trans) + +lemma below_trans: + assumes xy: "x \<^loc>\ y" and yz: "y \<^loc>\ z" + shows "x \<^loc>\ z" +proof - + from xy have x_xy: "x \ y = x" by (simp add: below_def) + from yz have y_yz: "y \ z = y" by (simp add: below_def) + from y_yz have "x \ y \ z = x \ y" by (simp add: assoc) + with x_xy have "x \ y \ z = x" by simp + moreover from x_xy have "x \ z = x \ y \ z" by simp + ultimately have "x \ z = x" by simp + then show ?thesis by (simp add: below_def) +qed + +lemma below_f_conv [simp]: "x \ y \ z = (x \ y \ x \ z)" proof assume "x \ y \ z" hence xyzx: "x \ (y \ z) = x" by(simp add: below_def) @@ -2020,7 +2060,17 @@ finally show "x \ y \ z" by(simp_all add: below_def) qed -lemma (in ACIfSLlin) above_f_conv: +end + +interpretation ACIfSL < order +by unfold_locales + (simp add: strict_below_def, auto intro: below_refl below_trans below_antisym) + +locale ACIfSLlin = ACIfSL + + assumes lin: "x\y \ {x,y}" +begin + +lemma above_f_conv: "x \ y \ z = (x \ z \ y \ z)" proof assume a: "x \ y \ z" @@ -2047,17 +2097,21 @@ qed qed - -lemma (in ACIfSLlin) strict_below_f_conv[simp]: "x \ y \ z = (x \ y \ x \ z)" +lemma strict_below_f_conv[simp]: "x \ y \ z = (x \ y \ x \ z)" apply(simp add: strict_below_def) using lin[of y z] by (auto simp:below_def ACI) - -lemma (in ACIfSLlin) strict_above_f_conv: +lemma strict_above_f_conv: "x \ y \ z = (x \ z \ y \ z)" apply(simp add: strict_below_def above_f_conv) using lin[of y z] lin[of x z] by (auto simp:below_def ACI) +end + +interpretation ACIfSLlin < linorder + by unfold_locales + (insert lin [simplified insert_iff], simp add: below_def commute) + subsubsection{* Lemmas about @{text fold1} *} @@ -2129,7 +2183,6 @@ qed qed - lemma (in ACIfSLlin) fold1_below_iff: assumes A: "finite A" "A \ {}" shows "fold1 f A \ x = (\a\A. a \ x)" @@ -2142,7 +2195,6 @@ using A by(induct rule:finite_ne_induct)(simp_all add:strict_above_f_conv) - lemma (in ACIfSLlin) fold1_antimono: assumes "A \ {}" and "A \ B" and "finite B" shows "fold1 f B \ fold1 f A" @@ -2165,40 +2217,35 @@ qed - -subsubsection{* Lattices *} - -(*FIXME integrate with FixedPoint.thy*) -locale Lattice = lattice + - fixes Inf :: "'a set \ 'a" ("\_" [900] 900) - and Sup :: "'a set \ 'a" ("\_" [900] 900) - defines "Inf == fold1 inf" and "Sup == fold1 sup" - -locale Distrib_Lattice = distrib_lattice + Lattice - -text{* Lattices are semilattices *} - -lemma (in Lattice) ACf_inf: "ACf inf" -by(blast intro: ACf.intro inf_commute inf_assoc) - -lemma (in Lattice) ACf_sup: "ACf sup" -by(blast intro: ACf.intro sup_commute sup_assoc) - -lemma (in Lattice) ACIf_inf: "ACIf inf" +subsubsection {* Fold1 in lattices with @{const inf} and @{const sup} *} + +text{* + As an application of @{text fold1} we define infimum + and supremum in (not necessarily complete!) lattices + over (non-empty) sets by means of @{text fold1}. +*} + +lemma (in lower_semilattice) ACf_inf: "ACf (op \)" + by (blast intro: ACf.intro inf_commute inf_assoc) + +lemma (in upper_semilattice) ACf_sup: "ACf (op \)" + by (blast intro: ACf.intro sup_commute sup_assoc) + +lemma (in lower_semilattice) ACIf_inf: "ACIf (op \)" apply(rule ACIf.intro) apply(rule ACf_inf) apply(rule ACIf_axioms.intro) apply(rule inf_idem) done -lemma (in Lattice) ACIf_sup: "ACIf sup" +lemma (in upper_semilattice) ACIf_sup: "ACIf (op \)" apply(rule ACIf.intro) apply(rule ACf_sup) apply(rule ACIf_axioms.intro) apply(rule sup_idem) done -lemma (in Lattice) ACIfSL_inf: "ACIfSL inf (op \)" +lemma (in lower_semilattice) ACIfSL_inf: "ACIfSL (op \<^loc>\) (op \<^loc><) (op \)" apply(rule ACIfSL.intro) apply(rule ACIf.intro) apply(rule ACf_inf) @@ -2208,10 +2255,10 @@ apply(blast intro: antisym inf_le1 inf_le2 inf_greatest refl) apply(erule subst) apply(rule inf_le2) +apply(rule less_le) done -lemma (in Lattice) ACIfSL_sup: "ACIfSL sup (%x y. y \ x)" -(* FIXME: insert ACf_sup and use unfold_locales *) +lemma (in upper_semilattice) ACIfSL_sup: "ACIfSL (%x y. y \<^loc>\ x) (%x y. y \<^loc>< x) (op \)" apply(rule ACIfSL.intro) apply(rule ACIf.intro) apply(rule ACf_sup) @@ -2221,10 +2268,25 @@ apply(blast intro: antisym sup_ge1 sup_ge2 sup_least refl) apply(erule subst) apply(rule sup_ge2) +apply(simp add: neq_commute less_le) done - -subsubsection{* Fold laws in lattices *} +locale Lattice = lattice -- {* we do not pollute the @{text lattice} clas *} +begin + +definition + Inf :: "'a set \ 'a" ("\_" [900] 900) +where + "Inf = fold1 (op \)" + +definition + Sup :: "'a set \ 'a" ("\_" [900] 900) +where + "Sup = fold1 (op \)" + +end + +locale Distrib_Lattice = distrib_lattice + Lattice lemma (in Lattice) Inf_le_Sup[simp]: "\ finite A; A \ {} \ \ \A \ \A" apply(unfold Sup_def Inf_def) @@ -2246,23 +2308,6 @@ "\ finite A; A \ {}; a \ A \ \ (a \ \A) = a" by(simp add:Sup_def inf_absorb1 ACIfSL.fold1_belowI[OF ACIfSL_sup]) - -lemma (in ACIf) hom_fold1_commute: -assumes hom: "!!x y. h(f x y) = f (h x) (h y)" -and N: "finite N" "N \ {}" shows "h(fold1 f N) = fold1 f (h ` N)" -using N proof (induct rule: finite_ne_induct) - case singleton thus ?case by simp -next - case (insert n N) - have "h(fold1 f (insert n N)) = h(f n (fold1 f N))" using insert by(simp) - also have "\ = f (h n) (h(fold1 f N))" by(rule hom) - also have "h(fold1 f N) = fold1 f (h ` N)" by(rule insert) - also have "f (h n) \ = fold1 f (insert (h n) (h ` N))" - using insert by(simp) - also have "insert (h n) (h ` N) = h ` insert n N" by simp - finally show ?case . -qed - lemma (in Distrib_Lattice) sup_Inf1_distrib: "finite A \ A \ {} \ (x \ \A) = \{x \ a|a. a \ A}" apply(simp add:Inf_def image_def @@ -2277,7 +2322,7 @@ using A proof (induct rule: finite_ne_induct) case singleton thus ?case - by(simp add: sup_Inf1_distrib[OF B] fold1_singleton_def[OF Inf_def]) + by (simp add: sup_Inf1_distrib[OF B] fold1_singleton_def[OF Inf_def]) next case (insert x A) have finB: "finite {x \ b |b. b \ B}" @@ -2290,7 +2335,9 @@ qed have ne: "{a \ b |a b. a \ A \ b \ B} \ {}" using insert B by blast have "\(insert x A) \ \B = (x \ \A) \ \B" - using insert by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def]) + using insert + thm ACIf.fold1_insert_idem_def + by(simp add:ACIf.fold1_insert_idem_def[OF ACIf_inf Inf_def]) also have "\ = (x \ \B) \ (\A \ \B)" by(rule sup_inf_distrib2) also have "\ = \{x \ b|b. b \ B} \ \{a \ b|a b. a \ A \ b \ B}" using insert by(simp add:sup_Inf1_distrib[OF B]) @@ -2344,191 +2391,257 @@ finally show ?case . qed - -subsection{*Min and Max*} - -text{* As an application of @{text fold1} we define the minimal and -maximal element of a (non-empty) set over a linear order. *} - -constdefs - Min :: "('a::linorder)set => 'a" - "Min == fold1 min" - - Max :: "('a::linorder)set => 'a" - "Max == fold1 max" - - -text{* Before we can do anything, we need to show that @{text min} and -@{text max} are ACI and the ordering is linear: *} - -interpretation min: ACf ["min:: 'a::linorder \ 'a \ 'a"] -apply(rule ACf.intro) -apply(auto simp:min_def) -done - -interpretation min: ACIf ["min:: 'a::linorder \ 'a \ 'a"] -apply unfold_locales -apply(auto simp:min_def) -done - -interpretation max: ACf ["max :: 'a::linorder \ 'a \ 'a"] -apply unfold_locales -apply(auto simp:max_def) -done - -interpretation max: ACIf ["max:: 'a::linorder \ 'a \ 'a"] -apply unfold_locales -apply(auto simp:max_def) -done - -interpretation min: - ACIfSL ["min:: 'a::linorder \ 'a \ 'a" "op \" "op <"] -apply(simp add:order_less_le) -apply unfold_locales -apply(auto simp:min_def) -done - -interpretation min: - ACIfSLlin ["min :: 'a::linorder \ 'a \ 'a" "op \" "op <"] -apply unfold_locales -apply(auto simp:min_def) -done - -interpretation max: - ACIfSL ["max :: 'a::linorder \ 'a \ 'a" "%x y. y\x" "%x y. y 'a \ 'a" "%x y. y\x" "%x y. y" "op <" "min :: 'a::linorder \ 'a \ 'a" "max" "Min" "Max"] -apply - -apply(rule Min_def) -apply(rule Max_def) -apply unfold_locales -done - - -interpretation min_max: - Distrib_Lattice ["op \" "op <" "min :: 'a::linorder \ 'a \ 'a" "max" "Min" "Max"] - by unfold_locales - - -text{* Now we instantiate the recursion equations and declare them -simplification rules: *} - -(* Making Min or Max a defined parameter of a locale, suitably - extending ACIf, could make the following interpretations more automatic. *) - -lemmas Min_singleton = fold1_singleton_def [OF Min_def] -lemmas Max_singleton = fold1_singleton_def [OF Max_def] -lemmas Min_insert = min.fold1_insert_idem_def [OF Min_def] -lemmas Max_insert = max.fold1_insert_idem_def [OF Max_def] - -declare Min_singleton [simp] Max_singleton [simp] -declare Min_insert [simp] Max_insert [simp] - - -text{* Now we instantiate some @{text fold1} properties: *} +text {* + Infimum and supremum in complete lattices may also + be characterized by @{const fold1}: +*} + +lemma (in complete_lattice) Inf_fold1: + assumes fin: "finite A" + and nonempty: "A \ {}" + shows "\A = fold1 (op \) A" +using fin nonempty +by (induct A set: finite) + (simp_all add: Inf_insert_simp ACIf.fold1_insert_idem [OF ACIf_inf]) + +lemma (in complete_lattice) Sup_fold1: + assumes fin: "finite A" + and nonempty: "A \ {}" + shows "\A = fold1 (op \) A" +using fin nonempty +by (induct A set: finite) + (simp_all add: Sup_insert_simp ACIf.fold1_insert_idem [OF ACIf_sup]) + + +subsubsection {* Fold1 in linear orders with @{const min} and @{const max} *} + +text{* + As an application of @{text fold1} we define minimum + and maximum in (not necessarily complete!) linear orders + over (non-empty) sets by means of @{text fold1}. +*} + +locale Linorder = linorder -- {* we do not pollute the @{text linorder} clas *} +begin + +definition + Min :: "'a set \ 'a" +where + "Min = fold1 min" + +definition + Max :: "'a set \ 'a" +where + "Max = fold1 max" + +text {* recall: @{term min} and @{term max} behave like @{const inf} and @{const sup} *} + +lemma ACIf_min: "ACIf min" + by (rule lower_semilattice.ACIf_inf, + rule lattice_pred.axioms, + rule distrib_lattice_pred.axioms, + rule distrib_lattice_min_max) + +lemma ACf_min: "ACf min" + by (rule lower_semilattice.ACf_inf, + rule lattice_pred.axioms, + rule distrib_lattice_pred.axioms, + rule distrib_lattice_min_max) + +lemma ACIfSL_min: "ACIfSL (op \<^loc>\) (op \<^loc><) min" + by (rule lower_semilattice.ACIfSL_inf, + rule lattice_pred.axioms, + rule distrib_lattice_pred.axioms, + rule distrib_lattice_min_max) + +lemma ACIfSLlin_min: "ACIfSLlin (op \<^loc>\) (op \<^loc><) min" + by (rule ACIfSLlin.intro, + rule lower_semilattice.ACIfSL_inf, + rule lattice_pred.axioms, + rule distrib_lattice_pred.axioms, + rule distrib_lattice_min_max) + (unfold_locales, simp add: min_def) + +lemma ACIf_max: "ACIf max" + by (rule upper_semilattice.ACIf_sup, + rule lattice_pred.axioms, + rule distrib_lattice_pred.axioms, + rule distrib_lattice_min_max) + +lemma ACf_max: "ACf max" + by (rule upper_semilattice.ACf_sup, + rule lattice_pred.axioms, + rule distrib_lattice_pred.axioms, + rule distrib_lattice_min_max) + +lemma ACIfSL_max: "ACIfSL (\x y. y \<^loc>\ x) (\x y. y \<^loc>< x) max" + by (rule upper_semilattice.ACIfSL_sup, + rule lattice_pred.axioms, + rule distrib_lattice_pred.axioms, + rule distrib_lattice_min_max) + +lemma ACIfSLlin_max: "ACIfSLlin (\x y. y \<^loc>\ x) (\x y. y \<^loc>< x) max" + by (rule ACIfSLlin.intro, + rule upper_semilattice.ACIfSL_sup, + rule lattice_pred.axioms, + rule distrib_lattice_pred.axioms, + rule distrib_lattice_min_max) + (unfold_locales, simp add: max_def) + +lemmas Min_singleton [simp] = fold1_singleton_def [OF Min_def] +lemmas Max_singleton [simp] = fold1_singleton_def [OF Max_def] +lemmas Min_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_min Min_def] +lemmas Max_insert [simp] = ACIf.fold1_insert_idem_def [OF ACIf_max Max_def] lemma Min_in [simp]: shows "finite A \ A \ {} \ Min A \ A" -using min.fold1_in -by(fastsimp simp: Min_def min_def) + using ACf.fold1_in [OF ACf_min] + by (fastsimp simp: Min_def min_def) lemma Max_in [simp]: shows "finite A \ A \ {} \ Max A \ A" -using max.fold1_in -by(fastsimp simp: Max_def max_def) - -lemma Min_antimono: "\ M \ N; M \ {}; finite N \ \ Min N \ Min M" - by (simp add: Min_def min.fold1_antimono) - -lemma Max_mono: "\ M \ N; M \ {}; finite N \ \ Max M \ Max N" - by (simp add: Max_def max.fold1_antimono) - -lemma Min_le [simp]: "\ finite A; A \ {}; x \ A \ \ Min A \ x" -by(simp add: Min_def min.fold1_belowI) - -lemma Max_ge [simp]: "\ finite A; A \ {}; x \ A \ \ x \ Max A" -by(simp add: Max_def max.fold1_belowI) - -lemma Min_ge_iff[simp]: - "\ finite A; A \ {} \ \ (x \ Min A) = (\a\A. x \ a)" -by(simp add: Min_def min.below_fold1_iff) - -lemma Max_le_iff[simp]: - "\ finite A; A \ {} \ \ (Max A \ x) = (\a\A. a \ x)" -by(simp add: Max_def max.below_fold1_iff) - -lemma Min_gr_iff[simp]: - "\ finite A; A \ {} \ \ (x < Min A) = (\a\A. x < a)" -by(simp add: Min_def min.strict_below_fold1_iff) - -lemma Max_less_iff[simp]: - "\ finite A; A \ {} \ \ (Max A < x) = (\a\A. a < x)" -by(simp add: Max_def max.strict_below_fold1_iff) + using ACf.fold1_in [OF ACf_max] + by (fastsimp simp: Max_def max_def) + +lemma Min_antimono: "\ M \ N; M \ {}; finite N \ \ Min N \<^loc>\ Min M" + by (simp add: Min_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_min]) + +lemma Max_mono: "\ M \ N; M \ {}; finite N \ \ Max M \<^loc>\ Max N" + by (simp add: Max_def ACIfSLlin.fold1_antimono [OF ACIfSLlin_max]) + +lemma Min_le [simp]: "\ finite A; A \ {}; x \ A \ \ Min A \<^loc>\ x" + by (simp add: Min_def ACIfSL.fold1_belowI [OF ACIfSL_min]) + +lemma Max_ge [simp]: "\ finite A; A \ {}; x \ A \ \ x \<^loc>\ Max A" + by (simp add: Max_def ACIfSL.fold1_belowI [OF ACIfSL_max]) + +lemma Min_ge_iff [simp]: + "\ finite A; A \ {} \ \ x \<^loc>\ Min A \ (\a\A. x \<^loc>\ a)" + by (simp add: Min_def ACIfSL.below_fold1_iff [OF ACIfSL_min]) + +lemma Max_le_iff [simp]: + "\ finite A; A \ {} \ \ Max A \<^loc>\ x \ (\a\A. a \<^loc>\ x)" + by (simp add: Max_def ACIfSL.below_fold1_iff [OF ACIfSL_max]) + +lemma Min_gr_iff [simp]: + "\ finite A; A \ {} \ \ x \<^loc>< Min A \ (\a\A. x \<^loc>< a)" + by (simp add: Min_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_min]) + +lemma Max_less_iff [simp]: + "\ finite A; A \ {} \ \ Max A \<^loc>< x \ (\a\A. a \<^loc>< x)" + by (simp add: Max_def ACIfSLlin.strict_below_fold1_iff [OF ACIfSLlin_max]) lemma Min_le_iff: - "\ finite A; A \ {} \