src/HOL/ex/Sorting_Algorithms_Examples.thy
 author haftmann Wed Nov 07 11:08:12 2018 +0000 (7 months ago) changeset 69252 fc359b60121c child 69597 ff784d5a5bfb permissions -rw-r--r--
dedicated examples for sorting
```     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
```