# HG changeset patch
# User paulson
# Date 1596657811 -3600
# Node ID 6b5421bd0fc365340f7e2b80c2b32255167a6e4c
# Parent  a36db1c8238e0d419a42635e0d04a5017ca6a024# Parent  cfb6c22a563616a80a36361877c08b11581615ef
merged

diff -r a36db1c8238e -r 6b5421bd0fc3 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Aug 05 19:06:39 2020 +0200
+++ b/src/HOL/Finite_Set.thy	Wed Aug 05 21:03:31 2020 +0100
@@ -1492,6 +1492,9 @@
 lemma card_Un_disjoint: "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> card (A \<union> B) = card A + card B"
   using card_Un_Int [of A B] by simp
 
+lemma card_Un_disjnt: "\<lbrakk>finite A; finite B; disjnt A B\<rbrakk> \<Longrightarrow> card (A \<union> B) = card A + card B"
+  by (simp add: card_Un_disjoint disjnt_def)
+
 lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
 proof (cases "finite A \<and> finite B")
   case True
diff -r a36db1c8238e -r 6b5421bd0fc3 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Aug 05 19:06:39 2020 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Aug 05 21:03:31 2020 +0100
@@ -165,6 +165,11 @@
   shows "F g A = F h B"
   using assms by (simp add: reindex)
 
+lemma image_eq:
+  assumes "inj_on g A"  
+  shows "F (\<lambda>x. x) (g ` A) = F g A"
+  using assms reindex_cong by fastforce
+
 lemma UNION_disjoint:
   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
@@ -1065,6 +1070,21 @@
   finally show ?thesis .
 qed
 
+lemma sum_strict_mono2:
+  fixes f :: "'a \<Rightarrow> 'b::ordered_cancel_comm_monoid_add"
+  assumes "finite B" "A \<subseteq> B" "b \<in> B-A" "f b > 0" and "\<And>x. x \<in> B \<Longrightarrow> f x \<ge> 0"
+  shows "sum f A < sum f B"
+proof -
+  have "B - A \<noteq> {}"
+    using assms(3) by blast
+  have "sum f (B-A) > 0"
+    by (rule sum_pos2) (use assms in auto)
+  moreover have "sum f B = sum f (B-A) + sum f A"
+    by (rule sum.subset_diff) (use assms in auto)
+  ultimately show ?thesis
+    using add_strict_increasing by auto
+qed
+
 lemma sum_cong_Suc:
   assumes "0 \<notin> A" "\<And>x. Suc x \<in> A \<Longrightarrow> f (Suc x) = g (Suc x)"
   shows "sum f A = sum g A"
diff -r a36db1c8238e -r 6b5421bd0fc3 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Wed Aug 05 19:06:39 2020 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Wed Aug 05 21:03:31 2020 +0100
@@ -263,6 +263,10 @@
 lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   by (induct m n rule: less_Suc_induct) (auto intro: enumerate_step)
 
+lemma enumerate_mono_iff [simp]:
+  "infinite S \<Longrightarrow> enumerate S m < enumerate S n \<longleftrightarrow> m < n"
+  by (metis enumerate_mono less_asym less_linear)
+
 lemma le_enumerate:
   assumes S: "infinite S"
   shows "n \<le> enumerate S n"
@@ -281,7 +285,7 @@
   assumes fS: "infinite S"
   shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. r n \<in> S)"
   unfolding strict_mono_def
-  using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
+  using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by blast
 
 lemma enumerate_Suc'':
   fixes S :: "'a::wellorder set"
@@ -435,6 +439,9 @@
 lemma finite_enumerate_mono: "\<lbrakk>m < n; finite S; n < card S\<rbrakk> \<Longrightarrow> enumerate S m < enumerate S n"
   by (induct m n rule: less_Suc_induct) (auto intro: finite_enumerate_step)
 
+lemma finite_enumerate_mono_iff [simp]:
+  "\<lbrakk>finite S; m < card S; n < card S\<rbrakk> \<Longrightarrow> enumerate S m < enumerate S n \<longleftrightarrow> m < n"
+  by (metis finite_enumerate_mono less_asym less_linear)
 
 lemma finite_le_enumerate:
   assumes "finite S" "n < card S"
@@ -484,7 +491,7 @@
 
 lemma finite_enumerate_initial_segment:
   fixes S :: "'a::wellorder set"
-  assumes "finite S" "s \<in> S" and n: "n < card (S \<inter> {..<s})"
+  assumes "finite S" and n: "n < card (S \<inter> {..<s})"
   shows "enumerate (S \<inter> {..<s}) n = enumerate S n"
   using n
 proof (induction n)
@@ -502,18 +509,20 @@
   case (Suc n)
   then have less_card: "Suc n < card S"
     by (meson assms(1) card_mono inf_sup_ord(1) leD le_less_linear order.trans)
-  obtain t where t: "t \<in> {s \<in> S. enumerate S n < s}"
+  obtain T where T: "T \<in> {s \<in> S. enumerate S n < s}"
     by (metis Infinite_Set.enumerate_step enumerate_in_set finite_enumerate_in_set finite_enumerate_step less_card mem_Collect_eq)
