Quelle Lattices_Big.thy Sprache: Isabelle

(*  Title:      HOL/Lattices_Big.thy
    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
                with contributions by Jeremy Avigad
*)

section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close>

theory Lattices_Big
  imports Groups_Big Option
begin

subsection \<open>Generic lattice operations over a set\<close>

subsubsection \<open>Without neutral element\<close>

locale semilattice_set = semilattice
begin

interpretation comp_fun_idem f
  by standard (simp_all add: fun_eq_iff left_commute)

definition F :: "'a set \ 'a"
where
  eq_fold': "F A = the (Finite_Set.fold (\x y. Some (case y of None \ x | Some z \ 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 = "\x y. Some (case y of None \ x | Some z \ f x z)"
  interpret comp_fun_idem "?f"
    by standard (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 \ A" and "A \ {}"
  shows "F (insert x A) = x \<^bold>* F A"
proof -
  from \<open>A \<noteq> {}\<close> obtain b where "b \<in> A" by blast
  then obtain B where *: "A = insert b B" "b \ B" by (blast dest: mk_disjoint_insert)
  with \<open>finite A\<close> and \<open>x \<notin> A\<close>
    have "finite (insert x B)" and "b \ insert x B" by auto
  then have "F (insert b (insert x B)) = x \<^bold>* 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 \ A"
  shows "x \<^bold>* F A = F A"
proof -
  from assms have "A \ {}" by auto
  with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
qed

lemma insert [simp]:
  assumes "finite A" and "A \ {}"
  shows "F (insert x A) = x \<^bold>* F A"
  using assms by (cases "x \ A") (simp_all add: insert_absorb in_idem insert_not_elem)

lemma union:
  assumes "finite A" "A \ {}" and "finite B" "B \ {}"
  shows "F (A \ B) = F A \<^bold>* F B"
  using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)

lemma remove:
  assumes "finite A" and "x \ A"
  shows "F A = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))"
proof -
  from assms obtain B where "A = insert x B" and "x \ 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 \<^bold>* F (A - {x}))"
  using assms by (cases "x \ A") (simp_all add: insert_absorb remove)

lemma subset:
  assumes "finite A" "B \ {}" and "B \ A"
  shows "F B \<^bold>* F A = F A"
proof -
  from assms have "A \ {}" 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 \ {}" and elem: "\x y. x \<^bold>* y \ {x, y}"
  shows "F A \ A"
using \<open>finite A\<close> \<open>A \<noteq> {}\<close> 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: "\x y. h (x \<^bold>* y) = h x \<^bold>* h y"
  and N: "finite N" "N \ {}"
  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 \<^bold>* F N)" by simp
  also have "\ = h n \<^bold>* h (F N)" by (rule hom)
  also have "h (F N) = F (h ` N)" by (rule insert)
  also have "h n \<^bold>* \ = 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 infinite: "\ finite A \ F A = the None"
  unfolding eq_fold' by (cases "finite (UNIV::'a set)") (auto intro: finite_subset fold_infinite)

end

locale semilattice_order_set = binary?: semilattice_order + semilattice_set
begin

lemma bounded_iff:
  assumes "finite A" and "A \ {}"
  shows "x \<^bold>\ F A \ (\a\A. x \<^bold>\ a)"
  using assms by (induct rule: finite_ne_induct) simp_all

lemma boundedI:
  assumes "finite A"
  assumes "A \ {}"
  assumes "\a. a \ A \ x \<^bold>\ a"
  shows "x \<^bold>\ F A"
  using assms by (simp add: bounded_iff)

lemma boundedE:
  assumes "finite A" and "A \ {}" and "x \<^bold>\ F A"
  obtains "\a. a \ A \ x \<^bold>\ a"
  using assms by (simp add: bounded_iff)

lemma coboundedI:
  assumes "finite A"
    and "a \ A"
  shows "F A \<^bold>\ a"
proof -
  from assms have "A \ {}" by auto
  from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> 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 \ a \ B" by simp
    then show ?case using insert by (auto intro: coboundedI2)
  qed
qed

lemma subset_imp:
  assumes "A \ B" and "A \ {}" and "finite B"
  shows "F B \<^bold>\ F A"
proof (cases "A = B")
  case True then show ?thesis by (simp add: refl)
next
  case False
  have B: "B = A \ (B - A)" using \A \ B\ by blast
  then have "F B = F (A \ (B - A))" by simp
  also have "\ = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
  also have "\ \<^bold>\ F A" by simp
  finally show ?thesis .
qed

end

subsubsection \<open>With neutral element\<close>

locale semilattice_neutr_set = semilattice_neutr
begin

interpretation comp_fun_idem f
  by standard (simp_all add: fun_eq_iff left_commute)

definition F :: "'a set \ 'a"
where
  eq_fold: "F A = Finite_Set.fold f \<^bold>1 A"

