src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
author huffman
Sun Apr 01 16:09:58 2012 +0200 (2012-04-01)
changeset 47255 30a1692557b0
parent 47108 2a1953f0d20d
child 58148 9764b994a421
permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
wenzelm@46879
     1
(*  Title:      HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
bulwahn@41907
     2
    Author:     Lukas Bulwahn
bulwahn@41907
     3
    Copyright   2011 TU Muenchen
bulwahn@41907
     4
*)
bulwahn@41907
     5
bulwahn@41932
     6
header {* Examples for narrowing-based testing  *}
bulwahn@41907
     7
bulwahn@41932
     8
theory Quickcheck_Narrowing_Examples
bulwahn@43318
     9
imports Main
bulwahn@41907
    10
begin
bulwahn@41907
    11
bulwahn@45773
    12
declare [[quickcheck_timeout = 3600]]
bulwahn@45773
    13
bulwahn@42020
    14
subsection {* Minimalistic examples *}
bulwahn@43356
    15
bulwahn@42020
    16
lemma
bulwahn@42020
    17
  "x = y"
bulwahn@42021
    18
quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
bulwahn@41907
    19
oops
bulwahn@43356
    20
bulwahn@42020
    21
lemma
bulwahn@42020
    22
  "x = y"
bulwahn@43356
    23
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
bulwahn@41907
    24
oops
bulwahn@41907
    25
bulwahn@43239
    26
subsection {* Simple examples with existentials *}
bulwahn@43239
    27
bulwahn@43239
    28
lemma
bulwahn@43239
    29
  "\<exists> y :: nat. \<forall> x. x = y"
bulwahn@43239
    30
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@43239
    31
oops
bulwahn@43356
    32
(*
bulwahn@43356
    33
lemma
bulwahn@43356
    34
  "\<exists> y :: int. \<forall> x. x = y"
bulwahn@43356
    35
quickcheck[tester = narrowing, size = 2]
bulwahn@43356
    36
oops
bulwahn@43356
    37
*)
bulwahn@43239
    38
lemma
bulwahn@43239
    39
  "x > 1 --> (\<exists>y :: nat. x < y & y <= 1)"
bulwahn@43239
    40
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@43239
    41
oops
bulwahn@43239
    42
bulwahn@43239
    43
lemma
bulwahn@43239
    44
  "x > 2 --> (\<exists>y :: nat. x < y & y <= 2)"
bulwahn@43239
    45
quickcheck[tester = narrowing, finite_types = false, size = 10]
bulwahn@43239
    46
oops
bulwahn@43239
    47
bulwahn@43239
    48
lemma
bulwahn@43239
    49
  "\<forall> x. \<exists> y :: nat. x > 3 --> (y < x & y > 3)"
bulwahn@43239
    50
quickcheck[tester = narrowing, finite_types = false, size = 7]
bulwahn@43239
    51
oops
bulwahn@43239
    52
bulwahn@43239
    53
text {* A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp} *}
bulwahn@43239
    54
lemma
bulwahn@43239
    55
  "~ distinct ws ==> EX xs ys zs y. ws = xs @ [y] @ ys @ [y]"
bulwahn@43239
    56
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
bulwahn@43239
    57
oops
bulwahn@43239
    58
bulwahn@43239
    59
text {* A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last} *}  
bulwahn@43239
    60
lemma
bulwahn@43239
    61
  "x : set xs ==> EX ys zs. xs = ys @ x # zs & x ~: set zs & x ~: set ys"
bulwahn@43239
    62
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
bulwahn@43239
    63
oops
bulwahn@43239
    64
bulwahn@43239
    65
text {* A false conjecture derived from @{thm map_eq_Cons_conv} with a typo *}
bulwahn@43239
    66
lemma
bulwahn@43239
    67
  "(map f xs = y # ys) = (EX z zs. xs = z' # zs & f z = y & map f zs = ys)"
bulwahn@43239
    68
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
bulwahn@43239
    69
oops
bulwahn@43239
    70
bulwahn@45441
    71
lemma "a # xs = ys @ [a] ==> EX zs. xs = zs @ [a] & ys = a#zs"
bulwahn@45441
    72
quickcheck[narrowing, expect = counterexample]
bulwahn@45441
    73
quickcheck[exhaustive, random, expect = no_counterexample]
bulwahn@45441
    74
oops
bulwahn@45441
    75
bulwahn@42020
    76
subsection {* Simple list examples *}
bulwahn@42020
    77
bulwahn@42020
    78
lemma "rev xs = xs"
bulwahn@43239
    79
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
bulwahn@42020
    80
oops
bulwahn@42020
    81
bulwahn@42020
    82
lemma "rev xs = xs"
bulwahn@43239
    83
quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
bulwahn@42021
    84
oops
huffman@47108
    85
bulwahn@42021
    86
lemma "rev xs = xs"
bulwahn@42023
    87
  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
bulwahn@42023
    88
oops
huffman@47108
    89
bulwahn@42023
    90
subsection {* Simple examples with functions *}
bulwahn@42023
    91
bulwahn@42023
    92
lemma "map f xs = map g xs"
bulwahn@43239
    93
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@42020
    94
