--- 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}"
--- 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:
--- 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"
--- 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"
--- 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]
--- 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. *}