lemma infinite [simp]:
  "\ finite A \ F A = \<^bold>1"
  by (simp add: eq_fold)

lemma empty [simp]:
  "F {} = \<^bold>1"
  by (simp add: eq_fold)

lemma insert [simp]:
  assumes "finite A"
  shows "F (insert x A) = x \<^bold>* F A"
  using assms by (simp add: eq_fold)

lemma in_idem:
  assumes "finite A" and "x \ A"
  shows "x \<^bold>* F A = F A"
proof -
  from assms have "A \ {}" by auto
  with \<open>finite A\<close> show ?thesis using \<open>x \<in> A\<close>
    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
qed

lemma union:
  assumes "finite A" and "finite B"
  shows "F (A \ B) = F A \<^bold>* F B"
  using assms by (induct A) (simp_all add: ac_simps)

lemma remove:
  assumes "finite A" and "x \ A"
  shows "F A = x \<^bold>* F (A - {x})"
proof -
  from assms obtain B where "A = insert x B" and "x \ 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 \<^bold>* F (A - {x})"
  using assms by (cases "x \ A") (simp_all add: insert_absorb remove)

lemma subset:
  assumes "finite A" and "B \ A"
  shows "F B \<^bold>* 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 \ {}" and elem: "\x y. x \<^bold>* y \ {x, y}"
  shows "F A \ A"
using \<open>finite A\<close> \<open>A \<noteq> {}\<close> 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 \<^bold>\ F A \ (\a\A. x \<^bold>\ a)"
  using assms by (induct A) simp_all

lemma boundedI:
  assumes "finite A"
  assumes "\a. a \ A \ x \<^bold>\ a"
  shows "x \<^bold>\ F A"
  using assms by (simp add: bounded_iff)

lemma boundedE:
  assumes "finite A" and "x \<^bold>\ F A"
  obtains "\a. a \ A \ x \<^bold>\ a"
  using assms by (simp add: bounded_iff)

lemma coboundedI:
  assumes "finite A"
    and "a \ A"
  shows "F A \<^bold>\ a"
proof -
  from assms have "A \ {}" by auto
  from \<open>finite A\<close> \<open>A \<noteq> {}\<close> \<open>a \<in> A\<close> 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 \ a \ B" by simp
    then show ?case using insert by (auto intro: coboundedI2)
  qed
qed

lemma subset_imp:
  assumes "A \ B" and "finite B"
  shows "F B \<^bold>\ F A"
proof (cases "A = B")
  case True then show ?thesis by (simp add: refl)
next
  case False
  have B: "B = A \ (B - A)" using \A \ B\ by blast
  then have "F B = F (A \ (B - A))" by simp
  also have "\ = F A \<^bold>* F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
  also have "\ \<^bold>\ F A" by simp
  finally show ?thesis .
qed

end

subsection \<open>Lattice operations on finite sets\<close>

context semilattice_inf
begin

sublocale Inf_fin: semilattice_order_set inf less_eq less
defines
  Inf_fin (\<open>\<Sqinter>\<^sub>f\<^sub>i\<^sub>n _\<close> [900] 900) = Inf_fin.F ..

end

context semilattice_sup
begin

sublocale Sup_fin: semilattice_order_set sup greater_eq greater
defines
  Sup_fin (\<open>\<Squnion>\<^sub>f\<^sub>i\<^sub>n _\<close> [900] 900) = Sup_fin.F ..

end

subsection \<open>Infimum and Supremum over non-empty sets\<close>

context lattice
begin

lemma Inf_fin_le_Sup_fin [simp]:
  assumes "finite A" and "A \ {}"
  shows "\\<^sub>f\<^sub>i\<^sub>nA \ \\<^sub>f\<^sub>i\<^sub>nA"
proof -
  from \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" by blast
  with \<open>finite A\<close> have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
  moreover from \<open>finite A\<close> \<open>a \<in> A\<close> 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 \ a \ A \ \\<^sub>f\<^sub>i\<^sub>nA \ a = a"
  by (rule sup_absorb2) (rule Inf_fin.coboundedI)