oops
bulwahn@42020
    95
bulwahn@42023
    96
lemma "map f xs = map f ys ==> xs = ys"
bulwahn@43239
    97
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@42024
    98
oops
bulwahn@42024
    99
bulwahn@42024
   100
lemma
bulwahn@42024
   101
  "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
bulwahn@45773
   102
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@42024
   103
oops
bulwahn@42024
   104
bulwahn@42024
   105
lemma "map f xs = F f xs"
bulwahn@42024
   106
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@42024
   107
oops
bulwahn@42024
   108
bulwahn@43239
   109
lemma "map f xs = F f xs"
bulwahn@43239
   110
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@43239
   111
oops
bulwahn@43239
   112
bulwahn@43239
   113
(* requires some work...*)
bulwahn@43239
   114
(*
bulwahn@42024
   115
lemma "R O S = S O R"
bulwahn@42024
   116
  quickcheck[tester = narrowing, size = 2]
bulwahn@42024
   117
oops
bulwahn@42024
   118
*)
bulwahn@42024
   119
bulwahn@45082
   120
subsection {* Simple examples with inductive predicates *}
bulwahn@45082
   121
bulwahn@45082
   122
inductive even where
bulwahn@45082
   123
  "even 0" |
bulwahn@45082
   124
  "even n ==> even (Suc (Suc n))"
bulwahn@45082
   125
bulwahn@45082
   126
code_pred even .
bulwahn@45082
   127
bulwahn@45082
   128
lemma "even (n - 2) ==> even n"
bulwahn@45082
   129
quickcheck[narrowing, expect = counterexample]
bulwahn@45082
   130
oops
bulwahn@45082
   131
bulwahn@45082
   132
bulwahn@41907
   133
subsection {* AVL Trees *}
bulwahn@41907
   134
bulwahn@41907
   135
datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
bulwahn@41907
   136
bulwahn@41907
   137
primrec set_of :: "'a tree \<Rightarrow> 'a set"
bulwahn@41907
   138
where
bulwahn@41907
   139
"set_of ET = {}" |
bulwahn@41907
   140
"set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
bulwahn@41907
   141
bulwahn@41907
   142
primrec height :: "'a tree \<Rightarrow> nat"
bulwahn@41907
   143
where
bulwahn@41907
   144
"height ET = 0" |
bulwahn@41907
   145
"height (MKT x l r h) = max (height l) (height r) + 1"
bulwahn@41907
   146
bulwahn@41907
   147
primrec avl :: "'a tree \<Rightarrow> bool"
bulwahn@41907
   148
where
bulwahn@41907
   149
"avl ET = True" |
bulwahn@41907
   150
"avl (MKT x l r h) =
bulwahn@41907
   151
 ((height l = height r \<or> height l = 1+height r \<or> height r = 1+height l) \<and> 
bulwahn@41907
   152
  h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
bulwahn@41907
   153
bulwahn@41907
   154
primrec is_ord :: "('a::order) tree \<Rightarrow> bool"
bulwahn@41907
   155
where
bulwahn@41907
   156
"is_ord ET = True" |
bulwahn@41907
   157
"is_ord (MKT n l r h) =
bulwahn@41907
   158
 ((\<forall>n' \<in> set_of l. n' < n) \<and> (\<forall>n' \<in> set_of r. n < n') \<and> is_ord l \<and> is_ord r)"
bulwahn@41907
   159
bulwahn@41907
   160
primrec is_in :: "('a::order) \<Rightarrow> 'a tree \<Rightarrow> bool"
bulwahn@41907
   161
where
bulwahn@41907
   162
 "is_in k ET = False" |
bulwahn@41907
   163
 "is_in k (MKT n l r h) = (if k = n then True else
bulwahn@41907
   164
                           if k < n then (is_in k l)
bulwahn@41907
   165
                           else (is_in k r))"
bulwahn@41907
   166
bulwahn@41907
   167
primrec ht :: "'a tree \<Rightarrow> nat"
bulwahn@41907
   168
where
bulwahn@41907
   169
"ht ET = 0" |
bulwahn@41907
   170
"ht (MKT x l r h) = h"
bulwahn@41907
   171
bulwahn@41907
   172
definition
bulwahn@41907
   173
 mkt :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
bulwahn@41907
   174
"mkt x l r = MKT x l r (max (ht l) (ht r) + 1)"
bulwahn@41907
   175
bulwahn@41907
   176
(* replaced MKT lrn lrl lrr by MKT lrr lrl *)
bulwahn@41907
   177
fun l_bal where
bulwahn@41907
   178
"l_bal(n, MKT ln ll lr h, r) =
bulwahn@41907
   179
 (if ht ll < ht lr
bulwahn@41907
   180
  then case lr of ET \<Rightarrow> ET (* impossible *)
bulwahn@41907
   181
                | MKT lrn lrr lrl lrh \<Rightarrow>
bulwahn@41907
   182
                  mkt lrn (mkt ln ll lrl) (mkt n lrr r)
bulwahn@41907
   183
  else mkt ln ll (mkt n lr r))"
bulwahn@41907
   184
