77 lemma [code_pred_inline]: "(x::nat) + 1 = Suc x" |
77 lemma [code_pred_inline]: "(x::nat) + 1 = Suc x" |
78 by simp |
78 by simp |
79 |
79 |
80 section {* Manual setup to find counterexample *} |
80 section {* Manual setup to find counterexample *} |
81 |
81 |
82 setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *} |
82 setup {* Context.theory_map (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 manual_reorder = []}) *} |
91 timeout = Time.fromSeconds 10, |
|
92 prolog_system = Code_Prolog.SWI_PROLOG}) *} |
|
93 |
91 |
94 lemma |
92 lemma |
95 "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U" |
93 "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U" |
96 quickcheck[generator = prolog, iterations = 1, expect = counterexample] |
94 quickcheck[generator = prolog, iterations = 1, expect = counterexample] |
97 oops |
95 oops |