isabelle: src/HOL/Predicate_Compile_Examples/List_Examples.thy@6c56f2ebe157 (annotated)

39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	1	theory List_Examples
41956 c15ef1b85035 modernized imports (untested!?); wenzelm parents: 41413 diff changeset	2	imports
c15ef1b85035 modernized imports (untested!?); wenzelm parents: 41413 diff changeset	3	Main
66453 cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63167 diff changeset	4	"HOL-Library.Predicate_Compile_Quickcheck"
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a; wenzelm parents: 63167 diff changeset	5	"HOL-Library.Code_Prolog"
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	6	begin
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	7
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62390 diff changeset	8	setup \<open>
52666 391913d17d15 tuned line length; wenzelm parents: 45451 diff changeset	9	Context.theory_map
391913d17d15 tuned line length; wenzelm parents: 45451 diff changeset	10	(Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals)))
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62390 diff changeset	11	\<close>
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	12
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62390 diff changeset	13	setup \<open>Code_Prolog.map_code_options (K
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	14	{ensure_groundness = true,
39800 17e29ddd538e adapting manual configuration in examples bulwahn parents: 39463 diff changeset	15	limit_globally = NONE,
69597 ff784d5a5bfb isabelle update -u control_cartouches; wenzelm parents: 66453 diff changeset	16	limited_types = [(\<^typ>\<open>nat\<close>, 2), (\<^typ>\<open>nat list\<close>, 4)],
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	17	limited_predicates = [(["appendP"], 4), (["revP"], 4)],
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	18	replacing =
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	19	[(("appendP", "limited_appendP"), "quickcheck"),
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	20	(("revP", "limited_revP"), "quickcheck"),
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	21	(("appendP", "limited_appendP"), "lim_revP")],
63167 0909deb8059b isabelle update_cartouches -c -t; wenzelm parents: 62390 diff changeset	22	manual_reorder = []})\<close>
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	23
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	24	lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
40924 a9be7f26b4e6 adapting predicate_compile_quickcheck bulwahn parents: 40137 diff changeset	25	quickcheck[tester = random, iterations = 10000]
45451 74515e8e6046 renaming example invocations: tester predicate_compile is renamed to smart_exhaustive bulwahn parents: 43937 diff changeset	26	quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
40924 a9be7f26b4e6 adapting predicate_compile_quickcheck bulwahn parents: 40137 diff changeset	27	quickcheck[tester = prolog, expect = counterexample]
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	28	oops
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	29
62390 842917225d56 more canonical names nipkow parents: 52666 diff changeset	30	end

author	wenzelm
	Tue, 11 May 2021 20:19:07 +0200
changeset 73675	6c56f2ebe157
parent 69597	ff784d5a5bfb
permissions	-rw-r--r--