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

39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	1	theory List_Examples
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	2	imports Main "Predicate_Compile_Quickcheck" "Code_Prolog"
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
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	5	setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
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,
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	9	limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	10	limited_predicates = [(["appendP"], 4), (["revP"], 4)],
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	11	replacing =
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	12	[(("appendP", "limited_appendP"), "quickcheck"),
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	13	(("revP", "limited_revP"), "quickcheck"),
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	14	(("appendP", "limited_appendP"), "lim_revP")],
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	15	manual_reorder = [],
39189 d183bf90dabd adapting example files bulwahn parents: 39184 diff changeset	16	timeout = Time.fromSeconds 10,
39184 71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	17	prolog_system = Code_Prolog.SWI_PROLOG}) *}
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	18
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	19	lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	20	quickcheck[generator = code, iterations = 200000, expect = counterexample]
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	21	quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	22	quickcheck[generator = prolog, expect = counterexample]
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	23	oops
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	24
71f3f194b962 adding a List example (challenge from Tobias) for counterexample search bulwahn parents: diff changeset	25	end

author	blanchet
	Thu, 16 Sep 2010 07:30:15 +0200
changeset 39444	beabb8443ee4
parent 39189	d183bf90dabd
child 39463	7ce0ed8dc4d6
permissions	-rw-r--r--