src/HOL/Predicate_Compile_Examples/List_Examples.thy
author bulwahn
Thu Sep 30 10:48:12 2010 +0200 (2010-09-30)
changeset 39800 17e29ddd538e
parent 39463 7ce0ed8dc4d6
child 40137 9eabcb1bfe50
permissions -rw-r--r--
adapting manual configuration in examples
bulwahn@39184
     1
theory List_Examples
bulwahn@39184
     2
imports Main "Predicate_Compile_Quickcheck" "Code_Prolog"
bulwahn@39184
     3
begin
bulwahn@39184
     4
bulwahn@39463
     5
setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
bulwahn@39184
     6
bulwahn@39184
     7
setup {* Code_Prolog.map_code_options (K 
bulwahn@39184
     8
  {ensure_groundness = true,
bulwahn@39800
     9
   limit_globally = NONE,
bulwahn@39184
    10
   limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
bulwahn@39184
    11
   limited_predicates = [(["appendP"], 4), (["revP"], 4)],
bulwahn@39184
    12
   replacing =
bulwahn@39184
    13
     [(("appendP", "limited_appendP"), "quickcheck"),
bulwahn@39184
    14
      (("revP", "limited_revP"), "quickcheck"),
bulwahn@39184
    15
      (("appendP", "limited_appendP"), "lim_revP")],
bulwahn@39463
    16
   manual_reorder = []}) *}
bulwahn@39184
    17
bulwahn@39184
    18
lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
bulwahn@39184
    19
quickcheck[generator = code, iterations = 200000, expect = counterexample]
bulwahn@39184
    20
quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
bulwahn@39184
    21
quickcheck[generator = prolog, expect = counterexample]
bulwahn@39184
    22
oops
bulwahn@39184
    23
bulwahn@39184
    24
end