src/HOL/Library/Quickcheck_Narrowing.thy
author bulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42316 12635bb655fd
parent 42024 51df23535105
child 42980 859fe9cc0838
permissions -rw-r--r--
deactivating other compilations in quickcheck_exhaustive momentarily that only interesting for my benchmarks and experiments
     1 (* Author: Lukas Bulwahn, TU Muenchen *)
     2 
     3 header {* Counterexample generator preforming narrowing-based testing *}
     4 
     5 theory Quickcheck_Narrowing
     6 imports Main "~~/src/HOL/Library/Code_Char"
     7 uses
     8   ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
     9 begin
    10 
    11 subsection {* Counterexample generator *}
    12 
    13 subsubsection {* Code generation setup *}
    14 
    15 code_type typerep
    16   ("Haskell" "Typerep")
    17 
    18 code_const Typerep.Typerep
    19   ("Haskell" "Typerep")
    20 
    21 code_reserved Haskell Typerep
    22 
    23 subsubsection {* Type @{text "code_int"} for Haskell's Int type *}
    24 
    25 typedef (open) code_int = "UNIV \<Colon> int set"
    26   morphisms int_of of_int by rule
    27 
    28 lemma of_int_int_of [simp]:
    29   "of_int (int_of k) = k"
    30   by (rule int_of_inverse)
    31 
    32 lemma int_of_of_int [simp]:
    33   "int_of (of_int n) = n"
    34   by (rule of_int_inverse) (rule UNIV_I)
    35 
    36 lemma code_int:
    37   "(\<And>n\<Colon>code_int. PROP P n) \<equiv> (\<And>n\<Colon>int. PROP P (of_int n))"
    38 proof
    39   fix n :: int
    40   assume "\<And>n\<Colon>code_int. PROP P n"
    41   then show "PROP P (of_int n)" .
    42 next
    43   fix n :: code_int
    44   assume "\<And>n\<Colon>int. PROP P (of_int n)"
    45   then have "PROP P (of_int (int_of n))" .
    46   then show "PROP P n" by simp
    47 qed
    48 
    49 
    50 lemma int_of_inject [simp]:
    51   "int_of k = int_of l \<longleftrightarrow> k = l"
    52   by (rule int_of_inject)
    53 
    54 lemma of_int_inject [simp]:
    55   "of_int n = of_int m \<longleftrightarrow> n = m"
    56   by (rule of_int_inject) (rule UNIV_I)+
    57 
    58 instantiation code_int :: equal
    59 begin
    60 
    61 definition
    62   "HOL.equal k l \<longleftrightarrow> HOL.equal (int_of k) (int_of l)"
    63 
    64 instance proof
    65 qed (auto simp add: equal_code_int_def equal_int_def eq_int_refl)
    66 
    67 end
    68 
    69 instantiation code_int :: number
    70 begin
    71 
    72 definition
    73   "number_of = of_int"
    74 
    75 instance ..
    76 
    77 end
    78 
    79 lemma int_of_number [simp]:
    80   "int_of (number_of k) = number_of k"
    81   by (simp add: number_of_code_int_def number_of_is_id)
    82 
    83 
    84 definition nat_of :: "code_int => nat"
    85 where
    86   "nat_of i = nat (int_of i)"
    87 
    88 instantiation code_int :: "{minus, linordered_semidom, semiring_div, linorder}"
    89 begin
    90 
    91 definition [simp, code del]:
    92   "0 = of_int 0"
    93 
    94 definition [simp, code del]:
    95   "1 = of_int 1"
    96 
    97 definition [simp, code del]:
    98   "n + m = of_int (int_of n + int_of m)"
    99 
   100 definition [simp, code del]:
   101   "n - m = of_int (int_of n - int_of m)"
   102 
   103 definition [simp, code del]:
   104   "n * m = of_int (int_of n * int_of m)"
   105 
   106 definition [simp, code del]:
   107   "n div m = of_int (int_of n div int_of m)"
   108 
   109 definition [simp, code del]:
   110   "n mod m = of_int (int_of n mod int_of m)"
   111 
   112 definition [simp, code del]:
   113   "n \<le> m \<longleftrightarrow> int_of n \<le> int_of m"
   114 
   115 definition [simp, code del]:
   116   "n < m \<longleftrightarrow> int_of n < int_of m"
   117 
   118 
   119 instance proof
   120 qed (auto simp add: code_int left_distrib zmult_zless_mono2)
   121 
   122 end
   123 (*
   124 lemma zero_code_int_code [code, code_unfold]:
   125   "(0\<Colon>code_int) = Numeral0"
   126   by (simp add: number_of_code_numeral_def Pls_def)
   127 lemma [code_post]: "Numeral0 = (0\<Colon>code_numeral)"
   128   using zero_code_numeral_code ..
   129 
   130 lemma one_code_numeral_code [code, code_unfold]:
   131   "(1\<Colon>code_int) = Numeral1"
   132   by (simp add: number_of_code_numeral_def Pls_def Bit1_def)
   133 lemma [code_post]: "Numeral1 = (1\<Colon>code_int)"
   134   using one_code_numeral_code ..
   135 *)
   136 
   137 definition div_mod_code_int :: "code_int \<Rightarrow> code_int \<Rightarrow> code_int \<times> code_int" where
   138   [code del]: "div_mod_code_int n m = (n div m, n mod m)"
   139 
   140 lemma [code]:
   141   "div_mod_code_int n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   142   unfolding div_mod_code_int_def by auto
   143 
   144 lemma [code]:
   145   "n div m = fst (div_mod_code_int n m)"
   146   unfolding div_mod_code_int_def by simp
   147 
   148 lemma [code]:
   149   "n mod m = snd (div_mod_code_int n m)"
   150   unfolding div_mod_code_int_def by simp
   151 
   152 lemma int_of_code [code]:
   153   "int_of k = (if k = 0 then 0
   154     else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
   155 proof -
   156   have 1: "(int_of k div 2) * 2 + int_of k mod 2 = int_of k" 
   157     by (rule mod_div_equality)
   158   have "int_of k mod 2 = 0 \<or> int_of k mod 2 = 1" by auto
   159   from this show ?thesis
   160     apply auto
   161     apply (insert 1) by (auto simp add: mult_ac)
   162 qed
   163 
   164 
   165 code_instance code_numeral :: equal
   166   (Haskell -)
   167 
   168 setup {* fold (Numeral.add_code @{const_name number_code_int_inst.number_of_code_int}
   169   false Code_Printer.literal_numeral) ["Haskell"]  *}
   170 
   171 code_const "0 \<Colon> code_int"
   172   (Haskell "0")
   173 
   174 code_const "1 \<Colon> code_int"
   175   (Haskell "1")
   176 
   177 code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int"
   178   (Haskell "(_/ -/ _)")
   179 
   180 code_const div_mod_code_int
   181   (Haskell "divMod")
   182 
   183 code_const "HOL.equal \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
   184   (Haskell infix 4 "==")
   185 
   186 code_const "op \<le> \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
   187   (Haskell infix 4 "<=")
   188 
   189 code_const "op < \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
   190   (Haskell infix 4 "<")
   191 
   192 code_type code_int
   193   (Haskell "Int")
   194 
   195 code_abort of_int
   196 
   197 subsubsection {* Narrowing's deep representation of types and terms *}
   198 
   199 datatype type = SumOfProd "type list list"
   200 
   201 datatype "term" = Var "code_int list" type | Ctr code_int "term list"
   202 
   203 datatype 'a cons = C type "(term list => 'a) list"
   204 
   205 subsubsection {* Auxilary functions for Narrowing *}
   206 
   207 consts nth :: "'a list => code_int => 'a"
   208 
   209 code_const nth ("Haskell" infixl 9  "!!")
   210 
   211 consts error :: "char list => 'a"
   212 
   213 code_const error ("Haskell" "error")
   214 
   215 consts toEnum :: "code_int => char"
   216 
   217 code_const toEnum ("Haskell" "toEnum")
   218 
   219 consts map_index :: "(code_int * 'a => 'b) => 'a list => 'b list"  
   220 
   221 consts split_At :: "code_int => 'a list => 'a list * 'a list"
   222  
   223 subsubsection {* Narrowing's basic operations *}
   224 
   225 type_synonym 'a narrowing = "code_int => 'a cons"
   226 
   227 definition empty :: "'a narrowing"
   228 where
   229   "empty d = C (SumOfProd []) []"
   230   
   231 definition cons :: "'a => 'a narrowing"
   232 where
   233   "cons a d = (C (SumOfProd [[]]) [(%_. a)])"
   234 
   235 fun conv :: "(term list => 'a) list => term => 'a"
   236 where
   237   "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum p)"
   238 | "conv cs (Ctr i xs) = (nth cs i) xs"
   239 
   240 fun nonEmpty :: "type => bool"
   241 where
   242   "nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
   243 
   244 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
   245 where
   246   "apply f a d =
   247      (case f d of C (SumOfProd ps) cfs =>
   248        case a (d - 1) of C ta cas =>
   249        let
   250          shallow = (d > 0 \<and> nonEmpty ta);
   251          cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
   252        in C (SumOfProd [ta # p. shallow, p <- ps]) cs)"
   253 
   254 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
   255 where
   256   "sum a b d =
   257     (case a d of C (SumOfProd ssa) ca => 
   258       case b d of C (SumOfProd ssb) cb =>
   259       C (SumOfProd (ssa @ ssb)) (ca @ cb))"
   260 
   261 lemma [fundef_cong]:
   262   assumes "a d = a' d" "b d = b' d" "d = d'"
   263   shows "sum a b d = sum a' b' d'"
   264 using assms unfolding sum_def by (auto split: cons.split type.split)
   265 
   266 lemma [fundef_cong]:
   267   assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')"
   268   assumes "d = d'"
   269   shows "apply f a d = apply f' a' d'"
   270 proof -
   271   note assms moreover
   272   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)))"
   273     by (simp add: of_int_inverse)
   274   moreover
   275   have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'"
   276     by (simp add: of_int_inverse)
   277   ultimately show ?thesis
   278     unfolding apply_def by (auto split: cons.split type.split simp add: Let_def)
   279 qed
   280 
   281 type_synonym pos = "code_int list"
   282 (*
   283 subsubsection {* Term refinement *}
   284 
   285 definition new :: "pos => type list list => term list"
   286 where
   287   "new p ps = map_index (%(c, ts). Ctr c (map_index (%(i, t). Var (p @ [i]) t) ts)) ps"
   288 
   289 fun refine :: "term => pos => term list" and refineList :: "term list => pos => (term list) list"
   290 where
   291   "refine (Var p (SumOfProd ss)) [] = new p ss"
   292 | "refine (Ctr c xs) p = map (Ctr c) (refineList xs p)"
   293 | "refineList xs (i # is) = (let (ls, xrs) = split_At i xs in (case xrs of x#rs => [ls @ y # rs. y <- refine x is]))"
   294 
   295 text {* Find total instantiations of a partial value *}
   296 
   297 function total :: "term => term list"
   298 where
   299   "total (Ctr c xs) = [Ctr c ys. ys <- map total xs]"
   300 | "total (Var p (SumOfProd ss)) = [y. x <- new p ss, y <- total x]"
   301 by pat_completeness auto
   302 
   303 termination sorry
   304 *)
   305 subsubsection {* Narrowing generator type class *}
   306 
   307 class narrowing =
   308   fixes narrowing :: "code_int => 'a cons"
   309 
   310 definition cons1 :: "('a::narrowing => 'b) => 'b narrowing"
   311 where
   312   "cons1 f = apply (cons f) narrowing"
   313 
   314 definition cons2 :: "('a :: narrowing => 'b :: narrowing => 'c) => 'c narrowing"
   315 where
   316   "cons2 f = apply (apply (cons f) narrowing) narrowing"
   317 
   318 definition drawn_from :: "'a list => 'a cons"
   319 where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
   320 
   321 instantiation int :: narrowing
   322 begin
   323 
   324 definition
   325   "narrowing_int d = (let i = Quickcheck_Narrowing.int_of d in drawn_from [-i .. i])"
   326 
   327 instance ..
   328 
   329 end
   330 
   331 instantiation unit :: narrowing
   332 begin
   333 
   334 definition
   335   "narrowing = cons ()"
   336 
   337 instance ..
   338 
   339 end
   340 
   341 instantiation bool :: narrowing
   342 begin
   343 
   344 definition
   345   "narrowing = sum (cons True) (cons False)" 
   346 
   347 instance ..
   348 
   349 end
   350 
   351 instantiation option :: (narrowing) narrowing
   352 begin
   353 
   354 definition
   355   "narrowing = sum (cons None) (cons1 Some)"
   356 
   357 instance ..
   358 
   359 end
   360 
   361 instantiation sum :: (narrowing, narrowing) narrowing
   362 begin
   363 
   364 definition
   365   "narrowing = sum (cons1 Inl) (cons1 Inr)"
   366 
   367 instance ..
   368 
   369 end
   370 
   371 instantiation list :: (narrowing) narrowing
   372 begin
   373 
   374 function narrowing_list :: "'a list narrowing"
   375 where
   376   "narrowing_list d = sum (cons []) (apply (apply (cons Cons) narrowing) narrowing_list) d"
   377 by pat_completeness auto
   378 
   379 termination proof (relation "measure nat_of")
   380 qed (auto simp add: of_int_inverse nat_of_def)
   381     
   382 instance ..
   383 
   384 end
   385 
   386 instantiation nat :: narrowing
   387 begin
   388 
   389 function narrowing_nat :: "nat narrowing"
   390 where
   391   "narrowing_nat d = sum (cons 0) (apply (cons Suc) narrowing_nat) d"
   392 by pat_completeness auto
   393 
   394 termination proof (relation "measure nat_of")
   395 qed (auto simp add: of_int_inverse nat_of_def)
   396 
   397 instance ..
   398 
   399 end
   400 
   401 instantiation Enum.finite_1 :: narrowing
   402 begin
   403 
   404 definition narrowing_finite_1 :: "Enum.finite_1 narrowing"
   405 where
   406   "narrowing_finite_1 = cons (Enum.finite_1.a\<^isub>1 :: Enum.finite_1)"
   407 
   408 instance ..
   409 
   410 end
   411 
   412 instantiation Enum.finite_2 :: narrowing
   413 begin
   414 
   415 definition narrowing_finite_2 :: "Enum.finite_2 narrowing"
   416 where
   417   "narrowing_finite_2 = sum (cons (Enum.finite_2.a\<^isub>1 :: Enum.finite_2)) (cons (Enum.finite_2.a\<^isub>2 :: Enum.finite_2))"
   418 
   419 instance ..
   420 
   421 end
   422 
   423 instantiation Enum.finite_3 :: narrowing
   424 begin
   425 
   426 definition narrowing_finite_3 :: "Enum.finite_3 narrowing"
   427 where
   428   "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)))"
   429 
   430 instance ..
   431 
   432 end
   433 
   434 instantiation Enum.finite_4 :: narrowing
   435 begin
   436 
   437 definition narrowing_finite_4 :: "Enum.finite_4 narrowing"
   438 where
   439   "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)))"
   440 
   441 instance ..
   442 
   443 end
   444 
   445 subsubsection {* class @{text is_testable} *}
   446 
   447 text {* The class @{text is_testable} ensures that all necessary type instances are generated. *}
   448 
   449 class is_testable
   450 
   451 instance bool :: is_testable ..
   452 
   453 instance "fun" :: ("{term_of, narrowing}", is_testable) is_testable ..
   454 
   455 definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
   456 where
   457   "ensure_testable f = f"
   458 
   459 declare simp_thms(17,19)[code del]
   460 
   461 subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
   462 
   463 datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
   464 
   465 primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
   466 where
   467   "eval_ffun (Constant c) x = c"
   468 | "eval_ffun (Update x' y f) x = (if x = x' then y else eval_ffun f x)"
   469 
   470 hide_type (open) ffun
   471 hide_const (open) Constant Update eval_ffun
   472 
   473 datatype 'b cfun = Constant 'b
   474 
   475 primrec eval_cfun :: "'b cfun => 'a => 'b"
   476 where
   477   "eval_cfun (Constant c) y = c"
   478 
   479 hide_type (open) cfun
   480 hide_const (open) Constant eval_cfun
   481 
   482 subsubsection {* Setting up the counterexample generator *}
   483   
   484 use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
   485 
   486 setup {* Narrowing_Generators.setup *}
   487 
   488 hide_type (open) code_int type "term" cons
   489 hide_const (open) int_of of_int nth error toEnum map_index split_At empty
   490   cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
   491 
   492 end