bulwahn@41907
   185
fun r_bal where
bulwahn@41907
   186
"r_bal(n, l, MKT rn rl rr h) =
bulwahn@41907
   187
 (if ht rl > ht rr
bulwahn@41907
   188
  then case rl of ET \<Rightarrow> ET (* impossible *)
bulwahn@41907
   189
                | MKT rln rll rlr h \<Rightarrow> mkt rln (mkt n l rll) (mkt rn rlr rr)
bulwahn@41907
   190
  else mkt rn (mkt n l rl) rr)"
bulwahn@41907
   191
bulwahn@41907
   192
primrec insrt :: "'a::order \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
bulwahn@41907
   193
where
bulwahn@41907
   194
"insrt x ET = MKT x ET ET 1" |
bulwahn@41907
   195
"insrt x (MKT n l r h) = 
bulwahn@41907
   196
   (if x=n
bulwahn@41907
   197
    then MKT n l r h
bulwahn@41907
   198
    else if x<n
bulwahn@41907
   199
         then let l' = insrt x l; hl' = ht l'; hr = ht r
bulwahn@41907
   200
              in if hl' = 2+hr then l_bal(n,l',r)
bulwahn@41907
   201
                 else MKT n l' r (1 + max hl' hr)
bulwahn@41907
   202
         else let r' = insrt x r; hl = ht l; hr' = ht r'
bulwahn@41907
   203
              in if hr' = 2+hl then r_bal(n,l,r')
bulwahn@41907
   204
                 else MKT n l r' (1 + max hl hr'))"
bulwahn@41907
   205
bulwahn@41907
   206
bulwahn@41907
   207
subsubsection {* Necessary setup for code generation *}
bulwahn@41907
   208
bulwahn@41907
   209
primrec set_of'
bulwahn@41907
   210
where 
bulwahn@41907
   211
  "set_of' ET = []"
bulwahn@41907
   212
| "set_of' (MKT n l r h) = n # (set_of' l @ set_of' r)"
bulwahn@41907
   213
bulwahn@41907
   214
lemma set_of':
bulwahn@41907
   215
  "set (set_of' t) = set_of t"
bulwahn@41907
   216
by (induct t) auto
bulwahn@41907
   217
bulwahn@41907
   218
lemma is_ord_mkt:
bulwahn@41907
   219
  "is_ord (MKT n l r h) = ((ALL n': set (set_of' l). n' < n) & (ALL n': set (set_of' r). n < n') & is_ord l & is_ord r)"
bulwahn@41907
   220
by (simp add: set_of')
bulwahn@41907
   221
bulwahn@41907
   222
declare is_ord.simps(1)[code] is_ord_mkt[code]
bulwahn@41907
   223
bulwahn@41907
   224
subsubsection {* Invalid Lemma due to typo in lbal *}
bulwahn@41907
   225
bulwahn@41907
   226
lemma is_ord_l_bal:
bulwahn@41907
   227
 "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
bulwahn@45773
   228
quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, expect = counterexample]
bulwahn@41907
   229
oops
bulwahn@41907
   230
bulwahn@45790
   231
subsection {* Examples with hd and last *}
bulwahn@45790
   232
bulwahn@45790
   233
lemma
bulwahn@45790
   234
  "hd (xs @ ys) = hd ys"
bulwahn@45790
   235
quickcheck[narrowing, expect = counterexample]
bulwahn@45790
   236
oops
bulwahn@45790
   237
bulwahn@45790
   238
lemma
bulwahn@45790
   239
  "last(xs @ ys) = last xs"
bulwahn@45790
   240
quickcheck[narrowing, expect = counterexample]
bulwahn@45790
   241
oops
bulwahn@45790
   242
bulwahn@45790
   243
subsection {* Examples with underspecified/partial functions *}
bulwahn@45790
   244
bulwahn@45790
   245
lemma
bulwahn@45790
   246
  "xs = [] ==> hd xs \<noteq> x"
bulwahn@45790
   247
quickcheck[narrowing, expect = no_counterexample]
bulwahn@45790
   248
oops
bulwahn@45790
   249
bulwahn@45790
   250
lemma
bulwahn@45790
   251
  "xs = [] ==> hd xs = x"
bulwahn@45790
   252
quickcheck[narrowing, expect = no_counterexample]
bulwahn@45790
   253
oops
bulwahn@45790
   254
bulwahn@45790
   255
lemma "xs = [] ==> hd xs = x ==> x = y"
bulwahn@45790
   256
quickcheck[narrowing, expect = no_counterexample]
bulwahn@45790
   257
oops
bulwahn@45790
   258
bulwahn@45790
   259
lemma
bulwahn@45790
   260
  "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
bulwahn@45790
   261
quickcheck[narrowing, expect = no_counterexample]
bulwahn@45790
   262
oops
bulwahn@45790
   263
bulwahn@45790
   264
lemma
bulwahn@45790
   265
  "hd (map f xs) = f (hd xs)"
bulwahn@45790
   266
quickcheck[narrowing, expect = no_counterexample]
bulwahn@45790
   267
oops
bulwahn@41907
   268
bulwahn@41907
   269
end