src/HOL/Quickcheck_Narrowing.thy
changeset 51143 0a2371e7ced3
parent 50046 0051dc4f301f
child 52435 6646bb548c6b
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -9,188 +9,26 @@
     1.4  
     1.5  subsection {* Counterexample generator *}
     1.6  
     1.7 -text {* We create a new target for the necessary code generation setup. *}
     1.8 +subsubsection {* Code generation setup *}
     1.9  
    1.10  setup {* Code_Target.extend_target ("Haskell_Quickcheck", (Code_Haskell.target, K I)) *}
    1.11  
    1.12 -subsubsection {* Code generation setup *}
    1.13 -
    1.14  code_type typerep
    1.15    (Haskell_Quickcheck "Typerep")
    1.16  
    1.17  code_const Typerep.Typerep
    1.18    (Haskell_Quickcheck "Typerep")
    1.19  
    1.20 +code_type integer
    1.21 +  (Haskell_Quickcheck "Prelude.Int")
    1.22 +
    1.23  code_reserved Haskell_Quickcheck Typerep
    1.24  
    1.25 -subsubsection {* Type @{text "code_int"} for Haskell Quickcheck's Int type *}
    1.26 -
    1.27 -typedef code_int = "UNIV \<Colon> int set"
    1.28 -  morphisms int_of of_int by rule
    1.29 -
    1.30 -lemma of_int_int_of [simp]:
    1.31 -  "of_int (int_of k) = k"
    1.32 -  by (rule int_of_inverse)
    1.33 -
    1.34 -lemma int_of_of_int [simp]:
    1.35 -  "int_of (of_int n) = n"
    1.36 -  by (rule of_int_inverse) (rule UNIV_I)
    1.37 -
    1.38 -lemma code_int:
    1.39 -  "(\<And>n\<Colon>code_int. PROP P n) \<equiv> (\<And>n\<Colon>int. PROP P (of_int n))"
    1.40 -proof
    1.41 -  fix n :: int
    1.42 -  assume "\<And>n\<Colon>code_int. PROP P n"
    1.43 -  then show "PROP P (of_int n)" .
    1.44 -next
    1.45 -  fix n :: code_int
    1.46 -  assume "\<And>n\<Colon>int. PROP P (of_int n)"
    1.47 -  then have "PROP P (of_int (int_of n))" .
    1.48 -  then show "PROP P n" by simp
    1.49 -qed
    1.50 -
    1.51 -
    1.52 -lemma int_of_inject [simp]:
    1.53 -  "int_of k = int_of l \<longleftrightarrow> k = l"
    1.54 -  by (rule int_of_inject)
    1.55 -
    1.56 -lemma of_int_inject [simp]:
    1.57 -  "of_int n = of_int m \<longleftrightarrow> n = m"
    1.58 -  by (rule of_int_inject) (rule UNIV_I)+
    1.59 -
    1.60 -instantiation code_int :: equal
    1.61 -begin
    1.62 -
    1.63 -definition
    1.64 -  "HOL.equal k l \<longleftrightarrow> HOL.equal (int_of k) (int_of l)"
    1.65 -
    1.66 -instance proof
    1.67 -qed (auto simp add: equal_code_int_def equal_int_def equal_int_refl)
    1.68 -
    1.69 -end
    1.70 -
    1.71 -definition nat_of :: "code_int => nat"
    1.72 -where
    1.73 -  "nat_of i = nat (int_of i)"
    1.74 -  
    1.75 -instantiation code_int :: "{minus, linordered_semidom, semiring_div, neg_numeral, linorder}"
    1.76 -begin
    1.77 -
    1.78 -definition [simp, code del]:
    1.79 -  "0 = of_int 0"
    1.80 -
    1.81 -definition [simp, code del]:
    1.82 -  "1 = of_int 1"
    1.83 -
    1.84 -definition [simp, code del]:
    1.85 -  "n + m = of_int (int_of n + int_of m)"
    1.86 -
    1.87 -definition [simp, code del]:
    1.88 -  "- n = of_int (- int_of n)"
    1.89 -
    1.90 -definition [simp, code del]:
    1.91 -  "n - m = of_int (int_of n - int_of m)"
    1.92 -
    1.93 -definition [simp, code del]:
    1.94 -  "n * m = of_int (int_of n * int_of m)"
    1.95 -
    1.96 -definition [simp, code del]:
    1.97 -  "n div m = of_int (int_of n div int_of m)"
    1.98 -
    1.99 -definition [simp, code del]:
   1.100 -  "n mod m = of_int (int_of n mod int_of m)"
   1.101 -
   1.102 -definition [simp, code del]:
   1.103 -  "n \<le> m \<longleftrightarrow> int_of n \<le> int_of m"
   1.104 -
   1.105 -definition [simp, code del]:
   1.106 -  "n < m \<longleftrightarrow> int_of n < int_of m"
   1.107 -
   1.108 -instance proof
   1.109 -qed (auto simp add: code_int distrib_right zmult_zless_mono2)
   1.110 -
   1.111 -end
   1.112 -
   1.113 -lemma int_of_numeral [simp]:
   1.114 -  "int_of (numeral k) = numeral k"
   1.115 -  by (induct k) (simp_all only: numeral.simps plus_code_int_def
   1.116 -    one_code_int_def of_int_inverse UNIV_I)
   1.117 -
   1.118 -definition Num :: "num \<Rightarrow> code_int"
   1.119 -  where [code_abbrev]: "Num = numeral"
   1.120 -
   1.121 -lemma [code_abbrev]:
   1.122 -  "- numeral k = (neg_numeral k :: code_int)"
   1.123 -  by (unfold neg_numeral_def) simp
   1.124 -
   1.125 -code_datatype "0::code_int" Num
   1.126 -
   1.127 -lemma one_code_int_code [code, code_unfold]:
   1.128 -  "(1\<Colon>code_int) = Numeral1"
   1.129 -  by (simp only: numeral.simps)
   1.130 -
   1.131 -definition div_mod :: "code_int \<Rightarrow> code_int \<Rightarrow> code_int \<times> code_int" where
   1.132 -  [code del]: "div_mod n m = (n div m, n mod m)"
   1.133 -
   1.134 -lemma [code]:
   1.135 -  "n div m = fst (div_mod n m)"
   1.136 -  unfolding div_mod_def by simp
   1.137 -
   1.138 -lemma [code]:
   1.139 -  "n mod m = snd (div_mod n m)"
   1.140 -  unfolding div_mod_def by simp
   1.141 -
   1.142 -lemma int_of_code [code]:
   1.143 -  "int_of k = (if k = 0 then 0
   1.144 -    else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
   1.145 -proof -
   1.146 -  have 1: "(int_of k div 2) * 2 + int_of k mod 2 = int_of k" 
   1.147 -    by (rule mod_div_equality)
   1.148 -  have "int_of k mod 2 = 0 \<or> int_of k mod 2 = 1" by auto
   1.149 -  from this show ?thesis
   1.150 -    apply auto
   1.151 -    apply (insert 1) by (auto simp add: mult_ac)
   1.152 -qed
   1.153 -
   1.154 -
   1.155 -code_instance code_numeral :: equal
   1.156 -  (Haskell_Quickcheck -)
   1.157 -
   1.158 -setup {* fold (Numeral.add_code @{const_name Num}
   1.159 -  false Code_Printer.literal_numeral) ["Haskell_Quickcheck"]  *}
   1.160 -
   1.161 -code_type code_int
   1.162 -  (Haskell_Quickcheck "Prelude.Int")
   1.163 -
   1.164 -code_const "0 \<Colon> code_int"
   1.165 -  (Haskell_Quickcheck "0")
   1.166 -
   1.167 -code_const "1 \<Colon> code_int"
   1.168 -  (Haskell_Quickcheck "1")
   1.169 -
   1.170 -code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int"
   1.171 -  (Haskell_Quickcheck infixl 6 "-")
   1.172 -
   1.173 -code_const div_mod
   1.174 -  (Haskell_Quickcheck "divMod")
   1.175 -
   1.176 -code_const "HOL.equal \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
   1.177 -  (Haskell_Quickcheck infix 4 "==")
   1.178 -
   1.179 -code_const "less_eq \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
   1.180 -  (Haskell_Quickcheck infix 4 "<=")
   1.181 -
   1.182 -code_const "less \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
   1.183 -  (Haskell_Quickcheck infix 4 "<")
   1.184 -
   1.185 -code_abort of_int
   1.186 -
   1.187 -hide_const (open) Num div_mod
   1.188  
   1.189  subsubsection {* Narrowing's deep representation of types and terms *}
   1.190  
   1.191  datatype narrowing_type = Narrowing_sum_of_products "narrowing_type list list"
   1.192 -datatype narrowing_term = Narrowing_variable "code_int list" narrowing_type | Narrowing_constructor code_int "narrowing_term list"
   1.193 +datatype narrowing_term = Narrowing_variable "integer list" narrowing_type | Narrowing_constructor integer "narrowing_term list"
   1.194  datatype 'a narrowing_cons = Narrowing_cons narrowing_type "(narrowing_term list => 'a) list"
   1.195  
   1.196  primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
   1.197 @@ -207,7 +45,7 @@
   1.198   
   1.199  subsubsection {* Auxilary functions for Narrowing *}
   1.200  
   1.201 -consts nth :: "'a list => code_int => 'a"
   1.202 +consts nth :: "'a list => integer => 'a"
   1.203  
   1.204  code_const nth (Haskell_Quickcheck infixl 9  "!!")
   1.205  
   1.206 @@ -215,7 +53,7 @@
   1.207  
   1.208  code_const error (Haskell_Quickcheck "error")
   1.209  
   1.210 -consts toEnum :: "code_int => char"
   1.211 +consts toEnum :: "integer => char"
   1.212  
   1.213  code_const toEnum (Haskell_Quickcheck "Prelude.toEnum")
   1.214  
   1.215 @@ -225,7 +63,7 @@
   1.216  
   1.217  subsubsection {* Narrowing's basic operations *}
   1.218  
   1.219 -type_synonym 'a narrowing = "code_int => 'a narrowing_cons"
   1.220 +type_synonym 'a narrowing = "integer => 'a narrowing_cons"
   1.221  
   1.222  definition empty :: "'a narrowing"
   1.223  where
   1.224 @@ -267,35 +105,33 @@
   1.225  using assms unfolding sum_def by (auto split: narrowing_cons.split narrowing_type.split)
   1.226  
   1.227  lemma [fundef_cong]:
   1.228 -  assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')"
   1.229 +  assumes "f d = f' d" "(\<And>d'. 0 \<le> d' \<and> d' < d \<Longrightarrow> a d' = a' d')"
   1.230    assumes "d = d'"
   1.231    shows "apply f a d = apply f' a' d'"
   1.232  proof -
   1.233 -  note assms moreover
   1.234 -  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)))"
   1.235 -    by (simp add: of_int_inverse)
   1.236 -  moreover
   1.237 -  have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'"
   1.238 -    by (simp add: of_int_inverse)
   1.239 +  note assms
   1.240 +  moreover have "0 < d' \<Longrightarrow> 0 \<le> d' - 1"
   1.241 +    by (simp add: less_integer_def less_eq_integer_def)
   1.242    ultimately show ?thesis
   1.243 -    unfolding apply_def by (auto split: narrowing_cons.split narrowing_type.split simp add: Let_def)
   1.244 +    by (auto simp add: apply_def Let_def
   1.245 +      split: narrowing_cons.split narrowing_type.split)
   1.246  qed
   1.247  
   1.248  subsubsection {* Narrowing generator type class *}
   1.249  
   1.250  class narrowing =
   1.251 -  fixes narrowing :: "code_int => 'a narrowing_cons"
   1.252 +  fixes narrowing :: "integer => 'a narrowing_cons"
   1.253  
   1.254  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
   1.255  
   1.256  (* FIXME: hard-wired maximal depth of 100 here *)
   1.257  definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
   1.258  where
   1.259 -  "exists f = (case narrowing (100 :: code_int) of Narrowing_cons ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   1.260 +  "exists f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   1.261  
   1.262  definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
   1.263  where
   1.264 -  "all f = (case narrowing (100 :: code_int) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   1.265 +  "all f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   1.266  
   1.267  subsubsection {* class @{text is_testable} *}
   1.268  
   1.269 @@ -343,14 +179,14 @@
   1.270  where
   1.271    "narrowing_dummy_partial_term_of = partial_term_of"
   1.272  
   1.273 -definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) narrowing_cons"
   1.274 +definition narrowing_dummy_narrowing :: "integer => ('a :: narrowing) narrowing_cons"
   1.275  where
   1.276    "narrowing_dummy_narrowing = narrowing"
   1.277  
   1.278  lemma [code]:
   1.279    "ensure_testable f =
   1.280      (let
   1.281 -      x = narrowing_dummy_narrowing :: code_int => bool narrowing_cons;
   1.282 +      x = narrowing_dummy_narrowing :: integer => bool narrowing_cons;
   1.283        y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
   1.284        z = (conv :: _ => _ => unit)  in f)"
   1.285  unfolding Let_def ensure_testable_def ..
   1.286 @@ -369,47 +205,76 @@
   1.287  subsection {* Narrowing for integers *}
   1.288  
   1.289  
   1.290 -definition drawn_from :: "'a list => 'a narrowing_cons"
   1.291 -where "drawn_from xs = Narrowing_cons (Narrowing_sum_of_products (map (%_. []) xs)) (map (%x y. x) xs)"
   1.292 +definition drawn_from :: "'a list \<Rightarrow> 'a narrowing_cons"
   1.293 +where
   1.294 +  "drawn_from xs =
   1.295 +    Narrowing_cons (Narrowing_sum_of_products (map (\<lambda>_. []) xs)) (map (\<lambda>x _. x) xs)"
   1.296  
   1.297 -function around_zero :: "int => int list"
   1.298 +function around_zero :: "int \<Rightarrow> int list"
   1.299  where
   1.300    "around_zero i = (if i < 0 then [] else (if i = 0 then [0] else around_zero (i - 1) @ [i, -i]))"
   1.301 -by pat_completeness auto
   1.302 +  by pat_completeness auto
   1.303  termination by (relation "measure nat") auto
   1.304  
   1.305 -declare around_zero.simps[simp del]
   1.306 +declare around_zero.simps [simp del]
   1.307  
   1.308  lemma length_around_zero:
   1.309    assumes "i >= 0" 
   1.310    shows "length (around_zero i) = 2 * nat i + 1"
   1.311 -proof (induct rule: int_ge_induct[OF assms])
   1.312 +proof (induct rule: int_ge_induct [OF assms])
   1.313    case 1
   1.314    from 1 show ?case by (simp add: around_zero.simps)
   1.315  next
   1.316    case (2 i)
   1.317    from 2 show ?case
   1.318 -    by (simp add: around_zero.simps[of "i + 1"])
   1.319 +    by (simp add: around_zero.simps [of "i + 1"])
   1.320  qed
   1.321  
   1.322  instantiation int :: narrowing
   1.323  begin
   1.324  
   1.325  definition
   1.326 -  "narrowing_int d = (let (u :: _ => _ => unit) = conv; i = Quickcheck_Narrowing.int_of d in drawn_from (around_zero i))"
   1.327 +  "narrowing_int d = (let (u :: _ \<Rightarrow> _ \<Rightarrow> unit) = conv; i = int_of_integer d
   1.328 +    in drawn_from (around_zero i))"
   1.329  
   1.330  instance ..
   1.331  
   1.332  end
   1.333  
   1.334 -lemma [code, code del]: "partial_term_of (ty :: int itself) t == undefined"
   1.335 -by (rule partial_term_of_anything)+
   1.336 +lemma [code, code del]: "partial_term_of (ty :: int itself) t \<equiv> undefined"
   1.337 +  by (rule partial_term_of_anything)+
   1.338  
   1.339  lemma [code]:
   1.340 -  "partial_term_of (ty :: int itself) (Narrowing_variable p t) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
   1.341 -  "partial_term_of (ty :: int itself) (Narrowing_constructor i []) == (if i mod 2 = 0 then
   1.342 -     Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))"
   1.343 -by (rule partial_term_of_anything)+
   1.344 +  "partial_term_of (ty :: int itself) (Narrowing_variable p t) \<equiv>
   1.345 +    Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
   1.346 +  "partial_term_of (ty :: int itself) (Narrowing_constructor i []) \<equiv>
   1.347 +    (if i mod 2 = 0
   1.348 +     then Code_Evaluation.term_of (- (int_of_integer i) div 2)
   1.349 +     else Code_Evaluation.term_of ((int_of_integer i + 1) div 2))"
   1.350 +  by (rule partial_term_of_anything)+
   1.351 +
   1.352 +instantiation integer :: narrowing
   1.353 +begin
   1.354 +
   1.355 +definition
   1.356 +  "narrowing_integer d = (let (u :: _ \<Rightarrow> _ \<Rightarrow> unit) = conv; i = int_of_integer d
   1.357 +    in drawn_from (map integer_of_int (around_zero i)))"
   1.358 +
   1.359 +instance ..
   1.360 +
   1.361 +end
   1.362 +
   1.363 +lemma [code, code del]: "partial_term_of (ty :: integer itself) t \<equiv> undefined"
   1.364 +  by (rule partial_term_of_anything)+
   1.365 +
   1.366 +lemma [code]:
   1.367 +  "partial_term_of (ty :: integer itself) (Narrowing_variable p t) \<equiv>
   1.368 +    Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Code_Numeral.integer'') [])"
   1.369 +  "partial_term_of (ty :: integer itself) (Narrowing_constructor i []) \<equiv>
   1.370 +    (if i mod 2 = 0
   1.371 +     then Code_Evaluation.term_of (- i div 2)
   1.372 +     else Code_Evaluation.term_of ((i + 1) div 2))"
   1.373 +  by (rule partial_term_of_anything)+
   1.374  
   1.375  
   1.376  subsection {* The @{text find_unused_assms} command *}
   1.377 @@ -418,9 +283,10 @@
   1.378  
   1.379  subsection {* Closing up *}
   1.380  
   1.381 -hide_type code_int narrowing_type narrowing_term narrowing_cons property
   1.382 -hide_const int_of of_int nat_of map_cons nth error toEnum marker empty Narrowing_cons conv non_empty ensure_testable all exists drawn_from around_zero
   1.383 +hide_type narrowing_type narrowing_term narrowing_cons property
   1.384 +hide_const map_cons nth error toEnum marker empty Narrowing_cons conv non_empty ensure_testable all exists drawn_from around_zero
   1.385  hide_const (open) Narrowing_variable Narrowing_constructor "apply" sum cons
   1.386  hide_fact empty_def cons_def conv.simps non_empty.simps apply_def sum_def ensure_testable_def all_def exists_def
   1.387  
   1.388  end
   1.389 +