src/HOL/Quickcheck_Narrowing.thy
author bulwahn
Thu Jun 09 09:07:13 2011 +0200 (2011-06-09)
changeset 43317 f9283eb3a4bf
parent 43316 3e274608f06b
child 43341 acdac535c7fa
permissions -rw-r--r--
fixing code generation test
     1 (* Author: Lukas Bulwahn, TU Muenchen *)
     2 
     3 header {* Counterexample generator preforming 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 subsubsection {* From narrowing's deep representation of terms to Code_Evaluation's terms *}
   222 
   223 class partial_term_of = typerep +
   224   fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"
   225 
   226 lemma partial_term_of_anything: "partial_term_of x nt \<equiv> t"
   227   by (rule eq_reflection) (cases "partial_term_of x nt", cases t, simp)
   228 
   229 
   230 subsubsection {* Auxilary functions for Narrowing *}
   231 
   232 consts nth :: "'a list => code_int => 'a"
   233 
   234 code_const nth (Haskell_Quickcheck infixl 9  "!!")
   235 
   236 consts error :: "char list => 'a"
   237 
   238 code_const error (Haskell_Quickcheck "error")
   239 
   240 consts toEnum :: "code_int => char"
   241 
   242 code_const toEnum (Haskell_Quickcheck "toEnum")
   243 
   244 consts marker :: "char"
   245 
   246 code_const marker (Haskell_Quickcheck "''\\0'")
   247 
   248 subsubsection {* Narrowing's basic operations *}
   249 
   250 type_synonym 'a narrowing = "code_int => 'a cons"
   251 
   252 definition empty :: "'a narrowing"
   253 where
   254   "empty d = C (SumOfProd []) []"
   255   
   256 definition cons :: "'a => 'a narrowing"
   257 where
   258   "cons a d = (C (SumOfProd [[]]) [(%_. a)])"
   259 
   260 fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
   261 where
   262   "conv cs (Var p _) = error (marker # map toEnum p)"
   263 | "conv cs (Ctr i xs) = (nth cs i) xs"
   264 
   265 fun nonEmpty :: "narrowing_type => bool"
   266 where
   267   "nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
   268 
   269 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
   270 where
   271   "apply f a d =
   272      (case f d of C (SumOfProd ps) cfs =>
   273        case a (d - 1) of C ta cas =>
   274        let
   275          shallow = (d > 0 \<and> nonEmpty ta);
   276          cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
   277        in C (SumOfProd [ta # p. shallow, p <- ps]) cs)"
   278 
   279 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
   280 where
   281   "sum a b d =
   282     (case a d of C (SumOfProd ssa) ca => 
   283       case b d of C (SumOfProd ssb) cb =>
   284       C (SumOfProd (ssa @ ssb)) (ca @ cb))"
   285 
   286 lemma [fundef_cong]:
   287   assumes "a d = a' d" "b d = b' d" "d = d'"
   288   shows "sum a b d = sum a' b' d'"
   289 using assms unfolding sum_def by (auto split: cons.split narrowing_type.split)
   290 
   291 lemma [fundef_cong]:
   292   assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')"
   293   assumes "d = d'"
   294   shows "apply f a d = apply f' a' d'"
   295 proof -
   296   note assms moreover
   297   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)))"
   298     by (simp add: of_int_inverse)
   299   moreover
   300   have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'"
   301     by (simp add: of_int_inverse)
   302   ultimately show ?thesis
   303     unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def)
   304 qed
   305 
   306 subsubsection {* Narrowing generator type class *}
   307 
   308 class narrowing =
   309   fixes narrowing :: "code_int => 'a cons"
   310 
   311 definition drawn_from :: "'a list => 'a cons"
   312 where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
   313 
   314 instantiation int :: narrowing
   315 begin
   316 
   317 definition
   318   "narrowing_int d = (let i = Quickcheck_Narrowing.int_of d in drawn_from [-i .. i])"
   319 
   320 instance ..
   321 
   322 end
   323 
   324 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
   325 
   326 (* FIXME: hard-wired maximal depth of 100 here *)
   327 definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
   328 where
   329   "exists f = (case narrowing (100 :: code_int) of C ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   330 
   331 definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
   332 where
   333   "all f = (case narrowing (100 :: code_int) of C ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   334 
   335 subsubsection {* class @{text is_testable} *}
   336 
   337 text {* The class @{text is_testable} ensures that all necessary type instances are generated. *}
   338 
   339 class is_testable
   340 
   341 instance bool :: is_testable ..
   342 
   343 instance "fun" :: ("{term_of, narrowing, partial_term_of}", is_testable) is_testable ..
   344 
   345 definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
   346 where
   347   "ensure_testable f = f"
   348 
   349 
   350 subsubsection {* Defining a simple datatype to represent functions in an incomplete and redundant way *}
   351 
   352 datatype ('a, 'b) ffun = Constant 'b | Update 'a 'b "('a, 'b) ffun"
   353 
   354 primrec eval_ffun :: "('a, 'b) ffun => 'a => 'b"
   355 where
   356   "eval_ffun (Constant c) x = c"
   357 | "eval_ffun (Update x' y f) x = (if x = x' then y else eval_ffun f x)"
   358 
   359 hide_type (open) ffun
   360 hide_const (open) Constant Update eval_ffun
   361 
   362 datatype 'b cfun = Constant 'b
   363 
   364 primrec eval_cfun :: "'b cfun => 'a => 'b"
   365 where
   366   "eval_cfun (Constant c) y = c"
   367 
   368 hide_type (open) cfun
   369 hide_const (open) Constant eval_cfun
   370 
   371 subsubsection {* Setting up the counterexample generator *}
   372 
   373 setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")) *}
   374 setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")) *}
   375 use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
   376 
   377 setup {* Narrowing_Generators.setup *}
   378 
   379 hide_type code_int narrowing_type narrowing_term cons property
   380 hide_const int_of of_int nth error toEnum marker empty
   381   C cons conv nonEmpty "apply" sum ensure_testable all exists 
   382 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
   383 
   384 end