# HG changeset patch
# User wenzelm
# Date 1541596003 -3600
# Node ID 9f8d26b8c7317344fa1f0333585b41e51911d310
# Parent  fc359b60121c35688096b13d047faea6945a7f5a# Parent  8bfa615ddde4f732f098a3c4757b753949051577
merged

diff -r 8bfa615ddde4 -r 9f8d26b8c731 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Wed Nov 07 14:03:47 2018 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Wed Nov 07 14:06:43 2018 +0100
@@ -7,6 +7,7 @@
 imports
   Complex_Main
   "HOL-Library.Library"
+  "HOL-Library.Sorting_Algorithms"
   "HOL-Library.Subseq_Order"
   "HOL-Library.RBT"
   "HOL-Data_Structures.Tree_Map"
diff -r 8bfa615ddde4 -r 9f8d26b8c731 src/HOL/Library/Comparator.thy
--- a/src/HOL/Library/Comparator.thy	Wed Nov 07 14:03:47 2018 +0100
+++ b/src/HOL/Library/Comparator.thy	Wed Nov 07 14:06:43 2018 +0100
@@ -8,6 +8,8 @@
 
 section \<open>Comparators on linear quasi-orders\<close>
 
+subsection \<open>Basic properties\<close>
+
 datatype comp = Less | Equiv | Greater
 
 locale comparator =
@@ -222,7 +224,8 @@
 
 end
 
-text \<open>Fundamental comparator combinators\<close>
+
+subsection \<open>Fundamental comparator combinators\<close>
 
 lift_definition reversed :: "'a comparator \<Rightarrow> 'a comparator"
   is "\<lambda>cmp a b. cmp b a"
@@ -244,4 +247,48 @@
     by standard (auto intro: trans_equiv trans_less simp: greater_iff_sym_less)
 qed
 
+
+subsection \<open>Direct implementations for linear orders on selected types\<close>
+
+definition comparator_bool :: "bool comparator"
+  where [simp, code_abbrev]: "comparator_bool = default"
+
+lemma compare_comparator_bool [code abstract]:
+  "compare comparator_bool = (\<lambda>p q.
+    if p then if q then Equiv else Greater
+    else if q then Less else Equiv)"
+  by (auto simp add: fun_eq_iff) (transfer; simp)+
+
+definition raw_comparator_nat :: "nat \<Rightarrow> nat \<Rightarrow> comp"
+  where [simp]: "raw_comparator_nat = compare default"
+
+lemma default_comparator_nat [simp, code]:
+  "raw_comparator_nat (0::nat) 0 = Equiv"
+  "raw_comparator_nat (Suc m) 0 = Greater"
+  "raw_comparator_nat 0 (Suc n) = Less"
+  "raw_comparator_nat (Suc m) (Suc n) = raw_comparator_nat m n"
+  by (transfer; simp)+
+
+definition comparator_nat :: "nat comparator"
+  where [simp, code_abbrev]: "comparator_nat = default"
+
+lemma compare_comparator_nat [code abstract]:
+  "compare comparator_nat = raw_comparator_nat"
+  by simp
+
+definition comparator_linordered_group :: "'a::linordered_ab_group_add comparator"
+  where [simp, code_abbrev]: "comparator_linordered_group = default"
+
+lemma comparator_linordered_group [code abstract]:
+  "compare comparator_linordered_group = (\<lambda>a b.
+    let c = a - b in if c < 0 then Less
+    else if c = 0 then Equiv else Greater)"
+proof (rule ext)+
+  fix a b :: 'a
+  show "compare comparator_linordered_group a b =
+    (let c = a - b in if c < 0 then Less
+       else if c = 0 then Equiv else Greater)"
+    by (simp add: Let_def not_less) (transfer; auto)
+qed
+
 end
diff -r 8bfa615ddde4 -r 9f8d26b8c731 src/HOL/Library/Sorting_Algorithms.thy
--- a/src/HOL/Library/Sorting_Algorithms.thy	Wed Nov 07 14:03:47 2018 +0100
+++ b/src/HOL/Library/Sorting_Algorithms.thy	Wed Nov 07 14:06:43 2018 +0100
@@ -392,9 +392,9 @@
 lemma sort_by_quicksort_rec:
   "sort cmp xs = sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Less]
     @ stable_segment cmp (xs ! (length xs div 2)) xs
-    @ sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Greater]" (is "sort cmp ?lhs = ?rhs")
+    @ sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Greater]" (is "_ = ?rhs")
 proof (rule sort_eqI)
