--- a/src/HOL/IsaMakefile Mon Jul 25 10:42:32 2011 +0200
+++ b/src/HOL/IsaMakefile Mon Jul 25 10:43:14 2011 +0200
@@ -476,7 +476,7 @@
Library/RBT.thy Library/RBT_Impl.thy Library/RBT_Mapping.thy \
Library/README.html \
Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \
- Library/Reflection.thy Library/SML_Quickcheck.thy \
+ Library/Reflection.thy \
Library/Sublist_Order.thy Library/Sum_of_Squares.thy \
Library/Sum_of_Squares/sos_wrapper.ML \
Library/Sum_of_Squares/sum_of_squares.ML \
@@ -1062,7 +1062,7 @@
ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
- ex/Quickcheck_Narrowing_Examples.thy ex/SML_Quickcheck_Examples.thy \
+ ex/Quickcheck_Narrowing_Examples.thy \
ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
--- a/src/HOL/Library/Library.thy Mon Jul 25 10:42:32 2011 +0200
+++ b/src/HOL/Library/Library.thy Mon Jul 25 10:43:14 2011 +0200
@@ -55,7 +55,6 @@
Reflection
RBT_Mapping
Set_Algebras
- SML_Quickcheck
State_Monad
Sum_of_Squares
Transitive_Closure_Table
--- a/src/HOL/Library/SML_Quickcheck.thy Mon Jul 25 10:42:32 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-
-header {* Install quickcheck of SML code generator *}
-
-theory SML_Quickcheck
-imports Main
-begin
-
-ML {*
-signature SML_QUICKCHECK =
-sig
- val active : bool Config.T
- val setup : theory -> theory
-end;
-
-structure SML_Quickcheck : SML_QUICKCHECK =
-struct
-
-val active = Attrib.setup_config_bool @{binding quickcheck_SML_active} (K true);
-
-fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] =
- let
- val prop = list_abs_free (Term.add_frees t [], t)
- val test_fun = Codegen.test_term ctxt prop
- val iterations = Config.get ctxt Quickcheck.iterations
- fun iterate size 0 = NONE
- | iterate size j =
- let
- val result = test_fun size handle Match =>
- (if Config.get ctxt Quickcheck.quiet then ()
- else warning "Exception Match raised during quickcheck"; NONE)
- in
- case result of NONE => iterate size (j - 1) | SOME q => SOME q
- end
- in (iterate size iterations, NONE) end
-
-val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr
-
-val setup =
- Inductive_Codegen.quickcheck_setup
- #> Context.theory_map (Quickcheck.add_tester ("SML", (active, test_goals)))
-
-end;
-*}
-
-setup {* SML_Quickcheck.setup *}
-
-end
--- a/src/HOL/ex/ROOT.ML Mon Jul 25 10:42:32 2011 +0200
+++ b/src/HOL/ex/ROOT.ML Mon Jul 25 10:43:14 2011 +0200
@@ -64,7 +64,6 @@
"HarmonicSeries",
"Refute_Examples",
"Quickcheck_Examples",
- "SML_Quickcheck_Examples",
"Quickcheck_Lattice_Examples",
"Landau",
"Execute_Choice",
--- a/src/HOL/ex/SML_Quickcheck_Examples.thy Mon Jul 25 10:42:32 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,143 +0,0 @@
-(* Title: HOL/ex/SML_Quickcheck_Examples.thy
- Author: Stefan Berghofer, Lukas Bulwahn
- Copyright 2011 TU Muenchen
-*)
-
-theory SML_Quickcheck_Examples
-imports "~~/src/HOL/Library/SML_Quickcheck"
-begin
-
-text {*
-This is a regression test for the 'quickcheck' counterexample generator based on the
-SML code generator.
-
-The counterexample generator has been superseded by counterexample generators based on
-the generic code generator.
-*}
-
-declare [[quickcheck_finite_types = false]]
-declare [[quickcheck_timeout = 600.0]]
-
-subsection {* Lists *}
-
-theorem "map g (map f xs) = map (g o f) xs"
- quickcheck[SML, expect = no_counterexample]
- oops
-
-theorem "map g (map f xs) = map (f o g) xs"
- quickcheck[SML, expect = counterexample]
- oops
-
-theorem "rev (xs @ ys) = rev ys @ rev xs"
- quickcheck[SML, expect = no_counterexample]
- oops
-
-theorem "rev (xs @ ys) = rev xs @ rev ys"
- quickcheck[SML, expect = counterexample]
- oops
-
-theorem "rev (rev xs) = xs"
- quickcheck[SML, expect = no_counterexample]
- oops
-
-theorem "rev xs = xs"
- quickcheck[tester = SML, expect = counterexample]
-oops
-
-
-text {* An example involving functions inside other data structures *}
-
-primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
- "app [] x = x"
- | "app (f # fs) x = app fs (f x)"
-
-lemma "app (fs @ gs) x = app gs (app fs x)"
- quickcheck[SML, expect = no_counterexample]
- by (induct fs arbitrary: x) simp_all
-
-lemma "app (fs @ gs) x = app fs (app gs x)"
- quickcheck[SML, expect = counterexample]
- oops
-
-primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
- "occurs a [] = 0"
- | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
-
-primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "del1 a [] = []"
- | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
-
-text {* A lemma, you'd think to be true from our experience with delAll *}
-lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
- -- {* Wrong. Precondition needed.*}
- quickcheck[SML, expect = counterexample]
- oops
-
-lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
- quickcheck[SML, expect = counterexample]
- -- {* Also wrong.*}
- oops
-
-lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
- quickcheck[SML, expect = no_counterexample]
- by (induct xs) auto
-
-primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
- "replace a b [] = []"
- | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
- else (x#(replace a b xs)))"
-
-lemma "occurs a xs = occurs b (replace a b xs)"
- quickcheck[SML, expect = counterexample]
- -- {* Wrong. Precondition needed.*}
- oops
-
-lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
- quickcheck[SML, expect = no_counterexample]
- by (induct xs) simp_all
-
-
-subsection {* Trees *}
-
-datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree"
-
-primrec leaves :: "'a tree \<Rightarrow> 'a list" where
- "leaves Twig = []"
- | "leaves (Leaf a) = [a]"
- | "leaves (Branch l r) = (leaves l) @ (leaves r)"
-
-primrec plant :: "'a list \<Rightarrow> 'a tree" where
- "plant [] = Twig "
- | "plant (x#xs) = Branch (Leaf x) (plant xs)"
-
-primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
- "mirror (Twig) = Twig "
- | "mirror (Leaf a) = Leaf a "
- | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
-
-theorem "plant (rev (leaves xt)) = mirror xt"
- quickcheck[SML, expect = counterexample]
- --{* Wrong! *}
- oops
-
-theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
- quickcheck[SML, expect = counterexample]
- --{* Wrong! *}
- oops
-
-datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
-
-primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
- "inOrder (Tip a)= [a]"
- | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
-
-primrec root :: "'a ntree \<Rightarrow> 'a" where
- "root (Tip a) = a"
- | "root (Node f x y) = f"
-
-theorem "hd (inOrder xt) = root xt"
- quickcheck[SML, expect = counterexample]
- --{* Wrong! *}
- oops
-
-end