merged
authorpaulson
Mon Aug 03 11:46:19 2020 +0100 (6 weeks ago ago)
changeset 72312b6065cbbf5e2
parent 72311 8c355e2dd7db
parent 72310 5d17e7a0825a
child 72314 3f8e6c0166ac
merged
     1.1 --- a/src/HOL/Groups_Big.thy	Sat Aug 01 17:43:30 2020 +0000
     1.2 +++ b/src/HOL/Groups_Big.thy	Mon Aug 03 11:46:19 2020 +0100
     1.3 @@ -165,6 +165,11 @@
     1.4    shows "F g A = F h B"
     1.5    using assms by (simp add: reindex)
     1.6  
     1.7 +lemma image_eq:
     1.8 +  assumes "inj_on g A"  
     1.9 +  shows "F (\<lambda>x. x) (g ` A) = F g A"
    1.10 +  using assms reindex_cong by fastforce
    1.11 +
    1.12  lemma UNION_disjoint:
    1.13    assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
    1.14      and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
     2.1 --- a/src/HOL/Library/Infinite_Set.thy	Sat Aug 01 17:43:30 2020 +0000
     2.2 +++ b/src/HOL/Library/Infinite_Set.thy	Mon Aug 03 11:46:19 2020 +0100
     2.3 @@ -484,7 +484,7 @@
     2.4  
     2.5  lemma finite_enumerate_initial_segment:
     2.6    fixes S :: "'a::wellorder set"
     2.7 -  assumes "finite S" "s \<in> S" and n: "n < card (S \<inter> {..<s})"
     2.8 +  assumes "finite S" and n: "n < card (S \<inter> {..<s})"
     2.9    shows "enumerate (S \<inter> {..<s}) n = enumerate S n"
    2.10    using n
    2.11  proof (induction n)
    2.12 @@ -502,18 +502,20 @@
    2.13    case (Suc n)
    2.14    then have less_card: "Suc n < card S"
    2.15      by (meson assms(1) card_mono inf_sup_ord(1) leD le_less_linear order.trans)
    2.16 -  obtain t where t: "t \<in> {s \<in> S. enumerate S n < s}"
    2.17 +  obtain T where T: "T \<in> {s \<in> S. enumerate S n < s}"
    2.18      by (metis Infinite_Set.enumerate_step enumerate_in_set finite_enumerate_in_set finite_enumerate_step less_card mem_Collect_eq)
    2.19 -  have "(LEAST x. x \<in> S \<and> x < s \<and> enumerate S n < x) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
    2.20 +  have "(LEAST x. x \<in> S \<and> x < s \<and> enumerate S n < x) = (LEAST x. x \<in> S \<and> enumerate S n < x)"
    2.21         (is "_ = ?r")
    2.22    proof (intro Least_equality conjI)
    2.23      show "?r \<in> S"
    2.24 -      by (metis (mono_tags, lifting) LeastI mem_Collect_eq t)
    2.25 -    show "?r < s"
    2.26 -      using not_less_Least [of _ "\<lambda>t. t \<in> S \<and> enumerate S n < t"] Suc assms 
    2.27 -      by (metis (no_types, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def linorder_cases)
    2.28 +      by (metis (mono_tags, lifting) LeastI mem_Collect_eq T)
    2.29 +    have "\<not> s \<le> ?r"
    2.30 +      using not_less_Least [of _ "\<lambda>x. x \<in> S \<and> enumerate S n < x"] Suc assms
    2.31 +      by (metis (mono_tags, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def less_le_trans)
    2.32 +    then show "?r < s"
    2.33 +      by auto
    2.34      show "enumerate S n < ?r"
    2.35 -      by (metis (no_types, lifting) LeastI mem_Collect_eq t)
    2.36 +      by (metis (no_types, lifting) LeastI mem_Collect_eq T)
    2.37    qed (auto simp: Least_le)
    2.38    then show ?case
    2.39      using Suc assms by (simp add: finite_enumerate_Suc'' less_card)