# HG changeset patch # User nipkow # Date 1525767778 -7200 # Node ID 29da75b7e352e89b133939d25393a49bb9651d66 # Parent cebf36c142265bfe5f7cf59f21a68fa2a02565c9 more "sorted" changes diff -r cebf36c14226 -r 29da75b7e352 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue May 08 10:14:36 2018 +0200 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy Tue May 08 10:22:58 2018 +0200 @@ -556,7 +556,7 @@ by (simp add: subarray_nth_array_Cons, cases "l < p") (auto simp add: subarray_append subarray_Nil) with IH1' IH2 part_conds1' part_conds2' pivot have ?thesis unfolding subarray_def - apply (auto simp add: sorted_append sorted_Cons all_in_set_nths'_conv) + apply (auto simp add: sorted_append all_in_set_nths'_conv) by (auto simp add: set_nths' dest: order.trans [of _ "Array.get h' a ! p"]) } with True cr show ?thesis diff -r cebf36c14226 -r 29da75b7e352 src/HOL/Imperative_HOL/ex/Sorted_List.thy --- a/src/HOL/Imperative_HOL/ex/Sorted_List.thy Tue May 08 10:14:36 2018 +0200 +++ b/src/HOL/Imperative_HOL/ex/Sorted_List.thy Tue May 08 10:22:58 2018 +0200 @@ -26,10 +26,10 @@ lemma sorted_merge[simp]: "List.sorted (merge xs ys) = (List.sorted xs \ List.sorted ys)" -by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons) +by (induct xs ys rule: merge.induct, auto) lemma distinct_merge[simp]: "\ distinct xs; distinct ys; List.sorted xs; List.sorted ys \ \ distinct (merge xs ys)" -by (induct xs ys rule: merge.induct, auto simp add: sorted_Cons) +by (induct xs ys rule: merge.induct, auto) text \The remove function removes an element from a sorted list\ @@ -40,7 +40,7 @@ lemma remove': "sorted xs \ distinct xs \ sorted (remove a xs) \ distinct (remove a xs) \ set (remove a xs) = set xs - {a}" apply (induct xs) -apply (auto simp add: sorted_Cons) +apply (auto) done lemma set_remove[simp]: "\ sorted xs; distinct xs \ \ set (remove a xs) = set xs - {a}" @@ -61,7 +61,6 @@ lemma remove_insort_commute: "\ a \ b; sorted xs \ \ remove b (insort a xs) = insort a (remove b xs)" apply (induct xs) apply auto -apply (auto simp add: sorted_Cons) apply (case_tac xs) apply auto done @@ -74,7 +73,7 @@ lemma remove1_eq_remove: "sorted xs \ distinct xs \ remove1 x xs = remove x xs" apply (induct xs) -apply (auto simp add: sorted_Cons) +apply (auto) apply (subgoal_tac "x \ set xs") apply (simp add: notinset_remove) apply fastforce @@ -83,7 +82,7 @@ lemma sorted_remove1: "sorted xs \ sorted (remove1 x xs)" apply (induct xs) -apply (auto simp add: sorted_Cons) +apply (auto) done subsection \Efficient member function for sorted lists\ @@ -93,6 +92,6 @@ | "smember (y#ys) x \ x = y \ (x > y \ smember ys x)" lemma "sorted xs \ smember xs x \ (x \ set xs)" - by (induct xs) (auto simp add: sorted_Cons) + by (induct xs) (auto) end