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