lemma inf_Sup_absorb [simp]:
  "finite A \ a \ A \ a \ \\<^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 \ {}"
  shows "sup x (\\<^sub>f\<^sub>i\<^sub>nA) = \\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \ 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 \ {}" and B: "finite B" "B \ {}"
  shows "sup (\\<^sub>f\<^sub>i\<^sub>nA) (\\<^sub>f\<^sub>i\<^sub>nB) = \\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \ A \ b \ 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 \ B}"
    by (rule finite_surj [where f = "sup x", OF B(1)], auto)
  have finAB: "finite {sup a b |a b. a \ A \ b \ B}"
  proof -
    have "{sup a b |a b. a \ A \ b \ B} = (\a\A. \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 \ A \ b \ B} \ {}" using insert B by blast
  have "sup (\\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\\<^sub>f\<^sub>i\<^sub>nB) = sup (inf x (\\<^sub>f\<^sub>i\<^sub>nA)) (\\<^sub>f\<^sub>i\<^sub>nB)"
    using insert by simp
  also have "\ = inf (sup x (\\<^sub>f\<^sub>i\<^sub>nB)) (sup (\\<^sub>f\<^sub>i\<^sub>nA) (\\<^sub>f\<^sub>i\<^sub>nB))" by(rule sup_inf_distrib2)
  also have "\ = inf (\\<^sub>f\<^sub>i\<^sub>n{sup x b|b. b \ B}) (\\<^sub>f\<^sub>i\<^sub>n{sup a b|a b. a \ A \ b \ B})"
    using insert by(simp add:sup_Inf1_distrib[OF B])
  also have "\ = \\<^sub>f\<^sub>i\<^sub>n({sup x b |b. b \ B} \ {sup a b |a b. a \ A \ b \ B})"
    (is "_ = \\<^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 \ insert x A \ b \ B}"
    by blast
  finally show ?case .
qed

lemma inf_Sup1_distrib:
  assumes "finite A" and "A \ {}"
  shows "inf x (\\<^sub>f\<^sub>i\<^sub>nA) = \\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \ 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 \ {}" and B: "finite B" "B \ {}"
  shows "inf (\\<^sub>f\<^sub>i\<^sub>nA) (\\<^sub>f\<^sub>i\<^sub>nB) = \\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \ A \ b \ 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 \ B}"
    by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
  have finAB: "finite {inf a b |a b. a \ A \ b \ B}"
  proof -
    have "{inf a b |a b. a \ A \ b \ B} = (\a\A. \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 \ A \ b \ B} \ {}" using insert B by blast
  have "inf (\\<^sub>f\<^sub>i\<^sub>n(insert x A)) (\\<^sub>f\<^sub>i\<^sub>nB) = inf (sup x (\\<^sub>f\<^sub>i\<^sub>nA)) (\\<^sub>f\<^sub>i\<^sub>nB)"
    using insert by simp
  also have "\ = sup (inf x (\\<^sub>f\<^sub>i\<^sub>nB)) (inf (\\<^sub>f\<^sub>i\<^sub>nA) (\\<^sub>f\<^sub>i\<^sub>nB))" by(rule inf_sup_distrib2)
  also have "\ = sup (\\<^sub>f\<^sub>i\<^sub>n{inf x b|b. b \ B}) (\\<^sub>f\<^sub>i\<^sub>n{inf a b|a b. a \ A \ b \ B})"
    using insert by(simp add:inf_Sup1_distrib[OF B])
  also have "\ = \\<^sub>f\<^sub>i\<^sub>n({inf x b |b. b \ B} \ {inf a b |a b. a \ A \ b \ B})"
    (is "_ = \\<^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 \ insert x A \ b \ B}"
    by blast
  finally show ?case .
qed

end

context complete_lattice
begin

lemma Inf_fin_Inf:
  assumes "finite A" and "A \ {}"
  shows "\\<^sub>f\<^sub>i\<^sub>nA = \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 \ {}"
  shows "\\<^sub>f\<^sub>i\<^sub>nA = \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 \<open>Minimum and Maximum over non-empty sets\<close>

context linorder
begin

sublocale Min: semilattice_order_set min less_eq less
  + Max: semilattice_order_set max greater_eq greater
defines
  Min = Min.F and Max = Max.F ..

end

syntax
  "_MIN1"     :: "pttrns \ 'b \ 'b" (\(\indent=3 notation=\binder MIN\\MIN _./ _)\ [0, 10] 10)
  "_MIN"      :: "pttrn \ 'a set \ 'b \ 'b" (\(\indent=3 notation=\binder MIN\\MIN _\_./ _)\ [0, 0, 10] 10)
  "_MAX1"     :: "pttrns \ 'b \ 'b" (\(\indent=3 notation=\binder MAX\\MAX _./ _)\ [0, 10] 10)
  "_MAX"      :: "pttrn \ 'a set \ 'b \ 'b" (\(\indent=3 notation=\binder MAX\\MAX _\_./ _)\ [0, 0, 10] 10)

syntax_consts
  "_MIN1" "_MIN" \<rightleftharpoons> Min and
  "_MAX1" "_MAX" \<rightleftharpoons> Max

translations
  "MIN x y. f"   \<rightleftharpoons> "MIN x. MIN y. f"
  "MIN x. f"     \<rightleftharpoons> "CONST Min (CONST range (\<lambda>x. f))"
  "MIN x\A. f" \ "CONST Min ((\x. f) ` A)"
  "MAX x y. f"   \<rightleftharpoons> "MAX x. MAX y. f"
  "MAX x. f"     \<rightleftharpoons> "CONST Max (CONST range (\<lambda>x. f))"
  "MAX x\A. f" \ "CONST Max ((\x. f) ` A)"

text \<open>An aside: \<^const>\<open>Min\<close>/\<^const>\<open>Max\<close> on linear orders as special case of \<^const>\<open>Inf_fin\<close>/\<^const>\<open>Sup_fin\<close>\<close>

lemma Inf_fin_Min:
  "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \ 'a)"
  by (simp add: Inf_fin_def Min_def inf_min)

lemma Sup_fin_Max:
  "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \ 'a)"
  by (simp add: Sup_fin_def Max_def sup_max)

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 \ {}"
  shows "Min A \ A"
  using assms by (auto simp add: min_def Min.closed)

lemma Max_in [simp]:
  assumes "finite A" and "A \ {}"
  shows "Max A \ A"
  using assms by (auto simp add: max_def Max.closed)

lemma Min_insert2:
  assumes "finite A" and min: "\b. b \ A \ a \ b"
  shows "Min (insert a A) = a"
proof (cases "A = {}")
  case True
  then show ?thesis by simp
next
  case False
  with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
    by simp
  moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp
  ultimately show ?thesis by (simp add: min.absorb1)
qed

lemma Max_insert2:
  assumes "finite A" and max: "\b. b \ A \ b \ a"
  shows "Max (insert a A) = a"
proof (cases "A = {}")
  case True
  then show ?thesis by simp
next
  case False
  with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
    by simp
  moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp
  ultimately show ?thesis by (simp add: max.absorb1)
qed

lemma Max_const[simp]: "\ finite A; A \ {} \ \ Max ((\_. c) ` A) = c"
using Max_in image_is_empty by blast

lemma Min_const[simp]: "\ finite A; A \ {} \ \ Min ((\_. c) ` A) = c"
using Min_in image_is_empty by blast

lemma Min_le [simp]:
  assumes "finite A" and "x \ A"
  shows "Min A \ x"
  using assms by (fact Min.coboundedI)

lemma Max_ge [simp]:
  assumes "finite A" and "x \ A"
  shows "x \ Max A"
  using assms by (fact Max.coboundedI)

lemma Min_eqI:
  assumes "finite A"
  assumes "\y. y \ A \ y \ x"
    and "x \ A"
  shows "Min A = x"
proof (rule order.antisym)
  from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
  with assms show "Min A \ x" by simp
next
  from assms show "x \ Min A" by simp
qed

lemma Max_eqI:
  assumes "finite A"
  assumes "\y. y \ A \ y \ x"
    and "x \ A"
  shows "Max A = x"
proof (rule order.antisym)
  from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
  with assms show "Max A \ x" by simp
next
  from assms show "x \ Max A" by simp
qed

lemma eq_Min_iff:
  "\ finite A; A \ {} \ \ m = Min A \ m \ A \ (\a \ A. m \ a)"
by (meson Min_in Min_le order.antisym)

lemma Min_eq_iff:
  "\ finite A; A \ {} \ \ Min A = m \ m \ A \ (\a \ A. m \ a)"
by (meson Min_in Min_le order.antisym)

lemma eq_Max_iff:
  "\ finite A; A \ {} \ \ m = Max A \ m \ A \ (\a \ A. a \ m)"
by (meson Max_in Max_ge order.antisym)

lemma Max_eq_iff:
  "\ finite A; A \ {} \ \ Max A = m \ m \ A \ (\a \ A. a \ m)"
by (meson Max_in Max_ge order.antisym)

context
  fixes A :: "'a set"
  assumes fin_nonempty: "finite A" "A \ {}"
begin

lemma Min_ge_iff [simp]:
  "x \ Min A \ (\a\A. x \ a)"
  using fin_nonempty by (fact Min.bounded_iff)

lemma Max_le_iff [simp]:
  "Max A \ x \ (\a\A. a \ x)"
  using fin_nonempty by (fact Max.bounded_iff)

lemma Min_gr_iff [simp]:
  "x < Min A \ (\a\A. x < a)"
  using fin_nonempty  by (induct rule: finite_ne_induct) simp_all

lemma Max_less_iff [simp]:
  "Max A < x \ (\a\A. a < x)"
  using fin_nonempty by (induct rule: finite_ne_induct) simp_all

lemma Min_le_iff:
  "Min A \ x \ (\a\A. a \ x)"
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)

lemma Max_ge_iff:
  "x \ Max A \ (\a\A. x \ a)"
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)

