--- a/src/HOL/IsaMakefile Tue Feb 21 23:25:36 2012 +0100
+++ b/src/HOL/IsaMakefile Wed Feb 22 08:01:41 2012 +0100
@@ -61,6 +61,7 @@
HOL-Nitpick_Examples \
HOL-Number_Theory \
HOL-Old_Number_Theory \
+ HOL-Quickcheck_Examples \
HOL-Quotient_Examples \
HOL-Predicate_Compile_Examples \
HOL-Prolog \
@@ -1061,8 +1062,7 @@
ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
ex/Normalization_by_Evaluation.thy ex/Numeral_Representation.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/Quicksort.thy ex/ROOT.ML \
+ ex/Quicksort.thy ex/ROOT.ML \
ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \
ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \
ex/Set_Algebras.thy ex/Simproc_Tests.thy ex/SVC_Oracle.thy \
@@ -1508,6 +1508,15 @@
Mutabelle/mutabelle_extra.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mutabelle
+## HOL-Quickcheck_Examples
+
+HOL-Quickcheck_Examples: HOL $(LOG)/HOL-Quickcheck_Examples.gz
+
+$(LOG)/HOL-Quickcheck_Examples.gz: $(OUT)/HOL \
+ Quickcheck_Examples/Quickcheck_Examples.thy \
+ Quickcheck_Examples/Quickcheck_Lattice_Examples.thy \
+ Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
+ @$(ISABELLE_TOOL) usedir $(OUT)/HOL Quickcheck_Examples
## HOL-Quotient_Examples
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Wed Feb 22 08:01:41 2012 +0100
@@ -0,0 +1,541 @@
+(* Title: HOL/ex/Quickcheck_Examples.thy
+ Author: Stefan Berghofer, Lukas Bulwahn
+ Copyright 2004 - 2010 TU Muenchen
+*)
+
+header {* Examples for the 'quickcheck' command *}
+
+theory Quickcheck_Examples
+imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/Multiset"
+begin
+
+text {*
+The 'quickcheck' command allows to find counterexamples by evaluating
+formulae.
+Currently, there are two different exploration schemes:
+- random testing: this is incomplete, but explores the search space faster.
+- exhaustive testing: this is complete, but increasing the depth leads to
+ exponentially many assignments.
+
+quickcheck can handle quantifiers on finite universes.
+
+*}
+
+declare [[quickcheck_timeout = 3600]]
+
+subsection {* Lists *}
+
+theorem "map g (map f xs) = map (g o f) xs"
+ quickcheck[random, expect = no_counterexample]
+ quickcheck[exhaustive, size = 3, expect = no_counterexample]
+ oops
+
+theorem "map g (map f xs) = map (f o g) xs"
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
+ oops
+
+theorem "rev (xs @ ys) = rev ys @ rev xs"
+ quickcheck[random, expect = no_counterexample]
+ quickcheck[exhaustive, expect = no_counterexample]
+ quickcheck[exhaustive, size = 1000, timeout = 0.1]
+ oops
+
+theorem "rev (xs @ ys) = rev xs @ rev ys"
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
+ oops
+
+theorem "rev (rev xs) = xs"
+ quickcheck[random, expect = no_counterexample]
+ quickcheck[exhaustive, expect = no_counterexample]
+ oops
+
+theorem "rev xs = xs"
+ quickcheck[tester = random, finite_types = true, report = false, expect = counterexample]
+ quickcheck[tester = random, finite_types = false, report = false, expect = counterexample]
+ quickcheck[tester = random, finite_types = true, report = true, expect = counterexample]
+ quickcheck[tester = random, finite_types = false, report = true, expect = counterexample]
+ quickcheck[tester = exhaustive, finite_types = true, expect = counterexample]
+ quickcheck[tester = exhaustive, finite_types = false, 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[random, expect = no_counterexample]
+ quickcheck[exhaustive, size = 4, expect = no_counterexample]
+ by (induct fs arbitrary: x) simp_all
+
+lemma "app (fs @ gs) x = app fs (app gs x)"
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, 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[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
+ oops
+
+lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
+ -- {* Also wrong.*}
+ oops
+
+lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
+ quickcheck[random, expect = no_counterexample]
+ quickcheck[exhaustive, 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[random, expect = counterexample]
+ quickcheck[exhaustive, 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[random, expect = no_counterexample]
+ quickcheck[exhaustive, 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[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
+ --{* Wrong! *}
+ oops
+
+theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, 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[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
+ --{* Wrong! *}
+ oops
+
+
+subsection {* Exhaustive Testing beats Random Testing *}
+
+text {* Here are some examples from mutants from the List theory
+where exhaustive testing beats random testing *}
+
+lemma
+ "[] ~= xs ==> hd xs = last (x # xs)"
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ assumes "!!i. [| i < n; i < length xs |] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)"
+ shows "drop n xs = takeWhile P xs"
+quickcheck[random, iterations = 10000, quiet]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
+quickcheck[random, iterations = 10000, finite_types = false]
+quickcheck[exhaustive, finite_types = false, expect = counterexample]
+oops
+
+lemma
+ "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
+quickcheck[random, iterations = 10000, finite_types = false]
+quickcheck[exhaustive, finite_types = false, expect = counterexample]
+oops
+
+lemma
+ "ns ! k < length ns ==> k <= listsum ns"
+quickcheck[random, iterations = 10000, finite_types = false, quiet]
+quickcheck[exhaustive, finite_types = false, expect = counterexample]
+oops
+
+lemma
+ "[| ys = x # xs1; zs = xs1 @ xs |] ==> ys @ zs = x # xs"
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+"i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs"
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []"
+quickcheck[random, iterations = 10000]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "(ys = zs) = (xs @ ys = splice xs zs)"
+quickcheck[random]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+subsection {* Examples with quantifiers *}
+
+text {*
+ These examples show that we can handle quantifiers.
+*}
+
+lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
+ quickcheck[random, expect = counterexample]
+ quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
+ quickcheck[random, expect = counterexample]
+ quickcheck[expect = counterexample]
+oops
+
+lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
+ quickcheck[random, expect = counterexample]
+ quickcheck[expect = counterexample]
+oops
+
+
+subsection {* Examples with sets *}
+
+lemma
+ "{} = A Un - A"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "[| bij_betw f A B; bij_betw f C D |] ==> bij_betw f (A Un C) (B Un D)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+
+subsection {* Examples with relations *}
+
+lemma
+ "acyclic (R :: ('a * 'a) set) ==> acyclic S ==> acyclic (R Un S)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "acyclic (R :: (nat * nat) set) ==> acyclic S ==> acyclic (R Un S)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+(* FIXME: some dramatic performance decrease after changing the code equation of the ntrancl *)
+lemma
+ "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
+(*quickcheck[exhaustive, expect = counterexample]*)
+oops
+
+lemma
+ "wf (R :: ('a * 'a) set) ==> wf S ==> wf (R Un S)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "wf (R :: (nat * nat) set) ==> wf S ==> wf (R Un S)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "wf (R :: (int * int) set) ==> wf S ==> wf (R Un S)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+
+subsection {* Examples with the descriptive operator *}
+
+lemma
+ "(THE x. x = a) = b"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+subsection {* Examples with Multisets *}
+
+lemma
+ "X + Y = Y + (Z :: 'a multiset)"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "X - Y = Y - (Z :: 'a multiset)"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "N + M - N = (N::'a multiset)"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+subsection {* Examples with numerical types *}
+
+text {*
+Quickcheck supports the common types nat, int, rat and real.
+*}
+
+lemma
+ "(x :: nat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
+quickcheck[exhaustive, size = 10, expect = counterexample]
+quickcheck[random, size = 10]
+oops
+
+lemma
+ "(x :: int) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
+quickcheck[exhaustive, size = 10, expect = counterexample]
+quickcheck[random, size = 10]
+oops
+
+lemma
+ "(x :: rat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
+quickcheck[exhaustive, size = 10, expect = counterexample]
+quickcheck[random, size = 10]
+oops
+
+lemma "(x :: rat) >= 0"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
+quickcheck[exhaustive, size = 10, expect = counterexample]
+quickcheck[random, size = 10]
+oops
+
+lemma "(x :: real) >= 0"
+quickcheck[random, expect = counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+subsubsection {* floor and ceiling functions *}
+
+lemma
+ "floor x + floor y = floor (x + y :: rat)"
+quickcheck[expect = counterexample]
+oops
+
+lemma
+ "floor x + floor y = floor (x + y :: real)"
+quickcheck[expect = counterexample]
+oops
+
+lemma
+ "ceiling x + ceiling y = ceiling (x + y :: rat)"
+quickcheck[expect = counterexample]
+oops
+
+lemma
+ "ceiling x + ceiling y = ceiling (x + y :: real)"
+quickcheck[expect = counterexample]
+oops
+
+subsection {* Examples with abstract types *}
+
+lemma
+ "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1"
+quickcheck[exhaustive]
+quickcheck[random]
+oops
+
+lemma
+ "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1"
+quickcheck[exhaustive]
+quickcheck[random]
+oops
+
+subsection {* Examples with Records *}
+
+record point =
+ xpos :: nat
+ ypos :: nat
+
+lemma
+ "xpos r = xpos r' ==> r = r'"
+quickcheck[exhaustive, expect = counterexample]
+quickcheck[random, expect = counterexample]
+oops
+
+datatype colour = Red | Green | Blue
+
+record cpoint = point +
+ colour :: colour
+
+lemma
+ "xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'"
+quickcheck[exhaustive, expect = counterexample]
+quickcheck[random, expect = counterexample]
+oops
+
+subsection {* Examples with locales *}
+
+locale Truth
+
+context Truth
+begin
+
+lemma "False"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+end
+
+interpretation Truth .
+
+context Truth
+begin
+
+lemma "False"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+end
+
+locale antisym =
+ fixes R
+ assumes "R x y --> R y x --> x = y"
+begin
+
+lemma
+ "R x y --> R y z --> R x z"
+quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+end
+
+subsection {* Examples with HOL quantifiers *}
+
+lemma
+ "\<forall> xs ys. xs = [] --> xs = ys"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "ys = [] --> (\<forall>xs. xs = [] --> xs = y # ys)"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+lemma
+ "\<forall>xs. (\<exists> ys. ys = []) --> xs = ys"
+quickcheck[exhaustive, expect = counterexample]
+oops
+
+subsection {* Examples with underspecified/partial functions *}
+
+lemma
+ "xs = [] ==> hd xs \<noteq> x"
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
+oops
+
+lemma
+ "xs = [] ==> hd xs = x"
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
+oops
+
+lemma "xs = [] ==> hd xs = x ==> x = y"
+quickcheck[exhaustive, expect = no_counterexample]
+quickcheck[random, report = false, expect = no_counterexample]
+quickcheck[random, report = true, expect = no_counterexample]
+oops
+
+text {* with the simple testing scheme *}
+
+setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
+declare [[quickcheck_full_support = false]]
+
+lemma
+ "xs = [] ==> hd xs \<noteq> x"
+quickcheck[exhaustive, expect = no_counterexample]
+oops
+
+lemma
+ "xs = [] ==> hd xs = x"
+quickcheck[exhaustive, expect = no_counterexample]
+oops
+
+lemma "xs = [] ==> hd xs = x ==> x = y"
+quickcheck[exhaustive, expect = no_counterexample]
+oops
+
+declare [[quickcheck_full_support = true]]
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy Wed Feb 22 08:01:41 2012 +0100
@@ -0,0 +1,141 @@
+(* Title: HOL/ex/Quickcheck_Lattice_Examples.thy
+ Author: Lukas Bulwahn
+ Copyright 2010 TU Muenchen
+*)
+
+theory Quickcheck_Lattice_Examples
+imports "~~/src/HOL/Library/Quickcheck_Types"
+begin
+
+text {* We show how other default types help to find counterexamples to propositions if
+ the standard default type @{typ int} is insufficient. *}
+
+notation
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50) and
+ top ("\<top>") and
+ bot ("\<bottom>") and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65)
+
+declare [[quickcheck_narrowing_active = false, quickcheck_timeout = 3600]]
+
+subsection {* Distributive lattices *}
+
+lemma sup_inf_distrib2:
+ "((y :: 'a :: distrib_lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
+ quickcheck[expect = no_counterexample]
+by(simp add: inf_sup_aci sup_inf_distrib1)
+
+lemma sup_inf_distrib2_1:
+ "((y :: 'a :: lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
+ quickcheck[expect = counterexample]
+ oops
+
+lemma sup_inf_distrib2_2:
+ "((y :: 'a :: distrib_lattice) \<sqinter> z') \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
+ quickcheck[expect = counterexample]
+ oops
+
+lemma inf_sup_distrib1_1:
+ "(x :: 'a :: distrib_lattice) \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x' \<sqinter> z)"
+ quickcheck[expect = counterexample]
+ oops
+
+lemma inf_sup_distrib2_1:
+ "((y :: 'a :: distrib_lattice) \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (y \<sqinter> x)"
+ quickcheck[expect = counterexample]
+ oops
+
+subsection {* Bounded lattices *}
+
+lemma inf_bot_left [simp]:
+ "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
+ quickcheck[expect = no_counterexample]
+ by (rule inf_absorb1) simp
+
+lemma inf_bot_left_1:
+ "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = x"
+ quickcheck[expect = counterexample]
+ oops
+
+lemma inf_bot_left_2:
+ "y \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
+ quickcheck[expect = counterexample]
+ oops
+
+lemma inf_bot_left_3:
+ "x \<noteq> \<bottom> ==> y \<sqinter> (x :: 'a :: bounded_lattice_bot) \<noteq> \<bottom>"
+ quickcheck[expect = counterexample]
+ oops
+
+lemma inf_bot_right [simp]:
+ "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = \<bottom>"
+ quickcheck[expect = no_counterexample]
+ by (rule inf_absorb2) simp
+
+lemma inf_bot_right_1:
+ "x \<noteq> \<bottom> ==> (x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = y"
+ quickcheck[expect = counterexample]
+ oops
+
+lemma inf_bot_right_2:
+ "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>"
+ quickcheck[expect = counterexample]
+ oops
+
+lemma inf_bot_right [simp]:
+ "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>"
+ quickcheck[expect = counterexample]
+ oops
+
+lemma sup_bot_left [simp]:
+ "\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x"
+ quickcheck[expect = no_counterexample]
+ by (rule sup_absorb2) simp
+
+lemma sup_bot_right [simp]:
+ "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x"
+ quickcheck[expect = no_counterexample]
+ by (rule sup_absorb1) simp
+
+lemma sup_eq_bot_iff [simp]:
+ "(x :: 'a :: bounded_lattice_bot) \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+ quickcheck[expect = no_counterexample]
+ by (simp add: eq_iff)
+
+lemma sup_top_left [simp]:
+ "\<top> \<squnion> (x :: 'a :: bounded_lattice_top) = \<top>"
+ quickcheck[expect = no_counterexample]
+ by (rule sup_absorb1) simp
+
+lemma sup_top_right [simp]:
+ "(x :: 'a :: bounded_lattice_top) \<squnion> \<top> = \<top>"
+ quickcheck[expect = no_counterexample]
+ by (rule sup_absorb2) simp
+
+lemma inf_top_left [simp]:
+ "\<top> \<sqinter> x = (x :: 'a :: bounded_lattice_top)"
+ quickcheck[expect = no_counterexample]
+ by (rule inf_absorb2) simp
+
+lemma inf_top_right [simp]:
+ "x \<sqinter> \<top> = (x :: 'a :: bounded_lattice_top)"
+ quickcheck[expect = no_counterexample]
+ by (rule inf_absorb1) simp
+
+lemma inf_eq_top_iff [simp]:
+ "(x :: 'a :: bounded_lattice_top) \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
+ quickcheck[expect = no_counterexample]
+ by (simp add: eq_iff)
+
+
+no_notation
+ less_eq (infix "\<sqsubseteq>" 50) and
+ less (infix "\<sqsubset>" 50) and
+ inf (infixl "\<sqinter>" 70) and
+ sup (infixl "\<squnion>" 65) and
+ top ("\<top>") and
+ bot ("\<bottom>")
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy Wed Feb 22 08:01:41 2012 +0100
@@ -0,0 +1,270 @@
+(* Title: HOL/ex/Quickcheck_Narrowing_Examples.thy
+ Author: Lukas Bulwahn
+ Copyright 2011 TU Muenchen
+*)
+
+header {* Examples for narrowing-based testing *}
+
+theory Quickcheck_Narrowing_Examples
+imports Main
+begin
+
+declare [[quickcheck_timeout = 3600]]
+
+subsection {* Minimalistic examples *}
+
+lemma
+ "x = y"
+quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
+oops
+
+lemma
+ "x = y"
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
+oops
+
+subsection {* Simple examples with existentials *}
+
+lemma
+ "\<exists> y :: nat. \<forall> x. x = y"
+quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
+oops
+(*
+lemma
+ "\<exists> y :: int. \<forall> x. x = y"
+quickcheck[tester = narrowing, size = 2]
+oops
+*)
+lemma
+ "x > 1 --> (\<exists>y :: nat. x < y & y <= 1)"
+quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
+oops
+
+lemma
+ "x > 2 --> (\<exists>y :: nat. x < y & y <= 2)"
+quickcheck[tester = narrowing, finite_types = false, size = 10]
+oops
+
+lemma
+ "\<forall> x. \<exists> y :: nat. x > 3 --> (y < x & y > 3)"
+quickcheck[tester = narrowing, finite_types = false, size = 7]
+oops
+
+text {* A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp} *}
+lemma
+ "~ distinct ws ==> EX xs ys zs y. ws = xs @ [y] @ ys @ [y]"
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
+oops
+
+text {* A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last} *}
+lemma
+ "x : set xs ==> EX ys zs. xs = ys @ x # zs & x ~: set zs & x ~: set ys"
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
+oops
+
+text {* A false conjecture derived from @{thm map_eq_Cons_conv} with a typo *}
+lemma
+ "(map f xs = y # ys) = (EX z zs. xs = z' # zs & f z = y & map f zs = ys)"
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
+oops
+
+lemma "a # xs = ys @ [a] ==> EX zs. xs = zs @ [a] & ys = a#zs"
+quickcheck[narrowing, expect = counterexample]
+quickcheck[exhaustive, random, expect = no_counterexample]
+oops
+
+subsection {* Simple list examples *}
+
+lemma "rev xs = xs"
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
+oops
+
+(* FIXME: integer has strange representation! *)
+lemma "rev xs = xs"
+quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
+oops
+(*
+lemma "rev xs = xs"
+ quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
+oops
+*)
+subsection {* Simple examples with functions *}
+
+lemma "map f xs = map g xs"
+ quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
+oops
+
+lemma "map f xs = map f ys ==> xs = ys"
+ quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
+oops
+
+lemma
+ "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
+ quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
+oops
+
+lemma "map f xs = F f xs"
+ quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
+oops
+
+lemma "map f xs = F f xs"
+ quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
+oops
+
+(* requires some work...*)
+(*
+lemma "R O S = S O R"
+ quickcheck[tester = narrowing, size = 2]
+oops
+*)
+
+subsection {* Simple examples with inductive predicates *}
+
+inductive even where
+ "even 0" |
+ "even n ==> even (Suc (Suc n))"
+
+code_pred even .
+
+lemma "even (n - 2) ==> even n"
+quickcheck[narrowing, expect = counterexample]
+oops
+
+
+subsection {* AVL Trees *}
+
+datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
+
+primrec set_of :: "'a tree \<Rightarrow> 'a set"
+where
+"set_of ET = {}" |
+"set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
+
+primrec height :: "'a tree \<Rightarrow> nat"
+where
+"height ET = 0" |
+"height (MKT x l r h) = max (height l) (height r) + 1"
+
+primrec avl :: "'a tree \<Rightarrow> bool"
+where
+"avl ET = True" |
+"avl (MKT x l r h) =
+ ((height l = height r \<or> height l = 1+height r \<or> height r = 1+height l) \<and>
+ h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
+
+primrec is_ord :: "('a::order) tree \<Rightarrow> bool"
+where
+"is_ord ET = True" |
+"is_ord (MKT n l r h) =
+ ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
+
+primrec is_in :: "('a::order) \<Rightarrow> 'a tree \<Rightarrow> bool"
+where
+ "is_in k ET = False" |
+ "is_in k (MKT n l r h) = (if k = n then True else
+ if k < n then (is_in k l)
+ else (is_in k r))"
+
+primrec ht :: "'a tree \<Rightarrow> nat"
+where
+"ht ET = 0" |
+"ht (MKT x l r h) = h"
+
+definition
+ mkt :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
+"mkt x l r = MKT x l r (max (ht l) (ht r) + 1)"
+
+(* replaced MKT lrn lrl lrr by MKT lrr lrl *)
+fun l_bal where
+"l_bal(n, MKT ln ll lr h, r) =
+ (if ht ll < ht lr
+ then case lr of ET \<Rightarrow> ET (* impossible *)
+ | MKT lrn lrr lrl lrh \<Rightarrow>
+ mkt lrn (mkt ln ll lrl) (mkt n lrr r)
+ else mkt ln ll (mkt n lr r))"
+
+fun r_bal where
+"r_bal(n, l, MKT rn rl rr h) =
+ (if ht rl > ht rr
+ then case rl of ET \<Rightarrow> ET (* impossible *)
+ | MKT rln rll rlr h \<Rightarrow> mkt rln (mkt n l rll) (mkt rn rlr rr)
+ else mkt rn (mkt n l rl) rr)"
+
+primrec insrt :: "'a::order \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
+where
+"insrt x ET = MKT x ET ET 1" |
+"insrt x (MKT n l r h) =
+ (if x=n
+ then MKT n l r h
+ else if x<n
+ then let l' = insrt x l; hl' = ht l'; hr = ht r
+ in if hl' = 2+hr then l_bal(n,l',r)
+ else MKT n l' r (1 + max hl' hr)
+ else let r' = insrt x r; hl = ht l; hr' = ht r'
+ in if hr' = 2+hl then r_bal(n,l,r')
+ else MKT n l r' (1 + max hl hr'))"
+
+
+subsubsection {* Necessary setup for code generation *}
+
+primrec set_of'
+where
+ "set_of' ET = []"
+| "set_of' (MKT n l r h) = n # (set_of' l @ set_of' r)"
+
+lemma set_of':
+ "set (set_of' t) = set_of t"
+by (induct t) auto
+
+lemma is_ord_mkt:
+ "is_ord (MKT n l r h) = ((ALL n': set (set_of' l). n' < n) & (ALL n': set (set_of' r). n < n') & is_ord l & is_ord r)"
+by (simp add: set_of')
+
+declare is_ord.simps(1)[code] is_ord_mkt[code]
+
+subsubsection {* Invalid Lemma due to typo in lbal *}
+
+lemma is_ord_l_bal:
+ "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, expect = counterexample]
+oops
+
+subsection {* Examples with hd and last *}
+
+lemma
+ "hd (xs @ ys) = hd ys"
+quickcheck[narrowing, expect = counterexample]
+oops
+
+lemma
+ "last(xs @ ys) = last xs"
+quickcheck[narrowing, expect = counterexample]
+oops
+
+subsection {* Examples with underspecified/partial functions *}
+
+lemma
+ "xs = [] ==> hd xs \<noteq> x"
+quickcheck[narrowing, expect = no_counterexample]
+oops
+
+lemma
+ "xs = [] ==> hd xs = x"
+quickcheck[narrowing, expect = no_counterexample]
+oops
+
+lemma "xs = [] ==> hd xs = x ==> x = y"
+quickcheck[narrowing, expect = no_counterexample]
+oops
+
+lemma
+ "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
+quickcheck[narrowing, expect = no_counterexample]
+oops
+
+lemma
+ "hd (map f xs) = f (hd xs)"
+quickcheck[narrowing, expect = no_counterexample]
+oops
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/ROOT.ML Wed Feb 22 08:01:41 2012 +0100
@@ -0,0 +1,8 @@
+use_thys [
+ "Quickcheck_Examples",
+ "Quickcheck_Lattice_Examples"
+];
+
+if getenv "ISABELLE_GHC" = "" then ()
+else use_thy "Quickcheck_Narrowing_Examples";
+
--- a/src/HOL/ex/Quickcheck_Examples.thy Tue Feb 21 23:25:36 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,541 +0,0 @@
-(* Title: HOL/ex/Quickcheck_Examples.thy
- Author: Stefan Berghofer, Lukas Bulwahn
- Copyright 2004 - 2010 TU Muenchen
-*)
-
-header {* Examples for the 'quickcheck' command *}
-
-theory Quickcheck_Examples
-imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/Multiset"
-begin
-
-text {*
-The 'quickcheck' command allows to find counterexamples by evaluating
-formulae.
-Currently, there are two different exploration schemes:
-- random testing: this is incomplete, but explores the search space faster.
-- exhaustive testing: this is complete, but increasing the depth leads to
- exponentially many assignments.
-
-quickcheck can handle quantifiers on finite universes.
-
-*}
-
-declare [[quickcheck_timeout = 3600]]
-
-subsection {* Lists *}
-
-theorem "map g (map f xs) = map (g o f) xs"
- quickcheck[random, expect = no_counterexample]
- quickcheck[exhaustive, size = 3, expect = no_counterexample]
- oops
-
-theorem "map g (map f xs) = map (f o g) xs"
- quickcheck[random, expect = counterexample]
- quickcheck[exhaustive, expect = counterexample]
- oops
-
-theorem "rev (xs @ ys) = rev ys @ rev xs"
- quickcheck[random, expect = no_counterexample]
- quickcheck[exhaustive, expect = no_counterexample]
- quickcheck[exhaustive, size = 1000, timeout = 0.1]
- oops
-
-theorem "rev (xs @ ys) = rev xs @ rev ys"
- quickcheck[random, expect = counterexample]
- quickcheck[exhaustive, expect = counterexample]
- oops
-
-theorem "rev (rev xs) = xs"
- quickcheck[random, expect = no_counterexample]
- quickcheck[exhaustive, expect = no_counterexample]
- oops
-
-theorem "rev xs = xs"
- quickcheck[tester = random, finite_types = true, report = false, expect = counterexample]
- quickcheck[tester = random, finite_types = false, report = false, expect = counterexample]
- quickcheck[tester = random, finite_types = true, report = true, expect = counterexample]
- quickcheck[tester = random, finite_types = false, report = true, expect = counterexample]
- quickcheck[tester = exhaustive, finite_types = true, expect = counterexample]
- quickcheck[tester = exhaustive, finite_types = false, 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[random, expect = no_counterexample]
- quickcheck[exhaustive, size = 4, expect = no_counterexample]
- by (induct fs arbitrary: x) simp_all
-
-lemma "app (fs @ gs) x = app fs (app gs x)"
- quickcheck[random, expect = counterexample]
- quickcheck[exhaustive, 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[random, expect = counterexample]
- quickcheck[exhaustive, expect = counterexample]
- oops
-
-lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
- quickcheck[random, expect = counterexample]
- quickcheck[exhaustive, expect = counterexample]
- -- {* Also wrong.*}
- oops
-
-lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
- quickcheck[random, expect = no_counterexample]
- quickcheck[exhaustive, 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[random, expect = counterexample]
- quickcheck[exhaustive, 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[random, expect = no_counterexample]
- quickcheck[exhaustive, 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[random, expect = counterexample]
- quickcheck[exhaustive, expect = counterexample]
- --{* Wrong! *}
- oops
-
-theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
- quickcheck[random, expect = counterexample]
- quickcheck[exhaustive, 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[random, expect = counterexample]
- quickcheck[exhaustive, expect = counterexample]
- --{* Wrong! *}
- oops
-
-
-subsection {* Exhaustive Testing beats Random Testing *}
-
-text {* Here are some examples from mutants from the List theory
-where exhaustive testing beats random testing *}
-
-lemma
- "[] ~= xs ==> hd xs = last (x # xs)"
-quickcheck[random]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- assumes "!!i. [| i < n; i < length xs |] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)"
- shows "drop n xs = takeWhile P xs"
-quickcheck[random, iterations = 10000, quiet]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
-quickcheck[random, iterations = 10000]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
-quickcheck[random, iterations = 10000, finite_types = false]
-quickcheck[exhaustive, finite_types = false, expect = counterexample]
-oops
-
-lemma
- "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
-quickcheck[random, iterations = 10000, finite_types = false]
-quickcheck[exhaustive, finite_types = false, expect = counterexample]
-oops
-
-lemma
- "ns ! k < length ns ==> k <= listsum ns"
-quickcheck[random, iterations = 10000, finite_types = false, quiet]
-quickcheck[exhaustive, finite_types = false, expect = counterexample]
-oops
-
-lemma
- "[| ys = x # xs1; zs = xs1 @ xs |] ==> ys @ zs = x # xs"
-quickcheck[random, iterations = 10000]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
-"i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs"
-quickcheck[random, iterations = 10000]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []"
-quickcheck[random, iterations = 10000]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
-quickcheck[random]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. length ys \<in> {..<i}]"
-quickcheck[random]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "(ys = zs) = (xs @ ys = splice xs zs)"
-quickcheck[random]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-subsection {* Examples with quantifiers *}
-
-text {*
- These examples show that we can handle quantifiers.
-*}
-
-lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
- quickcheck[random, expect = counterexample]
- quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
- quickcheck[random, expect = counterexample]
- quickcheck[expect = counterexample]
-oops
-
-lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
- quickcheck[random, expect = counterexample]
- quickcheck[expect = counterexample]
-oops
-
-
-subsection {* Examples with sets *}
-
-lemma
- "{} = A Un - A"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "[| bij_betw f A B; bij_betw f C D |] ==> bij_betw f (A Un C) (B Un D)"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-
-subsection {* Examples with relations *}
-
-lemma
- "acyclic (R :: ('a * 'a) set) ==> acyclic S ==> acyclic (R Un S)"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "acyclic (R :: (nat * nat) set) ==> acyclic S ==> acyclic (R Un S)"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-(* FIXME: some dramatic performance decrease after changing the code equation of the ntrancl *)
-lemma
- "(x, z) : rtrancl (R Un S) ==> \<exists> y. (x, y) : rtrancl R & (y, z) : rtrancl S"
-(*quickcheck[exhaustive, expect = counterexample]*)
-oops
-
-lemma
- "wf (R :: ('a * 'a) set) ==> wf S ==> wf (R Un S)"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "wf (R :: (nat * nat) set) ==> wf S ==> wf (R Un S)"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "wf (R :: (int * int) set) ==> wf S ==> wf (R Un S)"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-
-subsection {* Examples with the descriptive operator *}
-
-lemma
- "(THE x. x = a) = b"
-quickcheck[random, expect = counterexample]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-subsection {* Examples with Multisets *}
-
-lemma
- "X + Y = Y + (Z :: 'a multiset)"
-quickcheck[random, expect = counterexample]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "X - Y = Y - (Z :: 'a multiset)"
-quickcheck[random, expect = counterexample]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "N + M - N = (N::'a multiset)"
-quickcheck[random, expect = counterexample]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-subsection {* Examples with numerical types *}
-
-text {*
-Quickcheck supports the common types nat, int, rat and real.
-*}
-
-lemma
- "(x :: nat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
-quickcheck[exhaustive, size = 10, expect = counterexample]
-quickcheck[random, size = 10]
-oops
-
-lemma
- "(x :: int) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
-quickcheck[exhaustive, size = 10, expect = counterexample]
-quickcheck[random, size = 10]
-oops
-
-lemma
- "(x :: rat) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
-quickcheck[exhaustive, size = 10, expect = counterexample]
-quickcheck[random, size = 10]
-oops
-
-lemma "(x :: rat) >= 0"
-quickcheck[random, expect = counterexample]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "(x :: real) > 0 ==> y > 0 ==> z > 0 ==> x * x + y * y \<noteq> z * z"
-quickcheck[exhaustive, size = 10, expect = counterexample]
-quickcheck[random, size = 10]
-oops
-
-lemma "(x :: real) >= 0"
-quickcheck[random, expect = counterexample]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-subsubsection {* floor and ceiling functions *}
-
-lemma
- "floor x + floor y = floor (x + y :: rat)"
-quickcheck[expect = counterexample]
-oops
-
-lemma
- "floor x + floor y = floor (x + y :: real)"
-quickcheck[expect = counterexample]
-oops
-
-lemma
- "ceiling x + ceiling y = ceiling (x + y :: rat)"
-quickcheck[expect = counterexample]
-oops
-
-lemma
- "ceiling x + ceiling y = ceiling (x + y :: real)"
-quickcheck[expect = counterexample]
-oops
-
-subsection {* Examples with abstract types *}
-
-lemma
- "Dlist.length (Dlist.remove x xs) = Dlist.length xs - 1"
-quickcheck[exhaustive]
-quickcheck[random]
-oops
-
-lemma
- "Dlist.length (Dlist.insert x xs) = Dlist.length xs + 1"
-quickcheck[exhaustive]
-quickcheck[random]
-oops
-
-subsection {* Examples with Records *}
-
-record point =
- xpos :: nat
- ypos :: nat
-
-lemma
- "xpos r = xpos r' ==> r = r'"
-quickcheck[exhaustive, expect = counterexample]
-quickcheck[random, expect = counterexample]
-oops
-
-datatype colour = Red | Green | Blue
-
-record cpoint = point +
- colour :: colour
-
-lemma
- "xpos r = xpos r' ==> ypos r = ypos r' ==> (r :: cpoint) = r'"
-quickcheck[exhaustive, expect = counterexample]
-quickcheck[random, expect = counterexample]
-oops
-
-subsection {* Examples with locales *}
-
-locale Truth
-
-context Truth
-begin
-
-lemma "False"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-end
-
-interpretation Truth .
-
-context Truth
-begin
-
-lemma "False"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-end
-
-locale antisym =
- fixes R
- assumes "R x y --> R y x --> x = y"
-begin
-
-lemma
- "R x y --> R y z --> R x z"
-quickcheck[exhaustive, finite_type_size = 2, expect = no_counterexample]
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-end
-
-subsection {* Examples with HOL quantifiers *}
-
-lemma
- "\<forall> xs ys. xs = [] --> xs = ys"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "ys = [] --> (\<forall>xs. xs = [] --> xs = y # ys)"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-lemma
- "\<forall>xs. (\<exists> ys. ys = []) --> xs = ys"
-quickcheck[exhaustive, expect = counterexample]
-oops
-
-subsection {* Examples with underspecified/partial functions *}
-
-lemma
- "xs = [] ==> hd xs \<noteq> x"
-quickcheck[exhaustive, expect = no_counterexample]
-quickcheck[random, report = false, expect = no_counterexample]
-quickcheck[random, report = true, expect = no_counterexample]
-oops
-
-lemma
- "xs = [] ==> hd xs = x"
-quickcheck[exhaustive, expect = no_counterexample]
-quickcheck[random, report = false, expect = no_counterexample]
-quickcheck[random, report = true, expect = no_counterexample]
-oops
-
-lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[exhaustive, expect = no_counterexample]
-quickcheck[random, report = false, expect = no_counterexample]
-quickcheck[random, report = true, expect = no_counterexample]
-oops
-
-text {* with the simple testing scheme *}
-
-setup {* Exhaustive_Generators.setup_exhaustive_datatype_interpretation *}
-declare [[quickcheck_full_support = false]]
-
-lemma
- "xs = [] ==> hd xs \<noteq> x"
-quickcheck[exhaustive, expect = no_counterexample]
-oops
-
-lemma
- "xs = [] ==> hd xs = x"
-quickcheck[exhaustive, expect = no_counterexample]
-oops
-
-lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[exhaustive, expect = no_counterexample]
-oops
-
-declare [[quickcheck_full_support = true]]
-
-end
--- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy Tue Feb 21 23:25:36 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(* Title: HOL/ex/Quickcheck_Lattice_Examples.thy
- Author: Lukas Bulwahn
- Copyright 2010 TU Muenchen
-*)
-
-theory Quickcheck_Lattice_Examples
-imports "~~/src/HOL/Library/Quickcheck_Types"
-begin
-
-text {* We show how other default types help to find counterexamples to propositions if
- the standard default type @{typ int} is insufficient. *}
-
-notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- top ("\<top>") and
- bot ("\<bottom>") and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65)
-
-declare [[quickcheck_narrowing_active = false, quickcheck_timeout = 3600]]
-
-subsection {* Distributive lattices *}
-
-lemma sup_inf_distrib2:
- "((y :: 'a :: distrib_lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
- quickcheck[expect = no_counterexample]
-by(simp add: inf_sup_aci sup_inf_distrib1)
-
-lemma sup_inf_distrib2_1:
- "((y :: 'a :: lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
- quickcheck[expect = counterexample]
- oops
-
-lemma sup_inf_distrib2_2:
- "((y :: 'a :: distrib_lattice) \<sqinter> z') \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
- quickcheck[expect = counterexample]
- oops
-
-lemma inf_sup_distrib1_1:
- "(x :: 'a :: distrib_lattice) \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x' \<sqinter> z)"
- quickcheck[expect = counterexample]
- oops
-
-lemma inf_sup_distrib2_1:
- "((y :: 'a :: distrib_lattice) \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (y \<sqinter> x)"
- quickcheck[expect = counterexample]
- oops
-
-subsection {* Bounded lattices *}
-
-lemma inf_bot_left [simp]:
- "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
- quickcheck[expect = no_counterexample]
- by (rule inf_absorb1) simp
-
-lemma inf_bot_left_1:
- "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = x"
- quickcheck[expect = counterexample]
- oops
-
-lemma inf_bot_left_2:
- "y \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
- quickcheck[expect = counterexample]
- oops
-
-lemma inf_bot_left_3:
- "x \<noteq> \<bottom> ==> y \<sqinter> (x :: 'a :: bounded_lattice_bot) \<noteq> \<bottom>"
- quickcheck[expect = counterexample]
- oops
-
-lemma inf_bot_right [simp]:
- "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = \<bottom>"
- quickcheck[expect = no_counterexample]
- by (rule inf_absorb2) simp
-
-lemma inf_bot_right_1:
- "x \<noteq> \<bottom> ==> (x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = y"
- quickcheck[expect = counterexample]
- oops
-
-lemma inf_bot_right_2:
- "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>"
- quickcheck[expect = counterexample]
- oops
-
-lemma inf_bot_right [simp]:
- "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>"
- quickcheck[expect = counterexample]
- oops
-
-lemma sup_bot_left [simp]:
- "\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x"
- quickcheck[expect = no_counterexample]
- by (rule sup_absorb2) simp
-
-lemma sup_bot_right [simp]:
- "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x"
- quickcheck[expect = no_counterexample]
- by (rule sup_absorb1) simp
-
-lemma sup_eq_bot_iff [simp]:
- "(x :: 'a :: bounded_lattice_bot) \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
- quickcheck[expect = no_counterexample]
- by (simp add: eq_iff)
-
-lemma sup_top_left [simp]:
- "\<top> \<squnion> (x :: 'a :: bounded_lattice_top) = \<top>"
- quickcheck[expect = no_counterexample]
- by (rule sup_absorb1) simp
-
-lemma sup_top_right [simp]:
- "(x :: 'a :: bounded_lattice_top) \<squnion> \<top> = \<top>"
- quickcheck[expect = no_counterexample]
- by (rule sup_absorb2) simp
-
-lemma inf_top_left [simp]:
- "\<top> \<sqinter> x = (x :: 'a :: bounded_lattice_top)"
- quickcheck[expect = no_counterexample]
- by (rule inf_absorb2) simp
-
-lemma inf_top_right [simp]:
- "x \<sqinter> \<top> = (x :: 'a :: bounded_lattice_top)"
- quickcheck[expect = no_counterexample]
- by (rule inf_absorb1) simp
-
-lemma inf_eq_top_iff [simp]:
- "(x :: 'a :: bounded_lattice_top) \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
- quickcheck[expect = no_counterexample]
- by (simp add: eq_iff)
-
-
-no_notation
- less_eq (infix "\<sqsubseteq>" 50) and
- less (infix "\<sqsubset>" 50) and
- inf (infixl "\<sqinter>" 70) and
- sup (infixl "\<squnion>" 65) and
- top ("\<top>") and
- bot ("\<bottom>")
-
-end
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy Tue Feb 21 23:25:36 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,270 +0,0 @@
-(* Title: HOL/ex/Quickcheck_Narrowing_Examples.thy
- Author: Lukas Bulwahn
- Copyright 2011 TU Muenchen
-*)
-
-header {* Examples for narrowing-based testing *}
-
-theory Quickcheck_Narrowing_Examples
-imports Main
-begin
-
-declare [[quickcheck_timeout = 3600]]
-
-subsection {* Minimalistic examples *}
-
-lemma
- "x = y"
-quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
-oops
-
-lemma
- "x = y"
-quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
-oops
-
-subsection {* Simple examples with existentials *}
-
-lemma
- "\<exists> y :: nat. \<forall> x. x = y"
-quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
-oops
-(*
-lemma
- "\<exists> y :: int. \<forall> x. x = y"
-quickcheck[tester = narrowing, size = 2]
-oops
-*)
-lemma
- "x > 1 --> (\<exists>y :: nat. x < y & y <= 1)"
-quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
-oops
-
-lemma
- "x > 2 --> (\<exists>y :: nat. x < y & y <= 2)"
-quickcheck[tester = narrowing, finite_types = false, size = 10]
-oops
-
-lemma
- "\<forall> x. \<exists> y :: nat. x > 3 --> (y < x & y > 3)"
-quickcheck[tester = narrowing, finite_types = false, size = 7]
-oops
-
-text {* A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp} *}
-lemma
- "~ distinct ws ==> EX xs ys zs y. ws = xs @ [y] @ ys @ [y]"
-quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
-oops
-
-text {* A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last} *}
-lemma
- "x : set xs ==> EX ys zs. xs = ys @ x # zs & x ~: set zs & x ~: set ys"
-quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
-oops
-
-text {* A false conjecture derived from @{thm map_eq_Cons_conv} with a typo *}
-lemma
- "(map f xs = y # ys) = (EX z zs. xs = z' # zs & f z = y & map f zs = ys)"
-quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
-oops
-
-lemma "a # xs = ys @ [a] ==> EX zs. xs = zs @ [a] & ys = a#zs"
-quickcheck[narrowing, expect = counterexample]
-quickcheck[exhaustive, random, expect = no_counterexample]
-oops
-
-subsection {* Simple list examples *}
-
-lemma "rev xs = xs"
-quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
-oops
-
-(* FIXME: integer has strange representation! *)
-lemma "rev xs = xs"
-quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
-oops
-(*
-lemma "rev xs = xs"
- quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
-oops
-*)
-subsection {* Simple examples with functions *}
-
-lemma "map f xs = map g xs"
- quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
-oops
-
-lemma "map f xs = map f ys ==> xs = ys"
- quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
-oops
-
-lemma
- "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
- quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
-oops
-
-lemma "map f xs = F f xs"
- quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
-oops
-
-lemma "map f xs = F f xs"
- quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
-oops
-
-(* requires some work...*)
-(*
-lemma "R O S = S O R"
- quickcheck[tester = narrowing, size = 2]
-oops
-*)
-
-subsection {* Simple examples with inductive predicates *}
-
-inductive even where
- "even 0" |
- "even n ==> even (Suc (Suc n))"
-
-code_pred even .
-
-lemma "even (n - 2) ==> even n"
-quickcheck[narrowing, expect = counterexample]
-oops
-
-
-subsection {* AVL Trees *}
-
-datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat
-
-primrec set_of :: "'a tree \<Rightarrow> 'a set"
-where
-"set_of ET = {}" |
-"set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
-
-primrec height :: "'a tree \<Rightarrow> nat"
-where
-"height ET = 0" |
-"height (MKT x l r h) = max (height l) (height r) + 1"
-
-primrec avl :: "'a tree \<Rightarrow> bool"
-where
-"avl ET = True" |
-"avl (MKT x l r h) =
- ((height l = height r \<or> height l = 1+height r \<or> height r = 1+height l) \<and>
- h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
-
-primrec is_ord :: "('a::order) tree \<Rightarrow> bool"
-where
-"is_ord ET = True" |
-"is_ord (MKT n l r h) =
- ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
-
-primrec is_in :: "('a::order) \<Rightarrow> 'a tree \<Rightarrow> bool"
-where
- "is_in k ET = False" |
- "is_in k (MKT n l r h) = (if k = n then True else
- if k < n then (is_in k l)
- else (is_in k r))"
-
-primrec ht :: "'a tree \<Rightarrow> nat"
-where
-"ht ET = 0" |
-"ht (MKT x l r h) = h"
-
-definition
- mkt :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
-"mkt x l r = MKT x l r (max (ht l) (ht r) + 1)"
-
-(* replaced MKT lrn lrl lrr by MKT lrr lrl *)
-fun l_bal where
-"l_bal(n, MKT ln ll lr h, r) =
- (if ht ll < ht lr
- then case lr of ET \<Rightarrow> ET (* impossible *)
- | MKT lrn lrr lrl lrh \<Rightarrow>
- mkt lrn (mkt ln ll lrl) (mkt n lrr r)
- else mkt ln ll (mkt n lr r))"
-
-fun r_bal where
-"r_bal(n, l, MKT rn rl rr h) =
- (if ht rl > ht rr
- then case rl of ET \<Rightarrow> ET (* impossible *)
- | MKT rln rll rlr h \<Rightarrow> mkt rln (mkt n l rll) (mkt rn rlr rr)
- else mkt rn (mkt n l rl) rr)"
-
-primrec insrt :: "'a::order \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
-where
-"insrt x ET = MKT x ET ET 1" |
-"insrt x (MKT n l r h) =
- (if x=n
- then MKT n l r h
- else if x<n
- then let l' = insrt x l; hl' = ht l'; hr = ht r
- in if hl' = 2+hr then l_bal(n,l',r)
- else MKT n l' r (1 + max hl' hr)
- else let r' = insrt x r; hl = ht l; hr' = ht r'
- in if hr' = 2+hl then r_bal(n,l,r')
- else MKT n l r' (1 + max hl hr'))"
-
-
-subsubsection {* Necessary setup for code generation *}
-
-primrec set_of'
-where
- "set_of' ET = []"
-| "set_of' (MKT n l r h) = n # (set_of' l @ set_of' r)"
-
-lemma set_of':
- "set (set_of' t) = set_of t"
-by (induct t) auto
-
-lemma is_ord_mkt:
- "is_ord (MKT n l r h) = ((ALL n': set (set_of' l). n' < n) & (ALL n': set (set_of' r). n < n') & is_ord l & is_ord r)"
-by (simp add: set_of')
-
-declare is_ord.simps(1)[code] is_ord_mkt[code]
-
-subsubsection {* Invalid Lemma due to typo in lbal *}
-
-lemma is_ord_l_bal:
- "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
-quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, expect = counterexample]
-oops
-
-subsection {* Examples with hd and last *}
-
-lemma
- "hd (xs @ ys) = hd ys"
-quickcheck[narrowing, expect = counterexample]
-oops
-
-lemma
- "last(xs @ ys) = last xs"
-quickcheck[narrowing, expect = counterexample]
-oops
-
-subsection {* Examples with underspecified/partial functions *}
-
-lemma
- "xs = [] ==> hd xs \<noteq> x"
-quickcheck[narrowing, expect = no_counterexample]
-oops
-
-lemma
- "xs = [] ==> hd xs = x"
-quickcheck[narrowing, expect = no_counterexample]
-oops
-
-lemma "xs = [] ==> hd xs = x ==> x = y"
-quickcheck[narrowing, expect = no_counterexample]
-oops
-
-lemma
- "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
-quickcheck[narrowing, expect = no_counterexample]
-oops
-
-lemma
- "hd (map f xs) = f (hd xs)"
-quickcheck[narrowing, expect = no_counterexample]
-oops
-
-end
--- a/src/HOL/ex/ROOT.ML Tue Feb 21 23:25:36 2012 +0100
+++ b/src/HOL/ex/ROOT.ML Wed Feb 22 08:01:41 2012 +0100
@@ -60,8 +60,6 @@
"Arithmetic_Series_Complex",
"HarmonicSeries",
"Refute_Examples",
- "Quickcheck_Examples",
- "Quickcheck_Lattice_Examples",
"Landau",
"Execute_Choice",
"Summation",
@@ -76,9 +74,6 @@
"Executable_Relation"
];
-if getenv "ISABELLE_GHC" = "" then ()
-else use_thy "Quickcheck_Narrowing_Examples";
-
use_thy "SVC_Oracle";
if getenv "SVC_HOME" = "" then ()
else use_thy "svc_test";