--- 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"