|
1 (* Title: HOL/ex/Sorting_Algorithms_Examples.thy |
|
2 Author: Florian Haftmann, TU Muenchen |
|
3 *) |
|
4 |
|
5 theory Sorting_Algorithms_Examples |
|
6 imports Main "HOL-Library.Sorting_Algorithms" |
|
7 begin |
|
8 |
|
9 subsection \<open>Evaluation examples\<close> |
|
10 |
|
11 definition int_abs_reversed :: "int comparator" |
|
12 where "int_abs_reversed = key abs (reversed default)" |
|
13 |
|
14 definition example_1 :: "int list" |
|
15 where "example_1 = [65, 1705, -2322, 734, 4, (-17::int)]" |
|
16 |
|
17 definition example_2 :: "int list" |
|
18 where "example_2 = [-3000..3000]" |
|
19 |
|
20 ML \<open> |
|
21 local |
|
22 |
|
23 val term_of_int_list = HOLogic.mk_list @{typ int} |
|
24 o map (HOLogic.mk_number @{typ int} o @{code integer_of_int}); |
|
25 |
|
26 fun raw_sort (ctxt, ct, ks) = Thm.mk_binop @{cterm "Pure.eq :: int list \<Rightarrow> int list \<Rightarrow> prop"} |
|
27 ct (Thm.cterm_of ctxt (term_of_int_list ks)); |
|
28 |
|
29 val (_, sort_oracle) = Context.>>> (Context.map_theory_result |
|
30 (Thm.add_oracle (@{binding sort}, raw_sort))); |
|
31 |
|
32 in |
|
33 |
|
34 val sort_int_abs_reversed_conv = @{computation_conv "int list" terms: int_abs_reversed |
|
35 "sort :: int comparator \<Rightarrow> _" |
|
36 "quicksort :: int comparator \<Rightarrow> _" |
|
37 "mergesort :: int comparator \<Rightarrow> _" |
|
38 example_1 example_2 |
|
39 } (fn ctxt => fn ct => fn ks => sort_oracle (ctxt, ks, ct)) |
|
40 |
|
41 end |
|
42 \<close> |
|
43 |
|
44 declare [[code_timing]] |
|
45 |
|
46 ML_val \<open>sort_int_abs_reversed_conv @{context} |
|
47 @{cterm "sort int_abs_reversed example_1"}\<close> |
|
48 |
|
49 ML_val \<open>sort_int_abs_reversed_conv @{context} |
|
50 @{cterm "quicksort int_abs_reversed example_1"}\<close> |
|
51 |
|
52 ML_val \<open>sort_int_abs_reversed_conv @{context} |
|
53 @{cterm "mergesort int_abs_reversed example_1"}\<close> |
|
54 |
|
55 ML_val \<open>sort_int_abs_reversed_conv @{context} |
|
56 @{cterm "sort int_abs_reversed example_2"}\<close> |
|
57 |
|
58 ML_val \<open>sort_int_abs_reversed_conv @{context} |
|
59 @{cterm "quicksort int_abs_reversed example_2"}\<close> |
|
60 |
|
61 ML_val \<open>sort_int_abs_reversed_conv @{context} |
|
62 @{cterm "mergesort int_abs_reversed example_2"}\<close> |
|
63 |
|
64 end |