# HG changeset patch # User nipkow # Date 1654023351 -7200 # Node ID 426afab39a55ffdd372674b3ea058d34ec049d92 # Parent 99b37c39143353e7c75315a29cd5894ba1fdfdd6 insort renamings diff -r 99b37c391433 -r 426afab39a55 src/HOL/Data_Structures/Selection.thy --- a/src/HOL/Data_Structures/Selection.thy Mon May 30 20:58:45 2022 +0200 +++ b/src/HOL/Data_Structures/Selection.thy Tue May 31 20:55:51 2022 +0200 @@ -4,7 +4,7 @@ *) section \The Median-of-Medians Selection Algorithm\ theory Selection - imports Complex_Main Sorting Time_Funs + imports Complex_Main Time_Funs Sorting begin text \ @@ -17,8 +17,8 @@ lemma replicate_numeral: "replicate (numeral n) x = x # replicate (pred_numeral n) x" by (simp add: numeral_eq_Suc) -lemma isort_correct: "isort xs = sort xs" - using sorted_isort mset_isort by (metis properties_for_sort) +lemma insort_correct: "insort xs = sort xs" + using sorted_insort mset_insort by (metis properties_for_sort) lemma sum_list_replicate [simp]: "sum_list (replicate n x) = n * x" by (induction n) auto @@ -498,13 +498,13 @@ using the naive selection algorithm where we sort the list using insertion sort. \ definition slow_select where - "slow_select k xs = isort xs ! k" + "slow_select k xs = insort xs ! k" definition slow_median where "slow_median xs = slow_select ((length xs - 1) div 2) xs" lemma slow_select_correct: "slow_select k xs = select k xs" - by (simp add: slow_select_def select_def isort_correct) + by (simp add: slow_select_def select_def insort_correct) lemma slow_median_correct: "slow_median xs = median xs" by (simp add: median_def slow_median_def slow_select_correct) @@ -635,18 +635,18 @@ by (induction x xs rule: T_partition3.induct) auto definition T_slow_select :: "nat \ 'a :: linorder list \ nat" where - "T_slow_select k xs = T_isort xs + T_nth (isort xs) k + 1" + "T_slow_select k xs = T_insort xs + T_nth (insort xs) k + 1" definition T_slow_median :: "'a :: linorder list \ nat" where "T_slow_median xs = T_slow_select ((length xs - 1) div 2) xs + 1" lemma T_slow_select_le: "T_slow_select k xs \ length xs ^ 2 + 3 * length xs + 3" proof - - have "T_slow_select k xs \ (length xs + 1)\<^sup>2 + (length (isort xs) + 1) + 1" + have "T_slow_select k xs \ (length xs + 1)\<^sup>2 + (length (insort xs) + 1) + 1" unfolding T_slow_select_def - by (intro add_mono T_isort_length) (auto simp: T_nth_eq) + by (intro add_mono T_insort_length) (auto simp: T_nth_eq) also have "\ = length xs ^ 2 + 3 * length xs + 3" - by (simp add: isort_correct algebra_simps power2_eq_square) + by (simp add: insort_correct algebra_simps power2_eq_square) finally show ?thesis . qed diff -r 99b37c391433 -r 426afab39a55 src/HOL/Data_Structures/Sorting.thy --- a/src/HOL/Data_Structures/Sorting.thy Mon May 30 20:58:45 2022 +0200 +++ b/src/HOL/Data_Structures/Sorting.thy Tue May 31 20:55:51 2022 +0200 @@ -15,40 +15,40 @@ subsection "Insertion Sort" -fun insort :: "'a::linorder \ 'a list \ 'a list" where -"insort x [] = [x]" | -"insort x (y#ys) = - (if x \ y then x#y#ys else y#(insort x ys))" +fun insort1 :: "'a::linorder \ 'a list \ 'a list" where +"insort1 x [] = [x]" | +"insort1 x (y#ys) = + (if x \ y then x#y#ys else y#(insort1 x ys))" -fun isort :: "'a::linorder list \ 'a list" where -"isort [] = []" | -"isort (x#xs) = insort x (isort xs)" +fun insort :: "'a::linorder list \ 'a list" where +"insort [] = []" | +"insort (x#xs) = insort1 x (insort xs)" subsubsection "Functional Correctness" -lemma mset_insort: "mset (insort x xs) = {#x#} + mset xs" +lemma mset_insort1: "mset (insort1 x xs) = {#x#} + mset xs" apply(induction xs) apply auto done -lemma mset_isort: "mset (isort xs) = mset xs" +lemma mset_insort: "mset (insort xs) = mset xs" apply(induction xs) apply simp -apply (simp add: mset_insort) +apply (simp add: mset_insort1) done -lemma set_insort: "set (insort x xs) = {x} \ set xs" -by(simp add: mset_insort flip: set_mset_mset) +lemma set_insort1: "set (insort1 x xs) = {x} \ set xs" +by(simp add: mset_insort1 flip: set_mset_mset) -lemma sorted_insort: "sorted (insort a xs) = sorted xs" +lemma sorted_insort1: "sorted (insort1 a xs) = sorted xs" apply(induction xs) -apply(auto simp add: set_insort) +apply(auto simp add: set_insort1) done -lemma sorted_isort: "sorted (isort xs)" +lemma sorted_insort: "sorted (insort xs)" apply(induction xs) -apply(auto simp: sorted_insort) +apply(auto simp: sorted_insort1) done @@ -57,49 +57,49 @@ text \We count the number of function calls.\ text\ -\insort x [] = [x]\ -\insort x (y#ys) = - (if x \ y then x#y#ys else y#(insort x ys))\ +\insort1 x [] = [x]\ +\insort1 x (y#ys) = + (if x \ y then x#y#ys else y#(insort1 x ys))\ \ -fun T_insort :: "'a::linorder \ 'a list \ nat" where -"T_insort x [] = 1" | -"T_insort x (y#ys) = - (if x \ y then 0 else T_insort x ys) + 1" +fun T_insort1 :: "'a::linorder \ 'a list \ nat" where +"T_insort1 x [] = 1" | +"T_insort1 x (y#ys) = + (if x \ y then 0 else T_insort1 x ys) + 1" text\ -\isort [] = []\ -\isort (x#xs) = insort x (isort xs)\ +\insort [] = []\ +\insort (x#xs) = insort1 x (insort xs)\ \ -fun T_isort :: "'a::linorder list \ nat" where -"T_isort [] = 1" | -"T_isort (x#xs) = T_isort xs + T_insort x (isort xs) + 1" +fun T_insort :: "'a::linorder list \ nat" where +"T_insort [] = 1" | +"T_insort (x#xs) = T_insort xs + T_insort1 x (insort xs) + 1" -lemma T_insort_length: "T_insort x xs \ length xs + 1" +lemma T_insort1_length: "T_insort1 x xs \ length xs + 1" apply(induction xs) apply auto done -lemma length_insort: "length (insort x xs) = length xs + 1" +lemma length_insort1: "length (insort1 x xs) = length xs + 1" apply(induction xs) apply auto done -lemma length_isort: "length (isort xs) = length xs" +lemma length_insort: "length (insort xs) = length xs" apply(induction xs) -apply (auto simp: length_insort) +apply (auto simp: length_insort1) done -lemma T_isort_length: "T_isort xs \ (length xs + 1) ^ 2" +lemma T_insort_length: "T_insort xs \ (length xs + 1) ^ 2" proof(induction xs) case Nil show ?case by simp next case (Cons x xs) - have "T_isort (x#xs) = T_isort xs + T_insort x (isort xs) + 1" by simp - also have "\ \ (length xs + 1) ^ 2 + T_insort x (isort xs) + 1" + have "T_insort (x#xs) = T_insort xs + T_insort1 x (insort xs) + 1" by simp + also have "\ \ (length xs + 1) ^ 2 + T_insort1 x (insort xs) + 1" using Cons.IH by simp also have "\ \ (length xs + 1) ^ 2 + length xs + 1 + 1" - using T_insort_length[of x "isort xs"] by (simp add: length_isort) + using T_insort1_length[of x "insort xs"] by (simp add: length_insort) also have "\ \ (length(x#xs) + 1) ^ 2" by (simp add: power2_eq_square) finally show ?case . @@ -379,61 +379,65 @@ subsection "Insertion Sort w.r.t. Keys and Stability" -text \Note that \<^const>\insort_key\ is already defined in theory \<^theory>\HOL.List\. -Thus some of the lemmas are already present as well.\ +hide_const List.insort_key -fun isort_key :: "('a \ 'k::linorder) \ 'a list \ 'a list" where -"isort_key f [] = []" | -"isort_key f (x # xs) = insort_key f x (isort_key f xs)" +fun insort1_key :: "('a \ 'k::linorder) \ 'a \ 'a list \ 'a list" where +"insort1_key f x [] = [x]" | +"insort1_key f x (y # ys) = (if f x \ f y then x # y # ys else y # insort1_key f x ys)" + +fun insort_key :: "('a \ 'k::linorder) \ 'a list \ 'a list" where +"insort_key f [] = []" | +"insort_key f (x # xs) = insort1_key f x (insort_key f xs)" subsubsection "Standard functional correctness" -lemma mset_insort_key: "mset (insort_key f x xs) = {#x#} + mset xs" +lemma mset_insort1_key: "mset (insort1_key f x xs) = {#x#} + mset xs" by(induction xs) simp_all -lemma mset_isort_key: "mset (isort_key f xs) = mset xs" -by(induction xs) (simp_all add: mset_insort_key) - -lemma set_isort_key: "set (isort_key f xs) = set xs" -by (rule mset_eq_setD[OF mset_isort_key]) +lemma mset_insort_key: "mset (insort_key f xs) = mset xs" +by(induction xs) (simp_all add: mset_insort1_key) -lemma sorted_insort_key: "sorted (map f (insort_key f a xs)) = sorted (map f xs)" -by(induction xs)(auto simp: set_insort_key) +(* Inductive proof simpler than derivation from mset lemma: *) +lemma set_insort1_key: "set (insort1_key f x xs) = {x} \ set xs" +by (induction xs) auto -lemma sorted_isort_key: "sorted (map f (isort_key f xs))" -by(induction xs)(simp_all add: sorted_insort_key) +lemma sorted_insort1_key: "sorted (map f (insort1_key f a xs)) = sorted (map f xs)" +by(induction xs)(auto simp: set_insort1_key) + +lemma sorted_insort_key: "sorted (map f (insort_key f xs))" +by(induction xs)(simp_all add: sorted_insort1_key) subsubsection "Stability" -lemma insort_is_Cons: "\x\set xs. f a \ f x \ insort_key f a xs = a # xs" +lemma insort1_is_Cons: "\x\set xs. f a \ f x \ insort1_key f a xs = a # xs" by (cases xs) auto -lemma filter_insort_key_neg: - "\ P x \ filter P (insort_key f x xs) = filter P xs" +lemma filter_insort1_key_neg: + "\ P x \ filter P (insort1_key f x xs) = filter P xs" by (induction xs) simp_all -lemma filter_insort_key_pos: - "sorted (map f xs) \ P x \ filter P (insort_key f x xs) = insort_key f x (filter P xs)" -by (induction xs) (auto, subst insort_is_Cons, auto) +lemma filter_insort1_key_pos: + "sorted (map f xs) \ P x \ filter P (insort1_key f x xs) = insort1_key f x (filter P xs)" +by (induction xs) (auto, subst insort1_is_Cons, auto) -lemma sort_key_stable: "filter (\y. f y = k) (isort_key f xs) = filter (\y. f y = k) xs" +lemma sort_key_stable: "filter (\y. f y = k) (insort_key f xs) = filter (\y. f y = k) xs" proof (induction xs) case Nil thus ?case by simp next case (Cons a xs) thus ?case proof (cases "f a = k") - case False thus ?thesis by (simp add: Cons.IH filter_insort_key_neg) + case False thus ?thesis by (simp add: Cons.IH filter_insort1_key_neg) next case True - have "filter (\y. f y = k) (isort_key f (a # xs)) - = filter (\y. f y = k) (insort_key f a (isort_key f xs))" by simp - also have "\ = insort_key f a (filter (\y. f y = k) (isort_key f xs))" - by (simp add: True filter_insort_key_pos sorted_isort_key) - also have "\ = insort_key f a (filter (\y. f y = k) xs)" by (simp add: Cons.IH) - also have "\ = a # (filter (\y. f y = k) xs)" by(simp add: True insort_is_Cons) + have "filter (\y. f y = k) (insort_key f (a # xs)) + = filter (\y. f y = k) (insort1_key f a (insort_key f xs))" by simp + also have "\ = insort1_key f a (filter (\y. f y = k) (insort_key f xs))" + by (simp add: True filter_insort1_key_pos sorted_insort_key) + also have "\ = insort1_key f a (filter (\y. f y = k) xs)" by (simp add: Cons.IH) + also have "\ = a # (filter (\y. f y = k) xs)" by(simp add: True insort1_is_Cons) also have "\ = filter (\y. f y = k) (a # xs)" by (simp add: True) finally show ?thesis . qed