src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 58148 9764b994a421
child 58310 91ea607a34d8
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     1 (*  Title:      HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
     2     Author:     Lukas Bulwahn
     3     Copyright   2011 TU Muenchen
     4 *)
     5 
     6 header {* Examples for narrowing-based testing  *}
     7 
     8 theory Quickcheck_Narrowing_Examples
     9 imports Main
    10 begin
    11 
    12 declare [[quickcheck_timeout = 3600]]
    13 
    14 subsection {* Minimalistic examples *}
    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 {* Simple examples with existentials *}
    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 {* A false conjecture derived from an partial copy-n-paste of @{thm not_distinct_decomp} *}
    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 {* A false conjecture derived from theorems @{thm split_list_first} and @{thm split_list_last} *}  
    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 {* A false conjecture derived from @{thm map_eq_Cons_conv} with a typo *}
    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 {* Simple list examples *}
    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 {* Simple examples with functions *}
    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 {* Simple examples with inductive predicates *}
   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 {* AVL Trees *}
   134 
   135 datatype_new '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 {* Necessary setup for code generation *}
   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 {* Invalid Lemma due to typo in @{const l_bal} *}
   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 {* Examples with hd and last *}
   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 {* Examples with underspecified/partial functions *}
   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