tuning and augmentation of min/max lemmas;
more lemmas and simp rules for abstract lattices with order;
tuned proofs
(* Title: HOL/Lattices_Big.thy
Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
with contributions by Jeremy Avigad
*)
header {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *}
theory Lattices_Big
imports Finite_Set
begin
subsection {* Generic lattice operations over a set *}
no_notation times (infixl "*" 70)
no_notation Groups.one ("1")
subsubsection {* Without neutral element *}
locale semilattice_set = semilattice
begin
interpretation comp_fun_idem f
by default (simp_all add: fun_eq_iff left_commute)
definition F :: "'a set \<Rightarrow> 'a"
where
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)"
lemma eq_fold:
assumes "finite A"
shows "F (insert x A) = Finite_Set.fold f x A"
proof (rule sym)
let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
interpret comp_fun_idem "?f"
by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
from assms show "Finite_Set.fold f x A = F (insert x A)"
proof induct
case empty then show ?case by (simp add: eq_fold')
next
case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
qed
qed
lemma singleton [simp]:
"F {x} = x"
by (simp add: eq_fold)
lemma insert_not_elem:
assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
shows "F (insert x A) = x * F A"
proof -
from `A \<noteq> {}` obtain b where "b \<in> A" by blast
then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
with `finite A` and `x \<notin> A`
have "finite (insert x B)" and "b \<notin> insert x B" by auto
then have "F (insert b (insert x B)) = x * F (insert b B)"
by (simp add: eq_fold)
then show ?thesis by (simp add: * insert_commute)
qed
lemma in_idem:
assumes "finite A" and "x \<in> A"
shows "x * F A = F A"
proof -
from assms have "A \<noteq> {}" by auto
with `finite A` show ?thesis using `x \<in> A`
by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
qed
lemma insert [simp]:
assumes "finite A" and "A \<noteq> {}"
shows "F (insert x A) = x * F A"
using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
lemma union:
assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
shows "F (A \<union> B) = F A * F B"
using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
lemma remove:
assumes "finite A" and "x \<in> A"
shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
proof -
from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
with assms show ?thesis by simp
qed
lemma insert_remove:
assumes "finite A"
shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
lemma subset:
assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
shows "F B * F A = F A"
proof -
from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
qed
lemma closed:
assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
shows "F A \<in> A"
using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
case singleton then show ?case by simp
next
case insert with elem show ?case by force
qed
lemma hom_commute:
assumes hom: "\<And>x y. h (x * y) = h x * h y"
and N: "finite N" "N \<noteq> {}"
shows "h (F N) = 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 (F (insert n N)) = h (n * F N)" by simp
also have "\<dots> = h n * h (F N)" by (rule hom)
also have "h (F N) = F (h ` N)" by (rule insert)
also have "h n * \<dots> = 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
end
locale semilattice_order_set = binary?: semilattice_order + semilattice_set
begin
lemma bounded_iff:
assumes "finite A" and "A \<noteq> {}"
shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
lemma boundedI:
assumes "finite A"
assumes "A \<noteq> {}"
assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
shows "x \<preceq> F A"
using assms by (simp add: bounded_iff)
lemma boundedE:
assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
using assms by (simp add: bounded_iff)
lemma coboundedI:
assumes "finite A"
and "a \<in> A"
shows "F A \<preceq> a"
proof -
from assms have "A \<noteq> {}" by auto
from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
proof (induct rule: finite_ne_induct)
case singleton thus ?case by (simp add: refl)
next
case (insert x B)
from insert have "a = x \<or> a \<in> B" by simp
then show ?case using insert by (auto intro: coboundedI2)
qed
qed
lemma antimono:
assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
shows "F B \<preceq> F A"
proof (cases "A = B")
case True then show ?thesis by (simp add: refl)
next
case False
have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
then have "F B = F (A \<union> (B - A))" by simp
also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
also have "\<dots> \<preceq> F A" by simp
finally show ?thesis .
qed
end
subsubsection {* With neutral element *}
locale semilattice_neutr_set = semilattice_neutr
begin
interpretation comp_fun_idem f
by default (simp_all add: fun_eq_iff left_commute)
definition F :: "'a set \<Rightarrow> 'a"
where
eq_fold: "F A = Finite_Set.fold f 1 A"
lemma infinite [simp]:
"\<not> finite A \<Longrightarrow> F A = 1"
by (simp add: eq_fold)
lemma empty [simp]:
"F {} = 1"
by (simp add: eq_fold)
lemma insert [simp]:
assumes "finite A"
shows "F (insert x A) = x * F A"
using assms by (simp add: eq_fold)
lemma in_idem:
assumes "finite A" and "x \<in> A"
shows "x * F A = F A"
proof -
from assms have "A \<noteq> {}" by auto
with `finite A` show ?thesis using `x \<in> A`
by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
qed
lemma union:
assumes "finite A" and "finite B"
shows "F (A \<union> B) = F A * F B"
using assms by (induct A) (simp_all add: ac_simps)
lemma remove:
assumes "finite A" and "x \<in> A"
shows "F A = x * F (A - {x})"
proof -
from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
with assms show ?thesis by simp
qed
lemma insert_remove:
assumes "finite A"
shows "F (insert x A) = x * F (A - {x})"
using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
lemma subset:
assumes "finite A" and "B \<subseteq> A"
shows "F B * F A = F A"
proof -
from assms have "finite B" by (auto dest: finite_subset)
with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
qed
lemma closed:
assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
shows "F A \<in> A"
using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
case singleton then show ?case by simp
next
case insert with elem show ?case by force
qed
end
locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set
begin
lemma bounded_iff:
assumes "finite A"
shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
using assms by (induct A) (simp_all add: bounded_iff)
lemma boundedI:
assumes "finite A"
assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
shows "x \<preceq> F A"
using assms by (simp add: bounded_iff)
lemma boundedE:
assumes "finite A" and "x \<preceq> F A"
obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
using assms by (simp add: bounded_iff)
lemma coboundedI:
assumes "finite A"
and "a \<in> A"
shows "F A \<preceq> a"
proof -
from assms have "A \<noteq> {}" by auto
from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
proof (induct rule: finite_ne_induct)
case singleton thus ?case by (simp add: refl)
next
case (insert x B)
from insert have "a = x \<or> a \<in> B" by simp
then show ?case using insert by (auto intro: coboundedI2)
qed
qed
lemma antimono:
assumes "A \<subseteq> B" and "finite B"
shows "F B \<preceq> F A"
proof (cases "A = B")
case True then show ?thesis by (simp add: refl)
next
case False
have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
then have "F B = F (A \<union> (B - A))" by simp
also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
also have "\<dots> \<preceq> F A" by simp
finally show ?thesis .
qed
end
notation times (infixl "*" 70)
notation Groups.one ("1")
subsection {* Lattice operations on finite sets *}
text {*
For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
to @{class linorder}. This is badly designed: both should depend on a common abstract
distributive lattice rather than having this non-subclass dependecy between two
classes. But for the moment we have to live with it. This forces us to setup
this sublocale dependency simultaneously with the lattice operations on finite
sets, to avoid garbage.
*}
definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
where
"Inf_fin = semilattice_set.F inf"
definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
where
"Sup_fin = semilattice_set.F sup"
context linorder
begin
definition Min :: "'a set \<Rightarrow> 'a"
where
"Min = semilattice_set.F min"
definition Max :: "'a set \<Rightarrow> 'a"
where
"Max = semilattice_set.F max"
sublocale Min!: semilattice_order_set min less_eq less
+ Max!: semilattice_order_set max greater_eq greater
where
"semilattice_set.F min = Min"
and "semilattice_set.F max = Max"
proof -
show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
then interpret Min!: semilattice_order_set min less_eq less .
show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
then interpret Max!: semilattice_order_set max greater_eq greater .
from Min_def show "semilattice_set.F min = Min" by rule
from Max_def show "semilattice_set.F max = Max" by rule
qed
text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
sublocale min_max!: distrib_lattice min less_eq less max
where
"semilattice_inf.Inf_fin min = Min"
and "semilattice_sup.Sup_fin max = Max"
proof -
show "class.distrib_lattice min less_eq less max"
proof
fix x y z
show "max x (min y z) = min (max x y) (max x z)"
by (auto simp add: min_def max_def)
qed (auto simp add: min_def max_def not_le less_imp_le)
then interpret min_max!: distrib_lattice min less_eq less max .
show "semilattice_inf.Inf_fin min = Min"
by (simp only: min_max.Inf_fin_def Min_def)
show "semilattice_sup.Sup_fin max = Max"
by (simp only: min_max.Sup_fin_def Max_def)
qed
lemmas le_maxI1 = min_max.sup_ge1
lemmas le_maxI2 = min_max.sup_ge2
lemmas min_ac = min.assoc min_max.inf_commute min.left_commute
lemmas max_ac = min_max.sup_assoc min_max.sup_commute max.left_commute
end
text {* Lattice operations proper *}
sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
where
"semilattice_set.F inf = Inf_fin"
proof -
show "semilattice_order_set inf less_eq less" ..
then interpret Inf_fin!: semilattice_order_set inf less_eq less .
from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
qed
sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
where
"semilattice_set.F sup = Sup_fin"
proof -
show "semilattice_order_set sup greater_eq greater" ..
then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
qed
text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
lemma Inf_fin_Min:
"Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
by (simp add: Inf_fin_def Min_def inf_min)
lemma Sup_fin_Max:
"Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
by (simp add: Sup_fin_def Max_def sup_max)
subsection {* Infimum and Supremum over non-empty sets *}
text {*
After this non-regular bootstrap, things continue canonically.
*}
context lattice
begin
lemma Inf_fin_le_Sup_fin [simp]:
assumes "finite A" and "A \<noteq> {}"
shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
proof -
from `A \<noteq> {}` obtain a where "a \<in> A" by blast
with `finite A` have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
moreover from `finite A` `a \<in> A` have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
ultimately show ?thesis by (rule order_trans)
qed
lemma sup_Inf_absorb [simp]:
"finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a"
by (rule sup_absorb2) (rule Inf_fin.coboundedI)
lemma inf_Sup_absorb [simp]:
"finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a"
by (rule inf_absorb1) (rule Sup_fin.coboundedI)
end
context distrib_lattice
begin
lemma sup_Inf1_distrib:
assumes "finite A"
and "A \<noteq> {}"
shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
(rule arg_cong [where f="Inf_fin"], blast)
lemma sup_Inf2_distrib:
assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
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 b|a b. a \<in> A \<and> b \<in> B}"
using A proof (induct rule: finite_ne_induct)
case singleton then show ?case
by (simp add: sup_Inf1_distrib [OF B])
next
case (insert x A)
have finB: "finite {sup x b |b. b \<in> B}"
by (rule finite_surj [where f = "sup x", OF B(1)], auto)
have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
proof -
have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
by blast
thus ?thesis by(simp add: insert(1) B(1))
qed
have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
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)"
using insert by simp
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)
also have "\<dots> = inf (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x b|b. b \<in> B}) (\<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \<in> A \<and> b \<in> B})"
using insert by(simp add:sup_Inf1_distrib[OF B])
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})"
(is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
using B insert
by (simp add: Inf_fin.union [OF finB _ finAB ne])
also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
by blast
finally show ?case .
qed
lemma inf_Sup1_distrib:
assumes "finite A" and "A \<noteq> {}"
shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
(rule arg_cong [where f="Sup_fin"], blast)
lemma inf_Sup2_distrib:
assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
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 b|a b. a \<in> A \<and> b \<in> B}"
using A proof (induct rule: finite_ne_induct)
case singleton thus ?case
by(simp add: inf_Sup1_distrib [OF B])
next
case (insert x A)
have finB: "finite {inf x b |b. b \<in> B}"
by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
proof -
have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
by blast
thus ?thesis by(simp add: insert(1) B(1))
qed
have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
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)"
using insert by simp
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)
also have "\<dots> = sup (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x b|b. b \<in> B}) (\<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \<in> A \<and> b \<in> B})"
using insert by(simp add:inf_Sup1_distrib[OF B])
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})"
(is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
using B insert
by (simp add: Sup_fin.union [OF finB _ finAB ne])
also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
by blast
finally show ?case .
qed
end
context complete_lattice
begin
lemma Inf_fin_Inf:
assumes "finite A" and "A \<noteq> {}"
shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
proof -
from assms obtain b B where "A = insert b B" and "finite B" by auto
then show ?thesis
by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
qed
lemma Sup_fin_Sup:
assumes "finite A" and "A \<noteq> {}"
shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
proof -
from assms obtain b B where "A = insert b B" and "finite B" by auto
then show ?thesis
by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
qed
end
subsection {* Minimum and Maximum over non-empty sets *}
context linorder
begin
lemma dual_min:
"ord.min greater_eq = max"
by (auto simp add: ord.min_def max_def fun_eq_iff)
lemma dual_max:
"ord.max greater_eq = min"
by (auto simp add: ord.max_def min_def fun_eq_iff)
lemma dual_Min:
"linorder.Min greater_eq = Max"
proof -
interpret dual!: linorder greater_eq greater by (fact dual_linorder)
show ?thesis by (simp add: dual.Min_def dual_min Max_def)
qed
lemma dual_Max:
"linorder.Max greater_eq = Min"
proof -
interpret dual!: linorder greater_eq greater by (fact dual_linorder)
show ?thesis by (simp add: dual.Max_def dual_max Min_def)
qed
lemmas Min_singleton = Min.singleton
lemmas Max_singleton = Max.singleton
lemmas Min_insert = Min.insert
lemmas Max_insert = Max.insert
lemmas Min_Un = Min.union
lemmas Max_Un = Max.union
lemmas hom_Min_commute = Min.hom_commute
lemmas hom_Max_commute = Max.hom_commute
lemma Min_in [simp]:
assumes "finite A" and "A \<noteq> {}"
shows "Min A \<in> A"
using assms by (auto simp add: min_def Min.closed)
lemma Max_in [simp]:
assumes "finite A" and "A \<noteq> {}"
shows "Max A \<in> A"
using assms by (auto simp add: max_def Max.closed)
lemma Min_le [simp]:
assumes "finite A" and "x \<in> A"
shows "Min A \<le> x"
using assms by (fact Min.coboundedI)
lemma Max_ge [simp]:
assumes "finite A" and "x \<in> A"
shows "x \<le> Max A"
using assms by (fact Max.coboundedI)
lemma Min_eqI:
assumes "finite A"
assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
and "x \<in> A"
shows "Min A = x"
proof (rule antisym)
from `x \<in> A` have "A \<noteq> {}" by auto
with assms show "Min A \<ge> x" by simp
next
from assms show "x \<ge> Min A" by simp
qed
lemma Max_eqI:
assumes "finite A"
assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
and "x \<in> A"
shows "Max A = x"
proof (rule antisym)
from `x \<in> A` have "A \<noteq> {}" by auto
with assms show "Max A \<le> x" by simp
next
from assms show "x \<le> Max A" by simp
qed
context
fixes A :: "'a set"
assumes fin_nonempty: "finite A" "A \<noteq> {}"
begin
lemma Min_ge_iff [simp]:
"x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
using fin_nonempty by (fact Min.bounded_iff)
lemma Max_le_iff [simp]:
"Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
using fin_nonempty by (fact Max.bounded_iff)
lemma Min_gr_iff [simp]:
"x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
using fin_nonempty by (induct rule: finite_ne_induct) simp_all
lemma Max_less_iff [simp]:
"Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
using fin_nonempty by (induct rule: finite_ne_induct) simp_all
lemma Min_le_iff:
"Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
lemma Max_ge_iff:
"x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
lemma Min_less_iff:
"Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
lemma Max_gr_iff:
"x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
end
lemma Min_antimono:
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
shows "Min N \<le> Min M"
using assms by (fact Min.antimono)
lemma Max_mono:
assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
shows "Max M \<le> Max N"
using assms by (fact Max.antimono)
lemma mono_Min_commute:
assumes "mono f"
assumes "finite A" and "A \<noteq> {}"
shows "f (Min A) = Min (f ` A)"
proof (rule linorder_class.Min_eqI [symmetric])
from `finite A` show "finite (f ` A)" by simp
from assms show "f (Min A) \<in> f ` A" by simp
fix x
assume "x \<in> f ` A"
then obtain y where "y \<in> A" and "x = f y" ..
with assms have "Min A \<le> y" by auto
with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
with `x = f y` show "f (Min A) \<le> x" by simp
qed
lemma mono_Max_commute:
assumes "mono f"
assumes "finite A" and "A \<noteq> {}"
shows "f (Max A) = Max (f ` A)"
proof (rule linorder_class.Max_eqI [symmetric])
from `finite A` show "finite (f ` A)" by simp
from assms show "f (Max A) \<in> f ` A" by simp
fix x
assume "x \<in> f ` A"
then obtain y where "y \<in> A" and "x = f y" ..
with assms have "y \<le> Max A" by auto
with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
with `x = f y` show "x \<le> f (Max A)" by simp
qed
lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
assumes fin: "finite A"
and empty: "P {}"
and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
shows "P A"
using fin empty insert
proof (induct rule: finite_psubset_induct)
case (psubset A)
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
have fin: "finite A" by fact
have empty: "P {}" by fact
have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
show "P A"
proof (cases "A = {}")
assume "A = {}"
then show "P A" using `P {}` by simp
next
let ?B = "A - {Max A}"
let ?A = "insert (Max A) ?B"
have "finite ?B" using `finite A` by simp
assume "A \<noteq> {}"
with `finite A` have "Max A : A" by auto
then have A: "?A = A" using insert_Diff_single insert_absorb by auto
then have "P ?B" using `P {}` step IH [of ?B] by blast
moreover
have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
qed
qed
lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
"\<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"
by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
lemma Least_Min:
assumes "finite {a. P a}" and "\<exists>a. P a"
shows "(LEAST a. P a) = Min {a. P a}"
proof -
{ fix A :: "'a set"
assume A: "finite A" "A \<noteq> {}"
have "(LEAST a. a \<in> A) = Min A"
using A proof (induct A rule: finite_ne_induct)
case singleton show ?case by (rule Least_equality) simp_all
next
case (insert a A)
have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
with insert show ?case by simp
qed
} from this [of "{a. P a}"] assms show ?thesis by simp
qed
end
context linordered_ab_semigroup_add
begin
lemma add_Min_commute:
fixes k
assumes "finite N" and "N \<noteq> {}"
shows "k + Min N = Min {k + m | m. m \<in> N}"
proof -
have "\<And>x y. k + min x y = min (k + x) (k + y)"
by (simp add: min_def not_le)
(blast intro: antisym less_imp_le add_left_mono)
with assms show ?thesis
using hom_Min_commute [of "plus k" N]
by simp (blast intro: arg_cong [where f = Min])
qed
lemma add_Max_commute:
fixes k
assumes "finite N" and "N \<noteq> {}"
shows "k + Max N = Max {k + m | m. m \<in> N}"
proof -
have "\<And>x y. k + max x y = max (k + x) (k + y)"
by (simp add: max_def not_le)
(blast intro: antisym less_imp_le add_left_mono)
with assms show ?thesis
using hom_Max_commute [of "plus k" N]
by simp (blast intro: arg_cong [where f = Max])
qed
end
context linordered_ab_group_add
begin
lemma minus_Max_eq_Min [simp]:
"finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
lemma minus_Min_eq_Max [simp]:
"finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
end
context complete_linorder
begin
lemma Min_Inf:
assumes "finite A" and "A \<noteq> {}"
shows "Min A = Inf A"
proof -
from assms obtain b B where "A = insert b B" and "finite B" by auto
then show ?thesis
by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
qed
lemma Max_Sup:
assumes "finite A" and "A \<noteq> {}"
shows "Max A = Sup A"
proof -
from assms obtain b B where "A = insert b B" and "finite B" by auto
then show ?thesis
by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
qed
end
end