# HG changeset patch # User bulwahn # Date 1301473862 -7200 # Node ID d1b39536e1fb1026d28a20bc956790f41b9b2449 # Parent 43cba90b080f486d6a45cb9c2f5caefd75b9e60a adding a regression test for SML_Quickcheck; putting SML_Quickcheck back in shape diff -r 43cba90b080f -r d1b39536e1fb src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Mar 30 09:44:17 2011 +0200 +++ b/src/HOL/IsaMakefile Wed Mar 30 10:31:02 2011 +0200 @@ -1049,7 +1049,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/Quickcheck_Narrowing_Examples.thy ex/SML_Quickcheck_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 43cba90b080f -r d1b39536e1fb src/HOL/Library/SML_Quickcheck.thy --- a/src/HOL/Library/SML_Quickcheck.thy Wed Mar 30 09:44:17 2011 +0200 +++ b/src/HOL/Library/SML_Quickcheck.thy Wed Mar 30 10:31:02 2011 +0200 @@ -10,7 +10,8 @@ Context.theory_map (Quickcheck.add_generator ("SML", fn ctxt => fn [(t, eval_terms)] => let - val test_fun = Codegen.test_term ctxt t + 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 = @@ -21,7 +22,7 @@ in case result of NONE => iterate size (j - 1) | SOME q => SOME q end - in fn [size] => (iterate size iterations, NONE) end)) + in fn [_, size] => (iterate size iterations, NONE) end)) *} end diff -r 43cba90b080f -r d1b39536e1fb src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Wed Mar 30 09:44:17 2011 +0200 +++ b/src/HOL/ex/ROOT.ML Wed Mar 30 10:31:02 2011 +0200 @@ -64,6 +64,7 @@ "HarmonicSeries", "Refute_Examples", "Quickcheck_Examples", + "SML_Quickcheck_Examples", "Quickcheck_Lattice_Examples", "Landau", "Execute_Choice", diff -r 43cba90b080f -r d1b39536e1fb src/HOL/ex/SML_Quickcheck_Examples.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/SML_Quickcheck_Examples.thy Wed Mar 30 10:31:02 2011 +0200 @@ -0,0 +1,142 @@ +(* 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]] + +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 \ No newline at end of file