# 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 \<open>The Median-of-Medians Selection Algorithm\<close>
 theory Selection
-  imports Complex_Main Sorting Time_Funs
+  imports Complex_Main Time_Funs Sorting
 begin
 
 text \<open>
@@ -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.
 \<close>
 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 \<Rightarrow> 'a :: linorder list \<Rightarrow> 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 \<Rightarrow> 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 \<le> length xs ^ 2 + 3 * length xs + 3"
 proof -
-  have "T_slow_select k xs \<le> (length xs + 1)\<^sup>2 + (length (isort xs) + 1) + 1"
+  have "T_slow_select k xs \<le> (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 "\<dots> = 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 \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"insort x [] = [x]" |
-"insort x (y#ys) =
-  (if x \<le> y then x#y#ys else y#(insort x ys))"
+fun insort1 :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"insort1 x [] = [x]" |
+"insort1 x (y#ys) =
+  (if x \<le> y then x#y#ys else y#(insort1 x ys))"
 
-fun isort :: "'a::linorder list \<Rightarrow> 'a list" where
-"isort [] = []" |
-"isort (x#xs) = insort x (isort xs)"
+fun insort :: "'a::linorder list \<Rightarrow> '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} \<union> set xs"
-by(simp add: mset_insort flip: set_mset_mset)
+lemma set_insort1: "set (insort1 x xs) = {x} \<union> 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 \<open>We count the number of function calls.\<close>
 
 text\<open>
-\<open>insort x [] = [x]\<close>
-\<open>insort x (y#ys) =
-  (if x \<le> y then x#y#ys else y#(insort x ys))\<close>
+\<open>insort1 x [] = [x]\<close>
+\<open>insort1 x (y#ys) =
+  (if x \<le> y then x#y#ys else y#(insort1 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_insort1 :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> nat" where
+"T_insort1 x [] = 1" |
+"T_insort1 x (y#ys) =
+  (if x \<le> y then 0 else T_insort1 x ys) + 1"
 
 text\<open>
-\<open>isort [] = []\<close>
-\<open>isort (x#xs) = insort x (isort xs)\<close>
+\<open>insort [] = []\<close>
+\<open>insort (x#xs) = insort1 x (insort 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_insort :: "'a::linorder list \<Rightarrow> 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 \<le> length xs + 1"
+lemma T_insort1_length: "T_insort1 x xs \<le> 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 \<le> (length xs + 1) ^ 2"
+lemma T_insort_length: "T_insort 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_insort (x#xs) = T_insort xs + T_insort1 x (insort xs) + 1" by simp
+  also have "\<dots> \<le> (length xs + 1) ^ 2 + T_insort1 x (insort 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_insort1_length[of x "insort xs"] by (simp add: length_insort)
   also have "\<dots> \<le> (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 \<open>Note that \<^const>\<open>insort_key\<close> is already defined in theory \<^theory>\<open>HOL.List\<close>.
-Thus some of the lemmas are already present as well.\<close>
+hide_const List.insort_key
 
-fun isort_key :: "('a \<Rightarrow> 'k::linorder) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"isort_key f [] = []" |
-"isort_key f (x # xs) = insort_key f x (isort_key f xs)"
+fun insort1_key :: "('a \<Rightarrow> 'k::linorder) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"insort1_key f x [] = [x]" |
+"insort1_key f x (y # ys) = (if f x \<le> f y then x # y # ys else y # insort1_key f x ys)"
+
+fun insort_key :: "('a \<Rightarrow> 'k::linorder) \<Rightarrow> 'a list \<Rightarrow> '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} \<union> 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: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
+lemma insort1_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort1_key f a xs = a # xs"
 by (cases xs) auto
 
-lemma filter_insort_key_neg:
-  "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
+lemma filter_insort1_key_neg:
+  "\<not> P x \<Longrightarrow> filter P (insort1_key f x xs) = filter P xs"
 by (induction xs) simp_all
 
-lemma filter_insort_key_pos:
-  "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> 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) \<Longrightarrow> P x \<Longrightarrow> 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 (\<lambda>y. f y = k) (isort_key f xs) = filter (\<lambda>y. f y = k) xs"
+lemma sort_key_stable: "filter (\<lambda>y. f y = k) (insort_key f xs) = filter (\<lambda>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 (\<lambda>y. f y = k) (isort_key f (a # xs))
-      = filter (\<lambda>y. f y = k) (insort_key f a (isort_key f xs))"  by simp
-    also have "\<dots> = insort_key f a (filter (\<lambda>y. f y = k) (isort_key f xs))"
-      by (simp add: True filter_insort_key_pos sorted_isort_key)
-    also have "\<dots> = insort_key f a (filter (\<lambda>y. f y = k) xs)"  by (simp add: Cons.IH)
-    also have "\<dots> = a # (filter (\<lambda>y. f y = k) xs)"  by(simp add: True insort_is_Cons)
+    have "filter (\<lambda>y. f y = k) (insort_key f (a # xs))
+      = filter (\<lambda>y. f y = k) (insort1_key f a (insort_key f xs))"  by simp
+    also have "\<dots> = insort1_key f a (filter (\<lambda>y. f y = k) (insort_key f xs))"
+      by (simp add: True filter_insort1_key_pos sorted_insort_key)
+    also have "\<dots> = insort1_key f a (filter (\<lambda>y. f y = k) xs)"  by (simp add: Cons.IH)
+    also have "\<dots> = a # (filter (\<lambda>y. f y = k) xs)"  by(simp add: True insort1_is_Cons)
     also have "\<dots> = filter (\<lambda>y. f y = k) (a # xs)" by (simp add: True)
     finally show ?thesis .
   qed