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
     1 theory List_Examples
     2 imports
     3   Main
     4   "~~/src/HOL/Library/Predicate_Compile_Quickcheck"
     5   "~~/src/HOL/Library/Code_Prolog"
     6 begin
     7 
     8 setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
     9 
    10 setup {* Code_Prolog.map_code_options (K 
    11   {ensure_groundness = true,
    12    limit_globally = NONE,
    13    limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
    14    limited_predicates = [(["appendP"], 4), (["revP"], 4)],
    15    replacing =
    16      [(("appendP", "limited_appendP"), "quickcheck"),
    17       (("revP", "limited_revP"), "quickcheck"),
    18       (("appendP", "limited_appendP"), "lim_revP")],
    19    manual_reorder = []}) *}
    20 
    21 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
    22 quickcheck[tester = random, iterations = 10000]
    23 quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
    24 quickcheck[tester = prolog, expect = counterexample]
    25 oops
    26 
    27 end