--- a/src/HOL/Finite_Set.thy Wed Aug 05 17:56:33 2020 +0100
+++ b/src/HOL/Finite_Set.thy Wed Aug 05 19:12:08 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/Library/Infinite_Set.thy Wed Aug 05 17:56:33 2020 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Wed Aug 05 19:12:08 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"
@@ -560,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 17:56:33 2020 +0100
+++ b/src/HOL/List.thy Wed Aug 05 19:12:08 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>