lemma Min_less_iff:
  "Min A < x \ (\a\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 \ (\a\A. x < a)"
  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)

end

text \<open>Handy results about @{term Max} and @{term Min} by Chelsea Edmonds\<close>
lemma obtains_Max:
  assumes "finite A" and "A \ {}"
  obtains x where "x \ A" and "Max A = x"
  using assms Max_in by blast

lemma obtains_MAX:
  assumes "finite A" and "A \ {}"
  obtains x where "x \ A" and "Max (f ` A) = f x"
  using obtains_Max
  by (metis (mono_tags, opaque_lifting) assms(1) assms(2) empty_is_image finite_imageI image_iff)

lemma obtains_Min:
  assumes "finite A" and "A \ {}"
  obtains x where "x \ A" and "Min A = x"
  using assms Min_in by blast

lemma obtains_MIN:
  assumes "finite A" and "A \ {}"
  obtains x where "x \ A" and "Min (f ` A) = f x"
  using obtains_Min assms empty_is_image finite_imageI image_iff
  by (metis (mono_tags, opaque_lifting))

lemma Max_eq_if:
  assumes "finite A"  "finite B"  "\a\A. \b\B. a \ b" "\b\B. \a\A. b \ a"
  shows "Max A = Max B"
proof cases
  assume "A = {}" thus ?thesis using assms by simp
