src/HOL/Infinite_Set.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 19363 667b5ea637dd child 19457 b6eb4b4546fa permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
 paulson@14442 ` 1` ```(* Title: HOL/Infnite_Set.thy ``` paulson@14442 ` 2` ``` ID: \$Id\$ ``` wenzelm@14896 ` 3` ``` Author: Stephan Merz ``` paulson@14442 ` 4` ```*) ``` paulson@14442 ` 5` paulson@14442 ` 6` ```header {* Infnite Sets and Related Concepts*} ``` paulson@14442 ` 7` nipkow@15131 ` 8` ```theory Infinite_Set ``` nipkow@16733 ` 9` ```imports Hilbert_Choice Binomial ``` nipkow@15131 ` 10` ```begin ``` paulson@14442 ` 11` paulson@14442 ` 12` ```subsection "Infinite Sets" ``` paulson@14442 ` 13` paulson@14442 ` 14` ```text {* Some elementary facts about infinite sets, by Stefan Merz. *} ``` paulson@14442 ` 15` wenzelm@19363 ` 16` ```abbreviation ``` wenzelm@19363 ` 17` ``` infinite :: "'a set \ bool" ``` wenzelm@19363 ` 18` ``` "infinite S == \ finite S" ``` paulson@14442 ` 19` paulson@14442 ` 20` ```text {* ``` paulson@14442 ` 21` ``` Infinite sets are non-empty, and if we remove some elements ``` paulson@14442 ` 22` ``` from an infinite set, the result is still infinite. ``` paulson@14442 ` 23` ```*} ``` paulson@14442 ` 24` paulson@14442 ` 25` ```lemma infinite_nonempty: ``` paulson@14442 ` 26` ``` "\ (infinite {})" ``` paulson@14442 ` 27` ```by simp ``` paulson@14442 ` 28` paulson@14442 ` 29` ```lemma infinite_remove: ``` paulson@14442 ` 30` ``` "infinite S \ infinite (S - {a})" ``` paulson@14442 ` 31` ```by simp ``` paulson@14442 ` 32` paulson@14442 ` 33` ```lemma Diff_infinite_finite: ``` paulson@14442 ` 34` ``` assumes T: "finite T" and S: "infinite S" ``` paulson@14442 ` 35` ``` shows "infinite (S-T)" ``` paulson@14442 ` 36` ```using T ``` paulson@14442 ` 37` ```proof (induct) ``` paulson@14442 ` 38` ``` from S ``` paulson@14442 ` 39` ``` show "infinite (S - {})" by auto ``` paulson@14442 ` 40` ```next ``` paulson@14442 ` 41` ``` fix T x ``` paulson@14442 ` 42` ``` assume ih: "infinite (S-T)" ``` paulson@14442 ` 43` ``` have "S - (insert x T) = (S-T) - {x}" ``` paulson@14442 ` 44` ``` by (rule Diff_insert) ``` paulson@14442 ` 45` ``` with ih ``` paulson@14442 ` 46` ``` show "infinite (S - (insert x T))" ``` paulson@14442 ` 47` ``` by (simp add: infinite_remove) ``` paulson@14442 ` 48` ```qed ``` paulson@14442 ` 49` paulson@14442 ` 50` ```lemma Un_infinite: ``` paulson@14442 ` 51` ``` "infinite S \ infinite (S \ T)" ``` paulson@14442 ` 52` ```by simp ``` paulson@14442 ` 53` paulson@14442 ` 54` ```lemma infinite_super: ``` paulson@14442 ` 55` ``` assumes T: "S \ T" and S: "infinite S" ``` paulson@14442 ` 56` ``` shows "infinite T" ``` paulson@14442 ` 57` ```proof (rule ccontr) ``` paulson@14442 ` 58` ``` assume "\(infinite T)" ``` paulson@14442 ` 59` ``` with T ``` paulson@14442 ` 60` ``` have "finite S" by (simp add: finite_subset) ``` paulson@14442 ` 61` ``` with S ``` paulson@14442 ` 62` ``` show False by simp ``` paulson@14442 ` 63` ```qed ``` paulson@14442 ` 64` paulson@14442 ` 65` ```text {* ``` paulson@14442 ` 66` ``` As a concrete example, we prove that the set of natural ``` paulson@14442 ` 67` ``` numbers is infinite. ``` paulson@14442 ` 68` ```*} ``` paulson@14442 ` 69` paulson@14442 ` 70` ```lemma finite_nat_bounded: ``` paulson@14442 ` 71` ``` assumes S: "finite (S::nat set)" ``` nipkow@15045 ` 72` ``` shows "\k. S \ {..k. ?bounded S k") ``` paulson@14442 ` 73` ```using S ``` paulson@14442 ` 74` ```proof (induct) ``` paulson@14442 ` 75` ``` have "?bounded {} 0" by simp ``` paulson@14442 ` 76` ``` thus "\k. ?bounded {} k" .. ``` paulson@14442 ` 77` ```next ``` paulson@14442 ` 78` ``` fix S x ``` paulson@14442 ` 79` ``` assume "\k. ?bounded S k" ``` paulson@14442 ` 80` ``` then obtain k where k: "?bounded S k" .. ``` paulson@14442 ` 81` ``` show "\k. ?bounded (insert x S) k" ``` paulson@14442 ` 82` ``` proof (cases "xk. S \ {.. {..k. S \ {..k})" (is "?lhs = ?rhs") ``` paulson@14442 ` 106` ```proof ``` paulson@14442 ` 107` ``` assume ?lhs ``` nipkow@15045 ` 108` ``` then obtain k where "S \ {.. {..k}" by auto ``` paulson@14442 ` 111` ``` thus ?rhs .. ``` paulson@14442 ` 112` ```next ``` paulson@14442 ` 113` ``` assume ?rhs ``` paulson@14442 ` 114` ``` then obtain k where "S \ {..k}" .. ``` paulson@14442 ` 115` ``` thus "finite S" ``` paulson@14442 ` 116` ``` by (rule finite_subset, simp) ``` paulson@14442 ` 117` ```qed ``` paulson@14442 ` 118` paulson@14442 ` 119` ```lemma infinite_nat_iff_unbounded: ``` paulson@14442 ` 120` ``` "infinite (S::nat set) = (\m. \n. m n\S)" ``` paulson@14442 ` 121` ``` (is "?lhs = ?rhs") ``` paulson@14442 ` 122` ```proof ``` paulson@14442 ` 123` ``` assume inf: ?lhs ``` paulson@14442 ` 124` ``` show ?rhs ``` paulson@14442 ` 125` ``` proof (rule ccontr) ``` paulson@14442 ` 126` ``` assume "\ ?rhs" ``` paulson@14442 ` 127` ``` then obtain m where m: "\n. m n\S" by blast ``` paulson@14442 ` 128` ``` hence "S \ {..m}" ``` paulson@16796 ` 129` ``` by (auto simp add: sym[OF linorder_not_less]) ``` paulson@14442 ` 130` ``` with inf show "False" ``` paulson@14442 ` 131` ``` by (simp add: finite_nat_iff_bounded_le) ``` paulson@14442 ` 132` ``` qed ``` paulson@14442 ` 133` ```next ``` paulson@14442 ` 134` ``` assume unbounded: ?rhs ``` paulson@14442 ` 135` ``` show ?lhs ``` paulson@14442 ` 136` ``` proof ``` paulson@14442 ` 137` ``` assume "finite S" ``` paulson@14442 ` 138` ``` then obtain m where "S \ {..m}" ``` paulson@14442 ` 139` ``` by (auto simp add: finite_nat_iff_bounded_le) ``` paulson@14442 ` 140` ``` hence "\n. m n\S" by auto ``` paulson@14442 ` 141` ``` with unbounded show "False" by blast ``` paulson@14442 ` 142` ``` qed ``` paulson@14442 ` 143` ```qed ``` paulson@14442 ` 144` paulson@14442 ` 145` ```lemma infinite_nat_iff_unbounded_le: ``` paulson@14442 ` 146` ``` "infinite (S::nat set) = (\m. \n. m\n \ n\S)" ``` paulson@14442 ` 147` ``` (is "?lhs = ?rhs") ``` paulson@14442 ` 148` ```proof ``` paulson@14442 ` 149` ``` assume inf: ?lhs ``` paulson@14442 ` 150` ``` show ?rhs ``` paulson@14442 ` 151` ``` proof ``` paulson@14442 ` 152` ``` fix m ``` paulson@14442 ` 153` ``` from inf obtain n where "m n\S" ``` paulson@14442 ` 154` ``` by (auto simp add: infinite_nat_iff_unbounded) ``` paulson@14442 ` 155` ``` hence "m\n \ n\S" by auto ``` paulson@14442 ` 156` ``` thus "\n. m \ n \ n \ S" .. ``` paulson@14442 ` 157` ``` qed ``` paulson@14442 ` 158` ```next ``` paulson@14442 ` 159` ``` assume unbounded: ?rhs ``` paulson@14442 ` 160` ``` show ?lhs ``` paulson@14442 ` 161` ``` proof (auto simp add: infinite_nat_iff_unbounded) ``` paulson@14442 ` 162` ``` fix m ``` paulson@14442 ` 163` ``` from unbounded obtain n where "(Suc m)\n \ n\S" ``` paulson@14442 ` 164` ``` by blast ``` paulson@14442 ` 165` ``` hence "m n\S" by auto ``` paulson@14442 ` 166` ``` thus "\n. m < n \ n \ S" .. ``` paulson@14442 ` 167` ``` qed ``` paulson@14442 ` 168` ```qed ``` paulson@14442 ` 169` paulson@14442 ` 170` ```text {* ``` paulson@14442 ` 171` ``` For a set of natural numbers to be infinite, it is enough ``` wenzelm@14957 ` 172` ``` to know that for any number larger than some @{text k}, there ``` paulson@14442 ` 173` ``` is some larger number that is an element of the set. ``` paulson@14442 ` 174` ```*} ``` paulson@14442 ` 175` paulson@14442 ` 176` ```lemma unbounded_k_infinite: ``` paulson@14442 ` 177` ``` assumes k: "\m. k (\n. m n\S)" ``` paulson@14442 ` 178` ``` shows "infinite (S::nat set)" ``` paulson@14442 ` 179` ```proof (auto simp add: infinite_nat_iff_unbounded) ``` paulson@14442 ` 180` ``` fix m show "\n. m n\S" ``` paulson@14442 ` 181` ``` proof (cases "k n\S" by auto ``` paulson@14442 ` 187` ``` with False have "m n\S" by auto ``` paulson@14442 ` 188` ``` thus ?thesis .. ``` paulson@14442 ` 189` ``` qed ``` paulson@14442 ` 190` ```qed ``` paulson@14442 ` 191` paulson@14442 ` 192` ```theorem nat_infinite [simp]: ``` paulson@14442 ` 193` ``` "infinite (UNIV :: nat set)" ``` paulson@14442 ` 194` ```by (auto simp add: infinite_nat_iff_unbounded) ``` paulson@14442 ` 195` paulson@14442 ` 196` ```theorem nat_not_finite [elim]: ``` paulson@14442 ` 197` ``` "finite (UNIV::nat set) \ R" ``` paulson@14442 ` 198` ```by simp ``` paulson@14442 ` 199` paulson@14442 ` 200` ```text {* ``` paulson@14442 ` 201` ``` Every infinite set contains a countable subset. More precisely ``` wenzelm@14957 ` 202` ``` we show that a set @{text S} is infinite if and only if there exists ``` wenzelm@14957 ` 203` ``` an injective function from the naturals into @{text S}. ``` paulson@14442 ` 204` ```*} ``` paulson@14442 ` 205` paulson@14442 ` 206` ```lemma range_inj_infinite: ``` paulson@14442 ` 207` ``` "inj (f::nat \ 'a) \ infinite (range f)" ``` paulson@14442 ` 208` ```proof ``` paulson@14442 ` 209` ``` assume "inj f" ``` paulson@14442 ` 210` ``` and "finite (range f)" ``` paulson@14442 ` 211` ``` hence "finite (UNIV::nat set)" ``` paulson@14442 ` 212` ``` by (auto intro: finite_imageD simp del: nat_infinite) ``` paulson@14442 ` 213` ``` thus "False" by simp ``` paulson@14442 ` 214` ```qed ``` paulson@14442 ` 215` paulson@14442 ` 216` ```text {* ``` paulson@14442 ` 217` ``` The ``only if'' direction is harder because it requires the ``` paulson@14442 ` 218` ``` construction of a sequence of pairwise different elements of ``` wenzelm@14957 ` 219` ``` an infinite set @{text S}. The idea is to construct a sequence of ``` wenzelm@14957 ` 220` ``` non-empty and infinite subsets of @{text S} obtained by successively ``` wenzelm@14957 ` 221` ``` removing elements of @{text S}. ``` paulson@14442 ` 222` ```*} ``` paulson@14442 ` 223` paulson@14442 ` 224` ```lemma linorder_injI: ``` paulson@14442 ` 225` ``` assumes hyp: "\x y. x < (y::'a::linorder) \ f x \ f y" ``` paulson@14442 ` 226` ``` shows "inj f" ``` paulson@14442 ` 227` ```proof (rule inj_onI) ``` paulson@14442 ` 228` ``` fix x y ``` paulson@14442 ` 229` ``` assume f_eq: "f x = f y" ``` paulson@14442 ` 230` ``` show "x = y" ``` paulson@14442 ` 231` ``` proof (rule linorder_cases) ``` paulson@14442 ` 232` ``` assume "x < y" ``` paulson@14442 ` 233` ``` with hyp have "f x \ f y" by blast ``` paulson@14442 ` 234` ``` with f_eq show ?thesis by simp ``` paulson@14442 ` 235` ``` next ``` paulson@14442 ` 236` ``` assume "x = y" ``` paulson@14442 ` 237` ``` thus ?thesis . ``` paulson@14442 ` 238` ``` next ``` paulson@14442 ` 239` ``` assume "y < x" ``` paulson@14442 ` 240` ``` with hyp have "f y \ f x" by blast ``` paulson@14442 ` 241` ``` with f_eq show ?thesis by simp ``` paulson@14442 ` 242` ``` qed ``` paulson@14442 ` 243` ```qed ``` paulson@14442 ` 244` paulson@14442 ` 245` ```lemma infinite_countable_subset: ``` paulson@14442 ` 246` ``` assumes inf: "infinite (S::'a set)" ``` paulson@14442 ` 247` ``` shows "\f. inj (f::nat \ 'a) \ range f \ S" ``` paulson@14442 ` 248` ```proof - ``` wenzelm@14766 ` 249` ``` def Sseq \ "nat_rec S (\n T. T - {SOME e. e \ T})" ``` wenzelm@14766 ` 250` ``` def pick \ "\n. (SOME e. e \ Sseq n)" ``` paulson@14442 ` 251` ``` have Sseq_inf: "\n. infinite (Sseq n)" ``` paulson@14442 ` 252` ``` proof - ``` paulson@14442 ` 253` ``` fix n ``` paulson@14442 ` 254` ``` show "infinite (Sseq n)" ``` paulson@14442 ` 255` ``` proof (induct n) ``` paulson@14442 ` 256` ``` from inf show "infinite (Sseq 0)" ``` paulson@14442 ` 257` ``` by (simp add: Sseq_def) ``` paulson@14442 ` 258` ``` next ``` paulson@14442 ` 259` ``` fix n ``` paulson@14442 ` 260` ``` assume "infinite (Sseq n)" thus "infinite (Sseq (Suc n))" ``` paulson@14442 ` 261` ``` by (simp add: Sseq_def infinite_remove) ``` paulson@14442 ` 262` ``` qed ``` paulson@14442 ` 263` ``` qed ``` paulson@14442 ` 264` ``` have Sseq_S: "\n. Sseq n \ S" ``` paulson@14442 ` 265` ``` proof - ``` paulson@14442 ` 266` ``` fix n ``` paulson@14442 ` 267` ``` show "Sseq n \ S" ``` paulson@14442 ` 268` ``` by (induct n, auto simp add: Sseq_def) ``` paulson@14442 ` 269` ``` qed ``` paulson@14442 ` 270` ``` have Sseq_pick: "\n. pick n \ Sseq n" ``` paulson@14442 ` 271` ``` proof - ``` paulson@14442 ` 272` ``` fix n ``` paulson@14442 ` 273` ``` show "pick n \ Sseq n" ``` paulson@14442 ` 274` ``` proof (unfold pick_def, rule someI_ex) ``` paulson@14442 ` 275` ``` from Sseq_inf have "infinite (Sseq n)" . ``` paulson@14442 ` 276` ``` hence "Sseq n \ {}" by auto ``` paulson@14442 ` 277` ``` thus "\x. x \ Sseq n" by auto ``` paulson@14442 ` 278` ``` qed ``` paulson@14442 ` 279` ``` qed ``` paulson@14442 ` 280` ``` with Sseq_S have rng: "range pick \ S" ``` paulson@14442 ` 281` ``` by auto ``` paulson@14442 ` 282` ``` have pick_Sseq_gt: "\n m. pick n \ Sseq (n + Suc m)" ``` paulson@14442 ` 283` ``` proof - ``` paulson@14442 ` 284` ``` fix n m ``` paulson@14442 ` 285` ``` show "pick n \ Sseq (n + Suc m)" ``` paulson@14442 ` 286` ``` by (induct m, auto simp add: Sseq_def pick_def) ``` paulson@14442 ` 287` ``` qed ``` paulson@14442 ` 288` ``` have pick_pick: "\n m. pick n \ pick (n + Suc m)" ``` paulson@14442 ` 289` ``` proof - ``` paulson@14442 ` 290` ``` fix n m ``` paulson@14442 ` 291` ``` from Sseq_pick have "pick (n + Suc m) \ Sseq (n + Suc m)" . ``` paulson@14442 ` 292` ``` moreover from pick_Sseq_gt ``` paulson@14442 ` 293` ``` have "pick n \ Sseq (n + Suc m)" . ``` paulson@14442 ` 294` ``` ultimately show "pick n \ pick (n + Suc m)" ``` paulson@14442 ` 295` ``` by auto ``` paulson@14442 ` 296` ``` qed ``` paulson@14442 ` 297` ``` have inj: "inj pick" ``` paulson@14442 ` 298` ``` proof (rule linorder_injI) ``` paulson@14442 ` 299` ``` show "\i j. i<(j::nat) \ pick i \ pick j" ``` paulson@14442 ` 300` ``` proof (clarify) ``` paulson@14442 ` 301` ``` fix i j ``` paulson@14442 ` 302` ``` assume ij: "i<(j::nat)" ``` paulson@14442 ` 303` ``` and eq: "pick i = pick j" ``` paulson@14442 ` 304` ``` from ij obtain k where "j = i + (Suc k)" ``` paulson@14442 ` 305` ``` by (auto simp add: less_iff_Suc_add) ``` paulson@14442 ` 306` ``` with pick_pick have "pick i \ pick j" by simp ``` paulson@14442 ` 307` ``` with eq show "False" by simp ``` paulson@14442 ` 308` ``` qed ``` paulson@14442 ` 309` ``` qed ``` paulson@14442 ` 310` ``` from rng inj show ?thesis by auto ``` paulson@14442 ` 311` ```qed ``` paulson@14442 ` 312` paulson@14442 ` 313` ```theorem infinite_iff_countable_subset: ``` paulson@14442 ` 314` ``` "infinite S = (\f. inj (f::nat \ 'a) \ range f \ S)" ``` paulson@14442 ` 315` ``` (is "?lhs = ?rhs") ``` paulson@14442 ` 316` ```by (auto simp add: infinite_countable_subset ``` paulson@14442 ` 317` ``` range_inj_infinite infinite_super) ``` paulson@14442 ` 318` paulson@14442 ` 319` ```text {* ``` paulson@14442 ` 320` ``` For any function with infinite domain and finite range ``` paulson@14442 ` 321` ``` there is some element that is the image of infinitely ``` paulson@14442 ` 322` ``` many domain elements. In particular, any infinite sequence ``` paulson@14442 ` 323` ``` of elements from a finite set contains some element that ``` paulson@14442 ` 324` ``` occurs infinitely often. ``` paulson@14442 ` 325` ```*} ``` paulson@14442 ` 326` paulson@14442 ` 327` ```theorem inf_img_fin_dom: ``` paulson@14442 ` 328` ``` assumes img: "finite (f`A)" and dom: "infinite A" ``` paulson@14442 ` 329` ``` shows "\y \ f`A. infinite (f -` {y})" ``` paulson@14442 ` 330` ```proof (rule ccontr) ``` paulson@14442 ` 331` ``` assume "\ (\y\f ` A. infinite (f -` {y}))" ``` paulson@14442 ` 332` ``` with img have "finite (UN y:f`A. f -` {y})" ``` paulson@14442 ` 333` ``` by (blast intro: finite_UN_I) ``` paulson@14442 ` 334` ``` moreover have "A \ (UN y:f`A. f -` {y})" by auto ``` paulson@14442 ` 335` ``` moreover note dom ``` paulson@14442 ` 336` ``` ultimately show "False" ``` paulson@14442 ` 337` ``` by (simp add: infinite_super) ``` paulson@14442 ` 338` ```qed ``` paulson@14442 ` 339` paulson@14442 ` 340` ```theorems inf_img_fin_domE = inf_img_fin_dom[THEN bexE] ``` paulson@14442 ` 341` paulson@14442 ` 342` paulson@14442 ` 343` ```subsection "Infinitely Many and Almost All" ``` paulson@14442 ` 344` paulson@14442 ` 345` ```text {* ``` paulson@14442 ` 346` ``` We often need to reason about the existence of infinitely many ``` paulson@14442 ` 347` ``` (resp., all but finitely many) objects satisfying some predicate, ``` paulson@14442 ` 348` ``` so we introduce corresponding binders and their proof rules. ``` paulson@14442 ` 349` ```*} ``` paulson@14442 ` 350` paulson@14442 ` 351` ```consts ``` paulson@14442 ` 352` ``` Inf_many :: "('a \ bool) \ bool" (binder "INF " 10) ``` paulson@14442 ` 353` ``` Alm_all :: "('a \ bool) \ bool" (binder "MOST " 10) ``` paulson@14442 ` 354` paulson@14442 ` 355` ```defs ``` paulson@14442 ` 356` ``` INF_def: "Inf_many P \ infinite {x. P x}" ``` paulson@14442 ` 357` ``` MOST_def: "Alm_all P \ \(INF x. \ P x)" ``` paulson@14442 ` 358` paulson@14442 ` 359` ```syntax (xsymbols) ``` paulson@14442 ` 360` ``` "MOST " :: "[idts, bool] \ bool" ("(3\\<^sub>\_./ _)" [0,10] 10) ``` paulson@14442 ` 361` ``` "INF " :: "[idts, bool] \ bool" ("(3\\<^sub>\_./ _)" [0,10] 10) ``` paulson@14442 ` 362` kleing@14565 ` 363` ```syntax (HTML output) ``` kleing@14565 ` 364` ``` "MOST " :: "[idts, bool] \ bool" ("(3\\<^sub>\_./ _)" [0,10] 10) ``` kleing@14565 ` 365` ``` "INF " :: "[idts, bool] \ bool" ("(3\\<^sub>\_./ _)" [0,10] 10) ``` kleing@14565 ` 366` paulson@14442 ` 367` ```lemma INF_EX: ``` paulson@14442 ` 368` ``` "(\\<^sub>\x. P x) \ (\x. P x)" ``` paulson@14442 ` 369` ```proof (unfold INF_def, rule ccontr) ``` paulson@14442 ` 370` ``` assume inf: "infinite {x. P x}" ``` paulson@14442 ` 371` ``` and notP: "\(\x. P x)" ``` paulson@14442 ` 372` ``` from notP have "{x. P x} = {}" by simp ``` paulson@14442 ` 373` ``` hence "finite {x. P x}" by simp ``` paulson@14442 ` 374` ``` with inf show "False" by simp ``` paulson@14442 ` 375` ```qed ``` paulson@14442 ` 376` paulson@14442 ` 377` ```lemma MOST_iff_finiteNeg: ``` paulson@14442 ` 378` ``` "(\\<^sub>\x. P x) = finite {x. \ P x}" ``` paulson@14442 ` 379` ```by (simp add: MOST_def INF_def) ``` paulson@14442 ` 380` paulson@14442 ` 381` ```lemma ALL_MOST: ``` paulson@14442 ` 382` ``` "\x. P x \ \\<^sub>\x. P x" ``` paulson@14442 ` 383` ```by (simp add: MOST_iff_finiteNeg) ``` paulson@14442 ` 384` paulson@14442 ` 385` ```lemma INF_mono: ``` paulson@14442 ` 386` ``` assumes inf: "\\<^sub>\x. P x" and q: "\x. P x \ Q x" ``` paulson@14442 ` 387` ``` shows "\\<^sub>\x. Q x" ``` paulson@14442 ` 388` ```proof - ``` paulson@14442 ` 389` ``` from inf have "infinite {x. P x}" by (unfold INF_def) ``` paulson@14442 ` 390` ``` moreover from q have "{x. P x} \ {x. Q x}" by auto ``` paulson@14442 ` 391` ``` ultimately show ?thesis ``` paulson@14442 ` 392` ``` by (simp add: INF_def infinite_super) ``` paulson@14442 ` 393` ```qed ``` paulson@14442 ` 394` paulson@14442 ` 395` ```lemma MOST_mono: ``` paulson@14442 ` 396` ``` "\ \\<^sub>\x. P x; \x. P x \ Q x \ \ \\<^sub>\x. Q x" ``` paulson@14442 ` 397` ```by (unfold MOST_def, blast intro: INF_mono) ``` paulson@14442 ` 398` paulson@14442 ` 399` ```lemma INF_nat: "(\\<^sub>\n. P (n::nat)) = (\m. \n. m P n)" ``` paulson@14442 ` 400` ```by (simp add: INF_def infinite_nat_iff_unbounded) ``` paulson@14442 ` 401` paulson@14442 ` 402` ```lemma INF_nat_le: "(\\<^sub>\n. P (n::nat)) = (\m. \n. m\n \ P n)" ``` paulson@14442 ` 403` ```by (simp add: INF_def infinite_nat_iff_unbounded_le) ``` paulson@14442 ` 404` paulson@14442 ` 405` ```lemma MOST_nat: "(\\<^sub>\n. P (n::nat)) = (\m. \n. m P n)" ``` paulson@14442 ` 406` ```by (simp add: MOST_def INF_nat) ``` paulson@14442 ` 407` paulson@14442 ` 408` ```lemma MOST_nat_le: "(\\<^sub>\n. P (n::nat)) = (\m. \n. m\n \ P n)" ``` paulson@14442 ` 409` ```by (simp add: MOST_def INF_nat_le) ``` paulson@14442 ` 410` paulson@14442 ` 411` paulson@14442 ` 412` ```subsection "Miscellaneous" ``` paulson@14442 ` 413` paulson@14442 ` 414` ```text {* ``` paulson@14442 ` 415` ``` A few trivial lemmas about sets that contain at most one element. ``` paulson@14442 ` 416` ``` These simplify the reasoning about deterministic automata. ``` paulson@14442 ` 417` ```*} ``` paulson@14442 ` 418` paulson@14442 ` 419` ```constdefs ``` paulson@14442 ` 420` ``` atmost_one :: "'a set \ bool" ``` paulson@14442 ` 421` ``` "atmost_one S \ \x y. x\S \ y\S \ x=y" ``` paulson@14442 ` 422` paulson@14442 ` 423` ```lemma atmost_one_empty: "S={} \ atmost_one S" ``` paulson@14442 ` 424` ```by (simp add: atmost_one_def) ``` paulson@14442 ` 425` paulson@14442 ` 426` ```lemma atmost_one_singleton: "S = {x} \ atmost_one S" ``` paulson@14442 ` 427` ```by (simp add: atmost_one_def) ``` paulson@14442 ` 428` paulson@14442 ` 429` ```lemma atmost_one_unique [elim]: "\ atmost_one S; x \ S; y \ S \ \ y=x" ``` paulson@14442 ` 430` ```by (simp add: atmost_one_def) ``` paulson@14442 ` 431` paulson@14442 ` 432` ```end ```