dedicated examples for sorting
authorhaftmann
Wed Nov 07 11:08:12 2018 +0000 (6 months ago)
changeset 69252fc359b60121c
parent 69251 d240598e8637
child 69254 9f8d26b8c731
dedicated examples for sorting
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/ROOT
src/HOL/ex/Sorting_Algorithms_Examples.thy
     1.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Wed Nov 07 11:08:11 2018 +0000
     1.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Wed Nov 07 11:08:12 2018 +0000
     1.3 @@ -7,6 +7,7 @@
     1.4  imports
     1.5    Complex_Main
     1.6    "HOL-Library.Library"
     1.7 +  "HOL-Library.Sorting_Algorithms"
     1.8    "HOL-Library.Subseq_Order"
     1.9    "HOL-Library.RBT"
    1.10    "HOL-Data_Structures.Tree_Map"
     2.1 --- a/src/HOL/ROOT	Wed Nov 07 11:08:11 2018 +0000
     2.2 +++ b/src/HOL/ROOT	Wed Nov 07 11:08:12 2018 +0000
     2.3 @@ -613,6 +613,7 @@
     2.4      Set_Theory
     2.5      Simproc_Tests
     2.6      Simps_Case_Conv_Examples
     2.7 +    Sorting_Algorithms_Examples
     2.8      Sqrt
     2.9      Sqrt_Script
    2.10      Sudoku
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy	Wed Nov 07 11:08:12 2018 +0000
     3.3 @@ -0,0 +1,64 @@
     3.4 +(*  Title:      HOL/ex/Sorting_Algorithms_Examples.thy
     3.5 +    Author:     Florian Haftmann, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +theory Sorting_Algorithms_Examples
     3.9 +  imports Main "HOL-Library.Sorting_Algorithms"
    3.10 +begin
    3.11 +
    3.12 +subsection \<open>Evaluation examples\<close>
    3.13 +
    3.14 +definition int_abs_reversed :: "int comparator"
    3.15 +  where "int_abs_reversed = key abs (reversed default)"
    3.16 +
    3.17 +definition example_1 :: "int list"
    3.18 +  where "example_1 = [65, 1705, -2322, 734, 4, (-17::int)]"
    3.19 +
    3.20 +definition example_2 :: "int list"
    3.21 +  where "example_2 = [-3000..3000]"
    3.22 +
    3.23 +ML \<open>
    3.24 +local
    3.25 +
    3.26 +  val term_of_int_list = HOLogic.mk_list @{typ int}
    3.27 +    o map (HOLogic.mk_number @{typ int} o @{code integer_of_int});
    3.28 +
    3.29 +  fun raw_sort (ctxt, ct, ks) = Thm.mk_binop @{cterm "Pure.eq :: int list \<Rightarrow> int list \<Rightarrow> prop"}
    3.30 +    ct (Thm.cterm_of ctxt (term_of_int_list ks));
    3.31 +
    3.32 +  val (_, sort_oracle) = Context.>>> (Context.map_theory_result
    3.33 +    (Thm.add_oracle (@{binding sort}, raw_sort)));
    3.34 +
    3.35 +in
    3.36 +
    3.37 +  val sort_int_abs_reversed_conv = @{computation_conv "int list" terms: int_abs_reversed
    3.38 +    "sort :: int comparator \<Rightarrow> _"
    3.39 +    "quicksort :: int comparator \<Rightarrow> _"
    3.40 +    "mergesort :: int comparator \<Rightarrow> _"
    3.41 +    example_1 example_2
    3.42 +  } (fn ctxt => fn ct => fn ks => sort_oracle (ctxt, ks, ct))
    3.43 +
    3.44 +end
    3.45 +\<close>
    3.46 +
    3.47 +declare [[code_timing]]
    3.48 +
    3.49 +ML_val \<open>sort_int_abs_reversed_conv @{context}
    3.50 +  @{cterm "sort int_abs_reversed example_1"}\<close>
    3.51 +
    3.52 +ML_val \<open>sort_int_abs_reversed_conv @{context}
    3.53 +  @{cterm "quicksort int_abs_reversed example_1"}\<close>
    3.54 +
    3.55 +ML_val \<open>sort_int_abs_reversed_conv @{context}
    3.56 +  @{cterm "mergesort int_abs_reversed example_1"}\<close>
    3.57 +
    3.58 +ML_val \<open>sort_int_abs_reversed_conv @{context}
    3.59 +  @{cterm "sort int_abs_reversed example_2"}\<close>
    3.60 +
    3.61 +ML_val \<open>sort_int_abs_reversed_conv @{context}
    3.62 +  @{cterm "quicksort int_abs_reversed example_2"}\<close>
    3.63 +
    3.64 +ML_val \<open>sort_int_abs_reversed_conv @{context}
    3.65 +  @{cterm "mergesort int_abs_reversed example_2"}\<close>
    3.66 +
    3.67 +end