next
  assume "A \ {}" thus ?thesis using assms
    by(blast intro: order.antisym Max_in Max_ge_iff[THEN iffD2])
qed

lemma Min_antimono:
  assumes "M \ N" and "M \ {}" and "finite N"
  shows "Min N \ Min M"
  using assms by (fact Min.subset_imp)

lemma Max_mono:
  assumes "M \ N" and "M \ {}" and "finite N"
  shows "Max M \ Max N"
  using assms by (fact Max.subset_imp)

lemma mono_Min_commute:
  assumes "mono f"
  assumes "finite A" and "A \ {}"
  shows "f (Min A) = Min (f ` A)"
proof (rule linorder_class.Min_eqI [symmetric])
  from \<open>finite A\<close> show "finite (f ` A)" by simp
  from assms show "f (Min A) \ f ` A" by simp
  fix x
  assume "x \ f ` A"
  then obtain y where "y \ A" and "x = f y" ..
  with assms have "Min A \ y" by auto
  with \<open>mono f\<close> have "f (Min A) \<le> f y" by (rule monoE)
  with \<open>x = f y\<close> show "f (Min A) \<le> x" by simp
qed

lemma mono_Max_commute:
  assumes "mono f"
  assumes "finite A" and "A \ {}"
  shows "f (Max A) = Max (f ` A)"
proof (rule linorder_class.Max_eqI [symmetric])
  from \<open>finite A\<close> show "finite (f ` A)" by simp
  from assms show "f (Max A) \ f ` A" by simp
  fix x
  assume "x \ f ` A"
  then obtain y where "y \ A" and "x = f y" ..
  with assms have "y \ Max A" by auto
  with \<open>mono f\<close> have "f y \<le> f (Max A)" by (rule monoE)
  with \<open>x = f y\<close> 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: "\b A. finite A \ \a\A. a < b \ P A \ P (insert b A)"
  shows "P A"
using fin empty insert
proof (induct rule: finite_psubset_induct)
  case (psubset A)
  have IH: "\B. \B < A; P {}; (\A b. \finite A; \a\A. a \ P (insert b A))\ \ P B" by fact
  have fin: "finite A" by fact
  have empty: "P {}" by fact
  have step: "\b A. \finite A; \a\A. a < b; P A\ \ P (insert b A)" by fact
  show "P A"
  proof (cases "A = {}")
    assume "A = {}"
    then show "P A" using \<open>P {}\<close> by simp
  next
    let ?B = "A - {Max A}"
    let ?A = "insert (Max A) ?B"
    have "finite ?B" using \<open>finite A\<close> by simp
    assume "A \ {}"
    with \<open>finite A\<close> have "Max A \<in> A" by auto
    then have A: "?A = A" using insert_Diff_single insert_absorb by auto
    then have "P ?B" using \<open>P {}\<close> step IH [of ?B] by blast
    moreover
    have "\a\?B. a < Max A" using Max_ge [OF \finite A\] by fastforce
    ultimately show "P A" using A insert_Diff_single step [OF \<open>finite ?B\<close>] by fastforce
  qed
qed

lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
  "\finite A; P {}; \b A. \finite A; \a\A. b < a; P A\ \ P (insert b A)\ \ P A"
  by (rule linorder.finite_linorder_max_induct [OF dual_linorder])

lemma finite_ranking_induct[consumes 1, case_names empty insert]:
  fixes f :: "'b \ 'a"
  assumes "finite S"
  assumes "P {}"
  assumes "\x S. finite S \ (\y. y \ S \ f y \ f x) \ P S \ P (insert x S)"
  shows "P S"
  using \<open>finite S\<close>
