src/HOL/Predicate_Compile_Examples/List_Examples.thy
author hoelzl
Tue Nov 05 09:44:57 2013 +0100 (2013-11-05)
changeset 54257 5c7a3b6b05a9
parent 52666 391913d17d15
child 62390 842917225d56
permissions -rw-r--r--
generalize SUP and INF to the syntactic type classes Sup and Inf
     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 {*
     9   Context.theory_map
    10     (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
    11 *}
    12 
    13 setup {* Code_Prolog.map_code_options (K 
    14   {ensure_groundness = true,
    15    limit_globally = NONE,
    16    limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
    17    limited_predicates = [(["appendP"], 4), (["revP"], 4)],
    18    replacing =
    19      [(("appendP", "limited_appendP"), "quickcheck"),
    20       (("revP", "limited_revP"), "quickcheck"),
    21       (("appendP", "limited_appendP"), "lim_revP")],
    22    manual_reorder = []}) *}
    23 
    24 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
    25 quickcheck[tester = random, iterations = 10000]
    26 quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
    27 quickcheck[tester = prolog, expect = counterexample]
    28 oops
    29 
    30 end