1.1 --- a/src/HOL/IsaMakefile	Wed Mar 30 09:44:17 2011 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed Mar 30 10:31:02 2011 +0200
     1.3 @@ -1049,7 +1049,7 @@
     1.4    ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy	\
     1.5    ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
     1.6    ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy		\
     1.7 -  ex/Quickcheck_Narrowing_Examples.thy \
     1.8 +  ex/Quickcheck_Narrowing_Examples.thy ex/SML_Quickcheck_Examples.thy   \
     1.9    ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
    1.10    ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy	\
    1.11    ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy			\

     2.1 --- a/src/HOL/Library/SML_Quickcheck.thy	Wed Mar 30 09:44:17 2011 +0200
     2.2 +++ b/src/HOL/Library/SML_Quickcheck.thy	Wed Mar 30 10:31:02 2011 +0200
     2.3 @@ -10,7 +10,8 @@
     2.4    Context.theory_map (Quickcheck.add_generator ("SML",
     2.5      fn ctxt => fn [(t, eval_terms)] =>
     2.6        let
     2.7 -        val test_fun = Codegen.test_term ctxt t 
     2.8 +        val prop = list_abs_free (Term.add_frees t [], t)
     2.9 +        val test_fun = Codegen.test_term ctxt prop 
    2.10          val iterations = Config.get ctxt Quickcheck.iterations
    2.11          fun iterate size 0 = NONE
    2.12            | iterate size j =
    2.13 @@ -21,7 +22,7 @@
    2.14              in
    2.15                case result of NONE => iterate size (j - 1) | SOME q => SOME q
    2.16              end
    2.17 -     in fn [size] => (iterate size iterations, NONE) end))
    2.18 +     in fn [_, size] => (iterate size iterations, NONE) end))
    2.19  *}
    2.20  
    2.21  end

     3.1 --- a/src/HOL/ex/ROOT.ML	Wed Mar 30 09:44:17 2011 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Wed Mar 30 10:31:02 2011 +0200
     3.3 @@ -64,6 +64,7 @@
     3.4    "HarmonicSeries",
     3.5    "Refute_Examples",
     3.6    "Quickcheck_Examples",
     3.7 +  "SML_Quickcheck_Examples",
     3.8    "Quickcheck_Lattice_Examples",
     3.9    "Landau",
    3.10    "Execute_Choice",

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/ex/SML_Quickcheck_Examples.thy	Wed Mar 30 10:31:02 2011 +0200
     4.3 @@ -0,0 +1,142 @@
     4.4 +(*  Title:      HOL/ex/SML_Quickcheck_Examples.thy
     4.5 +    Author:     Stefan Berghofer, Lukas Bulwahn
     4.6 +    Copyright   2011 TU Muenchen
     4.7 +*)
     4.8 +
     4.9 +theory SML_Quickcheck_Examples
    4.10 +imports "~~/src/HOL/Library/SML_Quickcheck"
    4.11 +begin
    4.12 +
    4.13 +text {*
    4.14 +This is a regression test for the 'quickcheck' counterexample generator based on the
    4.15 +SML code generator.
    4.16 +
    4.17 +The counterexample generator has been superseded by counterexample generators based on
    4.18 +the generic code generator.
    4.19 +*}
    4.20 +
    4.21 +declare [[quickcheck_finite_types = false]]
    4.22 +
    4.23 +subsection {* Lists *}
    4.24 +
    4.25 +theorem "map g (map f xs) = map (g o f) xs"
    4.26 +  quickcheck[SML, expect = no_counterexample]
    4.27 +  oops
    4.28 +
    4.29 +theorem "map g (map f xs) = map (f o g) xs"
    4.30 +  quickcheck[SML, expect = counterexample]
    4.31 +  oops
    4.32 +
    4.33 +theorem "rev (xs @ ys) = rev ys @ rev xs"
    4.34 +  quickcheck[SML, expect = no_counterexample]
    4.35 +  oops
    4.36 +
    4.37 +theorem "rev (xs @ ys) = rev xs @ rev ys"
    4.38 +  quickcheck[SML, expect = counterexample]
    4.39 +  oops
    4.40 +
    4.41 +theorem "rev (rev xs) = xs"
    4.42 +  quickcheck[SML, expect = no_counterexample]
    4.43 +  oops
    4.44 +
    4.45 +theorem "rev xs = xs"
    4.46 +  quickcheck[tester = SML, expect = counterexample]
    4.47 +oops
    4.48 +
    4.49 +
    4.50 +text {* An example involving functions inside other data structures *}
    4.51 +
    4.52 +primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
    4.53 +  "app [] x = x"
    4.54 +  | "app (f # fs) x = app fs (f x)"
    4.55 +
    4.56 +lemma "app (fs @ gs) x = app gs (app fs x)"
    4.57 +  quickcheck[SML, expect = no_counterexample]
    4.58 +  by (induct fs arbitrary: x) simp_all
    4.59 +
    4.60 +lemma "app (fs @ gs) x = app fs (app gs x)"
    4.61 +  quickcheck[SML, expect = counterexample]
    4.62 +  oops
    4.63 +
    4.64 +primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
    4.65 +  "occurs a [] = 0"
    4.66 +  | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
    4.67 +
    4.68 +primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    4.69 +  "del1 a [] = []"
    4.70 +  | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
    4.71 +
    4.72 +text {* A lemma, you'd think to be true from our experience with delAll *}
    4.73 +lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
    4.74 +  -- {* Wrong. Precondition needed.*}
    4.75 +  quickcheck[SML, expect = counterexample]
    4.76 +  oops
    4.77 +
    4.78 +lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
    4.79 +  quickcheck[SML, expect = counterexample]
    4.80 +    -- {* Also wrong.*}
    4.81 +  oops
    4.82 +
    4.83 +lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
    4.84 +  quickcheck[SML, expect = no_counterexample]
    4.85 +  by (induct xs) auto
    4.86 +
    4.87 +primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    4.88 +  "replace a b [] = []"
    4.89 +  | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
    4.90 +                            else (x#(replace a b xs)))"
    4.91 +
    4.92 +lemma "occurs a xs = occurs b (replace a b xs)"
    4.93 +  quickcheck[SML, expect = counterexample]
    4.94 +  -- {* Wrong. Precondition needed.*}
    4.95 +  oops
    4.96 +
    4.97 +lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
    4.98 +  quickcheck[SML, expect = no_counterexample]
    4.99 +  by (induct xs) simp_all
   4.100 +
   4.101 +
   4.102 +subsection {* Trees *}
   4.103 +
   4.104 +datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
   4.105 +
   4.106 +primrec leaves :: "'a tree \<Rightarrow> 'a list" where
   4.107 +  "leaves Twig = []"
   4.108 +  | "leaves (Leaf a) = [a]"
   4.109 +  | "leaves (Branch l r) = (leaves l) @ (leaves r)"
   4.110 +
   4.111 +primrec plant :: "'a list \<Rightarrow> 'a tree" where
   4.112 +  "plant [] = Twig "
   4.113 +  | "plant (x#xs) = Branch (Leaf x) (plant xs)"
   4.114 +
   4.115 +primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
   4.116 +  "mirror (Twig) = Twig "
   4.117 +  | "mirror (Leaf a) = Leaf a "
   4.118 +  | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
   4.119 +
   4.120 +theorem "plant (rev (leaves xt)) = mirror xt"
   4.121 +  quickcheck[SML, expect = counterexample]
   4.122 +    --{* Wrong! *} 
   4.123 +  oops
   4.124 +
   4.125 +theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
   4.126 +  quickcheck[SML, expect = counterexample]
   4.127 +    --{* Wrong! *} 
   4.128 +  oops
   4.129 +
   4.130 +datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
   4.131 +
   4.132 +primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
   4.133 +  "inOrder (Tip a)= [a]"
   4.134 +  | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
   4.135 +
   4.136 +primrec root :: "'a ntree \<Rightarrow> 'a" where
   4.137 +  "root (Tip a) = a"
   4.138 +  | "root (Node f x y) = f"
   4.139 +
   4.140 +theorem "hd (inOrder xt) = root xt"
   4.141 +  quickcheck[SML, expect = counterexample]
   4.142 +  --{* Wrong! *} 
   4.143 +  oops
   4.144 +
   4.145 +end
   4.146 \ No newline at end of file