src/HOL/Lattices_Big.thy
author haftmann
Sun Dec 15 15:10:14 2013 +0100 (2013-12-15)
changeset 54744 1e7f2d296e19
child 54745 46e441e61ff5
permissions -rw-r--r--
more algebraic terminology for theories about big operators
     1 (*  Title:      HOL/Lattices_Big.thy
     2     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     3                 with contributions by Jeremy Avigad
     4 *)
     5 
     6 header {* Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets *}
     7 
     8 theory Lattices_Big
     9 imports Finite_Set
    10 begin
    11 
    12 subsection {* Generic lattice operations over a set *}
    13 
    14 no_notation times (infixl "*" 70)
    15 no_notation Groups.one ("1")
    16 
    17 
    18 subsubsection {* Without neutral element *}
    19 
    20 locale semilattice_set = semilattice
    21 begin
    22 
    23 interpretation comp_fun_idem f
    24   by default (simp_all add: fun_eq_iff left_commute)
    25 
    26 definition F :: "'a set \<Rightarrow> 'a"
    27 where
    28   eq_fold': "F A = the (Finite_Set.fold (\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)) None A)"
    29 
    30 lemma eq_fold:
    31   assumes "finite A"
    32   shows "F (insert x A) = Finite_Set.fold f x A"
    33 proof (rule sym)
    34   let ?f = "\<lambda>x y. Some (case y of None \<Rightarrow> x | Some z \<Rightarrow> f x z)"
    35   interpret comp_fun_idem "?f"
    36     by default (simp_all add: fun_eq_iff commute left_commute split: option.split)
    37   from assms show "Finite_Set.fold f x A = F (insert x A)"
    38   proof induct
    39     case empty then show ?case by (simp add: eq_fold')
    40   next
    41     case (insert y B) then show ?case by (simp add: insert_commute [of x] eq_fold')
    42   qed
    43 qed
    44 
    45 lemma singleton [simp]:
    46   "F {x} = x"
    47   by (simp add: eq_fold)
    48 
    49 lemma insert_not_elem:
    50   assumes "finite A" and "x \<notin> A" and "A \<noteq> {}"
    51   shows "F (insert x A) = x * F A"
    52 proof -
    53   from `A \<noteq> {}` obtain b where "b \<in> A" by blast
    54   then obtain B where *: "A = insert b B" "b \<notin> B" by (blast dest: mk_disjoint_insert)
    55   with `finite A` and `x \<notin> A`
    56     have "finite (insert x B)" and "b \<notin> insert x B" by auto
    57   then have "F (insert b (insert x B)) = x * F (insert b B)"
    58     by (simp add: eq_fold)
    59   then show ?thesis by (simp add: * insert_commute)
    60 qed
    61 
    62 lemma in_idem:
    63   assumes "finite A" and "x \<in> A"
    64   shows "x * F A = F A"
    65 proof -
    66   from assms have "A \<noteq> {}" by auto
    67   with `finite A` show ?thesis using `x \<in> A`
    68     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps insert_not_elem)
    69 qed
    70 
    71 lemma insert [simp]:
    72   assumes "finite A" and "A \<noteq> {}"
    73   shows "F (insert x A) = x * F A"
    74   using assms by (cases "x \<in> A") (simp_all add: insert_absorb in_idem insert_not_elem)
    75 
    76 lemma union:
    77   assumes "finite A" "A \<noteq> {}" and "finite B" "B \<noteq> {}"
    78   shows "F (A \<union> B) = F A * F B"
    79   using assms by (induct A rule: finite_ne_induct) (simp_all add: ac_simps)
    80 
    81 lemma remove:
    82   assumes "finite A" and "x \<in> A"
    83   shows "F A = (if A - {x} = {} then x else x * F (A - {x}))"
    84 proof -
    85   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
    86   with assms show ?thesis by simp
    87 qed
    88 
    89 lemma insert_remove:
    90   assumes "finite A"
    91   shows "F (insert x A) = (if A - {x} = {} then x else x * F (A - {x}))"
    92   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
    93 
    94 lemma subset:
    95   assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A"
    96   shows "F B * F A = F A"
    97 proof -
    98   from assms have "A \<noteq> {}" and "finite B" by (auto dest: finite_subset)
    99   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
   100 qed
   101 
   102 lemma closed:
   103   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
   104   shows "F A \<in> A"
   105 using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
   106   case singleton then show ?case by simp
   107 next
   108   case insert with elem show ?case by force
   109 qed
   110 
   111 lemma hom_commute:
   112   assumes hom: "\<And>x y. h (x * y) = h x * h y"
   113   and N: "finite N" "N \<noteq> {}"
   114   shows "h (F N) = F (h ` N)"
   115 using N proof (induct rule: finite_ne_induct)
   116   case singleton thus ?case by simp
   117 next
   118   case (insert n N)
   119   then have "h (F (insert n N)) = h (n * F N)" by simp
   120   also have "\<dots> = h n * h (F N)" by (rule hom)
   121   also have "h (F N) = F (h ` N)" by (rule insert)
   122   also have "h n * \<dots> = F (insert (h n) (h ` N))"
   123     using insert by simp
   124   also have "insert (h n) (h ` N) = h ` insert n N" by simp
   125   finally show ?case .
   126 qed
   127 
   128 end
   129 
   130 locale semilattice_order_set = semilattice_order + semilattice_set
   131 begin
   132 
   133 lemma bounded_iff:
   134   assumes "finite A" and "A \<noteq> {}"
   135   shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
   136   using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
   137 
   138 lemma boundedI:
   139   assumes "finite A"
   140   assumes "A \<noteq> {}"
   141   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   142   shows "x \<preceq> F A"
   143   using assms by (simp add: bounded_iff)
   144 
   145 lemma boundedE:
   146   assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
   147   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   148   using assms by (simp add: bounded_iff)
   149 
   150 lemma coboundedI:
   151   assumes "finite A"
   152     and "a \<in> A"
   153   shows "F A \<preceq> a"
   154 proof -
   155   from assms have "A \<noteq> {}" by auto
   156   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
   157   proof (induct rule: finite_ne_induct)
   158     case singleton thus ?case by (simp add: refl)
   159   next
   160     case (insert x B)
   161     from insert have "a = x \<or> a \<in> B" by simp
   162     then show ?case using insert by (auto intro: coboundedI2)
   163   qed
   164 qed
   165 
   166 lemma antimono:
   167   assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
   168   shows "F B \<preceq> F A"
   169 proof (cases "A = B")
   170   case True then show ?thesis by (simp add: refl)
   171 next
   172   case False
   173   have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
   174   then have "F B = F (A \<union> (B - A))" by simp
   175   also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   176   also have "\<dots> \<preceq> F A" by simp
   177   finally show ?thesis .
   178 qed
   179 
   180 end
   181 
   182 
   183 subsubsection {* With neutral element *}
   184 
   185 locale semilattice_neutr_set = semilattice_neutr
   186 begin
   187 
   188 interpretation comp_fun_idem f
   189   by default (simp_all add: fun_eq_iff left_commute)
   190 
   191 definition F :: "'a set \<Rightarrow> 'a"
   192 where
   193   eq_fold: "F A = Finite_Set.fold f 1 A"
   194 
   195 lemma infinite [simp]:
   196   "\<not> finite A \<Longrightarrow> F A = 1"
   197   by (simp add: eq_fold)
   198 
   199 lemma empty [simp]:
   200   "F {} = 1"
   201   by (simp add: eq_fold)
   202 
   203 lemma insert [simp]:
   204   assumes "finite A"
   205   shows "F (insert x A) = x * F A"
   206   using assms by (simp add: eq_fold)
   207 
   208 lemma in_idem:
   209   assumes "finite A" and "x \<in> A"
   210   shows "x * F A = F A"
   211 proof -
   212   from assms have "A \<noteq> {}" by auto
   213   with `finite A` show ?thesis using `x \<in> A`
   214     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
   215 qed
   216 
   217 lemma union:
   218   assumes "finite A" and "finite B"
   219   shows "F (A \<union> B) = F A * F B"
   220   using assms by (induct A) (simp_all add: ac_simps)
   221 
   222 lemma remove:
   223   assumes "finite A" and "x \<in> A"
   224   shows "F A = x * F (A - {x})"
   225 proof -
   226   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
   227   with assms show ?thesis by simp
   228 qed
   229 
   230 lemma insert_remove:
   231   assumes "finite A"
   232   shows "F (insert x A) = x * F (A - {x})"
   233   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
   234 
   235 lemma subset:
   236   assumes "finite A" and "B \<subseteq> A"
   237   shows "F B * F A = F A"
   238 proof -
   239   from assms have "finite B" by (auto dest: finite_subset)
   240   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
   241 qed
   242 
   243 lemma closed:
   244   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
   245   shows "F A \<in> A"
   246 using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
   247   case singleton then show ?case by simp
   248 next
   249   case insert with elem show ?case by force
   250 qed
   251 
   252 end
   253 
   254 locale semilattice_order_neutr_set = semilattice_neutr_order + semilattice_neutr_set
   255 begin
   256 
   257 lemma bounded_iff:
   258   assumes "finite A"
   259   shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
   260   using assms by (induct A) (simp_all add: bounded_iff)
   261 
   262 lemma boundedI:
   263   assumes "finite A"
   264   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   265   shows "x \<preceq> F A"
   266   using assms by (simp add: bounded_iff)
   267 
   268 lemma boundedE:
   269   assumes "finite A" and "x \<preceq> F A"
   270   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   271   using assms by (simp add: bounded_iff)
   272 
   273 lemma coboundedI:
   274   assumes "finite A"
   275     and "a \<in> A"
   276   shows "F A \<preceq> a"
   277 proof -
   278   from assms have "A \<noteq> {}" by auto
   279   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
   280   proof (induct rule: finite_ne_induct)
   281     case singleton thus ?case by (simp add: refl)
   282   next
   283     case (insert x B)
   284     from insert have "a = x \<or> a \<in> B" by simp
   285     then show ?case using insert by (auto intro: coboundedI2)
   286   qed
   287 qed
   288 
   289 lemma antimono:
   290   assumes "A \<subseteq> B" and "finite B"
   291   shows "F B \<preceq> F A"
   292 proof (cases "A = B")
   293   case True then show ?thesis by (simp add: refl)
   294 next
   295   case False
   296   have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
   297   then have "F B = F (A \<union> (B - A))" by simp
   298   also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   299   also have "\<dots> \<preceq> F A" by simp
   300   finally show ?thesis .
   301 qed
   302 
   303 end
   304 
   305 notation times (infixl "*" 70)
   306 notation Groups.one ("1")
   307 
   308 
   309 subsection {* Lattice operations on finite sets *}
   310 
   311 text {*
   312   For historic reasons, there is the sublocale dependency from @{class distrib_lattice}
   313   to @{class linorder}.  This is badly designed: both should depend on a common abstract
   314   distributive lattice rather than having this non-subclass dependecy between two
   315   classes.  But for the moment we have to live with it.  This forces us to setup
   316   this sublocale dependency simultaneously with the lattice operations on finite
   317   sets, to avoid garbage.
   318 *}
   319 
   320 definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
   321 where
   322   "Inf_fin = semilattice_set.F inf"
   323 
   324 definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
   325 where
   326   "Sup_fin = semilattice_set.F sup"
   327 
   328 context linorder
   329 begin
   330 
   331 definition Min :: "'a set \<Rightarrow> 'a"
   332 where
   333   "Min = semilattice_set.F min"
   334 
   335 definition Max :: "'a set \<Rightarrow> 'a"
   336 where
   337   "Max = semilattice_set.F max"
   338 
   339 sublocale Min!: semilattice_order_set min less_eq less
   340   + Max!: semilattice_order_set max greater_eq greater
   341 where
   342   "semilattice_set.F min = Min"
   343   and "semilattice_set.F max = Max"
   344 proof -
   345   show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
   346   then interpret Min!: semilattice_order_set min less_eq less .
   347   show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
   348   then interpret Max!: semilattice_order_set max greater_eq greater .
   349   from Min_def show "semilattice_set.F min = Min" by rule
   350   from Max_def show "semilattice_set.F max = Max" by rule
   351 qed
   352 
   353 
   354 text {* An aside: @{const min}/@{const max} on linear orders as special case of @{const inf}/@{const sup} *}
   355 
   356 sublocale min_max!: distrib_lattice min less_eq less max
   357 where
   358   "semilattice_inf.Inf_fin min = Min"
   359   and "semilattice_sup.Sup_fin max = Max"
   360 proof -
   361   show "class.distrib_lattice min less_eq less max"
   362   proof
   363     fix x y z
   364     show "max x (min y z) = min (max x y) (max x z)"
   365       by (auto simp add: min_def max_def)
   366   qed (auto simp add: min_def max_def not_le less_imp_le)
   367   then interpret min_max!: distrib_lattice min less_eq less max .
   368   show "semilattice_inf.Inf_fin min = Min"
   369     by (simp only: min_max.Inf_fin_def Min_def)
   370   show "semilattice_sup.Sup_fin max = Max"
   371     by (simp only: min_max.Sup_fin_def Max_def)
   372 qed
   373 
   374 lemmas le_maxI1 = min_max.sup_ge1
   375 lemmas le_maxI2 = min_max.sup_ge2
   376  
   377 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   378   min.left_commute
   379 
   380 lemmas max_ac = min_max.sup_assoc min_max.sup_commute
   381   max.left_commute
   382 
   383 end
   384 
   385 
   386 text {* Lattice operations proper *}
   387 
   388 sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
   389 where
   390   "semilattice_set.F inf = Inf_fin"
   391 proof -
   392   show "semilattice_order_set inf less_eq less" ..
   393   then interpret Inf_fin!: semilattice_order_set inf less_eq less .
   394   from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
   395 qed
   396 
   397 sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
   398 where
   399   "semilattice_set.F sup = Sup_fin"
   400 proof -
   401   show "semilattice_order_set sup greater_eq greater" ..
   402   then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
   403   from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
   404 qed
   405 
   406 
   407 text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
   408 
   409 lemma Inf_fin_Min:
   410   "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
   411   by (simp add: Inf_fin_def Min_def inf_min)
   412 
   413 lemma Sup_fin_Max:
   414   "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
   415   by (simp add: Sup_fin_def Max_def sup_max)
   416 
   417 
   418 
   419 subsection {* Infimum and Supremum over non-empty sets *}
   420 
   421 text {*
   422   After this non-regular bootstrap, things continue canonically.
   423 *}
   424 
   425 context lattice
   426 begin
   427 
   428 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"
   429 apply(subgoal_tac "EX a. a:A")
   430 prefer 2 apply blast
   431 apply(erule exE)
   432 apply(rule order_trans)
   433 apply(erule (1) Inf_fin.coboundedI)
   434 apply(erule (1) Sup_fin.coboundedI)
   435 done
   436 
   437 lemma sup_Inf_absorb [simp]:
   438   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> sup a (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = a"
   439 apply(subst sup_commute)
   440 apply(simp add: sup_absorb2 Inf_fin.coboundedI)
   441 done
   442 
   443 lemma inf_Sup_absorb [simp]:
   444   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> inf a (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = a"
   445 by (simp add: inf_absorb1 Sup_fin.coboundedI)
   446 
   447 end
   448 
   449 context distrib_lattice
   450 begin
   451 
   452 lemma sup_Inf1_distrib:
   453   assumes "finite A"
   454     and "A \<noteq> {}"
   455   shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
   456 using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
   457   (rule arg_cong [where f="Inf_fin"], blast)
   458 
   459 lemma sup_Inf2_distrib:
   460   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   461   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}"
   462 using A proof (induct rule: finite_ne_induct)
   463   case singleton then show ?case
   464     by (simp add: sup_Inf1_distrib [OF B])
   465 next
   466   case (insert x A)
   467   have finB: "finite {sup x b |b. b \<in> B}"
   468     by (rule finite_surj [where f = "sup x", OF B(1)], auto)
   469   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
   470   proof -
   471     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
   472       by blast
   473     thus ?thesis by(simp add: insert(1) B(1))
   474   qed
   475   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   476   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)"
   477     using insert by simp
   478   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)
   479   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})"
   480     using insert by(simp add:sup_Inf1_distrib[OF B])
   481   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})"
   482     (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
   483     using B insert
   484     by (simp add: Inf_fin.union [OF finB _ finAB ne])
   485   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
   486     by blast
   487   finally show ?case .
   488 qed
   489 
   490 lemma inf_Sup1_distrib:
   491   assumes "finite A" and "A \<noteq> {}"
   492   shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
   493 using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
   494   (rule arg_cong [where f="Sup_fin"], blast)
   495 
   496 lemma inf_Sup2_distrib:
   497   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   498   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}"
   499 using A proof (induct rule: finite_ne_induct)
   500   case singleton thus ?case
   501     by(simp add: inf_Sup1_distrib [OF B])
   502 next
   503   case (insert x A)
   504   have finB: "finite {inf x b |b. b \<in> B}"
   505     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
   506   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
   507   proof -
   508     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
   509       by blast
   510     thus ?thesis by(simp add: insert(1) B(1))
   511   qed
   512   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   513   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)"
   514     using insert by simp
   515   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)
   516   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})"
   517     using insert by(simp add:inf_Sup1_distrib[OF B])
   518   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})"
   519     (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
   520     using B insert
   521     by (simp add: Sup_fin.union [OF finB _ finAB ne])
   522   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
   523     by blast
   524   finally show ?case .
   525 qed
   526 
   527 end
   528 
   529 context complete_lattice
   530 begin
   531 
   532 lemma Inf_fin_Inf:
   533   assumes "finite A" and "A \<noteq> {}"
   534   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
   535 proof -
   536   from assms obtain b B where "A = insert b B" and "finite B" by auto
   537   then show ?thesis
   538     by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
   539 qed
   540 
   541 lemma Sup_fin_Sup:
   542   assumes "finite A" and "A \<noteq> {}"
   543   shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
   544 proof -
   545   from assms obtain b B where "A = insert b B" and "finite B" by auto
   546   then show ?thesis
   547     by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
   548 qed
   549 
   550 end
   551 
   552 
   553 subsection {* Minimum and Maximum over non-empty sets *}
   554 
   555 context linorder
   556 begin
   557 
   558 lemma dual_min:
   559   "ord.min greater_eq = max"
   560   by (auto simp add: ord.min_def max_def fun_eq_iff)
   561 
   562 lemma dual_max:
   563   "ord.max greater_eq = min"
   564   by (auto simp add: ord.max_def min_def fun_eq_iff)
   565 
   566 lemma dual_Min:
   567   "linorder.Min greater_eq = Max"
   568 proof -
   569   interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   570   show ?thesis by (simp add: dual.Min_def dual_min Max_def)
   571 qed
   572 
   573 lemma dual_Max:
   574   "linorder.Max greater_eq = Min"
   575 proof -
   576   interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   577   show ?thesis by (simp add: dual.Max_def dual_max Min_def)
   578 qed
   579 
   580 lemmas Min_singleton = Min.singleton
   581 lemmas Max_singleton = Max.singleton
   582 lemmas Min_insert = Min.insert
   583 lemmas Max_insert = Max.insert
   584 lemmas Min_Un = Min.union
   585 lemmas Max_Un = Max.union
   586 lemmas hom_Min_commute = Min.hom_commute
   587 lemmas hom_Max_commute = Max.hom_commute
   588 
   589 lemma Min_in [simp]:
   590   assumes "finite A" and "A \<noteq> {}"
   591   shows "Min A \<in> A"
   592   using assms by (auto simp add: min_def Min.closed)
   593 
   594 lemma Max_in [simp]:
   595   assumes "finite A" and "A \<noteq> {}"
   596   shows "Max A \<in> A"
   597   using assms by (auto simp add: max_def Max.closed)
   598 
   599 lemma Min_le [simp]:
   600   assumes "finite A" and "x \<in> A"
   601   shows "Min A \<le> x"
   602   using assms by (fact Min.coboundedI)
   603 
   604 lemma Max_ge [simp]:
   605   assumes "finite A" and "x \<in> A"
   606   shows "x \<le> Max A"
   607   using assms by (fact Max.coboundedI)
   608 
   609 lemma Min_eqI:
   610   assumes "finite A"
   611   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
   612     and "x \<in> A"
   613   shows "Min A = x"
   614 proof (rule antisym)
   615   from `x \<in> A` have "A \<noteq> {}" by auto
   616   with assms show "Min A \<ge> x" by simp
   617 next
   618   from assms show "x \<ge> Min A" by simp
   619 qed
   620 
   621 lemma Max_eqI:
   622   assumes "finite A"
   623   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
   624     and "x \<in> A"
   625   shows "Max A = x"
   626 proof (rule antisym)
   627   from `x \<in> A` have "A \<noteq> {}" by auto
   628   with assms show "Max A \<le> x" by simp
   629 next
   630   from assms show "x \<le> Max A" by simp
   631 qed
   632 
   633 context
   634   fixes A :: "'a set"
   635   assumes fin_nonempty: "finite A" "A \<noteq> {}"
   636 begin
   637 
   638 lemma Min_ge_iff [simp]:
   639   "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   640   using fin_nonempty by (fact Min.bounded_iff)
   641 
   642 lemma Max_le_iff [simp]:
   643   "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   644   using fin_nonempty by (fact Max.bounded_iff)
   645 
   646 lemma Min_gr_iff [simp]:
   647   "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   648   using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
   649 
   650 lemma Max_less_iff [simp]:
   651   "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   652   using fin_nonempty by (induct rule: finite_ne_induct) simp_all
   653 
   654 lemma Min_le_iff:
   655   "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   656   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
   657 
   658 lemma Max_ge_iff:
   659   "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   660   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
   661 
   662 lemma Min_less_iff:
   663   "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   664   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
   665 
   666 lemma Max_gr_iff:
   667   "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   668   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
   669 
   670 end
   671 
   672 lemma Min_antimono:
   673   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   674   shows "Min N \<le> Min M"
   675   using assms by (fact Min.antimono)
   676 
   677 lemma Max_mono:
   678   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   679   shows "Max M \<le> Max N"
   680   using assms by (fact Max.antimono)
   681 
   682 lemma mono_Min_commute:
   683   assumes "mono f"
   684   assumes "finite A" and "A \<noteq> {}"
   685   shows "f (Min A) = Min (f ` A)"
   686 proof (rule linorder_class.Min_eqI [symmetric])
   687   from `finite A` show "finite (f ` A)" by simp
   688   from assms show "f (Min A) \<in> f ` A" by simp
   689   fix x
   690   assume "x \<in> f ` A"
   691   then obtain y where "y \<in> A" and "x = f y" ..
   692   with assms have "Min A \<le> y" by auto
   693   with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
   694   with `x = f y` show "f (Min A) \<le> x" by simp
   695 qed
   696 
   697 lemma mono_Max_commute:
   698   assumes "mono f"
   699   assumes "finite A" and "A \<noteq> {}"
   700   shows "f (Max A) = Max (f ` A)"
   701 proof (rule linorder_class.Max_eqI [symmetric])
   702   from `finite A` show "finite (f ` A)" by simp
   703   from assms show "f (Max A) \<in> f ` A" by simp
   704   fix x
   705   assume "x \<in> f ` A"
   706   then obtain y where "y \<in> A" and "x = f y" ..
   707   with assms have "y \<le> Max A" by auto
   708   with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
   709   with `x = f y` show "x \<le> f (Max A)" by simp
   710 qed
   711 
   712 lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
   713   assumes fin: "finite A"
   714   and empty: "P {}" 
   715   and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
   716   shows "P A"
   717 using fin empty insert
   718 proof (induct rule: finite_psubset_induct)
   719   case (psubset A)
   720   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 
   721   have fin: "finite A" by fact 
   722   have empty: "P {}" by fact
   723   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
   724   show "P A"
   725   proof (cases "A = {}")
   726     assume "A = {}" 
   727     then show "P A" using `P {}` by simp
   728   next
   729     let ?B = "A - {Max A}" 
   730     let ?A = "insert (Max A) ?B"
   731     have "finite ?B" using `finite A` by simp
   732     assume "A \<noteq> {}"
   733     with `finite A` have "Max A : A" by auto
   734     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
   735     then have "P ?B" using `P {}` step IH [of ?B] by blast
   736     moreover 
   737     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
   738     ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
   739   qed
   740 qed
   741 
   742 lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
   743   "\<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"
   744   by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
   745 
   746 lemma Least_Min:
   747   assumes "finite {a. P a}" and "\<exists>a. P a"
   748   shows "(LEAST a. P a) = Min {a. P a}"
   749 proof -
   750   { fix A :: "'a set"
   751     assume A: "finite A" "A \<noteq> {}"
   752     have "(LEAST a. a \<in> A) = Min A"
   753     using A proof (induct A rule: finite_ne_induct)
   754       case singleton show ?case by (rule Least_equality) simp_all
   755     next
   756       case (insert a A)
   757       have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
   758         by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
   759       with insert show ?case by simp
   760     qed
   761   } from this [of "{a. P a}"] assms show ?thesis by simp
   762 qed
   763 
   764 end
   765 
   766 context linordered_ab_semigroup_add
   767 begin
   768 
   769 lemma add_Min_commute:
   770   fixes k
   771   assumes "finite N" and "N \<noteq> {}"
   772   shows "k + Min N = Min {k + m | m. m \<in> N}"
   773 proof -
   774   have "\<And>x y. k + min x y = min (k + x) (k + y)"
   775     by (simp add: min_def not_le)
   776       (blast intro: antisym less_imp_le add_left_mono)
   777   with assms show ?thesis
   778     using hom_Min_commute [of "plus k" N]
   779     by simp (blast intro: arg_cong [where f = Min])
   780 qed
   781 
   782 lemma add_Max_commute:
   783   fixes k
   784   assumes "finite N" and "N \<noteq> {}"
   785   shows "k + Max N = Max {k + m | m. m \<in> N}"
   786 proof -
   787   have "\<And>x y. k + max x y = max (k + x) (k + y)"
   788     by (simp add: max_def not_le)
   789       (blast intro: antisym less_imp_le add_left_mono)
   790   with assms show ?thesis
   791     using hom_Max_commute [of "plus k" N]
   792     by simp (blast intro: arg_cong [where f = Max])
   793 qed
   794 
   795 end
   796 
   797 context linordered_ab_group_add
   798 begin
   799 
   800 lemma minus_Max_eq_Min [simp]:
   801   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
   802   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
   803 
   804 lemma minus_Min_eq_Max [simp]:
   805   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
   806   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
   807 
   808 end
   809 
   810 context complete_linorder
   811 begin
   812 
   813 lemma Min_Inf:
   814   assumes "finite A" and "A \<noteq> {}"
   815   shows "Min A = Inf A"
   816 proof -
   817   from assms obtain b B where "A = insert b B" and "finite B" by auto
   818   then show ?thesis
   819     by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
   820 qed
   821 
   822 lemma Max_Sup:
   823   assumes "finite A" and "A \<noteq> {}"
   824   shows "Max A = Sup A"
   825 proof -
   826   from assms obtain b B where "A = insert b B" and "finite B" by auto
   827   then show ?thesis
   828     by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
   829 qed
   830 
   831 end
   832 
   833 end