src/HOL/ex/Quickcheck_Narrowing_Examples.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45082 54c4e12bb5e0
child 45441 fb4ac1dd4fde
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn@41932
     1
(*  Title:      HOL/ex/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@42020
    12
subsection {* Minimalistic examples *}
bulwahn@43356
    13
bulwahn@42020
    14
lemma
bulwahn@42020
    15
  "x = y"
bulwahn@42021
    16
quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
bulwahn@41907
    17
oops
bulwahn@43356
    18
bulwahn@42020
    19
lemma
bulwahn@42020
    20
  "x = y"
bulwahn@43356
    21
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
bulwahn@41907
    22
oops
bulwahn@41907
    23
bulwahn@43239
    24
subsection {* Simple examples with existentials *}
bulwahn@43239
    25
bulwahn@43239
    26
lemma
bulwahn@43239
    27
  "\<exists> y :: nat. \<forall> x. x = y"
bulwahn@43239
    28
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@43239
    29
oops
bulwahn@43356
    30
(*
bulwahn@43356
    31
lemma
bulwahn@43356
    32
  "\<exists> y :: int. \<forall> x. x = y"
bulwahn@43356
    33
quickcheck[tester = narrowing, size = 2]
bulwahn@43356
    34
oops
bulwahn@43356
    35
*)
bulwahn@43239
    36
lemma
bulwahn@43239
    37
  "x > 1 --> (\<exists>y :: nat. x < y & y <= 1)"
bulwahn@43239
    38
quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@43239
    39
oops
bulwahn@43239
    40
bulwahn@43239
    41
lemma
bulwahn@43239
    42
  "x > 2 --> (\<exists>y :: nat. x < y & y <= 2)"
bulwahn@43239
    43
quickcheck[tester = narrowing, finite_types = false, size = 10]
bulwahn@43239
    44
oops
bulwahn@43239
    45
bulwahn@43239
    46
lemma
bulwahn@43239
    47
  "\<forall> x. \<exists> y :: nat. x > 3 --> (y < x & y > 3)"
bulwahn@43239
    48
quickcheck[tester = narrowing, finite_types = false, size = 7]
bulwahn@43239
    49
oops
bulwahn@43239
    50
bulwahn@43239
    51
text {* A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp} *}
bulwahn@43239
    52
lemma
bulwahn@43239
    53
  "~ distinct ws ==> EX xs ys zs y. ws = xs @ [y] @ ys @ [y]"
bulwahn@43239
    54
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
bulwahn@43239
    55
oops
bulwahn@43239
    56
bulwahn@43239
    57
text {* A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last} *}  
bulwahn@43239
    58
lemma
bulwahn@43239
    59
  "x : set xs ==> EX ys zs. xs = ys @ x # zs & x ~: set zs & x ~: set ys"
bulwahn@43239
    60
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
bulwahn@43239
    61
oops
bulwahn@43239
    62
bulwahn@43239
    63
text {* A false conjecture derived from @{thm map_eq_Cons_conv} with a typo *}
bulwahn@43239
    64
lemma
bulwahn@43239
    65
  "(map f xs = y # ys) = (EX z zs. xs = z' # zs & f z = y & map f zs = ys)"
bulwahn@43239
    66
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
bulwahn@43239
    67
oops
bulwahn@43239
    68
bulwahn@42020
    69
subsection {* Simple list examples *}
bulwahn@42020
    70
bulwahn@42020
    71
lemma "rev xs = xs"
bulwahn@43239
    72
quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
bulwahn@42020
    73
oops
bulwahn@42020
    74
bulwahn@43239
    75
(* FIXME: integer has strange representation! *)
bulwahn@42020
    76
lemma "rev xs = xs"
bulwahn@43239
    77
quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
bulwahn@42021
    78
oops
bulwahn@42184
    79
(*
bulwahn@42021
    80
lemma "rev xs = xs"
bulwahn@42023
    81
  quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
bulwahn@42023
    82
oops
bulwahn@42184
    83
*)
bulwahn@42023
    84
subsection {* Simple examples with functions *}
bulwahn@42023
    85
