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

39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	1	theory List_Examples
41413 64cd30d6b0b8 explicit file specifications -- avoid secondary load path; wenzelm parents: 40924 diff changeset	2	imports Main "~~/src/HOL/Library/Predicate_Compile_Quickcheck" "Code_Prolog"
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	3	begin
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	4
39463 7ce0ed8dc4d6 adapting examples bulwahn parents: 39189 diff changeset	5	setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	6
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	7	setup {* Code_Prolog.map_code_options (K
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	8	{ensure_groundness = true,
39800 17e29ddd538e adapting manual configuration in examples bulwahn parents: 39463 diff changeset	9	limit_globally = NONE,
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	10	limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	11	limited_predicates = [(["appendP"], 4), (["revP"], 4)],
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	12	replacing =
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	13	[(("appendP", "limited_appendP"), "quickcheck"),
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	14	(("revP", "limited_revP"), "quickcheck"),
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	15	(("appendP", "limited_appendP"), "lim_revP")],
39463 7ce0ed8dc4d6 adapting examples bulwahn parents: 39189 diff changeset	16	manual_reorder = []}) *}
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	17
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	18	lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
40924 a9be7f26b4e6 adapting predicate_compile_quickcheck bulwahn parents: 40137 diff changeset	19	quickcheck[tester = random, iterations = 10000]
a9be7f26b4e6 adapting predicate_compile_quickcheck bulwahn parents: 40137 diff changeset	20	quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
a9be7f26b4e6 adapting predicate_compile_quickcheck bulwahn parents: 40137 diff changeset	21	quickcheck[tester = prolog, expect = counterexample]
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	22	oops
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	end

author	wenzelm
	Mon, 24 Jan 2011 21:30:33 +0100
changeset 41628	ed4d793f0c26
parent 41413	64cd30d6b0b8
child 41956	c15ef1b85035
permissions	-rw-r--r--