# HG changeset patch
# User haftmann
# Date 1541588892 0
# Node ID fc359b60121c35688096b13d047faea6945a7f5a
# Parent  d240598e8637416a3926ff353a1723a3fc460bae
dedicated examples for sorting

diff -r d240598e8637 -r fc359b60121c src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Wed Nov 07 11:08:11 2018 +0000
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Wed Nov 07 11:08:12 2018 +0000
@@ -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 d240598e8637 -r fc359b60121c src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Nov 07 11:08:11 2018 +0000
+++ b/src/HOL/ROOT	Wed Nov 07 11:08:12 2018 +0000
@@ -613,6 +613,7 @@
     Set_Theory
     Simproc_Tests
     Simps_Case_Conv_Examples
+    Sorting_Algorithms_Examples
     Sqrt
     Sqrt_Script
     Sudoku
diff -r d240598e8637 -r fc359b60121c 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 11:08:12 2018 +0000
@@ -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