# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1596651128 -3600
# Node ID cfb6c22a563616a80a36361877c08b11581615ef
# Parent  beccb2a0410f00e35d227dea8043a786a00d6a5d
lemmas about sets and the enumerate operator

diff -r beccb2a0410f -r cfb6c22a5636 src/HOL/Finite_Set.thy
--- 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
diff -r beccb2a0410f -r cfb6c22a5636 src/HOL/Library/Infinite_Set.thy
--- 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"
diff -r beccb2a0410f -r cfb6c22a5636 src/HOL/List.thy
--- 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>