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