src/HOL/Library/Quickcheck_Narrowing.thy
author bulwahn
Fri Mar 11 15:21:13 2011 +0100 (2011-03-11)
changeset 41930 1e008cc4883a
parent 41929 c3c8b14f480a
child 41943 12f24ad566ea
permissions -rw-r--r--
renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn@41905
     1
(* Author: Lukas Bulwahn, TU Muenchen *)
bulwahn@41905
     2
bulwahn@41930
     3
header {* Counterexample generator preforming narrowing-based testing *}
bulwahn@41905
     4
bulwahn@41930
     5
theory Quickcheck_Narrowing
bulwahn@41905
     6
imports Main "~~/src/HOL/Library/Code_Char"
bulwahn@41930
     7
uses ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
bulwahn@41905
     8
begin
bulwahn@41905
     9
bulwahn@41905
    10
subsection {* Counterexample generator *}
bulwahn@41905
    11
bulwahn@41909
    12
subsubsection {* Code generation setup *}
bulwahn@41909
    13
bulwahn@41909
    14
code_type typerep
bulwahn@41909
    15
  ("Haskell" "Typerep")
bulwahn@41909
    16
bulwahn@41909
    17
code_const Typerep.Typerep
bulwahn@41909
    18
  ("Haskell" "Typerep")
bulwahn@41909
    19
bulwahn@41909
    20
code_reserved Haskell Typerep
bulwahn@41909
    21
bulwahn@41908
    22
