merged
authornipkow
Thu May 10 18:17:55 2018 +0200 (15 months ago)
changeset 6814253b4e204755e
parent 68138 c738f40e88d4
parent 68141 b105964ae3c4
child 68143 58c9231c2937
merged
     1.1 --- a/src/HOL/Data_Structures/Sorting.thy	Thu May 10 15:59:39 2018 +0100
     1.2 +++ b/src/HOL/Data_Structures/Sorting.thy	Thu May 10 18:17:55 2018 +0200
     1.3 @@ -306,17 +306,17 @@
     1.4  
     1.5  subsubsection "Time Complexity"
     1.6  
     1.7 -fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> real" where
     1.8 +fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where
     1.9  "c_merge_adj [] = 0" |
    1.10  "c_merge_adj [x] = 0" |
    1.11  "c_merge_adj (x # y # zs) = c_merge x y + c_merge_adj zs"
    1.12  
    1.13 -fun c_merge_all :: "('a::linorder) list list \<Rightarrow> real" where
    1.14 +fun c_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where
    1.15  "c_merge_all [] = undefined" |
    1.16  "c_merge_all [x] = 0" |
    1.17  "c_merge_all xs = c_merge_adj xs + c_merge_all (merge_adj xs)"
    1.18  
    1.19 -definition c_msort_bu :: "('a::linorder) list \<Rightarrow> real" where
    1.20 +definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where
    1.21  "c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))"
    1.22  
    1.23  lemma length_merge_adj:
     2.1 --- a/src/HOL/List.thy	Thu May 10 15:59:39 2018 +0100
     2.2 +++ b/src/HOL/List.thy	Thu May 10 18:17:55 2018 +0200
     2.3 @@ -4947,17 +4947,25 @@
     2.4  
     2.5  lemmas sorted_wrt2_simps = sorted_wrt1 sorted_wrt2
     2.6  
     2.7 +lemma sorted_wrt_true [simp]:
     2.8 +  "sorted_wrt (\<lambda>_ _. True) xs"
     2.9 +by (induction xs) simp_all
    2.10 +
    2.11  lemma sorted_wrt_append:
    2.12    "sorted_wrt P (xs @ ys) \<longleftrightarrow>
    2.13    sorted_wrt P xs \<and> sorted_wrt P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y)"
    2.14  by (induction xs) auto
    2.15  
    2.16 +lemma sorted_wrt_map:
    2.17 +  "sorted_wrt R (map f xs) = sorted_wrt (\<lambda>x y. R (f x) (f y)) xs"
    2.18 +by (induction xs) simp_all
    2.19 +
    2.20  lemma sorted_wrt_rev:
    2.21    "sorted_wrt P (rev xs) = sorted_wrt (\<lambda>x y. P y x) xs"
    2.22  by (induction xs) (auto simp add: sorted_wrt_append)
    2.23  
    2.24 -lemma sorted_wrt_mono:
    2.25 -  "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> sorted_wrt P xs \<Longrightarrow> sorted_wrt Q xs"
    2.26 +lemma sorted_wrt_mono_rel:
    2.27 +  "(\<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"
    2.28  by(induction xs)(auto)
    2.29  
    2.30  lemma sorted_wrt01: "length xs \<le> 1 \<Longrightarrow> sorted_wrt P xs"
    2.31 @@ -4965,7 +4973,7 @@
    2.32  
    2.33  text \<open>Strictly Ascending Sequences of Natural Numbers\<close>
    2.34  
    2.35 -lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [0..<n]"
    2.36 +lemma sorted_wrt_upt[simp]: "sorted_wrt (<) [m..<n]"
    2.37  by(induction n) (auto simp: sorted_wrt_append)
    2.38  
    2.39  text \<open>Each element is greater or equal to its index:\<close>