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