proof (induction rule: finite_psubset_induct)
  case (psubset A)
  {
    assume "A \ {}"
    hence "f ` A \ {}" and "finite (f ` A)"
      using psubset finite_image_iff by simp+
    then obtain a where "f a = Max (f ` A)" and "a \ A"
      by (metis Max_in[of "f ` A"] imageE)
    then have "P (A - {a})"
      using psubset(2) [of \<open>A - {a}\<close>] by auto
    moreover
    have "\y. y \ A \ f y \ f a"
      using \<open>f a = Max (f ` A)\<close> \<open>finite (f ` A)\<close> by simp
    ultimately
    have ?case
      by (metis \<open>a \<in> A\<close> DiffD1 insert_Diff assms(3) finite_Diff psubset.hyps)
  }
  thus ?case
    using assms(2) by blast
qed

lemma Least_Min:
  assumes "finite {a. P a}" and "\a. P a"
  shows "(LEAST a. P a) = Min {a. P a}"
proof -
  { fix A :: "'a set"
    assume A: "finite A" "A \ {}"
    have "(LEAST a. a \ 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 \ b \ A) = min a (LEAST a. a \ 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

lemma Greatest_Max:
  assumes "finite {a. P a}" and "\a. P a"
  shows "(GREATEST a. P a) = Max {a. P a}"
proof -
  { fix A :: "'a set"
    assume A: "finite A" "A \ {}"
    have "(GREATEST a. a \ A) = Max A"
    using A proof (induct A rule: finite_ne_induct)
      case singleton show ?case by (rule Greatest_equality) simp_all
    next
      case (insert a A)
      have "(GREATEST b. b = a \ b \ A) = max a (GREATEST a. a \ A)"
        by (auto intro!: Greatest_equality simp add: max_def not_le insert.hyps)
      with insert show ?case by simp
    qed
  } from this [of "{a. P a}"] assms show ?thesis by simp
qed

lemma infinite_growing:
  assumes "X \ {}"
  assumes *: "\x. x \ X \ \y\X. y > x"
  shows "\ finite X"
proof
  assume "finite X"
  with \<open>X \<noteq> {}\<close> have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X"
    by auto
  with *[of "Max X"] show False
    by auto
qed

end

lemma sum_le_card_Max: "finite A \ sum f A \ card A * Max (f ` A)"
using sum_bounded_above[of A f "Max (f ` A)"] by simp

lemma card_Min_le_sum: "finite A \ card A * Min (f ` A) \ sum f A"
using sum_bounded_below[of A "Min (f ` A)" f] by simp

context linordered_ab_semigroup_add
begin

lemma Min_add_commute:
  fixes k
  assumes "finite S" and "S \ {}"
  shows "Min ((\x. f x + k) ` S) = Min(f ` S) + k"
proof -
  have m: "\x y. min x y + k = min (x+k) (y+k)"
    by (simp add: min_def order.antisym add_right_mono)
  have "(\x. f x + k) ` S = (\y. y + k) ` (f ` S)" by auto
  also have "Min \ = Min (f ` S) + k"
    using assms hom_Min_commute [of "\y. y+k" "f ` S", OF m, symmetric] by simp
  finally show ?thesis by simp
qed

lemma Max_add_commute:
  fixes k
  assumes "finite S" and "S \ {}"
  shows "Max ((\x. f x + k) ` S) = Max(f ` S) + k"
proof -
  have m: "\x y. max x y + k = max (x+k) (y+k)"
    by (simp add: max_def order.antisym add_right_mono)
  have "(\x. f x + k) ` S = (\y. y + k) ` (f ` S)" by auto
  also have "Max \ = Max (f ` S) + k"
    using assms hom_Max_commute [of "\y. y+k" "f ` S", OF m, symmetric] by simp
  finally show ?thesis by simp
qed

end

context linordered_ab_group_add
begin

lemma minus_Max_eq_Min [simp]:
  "finite S \ S \ {} \ - 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 \ S \ {} \ - 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 \ {}"
  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 \ {}"
  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

lemma disjnt_ge_max: \<^marker>\<open>contributor \<open>Lars Hupel\<close>\<close>
  \<open>disjnt X Y\<close> if \<open>finite Y\<close> \<open>\<And>x. x \<in> X \<Longrightarrow> x > Max Y\<close>
  using that by (auto simp add: disjnt_def) (use Max_less_iff in blast)

subsection \<open>An aside: code generation for \<open>LEAST\<close> and \<open>GREATEST\<close>\<close>

context
begin

qualified definition Least :: \<open>'a::linorder set \<Rightarrow> 'a\<close> \<comment> \<open>only for code generation\<close>
  where Least_eq [code_abbrev, simp]: \<open>Least S = (LEAST x. x \<in> S)\<close>

qualified lemma Least_filter_eq [code_abbrev]:
  \<open>Least (Set.filter P S) = (LEAST x. x \<in> S \<and> P x)\<close>
  by simp

qualified definition Least_abort :: \<open>'a set \<Rightarrow> 'a::linorder\<close>
  where \<open>Least_abort = Least\<close>

qualified lemma Least_code [code abort: Lattices_Big.Least_abort, code]:
  \<open>Least A = (if finite A \<longrightarrow> Set.is_empty A then Least_abort A else Min A)\<close>
  using Least_Min [of \<open>\<lambda>x. x \<in> A\<close>] by (auto simp add: Least_abort_def)

qualified definition Greatest :: \<open>'a::linorder set \<Rightarrow> 'a\<close> \<comment> \<open>only for code generation\<close>
  where Greatest_eq [code_abbrev, simp]: \<open>Greatest S = (GREATEST x. x \<in> S)\<close>

qualified lemma Greatest_filter_eq [code_abbrev]:
  \<open>Greatest (Set.filter P S) = (GREATEST x. x \<in> S \<and> P x)\<close>
  by simp

qualified definition Greatest_abort :: \<open>'a set \<Rightarrow> 'a::linorder\<close>
  where \<open>Greatest_abort = Greatest\<close>

qualified lemma Greatest_code [code abort: Lattices_Big.Greatest_abort, code]:
  \<open>Greatest A = (if finite A \<longrightarrow> Set.is_empty A then Greatest_abort A else Max A)\<close>
  using Greatest_Max [of \<open>\<lambda>x. x \<in> A\<close>] by (auto simp add: Greatest_abort_def)

end

subsection \<open>Arg Min\<close>

context ord
begin

definition is_arg_min :: "('b \ 'a) \ ('b \ bool) \ 'b \ bool" where
"is_arg_min f P x = (P x \ \(\y. P y \ f y < f x))"

definition arg_min :: "('b \ 'a) \ ('b \ bool) \ 'b" where
"arg_min f P = (SOME x. is_arg_min f P x)"

definition arg_min_on :: "('b \ 'a) \ 'b set \ 'b" where
"arg_min_on f S = arg_min f (\x. x \ S)"

end

syntax
  "_arg_min" :: "('b \ 'a) \ pttrn \ bool \ 'b"
    (\<open>(\<open>indent=3 notation=\<open>binder ARG_MIN\<close>\<close>ARG'_MIN _ _./ _)\<close> [1000, 0, 10] 10)
syntax_consts
  "_arg_min" \<rightleftharpoons> arg_min
translations
  "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)"

lemma is_arg_min_linorder: fixes f :: "'a \ 'b :: linorder"
shows "is_arg_min f P x = (P x \ (\y. P y \ f x \ f y))"
by(auto simp add: is_arg_min_def)

lemma is_arg_min_antimono: fixes f :: "'a \ ('b::order)"
shows "\ is_arg_min f P x; f y \ f x; P y \ \ is_arg_min f P y"
by (simp add: order.order_iff_strict is_arg_min_def)

lemma arg_minI:
  "\ P x;
    \<And>y. P y \<Longrightarrow> \<not> f y < f x;
    \<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> \<not> f y < f x \<rbrakk> \<Longrightarrow> Q x \<rbrakk>
  \<Longrightarrow> Q (arg_min f P)"
  unfolding arg_min_def is_arg_min_def
  by (blast intro!: someI2_ex)

lemma arg_min_equality:
  "\ P k; \x. P x \ f k \ f x \ \ f (arg_min f P) = f k"
  for f :: "_ \ 'a::order"
  by (rule arg_minI; force simp: not_less less_le_not_le)

lemma wf_linord_ex_has_least:
  "\ wf r; \x y. (x, y) \ r\<^sup>+ \ (y, x) \ r\<^sup>*; P k \
   \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)"
  by (force dest!:  wf_trancl [THEN wf_eq_minimal [THEN iffD1, THEN spec], where x = "m ` Collect P"])

lemma ex_has_least_nat: "P k \ \x. P x \ (\y. P y \ m x \ m y)"
  for m :: "'a \ nat"
  unfolding pred_nat_trancl_eq_le [symmetric]
  apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
   apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
  by assumption

lemma arg_min_nat_lemma:
  "P k \ P(arg_min m P) \ (\y. P y \ m (arg_min m P) \ m y)"
  for m :: "'a \ nat"
  unfolding arg_min_def is_arg_min_linorder
  apply (rule someI_ex)
  apply (erule ex_has_least_nat)
  done

lemmas arg_min_natI = arg_min_nat_lemma [THEN conjunct1]

lemma is_arg_min_arg_min_nat: fixes m :: "'a \ nat"
shows "P x \ is_arg_min m P (arg_min m P)"
by (metis arg_min_nat_lemma is_arg_min_linorder)

lemma arg_min_nat_le: "P x \ m (arg_min m P) \ m x"
  for m :: "'a \ nat"
  by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp])

lemma ex_min_if_finite:
  "\ finite S; S \ {} \ \ \m\S. \(\x\S. x < (m::'a::order))"
  by(induction rule: finite.induct) (auto intro: order.strict_trans)

lemma ex_is_arg_min_if_finite: fixes f :: "'a \ 'b :: order"
  shows "\ finite S; S \ {} \ \ \x. is_arg_min f (\x. x \ S) x"
  unfolding is_arg_min_def
  using ex_min_if_finite[of "f ` S"]
  by auto

lemma arg_min_SOME_Min:
  "finite S \ arg_min_on f S = (SOME y. y \ S \ f y = Min(f ` S))"
  unfolding arg_min_on_def arg_min_def is_arg_min_linorder
  apply(rule arg_cong[where f = Eps])
  apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric])
  done

