src/HOL/Predicate_Compile_Examples/List_Examples.thy
author wenzelm
Sun Mar 13 21:21:48 2011 +0100 (2011-03-13)
changeset 41956 c15ef1b85035
parent 41413 64cd30d6b0b8
child 43937 768c70befd59
permissions -rw-r--r--
modernized imports (untested!?);
     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_generator ("prolog", Code_Prolog.quickcheck)) *}
     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