src/HOL/Lattices_Big.thy
author haftmann
Fri Jun 19 07:53:35 2015 +0200 (2015-06-19)
changeset 60517 f16e4fb20652
parent 59000 6eb0725503fc
child 60758 d8d85a8172b5
permissions -rw-r--r--
separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial
     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 {* 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 lemma infinite: "\<not> finite A \<Longrightarrow> F A = the None"
   129   unfolding eq_fold' by (cases "finite (UNIV::'a set)") (auto intro: finite_subset fold_infinite)
   130 
   131 end
   132 
   133 locale semilattice_order_set = binary?: semilattice_order + semilattice_set
   134 begin
   135 
   136 lemma bounded_iff:
   137   assumes "finite A" and "A \<noteq> {}"
   138   shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
   139   using assms by (induct rule: finite_ne_induct) (simp_all add: bounded_iff)
   140 
   141 lemma boundedI:
   142   assumes "finite A"
   143   assumes "A \<noteq> {}"
   144   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   145   shows "x \<preceq> F A"
   146   using assms by (simp add: bounded_iff)
   147 
   148 lemma boundedE:
   149   assumes "finite A" and "A \<noteq> {}" and "x \<preceq> F A"
   150   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   151   using assms by (simp add: bounded_iff)
   152 
   153 lemma coboundedI:
   154   assumes "finite A"
   155     and "a \<in> A"
   156   shows "F A \<preceq> a"
   157 proof -
   158   from assms have "A \<noteq> {}" by auto
   159   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
   160   proof (induct rule: finite_ne_induct)
   161     case singleton thus ?case by (simp add: refl)
   162   next
   163     case (insert x B)
   164     from insert have "a = x \<or> a \<in> B" by simp
   165     then show ?case using insert by (auto intro: coboundedI2)
   166   qed
   167 qed
   168 
   169 lemma antimono:
   170   assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B"
   171   shows "F B \<preceq> F A"
   172 proof (cases "A = B")
   173   case True then show ?thesis by (simp add: refl)
   174 next
   175   case False
   176   have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
   177   then have "F B = F (A \<union> (B - A))" by simp
   178   also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   179   also have "\<dots> \<preceq> F A" by simp
   180   finally show ?thesis .
   181 qed
   182 
   183 end
   184 
   185 
   186 subsubsection {* With neutral element *}
   187 
   188 locale semilattice_neutr_set = semilattice_neutr
   189 begin
   190 
   191 interpretation comp_fun_idem f
   192   by default (simp_all add: fun_eq_iff left_commute)
   193 
   194 definition F :: "'a set \<Rightarrow> 'a"
   195 where
   196   eq_fold: "F A = Finite_Set.fold f 1 A"
   197 
   198 lemma infinite [simp]:
   199   "\<not> finite A \<Longrightarrow> F A = 1"
   200   by (simp add: eq_fold)
   201 
   202 lemma empty [simp]:
   203   "F {} = 1"
   204   by (simp add: eq_fold)
   205 
   206 lemma insert [simp]:
   207   assumes "finite A"
   208   shows "F (insert x A) = x * F A"
   209   using assms by (simp add: eq_fold)
   210 
   211 lemma in_idem:
   212   assumes "finite A" and "x \<in> A"
   213   shows "x * F A = F A"
   214 proof -
   215   from assms have "A \<noteq> {}" by auto
   216   with `finite A` show ?thesis using `x \<in> A`
   217     by (induct A rule: finite_ne_induct) (auto simp add: ac_simps)
   218 qed
   219 
   220 lemma union:
   221   assumes "finite A" and "finite B"
   222   shows "F (A \<union> B) = F A * F B"
   223   using assms by (induct A) (simp_all add: ac_simps)
   224 
   225 lemma remove:
   226   assumes "finite A" and "x \<in> A"
   227   shows "F A = x * F (A - {x})"
   228 proof -
   229   from assms obtain B where "A = insert x B" and "x \<notin> B" by (blast dest: mk_disjoint_insert)
   230   with assms show ?thesis by simp
   231 qed
   232 
   233 lemma insert_remove:
   234   assumes "finite A"
   235   shows "F (insert x A) = x * F (A - {x})"
   236   using assms by (cases "x \<in> A") (simp_all add: insert_absorb remove)
   237 
   238 lemma subset:
   239   assumes "finite A" and "B \<subseteq> A"
   240   shows "F B * F A = F A"
   241 proof -
   242   from assms have "finite B" by (auto dest: finite_subset)
   243   with assms show ?thesis by (simp add: union [symmetric] Un_absorb1)
   244 qed
   245 
   246 lemma closed:
   247   assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x * y \<in> {x, y}"
   248   shows "F A \<in> A"
   249 using `finite A` `A \<noteq> {}` proof (induct rule: finite_ne_induct)
   250   case singleton then show ?case by simp
   251 next
   252   case insert with elem show ?case by force
   253 qed
   254 
   255 end
   256 
   257 locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set
   258 begin
   259 
   260 lemma bounded_iff:
   261   assumes "finite A"
   262   shows "x \<preceq> F A \<longleftrightarrow> (\<forall>a\<in>A. x \<preceq> a)"
   263   using assms by (induct A) (simp_all add: bounded_iff)
   264 
   265 lemma boundedI:
   266   assumes "finite A"
   267   assumes "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   268   shows "x \<preceq> F A"
   269   using assms by (simp add: bounded_iff)
   270 
   271 lemma boundedE:
   272   assumes "finite A" and "x \<preceq> F A"
   273   obtains "\<And>a. a \<in> A \<Longrightarrow> x \<preceq> a"
   274   using assms by (simp add: bounded_iff)
   275 
   276 lemma coboundedI:
   277   assumes "finite A"
   278     and "a \<in> A"
   279   shows "F A \<preceq> a"
   280 proof -
   281   from assms have "A \<noteq> {}" by auto
   282   from `finite A` `A \<noteq> {}` `a \<in> A` show ?thesis
   283   proof (induct rule: finite_ne_induct)
   284     case singleton thus ?case by (simp add: refl)
   285   next
   286     case (insert x B)
   287     from insert have "a = x \<or> a \<in> B" by simp
   288     then show ?case using insert by (auto intro: coboundedI2)
   289   qed
   290 qed
   291 
   292 lemma antimono:
   293   assumes "A \<subseteq> B" and "finite B"
   294   shows "F B \<preceq> F A"
   295 proof (cases "A = B")
   296   case True then show ?thesis by (simp add: refl)
   297 next
   298   case False
   299   have B: "B = A \<union> (B - A)" using `A \<subseteq> B` by blast
   300   then have "F B = F (A \<union> (B - A))" by simp
   301   also have "\<dots> = F A * F (B - A)" using False assms by (subst union) (auto intro: finite_subset)
   302   also have "\<dots> \<preceq> F A" by simp
   303   finally show ?thesis .
   304 qed
   305 
   306 end
   307 
   308 notation times (infixl "*" 70)
   309 notation Groups.one ("1")
   310 
   311 
   312 subsection {* Lattice operations on finite sets *}
   313 
   314 context semilattice_inf
   315 begin
   316 
   317 definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
   318 where
   319   "Inf_fin = semilattice_set.F inf"
   320 
   321 sublocale Inf_fin!: semilattice_order_set inf less_eq less
   322 where
   323   "semilattice_set.F inf = Inf_fin"
   324 proof -
   325   show "semilattice_order_set inf less_eq less" ..
   326   then interpret Inf_fin!: semilattice_order_set inf less_eq less .
   327   from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
   328 qed
   329 
   330 end
   331 
   332 context semilattice_sup
   333 begin
   334 
   335 definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
   336 where
   337   "Sup_fin = semilattice_set.F sup"
   338 
   339 sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
   340 where
   341   "semilattice_set.F sup = Sup_fin"
   342 proof -
   343   show "semilattice_order_set sup greater_eq greater" ..
   344   then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
   345   from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
   346 qed
   347 
   348 end
   349 
   350 
   351 subsection {* Infimum and Supremum over non-empty sets *}
   352 
   353 context lattice
   354 begin
   355 
   356 lemma Inf_fin_le_Sup_fin [simp]: 
   357   assumes "finite A" and "A \<noteq> {}"
   358   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA"
   359 proof -
   360   from `A \<noteq> {}` obtain a where "a \<in> A" by blast
   361   with `finite A` have "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<le> a" by (rule Inf_fin.coboundedI)
   362   moreover from `finite A` `a \<in> A` have "a \<le> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA" by (rule Sup_fin.coboundedI)
   363   ultimately show ?thesis by (rule order_trans)
   364 qed
   365 
   366 lemma sup_Inf_absorb [simp]:
   367   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> \<Sqinter>\<^sub>f\<^sub>i\<^sub>nA \<squnion> a = a"
   368   by (rule sup_absorb2) (rule Inf_fin.coboundedI)
   369 
   370 lemma inf_Sup_absorb [simp]:
   371   "finite A \<Longrightarrow> a \<in> A \<Longrightarrow> a \<sqinter> \<Squnion>\<^sub>f\<^sub>i\<^sub>nA = a"
   372   by (rule inf_absorb1) (rule Sup_fin.coboundedI)
   373 
   374 end
   375 
   376 context distrib_lattice
   377 begin
   378 
   379 lemma sup_Inf1_distrib:
   380   assumes "finite A"
   381     and "A \<noteq> {}"
   382   shows "sup x (\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA) = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n{sup x a|a. a \<in> A}"
   383 using assms by (simp add: image_def Inf_fin.hom_commute [where h="sup x", OF sup_inf_distrib1])
   384   (rule arg_cong [where f="Inf_fin"], blast)
   385 
   386 lemma sup_Inf2_distrib:
   387   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   388   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}"
   389 using A proof (induct rule: finite_ne_induct)
   390   case singleton then show ?case
   391     by (simp add: sup_Inf1_distrib [OF B])
   392 next
   393   case (insert x A)
   394   have finB: "finite {sup x b |b. b \<in> B}"
   395     by (rule finite_surj [where f = "sup x", OF B(1)], auto)
   396   have finAB: "finite {sup a b |a b. a \<in> A \<and> b \<in> B}"
   397   proof -
   398     have "{sup a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {sup a b})"
   399       by blast
   400     thus ?thesis by(simp add: insert(1) B(1))
   401   qed
   402   have ne: "{sup a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   403   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)"
   404     using insert by simp
   405   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)
   406   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})"
   407     using insert by(simp add:sup_Inf1_distrib[OF B])
   408   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})"
   409     (is "_ = \<Sqinter>\<^sub>f\<^sub>i\<^sub>n?M")
   410     using B insert
   411     by (simp add: Inf_fin.union [OF finB _ finAB ne])
   412   also have "?M = {sup a b |a b. a \<in> insert x A \<and> b \<in> B}"
   413     by blast
   414   finally show ?case .
   415 qed
   416 
   417 lemma inf_Sup1_distrib:
   418   assumes "finite A" and "A \<noteq> {}"
   419   shows "inf x (\<Squnion>\<^sub>f\<^sub>i\<^sub>nA) = \<Squnion>\<^sub>f\<^sub>i\<^sub>n{inf x a|a. a \<in> A}"
   420 using assms by (simp add: image_def Sup_fin.hom_commute [where h="inf x", OF inf_sup_distrib1])
   421   (rule arg_cong [where f="Sup_fin"], blast)
   422 
   423 lemma inf_Sup2_distrib:
   424   assumes A: "finite A" "A \<noteq> {}" and B: "finite B" "B \<noteq> {}"
   425   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}"
   426 using A proof (induct rule: finite_ne_induct)
   427   case singleton thus ?case
   428     by(simp add: inf_Sup1_distrib [OF B])
   429 next
   430   case (insert x A)
   431   have finB: "finite {inf x b |b. b \<in> B}"
   432     by(rule finite_surj[where f = "%b. inf x b", OF B(1)], auto)
   433   have finAB: "finite {inf a b |a b. a \<in> A \<and> b \<in> B}"
   434   proof -
   435     have "{inf a b |a b. a \<in> A \<and> b \<in> B} = (UN a:A. UN b:B. {inf a b})"
   436       by blast
   437     thus ?thesis by(simp add: insert(1) B(1))
   438   qed
   439   have ne: "{inf a b |a b. a \<in> A \<and> b \<in> B} \<noteq> {}" using insert B by blast
   440   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)"
   441     using insert by simp
   442   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)
   443   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})"
   444     using insert by(simp add:inf_Sup1_distrib[OF B])
   445   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})"
   446     (is "_ = \<Squnion>\<^sub>f\<^sub>i\<^sub>n?M")
   447     using B insert
   448     by (simp add: Sup_fin.union [OF finB _ finAB ne])
   449   also have "?M = {inf a b |a b. a \<in> insert x A \<and> b \<in> B}"
   450     by blast
   451   finally show ?case .
   452 qed
   453 
   454 end
   455 
   456 context complete_lattice
   457 begin
   458 
   459 lemma Inf_fin_Inf:
   460   assumes "finite A" and "A \<noteq> {}"
   461   shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = \<Sqinter>A"
   462 proof -
   463   from assms obtain b B where "A = insert b B" and "finite B" by auto
   464   then show ?thesis
   465     by (simp add: Inf_fin.eq_fold inf_Inf_fold_inf inf.commute [of b])
   466 qed
   467 
   468 lemma Sup_fin_Sup:
   469   assumes "finite A" and "A \<noteq> {}"
   470   shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = \<Squnion>A"
   471 proof -
   472   from assms obtain b B where "A = insert b B" and "finite B" by auto
   473   then show ?thesis
   474     by (simp add: Sup_fin.eq_fold sup_Sup_fold_sup sup.commute [of b])
   475 qed
   476 
   477 end
   478 
   479 
   480 subsection {* Minimum and Maximum over non-empty sets *}
   481 
   482 context linorder
   483 begin
   484 
   485 definition Min :: "'a set \<Rightarrow> 'a"
   486 where
   487   "Min = semilattice_set.F min"
   488 
   489 definition Max :: "'a set \<Rightarrow> 'a"
   490 where
   491   "Max = semilattice_set.F max"
   492 
   493 sublocale Min!: semilattice_order_set min less_eq less
   494   + Max!: semilattice_order_set max greater_eq greater
   495 where
   496   "semilattice_set.F min = Min"
   497   and "semilattice_set.F max = Max"
   498 proof -
   499   show "semilattice_order_set min less_eq less" by default (auto simp add: min_def)
   500   then interpret Min!: semilattice_order_set min less_eq less .
   501   show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def)
   502   then interpret Max!: semilattice_order_set max greater_eq greater .
   503   from Min_def show "semilattice_set.F min = Min" by rule
   504   from Max_def show "semilattice_set.F max = Max" by rule
   505 qed
   506 
   507 end
   508 
   509 text {* An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin} *}
   510 
   511 lemma Inf_fin_Min:
   512   "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)"
   513   by (simp add: Inf_fin_def Min_def inf_min)
   514 
   515 lemma Sup_fin_Max:
   516   "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)"
   517   by (simp add: Sup_fin_def Max_def sup_max)
   518 
   519 context linorder
   520 begin
   521 
   522 lemma dual_min:
   523   "ord.min greater_eq = max"
   524   by (auto simp add: ord.min_def max_def fun_eq_iff)
   525 
   526 lemma dual_max:
   527   "ord.max greater_eq = min"
   528   by (auto simp add: ord.max_def min_def fun_eq_iff)
   529 
   530 lemma dual_Min:
   531   "linorder.Min greater_eq = Max"
   532 proof -
   533   interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   534   show ?thesis by (simp add: dual.Min_def dual_min Max_def)
   535 qed
   536 
   537 lemma dual_Max:
   538   "linorder.Max greater_eq = Min"
   539 proof -
   540   interpret dual!: linorder greater_eq greater by (fact dual_linorder)
   541   show ?thesis by (simp add: dual.Max_def dual_max Min_def)
   542 qed
   543 
   544 lemmas Min_singleton = Min.singleton
   545 lemmas Max_singleton = Max.singleton
   546 lemmas Min_insert = Min.insert
   547 lemmas Max_insert = Max.insert
   548 lemmas Min_Un = Min.union
   549 lemmas Max_Un = Max.union
   550 lemmas hom_Min_commute = Min.hom_commute
   551 lemmas hom_Max_commute = Max.hom_commute
   552 
   553 lemma Min_in [simp]:
   554   assumes "finite A" and "A \<noteq> {}"
   555   shows "Min A \<in> A"
   556   using assms by (auto simp add: min_def Min.closed)
   557 
   558 lemma Max_in [simp]:
   559   assumes "finite A" and "A \<noteq> {}"
   560   shows "Max A \<in> A"
   561   using assms by (auto simp add: max_def Max.closed)
   562 
   563 lemma Min_insert2:
   564   assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b"
   565   shows "Min (insert a A) = a"
   566 proof (cases "A = {}")
   567   case True then show ?thesis by simp
   568 next
   569   case False with `finite A` have "Min (insert a A) = min a (Min A)"
   570     by simp
   571   moreover from `finite A` `A \<noteq> {}` min have "a \<le> Min A" by simp
   572   ultimately show ?thesis by (simp add: min.absorb1)
   573 qed
   574 
   575 lemma Max_insert2:
   576   assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a"
   577   shows "Max (insert a A) = a"
   578 proof (cases "A = {}")
   579   case True then show ?thesis by simp
   580 next
   581   case False with `finite A` have "Max (insert a A) = max a (Max A)"
   582     by simp
   583   moreover from `finite A` `A \<noteq> {}` max have "Max A \<le> a" by simp
   584   ultimately show ?thesis by (simp add: max.absorb1)
   585 qed
   586 
   587 lemma Min_le [simp]:
   588   assumes "finite A" and "x \<in> A"
   589   shows "Min A \<le> x"
   590   using assms by (fact Min.coboundedI)
   591 
   592 lemma Max_ge [simp]:
   593   assumes "finite A" and "x \<in> A"
   594   shows "x \<le> Max A"
   595   using assms by (fact Max.coboundedI)
   596 
   597 lemma Min_eqI:
   598   assumes "finite A"
   599   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
   600     and "x \<in> A"
   601   shows "Min A = x"
   602 proof (rule antisym)
   603   from `x \<in> A` have "A \<noteq> {}" by auto
   604   with assms show "Min A \<ge> x" by simp
   605 next
   606   from assms show "x \<ge> Min A" by simp
   607 qed
   608 
   609 lemma Max_eqI:
   610   assumes "finite A"
   611   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
   612     and "x \<in> A"
   613   shows "Max A = x"
   614 proof (rule antisym)
   615   from `x \<in> A` have "A \<noteq> {}" by auto
   616   with assms show "Max A \<le> x" by simp
   617 next
   618   from assms show "x \<le> Max A" by simp
   619 qed
   620 
   621 context
   622   fixes A :: "'a set"
   623   assumes fin_nonempty: "finite A" "A \<noteq> {}"
   624 begin
   625 
   626 lemma Min_ge_iff [simp]:
   627   "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
   628   using fin_nonempty by (fact Min.bounded_iff)
   629 
   630 lemma Max_le_iff [simp]:
   631   "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
   632   using fin_nonempty by (fact Max.bounded_iff)
   633 
   634 lemma Min_gr_iff [simp]:
   635   "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
   636   using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
   637 
   638 lemma Max_less_iff [simp]:
   639   "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
   640   using fin_nonempty by (induct rule: finite_ne_induct) simp_all
   641 
   642 lemma Min_le_iff:
   643   "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
   644   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
   645 
   646 lemma Max_ge_iff:
   647   "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
   648   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
   649 
   650 lemma Min_less_iff:
   651   "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
   652   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
   653 
   654 lemma Max_gr_iff:
   655   "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
   656   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
   657 
   658 end
   659 
   660 lemma Max_eq_if:
   661   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"
   662   shows "Max A = Max B"
   663 proof cases
   664   assume "A = {}" thus ?thesis using assms by simp
   665 next
   666   assume "A \<noteq> {}" thus ?thesis using assms
   667     by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2])
   668 qed
   669 
   670 lemma Min_antimono:
   671   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   672   shows "Min N \<le> Min M"
   673   using assms by (fact Min.antimono)
   674 
   675 lemma Max_mono:
   676   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
   677   shows "Max M \<le> Max N"
   678   using assms by (fact Max.antimono)
   679 
   680 end
   681 
   682 context linorder  (* FIXME *)
   683 begin
   684 
   685 lemma mono_Min_commute:
   686   assumes "mono f"
   687   assumes "finite A" and "A \<noteq> {}"
   688   shows "f (Min A) = Min (f ` A)"
   689 proof (rule linorder_class.Min_eqI [symmetric])
   690   from `finite A` show "finite (f ` A)" by simp
   691   from assms show "f (Min A) \<in> f ` A" by simp
   692   fix x
   693   assume "x \<in> f ` A"
   694   then obtain y where "y \<in> A" and "x = f y" ..
   695   with assms have "Min A \<le> y" by auto
   696   with `mono f` have "f (Min A) \<le> f y" by (rule monoE)
   697   with `x = f y` show "f (Min A) \<le> x" by simp
   698 qed
   699 
   700 lemma mono_Max_commute:
   701   assumes "mono f"
   702   assumes "finite A" and "A \<noteq> {}"
   703   shows "f (Max A) = Max (f ` A)"
   704 proof (rule linorder_class.Max_eqI [symmetric])
   705   from `finite A` show "finite (f ` A)" by simp
   706   from assms show "f (Max A) \<in> f ` A" by simp
   707   fix x
   708   assume "x \<in> f ` A"
   709   then obtain y where "y \<in> A" and "x = f y" ..
   710   with assms have "y \<le> Max A" by auto
   711   with `mono f` have "f y \<le> f (Max A)" by (rule monoE)
   712   with `x = f y` show "x \<le> f (Max A)" by simp
   713 qed
   714 
   715 lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
   716   assumes fin: "finite A"
   717   and empty: "P {}" 
   718   and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
   719   shows "P A"
   720 using fin empty insert
   721 proof (induct rule: finite_psubset_induct)
   722   case (psubset A)
   723   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 
   724   have fin: "finite A" by fact 
   725   have empty: "P {}" by fact
   726   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
   727   show "P A"
   728   proof (cases "A = {}")
   729     assume "A = {}" 
   730     then show "P A" using `P {}` by simp
   731   next
   732     let ?B = "A - {Max A}" 
   733     let ?A = "insert (Max A) ?B"
   734     have "finite ?B" using `finite A` by simp
   735     assume "A \<noteq> {}"
   736     with `finite A` have "Max A : A" by auto
   737     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
   738     then have "P ?B" using `P {}` step IH [of ?B] by blast
   739     moreover 
   740     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF `finite A`] by fastforce
   741     ultimately show "P A" using A insert_Diff_single step [OF `finite ?B`] by fastforce
   742   qed
   743 qed
   744 
   745 lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
   746   "\<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"
   747   by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
   748 
   749 lemma Least_Min:
   750   assumes "finite {a. P a}" and "\<exists>a. P a"
   751   shows "(LEAST a. P a) = Min {a. P a}"
   752 proof -
   753   { fix A :: "'a set"
   754     assume A: "finite A" "A \<noteq> {}"
   755     have "(LEAST a. a \<in> A) = Min A"
   756     using A proof (induct A rule: finite_ne_induct)
   757       case singleton show ?case by (rule Least_equality) simp_all
   758     next
   759       case (insert a A)
   760       have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
   761         by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
   762       with insert show ?case by simp
   763     qed
   764   } from this [of "{a. P a}"] assms show ?thesis by simp
   765 qed
   766 
   767 lemma infinite_growing:
   768   assumes "X \<noteq> {}"
   769   assumes *: "\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>X. y > x"
   770   shows "\<not> finite X"
   771 proof
   772   assume "finite X"
   773   with `X \<noteq> {}` have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X"
   774     by auto
   775   with *[of "Max X"] show False
   776     by auto
   777 qed
   778 
   779 end
   780 
   781 context linordered_ab_semigroup_add
   782 begin
   783 
   784 lemma add_Min_commute:
   785   fixes k
   786   assumes "finite N" and "N \<noteq> {}"
   787   shows "k + Min N = Min {k + m | m. m \<in> N}"
   788 proof -
   789   have "\<And>x y. k + min x y = min (k + x) (k + y)"
   790     by (simp add: min_def not_le)
   791       (blast intro: antisym less_imp_le add_left_mono)
   792   with assms show ?thesis
   793     using hom_Min_commute [of "plus k" N]
   794     by simp (blast intro: arg_cong [where f = Min])
   795 qed
   796 
   797 lemma add_Max_commute:
   798   fixes k
   799   assumes "finite N" and "N \<noteq> {}"
   800   shows "k + Max N = Max {k + m | m. m \<in> N}"
   801 proof -
   802   have "\<And>x y. k + max x y = max (k + x) (k + y)"
   803     by (simp add: max_def not_le)
   804       (blast intro: antisym less_imp_le add_left_mono)
   805   with assms show ?thesis
   806     using hom_Max_commute [of "plus k" N]
   807     by simp (blast intro: arg_cong [where f = Max])
   808 qed
   809 
   810 end
   811 
   812 context linordered_ab_group_add
   813 begin
   814 
   815 lemma minus_Max_eq_Min [simp]:
   816   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
   817   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
   818 
   819 lemma minus_Min_eq_Max [simp]:
   820   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
   821   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
   822 
   823 end
   824 
   825 context complete_linorder
   826 begin
   827 
   828 lemma Min_Inf:
   829   assumes "finite A" and "A \<noteq> {}"
   830   shows "Min A = Inf A"
   831 proof -
   832   from assms obtain b B where "A = insert b B" and "finite B" by auto
   833   then show ?thesis
   834     by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
   835 qed
   836 
   837 lemma Max_Sup:
   838   assumes "finite A" and "A \<noteq> {}"
   839   shows "Max A = Sup A"
   840 proof -
   841   from assms obtain b B where "A = insert b B" and "finite B" by auto
   842   then show ?thesis
   843     by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
   844 qed
   845 
   846 end
   847 
   848 end