diff -r d240598e8637 -r fc359b60121c src/HOL/ex/Sorting_Algorithms_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy Wed Nov 07 11:08:12 2018 +0000 @@ -0,0 +1,64 @@ +(* 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 @{typ int} + o map (HOLogic.mk_number @{typ int} o @{code integer_of_int}); + + fun raw_sort (ctxt, ct, ks) = Thm.mk_binop @{cterm "Pure.eq :: int list \ int list \ prop"} + ct (Thm.cterm_of ctxt (term_of_int_list ks)); + + val (_, sort_oracle) = Context.>>> (Context.map_theory_result + (Thm.add_oracle (@{binding 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 @{context} + @{cterm "sort int_abs_reversed example_1"}\ + +ML_val \sort_int_abs_reversed_conv @{context} + @{cterm "quicksort int_abs_reversed example_1"}\ + +ML_val \sort_int_abs_reversed_conv @{context} + @{cterm "mergesort int_abs_reversed example_1"}\ + +ML_val \sort_int_abs_reversed_conv @{context} + @{cterm "sort int_abs_reversed example_2"}\ + +ML_val \sort_int_abs_reversed_conv @{context} + @{cterm "quicksort int_abs_reversed example_2"}\ + +ML_val \sort_int_abs_reversed_conv @{context} + @{cterm "mergesort int_abs_reversed example_2"}\ + +end