src/HOL/Lattices_Big.thy
 author blanchet Tue Nov 07 15:16:42 2017 +0100 (19 months ago) changeset 67022 49309fe530fd parent 66425 8756322dc5de child 67036 783c901a62cb permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
```     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 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
```
```   526   then show ?thesis by simp
```
```   527 next
```
```   528   case False
```
```   529   with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)"
```
```   530     by simp
```
```   531   moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp
```
```   532   ultimately show ?thesis by (simp add: min.absorb1)
```
```   533 qed
```
```   534
```
```   535 lemma Max_insert2:
```
```   536   assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a"
```
```   537   shows "Max (insert a A) = a"
```
```   538 proof (cases "A = {}")
```
```   539   case True
```
```   540   then show ?thesis by simp
```
```   541 next
```
```   542   case False
```
```   543   with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)"
```
```   544     by simp
```
```   545   moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp
```
```   546   ultimately show ?thesis by (simp add: max.absorb1)
```
```   547 qed
```
```   548
```
```   549 lemma Min_le [simp]:
```
```   550   assumes "finite A" and "x \<in> A"
```
```   551   shows "Min A \<le> x"
```
```   552   using assms by (fact Min.coboundedI)
```
```   553
```
```   554 lemma Max_ge [simp]:
```
```   555   assumes "finite A" and "x \<in> A"
```
```   556   shows "x \<le> Max A"
```
```   557   using assms by (fact Max.coboundedI)
```
```   558
```
```   559 lemma Min_eqI:
```
```   560   assumes "finite A"
```
```   561   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x"
```
```   562     and "x \<in> A"
```
```   563   shows "Min A = x"
```
```   564 proof (rule antisym)
```
```   565   from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
```
```   566   with assms show "Min A \<ge> x" by simp
```
```   567 next
```
```   568   from assms show "x \<ge> Min A" by simp
```
```   569 qed
```
```   570
```
```   571 lemma Max_eqI:
```
```   572   assumes "finite A"
```
```   573   assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
```
```   574     and "x \<in> A"
```
```   575   shows "Max A = x"
```
```   576 proof (rule antisym)
```
```   577   from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto
```
```   578   with assms show "Max A \<le> x" by simp
```
```   579 next
```
```   580   from assms show "x \<le> Max A" by simp
```
```   581 qed
```
```   582
```
```   583 lemma eq_Min_iff:
```
```   584   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Min A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
```
```   585 by (meson Min_in Min_le antisym)
```
```   586
```
```   587 lemma Min_eq_iff:
```
```   588   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)"
```
```   589 by (meson Min_in Min_le antisym)
```
```   590
```
```   591 lemma eq_Max_iff:
```
```   592   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Max A  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
```
```   593 by (meson Max_in Max_ge antisym)
```
```   594
```
```   595 lemma Max_eq_iff:
```
```   596   "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A = m  \<longleftrightarrow>  m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)"
```
```   597 by (meson Max_in Max_ge antisym)
```
```   598
```
```   599 context
```
```   600   fixes A :: "'a set"
```
```   601   assumes fin_nonempty: "finite A" "A \<noteq> {}"
```
```   602 begin
```
```   603
```
```   604 lemma Min_ge_iff [simp]:
```
```   605   "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)"
```
```   606   using fin_nonempty by (fact Min.bounded_iff)
```
```   607
```
```   608 lemma Max_le_iff [simp]:
```
```   609   "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
```
```   610   using fin_nonempty by (fact Max.bounded_iff)
```
```   611
```
```   612 lemma Min_gr_iff [simp]:
```
```   613   "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)"
```
```   614   using fin_nonempty  by (induct rule: finite_ne_induct) simp_all
```
```   615
```
```   616 lemma Max_less_iff [simp]:
```
```   617   "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)"
```
```   618   using fin_nonempty by (induct rule: finite_ne_induct) simp_all
```
```   619
```
```   620 lemma Min_le_iff:
```
```   621   "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)"
```
```   622   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj)
```
```   623
```
```   624 lemma Max_ge_iff:
```
```   625   "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)"
```
```   626   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj)
```
```   627
```
```   628 lemma Min_less_iff:
```
```   629   "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)"
```
```   630   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj)
```
```   631
```
```   632 lemma Max_gr_iff:
```
```   633   "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)"
```
```   634   using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj)
```
```   635
```
```   636 end
```
```   637
```
```   638 lemma Max_eq_if:
```
```   639   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"
```
```   640   shows "Max A = Max B"
```
```   641 proof cases
```
```   642   assume "A = {}" thus ?thesis using assms by simp
```
```   643 next
```
```   644   assume "A \<noteq> {}" thus ?thesis using assms
```
```   645     by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2])
```
```   646 qed
```
```   647
```
```   648 lemma Min_antimono:
```
```   649   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
```
```   650   shows "Min N \<le> Min M"
```
```   651   using assms by (fact Min.antimono)
```
```   652
```
```   653 lemma Max_mono:
```
```   654   assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N"
```
```   655   shows "Max M \<le> Max N"
```
```   656   using assms by (fact Max.antimono)
```
```   657
```
```   658 end
```
```   659
```
```   660 context linorder  (* FIXME *)
```
```   661 begin
```
```   662
```
```   663 lemma mono_Min_commute:
```
```   664   assumes "mono f"
```
```   665   assumes "finite A" and "A \<noteq> {}"
```
```   666   shows "f (Min A) = Min (f ` A)"
```
```   667 proof (rule linorder_class.Min_eqI [symmetric])
```
```   668   from \<open>finite A\<close> show "finite (f ` A)" by simp
```
```   669   from assms show "f (Min A) \<in> f ` A" by simp
```
```   670   fix x
```
```   671   assume "x \<in> f ` A"
```
```   672   then obtain y where "y \<in> A" and "x = f y" ..
```
```   673   with assms have "Min A \<le> y" by auto
```
```   674   with \<open>mono f\<close> have "f (Min A) \<le> f y" by (rule monoE)
```
```   675   with \<open>x = f y\<close> show "f (Min A) \<le> x" by simp
```
```   676 qed
```
```   677
```
```   678 lemma mono_Max_commute:
```
```   679   assumes "mono f"
```
```   680   assumes "finite A" and "A \<noteq> {}"
```
```   681   shows "f (Max A) = Max (f ` A)"
```
```   682 proof (rule linorder_class.Max_eqI [symmetric])
```
```   683   from \<open>finite A\<close> show "finite (f ` A)" by simp
```
```   684   from assms show "f (Max A) \<in> f ` A" by simp
```
```   685   fix x
```
```   686   assume "x \<in> f ` A"
```
```   687   then obtain y where "y \<in> A" and "x = f y" ..
```
```   688   with assms have "y \<le> Max A" by auto
```
```   689   with \<open>mono f\<close> have "f y \<le> f (Max A)" by (rule monoE)
```
```   690   with \<open>x = f y\<close> show "x \<le> f (Max A)" by simp
```
```   691 qed
```
```   692
```
```   693 lemma finite_linorder_max_induct [consumes 1, case_names empty insert]:
```
```   694   assumes fin: "finite A"
```
```   695   and empty: "P {}"
```
```   696   and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)"
```
```   697   shows "P A"
```
```   698 using fin empty insert
```
```   699 proof (induct rule: finite_psubset_induct)
```
```   700   case (psubset A)
```
```   701   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
```
```   702   have fin: "finite A" by fact
```
```   703   have empty: "P {}" by fact
```
```   704   have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact
```
```   705   show "P A"
```
```   706   proof (cases "A = {}")
```
```   707     assume "A = {}"
```
```   708     then show "P A" using \<open>P {}\<close> by simp
```
```   709   next
```
```   710     let ?B = "A - {Max A}"
```
```   711     let ?A = "insert (Max A) ?B"
```
```   712     have "finite ?B" using \<open>finite A\<close> by simp
```
```   713     assume "A \<noteq> {}"
```
```   714     with \<open>finite A\<close> have "Max A : A" by auto
```
```   715     then have A: "?A = A" using insert_Diff_single insert_absorb by auto
```
```   716     then have "P ?B" using \<open>P {}\<close> step IH [of ?B] by blast
```
```   717     moreover
```
```   718     have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF \<open>finite A\<close>] by fastforce
```
```   719     ultimately show "P A" using A insert_Diff_single step [OF \<open>finite ?B\<close>] by fastforce
```
```   720   qed
```
```   721 qed
```
```   722
```
```   723 lemma finite_linorder_min_induct [consumes 1, case_names empty insert]:
```
```   724   "\<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"
```
```   725   by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
```
```   726
```
```   727 lemma Least_Min:
```
```   728   assumes "finite {a. P a}" and "\<exists>a. P a"
```
```   729   shows "(LEAST a. P a) = Min {a. P a}"
```
```   730 proof -
```
```   731   { fix A :: "'a set"
```
```   732     assume A: "finite A" "A \<noteq> {}"
```
```   733     have "(LEAST a. a \<in> A) = Min A"
```
```   734     using A proof (induct A rule: finite_ne_induct)
```
```   735       case singleton show ?case by (rule Least_equality) simp_all
```
```   736     next
```
```   737       case (insert a A)
```
```   738       have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
```
```   739         by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
```
```   740       with insert show ?case by simp
```
```   741     qed
```
```   742   } from this [of "{a. P a}"] assms show ?thesis by simp
```
```   743 qed
```
```   744
```
```   745 lemma infinite_growing:
```
```   746   assumes "X \<noteq> {}"
```
```   747   assumes *: "\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>X. y > x"
```
```   748   shows "\<not> finite X"
```
```   749 proof
```
```   750   assume "finite X"
```
```   751   with \<open>X \<noteq> {}\<close> have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X"
```
```   752     by auto
```
```   753   with *[of "Max X"] show False
```
```   754     by auto
```
```   755 qed
```
```   756
```
```   757 end
```
```   758
```
```   759 context linordered_ab_semigroup_add
```
```   760 begin
```
```   761
```
```   762 lemma add_Min_commute:
```
```   763   fixes k
```
```   764   assumes "finite N" and "N \<noteq> {}"
```
```   765   shows "k + Min N = Min {k + m | m. m \<in> N}"
```
```   766 proof -
```
```   767   have "\<And>x y. k + min x y = min (k + x) (k + y)"
```
```   768     by (simp add: min_def not_le)
```
```   769       (blast intro: antisym less_imp_le add_left_mono)
```
```   770   with assms show ?thesis
```
```   771     using hom_Min_commute [of "plus k" N]
```
```   772     by simp (blast intro: arg_cong [where f = Min])
```
```   773 qed
```
```   774
```
```   775 lemma add_Max_commute:
```
```   776   fixes k
```
```   777   assumes "finite N" and "N \<noteq> {}"
```
```   778   shows "k + Max N = Max {k + m | m. m \<in> N}"
```
```   779 proof -
```
```   780   have "\<And>x y. k + max x y = max (k + x) (k + y)"
```
```   781     by (simp add: max_def not_le)
```
```   782       (blast intro: antisym less_imp_le add_left_mono)
```
```   783   with assms show ?thesis
```
```   784     using hom_Max_commute [of "plus k" N]
```
```   785     by simp (blast intro: arg_cong [where f = Max])
```
```   786 qed
```
```   787
```
```   788 end
```
```   789
```
```   790 context linordered_ab_group_add
```
```   791 begin
```
```   792
```
```   793 lemma minus_Max_eq_Min [simp]:
```
```   794   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)"
```
```   795   by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min)
```
```   796
```
```   797 lemma minus_Min_eq_Max [simp]:
```
```   798   "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)"
```
```   799   by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max)
```
```   800
```
```   801 end
```
```   802
```
```   803 context complete_linorder
```
```   804 begin
```
```   805
```
```   806 lemma Min_Inf:
```
```   807   assumes "finite A" and "A \<noteq> {}"
```
```   808   shows "Min A = Inf A"
```
```   809 proof -
```
```   810   from assms obtain b B where "A = insert b B" and "finite B" by auto
```
```   811   then show ?thesis
```
```   812     by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b])
```
```   813 qed
```
```   814
```
```   815 lemma Max_Sup:
```
```   816   assumes "finite A" and "A \<noteq> {}"
```
```   817   shows "Max A = Sup A"
```
```   818 proof -
```
```   819   from assms obtain b B where "A = insert b B" and "finite B" by auto
```
```   820   then show ?thesis
```
```   821     by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b])
```
```   822 qed
```
```   823
```
```   824 end
```
```   825
```
```   826
```
```   827 subsection \<open>Arg Min\<close>
```
```   828
```
```   829 definition is_arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
```
```   830 "is_arg_min f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y < f x))"
```
```   831
```
```   832 definition arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
```
```   833 "arg_min f P = (SOME x. is_arg_min f P x)"
```
```   834
```
```   835 abbreviation arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
```
```   836 "arg_min_on f S \<equiv> arg_min f (\<lambda>x. x \<in> S)"
```
```   837
```
```   838 syntax
```
```   839   "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
```
```   840     ("(3ARG'_MIN _ _./ _)" [0, 0, 10] 10)
```
```   841 translations
```
```   842   "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)"
```
```   843
```
```   844 lemma is_arg_min_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder"
```
```   845 shows "is_arg_min f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<le> f y))"
```
```   846 by(auto simp add: is_arg_min_def)
```
```   847
```
```   848 lemma arg_minI:
```
```   849   "\<lbrakk> P x;
```
```   850     \<And>y. P y \<Longrightarrow> \<not> f y < f x;
```
```   851     \<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> \<not> f y < f x \<rbrakk> \<Longrightarrow> Q x \<rbrakk>
```
```   852   \<Longrightarrow> Q (arg_min f P)"
```
```   853 apply (simp add: arg_min_def is_arg_min_def)
```
```   854 apply (rule someI2_ex)
```
```   855  apply blast
```
```   856 apply blast
```
```   857 done
```
```   858
```
```   859 lemma arg_min_equality:
```
```   860   "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f k \<le> f x \<rbrakk> \<Longrightarrow> f (arg_min f P) = f k"
```
```   861   for f :: "_ \<Rightarrow> 'a::order"
```
```   862 apply (rule arg_minI)
```
```   863   apply assumption
```
```   864  apply (simp add: less_le_not_le)
```
```   865 by (metis le_less)
```
```   866
```
```   867 lemma wf_linord_ex_has_least:
```
```   868   "\<lbrakk> wf r; \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>*; P k \<rbrakk>
```
```   869    \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)"
```
```   870 apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]])
```
```   871 apply (drule_tac x = "m ` Collect P" in spec)
```
```   872 by force
```
```   873
```
```   874 lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)"
```
```   875   for m :: "'a \<Rightarrow> nat"
```
```   876 apply (simp only: pred_nat_trancl_eq_le [symmetric])
```
```   877 apply (rule wf_pred_nat [THEN wf_linord_ex_has_least])
```
```   878  apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le)
```
```   879 by assumption
```
```   880
```
```   881 lemma arg_min_nat_lemma:
```
```   882   "P k \<Longrightarrow> P(arg_min m P) \<and> (\<forall>y. P y \<longrightarrow> m (arg_min m P) \<le> m y)"
```
```   883   for m :: "'a \<Rightarrow> nat"
```
```   884 apply (simp add: arg_min_def is_arg_min_linorder)
```
```   885 apply (rule someI_ex)
```
```   886 apply (erule ex_has_least_nat)
```
```   887 done
```
```   888
```
```   889 lemmas arg_min_natI = arg_min_nat_lemma [THEN conjunct1]
```
```   890
```
```   891 lemma is_arg_min_arg_min_nat: fixes m :: "'a \<Rightarrow> nat"
```
```   892 shows "P x \<Longrightarrow> is_arg_min m P (arg_min m P)"
```
```   893 by (metis arg_min_nat_lemma is_arg_min_linorder)
```
```   894
```
```   895 lemma arg_min_nat_le: "P x \<Longrightarrow> m (arg_min m P) \<le> m x"
```
```   896   for m :: "'a \<Rightarrow> nat"
```
```   897 by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp])
```
```   898
```
```   899 lemma ex_min_if_finite:
```
```   900   "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>m\<in>S. \<not>(\<exists>x\<in>S. x < (m::'a::order))"
```
```   901 by(induction rule: finite.induct) (auto intro: order.strict_trans)
```
```   902
```
```   903 lemma ex_is_arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order"
```
```   904 shows "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>x. is_arg_min f (\<lambda>x. x : S) x"
```
```   905 unfolding is_arg_min_def
```
```   906 using ex_min_if_finite[of "f ` S"]
```
```   907 by auto
```
```   908
```
```   909 lemma arg_min_SOME_Min:
```
```   910   "finite S \<Longrightarrow> arg_min_on f S = (SOME y. y \<in> S \<and> f y = Min(f ` S))"
```
```   911 unfolding arg_min_def is_arg_min_linorder
```
```   912 apply(rule arg_cong[where f = Eps])
```
```   913 apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric])
```
```   914 done
```
```   915
```
```   916 lemma arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order"
```
```   917 assumes "finite S" "S \<noteq> {}"
```
```   918 shows  "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>S. f x < f (arg_min_on f S))"
```
```   919 using ex_is_arg_min_if_finite[OF assms, of f]
```
```   920 unfolding arg_min_def is_arg_min_def
```
```   921 by(auto dest!: someI_ex)
```
```   922
```
```   923 lemma arg_min_least: fixes f :: "'a \<Rightarrow> 'b :: linorder"
```
```   924 shows "\<lbrakk> finite S;  S \<noteq> {};  y \<in> S \<rbrakk> \<Longrightarrow> f(arg_min_on f S) \<le> f y"
```
```   925 by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f)
```
```   926
```
```   927 lemma arg_min_inj_eq: fixes f :: "'a \<Rightarrow> 'b :: order"
```
```   928 shows "\<lbrakk> inj_on f {x. P x}; P a; \<forall>y. P y \<longrightarrow> f a \<le> f y \<rbrakk> \<Longrightarrow> arg_min f P = a"
```
```   929 apply(simp add: arg_min_def is_arg_min_def)
```
```   930 apply(rule someI2[of _ a])
```
```   931  apply (simp add: less_le_not_le)
```
```   932 by (metis inj_on_eq_iff less_le mem_Collect_eq)
```
```   933
```
```   934
```
```   935 subsection \<open>Arg Max\<close>
```
```   936
```
```   937 definition is_arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where
```
```   938 "is_arg_max f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y > f x))"
```
```   939
```
```   940 definition arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
```
```   941 "arg_max f P = (SOME x. is_arg_max f P x)"
```
```   942
```
```   943 abbreviation arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where
```
```   944 "arg_max_on f S \<equiv> arg_max f (\<lambda>x. x \<in> S)"
```
```   945
```
```   946 syntax
```
```   947   "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a"
```
```   948     ("(3ARG'_MAX _ _./ _)" [0, 0, 10] 10)
```
```   949 translations
```
```   950   "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)"
```
```   951
```
```   952 lemma is_arg_max_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder"
```
```   953 shows "is_arg_max f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<ge> f y))"
```
```   954 by(auto simp add: is_arg_max_def)
```
```   955
```
```   956 lemma arg_maxI:
```
```   957   "P x \<Longrightarrow>
```
```   958     (\<And>y. P y \<Longrightarrow> \<not> f y > f x) \<Longrightarrow>
```
```   959     (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> \<not> f y > f x \<Longrightarrow> Q x) \<Longrightarrow>
```
```   960     Q (arg_max f P)"
```
```   961 apply (simp add: arg_max_def is_arg_max_def)
```
```   962 apply (rule someI2_ex)
```
```   963  apply blast
```
```   964 apply blast
```
```   965 done
```
```   966
```
```   967 lemma arg_max_equality:
```
```   968   "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f x \<le> f k \<rbrakk> \<Longrightarrow> f (arg_max f P) = f k"
```
```   969   for f :: "_ \<Rightarrow> 'a::order"
```
```   970 apply (rule arg_maxI [where f = f])
```
```   971   apply assumption
```
```   972  apply (simp add: less_le_not_le)
```
```   973 by (metis le_less)
```
```   974
```
```   975 lemma ex_has_greatest_nat_lemma:
```
```   976   "P k \<Longrightarrow> \<forall>x. P x \<longrightarrow> (\<exists>y. P y \<and> \<not> f y \<le> f x) \<Longrightarrow> \<exists>y. P y \<and> \<not> f y < f k + n"
```
```   977   for f :: "'a \<Rightarrow> nat"
```
```   978 by (induct n) (force simp: le_Suc_eq)+
```
```   979
```
```   980 lemma ex_has_greatest_nat:
```
```   981   "P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f x)"
```
```   982   for f :: "'a \<Rightarrow> nat"
```
```   983 apply (rule ccontr)
```
```   984 apply (cut_tac P = P and n = "b - f k" in ex_has_greatest_nat_lemma)
```
```   985   apply (subgoal_tac [3] "f k \<le> b")
```
```   986    apply auto
```
```   987 done
```
```   988
```
```   989 lemma arg_max_nat_lemma:
```
```   990   "\<lbrakk> P k;  \<forall>y. P y \<longrightarrow> f y < b \<rbrakk>
```
```   991   \<Longrightarrow> P (arg_max f P) \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f (arg_max f P))"
```
```   992   for f :: "'a \<Rightarrow> nat"
```
```   993 apply (simp add: arg_max_def is_arg_max_linorder)
```
```   994 apply (rule someI_ex)
```
```   995 apply (erule (1) ex_has_greatest_nat)
```
```   996 done
```
```   997
```
```   998 lemmas arg_max_natI = arg_max_nat_lemma [THEN conjunct1]
```
```   999
```
```  1000 lemma arg_max_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> f x \<le> f (arg_max f P)"
```
```  1001   for f :: "'a \<Rightarrow> nat"
```
```  1002 by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P])
```
```  1003
```
```  1004 end
```