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