1.1 --- a/src/HOL/IsaMakefile Mon Jul 25 10:42:32 2011 +0200
1.2 +++ b/src/HOL/IsaMakefile Mon Jul 25 10:43:14 2011 +0200
1.3 @@ -476,7 +476,7 @@
1.4 Library/RBT.thy Library/RBT_Impl.thy Library/RBT_Mapping.thy \
1.5 Library/README.html \
1.6 Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \
1.7 - Library/Reflection.thy Library/SML_Quickcheck.thy \
1.8 + Library/Reflection.thy \
1.9 Library/Sublist_Order.thy Library/Sum_of_Squares.thy \
1.10 Library/Sum_of_Squares/sos_wrapper.ML \
1.11 Library/Sum_of_Squares/sum_of_squares.ML \
1.12 @@ -1062,7 +1062,7 @@
1.13 ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
1.14 ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
1.15 ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
1.16 - ex/Quickcheck_Narrowing_Examples.thy ex/SML_Quickcheck_Examples.thy \
1.17 + ex/Quickcheck_Narrowing_Examples.thy \
1.18 ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
1.19 ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
1.20 ex/SVC_Oracle.thy ex/Serbian.thy ex/Set_Algebras.thy \
2.1 --- a/src/HOL/Library/Library.thy Mon Jul 25 10:42:32 2011 +0200
2.2 +++ b/src/HOL/Library/Library.thy Mon Jul 25 10:43:14 2011 +0200
2.3 @@ -55,7 +55,6 @@
2.4 Reflection
2.5 RBT_Mapping
2.6 Set_Algebras
2.7 - SML_Quickcheck
2.8 State_Monad
2.9 Sum_of_Squares
2.10 Transitive_Closure_Table
3.1 --- a/src/HOL/Library/SML_Quickcheck.thy Mon Jul 25 10:42:32 2011 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,47 +0,0 @@
3.4 -
3.5 -header {* Install quickcheck of SML code generator *}
3.6 -
3.7 -theory SML_Quickcheck
3.8 -imports Main
3.9 -begin
3.10 -
3.11 -ML {*
3.12 -signature SML_QUICKCHECK =
3.13 -sig
3.14 - val active : bool Config.T
3.15 - val setup : theory -> theory
3.16 -end;
3.17 -
3.18 -structure SML_Quickcheck : SML_QUICKCHECK =
3.19 -struct
3.20 -
3.21 -val active = Attrib.setup_config_bool @{binding quickcheck_SML_active} (K true);
3.22 -
3.23 -fun compile_generator_expr ctxt [(t, eval_terms)] [_, size] =
3.24 - let
3.25 - val prop = list_abs_free (Term.add_frees t [], t)
3.26 - val test_fun = Codegen.test_term ctxt prop
3.27 - val iterations = Config.get ctxt Quickcheck.iterations
3.28 - fun iterate size 0 = NONE
3.29 - | iterate size j =
3.30 - let
3.31 - val result = test_fun size handle Match =>
3.32 - (if Config.get ctxt Quickcheck.quiet then ()
3.33 - else warning "Exception Match raised during quickcheck"; NONE)
3.34 - in
3.35 - case result of NONE => iterate size (j - 1) | SOME q => SOME q
3.36 - end
3.37 - in (iterate size iterations, NONE) end
3.38 -
3.39 -val test_goals = Quickcheck.generator_test_goal_terms compile_generator_expr
3.40 -
3.41 -val setup =
3.42 - Inductive_Codegen.quickcheck_setup
3.43 - #> Context.theory_map (Quickcheck.add_tester ("SML", (active, test_goals)))
3.44 -
3.45 -end;
3.46 -*}
3.47 -
3.48 -setup {* SML_Quickcheck.setup *}
3.49 -
3.50 -end
4.1 --- a/src/HOL/ex/ROOT.ML Mon Jul 25 10:42:32 2011 +0200
4.2 +++ b/src/HOL/ex/ROOT.ML Mon Jul 25 10:43:14 2011 +0200
4.3 @@ -64,7 +64,6 @@
4.4 "HarmonicSeries",
4.5 "Refute_Examples",
4.6 "Quickcheck_Examples",
4.7 - "SML_Quickcheck_Examples",
4.8 "Quickcheck_Lattice_Examples",
4.9 "Landau",
4.10 "Execute_Choice",
5.1 --- a/src/HOL/ex/SML_Quickcheck_Examples.thy Mon Jul 25 10:42:32 2011 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,143 +0,0 @@
5.4 -(* Title: HOL/ex/SML_Quickcheck_Examples.thy
5.5 - Author: Stefan Berghofer, Lukas Bulwahn
5.6 - Copyright 2011 TU Muenchen
5.7 -*)
5.8 -
5.9 -theory SML_Quickcheck_Examples
5.10 -imports "~~/src/HOL/Library/SML_Quickcheck"
5.11 -begin
5.12 -
5.13 -text {*
5.14 -This is a regression test for the 'quickcheck' counterexample generator based on the
5.15 -SML code generator.
5.16 -
5.17 -The counterexample generator has been superseded by counterexample generators based on
5.18 -the generic code generator.
5.19 -*}
5.20 -
5.21 -declare [[quickcheck_finite_types = false]]
5.22 -declare [[quickcheck_timeout = 600.0]]
5.23 -
5.24 -subsection {* Lists *}
5.25 -
5.26 -theorem "map g (map f xs) = map (g o f) xs"
5.27 - quickcheck[SML, expect = no_counterexample]
5.28 - oops
5.29 -
5.30 -theorem "map g (map f xs) = map (f o g) xs"
5.31 - quickcheck[SML, expect = counterexample]
5.32 - oops
5.33 -
5.34 -theorem "rev (xs @ ys) = rev ys @ rev xs"
5.35 - quickcheck[SML, expect = no_counterexample]
5.36 - oops
5.37 -
5.38 -theorem "rev (xs @ ys) = rev xs @ rev ys"
5.39 - quickcheck[SML, expect = counterexample]
5.40 - oops
5.41 -
5.42 -theorem "rev (rev xs) = xs"
5.43 - quickcheck[SML, expect = no_counterexample]
5.44 - oops
5.45 -
5.46 -theorem "rev xs = xs"
5.47 - quickcheck[tester = SML, expect = counterexample]
5.48 -oops
5.49 -
5.50 -
5.51 -text {* An example involving functions inside other data structures *}
5.52 -
5.53 -primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
5.54 - "app [] x = x"
5.55 - | "app (f # fs) x = app fs (f x)"
5.56 -
5.57 -lemma "app (fs @ gs) x = app gs (app fs x)"
5.58 - quickcheck[SML, expect = no_counterexample]
5.59 - by (induct fs arbitrary: x) simp_all
5.60 -
5.61 -lemma "app (fs @ gs) x = app fs (app gs x)"
5.62 - quickcheck[SML, expect = counterexample]
5.63 - oops
5.64 -
5.65 -primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
5.66 - "occurs a [] = 0"
5.67 - | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
5.68 -
5.69 -primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
5.70 - "del1 a [] = []"
5.71 - | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
5.72 -
5.73 -text {* A lemma, you'd think to be true from our experience with delAll *}
5.74 -lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
5.75 - -- {* Wrong. Precondition needed.*}
5.76 - quickcheck[SML, expect = counterexample]
5.77 - oops
5.78 -
5.79 -lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
5.80 - quickcheck[SML, expect = counterexample]
5.81 - -- {* Also wrong.*}
5.82 - oops
5.83 -
5.84 -lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
5.85 - quickcheck[SML, expect = no_counterexample]
5.86 - by (induct xs) auto
5.87 -
5.88 -primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
5.89 - "replace a b [] = []"
5.90 - | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs))
5.91 - else (x#(replace a b xs)))"
5.92 -
5.93 -lemma "occurs a xs = occurs b (replace a b xs)"
5.94 - quickcheck[SML, expect = counterexample]
5.95 - -- {* Wrong. Precondition needed.*}
5.96 - oops
5.97 -
5.98 -lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
5.99 - quickcheck[SML, expect = no_counterexample]
5.100 - by (induct xs) simp_all
5.101 -
5.102 -
5.103 -subsection {* Trees *}
5.104 -
5.105 -datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree"
5.106 -
5.107 -primrec leaves :: "'a tree \<Rightarrow> 'a list" where
5.108 - "leaves Twig = []"
5.109 - | "leaves (Leaf a) = [a]"
5.110 - | "leaves (Branch l r) = (leaves l) @ (leaves r)"
5.111 -
5.112 -primrec plant :: "'a list \<Rightarrow> 'a tree" where
5.113 - "plant [] = Twig "
5.114 - | "plant (x#xs) = Branch (Leaf x) (plant xs)"
5.115 -
5.116 -primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
5.117 - "mirror (Twig) = Twig "
5.118 - | "mirror (Leaf a) = Leaf a "
5.119 - | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
5.120 -
5.121 -theorem "plant (rev (leaves xt)) = mirror xt"
5.122 - quickcheck[SML, expect = counterexample]
5.123 - --{* Wrong! *}
5.124 - oops
5.125 -
5.126 -theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
5.127 - quickcheck[SML, expect = counterexample]
5.128 - --{* Wrong! *}
5.129 - oops
5.130 -
5.131 -datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
5.132 -
5.133 -primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
5.134 - "inOrder (Tip a)= [a]"
5.135 - | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
5.136 -
5.137 -primrec root :: "'a ntree \<Rightarrow> 'a" where
5.138 - "root (Tip a) = a"
5.139 - | "root (Node f x y) = f"
5.140 -
5.141 -theorem "hd (inOrder xt) = root xt"
5.142 - quickcheck[SML, expect = counterexample]
5.143 - --{* Wrong! *}
5.144 - oops
5.145 -
5.146 -end