-  show "mset ?lhs = mset ?rhs"
+  show "mset xs = mset ?rhs"
     by (rule multiset_eqI) (auto simp add: compare.sym intro: comp.exhaust)
 next
   show "sorted cmp ?rhs"
@@ -402,7 +402,6 @@
 next
   let ?pivot = "xs ! (length xs div 2)"
   fix l
-  assume "l \<in> set xs"
   have "compare cmp x ?pivot = comp \<and> compare cmp l x = Equiv
     \<longleftrightarrow> compare cmp l ?pivot = comp \<and> compare cmp l x = Equiv" for x comp
   proof -
@@ -411,7 +410,7 @@
       using that by (simp add: compare.equiv_subst_left compare.sym)
     then show ?thesis by blast
   qed
-  then show "stable_segment cmp l ?lhs = stable_segment cmp l ?rhs"
+  then show "stable_segment cmp l xs = stable_segment cmp l ?rhs"
     by (simp add: stable_sort compare.sym [of _ ?pivot])
       (cases "compare cmp l ?pivot", simp_all)
 qed
@@ -444,10 +443,8 @@
         in quicksort cmp lts @ eqs @ quicksort cmp gts)"
 proof (cases "length xs \<ge> 3")
   case False
-  then have "length xs \<le> 2"
-    by simp
-  then have "length xs = 0 \<or> length xs = 1 \<or> length xs = 2"
-    using le_neq_trans less_2_cases by auto
+  then have "length xs \<in> {0, 1, 2}"
+    by (auto simp add: not_le le_less less_antisym)
   then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]"
     by (auto simp add: length_Suc_conv numeral_2_eq_2)
   then show ?thesis
@@ -466,9 +463,208 @@
 
 end
 
