src/HOL/Lattices_Big.thy
author haftmann
Wed Dec 25 17:39:06 2013 +0100 (2013-12-25)
changeset 54863 82acc20ded73
parent 54857 5c05f7c5f8ae
child 54864 a064732223ad
permissions -rw-r--r--
prefer more canonical names for lemmas on min/max
     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 = binary?: 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 = binary?: 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 = max.cobounded1
   375 lemmas le_maxI2 = max.cobounded2
   376 lemmas min_ac = min.assoc min.commute min.left_commute
   377 lemmas max_ac = max.assoc max.commute max.left_commute
   378 
   379 end
   380 
   381 
   382 text {* Lattice operations proper *}
   383 
   384 sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
   385 where
   386   "semilattice_set.F inf = Inf_fin"
   387 proof -
   388   show "semilattice_order_set inf less_eq less" ..
   389   then interpret Inf_fin!: semilattice_order_set inf less_eq less .
   390   from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
   391 qed
   392 
   393 sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
   394 where
   395   "semilattice_set.F sup = Sup_fin"
   396 proof -
   397   show "semilattice_order_set sup greater_eq greater" ..
   398   then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
   399   from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
   400 qed
   401 
   402 
   403 text {* An aside again: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
   404 
   405 lemma Inf_fin_Min:
   406   "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
   407   by (simp add: Inf_fin_def Min_def inf_min)
   408 
   409 lemma Sup_fin_Max:
   410   "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
   411   by (simp add: Sup_fin_def Max_def sup_max)
   412 
   413 
   414 
   415 subsection {* Infimum and Supremum over non-empty sets *}
   416 
   417 text {*
   418   After this non-regular bootstrap, things continue canonically.
   419 *}
   420 
   421 context lattice
   422 begin
   423 
   424 lemma Inf_fin_le_Sup_fin [simp]: 
   425   assumes "finite A" and "A \<noteq> {}"
   426   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
   427 proof -
   428   from `A \<noteq> {}` obtain a where "a \<in> A" by blast
   429   with `finite A` have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
   430   moreover from `finite A` `a \<in> A` have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
   431   ultimately show ?thesis by (rule order_trans)
   432 qed
   433 
   434 lemma sup_Inf_absorb [simp]:
   435   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a"
   436   by (rule sup_absorb2) (rule Inf_fin.coboundedI)
   437 
   438 lemma inf_Sup_absorb [simp]:
   439   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a"
   440   by (rule inf_absorb1) (rule Sup_fin.coboundedI)
   441 
   442 end
   443 
   444 context distrib_lattice
   445 begin
   446 
   447 lemma sup_Inf1_distrib:
   448   assumes "finite A"
   449     and "A \<noteq> {}"
   450   shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
   451 using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
   452   (rule arg_cong [where f="Inf_fin"], blast)
   453 
   454 lemma sup_Inf2_distrib:
   455   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   456   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}"
   457 using A proof (induct rule: finite_ne_induct)
   458   case singleton then show ?case
   459     by (simp add: sup_Inf1_distrib [OF B])
   460 next
   461   case (insert x A)
   462   have finB: "finite {sup x b |b. b \<in> B}"
   463     by (rule finite_surj [where f = "sup x", OF B(1)], auto)
   464   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
   465   proof -
   466     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
   467       by blast
   468     thus ?thesis by(simp add: insert(1) B(1))
   469   qed
   470   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   471   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)"
   472     using insert by simp
   473   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)
   474   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})"
   475     using insert by(simp add:sup_Inf1_distrib[OF B])
   476   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})"
   477     (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
   478     using B insert
   479     by (simp add: Inf_fin.union [OF finB _ finAB ne])
   480   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
   481     by blast
   482   finally show ?case .
   483 qed
   484 
   485 lemma inf_Sup1_distrib:
   486   assumes "finite A" and "A \<noteq> {}"
   487   shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
   488 using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
   489   (rule arg_cong [where f="Sup_fin"], blast)
   490 
   491 lemma inf_Sup2_distrib:
   492   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   493   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}"
   494 using A proof (induct rule: finite_ne_induct)
   495   case singleton thus ?case
   496     by(simp add: inf_Sup1_distrib [OF B])
   497 next
   498   case (insert x A)
   499   have finB: "finite {inf x b |b. b \<in> B}"
   500     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
   501   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
   502   proof -
   503     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
   504       by blast
   505     thus ?thesis by(simp add: insert(1) B(1))
   506   qed
   507   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   508   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)"
   509     using insert by simp
   510   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)
   511   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})"
   512     using insert by(simp add:inf_Sup1_distrib[OF B])
   513   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})"
   514     (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
   515     using B insert
   516     by (simp add: Sup_fin.union [OF finB _ finAB ne])
   517   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
   518     by blast
   519   finally show ?case .
   520 qed
   521 
   522 end
   523 
   524 context complete_lattice
   525 begin
   526 
   527 lemma Inf_fin_Inf:
   528   assumes "finite A" and "A \<noteq> {}"
   529   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
   530 proof -
   531   from assms obtain b B where "A = insert b B" and "finite B" by auto
   532   then show ?thesis
   533     by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
   534 qed
   535 
   536 lemma Sup_fin_Sup:
   537   assumes "finite A" and "A \<noteq> {}"
   538   shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
   539 proof -
   540   from assms obtain b B where "A = insert b B" and "finite B" by auto
   541   then show ?thesis
   542     by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
   543 qed
   544 
   545 end
   546 
   547 
   548 subsection {* Minimum and Maximum over non-empty sets *}
   549 
   550 context linorder
   551 begin
   552 
   553 lemma dual_min:
   554   "ord.min greater_eq = max"
   555   by (auto simp add: ord.min_def max_def fun_eq_iff)
   556 
   557 lemma dual_max:
   558   "ord.max greater_eq = min"
   559   by (auto simp add: ord.max_def min_def fun_eq_iff)
   560 
   561 lemma dual_Min:
   562   "linorder.Min greater_eq = Max"
   563 proof -
   564   interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   565   show ?thesis by (simp add: dual.Min_def dual_min Max_def)
   566 qed
   567 
   568 lemma dual_Max:
   569   "linorder.Max greater_eq = Min"
   570 proof -
   571   interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   572   show ?thesis by (simp add: dual.Max_def dual_max Min_def)
   573 qed
   574 
   575 lemmas Min_singleton = Min.singleton
   576 lemmas Max_singleton = Max.singleton
   577 lemmas Min_insert = Min.insert
   578 lemmas Max_insert = Max.insert
   579 lemmas Min_Un = Min.union
   580 lemmas Max_Un = Max.union
   581 lemmas hom_Min_commute = Min.hom_commute
   582 lemmas hom_Max_commute = Max.hom_commute
   583 
   584 lemma Min_in [simp]:
   585   assumes "finite A" and "A \<noteq> {}"
   586   shows "Min A \<in> A"
   587   using assms by (auto simp add: min_def Min.closed)
   588 
   589 lemma Max_in [simp]:
   590   assumes "finite A" and "A \<noteq> {}"
   591   shows "Max A \<in> A"
   592   using assms by (auto simp add: max_def Max.closed)
   593 
   594 lemma Min_le [simp]:
   595   assumes "finite A" and "x \<in> A"
   596   shows "Min A \<le> x"
   597   using assms by (fact Min.coboundedI)
   598 
   599 lemma Max_ge [simp]:
   600   assumes "finite A" and "x \<in> A"
   601   shows "x \<le> Max A"
   602   using assms by (fact Max.coboundedI)
   603 
   604 lemma Min_eqI:
   605   assumes "finite A"
   606   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
   607     and "x \<in> A"
   608   shows "Min A = x"
   609 proof (rule antisym)
   610   from `x \<in> A` have "A \<noteq> {}" by auto
   611   with assms show "Min A \<ge> x" by simp
   612 next
   613   from assms show "x \<ge> Min A" by simp
   614 qed
   615 
   616 lemma Max_eqI:
   617   assumes "finite A"
   618   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
   619     and "x \<in> A"
   620   shows "Max A = x"
   621 proof (rule antisym)
   622   from `x \<in> A` have "A \<noteq> {}" by auto
   623   with assms show "Max A \<le> x" by simp
   624 next
   625   from assms show "x \<le> Max A" by simp
   626 qed
   627 
   628 context
   629   fixes A :: "'a set"
   630   assumes fin_nonempty: "finite A" "A \<noteq> {}"
   631 begin
   632 
   633 lemma Min_ge_iff [simp]:
   634   "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   635   using fin_nonempty by (fact Min.bounded_iff)
   636 
   637 lemma Max_le_iff [simp]:
   638   "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   639   using fin_nonempty by (fact Max.bounded_iff)
   640 
   641 lemma Min_gr_iff [simp]:
   642   "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   643   using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
   644 
   645 lemma Max_less_iff [simp]:
   646   "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   647   using fin_nonempty by (induct rule: finite_ne_induct) simp_all
   648 
   649 lemma Min_le_iff:
   650   "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   651   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
   652 
   653 lemma Max_ge_iff:
   654   "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   655   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
   656 
   657 lemma Min_less_iff:
   658   "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   659   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
   660 
   661 lemma Max_gr_iff:
   662   "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   663   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
   664 
   665 end
   666 
   667 lemma Min_antimono:
   668   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   669   shows "Min N \<le> Min M"
   670   using assms by (fact Min.antimono)
   671 
   672 lemma Max_mono:
   673   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   674   shows "Max M \<le> Max N"
   675   using assms by (fact Max.antimono)
   676 
   677 lemma mono_Min_commute:
   678   assumes "mono f"
   679   assumes "finite A" and "A \<noteq> {}"
   680   shows "f (Min A) = Min (f ` A)"
   681 proof (rule linorder_class.Min_eqI [symmetric])
   682   from `finite A` show "finite (f ` A)" by simp
   683   from assms show "f (Min A) \<in> f ` A" by simp
   684   fix x
   685   assume "x \<in> f ` A"
   686   then obtain y where "y \<in> A" and "x = f y" ..
   687   with assms have "Min A \<le> y" by auto
   688   with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
   689   with `x = f y` show "f (Min A) \<le> x" by simp
   690 qed
   691 
   692 lemma mono_Max_commute:
   693   assumes "mono f"
   694   assumes "finite A" and "A \<noteq> {}"
   695   shows "f (Max A) = Max (f ` A)"
   696 proof (rule linorder_class.Max_eqI [symmetric])
   697   from `finite A` show "finite (f ` A)" by simp
   698   from assms show "f (Max A) \<in> f ` A" by simp
   699   fix x
   700   assume "x \<in> f ` A"
   701   then obtain y where "y \<in> A" and "x = f y" ..
   702   with assms have "y \<le> Max A" by auto
   703   with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
   704   with `x = f y` show "x \<le> f (Max A)" by simp
   705 qed
   706 
   707 lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
   708   assumes fin: "finite A"
   709   and empty: "P {}" 
   710   and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
   711   shows "P A"
   712 using fin empty insert
   713 proof (induct rule: finite_psubset_induct)
   714   case (psubset A)
   715   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 
   716   have fin: "finite A" by fact 
   717   have empty: "P {}" by fact
   718   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
   719   show "P A"
   720   proof (cases "A = {}")
   721     assume "A = {}" 
   722     then show "P A" using `P {}` by simp
   723   next
   724     let ?B = "A - {Max A}" 
   725     let ?A = "insert (Max A) ?B"
   726     have "finite ?B" using `finite A` by simp
   727     assume "A \<noteq> {}"
   728     with `finite A` have "Max A : A" by auto
   729     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
   730     then have "P ?B" using `P {}` step IH [of ?B] by blast
   731     moreover 
   732     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
   733     ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
   734   qed
   735 qed
   736 
   737 lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
   738   "\<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"
   739   by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
   740 
   741 lemma Least_Min:
   742   assumes "finite {a. P a}" and "\<exists>a. P a"
   743   shows "(LEAST a. P a) = Min {a. P a}"
   744 proof -
   745   { fix A :: "'a set"
   746     assume A: "finite A" "A \<noteq> {}"
   747     have "(LEAST a. a \<in> A) = Min A"
   748     using A proof (induct A rule: finite_ne_induct)
   749       case singleton show ?case by (rule Least_equality) simp_all
   750     next
   751       case (insert a A)
   752       have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
   753         by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
   754       with insert show ?case by simp
   755     qed
   756   } from this [of "{a. P a}"] assms show ?thesis by simp
   757 qed
   758 
   759 end
   760 
   761 context linordered_ab_semigroup_add
   762 begin
   763 
   764 lemma add_Min_commute:
   765   fixes k
   766   assumes "finite N" and "N \<noteq> {}"
   767   shows "k + Min N = Min {k + m | m. m \<in> N}"
   768 proof -
   769   have "\<And>x y. k + min x y = min (k + x) (k + y)"
   770     by (simp add: min_def not_le)
   771       (blast intro: antisym less_imp_le add_left_mono)
   772   with assms show ?thesis
   773     using hom_Min_commute [of "plus k" N]
   774     by simp (blast intro: arg_cong [where f = Min])
   775 qed
   776 
   777 lemma add_Max_commute:
   778   fixes k
   779   assumes "finite N" and "N \<noteq> {}"
   780   shows "k + Max N = Max {k + m | m. m \<in> N}"
   781 proof -
   782   have "\<And>x y. k + max x y = max (k + x) (k + y)"
   783     by (simp add: max_def not_le)
   784       (blast intro: antisym less_imp_le add_left_mono)
   785   with assms show ?thesis
   786     using hom_Max_commute [of "plus k" N]
   787     by simp (blast intro: arg_cong [where f = Max])
   788 qed
   789 
   790 end
   791 
   792 context linordered_ab_group_add
   793 begin
   794 
   795 lemma minus_Max_eq_Min [simp]:
   796   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
   797   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
   798 
   799 lemma minus_Min_eq_Max [simp]:
   800   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
   801   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
   802 
   803 end
   804 
   805 context complete_linorder
   806 begin
   807 
   808 lemma Min_Inf:
   809   assumes "finite A" and "A \<noteq> {}"
   810   shows "Min A = Inf A"
   811 proof -
   812   from assms obtain b B where "A = insert b B" and "finite B" by auto
   813   then show ?thesis
   814     by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
   815 qed
   816 
   817 lemma Max_Sup:
   818   assumes "finite A" and "A \<noteq> {}"
   819   shows "Max A = Sup A"
   820 proof -
   821   from assms obtain b B where "A = insert b B" and "finite B" by auto
   822   then show ?thesis
   823     by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
   824 qed
   825 
   826 end
   827 
   828 end