1(* Title: HOL/Lattices_Big.thy 2 Author: Tobias Nipkow, Lawrence C Paulson and Markus Wenzel 3 with contributions by Jeremy Avigad 4*) 5 6section \<open>Big infimum (minimum) and supremum (maximum) over finite (non-empty) sets\<close> 7 8theory Lattices_Big 9 imports Option 10begin 11 12subsection \<open>Generic lattice operations over a set\<close> 13 14subsubsection \<open>Without neutral element\<close> 15 16locale semilattice_set = semilattice 17begin 18 19interpretation comp_fun_idem f 20 by standard (simp_all add: fun_eq_iff left_commute) 21 22definition F :: "'a set \<Rightarrow> 'a" 23where 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 26lemma eq_fold: 27 assumes "finite A" 28 shows "F (insert x A) = Finite_Set.fold f x A" 29proof (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 39qed 40 41lemma singleton [simp]: 42 "F {x} = x" 43 by (simp add: eq_fold) 44 45lemma insert_not_elem: 46 assumes "finite A" and "x \<notin> A" and "A \<noteq> {}" 47 shows "F (insert x A) = x \<^bold>* F A" 48proof - 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) 56qed 57 58lemma in_idem: 59 assumes "finite A" and "x \<in> A" 60 shows "x \<^bold>* F A = F A" 61proof - 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) 65qed 66 67lemma 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 72lemma 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 77lemma remove: 78 assumes "finite A" and "x \<in> A" 79 shows "F A = (if A - {x} = {} then x else x \<^bold>* F (A - {x}))" 80proof - 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 83qed 84 85lemma 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 90lemma subset: 91 assumes "finite A" "B \<noteq> {}" and "B \<subseteq> A" 92 shows "F B \<^bold>* F A = F A" 93proof - 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) 96qed 97 98lemma closed: 99 assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}" 100 shows "F A \<in> A" 101using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct) 102 case singleton then show ?case by simp 103next 104 case insert with elem show ?case by force 105qed 106 107lemma 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)" 111using N proof (induct rule: finite_ne_induct) 112 case singleton thus ?case by simp 113next 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 . 122qed 123 124lemma 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 127end 128 129locale semilattice_order_set = binary?: semilattice_order + semilattice_set 130begin 131 132lemma 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 136 137lemma 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 144lemma 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 149lemma coboundedI: 150 assumes "finite A" 151 and "a \<in> A" 152 shows "F A \<^bold>\<le> a" 153proof - 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 163qed 164 165lemma subset_imp: 166 assumes "A \<subseteq> B" and "A \<noteq> {}" and "finite B" 167 shows "F B \<^bold>\<le> F A" 168proof (cases "A = B") 169 case True then show ?thesis by (simp add: refl) 170next 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 . 177qed 178 179end 180 181 182subsubsection \<open>With neutral element\<close> 183 184locale semilattice_neutr_set = semilattice_neutr 185begin 186 187interpretation comp_fun_idem f 188 by standard (simp_all add: fun_eq_iff left_commute) 189 190definition F :: "'a set \<Rightarrow> 'a" 191where 192 eq_fold: "F A = Finite_Set.fold f \<^bold>1 A" 193 194lemma infinite [simp]: 195 "\<not> finite A \<Longrightarrow> F A = \<^bold>1" 196 by (simp add: eq_fold) 197 198lemma empty [simp]: 199 "F {} = \<^bold>1" 200 by (simp add: eq_fold) 201 202lemma 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 207lemma in_idem: 208 assumes "finite A" and "x \<in> A" 209 shows "x \<^bold>* F A = F A" 210proof - 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) 214qed 215 216lemma 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 221lemma remove: 222 assumes "finite A" and "x \<in> A" 223 shows "F A = x \<^bold>* F (A - {x})" 224proof - 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 227qed 228 229lemma 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 234lemma subset: 235 assumes "finite A" and "B \<subseteq> A" 236 shows "F B \<^bold>* F A = F A" 237proof - 238 from assms have "finite B" by (auto dest: finite_subset) 239 with assms show ?thesis by (simp add: union [symmetric] Un_absorb1) 240qed 241 242lemma closed: 243 assumes "finite A" "A \<noteq> {}" and elem: "\<And>x y. x \<^bold>* y \<in> {x, y}" 244 shows "F A \<in> A" 245using \<open>finite A\<close> \<open>A \<noteq> {}\<close> proof (induct rule: finite_ne_induct) 246 case singleton then show ?case by simp 247next 248 case insert with elem show ?case by force 249qed 250 251end 252 253locale semilattice_order_neutr_set = binary?: semilattice_neutr_order + semilattice_neutr_set 254begin 255 256lemma 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 260 261lemma 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 267lemma 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 272lemma coboundedI: 273 assumes "finite A" 274 and "a \<in> A" 275 shows "F A \<^bold>\<le> a" 276proof - 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 286qed 287 288lemma subset_imp: 289 assumes "A \<subseteq> B" and "finite B" 290 shows "F B \<^bold>\<le> F A" 291proof (cases "A = B") 292 case True then show ?thesis by (simp add: refl) 293next 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 . 300qed 301 302end 303 304 305subsection \<open>Lattice operations on finite sets\<close> 306 307context semilattice_inf 308begin 309 310sublocale Inf_fin: semilattice_order_set inf less_eq less 311defines 312 Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Inf_fin.F .. 313 314end 315 316context semilattice_sup 317begin 318 319sublocale Sup_fin: semilattice_order_set sup greater_eq greater 320defines 321 Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Sup_fin.F .. 322 323end 324 325 326subsection \<open>Infimum and Supremum over non-empty sets\<close> 327 328context lattice 329begin 330 331lemma 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" 334proof - 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) 339qed 340 341lemma 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 345lemma 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 349end 350 351context distrib_lattice 352begin 353 354lemma 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}" 358using 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 361lemma 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}" 364using A proof (induct rule: finite_ne_induct) 365 case singleton then show ?case 366 by (simp add: sup_Inf1_distrib [OF B]) 367next 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} = (\<Union>a\<in>A. \<Union>b\<in>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 . 390qed 391 392lemma 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}" 395using 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 398lemma 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}" 401using A proof (induct rule: finite_ne_induct) 402 case singleton thus ?case 403 by(simp add: inf_Sup1_distrib [OF B]) 404next 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} = (\<Union>a\<in>A. \<Union>b\<in>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 . 427qed 428 429end 430 431context complete_lattice 432begin 433 434lemma Inf_fin_Inf: 435 assumes "finite A" and "A \<noteq> {}" 436 shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = \<Sqinter>A" 437proof - 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]) 441qed 442 443lemma Sup_fin_Sup: 444 assumes "finite A" and "A \<noteq> {}" 445 shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = \<Squnion>A" 446proof - 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]) 450qed 451 452end 453 454 455subsection \<open>Minimum and Maximum over non-empty sets\<close> 456 457context linorder 458begin 459 460sublocale Min: semilattice_order_set min less_eq less 461 + Max: semilattice_order_set max greater_eq greater 462defines 463 Min = Min.F and Max = Max.F .. 464 465end 466 467syntax 468 "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _./ _)" [0, 10] 10) 469 "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _\<in>_./ _)" [0, 0, 10] 10) 470 "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _./ _)" [0, 10] 10) 471 "_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _\<in>_./ _)" [0, 0, 10] 10) 472 473translations 474 "MIN x y. f" \<rightleftharpoons> "MIN x. MIN y. f" 475 "MIN x. f" \<rightleftharpoons> "CONST Min (CONST range (\<lambda>x. f))" 476 "MIN x\<in>A. f" \<rightleftharpoons> "CONST Min ((\<lambda>x. f) ` A)" 477 "MAX x y. f" \<rightleftharpoons> "MAX x. MAX y. f" 478 "MAX x. f" \<rightleftharpoons> "CONST Max (CONST range (\<lambda>x. f))" 479 "MAX x\<in>A. f" \<rightleftharpoons> "CONST Max ((\<lambda>x. f) ` A)" 480 481text \<open>An aside: \<^const>\<open>Min\<close>/\<^const>\<open>Max\<close> on linear orders as special case of \<^const>\<open>Inf_fin\<close>/\<^const>\<open>Sup_fin\<close>\<close> 482 483lemma Inf_fin_Min: 484 "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)" 485 by (simp add: Inf_fin_def Min_def inf_min) 486 487lemma Sup_fin_Max: 488 "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)" 489 by (simp add: Sup_fin_def Max_def sup_max) 490 491context linorder 492begin 493 494lemma dual_min: 495 "ord.min greater_eq = max" 496 by (auto simp add: ord.min_def max_def fun_eq_iff) 497 498lemma dual_max: 499 "ord.max greater_eq = min" 500 by (auto simp add: ord.max_def min_def fun_eq_iff) 501 502lemma dual_Min: 503 "linorder.Min greater_eq = Max" 504proof - 505 interpret dual: linorder greater_eq greater by (fact dual_linorder) 506 show ?thesis by (simp add: dual.Min_def dual_min Max_def) 507qed 508 509lemma dual_Max: 510 "linorder.Max greater_eq = Min" 511proof - 512 interpret dual: linorder greater_eq greater by (fact dual_linorder) 513 show ?thesis by (simp add: dual.Max_def dual_max Min_def) 514qed 515 516lemmas Min_singleton = Min.singleton 517lemmas Max_singleton = Max.singleton 518lemmas Min_insert = Min.insert 519lemmas Max_insert = Max.insert 520lemmas Min_Un = Min.union 521lemmas Max_Un = Max.union 522lemmas hom_Min_commute = Min.hom_commute 523lemmas hom_Max_commute = Max.hom_commute 524 525lemma Min_in [simp]: 526 assumes "finite A" and "A \<noteq> {}" 527 shows "Min A \<in> A" 528 using assms by (auto simp add: min_def Min.closed) 529 530lemma Max_in [simp]: 531 assumes "finite A" and "A \<noteq> {}" 532 shows "Max A \<in> A" 533 using assms by (auto simp add: max_def Max.closed) 534 535lemma Min_insert2: 536 assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b" 537 shows "Min (insert a A) = a" 538proof (cases "A = {}") 539 case True 540 then show ?thesis by simp 541next 542 case False 543 with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)" 544 by simp 545 moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp 546 ultimately show ?thesis by (simp add: min.absorb1) 547qed 548 549lemma Max_insert2: 550 assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a" 551 shows "Max (insert a A) = a" 552proof (cases "A = {}") 553 case True 554 then show ?thesis by simp 555next 556 case False 557 with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)" 558 by simp 559 moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp 560 ultimately show ?thesis by (simp add: max.absorb1) 561qed 562 563lemma Min_le [simp]: 564 assumes "finite A" and "x \<in> A" 565 shows "Min A \<le> x" 566 using assms by (fact Min.coboundedI) 567 568lemma Max_ge [simp]: 569 assumes "finite A" and "x \<in> A" 570 shows "x \<le> Max A" 571 using assms by (fact Max.coboundedI) 572 573lemma Min_eqI: 574 assumes "finite A" 575 assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x" 576 and "x \<in> A" 577 shows "Min A = x" 578proof (rule antisym) 579 from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto 580 with assms show "Min A \<ge> x" by simp 581next 582 from assms show "x \<ge> Min A" by simp 583qed 584 585lemma Max_eqI: 586 assumes "finite A" 587 assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" 588 and "x \<in> A" 589 shows "Max A = x" 590proof (rule antisym) 591 from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto 592 with assms show "Max A \<le> x" by simp 593next 594 from assms show "x \<le> Max A" by simp 595qed 596 597lemma eq_Min_iff: 598 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Min A \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)" 599by (meson Min_in Min_le antisym) 600 601lemma Min_eq_iff: 602 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A = m \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)" 603by (meson Min_in Min_le antisym) 604 605lemma eq_Max_iff: 606 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Max A \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)" 607by (meson Max_in Max_ge antisym) 608 609lemma Max_eq_iff: 610 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A = m \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)" 611by (meson Max_in Max_ge antisym) 612 613context 614 fixes A :: "'a set" 615 assumes fin_nonempty: "finite A" "A \<noteq> {}" 616begin 617 618lemma Min_ge_iff [simp]: 619 "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)" 620 using fin_nonempty by (fact Min.bounded_iff) 621 622lemma Max_le_iff [simp]: 623 "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)" 624 using fin_nonempty by (fact Max.bounded_iff) 625 626lemma Min_gr_iff [simp]: 627 "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)" 628 using fin_nonempty by (induct rule: finite_ne_induct) simp_all 629 630lemma Max_less_iff [simp]: 631 "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)" 632 using fin_nonempty by (induct rule: finite_ne_induct) simp_all 633 634lemma Min_le_iff: 635 "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)" 636 using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj) 637 638lemma Max_ge_iff: 639 "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)" 640 using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj) 641 642lemma Min_less_iff: 643 "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)" 644 using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj) 645 646lemma Max_gr_iff: 647 "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)" 648 using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj) 649 650end 651 652lemma Max_eq_if: 653 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" 654 shows "Max A = Max B" 655proof cases 656 assume "A = {}" thus ?thesis using assms by simp 657next 658 assume "A \<noteq> {}" thus ?thesis using assms 659 by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2]) 660qed 661 662lemma Min_antimono: 663 assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N" 664 shows "Min N \<le> Min M" 665 using assms by (fact Min.subset_imp) 666 667lemma Max_mono: 668 assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N" 669 shows "Max M \<le> Max N" 670 using assms by (fact Max.subset_imp) 671 672end 673 674context linorder (* FIXME *) 675begin 676 677lemma mono_Min_commute: 678 assumes "mono f" 679 assumes "finite A" and "A \<noteq> {}" 680 shows "f (Min A) = Min (f ` A)" 681proof (rule linorder_class.Min_eqI [symmetric]) 682 from \<open>finite A\<close> show "finite (f ` A)" by simp 683 from assms show "f (Min A) \<in> f ` A" by simp 684 fix x 685 assume "x \<in> f ` A" 686 then obtain y where "y \<in> A" and "x = f y" .. 687 with assms have "Min A \<le> y" by auto 688 with \<open>mono f\<close> have "f (Min A) \<le> f y" by (rule monoE) 689 with \<open>x = f y\<close> show "f (Min A) \<le> x" by simp 690qed 691 692lemma mono_Max_commute: 693 assumes "mono f" 694 assumes "finite A" and "A \<noteq> {}" 695 shows "f (Max A) = Max (f ` A)" 696proof (rule linorder_class.Max_eqI [symmetric]) 697 from \<open>finite A\<close> show "finite (f ` A)" by simp 698 from assms show "f (Max A) \<in> f ` A" by simp 699 fix x 700 assume "x \<in> f ` A" 701 then obtain y where "y \<in> A" and "x = f y" .. 702 with assms have "y \<le> Max A" by auto 703 with \<open>mono f\<close> have "f y \<le> f (Max A)" by (rule monoE) 704 with \<open>x = f y\<close> show "x \<le> f (Max A)" by simp 705qed 706 707lemma finite_linorder_max_induct [consumes 1, case_names empty insert]: 708 assumes fin: "finite A" 709 and empty: "P {}" 710 and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)" 711 shows "P A" 712using fin empty insert 713proof (induct rule: finite_psubset_induct) 714 case (psubset A) 715 have IH: "\<And>B. \<lbrakk>B < A; P {}; (\<And>A b. \<lbrakk>finite A; \<forall>a\<in>A. a<b; P A\<rbrakk> \<Longrightarrow> P (insert b A))\<rbrakk> \<Longrightarrow> P B" by fact 716 have fin: "finite A" by fact 717 have empty: "P {}" by fact 718 have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact 719 show "P A" 720 proof (cases "A = {}") 721 assume "A = {}" 722 then show "P A" using \<open>P {}\<close> by simp 723 next 724 let ?B = "A - {Max A}" 725 let ?A = "insert (Max A) ?B" 726 have "finite ?B" using \<open>finite A\<close> by simp 727 assume "A \<noteq> {}" 728 with \<open>finite A\<close> have "Max A \<in> A" by auto 729 then have A: "?A = A" using insert_Diff_single insert_absorb by auto 730 then have "P ?B" using \<open>P {}\<close> step IH [of ?B] by blast 731 moreover 732 have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF \<open>finite A\<close>] by fastforce 733 ultimately show "P A" using A insert_Diff_single step [OF \<open>finite ?B\<close>] by fastforce 734 qed 735qed 736 737lemma finite_linorder_min_induct [consumes 1, case_names empty insert]: 738 "\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A" 739 by (rule linorder.finite_linorder_max_induct [OF dual_linorder]) 740 741lemma finite_ranking_induct[consumes 1, case_names empty insert]: 742 fixes f :: "'b \<Rightarrow> 'a" 743 assumes "finite S" 744 assumes "P {}" 745 assumes "\<And>x S. finite S \<Longrightarrow> (\<And>y. y \<in> S \<Longrightarrow> f y \<le> f x) \<Longrightarrow> P S \<Longrightarrow> P (insert x S)" 746 shows "P S" 747 using `finite S` 748proof (induction rule: finite_psubset_induct) 749 case (psubset A) 750 { 751 assume "A \<noteq> {}" 752 hence "f ` A \<noteq> {}" and "finite (f ` A)" 753 using psubset finite_image_iff by simp+ 754 then obtain a where "f a = Max (f ` A)" and "a \<in> A" 755 by (metis Max_in[of "f ` A"] imageE) 756 then have "P (A - {a})" 757 using psubset member_remove by blast 758 moreover 759 have "\<And>y. y \<in> A \<Longrightarrow> f y \<le> f a" 760 using \<open>f a = Max (f ` A)\<close> \<open>finite (f ` A)\<close> by simp 761 ultimately 762 have ?case 763 by (metis \<open>a \<in> A\<close> DiffD1 insert_Diff assms(3) finite_Diff psubset.hyps) 764 } 765 thus ?case 766 using assms(2) by blast 767qed 768 769lemma Least_Min: 770 assumes "finite {a. P a}" and "\<exists>a. P a" 771 shows "(LEAST a. P a) = Min {a. P a}" 772proof - 773 { fix A :: "'a set" 774 assume A: "finite A" "A \<noteq> {}" 775 have "(LEAST a. a \<in> A) = Min A" 776 using A proof (induct A rule: finite_ne_induct) 777 case singleton show ?case by (rule Least_equality) simp_all 778 next 779 case (insert a A) 780 have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)" 781 by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le) 782 with insert show ?case by simp 783 qed 784 } from this [of "{a. P a}"] assms show ?thesis by simp 785qed 786 787lemma infinite_growing: 788 assumes "X \<noteq> {}" 789 assumes *: "\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>X. y > x" 790 shows "\<not> finite X" 791proof 792 assume "finite X" 793 with \<open>X \<noteq> {}\<close> have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X" 794 by auto 795 with *[of "Max X"] show False 796 by auto 797qed 798 799end 800 801context linordered_ab_semigroup_add 802begin 803 804lemma Min_add_commute: 805 fixes k 806 assumes "finite S" and "S \<noteq> {}" 807 shows "Min ((\<lambda>x. f x + k) ` S) = Min(f ` S) + k" 808proof - 809 have m: "\<And>x y. min x y + k = min (x+k) (y+k)" 810 by(simp add: min_def antisym add_right_mono) 811 have "(\<lambda>x. f x + k) ` S = (\<lambda>y. y + k) ` (f ` S)" by auto 812 also have "Min \<dots> = Min (f ` S) + k" 813 using assms hom_Min_commute [of "\<lambda>y. y+k" "f ` S", OF m, symmetric] by simp 814 finally show ?thesis by simp 815qed 816 817lemma Max_add_commute: 818 fixes k 819 assumes "finite S" and "S \<noteq> {}" 820 shows "Max ((\<lambda>x. f x + k) ` S) = Max(f ` S) + k" 821proof - 822 have m: "\<And>x y. max x y + k = max (x+k) (y+k)" 823 by(simp add: max_def antisym add_right_mono) 824 have "(\<lambda>x. f x + k) ` S = (\<lambda>y. y + k) ` (f ` S)" by auto 825 also have "Max \<dots> = Max (f ` S) + k" 826 using assms hom_Max_commute [of "\<lambda>y. y+k" "f ` S", OF m, symmetric] by simp 827 finally show ?thesis by simp 828qed 829 830end 831 832context linordered_ab_group_add 833begin 834 835lemma minus_Max_eq_Min [simp]: 836 "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)" 837 by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min) 838 839lemma minus_Min_eq_Max [simp]: 840 "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)" 841 by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max) 842 843end 844 845context complete_linorder 846begin 847 848lemma Min_Inf: 849 assumes "finite A" and "A \<noteq> {}" 850 shows "Min A = Inf A" 851proof - 852 from assms obtain b B where "A = insert b B" and "finite B" by auto 853 then show ?thesis 854 by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b]) 855qed 856 857lemma Max_Sup: 858 assumes "finite A" and "A \<noteq> {}" 859 shows "Max A = Sup A" 860proof - 861 from assms obtain b B where "A = insert b B" and "finite B" by auto 862 then show ?thesis 863 by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b]) 864qed 865 866end 867 868 869subsection \<open>Arg Min\<close> 870 871definition is_arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where 872"is_arg_min f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y < f x))" 873 874definition arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where 875"arg_min f P = (SOME x. is_arg_min f P x)" 876 877definition arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where 878"arg_min_on f S = arg_min f (\<lambda>x. x \<in> S)" 879 880syntax 881 "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a" 882 ("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10) 883translations 884 "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)" 885 886lemma is_arg_min_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder" 887shows "is_arg_min f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<le> f y))" 888by(auto simp add: is_arg_min_def) 889 890lemma is_arg_min_antimono: fixes f :: "'a \<Rightarrow> ('b::order)" 891shows "\<lbrakk> is_arg_min f P x; f y \<le> f x; P y \<rbrakk> \<Longrightarrow> is_arg_min f P y" 892by (simp add: order.order_iff_strict is_arg_min_def) 893 894lemma arg_minI: 895 "\<lbrakk> P x; 896 \<And>y. P y \<Longrightarrow> \<not> f y < f x; 897 \<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> \<not> f y < f x \<rbrakk> \<Longrightarrow> Q x \<rbrakk> 898 \<Longrightarrow> Q (arg_min f P)" 899apply (simp add: arg_min_def is_arg_min_def) 900apply (rule someI2_ex) 901 apply blast 902apply blast 903done 904 905lemma arg_min_equality: 906 "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f k \<le> f x \<rbrakk> \<Longrightarrow> f (arg_min f P) = f k" 907 for f :: "_ \<Rightarrow> 'a::order" 908apply (rule arg_minI) 909 apply assumption 910 apply (simp add: less_le_not_le) 911by (metis le_less) 912 913lemma wf_linord_ex_has_least: 914 "\<lbrakk> wf r; \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>*; P k \<rbrakk> 915 \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)" 916apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) 917apply (drule_tac x = "m ` Collect P" in spec) 918by force 919 920lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)" 921 for m :: "'a \<Rightarrow> nat" 922apply (simp only: pred_nat_trancl_eq_le [symmetric]) 923apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) 924 apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le) 925by assumption 926 927lemma arg_min_nat_lemma: 928 "P k \<Longrightarrow> P(arg_min m P) \<and> (\<forall>y. P y \<longrightarrow> m (arg_min m P) \<le> m y)" 929 for m :: "'a \<Rightarrow> nat" 930apply (simp add: arg_min_def is_arg_min_linorder) 931apply (rule someI_ex) 932apply (erule ex_has_least_nat) 933done 934 935lemmas arg_min_natI = arg_min_nat_lemma [THEN conjunct1] 936 937lemma is_arg_min_arg_min_nat: fixes m :: "'a \<Rightarrow> nat" 938shows "P x \<Longrightarrow> is_arg_min m P (arg_min m P)" 939by (metis arg_min_nat_lemma is_arg_min_linorder) 940 941lemma arg_min_nat_le: "P x \<Longrightarrow> m (arg_min m P) \<le> m x" 942 for m :: "'a \<Rightarrow> nat" 943by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp]) 944 945lemma ex_min_if_finite: 946 "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>m\<in>S. \<not>(\<exists>x\<in>S. x < (m::'a::order))" 947by(induction rule: finite.induct) (auto intro: order.strict_trans) 948 949lemma ex_is_arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order" 950shows "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>x. is_arg_min f (\<lambda>x. x \<in> S) x" 951unfolding is_arg_min_def 952using ex_min_if_finite[of "f ` S"] 953by auto 954 955lemma arg_min_SOME_Min: 956 "finite S \<Longrightarrow> arg_min_on f S = (SOME y. y \<in> S \<and> f y = Min(f ` S))" 957unfolding arg_min_on_def arg_min_def is_arg_min_linorder 958apply(rule arg_cong[where f = Eps]) 959apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric]) 960done 961 962lemma arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order" 963assumes "finite S" "S \<noteq> {}" 964shows "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>S. f x < f (arg_min_on f S))" 965using ex_is_arg_min_if_finite[OF assms, of f] 966unfolding arg_min_on_def arg_min_def is_arg_min_def 967by(auto dest!: someI_ex) 968 969lemma arg_min_least: fixes f :: "'a \<Rightarrow> 'b :: linorder" 970shows "\<lbrakk> finite S; S \<noteq> {}; y \<in> S \<rbrakk> \<Longrightarrow> f(arg_min_on f S) \<le> f y" 971by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f) 972 973lemma arg_min_inj_eq: fixes f :: "'a \<Rightarrow> 'b :: order" 974shows "\<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" 975apply(simp add: arg_min_def is_arg_min_def) 976apply(rule someI2[of _ a]) 977 apply (simp add: less_le_not_le) 978by (metis inj_on_eq_iff less_le mem_Collect_eq) 979 980 981subsection \<open>Arg Max\<close> 982 983definition is_arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where 984"is_arg_max f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y > f x))" 985 986definition arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where 987"arg_max f P = (SOME x. is_arg_max f P x)" 988 989definition arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where 990"arg_max_on f S = arg_max f (\<lambda>x. x \<in> S)" 991 992syntax 993 "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a" 994 ("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10) 995translations 996 "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)" 997 998lemma is_arg_max_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder" 999shows "is_arg_max f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<ge> f y))" 1000by(auto simp add: is_arg_max_def) 1001 1002lemma arg_maxI: 1003 "P x \<Longrightarrow> 1004 (\<And>y. P y \<Longrightarrow> \<not> f y > f x) \<Longrightarrow> 1005 (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> \<not> f y > f x \<Longrightarrow> Q x) \<Longrightarrow> 1006 Q (arg_max f P)" 1007apply (simp add: arg_max_def is_arg_max_def) 1008apply (rule someI2_ex) 1009 apply blast 1010apply blast 1011done 1012 1013lemma arg_max_equality: 1014 "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f x \<le> f k \<rbrakk> \<Longrightarrow> f (arg_max f P) = f k" 1015 for f :: "_ \<Rightarrow> 'a::order" 1016apply (rule arg_maxI [where f = f]) 1017 apply assumption 1018 apply (simp add: less_le_not_le) 1019by (metis le_less) 1020 1021lemma ex_has_greatest_nat_lemma: 1022 "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" 1023 for f :: "'a \<Rightarrow> nat" 1024by (induct n) (force simp: le_Suc_eq)+ 1025 1026lemma ex_has_greatest_nat: 1027 "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)" 1028 for f :: "'a \<Rightarrow> nat" 1029apply (rule ccontr) 1030apply (cut_tac P = P and n = "b - f k" in ex_has_greatest_nat_lemma) 1031 apply (subgoal_tac [3] "f k \<le> b") 1032 apply auto 1033done 1034 1035lemma arg_max_nat_lemma: 1036 "\<lbrakk> P k; \<forall>y. P y \<longrightarrow> f y < b \<rbrakk> 1037 \<Longrightarrow> P (arg_max f P) \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f (arg_max f P))" 1038 for f :: "'a \<Rightarrow> nat" 1039apply (simp add: arg_max_def is_arg_max_linorder) 1040apply (rule someI_ex) 1041apply (erule (1) ex_has_greatest_nat) 1042done 1043 1044lemmas arg_max_natI = arg_max_nat_lemma [THEN conjunct1] 1045 1046lemma arg_max_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> f x \<le> f (arg_max f P)" 1047 for f :: "'a \<Rightarrow> nat" 1048by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P]) 1049 1050end 1051