src/HOL/ex/SML_Quickcheck_Examples.thy
author bulwahn
Wed Jul 06 13:52:42 2011 +0200 (2011-07-06)
changeset 43686 bc7d63c7fd6f
parent 42161 d1b39536e1fb
permissions -rw-r--r--
tuning options to avoid spurious isabelle test failures
bulwahn@42161
     1
(*  Title:      HOL/ex/SML_Quickcheck_Examples.thy
bulwahn@42161
     2
    Author:     Stefan Berghofer, Lukas Bulwahn
bulwahn@42161
     3
    Copyright   2011 TU Muenchen
bulwahn@42161
     4
*)
bulwahn@42161
     5
bulwahn@42161
     6
theory SML_Quickcheck_Examples
bulwahn@42161
     7
imports "~~/src/HOL/Library/SML_Quickcheck"
bulwahn@42161
     8
begin
bulwahn@42161
     9
bulwahn@42161
    10
text {*
bulwahn@42161
    11
This is a regression test for the 'quickcheck' counterexample generator based on the
bulwahn@42161
    12
SML code generator.
bulwahn@42161
    13
bulwahn@42161
    14
The counterexample generator has been superseded by counterexample generators based on
bulwahn@42161
    15
the generic code generator.
bulwahn@42161
    16
*}
bulwahn@42161
    17
bulwahn@42161
    18
declare [[quickcheck_finite_types = false]]
bulwahn@43686
    19
declare [[quickcheck_timeout = 600.0]]
bulwahn@42161
    20
bulwahn@42161
    21
subsection {* Lists *}
bulwahn@42161
    22
bulwahn@42161
    23
theorem "map g (map f xs) = map (g o f) xs"
bulwahn@42161
    24
  quickcheck[SML, expect = no_counterexample]
bulwahn@42161
    25
  oops
bulwahn@42161
    26
bulwahn@42161
    27
theorem "map g (map f xs) = map (f o g) xs"
bulwahn@42161
    28
  quickcheck[SML, expect = counterexample]
bulwahn@42161
    29
  oops
bulwahn@42161
    30
bulwahn@42161
    31
theorem "rev (xs @ ys) = rev ys @ rev xs"
bulwahn@42161
    32
  quickcheck[SML, expect = no_counterexample]
bulwahn@42161
    33
  oops
bulwahn@42161
    34
bulwahn@42161
    35
theorem "rev (xs @ ys) = rev xs @ rev ys"
bulwahn@42161
    36
  quickcheck[SML, expect = counterexample]
bulwahn@42161
    37
  oops
bulwahn@42161
    38
bulwahn@42161
    39
theorem "rev (rev xs) = xs"
bulwahn@42161
    40
  quickcheck[SML, expect = no_counterexample]
bulwahn@42161
    41
  oops
bulwahn@42161
    42
bulwahn@42161
    43
theorem "rev xs = xs"
bulwahn@42161
    44
  quickcheck[tester = SML, expect = counterexample]
bulwahn@42161
    45
oops
bulwahn@42161
    46
bulwahn@42161
    47
bulwahn@42161
    48
text {* An example involving functions inside other data structures *}
bulwahn@42161
    49
bulwahn@42161
    50
primrec app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a" where
bulwahn@42161
    51
  "app [] x = x"
bulwahn@42161
    52
  | "app (f # fs) x = app fs (f x)"
bulwahn@42161
    53
bulwahn@42161
    54
lemma "app (fs @ gs) x = app gs (app fs x)"
bulwahn@42161
    55
  quickcheck[SML, expect = no_counterexample]
bulwahn@42161
    56
  by (induct fs arbitrary: x) simp_all
bulwahn@42161
    57
bulwahn@42161
    58
lemma "app (fs @ gs) x = app fs (app gs x)"
bulwahn@42161
    59
  quickcheck[SML, expect = counterexample]
bulwahn@42161
    60
  oops
bulwahn@42161
    61
bulwahn@42161
    62
primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
bulwahn@42161
    63
  "occurs a [] = 0"
bulwahn@42161
    64
  | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"
bulwahn@42161
    65
bulwahn@42161
    66
primrec del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
bulwahn@42161
    67
  "del1 a [] = []"
bulwahn@42161
    68
  | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
