diff -r d96dd69903fb -r 7ed1759fe1bd src/HOL/Data_Structures/Sorting.thy --- a/src/HOL/Data_Structures/Sorting.thy Fri Aug 25 09:56:45 2023 +0100 +++ b/src/HOL/Data_Structures/Sorting.thy Sat Aug 26 11:36:25 2023 +0100 @@ -3,9 +3,9 @@ section "Sorting" theory Sorting -imports - Complex_Main - "HOL-Library.Multiset" + imports + Complex_Main + "HOL-Library.Multiset" begin hide_const List.insort @@ -16,40 +16,31 @@ subsection "Insertion Sort" fun insort1 :: "'a::linorder \ 'a list \ 'a list" where -"insort1 x [] = [x]" | -"insort1 x (y#ys) = + "insort1 x [] = [x]" | + "insort1 x (y#ys) = (if x \ y then x#y#ys else y#(insort1 x ys))" fun insort :: "'a::linorder list \ 'a list" where -"insort [] = []" | -"insort (x#xs) = insort1 x (insort xs)" + "insort [] = []" | + "insort (x#xs) = insort1 x (insort xs)" subsubsection "Functional Correctness" lemma mset_insort1: "mset (insort1 x xs) = {#x#} + mset xs" -apply(induction xs) -apply auto -done + by (induction xs) auto lemma mset_insort: "mset (insort xs) = mset xs" -apply(induction xs) -apply simp -apply (simp add: mset_insort1) -done + by (induction xs) (auto simp: mset_insort1) lemma set_insort1: "set (insort1 x xs) = {x} \ set xs" -by(simp add: mset_insort1 flip: set_mset_mset) + by(simp add: mset_insort1 flip: set_mset_mset) lemma sorted_insort1: "sorted (insort1 a xs) = sorted xs" -apply(induction xs) -apply(auto simp add: set_insort1) -done + by (induction xs) (auto simp: set_insort1) lemma sorted_insort: "sorted (insort xs)" -apply(induction xs) -apply(auto simp: sorted_insort1) -done + by (induction xs) (auto simp: sorted_insort1) subsubsection "Time Complexity" @@ -62,8 +53,8 @@ (if x \ y then x#y#ys else y#(insort1 x ys))\ \ fun T_insort1 :: "'a::linorder \ 'a list \ nat" where -"T_insort1 x [] = 1" | -"T_insort1 x (y#ys) = + "T_insort1 x [] = 1" | + "T_insort1 x (y#ys) = (if x \ y then 0 else T_insort1 x ys) + 1" text\ @@ -71,24 +62,18 @@ \insort (x#xs) = insort1 x (insort xs)\ \ fun T_insort :: "'a::linorder list \ nat" where -"T_insort [] = 1" | -"T_insort (x#xs) = T_insort xs + T_insort1 x (insort xs) + 1" + "T_insort [] = 1" | + "T_insort (x#xs) = T_insort xs + T_insort1 x (insort xs) + 1" lemma T_insort1_length: "T_insort1 x xs \ length xs + 1" -apply(induction xs) -apply auto -done + by (induction xs) auto lemma length_insort1: "length (insort1 x xs) = length xs + 1" -apply(induction xs) -apply auto -done + by (induction xs) auto lemma length_insort: "length (insort xs) = length xs" -apply(induction xs) -apply (auto simp: length_insort1) -done + by (metis Sorting.mset_insort size_mset) lemma T_insort_length: "T_insort xs \ (length xs + 1) ^ 2" proof(induction xs) @@ -109,12 +94,12 @@ subsection "Merge Sort" fun merge :: "'a::linorder list \ 'a list \ 'a list" where -"merge [] ys = ys" | -"merge xs [] = xs" | -"merge (x#xs) (y#ys) = (if x \ y then x # merge xs (y#ys) else y # merge (x#xs) ys)" + "merge [] ys = ys" | + "merge xs [] = xs" | + "merge (x#xs) (y#ys) = (if x \ y then x # merge xs (y#ys) else y # merge (x#xs) ys)" fun msort :: "'a::linorder list \ 'a list" where -"msort xs = (let n = length xs in + "msort xs = (let n = length xs in if n \ 1 then xs else merge (msort (take (n div 2) xs)) (msort (drop (n div 2) xs)))" @@ -124,7 +109,7 @@ subsubsection "Functional Correctness" lemma mset_merge: "mset(merge xs ys) = mset xs + mset ys" -by(induction xs ys rule: merge.induct) auto + by(induction xs ys rule: merge.induct) auto lemma mset_msort: "mset (msort xs) = mset xs" proof(induction xs rule: msort.induct) @@ -151,13 +136,13 @@ text \Via the previous lemma or directly:\ lemma set_merge: "set(merge xs ys) = set xs \ set ys" -by (metis mset_merge set_mset_mset set_mset_union) + by (metis mset_merge set_mset_mset set_mset_union) lemma "set(merge xs ys) = set xs \ set ys" -by(induction xs ys rule: merge.induct) (auto) + by(induction xs ys rule: merge.induct) (auto) lemma sorted_merge: "sorted (merge xs ys) \ (sorted xs \ sorted ys)" -by(induction xs ys rule: merge.induct) (auto simp: set_merge) + by(induction xs ys rule: merge.induct) (auto simp: set_merge) lemma sorted_msort: "sorted (msort xs)" proof(induction xs rule: msort.induct) @@ -180,15 +165,15 @@ text \We only count the number of comparisons between list elements.\ fun C_merge :: "'a::linorder list \ 'a list \ nat" where -"C_merge [] ys = 0" | -"C_merge xs [] = 0" | -"C_merge (x#xs) (y#ys) = 1 + (if x \ y then C_merge xs (y#ys) else C_merge (x#xs) ys)" + "C_merge [] ys = 0" | + "C_merge xs [] = 0" | + "C_merge (x#xs) (y#ys) = 1 + (if x \ y then C_merge xs (y#ys) else C_merge (x#xs) ys)" lemma C_merge_ub: "C_merge xs ys \ length xs + length ys" -by (induction xs ys rule: C_merge.induct) auto + by (induction xs ys rule: C_merge.induct) auto fun C_msort :: "'a::linorder list \ nat" where -"C_msort xs = + "C_msort xs = (let n = length xs; ys = take (n div 2) xs; zs = drop (n div 2) xs @@ -198,9 +183,7 @@ declare C_msort.simps [simp del] lemma length_merge: "length(merge xs ys) = length xs + length ys" -apply (induction xs ys rule: merge.induct) -apply auto -done + by (induction xs ys rule: merge.induct) auto lemma length_msort: "length(msort xs) = length xs" proof (induction xs rule: msort.induct) @@ -245,78 +228,77 @@ (* Beware of implicit conversions: *) lemma C_msort_log: "length xs = 2^k \ C_msort xs \ length xs * log 2 (length xs)" -using C_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps) -by (metis (mono_tags) numeral_power_eq_of_nat_cancel_iff of_nat_le_iff of_nat_mult) + using C_msort_le[of xs k] + by (metis log2_of_power_eq mult.commute of_nat_mono of_nat_mult) subsection "Bottom-Up Merge Sort" fun merge_adj :: "('a::linorder) list list \ 'a list list" where -"merge_adj [] = []" | -"merge_adj [xs] = [xs]" | -"merge_adj (xs # ys # zss) = merge xs ys # merge_adj zss" + "merge_adj [] = []" | + "merge_adj [xs] = [xs]" | + "merge_adj (xs # ys # zss) = merge xs ys # merge_adj zss" text \For the termination proof of \merge_all\ below.\ lemma length_merge_adjacent[simp]: "length (merge_adj xs) = (length xs + 1) div 2" -by (induction xs rule: merge_adj.induct) auto + by (induction xs rule: merge_adj.induct) auto fun merge_all :: "('a::linorder) list list \ 'a list" where -"merge_all [] = []" | -"merge_all [xs] = xs" | -"merge_all xss = merge_all (merge_adj xss)" + "merge_all [] = []" | + "merge_all [xs] = xs" | + "merge_all xss = merge_all (merge_adj xss)" definition msort_bu :: "('a::linorder) list \ 'a list" where -"msort_bu xs = merge_all (map (\x. [x]) xs)" + "msort_bu xs = merge_all (map (\x. [x]) xs)" subsubsection "Functional Correctness" abbreviation mset_mset :: "'a list list \ 'a multiset" where -"mset_mset xss \ \\<^sub># (image_mset mset (mset xss))" + "mset_mset xss \ \\<^sub># (image_mset mset (mset xss))" lemma mset_merge_adj: "mset_mset (merge_adj xss) = mset_mset xss" -by(induction xss rule: merge_adj.induct) (auto simp: mset_merge) + by(induction xss rule: merge_adj.induct) (auto simp: mset_merge) lemma mset_merge_all: "mset (merge_all xss) = mset_mset xss" -by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj) + by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj) lemma mset_msort_bu: "mset (msort_bu xs) = mset xs" -by(simp add: msort_bu_def mset_merge_all multiset.map_comp comp_def) + by(simp add: msort_bu_def mset_merge_all multiset.map_comp comp_def) lemma sorted_merge_adj: "\xs \ set xss. sorted xs \ \xs \ set (merge_adj xss). sorted xs" -by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge) + by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge) lemma sorted_merge_all: "\xs \ set xss. sorted xs \ sorted (merge_all xss)" -apply(induction xss rule: merge_all.induct) -using [[simp_depth_limit=3]] by (auto simp add: sorted_merge_adj) + by (induction xss rule: merge_all.induct) (auto simp add: sorted_merge_adj) lemma sorted_msort_bu: "sorted (msort_bu xs)" -by(simp add: msort_bu_def sorted_merge_all) + by(simp add: msort_bu_def sorted_merge_all) subsubsection "Time Complexity" fun C_merge_adj :: "('a::linorder) list list \ nat" where -"C_merge_adj [] = 0" | -"C_merge_adj [xs] = 0" | -"C_merge_adj (xs # ys # zss) = C_merge xs ys + C_merge_adj zss" + "C_merge_adj [] = 0" | + "C_merge_adj [xs] = 0" | + "C_merge_adj (xs # ys # zss) = C_merge xs ys + C_merge_adj zss" fun C_merge_all :: "('a::linorder) list list \ nat" where -"C_merge_all [] = 0" | -"C_merge_all [xs] = 0" | -"C_merge_all xss = C_merge_adj xss + C_merge_all (merge_adj xss)" + "C_merge_all [] = 0" | + "C_merge_all [xs] = 0" | + "C_merge_all xss = C_merge_adj xss + C_merge_all (merge_adj xss)" definition C_msort_bu :: "('a::linorder) list \ nat" where -"C_msort_bu xs = C_merge_all (map (\x. [x]) xs)" + "C_msort_bu xs = C_merge_all (map (\x. [x]) xs)" lemma length_merge_adj: "\ even(length xss); \xs \ set xss. length xs = m \ \ \xs \ set (merge_adj xss). length xs = 2*m" -by(induction xss rule: merge_adj.induct) (auto simp: length_merge) + by(induction xss rule: merge_adj.induct) (auto simp: length_merge) lemma C_merge_adj: "\xs \ set xss. length xs = m \ C_merge_adj xss \ m * length xss" proof(induction xss rule: C_merge_adj.induct) @@ -354,27 +336,24 @@ qed corollary C_msort_bu: "length xs = 2 ^ k \ C_msort_bu xs \ k * 2 ^ k" -using C_merge_all[of "map (\x. [x]) xs" 1] by (simp add: C_msort_bu_def) + using C_merge_all[of "map (\x. [x]) xs" 1] by (simp add: C_msort_bu_def) subsection "Quicksort" fun quicksort :: "('a::linorder) list \ 'a list" where -"quicksort [] = []" | -"quicksort (x#xs) = quicksort (filter (\y. y < x) xs) @ [x] @ quicksort (filter (\y. x \ y) xs)" + "quicksort [] = []" | + "quicksort (x#xs) = quicksort (filter (\y. y < x) xs) @ [x] @ quicksort (filter (\y. x \ y) xs)" lemma mset_quicksort: "mset (quicksort xs) = mset xs" -apply (induction xs rule: quicksort.induct) -apply (auto simp: not_le) -done + by (induction xs rule: quicksort.induct) (auto simp: not_le) lemma set_quicksort: "set (quicksort xs) = set xs" -by(rule mset_eq_setD[OF mset_quicksort]) + by(rule mset_eq_setD[OF mset_quicksort]) lemma sorted_quicksort: "sorted (quicksort xs)" -apply (induction xs rule: quicksort.induct) -apply (auto simp add: sorted_append set_quicksort) -done +proof (induction xs rule: quicksort.induct) +qed (auto simp: sorted_append set_quicksort) subsection "Insertion Sort w.r.t. Keys and Stability" @@ -382,45 +361,45 @@ hide_const List.insort_key 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)" + "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)" + "insort_key f [] = []" | + "insort_key f (x # xs) = insort1_key f x (insort_key f xs)" subsubsection "Standard functional correctness" lemma mset_insort1_key: "mset (insort1_key f x xs) = {#x#} + mset xs" -by(induction xs) simp_all + by(induction xs) simp_all lemma mset_insort_key: "mset (insort_key f xs) = mset xs" -by(induction xs) (simp_all add: mset_insort1_key) + by(induction xs) (simp_all add: mset_insort1_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 + by (induction xs) auto lemma sorted_insort1_key: "sorted (map f (insort1_key f a xs)) = sorted (map f xs)" -by(induction xs)(auto simp: set_insort1_key) + 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) + by(induction xs)(simp_all add: sorted_insort1_key) subsubsection "Stability" lemma insort1_is_Cons: "\x\set xs. f a \ f x \ insort1_key f a xs = a # xs" -by (cases xs) auto + by (cases xs) auto lemma filter_insort1_key_neg: "\ P x \ filter P (insort1_key f x xs) = filter P xs" -by (induction xs) simp_all + by (induction xs) simp_all 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) + by (induction xs) (auto, subst insort1_is_Cons, auto) lemma sort_key_stable: "filter (\y. f y = k) (insort_key f xs) = filter (\y. f y = k) xs" proof (induction xs)