bulwahn@42023
    86
lemma "map f xs = map g xs"
bulwahn@43239
    87
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@42020
    88
oops
bulwahn@42020
    89
bulwahn@42023
    90
lemma "map f xs = map f ys ==> xs = ys"
bulwahn@43239
    91
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@42024
    92
oops
bulwahn@42024
    93
bulwahn@42024
    94
lemma
bulwahn@42024
    95
  "list_all2 P (rev xs) (rev ys) = list_all2 P xs (rev ys)"
bulwahn@43239
    96
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@42024
    97
oops
bulwahn@42024
    98
bulwahn@42024
    99
lemma "map f xs = F f xs"
bulwahn@42024
   100
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@42024
   101
oops
bulwahn@42024
   102
bulwahn@43239
   103
lemma "map f xs = F f xs"
bulwahn@43239
   104
  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
bulwahn@43239
   105
oops
bulwahn@43239
   106
bulwahn@43239
   107
(* requires some work...*)
bulwahn@43239
   108
(*
bulwahn@42024
   109
lemma "R O S = S O R"
bulwahn@42024
   110
  quickcheck[tester = narrowing, size = 2]
bulwahn@42024
   111
oops
bulwahn@42024
   112
*)
bulwahn@42024
   113
bulwahn@45082
   114
subsection {* Simple examples with inductive predicates *}
bulwahn@45082
   115
bulwahn@45082
   116
inductive even where
bulwahn@45082
   117
  "even 0" |
bulwahn@45082
   118
  "even n ==> even (Suc (Suc n))"
bulwahn@45082
   119
bulwahn@45082
   120
code_pred even .
bulwahn@45082
   121
bulwahn@45082
   122
lemma "even (n - 2) ==> even n"
bulwahn@45082
   123
quickcheck[narrowing, expect = counterexample]
bulwahn@45082
   124
oops
bulwahn@45082
   125
bulwahn@45082
   126
bulwahn@41907
   127
subsection {* AVL Trees *}
bulwahn@41907
   128
bulwahn@41907
   129
datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
bulwahn@41907
   130
bulwahn@41907
   131
primrec set_of :: "'a tree \<Rightarrow> 'a set"
bulwahn@41907
   132
where
bulwahn@41907
   133
"set_of ET = {}" |
bulwahn@41907
   134
"set_of (MKT n l r h) = insert n (set_of l \<union> set_of r)"
bulwahn@41907
   135
bulwahn@41907
   136
primrec height :: "'a tree \<Rightarrow> nat"
bulwahn@41907
   137
where
bulwahn@41907
   138
"height ET = 0" |
bulwahn@41907
   139
"height (MKT x l r h) = max (height l) (height r) + 1"
bulwahn@41907
   140
bulwahn@41907
   141
primrec avl :: "'a tree \<Rightarrow> bool"
bulwahn@41907
   142
where
bulwahn@41907
   143
"avl ET = True" |
bulwahn@41907
   144
