src/HOL/Predicate_Compile_Examples/List_Examples.thy
author bulwahn
Thu Jul 21 08:31:35 2011 +0200 (2011-07-21)
changeset 43937 768c70befd59
parent 41956 c15ef1b85035
child 45451 74515e8e6046
permissions -rw-r--r--
adapting two examples in Predicate_Compile_Examples
bulwahn@39184
     1
theory List_Examples
wenzelm@41956
     2
imports
wenzelm@41956
     3
  Main
wenzelm@41956
     4
  "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
wenzelm@41956
     5
  "~~/src/HOL/Library/Code_Prolog"
bulwahn@39184
     6
begin
bulwahn@39184
     7
bulwahn@43937
     8
setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
bulwahn@39184
     9
bulwahn@39184
    10
setup {* Code_Prolog.map_code_options (K 
bulwahn@39184
    11
  {ensure_groundness = true,
bulwahn@39800
    12
   limit_globally = NONE,
bulwahn@39184
    13
   limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
bulwahn@39184
    14
   limited_predicates = [(["appendP"], 4), (["revP"], 4)],
bulwahn@39184
    15
   replacing =
bulwahn@39184
    16
     [(("appendP", "limited_appendP"), "quickcheck"),
bulwahn@39184
    17
      (("revP", "limited_revP"), "quickcheck"),
bulwahn@39184
    18
      (("appendP", "limited_appendP"), "lim_revP")],
bulwahn@39463
    19
   manual_reorder = []}) *}
bulwahn@39184
    20
bulwahn@39184
    21
lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
bulwahn@40924
    22
quickcheck[tester = random, iterations = 10000]
bulwahn@40924
    23
quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
bulwahn@40924
    24
quickcheck[tester = prolog, expect = counterexample]
bulwahn@39184
    25
oops
bulwahn@39184
    26
bulwahn@39184
    27
end