src/HOL/ex/Quickcheck_Examples.thy
author wenzelm
Wed Sep 14 22:08:08 2005 +0200 (2005-09-14)
changeset 17388 495c799df31d
parent 16417 9bc16273c2d4
child 25891 1bd12187a96e
permissions -rw-r--r--
tuned headers etc.;
berghofe@14592
     1
(*  Title:      HOL/ex/Quickcheck_Examples.thy
berghofe@14592
     2
    ID:         $Id$
berghofe@14592
     3
    Author:     Stefan Berghofer
berghofe@14592
     4
    Copyright   2004 TU Muenchen
berghofe@14592
     5
*)
berghofe@14592
     6
berghofe@14592
     7
header {* Examples for the 'quickcheck' command *}
berghofe@14592
     8
haftmann@16417
     9
theory Quickcheck_Examples imports Main begin
berghofe@14592
    10
berghofe@14592
    11
text {*
berghofe@14592
    12
The 'quickcheck' command allows to find counterexamples by evaluating
berghofe@14592
    13
formulae under an assignment of free variables to random values.
berghofe@14592
    14
In contrast to 'refute', it can deal with inductive datatypes,
berghofe@14592
    15
but cannot handle quantifiers.
berghofe@14592
    16
*}
berghofe@14592
    17
berghofe@14592
    18
subsection {* Lists *}
berghofe@14592
    19
berghofe@14592
    20
theorem "map g (map f xs) = map (g o f) xs"
berghofe@14592
    21
  quickcheck
berghofe@14592
    22
  oops
berghofe@14592
    23
berghofe@14592
    24
theorem "map g (map f xs) = map (f o g) xs"
berghofe@14592
    25
  quickcheck
berghofe@14592
    26
  oops
berghofe@14592
    27
berghofe@14592
    28
theorem "rev (xs @ ys) = rev ys @ rev xs"
berghofe@14592
    29
  quickcheck
berghofe@14592
    30
  oops
berghofe@14592
    31
berghofe@14592
    32
theorem "rev (xs @ ys) = rev xs @ rev ys"
berghofe@14592
    33
  quickcheck
berghofe@14592
    34
  oops
berghofe@14592
    35
berghofe@14592
    36
theorem "rev (rev xs) = xs"
berghofe@14592
    37
  quickcheck
berghofe@14592
    38
  oops
berghofe@14592
    39
berghofe@14592
    40
theorem "rev xs = xs"
berghofe@14592
    41
  quickcheck
berghofe@14592
    42
  oops
berghofe@14592
    43
berghofe@14592
    44
consts
berghofe@14592
    45
  occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
berghofe@14592
    46
primrec
berghofe@14592
    47
  "occurs a [] = 0"
berghofe@14592
    48
  "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
berghofe@14592
    49
berghofe@14592
    50
consts
berghofe@14592
    51
  del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
berghofe@14592
    52
primrec
berghofe@14592
    53
  "del1 a [] = []"
berghofe@14592
    54
  "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
berghofe@14592
    55
berghofe@14592
    56
(* A lemma, you'd think to be true from our experience with delAll*)
berghofe@14592
    57
lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
berghofe@14592
    58
  -- {* Wrong. Precondition needed.*}
berghofe@14592
    59
  quickcheck
berghofe@14592
    60
  oops
berghofe@14592
    61
berghofe@14592
    62
lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
berghofe@14592
    63
  quickcheck
berghofe@14592
    64
    -- {* Also wrong.*}
berghofe@14592
    65
  oops
berghofe@14592
    66
berghofe@14592
    67
lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
berghofe@14592
    68
  quickcheck
berghofe@14592
    69
  apply (induct_tac xs)  
berghofe@14592
    70
  apply auto
berghofe@14592
    71
    -- {* Correct! *}
berghofe@14592
    72
  done
berghofe@14592
    73
berghofe@14592
    74
consts
berghofe@14592
    75
  replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
berghofe@14592
    76
primrec
berghofe@14592
    77
  "replace a b [] = []"
berghofe@14592
    78
  "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
berghofe@14592
    79
                            else (x#(replace a b xs)))"
berghofe@14592
    80
berghofe@14592
    81
lemma "occurs a xs = occurs b (replace a b xs)"
berghofe@14592
    82
  quickcheck
berghofe@14592
    83
  -- {* Wrong. Precondition needed.*}
berghofe@14592
    84
  oops
berghofe@14592
    85
berghofe@14592
    86
lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
berghofe@14592
    87
  quickcheck
berghofe@14592
    88
  apply (induct_tac xs)  
berghofe@14592
    89
  apply auto
berghofe@14592
    90
  done
berghofe@14592
    91
berghofe@14592
    92
berghofe@14592
    93
subsection {* Trees *}
berghofe@14592
    94
berghofe@14592
    95
datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
berghofe@14592
    96
berghofe@14592
    97
consts
berghofe@14592
    98
  leaves :: "'a tree \<Rightarrow> 'a list"
berghofe@14592
    99
primrec
berghofe@14592
   100
  "leaves Twig = []"
berghofe@14592
   101
  "leaves (Leaf a) = [a]"
berghofe@14592
   102
  "leaves (Branch l r) = (leaves l) @ (leaves r)"
berghofe@14592
   103
berghofe@14592
   104
consts
berghofe@14592
   105
  plant :: "'a list \<Rightarrow> 'a tree"
berghofe@14592
   106
primrec
berghofe@14592
   107
  "plant [] = Twig "
berghofe@14592
   108
  "plant (x#xs) = Branch (Leaf x) (plant xs)"
berghofe@14592
   109
berghofe@14592
   110
consts
berghofe@14592
   111
  mirror :: "'a tree \<Rightarrow> 'a tree"
berghofe@14592
   112
primrec
berghofe@14592
   113
  "mirror (Twig) = Twig "
berghofe@14592
   114
  "mirror (Leaf a) = Leaf a "
berghofe@14592
   115
  "mirror (Branch l r) = Branch (mirror r) (mirror l)"
berghofe@14592
   116
berghofe@14592
   117
theorem "plant (rev (leaves xt)) = mirror xt"
berghofe@14592
   118
  quickcheck
berghofe@14592
   119
    --{* Wrong! *} 
berghofe@14592
   120
  oops
berghofe@14592
   121
berghofe@14592
   122
theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
berghofe@14592
   123
  quickcheck
berghofe@14592
   124
    --{* Wrong! *} 
berghofe@14592
   125
  oops
berghofe@14592
   126
berghofe@14592
   127
datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
berghofe@14592
   128
berghofe@14592
   129
consts
berghofe@14592
   130
  inOrder :: "'a ntree \<Rightarrow> 'a list"
berghofe@14592
   131
primrec
berghofe@14592
   132
  "inOrder (Tip a)= [a]"
berghofe@14592
   133
  "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
berghofe@14592
   134
berghofe@14592
   135
consts
berghofe@14592
   136
  root :: "'a ntree \<Rightarrow> 'a"
berghofe@14592
   137
primrec
berghofe@14592
   138
  "root (Tip a) = a"
berghofe@14592
   139
  "root (Node f x y) = f"
berghofe@14592
   140
berghofe@14592
   141
theorem "hd(inOrder xt) = root xt"
berghofe@14592
   142
  quickcheck
berghofe@14592
   143
    --{* Wrong! *} 
berghofe@14592
   144
  oops
berghofe@14592
   145
berghofe@14592
   146
end