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