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