82 setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} |
82 setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} |
83 |
83 |
84 setup {* Code_Prolog.map_code_options (K |
84 setup {* Code_Prolog.map_code_options (K |
85 { ensure_groundness = true, |
85 { ensure_groundness = true, |
86 limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)], |
86 limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)], |
87 limited_predicates = [("typing", 2), ("nthel1", 2)], |
87 limited_predicates = [(["typing"], 2), (["nthel1"], 2)], |
88 replacing = [(("typing", "limited_typing"), "quickcheck"), |
88 replacing = [(("typing", "limited_typing"), "quickcheck"), |
89 (("nthel1", "limited_nthel1"), "lim_typing")], |
89 (("nthel1", "limited_nthel1"), "lim_typing")], |
|
90 manual_reorder = [], |
90 prolog_system = Code_Prolog.SWI_PROLOG}) *} |
91 prolog_system = Code_Prolog.SWI_PROLOG}) *} |
91 |
92 |
92 lemma |
93 lemma |
93 "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U" |
94 "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U" |
94 quickcheck[generator = prolog, iterations = 1, expect = counterexample] |
95 quickcheck[generator = prolog, iterations = 1, expect = counterexample] |