"avl (MKT x l r h) =
bulwahn@41907
   145
 ((height l = height r \<or> height l = 1+height r \<or> height r = 1+height l) \<and> 
bulwahn@41907
   146
  h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
bulwahn@41907
   147
bulwahn@41907
   148
primrec is_ord :: "('a::order) tree \<Rightarrow> bool"
bulwahn@41907
   149
where
bulwahn@41907
   150
"is_ord ET = True" |
bulwahn@41907
   151
"is_ord (MKT n l r h) =
bulwahn@41907
   152
 ((\<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
   153
bulwahn@41907
   154
primrec is_in :: "('a::order) \<Rightarrow> 'a tree \<Rightarrow> bool"
bulwahn@41907
   155
where
bulwahn@41907
   156
 "is_in k ET = False" |
bulwahn@41907
   157
 "is_in k (MKT n l r h) = (if k = n then True else
bulwahn@41907
   158
                           if k < n then (is_in k l)
bulwahn@41907
   159
                           else (is_in k r))"
bulwahn@41907
   160
bulwahn@41907
   161
primrec ht :: "'a tree \<Rightarrow> nat"
bulwahn@41907
   162
where
bulwahn@41907
   163
"ht ET = 0" |
bulwahn@41907
   164
"ht (MKT x l r h) = h"
bulwahn@41907
   165
bulwahn@41907
   166
definition
bulwahn@41907
   167
 mkt :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
bulwahn@41907
   168
"mkt x l r = MKT x l r (max (ht l) (ht r) + 1)"
bulwahn@41907
   169
bulwahn@41907
   170
(* replaced MKT lrn lrl lrr by MKT lrr lrl *)
bulwahn@41907
   171
fun l_bal where
bulwahn@41907
   172
"l_bal(n, MKT ln ll lr h, r) =
bulwahn@41907
   173
 (if ht ll < ht lr
bulwahn@41907
   174
  then case lr of ET \<Rightarrow> ET (* impossible *)
bulwahn@41907
   175
                | MKT lrn lrr lrl lrh \<Rightarrow>
bulwahn@41907
   176
                  mkt lrn (mkt ln ll lrl) (mkt n lrr r)
bulwahn@41907
   177
  else mkt ln ll (mkt n lr r))"
bulwahn@41907
   178
bulwahn@41907
   179
fun r_bal where
bulwahn@41907
   180
"r_bal(n, l, MKT rn rl rr h) =
bulwahn@41907
   181
 (if ht rl > ht rr
bulwahn@41907
   182
  then case rl of ET \<Rightarrow> ET (* impossible *)
bulwahn@41907
   183
                | MKT rln rll rlr h \<Rightarrow> mkt rln (mkt n l rll) (mkt rn rlr rr)
bulwahn@41907
   184
  else mkt rn (mkt n l rl) rr)"
bulwahn@41907
   185
bulwahn@41907
   186
primrec insrt :: "'a::order \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
bulwahn@41907
   187
where
bulwahn@41907
   188
"insrt x ET = MKT x ET ET 1" |
bulwahn@41907
   189
"insrt x (MKT n l r h) = 
bulwahn@41907
   190
   (if x=n
bulwahn@41907
   191
    then MKT n l r h
bulwahn@41907
   192
    else if x<n
bulwahn@41907
   193
         then let l' = insrt x l; hl' = ht l'; hr = ht r
bulwahn@41907
   194
              in if hl' = 2+hr then l_bal(n,l',r)
bulwahn@41907
   195
                 else MKT n l' r (1 + max hl' hr)
bulwahn@41907
   196
         else let r' = insrt x r; hl = ht l; hr' = ht r'
bulwahn@41907
   197
              in if hr' = 2+hl then r_bal(n,l,r')
bulwahn@41907
   198
                 else MKT n l r' (1 + max hl hr'))"
bulwahn@41907
   199
bulwahn@41907
   200
bulwahn@41907
   201
subsubsection {* Necessary setup for code generation *}
bulwahn@41907
   202
bulwahn@41907
   203
primrec set_of'
bulwahn@41907
   204
where 
bulwahn@41907
   205
  "set_of' ET = []"
bulwahn@41907
   206
| "set_of' (MKT n l r h) = n # (set_of' l @ set_of' r)"
bulwahn@41907
   207
bulwahn@41907
   208
lemma set_of':
bulwahn@41907
   209
  "set (set_of' t) = set_of t"
bulwahn@41907
   210
by (induct t) auto
bulwahn@41907
   211
bulwahn@41907
   212
lemma is_ord_mkt:
bulwahn@41907
   213
  "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
   214
by (simp add: set_of')
bulwahn@41907
   215
bulwahn@41907
   216
declare is_ord.simps(1)[code] is_ord_mkt[code]
bulwahn@41907
   217
bulwahn@41907
   218
subsubsection {* Invalid Lemma due to typo in lbal *}
bulwahn@41907
   219
bulwahn@41907
   220
lemma is_ord_l_bal:
bulwahn@41907
   221
 "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
bulwahn@42184
   222
quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, timeout = 1000, expect = counterexample]
bulwahn@41907
   223
oops
bulwahn@41907
   224
bulwahn@41907
   225
bulwahn@41907
   226
end