lemma arg_min_if_finite: fixes f :: "'a \ 'b :: order"
  assumes "finite S" "S \ {}"
  shows  "arg_min_on f S \ S" and "\(\x\S. f x < f (arg_min_on f S))"
  using ex_is_arg_min_if_finite[OF assms, of f]
  unfolding arg_min_on_def arg_min_def is_arg_min_def
  by(auto dest!: someI_ex)

lemma arg_min_least: fixes f :: "'a \ 'b :: linorder"
  shows "\ finite S; S \ {}; y \ S \ \ f(arg_min_on f S) \ f y"
  by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f)

lemma arg_min_inj_eq: fixes f :: "'a \ 'b :: order"
shows "\ inj_on f {x. P x}; P a; \y. P y \ f a \ f y \ \ arg_min f P = a"
apply(simp add: arg_min_def is_arg_min_def)
apply(rule someI2[of _ a])
apply (simp add: less_le_not_le)
by (metis inj_on_eq_iff less_le mem_Collect_eq)

subsection \<open>Arg Max\<close>

context ord
begin

definition is_arg_max :: "('b \ 'a) \ ('b \ bool) \ 'b \ bool" where
"is_arg_max f P x = (P x \ \(\y. P y \ f y > f x))"

definition arg_max :: "('b \ 'a) \ ('b \ bool) \ 'b" where
"arg_max f P = (SOME x. is_arg_max f P x)"

