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