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)
```
```   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)
```
```   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
```