Quelle  Sorting_Algorithms_Examples.thy

(*  Title:      HOL/ex/Sorting_Algorithms_Examples.thy
  Author: Florian Haftmann, TU Muenchen
*)

theory Sorting_Algorithms_Examples
  imports Main "HOL-Library.Sorting_Algorithms"
begin

subsection ‹Evaluation examples›

definition int_abs_reversed :: "int comparator"
  where "int_abs_reversed = key abs (reversed default)"

definition example_1 :: "int list"
  where "example_1 = [65, 1705, -2322, 734, 4, (-17::int)]"

definition example_2 :: "int list"
  where "example_2 = [-3000..3000]"

ML ‹
 local
 
  val term_of_int_list = HOLogic.mk_list 🍋‹int›
  o map (HOLogic.mk_number 🍋‹int› o @{code integer_of_int});
 
  fun raw_sort (ctxt, ct, ks) =
  🍋‹x = ct and y = ‹Thm.cterm_of ctxt (term_of_int_list ks)›
  in cterm ‹x ≡ y› for x y :: ‹int list›\›;
 
  val (_, sort_oracle) = Theory.setup_result (Thm.add_oracle (🍋‹sort›, raw_sort));
 
 in
 
  val sort_int_abs_reversed_conv = @{computation_conv "int list" terms: int_abs_reversed
  "sort :: int comparator ==> _"
  "quicksort :: int comparator ==> _"
  "mergesort :: int comparator ==> _"
  example_1 example_2
  } (fn ctxt => fn ct => fn ks => sort_oracle (ctxt, ks, ct))
 
 end
 ›

declare [[code_timing]]

ML_val ‹sort_int_abs_reversed_conv 🍋
  🍋‹sort int_abs_reversed example_1›\›

ML_val ‹sort_int_abs_reversed_conv 🍋
  🍋‹quicksort int_abs_reversed example_1›\›

ML_val ‹sort_int_abs_reversed_conv 🍋
  🍋‹mergesort int_abs_reversed example_1›\›

ML_val ‹sort_int_abs_reversed_conv 🍋
  🍋‹sort int_abs_reversed example_2›\›

ML_val ‹sort_int_abs_reversed_conv 🍋
  🍋‹quicksort int_abs_reversed example_2›\›

ML_val ‹sort_int_abs_reversed_conv 🍋
  🍋‹mergesort int_abs_reversed example_2›\›

end