subsubsection {* Type code_int for Haskell's Int type *}
bulwahn@41908
    23
bulwahn@41908
    24
typedef (open) code_int = "UNIV \<Colon> int set"
bulwahn@41908
    25
  morphisms int_of of_int by rule
bulwahn@41908
    26
bulwahn@41908
    27
lemma int_of_inject [simp]:
bulwahn@41908
    28
  "int_of k = int_of l \<longleftrightarrow> k = l"
bulwahn@41908
    29
  by (rule int_of_inject)
bulwahn@41908
    30
bulwahn@41912
    31
definition nat_of :: "code_int => nat"
bulwahn@41912
    32
where
bulwahn@41912
    33
  "nat_of i = nat (int_of i)"
bulwahn@41908
    34
bulwahn@41908
    35
instantiation code_int :: "{zero, one, minus, linorder}"
bulwahn@41908
    36
begin
bulwahn@41908
    37
bulwahn@41908
    38
definition [simp, code del]:
bulwahn@41908
    39
  "0 = of_int 0"
bulwahn@41908
    40
bulwahn@41908
    41
definition [simp, code del]:
bulwahn@41908
    42
  "1 = of_int 1"
bulwahn@41908
    43
bulwahn@41908
    44
definition [simp, code del]:
bulwahn@41908
    45
  "n - m = of_int (int_of n - int_of m)"
bulwahn@41908
    46
bulwahn@41908
    47
definition [simp, code del]:
bulwahn@41908
    48
  "n \<le> m \<longleftrightarrow> int_of n \<le> int_of m"
bulwahn@41908
    49
bulwahn@41908
    50
definition [simp, code del]:
bulwahn@41908
    51
  "n < m \<longleftrightarrow> int_of n < int_of m"
bulwahn@41908
    52
bulwahn@41908
    53
bulwahn@41908
    54
instance proof qed (auto)
bulwahn@41908
    55
bulwahn@41908
    56
end
bulwahn@41908
    57
(*
bulwahn@41908
    58
lemma zero_code_int_code [code, code_unfold]:
bulwahn@41908
    59
  "(0\<Colon>code_int) = Numeral0"
bulwahn@41908
    60
  by (simp add: number_of_code_numeral_def Pls_def)
bulwahn@41908
    61
lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
bulwahn@41908
    62
  using zero_code_numeral_code ..
bulwahn@41908
    63
bulwahn@41908
    64
lemma one_code_numeral_code [code, code_unfold]:
bulwahn@41908
    65
  "(1\<Colon>code_int) = Numeral1"
bulwahn@41908
    66
  by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
bulwahn@41908
    67
lemma [code_post]: "Numeral1 = (1\<Colon>code_int)"
bulwahn@41908
    68
  using one_code_numeral_code ..
bulwahn@41908
    69
*)
bulwahn@41908
    70
bulwahn@41908
    71
code_const "0 \<Colon> code_int"
bulwahn@41908
    72
  (Haskell "0")
bulwahn@41908
    73
bulwahn@41908
    74
code_const "1 \<Colon> code_int"
bulwahn@41908
    75
  (Haskell "1")
bulwahn@41908
    76
bulwahn@41908
    77
code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int"
bulwahn@41908
    78
  (Haskell "(_/ -/ _)")
bulwahn@41908
    79
bulwahn@41908
    80
code_const "op \<le> \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
bulwahn@41908
    81
  (Haskell infix 4 "<=")
bulwahn@41908
    82
bulwahn@41908
    83
code_const "op < \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
bulwahn@41908
    84
  (Haskell infix 4 "<")
bulwahn@41908
    85
bulwahn@41908
    86
code_type code_int
bulwahn@41908
    87
  (Haskell "Int")
bulwahn@41908
    88
bulwahn@41905
    89
subsubsection {* LSC's deep representation of types of terms *}
bulwahn@41905
    90
bulwahn@41905
    91
datatype type = SumOfProd "type list list"
bulwahn@41905
    92
bulwahn@41908
    93
datatype "term" = Var "code_int list" type | Ctr code_int "term list"
bulwahn@41905
    94
bulwahn@41905
    95
datatype 'a cons = C type "(term list => 'a) list"
bulwahn@41905
    96
bulwahn@41905
    97
subsubsection {* auxilary functions for LSC *}
bulwahn@41905
    98
bulwahn@41908
    99
consts nth :: "'a list => code_int => 'a"
bulwahn@41905
   100
bulwahn@41908
   101
code_const nth ("Haskell" infixl 9  "!!")
bulwahn@41905
   102
bulwahn@41908
   103
consts error :: "char list => 'a"
bulwahn@41905
   104
bulwahn@41905
   105
code_const error ("Haskell" "error")
bulwahn@41905
   106
bulwahn@41908
   107
consts toEnum :: "code_int => char"
bulwahn@41908
   108
bulwahn@41908
   109
code_const toEnum ("Haskell" "toEnum")
bulwahn@41905
   110
bulwahn@41908
   111
consts map_index :: "(code_int * 'a => 'b) => 'a list => 'b list"  
bulwahn@41905
   112
bulwahn@41908
   113
consts split_At :: "code_int => 'a list => 'a list * 'a list"
bulwahn@41908
   114
 
bulwahn@41905
   115
subsubsection {* LSC's basic operations *}
bulwahn@41905
   116
bulwahn@41908
   117
type_synonym 'a series = "code_int => 'a cons"
bulwahn@41905
   118
bulwahn@41905
   119
definition empty :: "'a series"
bulwahn@41905
   120
where
bulwahn@41905
   121
  "empty d = C (SumOfProd []) []"
bulwahn@41905
   122
  
bulwahn@41905
   123
definition cons :: "'a => 'a series"
bulwahn@41905
   124
where
bulwahn@41905
   125
  "cons a d = (C (SumOfProd [[]]) [(%_. a)])"
bulwahn@41905
   126
bulwahn@41905
   127
fun conv :: "(term list => 'a) list => term => 'a"
bulwahn@41905
   128
where
bulwahn@41908
   129
  "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum p)"
bulwahn@41905
   130
| "conv cs (Ctr i xs) = (nth cs i) xs"
bulwahn@41905
   131
bulwahn@41905
   132
fun nonEmpty :: "type => bool"
bulwahn@41905
   133
where
bulwahn@41905
   134
  "nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
bulwahn@41905
   135
bulwahn@41905
   136
definition "apply" :: "('a => 'b) series => 'a series => 'b series"
bulwahn@41905
   137
where
bulwahn@41905
   138
  "apply f a d =
bulwahn@41905
   139
     (case f d of C (SumOfProd ps) cfs =>
bulwahn@41905
   140
       case a (d - 1) of C ta cas =>
bulwahn@41905
   141
       let
bulwahn@41905
   142
         shallow = (d > 0 \<and> nonEmpty ta);
bulwahn@41905
   143
         cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
bulwahn@41905
   144
       in C (SumOfProd [ta # p. shallow, p <- ps]) cs)"
bulwahn@41905
   145
bulwahn@41905
   146
definition sum :: "'a series => 'a series => 'a series"
bulwahn@41905
   147
where
bulwahn@41905
   148
  "sum a b d =
bulwahn@41905
   149
    (case a d of C (SumOfProd ssa) ca => 
bulwahn@41905
   150
      case b d of C (SumOfProd ssb) cb =>
bulwahn@41905
   151
      C (SumOfProd (ssa @ ssb)) (ca @ cb))"
bulwahn@41905
   152
bulwahn@41912
   153
lemma [fundef_cong]:
bulwahn@41912
   154
  assumes "a d = a' d" "b d = b' d" "d = d'"
bulwahn@41912
   155
  shows "sum a b d = sum a' b' d'"
bulwahn@41912
   156
using assms unfolding sum_def by (auto split: cons.split type.split)
bulwahn@41912
   157
bulwahn@41912
   158
lemma [fundef_cong]:
bulwahn@41912
   159
  assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')"
bulwahn@41912
   160
  assumes "d = d'"
bulwahn@41912
   161
  shows "apply f a d = apply f' a' d'"
bulwahn@41912
   162
proof -
bulwahn@41912
   163
  note assms moreover
bulwahn@41930
   164
  have "int_of (of_int 0) < int_of d' ==> int_of (of_int 0) <= int_of (of_int (int_of d' - int_of (of_int 1)))"
bulwahn@41912
   165
    by (simp add: of_int_inverse)
bulwahn@41912
   166
  moreover
bulwahn@41930
   167
  have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'"
bulwahn@41912
   168
    by (simp add: of_int_inverse)
bulwahn@41912
   169
  ultimately show ?thesis
bulwahn@41912
   170
    unfolding apply_def by (auto split: cons.split type.split simp add: Let_def)
bulwahn@41912
   171
qed
bulwahn@41912
   172
bulwahn@41905
   173
definition cons0 :: "'a => 'a series"
bulwahn@41905
   174
where
bulwahn@41905
   175
  "cons0 f = cons f"
bulwahn@41905
   176
bulwahn@41908
   177
type_synonym pos = "code_int list"
bulwahn@41912
   178
(*
bulwahn@41908
   179
subsubsection {* Term refinement *}
bulwahn@41908
   180
bulwahn@41908
   181
definition new :: "pos => type list list => term list"
bulwahn@41908
   182
where
bulwahn@41908
   183
  "new p ps = map_index (%(c, ts). Ctr c (map_index (%(i, t). Var (p @ [i]) t) ts)) ps"
bulwahn@41908
   184
bulwahn@41908
   185
fun refine :: "term => pos => term list" and refineList :: "term list => pos => (term list) list"
bulwahn@41908
   186
where
bulwahn@41908
   187
  "refine (Var p (SumOfProd ss)) [] = new p ss"
bulwahn@41908
   188
| "refine (Ctr c xs) p = map (Ctr c) (refineList xs p)"
bulwahn@41908
   189
| "refineList xs (i # is) = (let (ls, xrs) = split_At i xs in (case xrs of x#rs => [ls @ y # rs. y <- refine x is]))"
bulwahn@41908
   190
bulwahn@41908
   191
text {* Find total instantiations of a partial value *}
bulwahn@41908
   192
bulwahn@41908
   193
function total :: "term => term list"
bulwahn@41908
   194
where
bulwahn@41908
   195
  "total (Ctr c xs) = [Ctr c ys. ys <- map total xs]"
bulwahn@41908
   196
| "total (Var p (SumOfProd ss)) = [y. x <- new p ss, y <- total x]"
bulwahn@41908
   197
by pat_completeness auto
bulwahn@41908
   198
bulwahn@41908
   199
termination sorry
bulwahn@41912
   200
*)
bulwahn@41905
   201
subsubsection {* LSC's type class for enumeration *}
bulwahn@41905
   202
bulwahn@41905
   203
class serial =
bulwahn@41908
   204
  fixes series :: "code_int => 'a cons"
bulwahn@41905
   205
bulwahn@41905
   206
definition cons1 :: "('a::serial => 'b) => 'b series"
bulwahn@41905
   207
where
bulwahn@41905
   208
  "cons1 f = apply (cons f) series"
bulwahn@41905
   209
bulwahn@41905
   210
definition cons2 :: "('a :: serial => 'b :: serial => 'c) => 'c series"
bulwahn@41905
   211
where
bulwahn@41905
   212
  "cons2 f = apply (apply (cons f) series) series"
bulwahn@41905
   213
  
bulwahn@41905
   214
instantiation unit :: serial
bulwahn@41905
   215
begin
bulwahn@41905
   216
bulwahn@41905
   217
definition
bulwahn@41905
   218
  "series = cons0 ()"
bulwahn@41905
   219
bulwahn@41905
   220
instance ..
bulwahn@41905
   221
bulwahn@41905
   222
end
bulwahn@41905
   223
bulwahn@41905
   224
instantiation bool :: serial
bulwahn@41905
   225
begin
bulwahn@41905
   226
bulwahn@41905
   227
definition
bulwahn@41905
   228
  "series = sum (cons0 True) (cons0 False)" 
bulwahn@41905
   229
bulwahn@41905
   230
instance ..
bulwahn@41905
   231
bulwahn@41905
   232
end
bulwahn@41905
   233
bulwahn@41905
   234
instantiation option :: (serial) serial
bulwahn@41905
   235
begin
bulwahn@41905
   236
bulwahn@41905
   237
definition
bulwahn@41905
   238
  "series = sum (cons0 None) (cons1 Some)"
bulwahn@41905
   239
bulwahn@41905
   240
instance ..
bulwahn@41905
   241
bulwahn@41905
   242
end
bulwahn@41905
   243
bulwahn@41905
   244
instantiation sum :: (serial, serial) serial
bulwahn@41905
   245
begin
bulwahn@41905
   246
bulwahn@41905
   247
definition
bulwahn@41905
   248
  "series = sum (cons1 Inl) (cons1 Inr)"
bulwahn@41905
   249
bulwahn@41905
   250
instance ..
bulwahn@41905
   251
bulwahn@41905
   252
end
bulwahn@41905
   253
bulwahn@41905
   254
instantiation list :: (serial) serial
bulwahn@41905
   255
begin
bulwahn@41905
   256
bulwahn@41905
   257
function series_list :: "'a list series"
bulwahn@41905
   258
where
bulwahn@41905
   259
  "series_list d = sum (cons []) (apply (apply (cons Cons) series) series_list) d"
bulwahn@41905
   260
by pat_completeness auto
bulwahn@41905
   261
bulwahn@41912
   262
termination proof (relation "measure nat_of")
bulwahn@41912
   263
qed (auto simp add: of_int_inverse nat_of_def)
bulwahn@41912
   264
    
bulwahn@41905
   265
instance ..
bulwahn@41905
   266
bulwahn@41905
   267
end
bulwahn@41905
   268
bulwahn@41905
   269
instantiation nat :: serial
bulwahn@41905
   270
begin
bulwahn@41905
   271
bulwahn@41905
   272
function series_nat :: "nat series"
bulwahn@41905
   273
where
bulwahn@41905
   274
  "series_nat d = sum (cons 0) (apply (cons Suc) series_nat) d"
bulwahn@41905
   275
by pat_completeness auto
bulwahn@41905
   276
bulwahn@41912
   277
termination proof (relation "measure nat_of")
bulwahn@41912
   278
qed (auto simp add: of_int_inverse nat_of_def)
bulwahn@41905
   279
bulwahn@41905
   280
instance ..
bulwahn@41905
   281
bulwahn@41905
   282
end
bulwahn@41905
   283
bulwahn@41905
   284
instantiation Enum.finite_1 :: serial
bulwahn@41905
   285
begin
bulwahn@41905
   286
bulwahn@41905
   287
definition series_finite_1 :: "Enum.finite_1 series"
bulwahn@41905
   288
where
bulwahn@41905
   289
  "series_finite_1 = cons (Enum.finite_1.a\<^isub>1 :: Enum.finite_1)"
bulwahn@41905
   290
bulwahn@41905
   291
instance ..
bulwahn@41905
   292
bulwahn@41905
   293
end
bulwahn@41905
   294
bulwahn@41905
   295
instantiation Enum.finite_2 :: serial
bulwahn@41905
   296
begin
bulwahn@41905
   297
bulwahn@41905
   298
definition series_finite_2 :: "Enum.finite_2 series"
bulwahn@41905
   299
where
bulwahn@41905
   300
  "series_finite_2 = sum (cons (Enum.finite_2.a\<^isub>1 :: Enum.finite_2)) (cons (Enum.finite_2.a\<^isub>2 :: Enum.finite_2))"
bulwahn@41905
   301
bulwahn@41905
   302
instance ..
bulwahn@41905
   303
bulwahn@41905
   304
end
bulwahn@41905
   305
bulwahn@41905
   306
instantiation Enum.finite_3 :: serial
bulwahn@41905
   307
begin
bulwahn@41905
   308
bulwahn@41905
   309
definition series_finite_3 :: "Enum.finite_3 series"
bulwahn@41905
   310
where
bulwahn@41905
   311
  "series_finite_3 = sum (cons (Enum.finite_3.a\<^isub>1 :: Enum.finite_3)) (sum (cons (Enum.finite_3.a\<^isub>2 :: Enum.finite_3)) (cons (Enum.finite_3.a\<^isub>3 :: Enum.finite_3)))"
bulwahn@41905
   312
bulwahn@41905
   313
instance ..
bulwahn@41905
   314
bulwahn@41905
   315
end
bulwahn@41905
   316
bulwahn@41910
   317
instantiation Enum.finite_4 :: serial
bulwahn@41910
   318
begin
bulwahn@41910
   319
bulwahn@41910
   320
definition series_finite_4 :: "Enum.finite_4 series"
bulwahn@41910
   321
where
bulwahn@41910
   322
  "series_finite_4 = sum (cons Enum.finite_4.a\<^isub>1) (sum (cons Enum.finite_4.a\<^isub>2) (sum (cons Enum.finite_4.a\<^isub>3) (cons Enum.finite_4.a\<^isub>4)))"
bulwahn@41910
   323
bulwahn@41910
   324
instance ..
bulwahn@41910
   325
bulwahn@41910
   326
end
bulwahn@41910
   327
bulwahn@41905
   328
subsubsection {* class is_testable *}
bulwahn@41905
   329
bulwahn@41905
   330
text {* The class is_testable ensures that all necessary type instances are generated. *}
bulwahn@41905
   331
bulwahn@41905
   332
class is_testable
bulwahn@41905
   333
bulwahn@41905
   334
instance bool :: is_testable ..
bulwahn@41905
   335
bulwahn@41905
   336
instance "fun" :: ("{term_of, serial}", is_testable) is_testable ..
bulwahn@41905
   337
bulwahn@41905
   338
definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
bulwahn@41905
   339
where
bulwahn@41905
   340
  "ensure_testable f = f"
bulwahn@41905
   341
bulwahn@41910
   342
declare simp_thms(17,19)[code del]
bulwahn@41910
   343
bulwahn@41905
   344
subsubsection {* Setting up the counterexample generator *}
bulwahn@41905
   345
  
bulwahn@41930
   346
use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
bulwahn@41905
   347
bulwahn@41930
   348
setup {* Narrowing_Generators.setup *}
bulwahn@41905
   349
bulwahn@41908
   350
hide_const (open) empty
bulwahn@41908
   351
bulwahn@41905
   352
end