src/HOL/Predicate_Compile_Examples/List_Examples.thy
author bulwahn
Tue Sep 07 11:51:53 2010 +0200 (2010-09-07)
changeset 39184 71f3f194b962
child 39189 d183bf90dabd
permissions -rw-r--r--
adding a List example (challenge from Tobias) for counterexample search
     1 theory List_Examples
     2 imports Main "Predicate_Compile_Quickcheck" "Code_Prolog"
     3 begin
     4 
     5 setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
     6 
     7 setup {* Code_Prolog.map_code_options (K 
     8   {ensure_groundness = true,
     9    limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
    10    limited_predicates = [(["appendP"], 4), (["revP"], 4)],
    11    replacing =
    12      [(("appendP", "limited_appendP"), "quickcheck"),
    13       (("revP", "limited_revP"), "quickcheck"),
    14       (("appendP", "limited_appendP"), "lim_revP")],
    15    manual_reorder = [],
    16    prolog_system = Code_Prolog.SWI_PROLOG}) *}
    17 
    18 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
    19 quickcheck[generator = code, iterations = 200000, expect = counterexample]
    20 quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
    21 quickcheck[generator = prolog, expect = counterexample]
    22 oops
    23 
    24 end