# HG changeset patch
# User bulwahn
# Date 1283853113 -7200
# Node ID 71f3f194b962f1efc7e05119b0c01314349b1f0e
# Parent  512c10416590ee5d7157a330d117bd207ee85f8c
adding a List example (challenge from Tobias) for counterexample search

diff -r 512c10416590 -r 71f3f194b962 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 07 11:51:53 2010 +0200
@@ -1326,7 +1326,8 @@
   Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy  \
   Predicate_Compile_Examples/Code_Prolog_Examples.thy 			\
   Predicate_Compile_Examples/Hotel_Example.thy 				\
-  Predicate_Compile_Examples/Lambda_Example.thy 
+  Predicate_Compile_Examples/Lambda_Example.thy 			\
+  Predicate_Compile_Examples/List_Examples.thy 
 	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
 
 
diff -r 512c10416590 -r 71f3f194b962 src/HOL/Predicate_Compile_Examples/List_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -0,0 +1,24 @@
+theory List_Examples
+imports Main "Predicate_Compile_Quickcheck" "Code_Prolog"
+begin
+
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+
+setup {* Code_Prolog.map_code_options (K 
+  {ensure_groundness = true,
+   limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
+   limited_predicates = [(["appendP"], 4), (["revP"], 4)],
+   replacing =
+     [(("appendP", "limited_appendP"), "quickcheck"),
+      (("revP", "limited_revP"), "quickcheck"),
+      (("appendP", "limited_appendP"), "lim_revP")],
+   manual_reorder = [],
+   prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
+quickcheck[generator = code, iterations = 200000, expect = counterexample]
+quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
+quickcheck[generator = prolog, expect = counterexample]
+oops
+
+end
\ No newline at end of file
diff -r 512c10416590 -r 71f3f194b962 src/HOL/Predicate_Compile_Examples/ROOT.ML
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Tue Sep 07 11:51:53 2010 +0200
@@ -1,2 +1,2 @@
 use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
-if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example", "Lambda_Example"];
+if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example", "Lambda_Example", "List_Examples"];