src/HOL/Predicate_Compile_Examples/List_Examples.thy
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 40924 a9be7f26b4e6
child 41413 64cd30d6b0b8
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     1 theory List_Examples
     2 imports Main "Predicate_Compile_Quickcheck" "Code_Prolog"
     3 begin
     4 
     5 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
     6 
     7 setup {* Code_Prolog.map_code_options (K 
     8   {ensure_groundness = true,
     9    limit_globally = NONE,
    10    limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
    11    limited_predicates = [(["appendP"], 4), (["revP"], 4)],
    12    replacing =
    13      [(("appendP", "limited_appendP"), "quickcheck"),
    14       (("revP", "limited_revP"), "quickcheck"),
    15       (("appendP", "limited_appendP"), "lim_revP")],
    16    manual_reorder = []}) *}
    17 
    18 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
    19 quickcheck[tester = random, iterations = 10000]
    20 quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
    21 quickcheck[tester = prolog, expect = counterexample]
    22 oops
    23 
    24 end