# HG changeset patch
# User bulwahn
# Date 1284637748 -7200
# Node ID 7ce0ed8dc4d6f76b7c9e41c99fcc1d2f339e3c44
# Parent  3a86194d15344fbf601d224f21170aa33ac1cd08
adapting examples

diff -r 3a86194d1534 -r 7ce0ed8dc4d6 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Sep 16 13:49:06 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Sep 16 13:49:08 2010 +0200
@@ -15,9 +15,7 @@
    limited_types = [],
    limited_predicates = [],
    replacing = [],
-   manual_reorder = [],
-   timeout = Time.fromSeconds 10,
-   prolog_system = Code_Prolog.SWI_PROLOG}) *}
+   manual_reorder = []}) *}
 
 values "{(x, y, z). append x y z}"
 
@@ -28,9 +26,7 @@
    limited_types = [],
    limited_predicates = [],
    replacing = [],
-   manual_reorder = [],
-   timeout = Time.fromSeconds 10,
-   prolog_system = Code_Prolog.YAP}) *}
+   manual_reorder = []}) *}
 
 values "{(x, y, z). append x y z}"
 
@@ -39,9 +35,7 @@
    limited_types = [],
    limited_predicates = [],
    replacing = [],
-   manual_reorder = [],
-   timeout = Time.fromSeconds 10,
-   prolog_system = Code_Prolog.SWI_PROLOG}) *}
+   manual_reorder = []}) *}
 
 
 section {* Example queens *}
@@ -209,9 +203,7 @@
    limited_types = [],
    limited_predicates = [],
    replacing = [],
-   manual_reorder = [], 
-   timeout = Time.fromSeconds 10,
-   prolog_system = Code_Prolog.SWI_PROLOG}) *}
+   manual_reorder = []}) *}
 
 values 2 "{y. notB y}"
 
diff -r 3a86194d1534 -r 7ce0ed8dc4d6 src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Thu Sep 16 13:49:06 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Thu Sep 16 13:49:08 2010 +0200
@@ -19,7 +19,7 @@
 declare size_list_def[symmetric, code_pred_inline]
 
 
-setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
 
 datatype alphabet = a | b
 
@@ -61,9 +61,7 @@
   limited_types = [],
   limited_predicates = [(["s1", "a1", "b1"], 2)],
   replacing = [(("s1", "limited_s1"), "quickcheck")],
-  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
-  timeout = Time.fromSeconds 10,
-  prolog_system = Code_Prolog.SWI_PROLOG}) *}
+  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
 
 
 theorem S\<^isub>1_sound:
@@ -86,9 +84,7 @@
   limited_types = [],
   limited_predicates = [(["s2", "a2", "b2"], 3)],
   replacing = [(("s2", "limited_s2"), "quickcheck")],
-  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
-  timeout = Time.fromSeconds 10,
-  prolog_system = Code_Prolog.SWI_PROLOG}) *}
+  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
 
 
 theorem S\<^isub>2_sound:
@@ -110,9 +106,7 @@
   limited_types = [],
   limited_predicates = [(["s3", "a3", "b3"], 6)],
   replacing = [(("s3", "limited_s3"), "quickcheck")],
-  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
-  timeout = Time.fromSeconds 10,
-  prolog_system = Code_Prolog.SWI_PROLOG}) *}
+  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
 
 lemma S\<^isub>3_sound:
 "w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
@@ -152,9 +146,7 @@
   limited_types = [],
   limited_predicates = [(["s4", "a4", "b4"], 6)],
   replacing = [(("s4", "limited_s4"), "quickcheck")],
-  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
-  timeout = Time.fromSeconds 10,
-  prolog_system = Code_Prolog.SWI_PROLOG}) *}
+  manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])]}) *}
 
 
 theorem S\<^isub>4_sound:
diff -r 3a86194d1534 -r 7ce0ed8dc4d6 src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Sep 16 13:49:06 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy	Thu Sep 16 13:49:08 2010 +0200
@@ -89,14 +89,12 @@
   limited_types = [],
   limited_predicates = [],
   replacing = [],
-  manual_reorder = [],
-  timeout = Time.fromSeconds 10,
-  prolog_system = Code_Prolog.SWI_PROLOG}) *}
+  manual_reorder = []}) *}
 
 values 40 "{s. hotel s}"
 
 
-setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
 
 lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
 quickcheck[generator = code, iterations = 100000, report]
@@ -119,9 +117,7 @@
    limited_types = [],
    limited_predicates = [(["hotel"], 5)],
    replacing = [(("hotel", "limited_hotel"), "quickcheck")],
-   manual_reorder = [],
-   timeout = Time.fromSeconds 10,
-   prolog_system = Code_Prolog.SWI_PROLOG}) *}
+   manual_reorder = []}) *}
 
 lemma
   "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
diff -r 3a86194d1534 -r 7ce0ed8dc4d6 src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Thu Sep 16 13:49:06 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Thu Sep 16 13:49:08 2010 +0200
@@ -79,7 +79,7 @@
 
 section {* Manual setup to find counterexample *}
 
-setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
 
 setup {* Code_Prolog.map_code_options (K 
   { ensure_groundness = true,
@@ -87,9 +87,7 @@
     limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
     replacing = [(("typing", "limited_typing"), "quickcheck"),
                  (("nthel1", "limited_nthel1"), "lim_typing")],
-    manual_reorder = [],
-    timeout = Time.fromSeconds 10,
-    prolog_system = Code_Prolog.SWI_PROLOG}) *}
+    manual_reorder = []}) *}
 
 lemma
   "\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
diff -r 3a86194d1534 -r 7ce0ed8dc4d6 src/HOL/Predicate_Compile_Examples/List_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Thu Sep 16 13:49:06 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Thu Sep 16 13:49:08 2010 +0200
@@ -2,7 +2,7 @@
 imports Main "Predicate_Compile_Quickcheck" "Code_Prolog"
 begin
 
-setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
 
 setup {* Code_Prolog.map_code_options (K 
   {ensure_groundness = true,
@@ -12,9 +12,7 @@
      [(("appendP", "limited_appendP"), "quickcheck"),
       (("revP", "limited_revP"), "quickcheck"),
       (("appendP", "limited_appendP"), "lim_revP")],
-   manual_reorder = [],
-   timeout = Time.fromSeconds 10,
-   prolog_system = Code_Prolog.SWI_PROLOG}) *}
+   manual_reorder = []}) *}
 
 lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
 quickcheck[generator = code, iterations = 200000, expect = counterexample]
diff -r 3a86194d1534 -r 7ce0ed8dc4d6 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Thu Sep 16 13:49:06 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Thu Sep 16 13:49:08 2010 +0200
@@ -96,7 +96,7 @@
 oops
 
 
-setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
 
 setup {* Code_Prolog.map_code_options (K 
   {ensure_groundness = true,
@@ -108,9 +108,7 @@
       (("subP", "limited_subP"), "repIntP"),
       (("repIntPa", "limited_repIntPa"), "repIntP"),
       (("accepts", "limited_accepts"), "quickcheck")],  
-   manual_reorder = [],
-   timeout = Time.fromSeconds 10,
-   prolog_system = Code_Prolog.SWI_PROLOG}) *}
+   manual_reorder = []}) *}
 
 text {* Finding the counterexample still seems out of reach for the
  prolog-style generation. *}