--- 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
--- 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"
--- 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"
--- 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>