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

author | nipkow |

Thu, 22 Oct 2020 08:39:08 +0200 | |

changeset 72501 | 70b420065a07 |

parent 72500 | 7d7fa4e35053 |

child 72502 | ff181cd78bb7 |

tuned names: t_ -> T_

--- a/src/HOL/Data_Structures/Sorting.thy Thu Oct 22 07:31:25 2020 +0200 +++ b/src/HOL/Data_Structures/Sorting.thy Thu Oct 22 08:39:08 2020 +0200 @@ -61,21 +61,21 @@ \<open>insort x (y#ys) = (if x \<le> y then x#y#ys else y#(insort x ys))\<close> \<close> -fun t_insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> nat" where -"t_insort x [] = 1" | -"t_insort x (y#ys) = - (if x \<le> y then 0 else t_insort x ys) + 1" +fun T_insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> nat" where +"T_insort x [] = 1" | +"T_insort x (y#ys) = + (if x \<le> y then 0 else T_insort x ys) + 1" text\<open> \<open>isort [] = []\<close> \<open>isort (x#xs) = insort x (isort xs)\<close> \<close> -fun t_isort :: "'a::linorder list \<Rightarrow> nat" where -"t_isort [] = 1" | -"t_isort (x#xs) = t_isort xs + t_insort x (isort xs) + 1" +fun T_isort :: "'a::linorder list \<Rightarrow> nat" where +"T_isort [] = 1" | +"T_isort (x#xs) = T_isort xs + T_insort x (isort xs) + 1" -lemma t_insort_length: "t_insort x xs \<le> length xs + 1" +lemma T_insort_length: "T_insort x xs \<le> length xs + 1" apply(induction xs) apply auto done @@ -90,16 +90,16 @@ apply (auto simp: length_insort) done -lemma t_isort_length: "t_isort xs \<le> (length xs + 1) ^ 2" +lemma T_isort_length: "T_isort xs \<le> (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 "\<dots> \<le> (length xs + 1) ^ 2 + t_insort x (isort xs) + 1" + have "T_isort (x#xs) = T_isort xs + T_insort x (isort xs) + 1" by simp + also have "\<dots> \<le> (length xs + 1) ^ 2 + T_insort x (isort xs) + 1" using Cons.IH by simp also have "\<dots> \<le> (length xs + 1) ^ 2 + length xs + 1 + 1" - using t_insort_length[of x "isort xs"] by (simp add: length_isort) + using T_insort_length[of x "isort xs"] by (simp add: length_isort) also have "\<dots> \<le> (length(x#xs) + 1) ^ 2" by (simp add: power2_eq_square) finally show ?case . @@ -179,23 +179,23 @@ text \<open>We only count the number of comparisons between list elements.\<close> -fun c_merge :: "'a::linorder list \<Rightarrow> 'a list \<Rightarrow> nat" where -"c_merge [] ys = 0" | -"c_merge xs [] = 0" | -"c_merge (x#xs) (y#ys) = 1 + (if x \<le> y then c_merge xs (y#ys) else c_merge (x#xs) ys)" +fun C_merge :: "'a::linorder list \<Rightarrow> 'a list \<Rightarrow> nat" where +"C_merge [] ys = 0" | +"C_merge xs [] = 0" | +"C_merge (x#xs) (y#ys) = 1 + (if x \<le> y then C_merge xs (y#ys) else C_merge (x#xs) ys)" -lemma c_merge_ub: "c_merge xs ys \<le> length xs + length ys" -by (induction xs ys rule: c_merge.induct) auto +lemma C_merge_ub: "C_merge xs ys \<le> length xs + length ys" +by (induction xs ys rule: C_merge.induct) auto -fun c_msort :: "'a::linorder list \<Rightarrow> nat" where -"c_msort xs = +fun C_msort :: "'a::linorder list \<Rightarrow> nat" where +"C_msort xs = (let n = length xs; ys = take (n div 2) xs; zs = drop (n div 2) xs in if n \<le> 1 then 0 - else c_msort ys + c_msort zs + c_merge (msort ys) (msort zs))" + else C_msort ys + C_msort zs + C_merge (msort ys) (msort zs))" -declare c_msort.simps [simp del] +declare C_msort.simps [simp del] lemma length_merge: "length(merge xs ys) = length xs + length ys" apply (induction xs ys rule: merge.induct) @@ -213,9 +213,9 @@ to ensure that msort.simps cannot be used recursively. Also works without this precaution, but that is just luck.\<close> -lemma c_msort_le: "length xs = 2^k \<Longrightarrow> c_msort xs \<le> k * 2^k" +lemma C_msort_le: "length xs = 2^k \<Longrightarrow> C_msort xs \<le> k * 2^k" proof(induction k arbitrary: xs) - case 0 thus ?case by (simp add: c_msort.simps) + case 0 thus ?case by (simp add: C_msort.simps) next case (Suc k) let ?n = "length xs" @@ -224,16 +224,16 @@ show ?case proof (cases "?n \<le> 1") case True - thus ?thesis by(simp add: c_msort.simps) + thus ?thesis by(simp add: C_msort.simps) next case False - have "c_msort(xs) = - c_msort ?ys + c_msort ?zs + c_merge (msort ?ys) (msort ?zs)" - by (simp add: c_msort.simps msort.simps) - also have "\<dots> \<le> c_msort ?ys + c_msort ?zs + length ?ys + length ?zs" - using c_merge_ub[of "msort ?ys" "msort ?zs"] length_msort[of ?ys] length_msort[of ?zs] + have "C_msort(xs) = + C_msort ?ys + C_msort ?zs + C_merge (msort ?ys) (msort ?zs)" + by (simp add: C_msort.simps msort.simps) + also have "\<dots> \<le> C_msort ?ys + C_msort ?zs + length ?ys + length ?zs" + using C_merge_ub[of "msort ?ys" "msort ?zs"] length_msort[of ?ys] length_msort[of ?zs] by arith - also have "\<dots> \<le> k * 2^k + c_msort ?zs + length ?ys + length ?zs" + also have "\<dots> \<le> k * 2^k + C_msort ?zs + length ?ys + length ?zs" using Suc.IH[of ?ys] Suc.prems by simp also have "\<dots> \<le> k * 2^k + k * 2^k + length ?ys + length ?zs" using Suc.IH[of ?zs] Suc.prems by simp @@ -244,8 +244,8 @@ qed (* Beware of implicit conversions: *) -lemma c_msort_log: "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)" -using c_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps) +lemma C_msort_log: "length xs = 2^k \<Longrightarrow> C_msort xs \<le> 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) @@ -297,36 +297,36 @@ subsubsection "Time Complexity" -fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> 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" +fun C_merge_adj :: "('a::linorder) list list \<Rightarrow> 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" -fun c_merge_all :: "('a::linorder) list list \<Rightarrow> 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)" +fun C_merge_all :: "('a::linorder) list list \<Rightarrow> 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)" -definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where -"c_msort_bu xs = c_merge_all (map (\<lambda>x. [x]) xs)" +definition C_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where +"C_msort_bu xs = C_merge_all (map (\<lambda>x. [x]) xs)" lemma length_merge_adj: "\<lbrakk> even(length xss); \<forall>xs \<in> set xss. length xs = m \<rbrakk> \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). length xs = 2*m" by(induction xss rule: merge_adj.induct) (auto simp: length_merge) -lemma c_merge_adj: "\<forall>xs \<in> set xss. length xs = m \<Longrightarrow> c_merge_adj xss \<le> m * length xss" -proof(induction xss rule: c_merge_adj.induct) +lemma C_merge_adj: "\<forall>xs \<in> set xss. length xs = m \<Longrightarrow> C_merge_adj xss \<le> m * length xss" +proof(induction xss rule: C_merge_adj.induct) case 1 thus ?case by simp next case 2 thus ?case by simp next - case (3 x y) thus ?case using c_merge_ub[of x y] by (simp add: algebra_simps) + case (3 x y) thus ?case using C_merge_ub[of x y] by (simp add: algebra_simps) qed -lemma c_merge_all: "\<lbrakk> \<forall>xs \<in> set xss. length xs = m; length xss = 2^k \<rbrakk> - \<Longrightarrow> c_merge_all xss \<le> m * k * 2^k" -proof (induction xss arbitrary: k m rule: c_merge_all.induct) +lemma C_merge_all: "\<lbrakk> \<forall>xs \<in> set xss. length xs = m; length xss = 2^k \<rbrakk> + \<Longrightarrow> C_merge_all xss \<le> m * k * 2^k" +proof (induction xss arbitrary: k m rule: C_merge_all.induct) case 1 thus ?case by simp next case 2 thus ?case by simp @@ -340,9 +340,9 @@ from length_merge_adj[OF this "3.prems"(1)] have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" . have **: "length ?xss2 = 2 ^ k'" using "3.prems"(2) k' by auto - have "c_merge_all ?xss = c_merge_adj ?xss + c_merge_all ?xss2" by simp - also have "\<dots> \<le> m * 2^k + c_merge_all ?xss2" - using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) + have "C_merge_all ?xss = C_merge_adj ?xss + C_merge_all ?xss2" by simp + also have "\<dots> \<le> m * 2^k + C_merge_all ?xss2" + using "3.prems"(2) C_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'" using "3.IH"[OF * **] by simp also have "\<dots> = m * k * 2^k" @@ -350,8 +350,8 @@ finally show ?case . qed -corollary c_msort_bu: "length xs = 2 ^ k \<Longrightarrow> c_msort_bu xs \<le> k * 2 ^ k" -using c_merge_all[of "map (\<lambda>x. [x]) xs" 1] by (simp add: c_msort_bu_def) +corollary C_msort_bu: "length xs = 2 ^ k \<Longrightarrow> C_msort_bu xs \<le> k * 2 ^ k" +using C_merge_all[of "map (\<lambda>x. [x]) xs" 1] by (simp add: C_msort_bu_def) subsection "Quicksort"