src/HOL/Predicate_Compile_Examples/List_Examples.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66453 cc19f7ca2ed6
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more robust sorted_entries;
bulwahn@39184
     1
theory List_Examples
wenzelm@41956
     2
imports
wenzelm@41956
     3
  Main
wenzelm@66453
     4
  "HOL-Library.Predicate_Compile_Quickcheck"
wenzelm@66453
     5
  "HOL-Library.Code_Prolog"
bulwahn@39184
     6
begin
bulwahn@39184
     7
wenzelm@63167
     8
setup \<open>
wenzelm@52666
     9
  Context.theory_map
wenzelm@52666
    10
    (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
wenzelm@63167
    11
\<close>
bulwahn@39184
    12
wenzelm@63167
    13
setup \<open>Code_Prolog.map_code_options (K 
bulwahn@39184
    14
  {ensure_groundness = true,
bulwahn@39800
    15
   limit_globally = NONE,
bulwahn@39184
    16
   limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
bulwahn@39184
    17
   limited_predicates = [(["appendP"], 4), (["revP"], 4)],
bulwahn@39184
    18
   replacing =
bulwahn@39184
    19
     [(("appendP", "limited_appendP"), "quickcheck"),
bulwahn@39184
    20
      (("revP", "limited_revP"), "quickcheck"),
bulwahn@39184
    21
      (("appendP", "limited_appendP"), "lim_revP")],
wenzelm@63167
    22
   manual_reorder = []})\<close>
bulwahn@39184
    23
bulwahn@39184
    24
lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
bulwahn@40924
    25
quickcheck[tester = random, iterations = 10000]
bulwahn@45451
    26
quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
bulwahn@40924
    27
quickcheck[tester = prolog, expect = counterexample]
bulwahn@39184
    28
oops
bulwahn@39184
    29
nipkow@62390
    30
end