# HG changeset patch
# User nipkow
# Date 1525969075 -7200
# Node ID 53b4e204755e22ce367db1326beaefeebfefea4b
# Parent  c738f40e88d493959787a2cd863f0ba5b453b578# Parent  b105964ae3c4f99f787e34d167ccc8cc4329a42a
merged

diff -r c738f40e88d4 -r 53b4e204755e src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Thu May 10 15:59:39 2018 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy	Thu May 10 18:17:55 2018 +0200
@@ -306,17 +306,17 @@
 
 subsubsection "Time Complexity"
 
-fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> real" where
+fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where
 "c_merge_adj [] = 0" |
 "c_merge_adj [x] = 0" |
 "c_merge_adj (x # y # zs) = c_merge x y + c_merge_adj zs"
 
-fun c_merge_all :: "('a::linorder) list list \<Rightarrow> real" where
+fun c_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where
 "c_merge_all [] = undefined" |
 "c_merge_all [x] = 0" |
 "c_merge_all xs = c_merge_adj xs + c_merge_all (merge_adj xs)"
 
-definition c_msort_bu :: "('a::linorder) list \<Rightarrow> real" where
+definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where
 "c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))"
 
 lemma length_merge_adj:
diff -r c738f40e88d4 -r 53b4e204755e src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 10 15:59:39 2018 +0100
+++ b/src/HOL/List.thy	Thu May 10 18:17:55 2018 +0200
@@ -4947,17 +4947,25 @@
 
 lemmas sorted_wrt2_simps = sorted_wrt1 sorted_wrt2
 
+lemma sorted_wrt_true [simp]:
+  "sorted_wrt (\<lambda>_ _. True) xs"
+by (induction xs) simp_all
+
 lemma sorted_wrt_append:
   "sorted_wrt P (xs @ ys) \<longleftrightarrow>
   sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)"
 by (induction xs) auto
 
+lemma sorted_wrt_map:
+  "sorted_wrt R (map f xs) = sorted_wrt (\<lambda>x y. R (f x) (f y)) xs"
+by (induction xs) simp_all
+
 lemma sorted_wrt_rev:
   "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
 by (induction xs) (auto simp add: sorted_wrt_append)
 
-lemma sorted_wrt_mono:
-  "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
+lemma sorted_wrt_mono_rel:
+  "(\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs; P x y \<rbrakk> \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
 by(induction xs)(auto)
 
 lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs"
@@ -4965,7 +4973,7 @@
 
 text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
 
-lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [0..<n]"
+lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]"
 by(induction n) (auto simp: sorted_wrt_append)
 
 text \<open>Each element is greater or equal to its index:\<close>