-text \<open>Evaluation example\<close>
+
+subsection \<open>Mergesort\<close>
+
+definition mergesort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  where mergesort_is_sort [simp]: "mergesort = sort"
+
+lemma sort_by_mergesort:
+  "sort = mergesort"
+  by simp
+
+context
+  fixes cmp :: "'a comparator"
+begin
+
+qualified function merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+  where "merge [] ys = ys"
+  | "merge xs [] = xs"
+  | "merge (x # xs) (y # ys) = (if compare cmp x y = Greater
+      then y # merge (x # xs) ys else x # merge xs (y # ys))"
+  by pat_completeness auto
+
+qualified termination by lexicographic_order
+
+lemma mset_merge:
+  "mset (merge xs ys) = mset xs + mset ys"
+  by (induction xs ys rule: merge.induct) simp_all
+
+lemma merge_eq_Cons_imp:
+  "xs \<noteq> [] \<and> z = hd xs \<or> ys \<noteq> [] \<and> z = hd ys"
+    if "merge xs ys = z # zs"
+  using that by (induction xs ys rule: merge.induct) (auto split: if_splits)
+
+lemma filter_merge:
+  "filter P (merge xs ys) = merge (filter P xs) (filter P ys)"
+    if "sorted cmp xs" and "sorted cmp ys"
+using that proof (induction xs ys rule: merge.induct)
+  case (1 ys)
+  then show ?case
+    by simp
+next
+  case (2 xs)
+  then show ?case
+    by simp
+next
+  case (3 x xs y ys)
+  show ?case
+  proof (cases "compare cmp x y = Greater")
+    case True
+    with 3 have hyp: "filter P (merge (x # xs) ys) =
+      merge (filter P (x # xs)) (filter P ys)"
+      by (simp add: sorted_Cons_imp_sorted)
+    show ?thesis
+    proof (cases "\<not> P x \<and> P y")
+      case False
+      with \<open>compare cmp x y = Greater\<close> show ?thesis
+        by (auto simp add: hyp)
+    next
+      case True
+      from \<open>compare cmp x y = Greater\<close> "3.prems"
+      have *: "compare cmp z y = Greater" if "z \<in> set (filter P xs)" for z
+        using that by (auto dest: compare.trans_not_greater sorted_Cons_imp_not_less)
+      from \<open>compare cmp x y = Greater\<close> show ?thesis
+        by (cases "filter P xs") (simp_all add: hyp *)
+    qed
+  next
+    case False
+    with 3 have hyp: "filter P (merge xs (y # ys)) =
+      merge (filter P xs) (filter P (y # ys))"
+      by (simp add: sorted_Cons_imp_sorted)
+    show ?thesis
+    proof (cases "P x \<and> \<not> P y")
+      case False
+      with \<open>compare cmp x y \<noteq> Greater\<close> show ?thesis
+        by (auto simp add: hyp)
+    next
+      case True
+      from \<open>compare cmp x y \<noteq> Greater\<close> "3.prems"
+      have *: "compare cmp x z \<noteq> Greater" if "z \<in> set (filter P ys)" for z
+        using that by (auto dest: compare.trans_not_greater sorted_Cons_imp_not_less)
+      from \<open>compare cmp x y \<noteq> Greater\<close> show ?thesis
+        by (cases "filter P ys") (simp_all add: hyp *)
+    qed
+  qed
+qed
 
-value "let cmp = key abs (reversed default)
-  in quicksort cmp [65, 1705, -2322, 734, 4, (-17::int)]"
+lemma sorted_merge:
+  "sorted cmp (merge xs ys)" if "sorted cmp xs" and "sorted cmp ys"
+using that proof (induction xs ys rule: merge.induct)
+  case (1 ys)
+  then show ?case
+    by simp
+next
+  case (2 xs)
+  then show ?case
+    by simp
+next
+  case (3 x xs y ys)
+  show ?case
+  proof (cases "compare cmp x y = Greater")
+    case True
+    with 3 have "sorted cmp (merge (x # xs) ys)"
+      by (simp add: sorted_Cons_imp_sorted)
+    then have "sorted cmp (y # merge (x # xs) ys)"
+    proof (rule sorted_ConsI)
+      fix z zs
+      assume "merge (x # xs) ys = z # zs"
+      with 3(4) True show "compare cmp y z \<noteq> Greater"
+        by (clarsimp simp add: sorted_Cons_imp_sorted dest!: merge_eq_Cons_imp)
+          (auto simp add: compare.asym_greater sorted_Cons_imp_not_less)
+    qed
+    with True show ?thesis
+      by simp
+  next
+    case False
+    with 3 have "sorted cmp (merge xs (y # ys))"
+      by (simp add: sorted_Cons_imp_sorted)
+    then have "sorted cmp (x # merge xs (y # ys))"
+    proof (rule sorted_ConsI)
+      fix z zs
+      assume "merge xs (y # ys) = z # zs"
+      with 3(3) False show "compare cmp x z \<noteq> Greater"
+        by (clarsimp simp add: sorted_Cons_imp_sorted dest!: merge_eq_Cons_imp)
+          (auto simp add: compare.asym_greater sorted_Cons_imp_not_less)
+    qed
+    with False show ?thesis
+      by simp
+  qed
+qed
+
+lemma merge_eq_appendI:
+  "merge xs ys = xs @ ys"
+    if "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set ys \<Longrightarrow> compare cmp x y \<noteq> Greater"
+  using that by (induction xs ys rule: merge.induct) simp_all
+
+lemma merge_stable_segments:
+  "merge (stable_segment cmp l xs) (stable_segment cmp l ys) =
+     stable_segment cmp l xs @ stable_segment cmp l ys"
+  by (rule merge_eq_appendI) (auto dest: compare.trans_equiv_greater)
+
+lemma sort_by_mergesort_rec:
+  "sort cmp xs =
+    merge (sort cmp (take (length xs div 2) xs))
+      (sort cmp (drop (length xs div 2) xs))" (is "_ = ?rhs")
+proof (rule sort_eqI)
+  have "mset (take (length xs div 2) xs) + mset (drop (length xs div 2) xs) =
+    mset (take (length xs div 2) xs @ drop (length xs div 2) xs)"
+    by (simp only: mset_append)
+  then show "mset xs = mset ?rhs"
+    by (simp add: mset_merge)
+next
+  show "sorted cmp ?rhs"
+    by (simp add: sorted_merge)
+next
+  fix l
+  have "stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)
+    = stable_segment cmp l xs"
+    by (simp only: filter_append [symmetric] append_take_drop_id)
+  have "merge (stable_segment cmp l (take (length xs div 2) xs))
+    (stable_segment cmp l (drop (length xs div 2) xs)) =
+    stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)"
+    by (rule merge_eq_appendI) (auto simp add: compare.trans_equiv_greater)
+  also have "\<dots> = stable_segment cmp l xs"
+    by (simp only: filter_append [symmetric] append_take_drop_id)
+  finally show "stable_segment cmp l xs = stable_segment cmp l ?rhs"
+    by (simp add: stable_sort filter_merge)
+qed
+
+lemma mergesort_code [code]:
+  "mergesort cmp xs =
+    (case xs of
+      [] \<Rightarrow> []
+    | [x] \<Rightarrow> xs
+    | [x, y] \<Rightarrow> (if compare cmp x y \<noteq> Greater then xs else [y, x])
+    | _ \<Rightarrow>
+        let
+          half = length xs div 2;
+          ys = take half xs;
+          zs = drop half xs
+        in merge (mergesort cmp ys) (mergesort cmp zs))"
+proof (cases "length xs \<ge> 3")
+  case False
+  then have "length xs \<in> {0, 1, 2}"
+    by (auto simp add: not_le le_less less_antisym)
+  then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]"
+    by (auto simp add: length_Suc_conv numeral_2_eq_2)
+  then show ?thesis
+    by cases simp_all
+next
+  case True
+  then obtain x y z zs where "xs = x # y # z # zs"
+    by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3)
+  moreover have "mergesort cmp xs =
+    (let
+       half = length xs div 2;
+       ys = take half xs;
+       zs = drop half xs
+     in merge (mergesort cmp ys) (mergesort cmp zs))"
+    using sort_by_mergesort_rec [of xs] by (simp add: Let_def)
+  ultimately show ?thesis
+    by simp
+qed
 
 end
+
+end
diff -r 8bfa615ddde4 -r 9f8d26b8c731 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Nov 07 14:03:47 2018 +0100
+++ b/src/HOL/ROOT	Wed Nov 07 14:06:43 2018 +0100
@@ -613,6 +613,7 @@
     Set_Theory
     Simproc_Tests
     Simps_Case_Conv_Examples
+    Sorting_Algorithms_Examples
     Sqrt
     Sqrt_Script
     Sudoku
diff -r 8bfa615ddde4 -r 9f8d26b8c731 src/HOL/ex/Sorting_Algorithms_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy	Wed Nov 07 14:06:43 2018 +0100
@@ -0,0 +1,64 @@
+(*  Title:      HOL/ex/Sorting_Algorithms_Examples.thy
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+theory Sorting_Algorithms_Examples
+  imports Main "HOL-Library.Sorting_Algorithms"
+begin
+
+subsection \<open>Evaluation examples\<close>
+
+definition int_abs_reversed :: "int comparator"
+  where "int_abs_reversed = key abs (reversed default)"
+
+definition example_1 :: "int list"
+  where "example_1 = [65, 1705, -2322, 734, 4, (-17::int)]"
+
+definition example_2 :: "int list"
+  where "example_2 = [-3000..3000]"
+
+ML \<open>
+local
+
+  val term_of_int_list = HOLogic.mk_list @{typ int}
+    o map (HOLogic.mk_number @{typ int} o @{code integer_of_int});
+
+  fun raw_sort (ctxt, ct, ks) = Thm.mk_binop @{cterm "Pure.eq :: int list \<Rightarrow> int list \<Rightarrow> prop"}
+    ct (Thm.cterm_of ctxt (term_of_int_list ks));
+
+  val (_, sort_oracle) = Context.>>> (Context.map_theory_result
+    (Thm.add_oracle (@{binding sort}, raw_sort)));
+
+in
+
+  val sort_int_abs_reversed_conv = @{computation_conv "int list" terms: int_abs_reversed
+    "sort :: int comparator \<Rightarrow> _"
+    "quicksort :: int comparator \<Rightarrow> _"
+    "mergesort :: int comparator \<Rightarrow> _"
+    example_1 example_2
+  } (fn ctxt => fn ct => fn ks => sort_oracle (ctxt, ks, ct))
+
+end
+\<close>
+
+declare [[code_timing]]
+
+ML_val \<open>sort_int_abs_reversed_conv @{context}
+  @{cterm "sort int_abs_reversed example_1"}\<close>
+
+ML_val \<open>sort_int_abs_reversed_conv @{context}
+  @{cterm "quicksort int_abs_reversed example_1"}\<close>
+
+ML_val \<open>sort_int_abs_reversed_conv @{context}
+  @{cterm "mergesort int_abs_reversed example_1"}\<close>
+
+ML_val \<open>sort_int_abs_reversed_conv @{context}
+  @{cterm "sort int_abs_reversed example_2"}\<close>
+
+ML_val \<open>sort_int_abs_reversed_conv @{context}
+  @{cterm "quicksort int_abs_reversed example_2"}\<close>
+
+ML_val \<open>sort_int_abs_reversed_conv @{context}
+  @{cterm "mergesort int_abs_reversed example_2"}\<close>
+
+end