definition arg_max_on :: "('b \ 'a) \ 'b set \ 'b" where
"arg_max_on f S = arg_max f (\x. x \ S)"

end

syntax
  "_arg_max" :: "('b \ 'a) \ pttrn \ bool \ 'a"
    (\<open>(\<open>indent=3 notation=\<open>binder ARG_MAX\<close>\<close>ARG'_MAX _ _./ _)\<close> [1000, 0, 10] 10)
syntax_consts
  "_arg_max" \<rightleftharpoons> arg_max
translations
  "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)"

lemma is_arg_max_linorder: fixes f :: "'a \ 'b :: linorder"
shows "is_arg_max f P x = (P x \ (\y. P y \ f x \ f y))"
by(auto simp add: is_arg_max_def)

lemma arg_maxI:
  "P x \
    (\<And>y. P y \<Longrightarrow> \<not> f y > f x) \<Longrightarrow>
    (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> \<not> f y > f x \<Longrightarrow> Q x) \<Longrightarrow>
    Q (arg_max f P)"
  unfolding arg_max_def is_arg_max_def
  by (blast intro!: someI2_ex elim: )

lemma arg_max_equality:
  "\ P k; \x. P x \ f x \ f k \ \ f (arg_max f P) = f k"
  for f :: "_ \ 'a::order"
apply (rule arg_maxI [where f = f])
  apply assumption
apply (simp add: less_le_not_le)
by (metis le_less)

lemma ex_has_greatest_nat_lemma:
  "P k \ \x. P x \ (\y. P y \ \ f y \ f x) \ \y. P y \ \ f y < f k + n"
  for f :: "'a \ nat"
  by (induct n) (force simp: le_Suc_eq)+

lemma ex_has_greatest_nat:
  assumes "P k"
    and "\y. P y \ (f:: 'a \ nat) y < b"
shows "\x. P x \ (\y. P y \ f y \ f x)"
proof (rule ccontr)
  assume "\x. P x \ (\y. P y \ f y \ f x)"
  then have "\x. P x \ (\y. P y \ \ f y \ f x)"
    by auto
  then have "\y. P y \ \ f y < f k + (b - f k)"
    using assms ex_has_greatest_nat_lemma[of P k f "b - f k"]
    by blast
  then show "False"
    using assms by auto
qed

lemma arg_max_nat_lemma:
  "\ P k; \y. P y \ f y < b \
  \<Longrightarrow> P (arg_max f P) \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f (arg_max f P))"
  for f :: "'a \ nat"
  unfolding arg_max_def is_arg_max_linorder
  by (rule someI_ex) (metis ex_has_greatest_nat)

lemmas arg_max_natI = arg_max_nat_lemma [THEN conjunct1]

lemma arg_max_nat_le: "P x \ \y. P y \ f y < b \ f x \ f (arg_max f P)"
  for f :: "'a \ nat"
  using arg_max_nat_lemma by metis

end

quality97%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.22Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.