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