# HG changeset patch
# User nipkow
# Date 1603348748 -7200
# Node ID 70b420065a07cb108bf9cdf35159d064a701f8cb
# Parent  7d7fa4e35053e50a0715965b886c2e094e2640b6
tuned names: t_ -> T_

diff -r 7d7fa4e35053 -r 70b420065a07 src/HOL/Data_Structures/Sorting.thy
--- 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"