# HG changeset patch
# User berghofe
# Date 1082131764 -7200
# Node ID dd1a2905ea73f3b9154a99555d1d9857e38be92b
# Parent  7be4d5dadf152f12a477163d7d95a78f5107cea3
Added theory with examples for quickcheck command.

diff -r 7be4d5dadf15 -r dd1a2905ea73 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 16 15:46:50 2004 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 16 18:09:24 2004 +0200
@@ -591,7 +591,7 @@
   ex/Lagrange.ML ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy \
   ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
   ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy \
-  ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
+  ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
   ex/Refute_Examples.thy \
   ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
   ex/Tarski.thy ex/Tuple.thy ex/Classical.thy \
diff -r 7be4d5dadf15 -r dd1a2905ea73 src/HOL/ex/Quickcheck_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Fri Apr 16 18:09:24 2004 +0200
@@ -0,0 +1,148 @@
+(*  Title:      HOL/ex/Quickcheck_Examples.thy
+    ID:         $Id$
+    Author:     Stefan Berghofer
+    Copyright   2004 TU Muenchen
+*)
+
+header {* Examples for the 'quickcheck' command *}
+
+theory Quickcheck_Examples = Main:
+
+text {*
+The 'quickcheck' command allows to find counterexamples by evaluating
+formulae under an assignment of free variables to random values.
+In contrast to 'refute', it can deal with inductive datatypes,
+but cannot handle quantifiers.
+*}
+
+subsection {* Lists *}
+
+theorem "map g (map f xs) = map (g o f) xs"
+  quickcheck
+  oops
+
+theorem "map g (map f xs) = map (f o g) xs"
+  quickcheck
+  oops
+
+theorem "rev (xs @ ys) = rev ys @ rev xs"
+  quickcheck
+  oops
+
+theorem "rev (xs @ ys) = rev xs @ rev ys"
+  quickcheck
+  oops
+
+theorem "rev (rev xs) = xs"
+  quickcheck
+  oops
+
+theorem "rev xs = xs"
+  quickcheck
+  oops
+
+consts
+  occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
+primrec
+  "occurs a [] = 0"
+  "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
+
+consts
+  del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+primrec
+  "del1 a [] = []"
+  "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
+
+(* 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
+  oops
+
+lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
+  quickcheck
+    -- {* Also wrong.*}
+  oops
+
+lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
+  quickcheck
+  apply (induct_tac xs)  
+  apply auto
+    -- {* Correct! *}
+  done
+
+consts
+  replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+primrec
+  "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
+  -- {* Wrong. Precondition needed.*}
+  oops
+
+lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
+  quickcheck
+  apply (induct_tac xs)  
+  apply auto
+  done
+
+
+subsection {* Trees *}
+
+datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
+
+consts
+  leaves :: "'a tree \<Rightarrow> 'a list"
+primrec
+  "leaves Twig = []"
+  "leaves (Leaf a) = [a]"
+  "leaves (Branch l r) = (leaves l) @ (leaves r)"
+
+consts
+  plant :: "'a list \<Rightarrow> 'a tree"
+primrec
+  "plant [] = Twig "
+  "plant (x#xs) = Branch (Leaf x) (plant xs)"
+
+consts
+  mirror :: "'a tree \<Rightarrow> 'a tree"
+primrec
+  "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
+    --{* Wrong! *} 
+  oops
+
+theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
+  quickcheck
+    --{* Wrong! *} 
+  oops
+
+datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
+
+consts
+  inOrder :: "'a ntree \<Rightarrow> 'a list"
+primrec
+  "inOrder (Tip a)= [a]"
+  "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
+
+consts
+  root :: "'a ntree \<Rightarrow> 'a"
+primrec
+  "root (Tip a) = a"
+  "root (Node f x y) = f"
+
+theorem "hd(inOrder xt) = root xt"
+  quickcheck
+    --{* Wrong! *} 
+  oops
+
+end
+
+
diff -r 7be4d5dadf15 -r dd1a2905ea73 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Apr 16 15:46:50 2004 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Apr 16 18:09:24 2004 +0200
@@ -45,6 +45,7 @@
 if_svc_enabled time_use_thy "svc_test";
 
 time_use_thy "Refute_Examples";
+time_use_thy "Quickcheck_Examples";
 
 no_document use_thy "Word";
 time_use_thy "Adder";