# HG changeset patch # User paulson # Date 1621430260 -3600 # Node ID 58bd53caf8006dbd221a4dd7cef7aa8be8f30794 # Parent 2e3a60ce5a9f9e9cbc803bcb8202fdc3af2d35f2 things need to be ugly diff -r 2e3a60ce5a9f -r 58bd53caf800 src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Tue May 18 20:25:19 2021 +0100 +++ b/src/HOL/Library/Ramsey.thy Wed May 19 14:17:40 2021 +0100 @@ -10,6 +10,9 @@ subsection \Preliminary definitions\ +abbreviation strict_sorted :: "'a::linorder list \ bool" where + "strict_sorted \ sorted_wrt (<)" + subsubsection \The $n$-element subsets of a set $A$\ definition nsets :: "['a set, nat] \ 'a set set" ("([_]\<^bsup>_\<^esup>)" [0,999] 999) @@ -992,7 +995,7 @@ then show "(s ?j, s ?i) \ T k" by (simp add: k transition_idx_in ij) qed then have "\ wf (T k)" - by (meson wf_iff_no_infinite_down_chain) + unfolding wf_iff_no_infinite_down_chain by iprover with wfT \k < n\ show False by blast qed diff -r 2e3a60ce5a9f -r 58bd53caf800 src/HOL/List.thy --- a/src/HOL/List.thy Tue May 18 20:25:19 2021 +0100 +++ b/src/HOL/List.thy Wed May 19 14:17:40 2021 +0100 @@ -373,13 +373,10 @@ abbreviation sorted :: "'a list \ bool" where "sorted \ sorted_wrt (\)" -abbreviation strict_sorted :: "'a list \ bool" where - "strict_sorted \ sorted_wrt (<)" - lemma sorted_simps: "sorted [] = True" "sorted (x # ys) = ((\y \ set ys. x\y) \ sorted ys)" by auto -lemma strict_sorted_simps: "strict_sorted [] = True" "strict_sorted (x # ys) = ((\y \ set ys. x strict_sorted ys)" +lemma strict_sorted_simps: "sorted_wrt (<) [] = True" "sorted_wrt (<) (x # ys) = ((\y \ set ys. x sorted_wrt (<) ys)" by auto primrec insort_key :: "('b \ 'a) \ 'b \ 'b list \ 'b list" where @@ -402,10 +399,10 @@ "stable_sort_key sk = (\f xs k. filter (\y. f y = k) (sk f xs) = filter (\y. f y = k) xs)" -lemma strict_sorted_iff: "strict_sorted l \ sorted l \ distinct l" +lemma strict_sorted_iff: "sorted_wrt (<) l \ sorted l \ distinct l" by (induction l) (auto iff: antisym_conv1) -lemma strict_sorted_imp_sorted: "strict_sorted xs \ sorted xs" +lemma strict_sorted_imp_sorted: "sorted_wrt (<) xs \ sorted xs" by (auto simp: strict_sorted_iff) end @@ -6169,17 +6166,17 @@ with assms show ?thesis by simp qed -lemma strict_sorted_list_of_set [simp]: "strict_sorted (sorted_list_of_set A)" +lemma strict_sorted_list_of_set [simp]: "sorted_wrt (<) (sorted_list_of_set A)" by (simp add: strict_sorted_iff) lemma finite_set_strict_sorted: assumes "finite A" - obtains l where "strict_sorted l" "set l = A" "length l = card A" + obtains l where "sorted_wrt (<) l" "set l = A" "length l = card A" by (metis assms distinct_card distinct_sorted_list_of_set set_sorted_list_of_set strict_sorted_list_of_set) lemma strict_sorted_equal: - assumes "strict_sorted xs" - and "strict_sorted ys" + assumes "sorted_wrt (<) xs" + and "sorted_wrt (<) ys" and "set ys = set xs" shows "ys = xs" using assms @@ -6201,7 +6198,7 @@ qed qed auto -lemma strict_sorted_equal_Uniq: "\\<^sub>\\<^sub>1xs. strict_sorted xs \ set xs = A" +lemma strict_sorted_equal_Uniq: "\\<^sub>\\<^sub>1xs. sorted_wrt (<) xs \ set xs = A" by (simp add: Uniq_def strict_sorted_equal) lemma sorted_list_of_set_inject: @@ -6211,7 +6208,7 @@ lemma sorted_list_of_set_unique: assumes "finite A" - shows "strict_sorted l \ set l = A \ length l = card A \ sorted_list_of_set A = l" + shows "sorted_wrt (<) l \ set l = A \ length l = card A \ sorted_list_of_set A = l" using assms strict_sorted_equal by force end