author bulwahn Fri, 03 Dec 2010 08:40:47 +0100 changeset 40924 a9be7f26b4e6 parent 40923 be80c93ac0a2 child 40925 7abeb749ae99
```--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -33,7 +33,7 @@

lemma
"w \<in> S\<^isub>1 \<Longrightarrow> w = []"
-quickcheck[generator = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops

definition "filter_a = filter (\<lambda>x. x = a)"
@@ -67,7 +67,7 @@

theorem S\<^isub>1_sound:
"w \<in> S\<^isub>1 \<Longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops

@@ -91,7 +91,7 @@

theorem S\<^isub>2_sound:
"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=prolog, iterations=1, expect = counterexample]
+quickcheck[tester = prolog, iterations=1, expect = counterexample]
oops

inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
@@ -113,7 +113,7 @@

lemma S\<^isub>3_sound:
"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator=prolog, iterations=1, size=1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations=1, size=1, expect = no_counterexample]
oops

@@ -131,7 +131,7 @@

theorem S\<^isub>3_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
-quickcheck[generator = prolog, size=1, iterations=1]
+quickcheck[tester = prolog, size=1, iterations=1]
oops
*)

@@ -156,7 +156,7 @@

theorem S\<^isub>4_sound:
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = prolog, size=1, iterations=1, expect = no_counterexample]
+quickcheck[tester = prolog, size=1, iterations=1, expect = no_counterexample]
oops

(*```
```--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -23,8 +23,8 @@
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 = 10000, report]
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = random, iterations = 10000, report]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops

section {* Manual setup to find the counterexample *}
@@ -39,7 +39,7 @@

lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
oops

setup {* Code_Prolog.map_code_options (K
@@ -52,7 +52,7 @@

lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops

section {* Simulating a global depth limit manually by limiting all predicates *}
@@ -70,7 +70,7 @@

lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
oops

setup {*
@@ -86,7 +86,7 @@

lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops

section {* Using a global limit for limiting the execution *}
@@ -105,7 +105,7 @@

lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = no_counterexample]
oops

text {* But a global depth limit of 14 does. *}
@@ -122,7 +122,7 @@

lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops

end
\ No newline at end of file```
```--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -50,8 +50,8 @@

lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
-quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
+quickcheck[tester = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
+quickcheck[tester = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
oops

```
```--- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -27,7 +27,7 @@

lemma
"exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 10, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10, expect = counterexample]
oops

```
```--- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -30,7 +30,7 @@

lemma
"exec c s s' ==> exec (Seq c c) s s'"
-quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 10]
+quickcheck[tester = predicate_compile_wo_ff, size = 2, iterations = 10]
oops

```
```--- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -30,7 +30,7 @@

lemma
"exec c s s' ==> exec (Seq c c) s s'"
-  quickcheck[generator = predicate_compile_ff_nofs, size=2, iterations=10, quiet = false, expect = counterexample]
+  quickcheck[tester = predicate_compile_ff_nofs, size=2, iterations=10, quiet = false, expect = counterexample]
oops

```
```--- a/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -31,7 +31,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
nitpick (* nitpick fails here! *)
-  quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample]
+  quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample]
oops

end
\ No newline at end of file```
```--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -92,7 +92,7 @@

lemma
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
-quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, iterations = 1, expect = counterexample]
oops

text {* Verifying that the found counterexample really is one by means of a proof *}```
```--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -16,9 +16,9 @@
manual_reorder = []}) *}

lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
-quickcheck[generator = code, iterations = 10000]
-quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
-quickcheck[generator = prolog, expect = counterexample]
+quickcheck[tester = random, iterations = 10000]
+quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
+quickcheck[tester = prolog, expect = counterexample]
oops

end
\ No newline at end of file```
```--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -48,7 +48,7 @@

lemma
"is_ten x = is_eleven x"
-quickcheck[generator = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff, iterations = 1, size = 1, expect = counterexample]
oops

section {* Context Free Grammar *}
@@ -65,7 +65,7 @@

lemma
"w \<in> S\<^isub>1 \<Longrightarrow> w = []"
-quickcheck[generator = predicate_compile_ff_nofs, iterations=1]
+quickcheck[tester = predicate_compile_ff_nofs, iterations=1]
oops

theorem S\<^isub>1_sound:
@@ -136,7 +136,7 @@
oops

lemma "\<not> (length w > 2) \<or> \<not> (length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b])"
-quickcheck[size=10, generator = predicate_compile_ff_fs]
+quickcheck[size=10, tester = predicate_compile_ff_fs]
oops

theorem S\<^isub>3_complete:
@@ -157,12 +157,12 @@

theorem S\<^isub>4_sound:
"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
-quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
+quickcheck[tester = predicate_compile_ff_nofs, size=5, iterations=1]
oops

theorem S\<^isub>4_complete:
"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
-quickcheck[generator = predicate_compile_ff_nofs, size=5, iterations=1]
+quickcheck[tester = predicate_compile_ff_nofs, size=5, iterations=1]
oops

hide_const a b
@@ -202,7 +202,7 @@

lemma
"exec c s s' ==> exec (Seq c c) s s'"
-  quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample]
+  quickcheck[tester = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample]
oops

subsection {* Lambda *}
@@ -257,7 +257,7 @@

lemma
"\<Gamma> \<turnstile> t : U \<Longrightarrow> t \<rightarrow>\<^sub>\<beta> t' \<Longrightarrow> \<Gamma> \<turnstile> t' : U"
-quickcheck[generator = predicate_compile_ff_fs, size = 7, iterations = 10]
+quickcheck[tester = predicate_compile_ff_fs, size = 7, iterations = 10]
oops

@@ -341,12 +341,12 @@
"jad_mv v = inflate o split zip o apsnd (map listsum o transpose o map (map (\<lambda> (i, x). v ! i * x)))"

lemma "matrix (M::int list list) rs cs \<Longrightarrow> False"
-quickcheck[generator = predicate_compile_ff_nofs, size = 6]
+quickcheck[tester = predicate_compile_ff_nofs, size = 6]
oops

lemma
"\<lbrakk> matrix M rs cs ; length v = cs \<rbrakk> \<Longrightarrow> jad_mv v (jad M) = mv M v"
-quickcheck[generator = predicate_compile_wo_ff]
+quickcheck[tester = predicate_compile_wo_ff]
oops

end```
```--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Fri Dec 03 08:40:47 2010 +0100
@@ -89,9 +89,9 @@

lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
(*nitpick
-quickcheck[generator = code, iterations = 10000]
-quickcheck[generator = predicate_compile_wo_ff]
-quickcheck[generator = predicate_compile_ff_fs]
+quickcheck[tester = random, iterations = 10000]
+quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = predicate_compile_ff_fs]
oops*)
oops

@@ -115,10 +115,10 @@
prolog-style generation. *}

lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-quickcheck[generator = code, iterations = 100000, expect = counterexample]
-(*quickcheck[generator = predicate_compile_wo_ff]*)
-(*quickcheck[generator = predicate_compile_ff_fs, iterations = 1]*)
-(*quickcheck[generator = prolog, iterations = 1, size = 1]*)
+quickcheck[tester = random, iterations = 100000, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff]*)
+(*quickcheck[tester = predicate_compile_ff_fs, iterations = 1]*)
+(*quickcheck[tester = prolog, iterations = 1, size = 1]*)
oops

section {* Given a partial solution *}
@@ -130,8 +130,8 @@
assumes "q = Seq (Sym N0) (Sym N0)"
(*  assumes "s = [N0, N0]"*)
shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1]*)
-quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1]*)
+quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
oops

section {* Checking the counterexample *}
@@ -147,7 +147,7 @@
assumes "q = Seq (Sym N0) (Sym N0)"
assumes "s = [N0, N0]"
shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
-(*quickcheck[generator = predicate_compile_wo_ff]*)
+(*quickcheck[tester = predicate_compile_wo_ff]*)
oops

lemma
@@ -157,8 +157,8 @@
assumes "q = Seq (Sym N0) (Sym N0)"
assumes "s = [N0, N0]"
shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
-(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
-quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+(*quickcheck[tester = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
+quickcheck[tester = prolog, iterations = 1, size = 1, expect = counterexample]
oops

lemma
@@ -168,13 +168,13 @@
assumes "q = Seq (Sym N0) (Sym N0)"
assumes "s = [N0, N0]"
shows "prop_regex (n, (k, (p, (q, s))))"
-quickcheck[generator = predicate_compile_wo_ff]
-quickcheck[generator = prolog, expect = counterexample]
+quickcheck[tester = predicate_compile_wo_ff]
+quickcheck[tester = prolog, expect = counterexample]
oops

lemma "prop_regex a_sol"
-quickcheck[generator = code, expect = counterexample]
-quickcheck[generator = predicate_compile_ff_fs]
+quickcheck[tester = random, expect = counterexample]
+quickcheck[tester = predicate_compile_ff_fs]
oops

value [code] "prop_regex a_sol"```
```--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -38,7 +38,7 @@
val write_program : logic_program -> string
val run : (Time.time * prolog_system) -> logic_program -> (string * prol_term list) -> string list -> int option -> prol_term list list

-  val quickcheck : Proof.context -> term -> int -> term list option * (bool list * bool)
+  val quickcheck : Proof.context -> term -> int -> term list option * Quickcheck.report option

val trace : bool Unsynchronized.ref

@@ -129,8 +129,8 @@

(* general string functions *)

-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
+val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
+val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;

(* internal program representation *)

@@ -835,7 +835,7 @@

val parse_term = fst o Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise Fail "parsing prolog output failed")) scan_term)
-  o explode
+  o raw_explode

fun parse_solutions sol =
let
@@ -1030,9 +1030,8 @@
case tss of
[ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ map snd vs'))
| _ => NONE
-    val empty_report = ([], false)
in
-    (res, empty_report)
+    (res, NONE)
end;

end;```
```--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -22,7 +22,7 @@
val tracing : bool Unsynchronized.ref;
val quiet : bool Unsynchronized.ref;
val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
-    Proof.context -> term -> int -> term list option * (bool list * bool);
+    Proof.context -> term -> int -> term list option * Quickcheck.report option;
(*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
val nrandom : int Unsynchronized.ref;
val debug : bool Unsynchronized.ref;
@@ -344,9 +344,8 @@
fun compile_term' compilation options depth ctxt t =
let
val c = compile_term compilation options ctxt t
-    val dummy_report = ([], false)
in
-    fn size => (try_upto (!quiet) (c size (!nrandom)) depth, dummy_report)
+    fn size => (try_upto (!quiet) (c size (!nrandom)) depth, NONE)
end

fun quickcheck_compile_term compilation function_flattening fail_safe_function_flattening depth =```