src/HOL/ex/Sorting_Algorithms_Examples.thy
 changeset 69252 fc359b60121c child 69597 ff784d5a5bfb
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy	Wed Nov 07 11:08:12 2018 +0000
1.3 @@ -0,0 +1,64 @@
1.4 +(*  Title:      HOL/ex/Sorting_Algorithms_Examples.thy
1.5 +    Author:     Florian Haftmann, TU Muenchen
1.6 +*)
1.7 +
1.8 +theory Sorting_Algorithms_Examples
1.9 +  imports Main "HOL-Library.Sorting_Algorithms"
1.10 +begin
1.11 +
1.12 +subsection \<open>Evaluation examples\<close>
1.13 +
1.14 +definition int_abs_reversed :: "int comparator"
1.15 +  where "int_abs_reversed = key abs (reversed default)"
1.16 +
1.17 +definition example_1 :: "int list"
1.18 +  where "example_1 = [65, 1705, -2322, 734, 4, (-17::int)]"
1.19 +
1.20 +definition example_2 :: "int list"
1.21 +  where "example_2 = [-3000..3000]"
1.22 +
1.23 +ML \<open>
1.24 +local
1.25 +
1.26 +  val term_of_int_list = HOLogic.mk_list @{typ int}
1.27 +    o map (HOLogic.mk_number @{typ int} o @{code integer_of_int});
1.28 +
1.29 +  fun raw_sort (ctxt, ct, ks) = Thm.mk_binop @{cterm "Pure.eq :: int list \<Rightarrow> int list \<Rightarrow> prop"}
1.30 +    ct (Thm.cterm_of ctxt (term_of_int_list ks));
1.31 +
1.32 +  val (_, sort_oracle) = Context.>>> (Context.map_theory_result
1.33 +    (Thm.add_oracle (@{binding sort}, raw_sort)));
1.34 +
1.35 +in
1.36 +
1.37 +  val sort_int_abs_reversed_conv = @{computation_conv "int list" terms: int_abs_reversed
1.38 +    "sort :: int comparator \<Rightarrow> _"
1.39 +    "quicksort :: int comparator \<Rightarrow> _"
1.40 +    "mergesort :: int comparator \<Rightarrow> _"
1.41 +    example_1 example_2
1.42 +  } (fn ctxt => fn ct => fn ks => sort_oracle (ctxt, ks, ct))
1.43 +
1.44 +end
1.45 +\<close>
1.46 +
1.47 +declare [[code_timing]]
1.48 +
1.49 +ML_val \<open>sort_int_abs_reversed_conv @{context}
1.50 +  @{cterm "sort int_abs_reversed example_1"}\<close>
1.51 +
1.52 +ML_val \<open>sort_int_abs_reversed_conv @{context}
1.53 +  @{cterm "quicksort int_abs_reversed example_1"}\<close>
1.54 +
1.55 +ML_val \<open>sort_int_abs_reversed_conv @{context}
1.56 +  @{cterm "mergesort int_abs_reversed example_1"}\<close>
1.57 +
1.58 +ML_val \<open>sort_int_abs_reversed_conv @{context}
1.59 +  @{cterm "sort int_abs_reversed example_2"}\<close>
1.60 +
1.61 +ML_val \<open>sort_int_abs_reversed_conv @{context}
1.62 +  @{cterm "quicksort int_abs_reversed example_2"}\<close>
1.63 +
1.64 +ML_val \<open>sort_int_abs_reversed_conv @{context}
1.65 +  @{cterm "mergesort int_abs_reversed example_2"}\<close>
1.66 +
1.67 +end
```