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