equal
deleted
inserted
replaced
4928 by simp |
4928 by simp |
4929 |
4929 |
4930 |
4930 |
4931 subsection \<open>Sorting\<close> |
4931 subsection \<open>Sorting\<close> |
4932 |
4932 |
4933 |
|
4934 subsubsection \<open>@{const sorted_wrt}\<close> |
4933 subsubsection \<open>@{const sorted_wrt}\<close> |
4935 |
4934 |
4936 lemma sorted_wrt_ConsI: |
4935 text \<open>Sometimes the second equation in the definition of @{const sorted_wrt} is to aggressive |
4937 "\<lbrakk> \<And>y. y \<in> set xs \<Longrightarrow> P x y; sorted_wrt P xs \<rbrakk> \<Longrightarrow> sorted_wrt P (x # xs)" |
4936 because it relates each list element to \emph{all} its successors. Then this equation |
4938 by (induction xs) simp_all |
4937 should be removed and \<open>sorted_wrt2_simps\<close> should be added instead.\<close> |
|
4938 |
|
4939 lemma sorted_wrt1: "sorted_wrt P [x] = True" |
|
4940 by(simp) |
|
4941 |
|
4942 lemma sorted_wrt2: "transp P \<Longrightarrow> sorted_wrt P (x # y # zs) = (P x y \<and> sorted_wrt P (y # zs))" |
|
4943 apply(induction zs arbitrary: x y) |
|
4944 apply(auto dest: transpD) |
|
4945 apply (meson transpD) |
|
4946 done |
|
4947 |
|
4948 lemmas sorted_wrt2_simps = sorted_wrt1 sorted_wrt2 |
4939 |
4949 |
4940 lemma sorted_wrt_append: |
4950 lemma sorted_wrt_append: |
4941 "sorted_wrt P (xs @ ys) \<longleftrightarrow> |
4951 "sorted_wrt P (xs @ ys) \<longleftrightarrow> |
4942 sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)" |
4952 sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)" |
4943 by (induction xs) auto |
4953 by (induction xs) auto |