src/HOL/Lattices_Big.thy
changeset 54744 1e7f2d296e19
child 54745 46e441e61ff5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Lattices_Big.thy	Sun Dec 15 15:10:14 2013 +0100
     1.3 @@ -0,0 +1,833 @@
     1.4 +(*  Title:      HOL/Lattices_Big.thy
     1.5 +    Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     1.6 +                with contributions by Jeremy Avigad
     1.7 +*)
     1.8 +
     1.9 +header {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *}
    1.10 +
    1.11 +theory Lattices_Big
    1.12 +imports Finite_Set
    1.13 +begin
    1.14 +
    1.15 +subsection {* Generic lattice operations over a set *}
    1.16 +
    1.17 +no_notation times (infixl "*" 70)
    1.18 +no_notation Groups.one ("1")
    1.19 +
    1.20 +
    1.21 +subsubsection {* Without neutral element *}
    1.22 +
    1.23 +locale semilattice_set = semilattice
    1.24 +begin
    1.25 +
    1.26 +interpretation comp_fun_idem f
    1.27 +  by default (simp_all add: fun_eq_iff left_commute)
    1.28 +
    1.29 +definition F :: "'a set \<Rightarrow> 'a"
    1.30 +where
    1.31 +  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)"
    1.32 +
    1.33 +lemma eq_fold:
    1.34 +  assumes "finite A"
    1.35 +  shows "F (insert x A) = Finite_Set.fold f x A"
    1.36 +proof (rule sym)
    1.37 +  let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
    1.38 +  interpret comp_fun_idem "?f"
    1.39 +    by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
    1.40 +  from assms show "Finite_Set.fold f x A = F (insert x A)"
    1.41 +  proof induct
    1.42 +    case empty then show ?case by (simp add: eq_fold')
    1.43 +  next
    1.44 +    case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
    1.45 +  qed
    1.46 +qed
    1.47 +
    1.48 +lemma singleton [simp]:
    1.49 +  "F {x} = x"
    1.50 +  by (simp add: eq_fold)
    1.51 +
    1.52 +lemma insert_not_elem:
    1.53 +  assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
    1.54 +  shows "F (insert x A) = x * F A"
    1.55 +proof -
    1.56 +  from `A \<noteq> {}` obtain b where "b \<in> A" by blast
    1.57 +  then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
    1.58 +  with `finite A` and `x \<notin> A`
    1.59 +    have "finite (insert x B)" and "b \<notin> insert x B" by auto
    1.60 +  then have "F (insert b (insert x B)) = x * F (insert b B)"
    1.61 +    by (simp add: eq_fold)
    1.62 +  then show ?thesis by (simp add: * insert_commute)
    1.63 +qed
    1.64 +
    1.65 +lemma in_idem:
    1.66 +  assumes "finite A" and "x \<in> A"
    1.67 +  shows "x * F A = F A"
    1.68 +proof -
    1.69 +  from assms have "A \<noteq> {}" by auto
    1.70 +  with `finite A` show ?thesis using `x \<in> A`
    1.71 +    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
    1.72 +qed
    1.73 +
    1.74 +lemma insert [simp]:
    1.75 +  assumes "finite A" and "A \<noteq> {}"
    1.76 +  shows "F (insert x A) = x * F A"
    1.77 +  using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
    1.78 +
    1.79 +lemma union:
    1.80 +  assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
    1.81 +  shows "F (A \<union> B) = F A * F B"
    1.82 +  using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
    1.83 +
    1.84 +lemma remove:
    1.85 +  assumes "finite A" and "x \<in> A"
    1.86 +  shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
    1.87 +proof -
    1.88 +  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
    1.89 +  with assms show ?thesis by simp
    1.90 +qed
    1.91 +
    1.92 +lemma insert_remove:
    1.93 +  assumes "finite A"
    1.94 +  shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
    1.95 +  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
    1.96 +
    1.97 +lemma subset:
    1.98 +  assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
    1.99 +  shows "F B * F A = F A"
   1.100 +proof -
   1.101 +  from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
   1.102 +  with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
   1.103 +qed
   1.104 +
   1.105 +lemma closed:
   1.106 +  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
   1.107 +  shows "F A \<in> A"
   1.108 +using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
   1.109 +  case singleton then show ?case by simp
   1.110 +next
   1.111 +  case insert with elem show ?case by force
   1.112 +qed
   1.113 +
   1.114 +lemma hom_commute:
   1.115 +  assumes hom: "\<And>x y. h (x * y) = h x * h y"
   1.116 +  and N: "finite N" "N \<noteq> {}"
   1.117 +  shows "h (F N) = F (h ` N)"
   1.118 +using N proof (induct rule: finite_ne_induct)
   1.119 +  case singleton thus ?case by simp
   1.120 +next
   1.121 +  case (insert n N)
   1.122 +  then have "h (F (insert n N)) = h (n * F N)" by simp
   1.123 +  also have "\<dots> = h n * h (F N)" by (rule hom)
   1.124 +  also have "h (F N) = F (h ` N)" by (rule insert)
   1.125 +  also have "h n * \<dots> = F (insert (h n) (h ` N))"
   1.126 +    using insert by simp
   1.127 +  also have "insert (h n) (h ` N) = h ` insert n N" by simp
   1.128 +  finally show ?case .
   1.129 +qed
   1.130 +
   1.131 +end
   1.132 +
   1.133 +locale semilattice_order_set = semilattice_order + semilattice_set
   1.134 +begin
   1.135 +
   1.136 +lemma bounded_iff:
   1.137 +  assumes "finite A" and "A \<noteq> {}"
   1.138 +  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
   1.139 +  using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
   1.140 +
   1.141 +lemma boundedI:
   1.142 +  assumes "finite A"
   1.143 +  assumes "A \<noteq> {}"
   1.144 +  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   1.145 +  shows "x \<preceq> F A"
   1.146 +  using assms by (simp add: bounded_iff)
   1.147 +
   1.148 +lemma boundedE:
   1.149 +  assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
   1.150 +  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   1.151 +  using assms by (simp add: bounded_iff)
   1.152 +
   1.153 +lemma coboundedI:
   1.154 +  assumes "finite A"
   1.155 +    and "a \<in> A"
   1.156 +  shows "F A \<preceq> a"
   1.157 +proof -
   1.158 +  from assms have "A \<noteq> {}" by auto
   1.159 +  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
   1.160 +  proof (induct rule: finite_ne_induct)
   1.161 +    case singleton thus ?case by (simp add: refl)
   1.162 +  next
   1.163 +    case (insert x B)
   1.164 +    from insert have "a = x \<or> a \<in> B" by simp
   1.165 +    then show ?case using insert by (auto intro: coboundedI2)
   1.166 +  qed
   1.167 +qed
   1.168 +
   1.169 +lemma antimono:
   1.170 +  assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
   1.171 +  shows "F B \<preceq> F A"
   1.172 +proof (cases "A = B")
   1.173 +  case True then show ?thesis by (simp add: refl)
   1.174 +next
   1.175 +  case False
   1.176 +  have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
   1.177 +  then have "F B = F (A \<union> (B - A))" by simp
   1.178 +  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   1.179 +  also have "\<dots> \<preceq> F A" by simp
   1.180 +  finally show ?thesis .
   1.181 +qed
   1.182 +
   1.183 +end
   1.184 +
   1.185 +
   1.186 +subsubsection {* With neutral element *}
   1.187 +
   1.188 +locale semilattice_neutr_set = semilattice_neutr
   1.189 +begin
   1.190 +
   1.191 +interpretation comp_fun_idem f
   1.192 +  by default (simp_all add: fun_eq_iff left_commute)
   1.193 +
   1.194 +definition F :: "'a set \<Rightarrow> 'a"
   1.195 +where
   1.196 +  eq_fold: "F A = Finite_Set.fold f 1 A"
   1.197 +
   1.198 +lemma infinite [simp]:
   1.199 +  "\<not> finite A \<Longrightarrow> F A = 1"
   1.200 +  by (simp add: eq_fold)
   1.201 +
   1.202 +lemma empty [simp]:
   1.203 +  "F {} = 1"
   1.204 +  by (simp add: eq_fold)
   1.205 +
   1.206 +lemma insert [simp]:
   1.207 +  assumes "finite A"
   1.208 +  shows "F (insert x A) = x * F A"
   1.209 +  using assms by (simp add: eq_fold)
   1.210 +
   1.211 +lemma in_idem:
   1.212 +  assumes "finite A" and "x \<in> A"
   1.213 +  shows "x * F A = F A"
   1.214 +proof -
   1.215 +  from assms have "A \<noteq> {}" by auto
   1.216 +  with `finite A` show ?thesis using `x \<in> A`
   1.217 +    by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
   1.218 +qed
   1.219 +
   1.220 +lemma union:
   1.221 +  assumes "finite A" and "finite B"
   1.222 +  shows "F (A \<union> B) = F A * F B"
   1.223 +  using assms by (induct A) (simp_all add: ac_simps)
   1.224 +
   1.225 +lemma remove:
   1.226 +  assumes "finite A" and "x \<in> A"
   1.227 +  shows "F A = x * F (A - {x})"
   1.228 +proof -
   1.229 +  from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
   1.230 +  with assms show ?thesis by simp
   1.231 +qed
   1.232 +
   1.233 +lemma insert_remove:
   1.234 +  assumes "finite A"
   1.235 +  shows "F (insert x A) = x * F (A - {x})"
   1.236 +  using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
   1.237 +
   1.238 +lemma subset:
   1.239 +  assumes "finite A" and "B \<subseteq> A"
   1.240 +  shows "F B * F A = F A"
   1.241 +proof -
   1.242 +  from assms have "finite B" by (auto dest: finite_subset)
   1.243 +  with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
   1.244 +qed
   1.245 +
   1.246 +lemma closed:
   1.247 +  assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
   1.248 +  shows "F A \<in> A"
   1.249 +using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
   1.250 +  case singleton then show ?case by simp
   1.251 +next
   1.252 +  case insert with elem show ?case by force
   1.253 +qed
   1.254 +
   1.255 +end
   1.256 +
   1.257 +locale semilattice_order_neutr_set = semilattice_neutr_order + semilattice_neutr_set
   1.258 +begin
   1.259 +
   1.260 +lemma bounded_iff:
   1.261 +  assumes "finite A"
   1.262 +  shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
   1.263 +  using assms by (induct A) (simp_all add: bounded_iff)
   1.264 +
   1.265 +lemma boundedI:
   1.266 +  assumes "finite A"
   1.267 +  assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   1.268 +  shows "x \<preceq> F A"
   1.269 +  using assms by (simp add: bounded_iff)
   1.270 +
   1.271 +lemma boundedE:
   1.272 +  assumes "finite A" and "x \<preceq> F A"
   1.273 +  obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   1.274 +  using assms by (simp add: bounded_iff)
   1.275 +
   1.276 +lemma coboundedI:
   1.277 +  assumes "finite A"
   1.278 +    and "a \<in> A"
   1.279 +  shows "F A \<preceq> a"
   1.280 +proof -
   1.281 +  from assms have "A \<noteq> {}" by auto
   1.282 +  from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
   1.283 +  proof (induct rule: finite_ne_induct)
   1.284 +    case singleton thus ?case by (simp add: refl)
   1.285 +  next
   1.286 +    case (insert x B)
   1.287 +    from insert have "a = x \<or> a \<in> B" by simp
   1.288 +    then show ?case using insert by (auto intro: coboundedI2)
   1.289 +  qed
   1.290 +qed
   1.291 +
   1.292 +lemma antimono:
   1.293 +  assumes "A \<subseteq> B" and "finite B"
   1.294 +  shows "F B \<preceq> F A"
   1.295 +proof (cases "A = B")
   1.296 +  case True then show ?thesis by (simp add: refl)
   1.297 +next
   1.298 +  case False
   1.299 +  have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
   1.300 +  then have "F B = F (A \<union> (B - A))" by simp
   1.301 +  also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   1.302 +  also have "\<dots> \<preceq> F A" by simp
   1.303 +  finally show ?thesis .
   1.304 +qed
   1.305 +
   1.306 +end
   1.307 +
   1.308 +notation times (infixl "*" 70)
   1.309 +notation Groups.one ("1")
   1.310 +
   1.311 +
   1.312 +subsection {* Lattice operations on finite sets *}
   1.313 +
   1.314 +text {*
   1.315 +  For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
   1.316 +  to @{class linorder}.  This is badly designed: both should depend on a common abstract
   1.317 +  distributive lattice rather than having this non-subclass dependecy between two
   1.318 +  classes.  But for the moment we have to live with it.  This forces us to setup
   1.319 +  this sublocale dependency simultaneously with the lattice operations on finite
   1.320 +  sets, to avoid garbage.
   1.321 +*}
   1.322 +
   1.323 +definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
   1.324 +where
   1.325 +  "Inf_fin = semilattice_set.F inf"
   1.326 +
   1.327 +definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
   1.328 +where
   1.329 +  "Sup_fin = semilattice_set.F sup"
   1.330 +
   1.331 +context linorder
   1.332 +begin
   1.333 +
   1.334 +definition Min :: "'a set \<Rightarrow> 'a"
   1.335 +where
   1.336 +  "Min = semilattice_set.F min"
   1.337 +
   1.338 +definition Max :: "'a set \<Rightarrow> 'a"
   1.339 +where
   1.340 +  "Max = semilattice_set.F max"
   1.341 +
   1.342 +sublocale Min!: semilattice_order_set min less_eq less
   1.343 +  + Max!: semilattice_order_set max greater_eq greater
   1.344 +where
   1.345 +  "semilattice_set.F min = Min"
   1.346 +  and "semilattice_set.F max = Max"
   1.347 +proof -
   1.348 +  show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
   1.349 +  then interpret Min!: semilattice_order_set min less_eq less .
   1.350 +  show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
   1.351 +  then interpret Max!: semilattice_order_set max greater_eq greater .
   1.352 +  from Min_def show "semilattice_set.F min = Min" by rule
   1.353 +  from Max_def show "semilattice_set.F max = Max" by rule
   1.354 +qed
   1.355 +
   1.356 +
   1.357 +text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
   1.358 +
   1.359 +sublocale min_max!: distrib_lattice min less_eq less max
   1.360 +where
   1.361 +  "semilattice_inf.Inf_fin min = Min"
   1.362 +  and "semilattice_sup.Sup_fin max = Max"
   1.363 +proof -
   1.364 +  show "class.distrib_lattice min less_eq less max"
   1.365 +  proof
   1.366 +    fix x y z
   1.367 +    show "max x (min y z) = min (max x y) (max x z)"
   1.368 +      by (auto simp add: min_def max_def)
   1.369 +  qed (auto simp add: min_def max_def not_le less_imp_le)
   1.370 +  then interpret min_max!: distrib_lattice min less_eq less max .
   1.371 +  show "semilattice_inf.Inf_fin min = Min"
   1.372 +    by (simp only: min_max.Inf_fin_def Min_def)
   1.373 +  show "semilattice_sup.Sup_fin max = Max"
   1.374 +    by (simp only: min_max.Sup_fin_def Max_def)
   1.375 +qed
   1.376 +
   1.377 +lemmas le_maxI1 = min_max.sup_ge1
   1.378 +lemmas le_maxI2 = min_max.sup_ge2
   1.379 + 
   1.380 +lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   1.381 +  min.left_commute
   1.382 +
   1.383 +lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   1.384 +  max.left_commute
   1.385 +
   1.386 +end
   1.387 +
   1.388 +
   1.389 +text {* Lattice operations proper *}
   1.390 +
   1.391 +sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
   1.392 +where
   1.393 +  "semilattice_set.F inf = Inf_fin"
   1.394 +proof -
   1.395 +  show "semilattice_order_set inf less_eq less" ..
   1.396 +  then interpret Inf_fin!: semilattice_order_set inf less_eq less .
   1.397 +  from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
   1.398 +qed
   1.399 +
   1.400 +sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
   1.401 +where
   1.402 +  "semilattice_set.F sup = Sup_fin"
   1.403 +proof -
   1.404 +  show "semilattice_order_set sup greater_eq greater" ..
   1.405 +  then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
   1.406 +  from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
   1.407 +qed
   1.408 +
   1.409 +
   1.410 +text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
   1.411 +
   1.412 +lemma Inf_fin_Min:
   1.413 +  "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
   1.414 +  by (simp add: Inf_fin_def Min_def inf_min)
   1.415 +
   1.416 +lemma Sup_fin_Max:
   1.417 +  "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
   1.418 +  by (simp add: Sup_fin_def Max_def sup_max)
   1.419 +
   1.420 +
   1.421 +
   1.422 +subsection {* Infimum and Supremum over non-empty sets *}
   1.423 +
   1.424 +text {*
   1.425 +  After this non-regular bootstrap, things continue canonically.
   1.426 +*}
   1.427 +
   1.428 +context lattice
   1.429 +begin
   1.430 +
   1.431 +lemma Inf_le_Sup [simp]: "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
   1.432 +apply(subgoal_tac "EX a. a:A")
   1.433 +prefer 2 apply blast
   1.434 +apply(erule exE)
   1.435 +apply(rule order_trans)
   1.436 +apply(erule (1) Inf_fin.coboundedI)
   1.437 +apply(erule (1) Sup_fin.coboundedI)
   1.438 +done
   1.439 +
   1.440 +lemma sup_Inf_absorb [simp]:
   1.441 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = a"
   1.442 +apply(subst sup_commute)
   1.443 +apply(simp add: sup_absorb2 Inf_fin.coboundedI)
   1.444 +done
   1.445 +
   1.446 +lemma inf_Sup_absorb [simp]:
   1.447 +  "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = a"
   1.448 +by (simp add: inf_absorb1 Sup_fin.coboundedI)
   1.449 +
   1.450 +end
   1.451 +
   1.452 +context distrib_lattice
   1.453 +begin
   1.454 +
   1.455 +lemma sup_Inf1_distrib:
   1.456 +  assumes "finite A"
   1.457 +    and "A \<noteq> {}"
   1.458 +  shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
   1.459 +using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
   1.460 +  (rule arg_cong [where f="Inf_fin"], blast)
   1.461 +
   1.462 +lemma sup_Inf2_distrib:
   1.463 +  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   1.464 +  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}"
   1.465 +using A proof (induct rule: finite_ne_induct)
   1.466 +  case singleton then show ?case
   1.467 +    by (simp add: sup_Inf1_distrib [OF B])
   1.468 +next
   1.469 +  case (insert x A)
   1.470 +  have finB: "finite {sup x b |b. b \<in> B}"
   1.471 +    by (rule finite_surj [where f = "sup x", OF B(1)], auto)
   1.472 +  have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
   1.473 +  proof -
   1.474 +    have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
   1.475 +      by blast
   1.476 +    thus ?thesis by(simp add: insert(1) B(1))
   1.477 +  qed
   1.478 +  have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   1.479 +  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)"
   1.480 +    using insert by simp
   1.481 +  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)
   1.482 +  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})"
   1.483 +    using insert by(simp add:sup_Inf1_distrib[OF B])
   1.484 +  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})"
   1.485 +    (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
   1.486 +    using B insert
   1.487 +    by (simp add: Inf_fin.union [OF finB _ finAB ne])
   1.488 +  also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
   1.489 +    by blast
   1.490 +  finally show ?case .
   1.491 +qed
   1.492 +
   1.493 +lemma inf_Sup1_distrib:
   1.494 +  assumes "finite A" and "A \<noteq> {}"
   1.495 +  shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
   1.496 +using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
   1.497 +  (rule arg_cong [where f="Sup_fin"], blast)
   1.498 +
   1.499 +lemma inf_Sup2_distrib:
   1.500 +  assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   1.501 +  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}"
   1.502 +using A proof (induct rule: finite_ne_induct)
   1.503 +  case singleton thus ?case
   1.504 +    by(simp add: inf_Sup1_distrib [OF B])
   1.505 +next
   1.506 +  case (insert x A)
   1.507 +  have finB: "finite {inf x b |b. b \<in> B}"
   1.508 +    by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
   1.509 +  have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
   1.510 +  proof -
   1.511 +    have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
   1.512 +      by blast
   1.513 +    thus ?thesis by(simp add: insert(1) B(1))
   1.514 +  qed
   1.515 +  have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   1.516 +  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)"
   1.517 +    using insert by simp
   1.518 +  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)
   1.519 +  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})"
   1.520 +    using insert by(simp add:inf_Sup1_distrib[OF B])
   1.521 +  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})"
   1.522 +    (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
   1.523 +    using B insert
   1.524 +    by (simp add: Sup_fin.union [OF finB _ finAB ne])
   1.525 +  also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
   1.526 +    by blast
   1.527 +  finally show ?case .
   1.528 +qed
   1.529 +
   1.530 +end
   1.531 +
   1.532 +context complete_lattice
   1.533 +begin
   1.534 +
   1.535 +lemma Inf_fin_Inf:
   1.536 +  assumes "finite A" and "A \<noteq> {}"
   1.537 +  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
   1.538 +proof -
   1.539 +  from assms obtain b B where "A = insert b B" and "finite B" by auto
   1.540 +  then show ?thesis
   1.541 +    by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
   1.542 +qed
   1.543 +
   1.544 +lemma Sup_fin_Sup:
   1.545 +  assumes "finite A" and "A \<noteq> {}"
   1.546 +  shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
   1.547 +proof -
   1.548 +  from assms obtain b B where "A = insert b B" and "finite B" by auto
   1.549 +  then show ?thesis
   1.550 +    by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
   1.551 +qed
   1.552 +
   1.553 +end
   1.554 +
   1.555 +
   1.556 +subsection {* Minimum and Maximum over non-empty sets *}
   1.557 +
   1.558 +context linorder
   1.559 +begin
   1.560 +
   1.561 +lemma dual_min:
   1.562 +  "ord.min greater_eq = max"
   1.563 +  by (auto simp add: ord.min_def max_def fun_eq_iff)
   1.564 +
   1.565 +lemma dual_max:
   1.566 +  "ord.max greater_eq = min"
   1.567 +  by (auto simp add: ord.max_def min_def fun_eq_iff)
   1.568 +
   1.569 +lemma dual_Min:
   1.570 +  "linorder.Min greater_eq = Max"
   1.571 +proof -
   1.572 +  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   1.573 +  show ?thesis by (simp add: dual.Min_def dual_min Max_def)
   1.574 +qed
   1.575 +
   1.576 +lemma dual_Max:
   1.577 +  "linorder.Max greater_eq = Min"
   1.578 +proof -
   1.579 +  interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   1.580 +  show ?thesis by (simp add: dual.Max_def dual_max Min_def)
   1.581 +qed
   1.582 +
   1.583 +lemmas Min_singleton = Min.singleton
   1.584 +lemmas Max_singleton = Max.singleton
   1.585 +lemmas Min_insert = Min.insert
   1.586 +lemmas Max_insert = Max.insert
   1.587 +lemmas Min_Un = Min.union
   1.588 +lemmas Max_Un = Max.union
   1.589 +lemmas hom_Min_commute = Min.hom_commute
   1.590 +lemmas hom_Max_commute = Max.hom_commute
   1.591 +
   1.592 +lemma Min_in [simp]:
   1.593 +  assumes "finite A" and "A \<noteq> {}"
   1.594 +  shows "Min A \<in> A"
   1.595 +  using assms by (auto simp add: min_def Min.closed)
   1.596 +
   1.597 +lemma Max_in [simp]:
   1.598 +  assumes "finite A" and "A \<noteq> {}"
   1.599 +  shows "Max A \<in> A"
   1.600 +  using assms by (auto simp add: max_def Max.closed)
   1.601 +
   1.602 +lemma Min_le [simp]:
   1.603 +  assumes "finite A" and "x \<in> A"
   1.604 +  shows "Min A \<le> x"
   1.605 +  using assms by (fact Min.coboundedI)
   1.606 +
   1.607 +lemma Max_ge [simp]:
   1.608 +  assumes "finite A" and "x \<in> A"
   1.609 +  shows "x \<le> Max A"
   1.610 +  using assms by (fact Max.coboundedI)
   1.611 +
   1.612 +lemma Min_eqI:
   1.613 +  assumes "finite A"
   1.614 +  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
   1.615 +    and "x \<in> A"
   1.616 +  shows "Min A = x"
   1.617 +proof (rule antisym)
   1.618 +  from `x \<in> A` have "A \<noteq> {}" by auto
   1.619 +  with assms show "Min A \<ge> x" by simp
   1.620 +next
   1.621 +  from assms show "x \<ge> Min A" by simp
   1.622 +qed
   1.623 +
   1.624 +lemma Max_eqI:
   1.625 +  assumes "finite A"
   1.626 +  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
   1.627 +    and "x \<in> A"
   1.628 +  shows "Max A = x"
   1.629 +proof (rule antisym)
   1.630 +  from `x \<in> A` have "A \<noteq> {}" by auto
   1.631 +  with assms show "Max A \<le> x" by simp
   1.632 +next
   1.633 +  from assms show "x \<le> Max A" by simp
   1.634 +qed
   1.635 +
   1.636 +context
   1.637 +  fixes A :: "'a set"
   1.638 +  assumes fin_nonempty: "finite A" "A \<noteq> {}"
   1.639 +begin
   1.640 +
   1.641 +lemma Min_ge_iff [simp]:
   1.642 +  "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   1.643 +  using fin_nonempty by (fact Min.bounded_iff)
   1.644 +
   1.645 +lemma Max_le_iff [simp]:
   1.646 +  "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   1.647 +  using fin_nonempty by (fact Max.bounded_iff)
   1.648 +
   1.649 +lemma Min_gr_iff [simp]:
   1.650 +  "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   1.651 +  using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
   1.652 +
   1.653 +lemma Max_less_iff [simp]:
   1.654 +  "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   1.655 +  using fin_nonempty by (induct rule: finite_ne_induct) simp_all
   1.656 +
   1.657 +lemma Min_le_iff:
   1.658 +  "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   1.659 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
   1.660 +
   1.661 +lemma Max_ge_iff:
   1.662 +  "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   1.663 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
   1.664 +
   1.665 +lemma Min_less_iff:
   1.666 +  "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   1.667 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
   1.668 +
   1.669 +lemma Max_gr_iff:
   1.670 +  "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   1.671 +  using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
   1.672 +
   1.673 +end
   1.674 +
   1.675 +lemma Min_antimono:
   1.676 +  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   1.677 +  shows "Min N \<le> Min M"
   1.678 +  using assms by (fact Min.antimono)
   1.679 +
   1.680 +lemma Max_mono:
   1.681 +  assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   1.682 +  shows "Max M \<le> Max N"
   1.683 +  using assms by (fact Max.antimono)
   1.684 +
   1.685 +lemma mono_Min_commute:
   1.686 +  assumes "mono f"
   1.687 +  assumes "finite A" and "A \<noteq> {}"
   1.688 +  shows "f (Min A) = Min (f ` A)"
   1.689 +proof (rule linorder_class.Min_eqI [symmetric])
   1.690 +  from `finite A` show "finite (f ` A)" by simp
   1.691 +  from assms show "f (Min A) \<in> f ` A" by simp
   1.692 +  fix x
   1.693 +  assume "x \<in> f ` A"
   1.694 +  then obtain y where "y \<in> A" and "x = f y" ..
   1.695 +  with assms have "Min A \<le> y" by auto
   1.696 +  with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
   1.697 +  with `x = f y` show "f (Min A) \<le> x" by simp
   1.698 +qed
   1.699 +
   1.700 +lemma mono_Max_commute:
   1.701 +  assumes "mono f"
   1.702 +  assumes "finite A" and "A \<noteq> {}"
   1.703 +  shows "f (Max A) = Max (f ` A)"
   1.704 +proof (rule linorder_class.Max_eqI [symmetric])
   1.705 +  from `finite A` show "finite (f ` A)" by simp
   1.706 +  from assms show "f (Max A) \<in> f ` A" by simp
   1.707 +  fix x
   1.708 +  assume "x \<in> f ` A"
   1.709 +  then obtain y where "y \<in> A" and "x = f y" ..
   1.710 +  with assms have "y \<le> Max A" by auto
   1.711 +  with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
   1.712 +  with `x = f y` show "x \<le> f (Max A)" by simp
   1.713 +qed
   1.714 +
   1.715 +lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
   1.716 +  assumes fin: "finite A"
   1.717 +  and empty: "P {}" 
   1.718 +  and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
   1.719 +  shows "P A"
   1.720 +using fin empty insert
   1.721 +proof (induct rule: finite_psubset_induct)
   1.722 +  case (psubset A)
   1.723 +  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 
   1.724 +  have fin: "finite A" by fact 
   1.725 +  have empty: "P {}" by fact
   1.726 +  have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
   1.727 +  show "P A"
   1.728 +  proof (cases "A = {}")
   1.729 +    assume "A = {}" 
   1.730 +    then show "P A" using `P {}` by simp
   1.731 +  next
   1.732 +    let ?B = "A - {Max A}" 
   1.733 +    let ?A = "insert (Max A) ?B"
   1.734 +    have "finite ?B" using `finite A` by simp
   1.735 +    assume "A \<noteq> {}"
   1.736 +    with `finite A` have "Max A : A" by auto
   1.737 +    then have A: "?A = A" using insert_Diff_single insert_absorb by auto
   1.738 +    then have "P ?B" using `P {}` step IH [of ?B] by blast
   1.739 +    moreover 
   1.740 +    have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
   1.741 +    ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
   1.742 +  qed
   1.743 +qed
   1.744 +
   1.745 +lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
   1.746 +  "\<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"
   1.747 +  by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
   1.748 +
   1.749 +lemma Least_Min:
   1.750 +  assumes "finite {a. P a}" and "\<exists>a. P a"
   1.751 +  shows "(LEAST a. P a) = Min {a. P a}"
   1.752 +proof -
   1.753 +  { fix A :: "'a set"
   1.754 +    assume A: "finite A" "A \<noteq> {}"
   1.755 +    have "(LEAST a. a \<in> A) = Min A"
   1.756 +    using A proof (induct A rule: finite_ne_induct)
   1.757 +      case singleton show ?case by (rule Least_equality) simp_all
   1.758 +    next
   1.759 +      case (insert a A)
   1.760 +      have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
   1.761 +        by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
   1.762 +      with insert show ?case by simp
   1.763 +    qed
   1.764 +  } from this [of "{a. P a}"] assms show ?thesis by simp
   1.765 +qed
   1.766 +
   1.767 +end
   1.768 +
   1.769 +context linordered_ab_semigroup_add
   1.770 +begin
   1.771 +
   1.772 +lemma add_Min_commute:
   1.773 +  fixes k
   1.774 +  assumes "finite N" and "N \<noteq> {}"
   1.775 +  shows "k + Min N = Min {k + m | m. m \<in> N}"
   1.776 +proof -
   1.777 +  have "\<And>x y. k + min x y = min (k + x) (k + y)"
   1.778 +    by (simp add: min_def not_le)
   1.779 +      (blast intro: antisym less_imp_le add_left_mono)
   1.780 +  with assms show ?thesis
   1.781 +    using hom_Min_commute [of "plus k" N]
   1.782 +    by simp (blast intro: arg_cong [where f = Min])
   1.783 +qed
   1.784 +
   1.785 +lemma add_Max_commute:
   1.786 +  fixes k
   1.787 +  assumes "finite N" and "N \<noteq> {}"
   1.788 +  shows "k + Max N = Max {k + m | m. m \<in> N}"
   1.789 +proof -
   1.790 +  have "\<And>x y. k + max x y = max (k + x) (k + y)"
   1.791 +    by (simp add: max_def not_le)
   1.792 +      (blast intro: antisym less_imp_le add_left_mono)
   1.793 +  with assms show ?thesis
   1.794 +    using hom_Max_commute [of "plus k" N]
   1.795 +    by simp (blast intro: arg_cong [where f = Max])
   1.796 +qed
   1.797 +
   1.798 +end
   1.799 +
   1.800 +context linordered_ab_group_add
   1.801 +begin
   1.802 +
   1.803 +lemma minus_Max_eq_Min [simp]:
   1.804 +  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
   1.805 +  by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
   1.806 +
   1.807 +lemma minus_Min_eq_Max [simp]:
   1.808 +  "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
   1.809 +  by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
   1.810 +
   1.811 +end
   1.812 +
   1.813 +context complete_linorder
   1.814 +begin
   1.815 +
   1.816 +lemma Min_Inf:
   1.817 +  assumes "finite A" and "A \<noteq> {}"
   1.818 +  shows "Min A = Inf A"
   1.819 +proof -
   1.820 +  from assms obtain b B where "A = insert b B" and "finite B" by auto
   1.821 +  then show ?thesis
   1.822 +    by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
   1.823 +qed
   1.824 +
   1.825 +lemma Max_Sup:
   1.826 +  assumes "finite A" and "A \<noteq> {}"
   1.827 +  shows "Max A = Sup A"
   1.828 +proof -
   1.829 +  from assms obtain b B where "A = insert b B" and "finite B" by auto
   1.830 +  then show ?thesis
   1.831 +    by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
   1.832 +qed
   1.833 +
   1.834 +end
   1.835 +
   1.836 +end