adding a List example (challenge from Tobias) for counterexample search
authorbulwahn
Tue Sep 07 11:51:53 2010 +0200 (2010-09-07)
changeset 3918471f3f194b962
parent 39183 512c10416590
child 39185 c035d01a7e77
adding a List example (challenge from Tobias) for counterexample search
src/HOL/IsaMakefile
src/HOL/Predicate_Compile_Examples/List_Examples.thy
src/HOL/Predicate_Compile_Examples/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Sep 07 11:51:53 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Sep 07 11:51:53 2010 +0200
     1.3 @@ -1326,7 +1326,8 @@
     1.4    Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy  \
     1.5    Predicate_Compile_Examples/Code_Prolog_Examples.thy 			\
     1.6    Predicate_Compile_Examples/Hotel_Example.thy 				\
     1.7 -  Predicate_Compile_Examples/Lambda_Example.thy 
     1.8 +  Predicate_Compile_Examples/Lambda_Example.thy 			\
     1.9 +  Predicate_Compile_Examples/List_Examples.thy 
    1.10  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
    1.11  
    1.12  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
     2.3 @@ -0,0 +1,24 @@
     2.4 +theory List_Examples
     2.5 +imports Main "Predicate_Compile_Quickcheck" "Code_Prolog"
     2.6 +begin
     2.7 +
     2.8 +setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
     2.9 +
    2.10 +setup {* Code_Prolog.map_code_options (K 
    2.11 +  {ensure_groundness = true,
    2.12 +   limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
    2.13 +   limited_predicates = [(["appendP"], 4), (["revP"], 4)],
    2.14 +   replacing =
    2.15 +     [(("appendP", "limited_appendP"), "quickcheck"),
    2.16 +      (("revP", "limited_revP"), "quickcheck"),
    2.17 +      (("appendP", "limited_appendP"), "lim_revP")],
    2.18 +   manual_reorder = [],
    2.19 +   prolog_system = Code_Prolog.SWI_PROLOG}) *}
    2.20 +
    2.21 +lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
    2.22 +quickcheck[generator = code, iterations = 200000, expect = counterexample]
    2.23 +quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
    2.24 +quickcheck[generator = prolog, expect = counterexample]
    2.25 +oops
    2.26 +
    2.27 +end
    2.28 \ No newline at end of file
     3.1 --- a/src/HOL/Predicate_Compile_Examples/ROOT.ML	Tue Sep 07 11:51:53 2010 +0200
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML	Tue Sep 07 11:51:53 2010 +0200
     3.3 @@ -1,2 +1,2 @@
     3.4  use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
     3.5 -if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example", "Lambda_Example"];
     3.6 +if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example", "Lambda_Example", "List_Examples"];