isabelle: src/HOL/Predicate_Compile_Examples/List_Examples.thy@b041137f7fe5 (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
c15ef1b85035 modernized imports (untested!?); wenzelm parents: 41413 diff changeset	4	"~~/src/HOL/Library/Predicate_Compile_Quickcheck"
c15ef1b85035 modernized imports (untested!?); wenzelm parents: 41413 diff changeset	5	"~~/src/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
43937 768c70befd59 adapting two examples in Predicate_Compile_Examples bulwahn parents: 41956 diff changeset	8	setup {* Context.theory_map (Quickcheck.add_tester ("prolog", (Code_Prolog.active, Code_Prolog.test_goals))) *}
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	9
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	10	setup {* Code_Prolog.map_code_options (K
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	11	{ensure_groundness = true,
39800 17e29ddd538e adapting manual configuration in examples bulwahn parents: 39463 diff changeset	12	limit_globally = NONE,
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	13	limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	14	limited_predicates = [(["appendP"], 4), (["revP"], 4)],
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	15	replacing =
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	16	[(("appendP", "limited_appendP"), "quickcheck"),
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	17	(("revP", "limited_revP"), "quickcheck"),
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	18	(("appendP", "limited_appendP"), "lim_revP")],
39463 7ce0ed8dc4d6 adapting examples bulwahn parents: 39189 diff changeset	19	manual_reorder = []}) *}
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	20
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	21	lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
40924 a9be7f26b4e6 adapting predicate_compile_quickcheck bulwahn parents: 40137 diff changeset	22	quickcheck[tester = random, iterations = 10000]
45451 74515e8e6046 renaming example invocations: tester predicate_compile is renamed to smart_exhaustive bulwahn parents: 43937 diff changeset	23	quickcheck[tester = smart_exhaustive, iterations = 1, expect = counterexample]
40924 a9be7f26b4e6 adapting predicate_compile_quickcheck bulwahn parents: 40137 diff changeset	24	quickcheck[tester = prolog, expect = counterexample]
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	25	oops
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	26
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	27	end

author	nipkow
	Mon, 18 Mar 2013 12:31:13 +0100
changeset 51448	b041137f7fe5
parent 45451	74515e8e6046
child 52666	391913d17d15
permissions	-rw-r--r--