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