Added theory with examples for quickcheck command.
authorberghofe
Fri Apr 16 18:09:24 2004 +0200 (2004-04-16)
changeset 14592dd1a2905ea73
parent 14591 7be4d5dadf15
child 14593 90c88e7ef62d
Added theory with examples for quickcheck command.
src/HOL/IsaMakefile
src/HOL/ex/Quickcheck_Examples.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Fri Apr 16 15:46:50 2004 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Apr 16 18:09:24 2004 +0200
     1.3 @@ -591,7 +591,7 @@
     1.4    ex/Lagrange.ML ex/Lagrange.thy ex/Locales.thy ex/MergeSort.thy \
     1.5    ex/MT.ML ex/MT.thy ex/MonoidGroup.thy ex/Multiquote.thy \
     1.6    ex/NatSum.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy ex/Puzzle.thy \
     1.7 -  ex/Qsort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
     1.8 +  ex/Qsort.thy ex/Quickcheck_Examples.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
     1.9    ex/Refute_Examples.thy \
    1.10    ex/Ring.ML ex/Ring.thy ex/StringEx.thy ex/SVC_Oracle.ML ex/SVC_Oracle.thy \
    1.11    ex/Tarski.thy ex/Tuple.thy ex/Classical.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Fri Apr 16 18:09:24 2004 +0200
     2.3 @@ -0,0 +1,148 @@
     2.4 +(*  Title:      HOL/ex/Quickcheck_Examples.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Stefan Berghofer
     2.7 +    Copyright   2004 TU Muenchen
     2.8 +*)
     2.9 +
    2.10 +header {* Examples for the 'quickcheck' command *}
    2.11 +
    2.12 +theory Quickcheck_Examples = Main:
    2.13 +
    2.14 +text {*
    2.15 +The 'quickcheck' command allows to find counterexamples by evaluating
    2.16 +formulae under an assignment of free variables to random values.
    2.17 +In contrast to 'refute', it can deal with inductive datatypes,
    2.18 +but cannot handle quantifiers.
    2.19 +*}
    2.20 +
    2.21 +subsection {* Lists *}
    2.22 +
    2.23 +theorem "map g (map f xs) = map (g o f) xs"
    2.24 +  quickcheck
    2.25 +  oops
    2.26 +
    2.27 +theorem "map g (map f xs) = map (f o g) xs"
    2.28 +  quickcheck
    2.29 +  oops
    2.30 +
    2.31 +theorem "rev (xs @ ys) = rev ys @ rev xs"
    2.32 +  quickcheck
    2.33 +  oops
    2.34 +
    2.35 +theorem "rev (xs @ ys) = rev xs @ rev ys"
    2.36 +  quickcheck
    2.37 +  oops
    2.38 +
    2.39 +theorem "rev (rev xs) = xs"
    2.40 +  quickcheck
    2.41 +  oops
    2.42 +
    2.43 +theorem "rev xs = xs"
    2.44 +  quickcheck
    2.45 +  oops
    2.46 +
    2.47 +consts
    2.48 +  occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
    2.49 +primrec
    2.50 +  "occurs a [] = 0"
    2.51 +  "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
    2.52 +
    2.53 +consts
    2.54 +  del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    2.55 +primrec
    2.56 +  "del1 a [] = []"
    2.57 +  "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
    2.58 +
    2.59 +(* A lemma, you'd think to be true from our experience with delAll*)
    2.60 +lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
    2.61 +  -- {* Wrong. Precondition needed.*}
    2.62 +  quickcheck
    2.63 +  oops
    2.64 +
    2.65 +lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
    2.66 +  quickcheck
    2.67 +    -- {* Also wrong.*}
    2.68 +  oops
    2.69 +
    2.70 +lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
    2.71 +  quickcheck
    2.72 +  apply (induct_tac xs)  
    2.73 +  apply auto
    2.74 +    -- {* Correct! *}
    2.75 +  done
    2.76 +
    2.77 +consts
    2.78 +  replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    2.79 +primrec
    2.80 +  "replace a b [] = []"
    2.81 +  "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
    2.82 +                            else (x#(replace a b xs)))"
    2.83 +
    2.84 +lemma "occurs a xs = occurs b (replace a b xs)"
    2.85 +  quickcheck
    2.86 +  -- {* Wrong. Precondition needed.*}
    2.87 +  oops
    2.88 +
    2.89 +lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
    2.90 +  quickcheck
    2.91 +  apply (induct_tac xs)  
    2.92 +  apply auto
    2.93 +  done
    2.94 +
    2.95 +
    2.96 +subsection {* Trees *}
    2.97 +
    2.98 +datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
    2.99 +
   2.100 +consts
   2.101 +  leaves :: "'a tree \<Rightarrow> 'a list"
   2.102 +primrec
   2.103 +  "leaves Twig = []"
   2.104 +  "leaves (Leaf a) = [a]"
   2.105 +  "leaves (Branch l r) = (leaves l) @ (leaves r)"
   2.106 +
   2.107 +consts
   2.108 +  plant :: "'a list \<Rightarrow> 'a tree"
   2.109 +primrec
   2.110 +  "plant [] = Twig "
   2.111 +  "plant (x#xs) = Branch (Leaf x) (plant xs)"
   2.112 +
   2.113 +consts
   2.114 +  mirror :: "'a tree \<Rightarrow> 'a tree"
   2.115 +primrec
   2.116 +  "mirror (Twig) = Twig "
   2.117 +  "mirror (Leaf a) = Leaf a "
   2.118 +  "mirror (Branch l r) = Branch (mirror r) (mirror l)"
   2.119 +
   2.120 +theorem "plant (rev (leaves xt)) = mirror xt"
   2.121 +  quickcheck
   2.122 +    --{* Wrong! *} 
   2.123 +  oops
   2.124 +
   2.125 +theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
   2.126 +  quickcheck
   2.127 +    --{* Wrong! *} 
   2.128 +  oops
   2.129 +
   2.130 +datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
   2.131 +
   2.132 +consts
   2.133 +  inOrder :: "'a ntree \<Rightarrow> 'a list"
   2.134 +primrec
   2.135 +  "inOrder (Tip a)= [a]"
   2.136 +  "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
   2.137 +
   2.138 +consts
   2.139 +  root :: "'a ntree \<Rightarrow> 'a"
   2.140 +primrec
   2.141 +  "root (Tip a) = a"
   2.142 +  "root (Node f x y) = f"
   2.143 +
   2.144 +theorem "hd(inOrder xt) = root xt"
   2.145 +  quickcheck
   2.146 +    --{* Wrong! *} 
   2.147 +  oops
   2.148 +
   2.149 +end
   2.150 +
   2.151 +
     3.1 --- a/src/HOL/ex/ROOT.ML	Fri Apr 16 15:46:50 2004 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Fri Apr 16 18:09:24 2004 +0200
     3.3 @@ -45,6 +45,7 @@
     3.4  if_svc_enabled time_use_thy "svc_test";
     3.5  
     3.6  time_use_thy "Refute_Examples";
     3.7 +time_use_thy "Quickcheck_Examples";
     3.8  
     3.9  no_document use_thy "Word";
    3.10  time_use_thy "Adder";