summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson <lp15@cam.ac.uk> |

Wed, 19 May 2021 14:17:40 +0100 | |

changeset 73709 | 58bd53caf800 |

parent 73708 | 2e3a60ce5a9f |

child 73772 | 6b4c47666267 |

things need to be ugly

src/HOL/Library/Ramsey.thy | file | annotate | diff | comparison | revisions | |

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- 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 \<open>Preliminary definitions\<close> +abbreviation strict_sorted :: "'a::linorder list \<Rightarrow> bool" where + "strict_sorted \<equiv> sorted_wrt (<)" + subsubsection \<open>The $n$-element subsets of a set $A$\<close> definition nsets :: "['a set, nat] \<Rightarrow> 'a set set" ("([_]\<^bsup>_\<^esup>)" [0,999] 999) @@ -992,7 +995,7 @@ then show "(s ?j, s ?i) \<in> T k" by (simp add: k transition_idx_in ij) qed then have "\<not> wf (T k)" - by (meson wf_iff_no_infinite_down_chain) + unfolding wf_iff_no_infinite_down_chain by iprover with wfT \<open>k < n\<close> show False by blast qed

--- 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 \<Rightarrow> bool" where "sorted \<equiv> sorted_wrt (\<le>)" -abbreviation strict_sorted :: "'a list \<Rightarrow> bool" where - "strict_sorted \<equiv> sorted_wrt (<)" - lemma sorted_simps: "sorted [] = True" "sorted (x # ys) = ((\<forall>y \<in> set ys. x\<le>y) \<and> sorted ys)" by auto -lemma strict_sorted_simps: "strict_sorted [] = True" "strict_sorted (x # ys) = ((\<forall>y \<in> set ys. x<y) \<and> strict_sorted ys)" +lemma strict_sorted_simps: "sorted_wrt (<) [] = True" "sorted_wrt (<) (x # ys) = ((\<forall>y \<in> set ys. x<y) \<and> sorted_wrt (<) ys)" by auto primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where @@ -402,10 +399,10 @@ "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" +lemma strict_sorted_iff: "sorted_wrt (<) l \<longleftrightarrow> sorted l \<and> distinct l" by (induction l) (auto iff: antisym_conv1) -lemma strict_sorted_imp_sorted: "strict_sorted xs \<Longrightarrow> sorted xs" +lemma strict_sorted_imp_sorted: "sorted_wrt (<) xs \<Longrightarrow> 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: "\<exists>\<^sub>\<le>\<^sub>1xs. strict_sorted xs \<and> set xs = A" +lemma strict_sorted_equal_Uniq: "\<exists>\<^sub>\<le>\<^sub>1xs. sorted_wrt (<) xs \<and> 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 \<and> set l = A \<and> length l = card A \<longleftrightarrow> sorted_list_of_set A = l" + shows "sorted_wrt (<) l \<and> set l = A \<and> length l = card A \<longleftrightarrow> sorted_list_of_set A = l" using assms strict_sorted_equal by force end