94 quickcheck[generator = predicate_compile_ff_fs] |
94 quickcheck[generator = predicate_compile_ff_fs] |
95 oops*) |
95 oops*) |
96 oops |
96 oops |
97 |
97 |
98 |
98 |
99 setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} |
99 setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *} |
100 |
100 |
101 setup {* Code_Prolog.map_code_options (K |
101 setup {* Code_Prolog.map_code_options (K |
102 {ensure_groundness = true, |
102 {ensure_groundness = true, |
103 limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)], |
103 limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)], |
104 limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0), |
104 limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0), |
106 replacing = |
106 replacing = |
107 [(("repP", "limited_repP"), "lim_repIntPa"), |
107 [(("repP", "limited_repP"), "lim_repIntPa"), |
108 (("subP", "limited_subP"), "repIntP"), |
108 (("subP", "limited_subP"), "repIntP"), |
109 (("repIntPa", "limited_repIntPa"), "repIntP"), |
109 (("repIntPa", "limited_repIntPa"), "repIntP"), |
110 (("accepts", "limited_accepts"), "quickcheck")], |
110 (("accepts", "limited_accepts"), "quickcheck")], |
111 manual_reorder = [], |
111 manual_reorder = []}) *} |
112 timeout = Time.fromSeconds 10, |
|
113 prolog_system = Code_Prolog.SWI_PROLOG}) *} |
|
114 |
112 |
115 text {* Finding the counterexample still seems out of reach for the |
113 text {* Finding the counterexample still seems out of reach for the |
116 prolog-style generation. *} |
114 prolog-style generation. *} |
117 |
115 |
118 lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" |
116 lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s" |