# HG changeset patch
# User bulwahn
# Date 1329894101 -3600
# Node ID f462e49eaf115a27f8ac058f0f094e8c46c51e37
# Parent  a935175fe6b61cd9105413d0ed0fd38f5bd37d85
moving Quickcheck's example to its own session

diff -r a935175fe6b6 -r f462e49eaf11 src/HOL/IsaMakefile
--- 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
 
diff -r a935175fe6b6 -r f462e49eaf11 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- /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
diff -r a935175fe6b6 -r f462e49eaf11 src/HOL/Quickcheck_Examples/Quickcheck_Lattice_Examples.thy
--- /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
diff -r a935175fe6b6 -r f462e49eaf11 src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
--- /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
diff -r a935175fe6b6 -r f462e49eaf11 src/HOL/Quickcheck_Examples/ROOT.ML
--- /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";
+
diff -r a935175fe6b6 -r f462e49eaf11 src/HOL/ex/Quickcheck_Examples.thy
--- 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
diff -r a935175fe6b6 -r f462e49eaf11 src/HOL/ex/Quickcheck_Lattice_Examples.thy
--- 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
diff -r a935175fe6b6 -r f462e49eaf11 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- 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
diff -r a935175fe6b6 -r f462e49eaf11 src/HOL/ex/ROOT.ML
--- 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";