-  have "(LEAST x. x \<in> S \<and> x < s \<and> enumerate S n < x) = (LEAST s. s \<in> S \<and> enumerate S n < s)"
+  have "(LEAST x. x \<in> S \<and> x < s \<and> enumerate S n < x) = (LEAST x. x \<in> S \<and> enumerate S n < x)"
        (is "_ = ?r")
   proof (intro Least_equality conjI)
     show "?r \<in> S"
-      by (metis (mono_tags, lifting) LeastI mem_Collect_eq t)
-    show "?r < s"
-      using not_less_Least [of _ "\<lambda>t. t \<in> S \<and> enumerate S n < t"] Suc assms 
-      by (metis (no_types, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def linorder_cases)
+      by (metis (mono_tags, lifting) LeastI mem_Collect_eq T)
+    have "\<not> s \<le> ?r"
+      using not_less_Least [of _ "\<lambda>x. x \<in> S \<and> enumerate S n < x"] Suc assms
+      by (metis (mono_tags, lifting) Int_Collect Suc_lessD finite_Int finite_enumerate_in_set finite_enumerate_step lessThan_def less_le_trans)
+    then show "?r < s"
+      by auto
     show "enumerate S n < ?r"
-      by (metis (no_types, lifting) LeastI mem_Collect_eq t)
+      by (metis (no_types, lifting) LeastI mem_Collect_eq T)
   qed (auto simp: Least_le)
   then show ?case
     using Suc assms by (simp add: finite_enumerate_Suc'' less_card)
@@ -558,6 +567,16 @@
   qed
 qed
 
+lemma finite_enum_subset:
+  assumes "\<And>i. i < card X \<Longrightarrow> enumerate X i = enumerate Y i" and "finite X" "finite Y" "card X \<le> card Y"
+  shows "X \<subseteq> Y"
+  by (metis assms finite_enumerate_Ex finite_enumerate_in_set less_le_trans subsetI)
+
+lemma finite_enum_ext:
+  assumes "\<And>i. i < card X \<Longrightarrow> enumerate X i = enumerate Y i" and "finite X" "finite Y" "card X = card Y"
+  shows "X = Y"
+  by (intro antisym finite_enum_subset) (auto simp: assms)
+
 lemma finite_bij_enumerate:
   fixes S :: "'a::wellorder set"
   assumes S: "finite S"
diff -r a36db1c8238e -r 6b5421bd0fc3 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 05 19:06:39 2020 +0200
+++ b/src/HOL/List.thy	Wed Aug 05 21:03:31 2020 +0100
@@ -391,15 +391,15 @@
 qed
 
 primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-"insort_key f x [] = [x]" |
-"insort_key f x (y#ys) =
+  "insort_key f x [] = [x]" |
+  "insort_key f x (y#ys) =
   (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
 
 definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-"sort_key f xs = foldr (insort_key f) xs []"
+  "sort_key f xs = foldr (insort_key f) xs []"
 
 definition insort_insert_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-"insort_insert_key f x xs =
+  "insort_insert_key f x xs =
   (if f x \<in> f ` set xs then xs else insort_key f x xs)"
 
 abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
@@ -407,11 +407,14 @@
 abbreviation "insort_insert \<equiv> insort_insert_key (\<lambda>x. x)"
 
 definition stable_sort_key :: "(('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list) \<Rightarrow> bool" where
-"stable_sort_key sk =
+  "stable_sort_key sk =
    (\<forall>f xs k. filter (\<lambda>y. f y = k) (sk f xs) = filter (\<lambda>y. f y = k) xs)"
 
 lemma strict_sorted_iff: "strict_sorted l \<longleftrightarrow> sorted l \<and> distinct l"
-by (induction l) (auto iff: antisym_conv1)
+  by (induction l) (auto iff: antisym_conv1)
+
+lemma strict_sorted_imp_sorted: "strict_sorted xs \<Longrightarrow> sorted xs"
+  by (auto simp: strict_sorted_iff)
 
 end
 
@@ -6152,6 +6155,11 @@
   "sorted_list_of_set {..Suc k} = sorted_list_of_set {..k} @ [Suc k]"
   using lessThan_Suc_atMost sorted_list_of_set_lessThan_Suc by fastforce
 
+lemma sorted_list_of_set_nonempty:
+  assumes "finite A" "A \<noteq> {}"
+  shows "sorted_list_of_set A = Min A # sorted_list_of_set (A - {Min A})"
+  using assms by (auto simp: less_le simp flip: sorted_list_of_set_unique intro: Min_in)
+
 lemma sorted_list_of_set_greaterThanLessThan:
   assumes "Suc i < j" 
     shows "sorted_list_of_set {i<..<j} = Suc i # sorted_list_of_set {Suc i<..<j}"
@@ -6525,6 +6533,9 @@
 lemma irrefl_lex: "irrefl r \<Longrightarrow> irrefl (lex r)"
   by (meson irrefl_def lex_take_index)
 
+lemma lexl_not_refl [simp]: "irrefl r \<Longrightarrow> (x,x) \<notin> lex r"
+  by (meson irrefl_def lex_take_index)
+
 
 subsubsection \<open>Lexicographic Ordering\<close>