# HG changeset patch # User bulwahn # Date 1311583394 -7200 # Node ID bc5e767f0f464f67bdeada2c527392256c4c631b # Parent 64f88ef1835e125c86c86d056ee679f694a1c6e1 removing SML_Quickcheck diff -r 64f88ef1835e -r bc5e767f0f46 src/HOL/IsaMakefile --- 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 \ diff -r 64f88ef1835e -r bc5e767f0f46 src/HOL/Library/Library.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 diff -r 64f88ef1835e -r bc5e767f0f46 src/HOL/Library/SML_Quickcheck.thy --- 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 diff -r 64f88ef1835e -r bc5e767f0f46 src/HOL/ex/ROOT.ML --- 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", diff -r 64f88ef1835e -r bc5e767f0f46 src/HOL/ex/SML_Quickcheck_Examples.thy --- 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 \ 'a) list \ 'a \ '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 \ 'a list \ nat" where - "occurs a [] = 0" - | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" - -primrec del1 :: "'a \ 'a list \ '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 ~= [] \ Suc (occurs a (del1 a xs)) = occurs a xs" - quickcheck[SML, expect = counterexample] - -- {* Also wrong.*} - oops - -lemma "0 < occurs a xs \ Suc (occurs a (del1 a xs)) = occurs a xs" - quickcheck[SML, expect = no_counterexample] - by (induct xs) auto - -primrec replace :: "'a \ 'a \ 'a list \ '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 \ a=b \ 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 \ 'a list" where - "leaves Twig = []" - | "leaves (Leaf a) = [a]" - | "leaves (Branch l r) = (leaves l) @ (leaves r)" - -primrec plant :: "'a list \ 'a tree" where - "plant [] = Twig " - | "plant (x#xs) = Branch (Leaf x) (plant xs)" - -primrec mirror :: "'a tree \ '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 \ 'a list" where - "inOrder (Tip a)= [a]" - | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)" - -primrec root :: "'a ntree \ '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