# 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"];