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} = (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 . 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} = (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 . 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 465abbreviation MINIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" 466 where "MINIMUM A f \<equiv> Min(f ` A)" 467abbreviation MAXIMUM :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" 468 where "MAXIMUM A f \<equiv> Max(f ` A)" 469 470end 471 472 473syntax (ASCII) 474 "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _./ _)" [0, 10] 10) 475 "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _:_./ _)" [0, 0, 10] 10) 476 "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _./ _)" [0, 10] 10) 477 "_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _:_./ _)" [0, 0, 10] 10) 478 479syntax (output) 480 "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _./ _)" [0, 10] 10) 481 "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _:_./ _)" [0, 0, 10] 10) 482 "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _./ _)" [0, 10] 10) 483 "_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _:_./ _)" [0, 0, 10] 10) 484 485syntax 486 "_MIN1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _./ _)" [0, 10] 10) 487 "_MIN" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MIN _\<in>_./ _)" [0, 0, 10] 10) 488 "_MAX1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _./ _)" [0, 10] 10) 489 "_MAX" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3MAX _\<in>_./ _)" [0, 0, 10] 10) 490 491translations 492 "MIN x y. B" \<rightleftharpoons> "MIN x. MIN y. B" 493 "MIN x. B" \<rightleftharpoons> "CONST MINIMUM CONST UNIV (\<lambda>x. B)" 494 "MIN x. B" \<rightleftharpoons> "MIN x \<in> CONST UNIV. B" 495 "MIN x\<in>A. B" \<rightleftharpoons> "CONST MINIMUM A (\<lambda>x. B)" 496 "MAX x y. B" \<rightleftharpoons> "MAX x. MAX y. B" 497 "MAX x. B" \<rightleftharpoons> "CONST MAXIMUM CONST UNIV (\<lambda>x. B)" 498 "MAX x. B" \<rightleftharpoons> "MAX x \<in> CONST UNIV. B" 499 "MAX x\<in>A. B" \<rightleftharpoons> "CONST MAXIMUM A (\<lambda>x. B)" 500 501print_translation \<open> 502 [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"}, 503 Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax SUPREMUM} @{syntax_const "_SUP"}] 504\<close> \<comment> \<open>to avoid eta-contraction of body\<close> 505 506text \<open>An aside: @{const Min}/@{const Max} on linear orders as special case of @{const Inf_fin}/@{const Sup_fin}\<close> 507 508lemma Inf_fin_Min: 509 "Inf_fin = (Min :: 'a::{semilattice_inf, linorder} set \<Rightarrow> 'a)" 510 by (simp add: Inf_fin_def Min_def inf_min) 511 512lemma Sup_fin_Max: 513 "Sup_fin = (Max :: 'a::{semilattice_sup, linorder} set \<Rightarrow> 'a)" 514 by (simp add: Sup_fin_def Max_def sup_max) 515 516context linorder 517begin 518 519lemma dual_min: 520 "ord.min greater_eq = max" 521 by (auto simp add: ord.min_def max_def fun_eq_iff) 522 523lemma dual_max: 524 "ord.max greater_eq = min" 525 by (auto simp add: ord.max_def min_def fun_eq_iff) 526 527lemma dual_Min: 528 "linorder.Min greater_eq = Max" 529proof - 530 interpret dual: linorder greater_eq greater by (fact dual_linorder) 531 show ?thesis by (simp add: dual.Min_def dual_min Max_def) 532qed 533 534lemma dual_Max: 535 "linorder.Max greater_eq = Min" 536proof - 537 interpret dual: linorder greater_eq greater by (fact dual_linorder) 538 show ?thesis by (simp add: dual.Max_def dual_max Min_def) 539qed 540 541lemmas Min_singleton = Min.singleton 542lemmas Max_singleton = Max.singleton 543lemmas Min_insert = Min.insert 544lemmas Max_insert = Max.insert 545lemmas Min_Un = Min.union 546lemmas Max_Un = Max.union 547lemmas hom_Min_commute = Min.hom_commute 548lemmas hom_Max_commute = Max.hom_commute 549 550lemma Min_in [simp]: 551 assumes "finite A" and "A \<noteq> {}" 552 shows "Min A \<in> A" 553 using assms by (auto simp add: min_def Min.closed) 554 555lemma Max_in [simp]: 556 assumes "finite A" and "A \<noteq> {}" 557 shows "Max A \<in> A" 558 using assms by (auto simp add: max_def Max.closed) 559 560lemma Min_insert2: 561 assumes "finite A" and min: "\<And>b. b \<in> A \<Longrightarrow> a \<le> b" 562 shows "Min (insert a A) = a" 563proof (cases "A = {}") 564 case True 565 then show ?thesis by simp 566next 567 case False 568 with \<open>finite A\<close> have "Min (insert a A) = min a (Min A)" 569 by simp 570 moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> min have "a \<le> Min A" by simp 571 ultimately show ?thesis by (simp add: min.absorb1) 572qed 573 574lemma Max_insert2: 575 assumes "finite A" and max: "\<And>b. b \<in> A \<Longrightarrow> b \<le> a" 576 shows "Max (insert a A) = a" 577proof (cases "A = {}") 578 case True 579 then show ?thesis by simp 580next 581 case False 582 with \<open>finite A\<close> have "Max (insert a A) = max a (Max A)" 583 by simp 584 moreover from \<open>finite A\<close> \<open>A \<noteq> {}\<close> max have "Max A \<le> a" by simp 585 ultimately show ?thesis by (simp add: max.absorb1) 586qed 587 588lemma Min_le [simp]: 589 assumes "finite A" and "x \<in> A" 590 shows "Min A \<le> x" 591 using assms by (fact Min.coboundedI) 592 593lemma Max_ge [simp]: 594 assumes "finite A" and "x \<in> A" 595 shows "x \<le> Max A" 596 using assms by (fact Max.coboundedI) 597 598lemma Min_eqI: 599 assumes "finite A" 600 assumes "\<And>y. y \<in> A \<Longrightarrow> y \<ge> x" 601 and "x \<in> A" 602 shows "Min A = x" 603proof (rule antisym) 604 from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto 605 with assms show "Min A \<ge> x" by simp 606next 607 from assms show "x \<ge> Min A" by simp 608qed 609 610lemma Max_eqI: 611 assumes "finite A" 612 assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" 613 and "x \<in> A" 614 shows "Max A = x" 615proof (rule antisym) 616 from \<open>x \<in> A\<close> have "A \<noteq> {}" by auto 617 with assms show "Max A \<le> x" by simp 618next 619 from assms show "x \<le> Max A" by simp 620qed 621 622lemma eq_Min_iff: 623 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Min A \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)" 624by (meson Min_in Min_le antisym) 625 626lemma Min_eq_iff: 627 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Min A = m \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. m \<le> a)" 628by (meson Min_in Min_le antisym) 629 630lemma eq_Max_iff: 631 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> m = Max A \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)" 632by (meson Max_in Max_ge antisym) 633 634lemma Max_eq_iff: 635 "\<lbrakk> finite A; A \<noteq> {} \<rbrakk> \<Longrightarrow> Max A = m \<longleftrightarrow> m \<in> A \<and> (\<forall>a \<in> A. a \<le> m)" 636by (meson Max_in Max_ge antisym) 637 638context 639 fixes A :: "'a set" 640 assumes fin_nonempty: "finite A" "A \<noteq> {}" 641begin 642 643lemma Min_ge_iff [simp]: 644 "x \<le> Min A \<longleftrightarrow> (\<forall>a\<in>A. x \<le> a)" 645 using fin_nonempty by (fact Min.bounded_iff) 646 647lemma Max_le_iff [simp]: 648 "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)" 649 using fin_nonempty by (fact Max.bounded_iff) 650 651lemma Min_gr_iff [simp]: 652 "x < Min A \<longleftrightarrow> (\<forall>a\<in>A. x < a)" 653 using fin_nonempty by (induct rule: finite_ne_induct) simp_all 654 655lemma Max_less_iff [simp]: 656 "Max A < x \<longleftrightarrow> (\<forall>a\<in>A. a < x)" 657 using fin_nonempty by (induct rule: finite_ne_induct) simp_all 658 659lemma Min_le_iff: 660 "Min A \<le> x \<longleftrightarrow> (\<exists>a\<in>A. a \<le> x)" 661 using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_le_iff_disj) 662 663lemma Max_ge_iff: 664 "x \<le> Max A \<longleftrightarrow> (\<exists>a\<in>A. x \<le> a)" 665 using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: le_max_iff_disj) 666 667lemma Min_less_iff: 668 "Min A < x \<longleftrightarrow> (\<exists>a\<in>A. a < x)" 669 using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: min_less_iff_disj) 670 671lemma Max_gr_iff: 672 "x < Max A \<longleftrightarrow> (\<exists>a\<in>A. x < a)" 673 using fin_nonempty by (induct rule: finite_ne_induct) (simp_all add: less_max_iff_disj) 674 675end 676 677lemma Max_eq_if: 678 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" 679 shows "Max A = Max B" 680proof cases 681 assume "A = {}" thus ?thesis using assms by simp 682next 683 assume "A \<noteq> {}" thus ?thesis using assms 684 by(blast intro: antisym Max_in Max_ge_iff[THEN iffD2]) 685qed 686 687lemma Min_antimono: 688 assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N" 689 shows "Min N \<le> Min M" 690 using assms by (fact Min.subset_imp) 691 692lemma Max_mono: 693 assumes "M \<subseteq> N" and "M \<noteq> {}" and "finite N" 694 shows "Max M \<le> Max N" 695 using assms by (fact Max.subset_imp) 696 697end 698 699context linorder (* FIXME *) 700begin 701 702lemma mono_Min_commute: 703 assumes "mono f" 704 assumes "finite A" and "A \<noteq> {}" 705 shows "f (Min A) = Min (f ` A)" 706proof (rule linorder_class.Min_eqI [symmetric]) 707 from \<open>finite A\<close> show "finite (f ` A)" by simp 708 from assms show "f (Min A) \<in> f ` A" by simp 709 fix x 710 assume "x \<in> f ` A" 711 then obtain y where "y \<in> A" and "x = f y" .. 712 with assms have "Min A \<le> y" by auto 713 with \<open>mono f\<close> have "f (Min A) \<le> f y" by (rule monoE) 714 with \<open>x = f y\<close> show "f (Min A) \<le> x" by simp 715qed 716 717lemma mono_Max_commute: 718 assumes "mono f" 719 assumes "finite A" and "A \<noteq> {}" 720 shows "f (Max A) = Max (f ` A)" 721proof (rule linorder_class.Max_eqI [symmetric]) 722 from \<open>finite A\<close> show "finite (f ` A)" by simp 723 from assms show "f (Max A) \<in> f ` A" by simp 724 fix x 725 assume "x \<in> f ` A" 726 then obtain y where "y \<in> A" and "x = f y" .. 727 with assms have "y \<le> Max A" by auto 728 with \<open>mono f\<close> have "f y \<le> f (Max A)" by (rule monoE) 729 with \<open>x = f y\<close> show "x \<le> f (Max A)" by simp 730qed 731 732lemma finite_linorder_max_induct [consumes 1, case_names empty insert]: 733 assumes fin: "finite A" 734 and empty: "P {}" 735 and insert: "\<And>b A. finite A \<Longrightarrow> \<forall>a\<in>A. a < b \<Longrightarrow> P A \<Longrightarrow> P (insert b A)" 736 shows "P A" 737using fin empty insert 738proof (induct rule: finite_psubset_induct) 739 case (psubset A) 740 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 741 have fin: "finite A" by fact 742 have empty: "P {}" by fact 743 have step: "\<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. a < b; P A\<rbrakk> \<Longrightarrow> P (insert b A)" by fact 744 show "P A" 745 proof (cases "A = {}") 746 assume "A = {}" 747 then show "P A" using \<open>P {}\<close> by simp 748 next 749 let ?B = "A - {Max A}" 750 let ?A = "insert (Max A) ?B" 751 have "finite ?B" using \<open>finite A\<close> by simp 752 assume "A \<noteq> {}" 753 with \<open>finite A\<close> have "Max A \<in> A" by auto 754 then have A: "?A = A" using insert_Diff_single insert_absorb by auto 755 then have "P ?B" using \<open>P {}\<close> step IH [of ?B] by blast 756 moreover 757 have "\<forall>a\<in>?B. a < Max A" using Max_ge [OF \<open>finite A\<close>] by fastforce 758 ultimately show "P A" using A insert_Diff_single step [OF \<open>finite ?B\<close>] by fastforce 759 qed 760qed 761 762lemma finite_linorder_min_induct [consumes 1, case_names empty insert]: 763 "\<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" 764 by (rule linorder.finite_linorder_max_induct [OF dual_linorder]) 765 766lemma Least_Min: 767 assumes "finite {a. P a}" and "\<exists>a. P a" 768 shows "(LEAST a. P a) = Min {a. P a}" 769proof - 770 { fix A :: "'a set" 771 assume A: "finite A" "A \<noteq> {}" 772 have "(LEAST a. a \<in> A) = Min A" 773 using A proof (induct A rule: finite_ne_induct) 774 case singleton show ?case by (rule Least_equality) simp_all 775 next 776 case (insert a A) 777 have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)" 778 by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le) 779 with insert show ?case by simp 780 qed 781 } from this [of "{a. P a}"] assms show ?thesis by simp 782qed 783 784lemma infinite_growing: 785 assumes "X \<noteq> {}" 786 assumes *: "\<And>x. x \<in> X \<Longrightarrow> \<exists>y\<in>X. y > x" 787 shows "\<not> finite X" 788proof 789 assume "finite X" 790 with \<open>X \<noteq> {}\<close> have "Max X \<in> X" "\<forall>x\<in>X. x \<le> Max X" 791 by auto 792 with *[of "Max X"] show False 793 by auto 794qed 795 796end 797 798context linordered_ab_semigroup_add 799begin 800 801lemma add_Min_commute: 802 fixes k 803 assumes "finite N" and "N \<noteq> {}" 804 shows "k + Min N = Min {k + m | m. m \<in> N}" 805proof - 806 have "\<And>x y. k + min x y = min (k + x) (k + y)" 807 by (simp add: min_def not_le) 808 (blast intro: antisym less_imp_le add_left_mono) 809 with assms show ?thesis 810 using hom_Min_commute [of "plus k" N] 811 by simp (blast intro: arg_cong [where f = Min]) 812qed 813 814lemma add_Max_commute: 815 fixes k 816 assumes "finite N" and "N \<noteq> {}" 817 shows "k + Max N = Max {k + m | m. m \<in> N}" 818proof - 819 have "\<And>x y. k + max x y = max (k + x) (k + y)" 820 by (simp add: max_def not_le) 821 (blast intro: antisym less_imp_le add_left_mono) 822 with assms show ?thesis 823 using hom_Max_commute [of "plus k" N] 824 by simp (blast intro: arg_cong [where f = Max]) 825qed 826 827end 828 829context linordered_ab_group_add 830begin 831 832lemma minus_Max_eq_Min [simp]: 833 "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Max S = Min (uminus ` S)" 834 by (induct S rule: finite_ne_induct) (simp_all add: minus_max_eq_min) 835 836lemma minus_Min_eq_Max [simp]: 837 "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - Min S = Max (uminus ` S)" 838 by (induct S rule: finite_ne_induct) (simp_all add: minus_min_eq_max) 839 840end 841 842context complete_linorder 843begin 844 845lemma Min_Inf: 846 assumes "finite A" and "A \<noteq> {}" 847 shows "Min A = Inf A" 848proof - 849 from assms obtain b B where "A = insert b B" and "finite B" by auto 850 then show ?thesis 851 by (simp add: Min.eq_fold complete_linorder_inf_min [symmetric] inf_Inf_fold_inf inf.commute [of b]) 852qed 853 854lemma Max_Sup: 855 assumes "finite A" and "A \<noteq> {}" 856 shows "Max A = Sup A" 857proof - 858 from assms obtain b B where "A = insert b B" and "finite B" by auto 859 then show ?thesis 860 by (simp add: Max.eq_fold complete_linorder_sup_max [symmetric] sup_Sup_fold_sup sup.commute [of b]) 861qed 862 863end 864 865 866subsection \<open>Arg Min\<close> 867 868definition is_arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where 869"is_arg_min f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y < f x))" 870 871definition arg_min :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where 872"arg_min f P = (SOME x. is_arg_min f P x)" 873 874definition arg_min_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where 875"arg_min_on f S = arg_min f (\<lambda>x. x \<in> S)" 876 877syntax 878 "_arg_min" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a" 879 ("(3ARG'_MIN _ _./ _)" [1000, 0, 10] 10) 880translations 881 "ARG_MIN f x. P" \<rightleftharpoons> "CONST arg_min f (\<lambda>x. P)" 882 883lemma is_arg_min_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder" 884shows "is_arg_min f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<le> f y))" 885by(auto simp add: is_arg_min_def) 886 887lemma is_arg_min_antimono: fixes f :: "'a \<Rightarrow> ('b::order)" 888shows "\<lbrakk> is_arg_min f P x; f y \<le> f x; P y \<rbrakk> \<Longrightarrow> is_arg_min f P y" 889by (simp add: order.order_iff_strict is_arg_min_def) 890 891lemma arg_minI: 892 "\<lbrakk> P x; 893 \<And>y. P y \<Longrightarrow> \<not> f y < f x; 894 \<And>x. \<lbrakk> P x; \<forall>y. P y \<longrightarrow> \<not> f y < f x \<rbrakk> \<Longrightarrow> Q x \<rbrakk> 895 \<Longrightarrow> Q (arg_min f P)" 896apply (simp add: arg_min_def is_arg_min_def) 897apply (rule someI2_ex) 898 apply blast 899apply blast 900done 901 902lemma arg_min_equality: 903 "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f k \<le> f x \<rbrakk> \<Longrightarrow> f (arg_min f P) = f k" 904 for f :: "_ \<Rightarrow> 'a::order" 905apply (rule arg_minI) 906 apply assumption 907 apply (simp add: less_le_not_le) 908by (metis le_less) 909 910lemma wf_linord_ex_has_least: 911 "\<lbrakk> wf r; \<forall>x y. (x, y) \<in> r\<^sup>+ \<longleftrightarrow> (y, x) \<notin> r\<^sup>*; P k \<rbrakk> 912 \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> (m x, m y) \<in> r\<^sup>*)" 913apply (drule wf_trancl [THEN wf_eq_minimal [THEN iffD1]]) 914apply (drule_tac x = "m ` Collect P" in spec) 915by force 916 917lemma ex_has_least_nat: "P k \<Longrightarrow> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> m x \<le> m y)" 918 for m :: "'a \<Rightarrow> nat" 919apply (simp only: pred_nat_trancl_eq_le [symmetric]) 920apply (rule wf_pred_nat [THEN wf_linord_ex_has_least]) 921 apply (simp add: less_eq linorder_not_le pred_nat_trancl_eq_le) 922by assumption 923 924lemma arg_min_nat_lemma: 925 "P k \<Longrightarrow> P(arg_min m P) \<and> (\<forall>y. P y \<longrightarrow> m (arg_min m P) \<le> m y)" 926 for m :: "'a \<Rightarrow> nat" 927apply (simp add: arg_min_def is_arg_min_linorder) 928apply (rule someI_ex) 929apply (erule ex_has_least_nat) 930done 931 932lemmas arg_min_natI = arg_min_nat_lemma [THEN conjunct1] 933 934lemma is_arg_min_arg_min_nat: fixes m :: "'a \<Rightarrow> nat" 935shows "P x \<Longrightarrow> is_arg_min m P (arg_min m P)" 936by (metis arg_min_nat_lemma is_arg_min_linorder) 937 938lemma arg_min_nat_le: "P x \<Longrightarrow> m (arg_min m P) \<le> m x" 939 for m :: "'a \<Rightarrow> nat" 940by (rule arg_min_nat_lemma [THEN conjunct2, THEN spec, THEN mp]) 941 942lemma ex_min_if_finite: 943 "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>m\<in>S. \<not>(\<exists>x\<in>S. x < (m::'a::order))" 944by(induction rule: finite.induct) (auto intro: order.strict_trans) 945 946lemma ex_is_arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order" 947shows "\<lbrakk> finite S; S \<noteq> {} \<rbrakk> \<Longrightarrow> \<exists>x. is_arg_min f (\<lambda>x. x \<in> S) x" 948unfolding is_arg_min_def 949using ex_min_if_finite[of "f ` S"] 950by auto 951 952lemma arg_min_SOME_Min: 953 "finite S \<Longrightarrow> arg_min_on f S = (SOME y. y \<in> S \<and> f y = Min(f ` S))" 954unfolding arg_min_on_def arg_min_def is_arg_min_linorder 955apply(rule arg_cong[where f = Eps]) 956apply (auto simp: fun_eq_iff intro: Min_eqI[symmetric]) 957done 958 959lemma arg_min_if_finite: fixes f :: "'a \<Rightarrow> 'b :: order" 960assumes "finite S" "S \<noteq> {}" 961shows "arg_min_on f S \<in> S" and "\<not>(\<exists>x\<in>S. f x < f (arg_min_on f S))" 962using ex_is_arg_min_if_finite[OF assms, of f] 963unfolding arg_min_on_def arg_min_def is_arg_min_def 964by(auto dest!: someI_ex) 965 966lemma arg_min_least: fixes f :: "'a \<Rightarrow> 'b :: linorder" 967shows "\<lbrakk> finite S; S \<noteq> {}; y \<in> S \<rbrakk> \<Longrightarrow> f(arg_min_on f S) \<le> f y" 968by(simp add: arg_min_SOME_Min inv_into_def2[symmetric] f_inv_into_f) 969 970lemma arg_min_inj_eq: fixes f :: "'a \<Rightarrow> 'b :: order" 971shows "\<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" 972apply(simp add: arg_min_def is_arg_min_def) 973apply(rule someI2[of _ a]) 974 apply (simp add: less_le_not_le) 975by (metis inj_on_eq_iff less_le mem_Collect_eq) 976 977 978subsection \<open>Arg Max\<close> 979 980definition is_arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" where 981"is_arg_max f P x = (P x \<and> \<not>(\<exists>y. P y \<and> f y > f x))" 982 983definition arg_max :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where 984"arg_max f P = (SOME x. is_arg_max f P x)" 985 986definition arg_max_on :: "('a \<Rightarrow> 'b::ord) \<Rightarrow> 'a set \<Rightarrow> 'a" where 987"arg_max_on f S = arg_max f (\<lambda>x. x \<in> S)" 988 989syntax 990 "_arg_max" :: "('a \<Rightarrow> 'b) \<Rightarrow> pttrn \<Rightarrow> bool \<Rightarrow> 'a" 991 ("(3ARG'_MAX _ _./ _)" [1000, 0, 10] 10) 992translations 993 "ARG_MAX f x. P" \<rightleftharpoons> "CONST arg_max f (\<lambda>x. P)" 994 995lemma is_arg_max_linorder: fixes f :: "'a \<Rightarrow> 'b :: linorder" 996shows "is_arg_max f P x = (P x \<and> (\<forall>y. P y \<longrightarrow> f x \<ge> f y))" 997by(auto simp add: is_arg_max_def) 998 999lemma arg_maxI: 1000 "P x \<Longrightarrow> 1001 (\<And>y. P y \<Longrightarrow> \<not> f y > f x) \<Longrightarrow> 1002 (\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> \<not> f y > f x \<Longrightarrow> Q x) \<Longrightarrow> 1003 Q (arg_max f P)" 1004apply (simp add: arg_max_def is_arg_max_def) 1005apply (rule someI2_ex) 1006 apply blast 1007apply blast 1008done 1009 1010lemma arg_max_equality: 1011 "\<lbrakk> P k; \<And>x. P x \<Longrightarrow> f x \<le> f k \<rbrakk> \<Longrightarrow> f (arg_max f P) = f k" 1012 for f :: "_ \<Rightarrow> 'a::order" 1013apply (rule arg_maxI [where f = f]) 1014 apply assumption 1015 apply (simp add: less_le_not_le) 1016by (metis le_less) 1017 1018lemma ex_has_greatest_nat_lemma: 1019 "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" 1020 for f :: "'a \<Rightarrow> nat" 1021by (induct n) (force simp: le_Suc_eq)+ 1022 1023lemma ex_has_greatest_nat: 1024 "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)" 1025 for f :: "'a \<Rightarrow> nat" 1026apply (rule ccontr) 1027apply (cut_tac P = P and n = "b - f k" in ex_has_greatest_nat_lemma) 1028 apply (subgoal_tac [3] "f k \<le> b") 1029 apply auto 1030done 1031 1032lemma arg_max_nat_lemma: 1033 "\<lbrakk> P k; \<forall>y. P y \<longrightarrow> f y < b \<rbrakk> 1034 \<Longrightarrow> P (arg_max f P) \<and> (\<forall>y. P y \<longrightarrow> f y \<le> f (arg_max f P))" 1035 for f :: "'a \<Rightarrow> nat" 1036apply (simp add: arg_max_def is_arg_max_linorder) 1037apply (rule someI_ex) 1038apply (erule (1) ex_has_greatest_nat) 1039done 1040 1041lemmas arg_max_natI = arg_max_nat_lemma [THEN conjunct1] 1042 1043lemma arg_max_nat_le: "P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> f y < b \<Longrightarrow> f x \<le> f (arg_max f P)" 1044 for f :: "'a \<Rightarrow> nat" 1045by (blast dest: arg_max_nat_lemma [THEN conjunct2, THEN spec, of P]) 1046 1047end 1048