bulwahn@42161
    69
bulwahn@42161
    70
text {* A lemma, you'd think to be true from our experience with delAll *}
bulwahn@42161
    71
lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
bulwahn@42161
    72
  -- {* Wrong. Precondition needed.*}
bulwahn@42161
    73
  quickcheck[SML, expect = counterexample]
bulwahn@42161
    74
  oops
bulwahn@42161
    75
bulwahn@42161
    76
lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
bulwahn@42161
    77
  quickcheck[SML, expect = counterexample]
bulwahn@42161
    78
    -- {* Also wrong.*}
bulwahn@42161
    79
  oops
bulwahn@42161
    80
bulwahn@42161
    81
lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
bulwahn@42161
    82
  quickcheck[SML, expect = no_counterexample]
bulwahn@42161
    83
  by (induct xs) auto
bulwahn@42161
    84
bulwahn@42161
    85
primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
bulwahn@42161
    86
  "replace a b [] = []"
bulwahn@42161
    87
  | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
bulwahn@42161
    88
                            else (x#(replace a b xs)))"
bulwahn@42161
    89
bulwahn@42161
    90
lemma "occurs a xs = occurs b (replace a b xs)"
bulwahn@42161
    91
  quickcheck[SML, expect = counterexample]
bulwahn@42161
    92
  -- {* Wrong. Precondition needed.*}
bulwahn@42161
    93
  oops
bulwahn@42161
    94
bulwahn@42161
    95
lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
bulwahn@42161
    96
  quickcheck[SML, expect = no_counterexample]
bulwahn@42161
    97
  by (induct xs) simp_all
bulwahn@42161
    98
bulwahn@42161
    99
bulwahn@42161
   100
subsection {* Trees *}
bulwahn@42161
   101
bulwahn@42161
   102
datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"
bulwahn@42161
   103
bulwahn@42161
   104
primrec leaves :: "'a tree \<Rightarrow> 'a list" where
bulwahn@42161
   105
  "leaves Twig = []"
bulwahn@42161
   106
  | "leaves (Leaf a) = [a]"
bulwahn@42161
   107
  | "leaves (Branch l r) = (leaves l) @ (leaves r)"
bulwahn@42161
   108
bulwahn@42161
   109
primrec plant :: "'a list \<Rightarrow> 'a tree" where
bulwahn@42161
   110
  "plant [] = Twig "
bulwahn@42161
   111
  | "plant (x#xs) = Branch (Leaf x) (plant xs)"
bulwahn@42161
   112
bulwahn@42161
   113
primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
bulwahn@42161
   114
  "mirror (Twig) = Twig "
bulwahn@42161
   115
  | "mirror (Leaf a) = Leaf a "
bulwahn@42161
   116
  | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
bulwahn@42161
   117
bulwahn@42161
   118
theorem "plant (rev (leaves xt)) = mirror xt"
bulwahn@42161
   119
  quickcheck[SML, expect = counterexample]
bulwahn@42161
   120
    --{* Wrong! *} 
bulwahn@42161
   121
  oops
bulwahn@42161
   122
bulwahn@42161
   123
theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
bulwahn@42161
   124
  quickcheck[SML, expect = counterexample]
bulwahn@42161
   125
    --{* Wrong! *} 
bulwahn@42161
   126
  oops
bulwahn@42161
   127
bulwahn@42161
   128
datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"
bulwahn@42161
   129
bulwahn@42161
   130
primrec inOrder :: "'a ntree \<Rightarrow> 'a list" where
bulwahn@42161
   131
  "inOrder (Tip a)= [a]"
bulwahn@42161
   132
  | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"
bulwahn@42161
   133
bulwahn@42161
   134
primrec root :: "'a ntree \<Rightarrow> 'a" where
bulwahn@42161
   135
  "root (Tip a) = a"
bulwahn@42161
   136
  | "root (Node f x y) = f"
bulwahn@42161
   137
bulwahn@42161
   138
theorem "hd (inOrder xt) = root xt"
bulwahn@42161
   139
  quickcheck[SML, expect = counterexample]
bulwahn@42161
   140
  --{* Wrong! *} 
bulwahn@42161
   141
  oops
bulwahn@42161
   142
bulwahn@43686
   143
end