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

author | haftmann |

Wed, 03 Nov 2010 11:50:29 +0100 | |

changeset 40346 | 58af2b8327b7 |

parent 40320 | abc52faa7761 |

child 40347 | 429bf4388b2f |

tuned proof

--- a/src/HOL/Library/Multiset.thy Wed Nov 03 10:44:53 2010 +0100 +++ b/src/HOL/Library/Multiset.thy Wed Nov 03 11:50:29 2010 +0100 @@ -901,30 +901,27 @@ next fix l assume "l \<in> set ?rhs" - have *: "\<And>x P. P (f x) \<and> f l = f x \<longleftrightarrow> P (f l) \<and> f l = f x" by auto - have **: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto + let ?pivot = "f (xs ! (length xs div 2))" + have *: "\<And>x. f l = f x \<longleftrightarrow> f x = f l" by auto have "[x \<leftarrow> sort_key f xs . f x = f l] = [x \<leftarrow> xs. f x = f l]" unfolding filter_sort by (rule properties_for_sort_key) (auto intro: sorted_map_same) - with ** have [simp]: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp - let ?pivot = "f (xs ! (length xs div 2))" + with * have **: "[x \<leftarrow> sort_key f xs . f l = f x] = [x \<leftarrow> xs. f l = f x]" by simp + have "\<And>x P. P (f x) ?pivot \<and> f l = f x \<longleftrightarrow> P (f l) ?pivot \<and> f l = f x" by auto + then have "\<And>P. [x \<leftarrow> sort_key f xs . P (f x) ?pivot \<and> f l = f x] = + [x \<leftarrow> sort_key f xs. P (f l) ?pivot \<and> f l = f x]" by simp + note *** = this [of "op <"] this [of "op >"] this [of "op ="] show "[x \<leftarrow> ?rhs. f l = f x] = [x \<leftarrow> ?lhs. f l = f x]" proof (cases "f l" ?pivot rule: linorder_cases) case less then moreover have "f l \<noteq> ?pivot" and "\<not> f l > ?pivot" by auto ultimately show ?thesis - apply (auto simp add: filter_sort [symmetric]) - apply (subst *) apply simp - apply (subst *) apply simp - done + by (simp add: filter_sort [symmetric] ** ***) next case equal then show ?thesis - by (auto simp add: ** less_le) + by (simp add: * less_le) next case greater then moreover have "f l \<noteq> ?pivot" and "\<not> f l < ?pivot" by auto ultimately show ?thesis - apply (auto simp add: filter_sort [symmetric]) - apply (subst *) apply simp - apply (subst *) apply simp - done + by (simp add: filter_sort [symmetric] ** ***) qed qed