482 by (auto simp flip: enumerate_Suc') |
482 by (auto simp flip: enumerate_Suc') |
483 qed |
483 qed |
484 |
484 |
485 lemma finite_enumerate_initial_segment: |
485 lemma finite_enumerate_initial_segment: |
486 fixes S :: "'a::wellorder set" |
486 fixes S :: "'a::wellorder set" |
487 assumes "finite S" "s \<in> S" and n: "n < card (S \<inter> {..<s})" |
487 assumes "finite S" and n: "n < card (S \<inter> {..<s})" |
488 shows "enumerate (S \<inter> {..<s}) n = enumerate S n" |
488 shows "enumerate (S \<inter> {..<s}) n = enumerate S n" |
489 using n |
489 using n |
490 proof (induction n) |
490 proof (induction n) |
491 case 0 |
491 case 0 |
492 have "(LEAST n. n \<in> S \<and> n < s) = (LEAST n. n \<in> S)" |
492 have "(LEAST n. n \<in> S \<and> n < s) = (LEAST n. n \<in> S)" |
500 by (auto simp: enumerate_0) |
500 by (auto simp: enumerate_0) |
501 next |
501 next |
502 case (Suc n) |
502 case (Suc n) |
503 then have less_card: "Suc n < card S" |
503 then have less_card: "Suc n < card S" |
504 by (meson assms(1) card_mono inf_sup_ord(1) leD le_less_linear order.trans) |
504 by (meson assms(1) card_mono inf_sup_ord(1) leD le_less_linear order.trans) |
505 obtain t where t: "t \<in> {s \<in> S. enumerate S n < s}" |
505 obtain T where T: "T \<in> {s \<in> S. enumerate S n < s}" |
506 by (metis Infinite_Set.enumerate_step enumerate_in_set finite_enumerate_in_set finite_enumerate_step less_card mem_Collect_eq) |
506 by (metis Infinite_Set.enumerate_step enumerate_in_set finite_enumerate_in_set finite_enumerate_step less_card mem_Collect_eq) |
507 have "(LEAST x. x \<in> S \<and> x < s \<and> enumerate S n < x) = (LEAST s. s \<in> S \<and> enumerate S n < s)" |
507 have "(LEAST x. x \<in> S \<and> x < s \<and> enumerate S n < x) = (LEAST x. x \<in> S \<and> enumerate S n < x)" |
508 (is "_ = ?r") |
508 (is "_ = ?r") |
509 proof (intro Least_equality conjI) |
509 proof (intro Least_equality conjI) |
510 show "?r \<in> S" |
510 show "?r \<in> S" |
511 by (metis (mono_tags, lifting) LeastI mem_Collect_eq t) |
511 by (metis (mono_tags, lifting) LeastI mem_Collect_eq T) |
512 show "?r < s" |
512 have "\<not> s \<le> ?r" |
513 using not_less_Least [of _ "\<lambda>t. t \<in> S \<and> enumerate S n < t"] Suc assms |
513 using not_less_Least [of _ "\<lambda>x. x \<in> S \<and> enumerate S n < x"] Suc assms |
514 by (metis (no_types, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def linorder_cases) |
514 by (metis (mono_tags, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def less_le_trans) |
|
515 then show "?r < s" |
|
516 by auto |
515 show "enumerate S n < ?r" |
517 show "enumerate S n < ?r" |
516 by (metis (no_types, lifting) LeastI mem_Collect_eq t) |
518 by (metis (no_types, lifting) LeastI mem_Collect_eq T) |
517 qed (auto simp: Least_le) |
519 qed (auto simp: Least_le) |
518 then show ?case |
520 then show ?case |
519 using Suc assms by (simp add: finite_enumerate_Suc'' less_card) |
521 using Suc assms by (simp add: finite_enumerate_Suc'' less_card) |
520 qed |
522 qed |
521 |
523 |