merged
authorhaftmann
Mon Nov 22 17:49:12 2010 +0100 (2010-11-22)
changeset 406733b9b39ac1f24
parent 40672 abd4e7358847
parent 40661 f643399acab3
child 40675 05f4885cbbe0
merged
NEWS
src/HOL/IsaMakefile
src/HOL/Library/Enum.thy
src/HOL/Library/Library.thy
     1.1 --- a/NEWS	Mon Nov 22 17:46:51 2010 +0100
     1.2 +++ b/NEWS	Mon Nov 22 17:49:12 2010 +0100
     1.3 @@ -92,6 +92,9 @@
     1.4  * Renamed theory Fset to Cset, type Fset.fset to Cset.set, in order to
     1.5  avoid confusion with finite sets.  INCOMPATIBILITY.
     1.6  
     1.7 +* Quickcheck's generator for random generation is renamed from "code" to
     1.8 +"random". INCOMPATIBILITY. 
     1.9 +
    1.10  * Theory Multiset provides stable quicksort implementation of sort_key.
    1.11  
    1.12  * Quickcheck now has a configurable time limit which is set to 30 seconds
     2.1 --- a/src/HOL/Code_Evaluation.thy	Mon Nov 22 17:46:51 2010 +0100
     2.2 +++ b/src/HOL/Code_Evaluation.thy	Mon Nov 22 17:49:12 2010 +0100
     2.3 @@ -21,7 +21,10 @@
     2.4  definition App :: "term \<Rightarrow> term \<Rightarrow> term" where
     2.5    "App _ _ = dummy_term"
     2.6  
     2.7 -code_datatype Const App
     2.8 +definition Abs :: "String.literal \<Rightarrow> typerep \<Rightarrow> term \<Rightarrow> term" where
     2.9 +  "Abs _ _ _ = dummy_term"
    2.10 +
    2.11 +code_datatype Const App Abs
    2.12  
    2.13  class term_of = typerep +
    2.14    fixes term_of :: "'a \<Rightarrow> term"
    2.15 @@ -124,8 +127,8 @@
    2.16  code_type "term"
    2.17    (Eval "Term.term")
    2.18  
    2.19 -code_const Const and App
    2.20 -  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))")
    2.21 +code_const Const and App and Abs
    2.22 +  (Eval "Term.Const/ ((_), (_))" and "Term.$/ ((_), (_))" and "Term.Abs/ ((_), (_), (_))")
    2.23  
    2.24  code_const "term_of \<Colon> String.literal \<Rightarrow> term"
    2.25    (Eval "HOLogic.mk'_literal")
    2.26 @@ -184,7 +187,7 @@
    2.27    (Eval "Code'_Evaluation.tracing")
    2.28  
    2.29  
    2.30 -hide_const dummy_term App valapp
    2.31 -hide_const (open) Const termify valtermify term_of term_of_num tracing
    2.32 +hide_const dummy_term valapp
    2.33 +hide_const (open) Const App Abs termify valtermify term_of term_of_num tracing
    2.34  
    2.35  end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Enum.thy	Mon Nov 22 17:49:12 2010 +0100
     3.3 @@ -0,0 +1,458 @@
     3.4 +(* Author: Florian Haftmann, TU Muenchen *)
     3.5 +
     3.6 +header {* Finite types as explicit enumerations *}
     3.7 +
     3.8 +theory Enum
     3.9 +imports Map String
    3.10 +begin
    3.11 +
    3.12 +subsection {* Class @{text enum} *}
    3.13 +
    3.14 +class enum =
    3.15 +  fixes enum :: "'a list"
    3.16 +  assumes UNIV_enum: "UNIV = set enum"
    3.17 +    and enum_distinct: "distinct enum"
    3.18 +begin
    3.19 +
    3.20 +subclass finite proof
    3.21 +qed (simp add: UNIV_enum)
    3.22 +
    3.23 +lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
    3.24 +
    3.25 +lemma in_enum [intro]: "x \<in> set enum"
    3.26 +  unfolding enum_all by auto
    3.27 +
    3.28 +lemma enum_eq_I:
    3.29 +  assumes "\<And>x. x \<in> set xs"
    3.30 +  shows "set enum = set xs"
    3.31 +proof -
    3.32 +  from assms UNIV_eq_I have "UNIV = set xs" by auto
    3.33 +  with enum_all show ?thesis by simp
    3.34 +qed
    3.35 +
    3.36 +end
    3.37 +
    3.38 +
    3.39 +subsection {* Equality and order on functions *}
    3.40 +
    3.41 +instantiation "fun" :: (enum, equal) equal
    3.42 +begin
    3.43 +
    3.44 +definition
    3.45 +  "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
    3.46 +
    3.47 +instance proof
    3.48 +qed (simp_all add: equal_fun_def enum_all fun_eq_iff)
    3.49 +
    3.50 +end
    3.51 +
    3.52 +lemma [code nbe]:
    3.53 +  "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
    3.54 +  by (fact equal_refl)
    3.55 +
    3.56 +lemma [code]:
    3.57 +  "HOL.equal f g \<longleftrightarrow>  list_all (%x. f x = g x) enum"
    3.58 +by (auto simp add: list_all_iff enum_all equal fun_eq_iff)
    3.59 +
    3.60 +lemma order_fun [code]:
    3.61 +  fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
    3.62 +  shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
    3.63 +    and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"
    3.64 +  by (simp_all add: list_all_iff list_ex_iff enum_all fun_eq_iff le_fun_def order_less_le)
    3.65 +
    3.66 +
    3.67 +subsection {* Quantifiers *}
    3.68 +
    3.69 +lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
    3.70 +  by (simp add: list_all_iff enum_all)
    3.71 +
    3.72 +lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
    3.73 +  by (simp add: list_ex_iff enum_all)
    3.74 +
    3.75 +lemma exists1_code[code]: "(\<exists>!x. P x) \<longleftrightarrow> list_ex1 P enum"
    3.76 +unfolding list_ex1_iff enum_all by auto
    3.77 +
    3.78 +
    3.79 +subsection {* Default instances *}
    3.80 +
    3.81 +primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
    3.82 +  "n_lists 0 xs = [[]]"
    3.83 +  | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
    3.84 +
    3.85 +lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
    3.86 +  by (induct n) simp_all
    3.87 +
    3.88 +lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
    3.89 +  by (induct n) (auto simp add: length_concat o_def listsum_triv)
    3.90 +
    3.91 +lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    3.92 +  by (induct n arbitrary: ys) auto
    3.93 +
    3.94 +lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    3.95 +proof (rule set_eqI)
    3.96 +  fix ys :: "'a list"
    3.97 +  show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    3.98 +  proof -
    3.99 +    have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
   3.100 +      by (induct n arbitrary: ys) auto
   3.101 +    moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
   3.102 +      by (induct n arbitrary: ys) auto
   3.103 +    moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
   3.104 +      by (induct ys) auto
   3.105 +    ultimately show ?thesis by auto
   3.106 +  qed
   3.107 +qed
   3.108 +
   3.109 +lemma distinct_n_lists:
   3.110 +  assumes "distinct xs"
   3.111 +  shows "distinct (n_lists n xs)"
   3.112 +proof (rule card_distinct)
   3.113 +  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
   3.114 +  have "card (set (n_lists n xs)) = card (set xs) ^ n"
   3.115 +  proof (induct n)
   3.116 +    case 0 then show ?case by simp
   3.117 +  next
   3.118 +    case (Suc n)
   3.119 +    moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
   3.120 +      = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
   3.121 +      by (rule card_UN_disjoint) auto
   3.122 +    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
   3.123 +      by (rule card_image) (simp add: inj_on_def)
   3.124 +    ultimately show ?case by auto
   3.125 +  qed
   3.126 +  also have "\<dots> = length xs ^ n" by (simp add: card_length)
   3.127 +  finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
   3.128 +    by (simp add: length_n_lists)
   3.129 +qed
   3.130 +
   3.131 +lemma map_of_zip_enum_is_Some:
   3.132 +  assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   3.133 +  shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
   3.134 +proof -
   3.135 +  from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
   3.136 +    (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
   3.137 +    by (auto intro!: map_of_zip_is_Some)
   3.138 +  then show ?thesis using enum_all by auto
   3.139 +qed
   3.140 +
   3.141 +lemma map_of_zip_enum_inject:
   3.142 +  fixes xs ys :: "'b\<Colon>enum list"
   3.143 +  assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)"
   3.144 +      "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   3.145 +    and map_of: "the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys)"
   3.146 +  shows "xs = ys"
   3.147 +proof -
   3.148 +  have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)"
   3.149 +  proof
   3.150 +    fix x :: 'a
   3.151 +    from length map_of_zip_enum_is_Some obtain y1 y2
   3.152 +      where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
   3.153 +        and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
   3.154 +    moreover from map_of have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)"
   3.155 +      by (auto dest: fun_cong)
   3.156 +    ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
   3.157 +      by simp
   3.158 +  qed
   3.159 +  with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
   3.160 +qed
   3.161 +
   3.162 +instantiation "fun" :: (enum, enum) enum
   3.163 +begin
   3.164 +
   3.165 +definition
   3.166 +  "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
   3.167 +
   3.168 +instance proof
   3.169 +  show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
   3.170 +  proof (rule UNIV_eq_I)
   3.171 +    fix f :: "'a \<Rightarrow> 'b"
   3.172 +    have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
   3.173 +      by (auto simp add: map_of_zip_map fun_eq_iff)
   3.174 +    then show "f \<in> set enum"
   3.175 +      by (auto simp add: enum_fun_def set_n_lists)
   3.176 +  qed
   3.177 +next
   3.178 +  from map_of_zip_enum_inject
   3.179 +  show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
   3.180 +    by (auto intro!: inj_onI simp add: enum_fun_def
   3.181 +      distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
   3.182 +qed
   3.183 +
   3.184 +end
   3.185 +
   3.186 +lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
   3.187 +  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
   3.188 +  by (simp add: enum_fun_def Let_def)
   3.189 +
   3.190 +instantiation unit :: enum
   3.191 +begin
   3.192 +
   3.193 +definition
   3.194 +  "enum = [()]"
   3.195 +
   3.196 +instance proof
   3.197 +qed (simp_all add: enum_unit_def UNIV_unit)
   3.198 +
   3.199 +end
   3.200 +
   3.201 +instantiation bool :: enum
   3.202 +begin
   3.203 +
   3.204 +definition
   3.205 +  "enum = [False, True]"
   3.206 +
   3.207 +instance proof
   3.208 +qed (simp_all add: enum_bool_def UNIV_bool)
   3.209 +
   3.210 +end
   3.211 +
   3.212 +primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   3.213 +  "product [] _ = []"
   3.214 +  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
   3.215 +
   3.216 +lemma product_list_set:
   3.217 +  "set (product xs ys) = set xs \<times> set ys"
   3.218 +  by (induct xs) auto
   3.219 +
   3.220 +lemma distinct_product:
   3.221 +  assumes "distinct xs" and "distinct ys"
   3.222 +  shows "distinct (product xs ys)"
   3.223 +  using assms by (induct xs)
   3.224 +    (auto intro: inj_onI simp add: product_list_set distinct_map)
   3.225 +
   3.226 +instantiation prod :: (enum, enum) enum
   3.227 +begin
   3.228 +
   3.229 +definition
   3.230 +  "enum = product enum enum"
   3.231 +
   3.232 +instance by default
   3.233 +  (simp_all add: enum_prod_def product_list_set distinct_product enum_all enum_distinct)
   3.234 +
   3.235 +end
   3.236 +
   3.237 +instantiation sum :: (enum, enum) enum
   3.238 +begin
   3.239 +
   3.240 +definition
   3.241 +  "enum = map Inl enum @ map Inr enum"
   3.242 +
   3.243 +instance by default
   3.244 +  (auto simp add: enum_all enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
   3.245 +
   3.246 +end
   3.247 +
   3.248 +primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   3.249 +  "sublists [] = [[]]"
   3.250 +  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   3.251 +
   3.252 +lemma length_sublists:
   3.253 +  "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
   3.254 +  by (induct xs) (simp_all add: Let_def)
   3.255 +
   3.256 +lemma sublists_powset:
   3.257 +  "set ` set (sublists xs) = Pow (set xs)"
   3.258 +proof -
   3.259 +  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
   3.260 +    by (auto simp add: image_def)
   3.261 +  have "set (map set (sublists xs)) = Pow (set xs)"
   3.262 +    by (induct xs)
   3.263 +      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
   3.264 +  then show ?thesis by simp
   3.265 +qed
   3.266 +
   3.267 +lemma distinct_set_sublists:
   3.268 +  assumes "distinct xs"
   3.269 +  shows "distinct (map set (sublists xs))"
   3.270 +proof (rule card_distinct)
   3.271 +  have "finite (set xs)" by rule
   3.272 +  then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
   3.273 +  with assms distinct_card [of xs]
   3.274 +    have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
   3.275 +  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
   3.276 +    by (simp add: sublists_powset length_sublists)
   3.277 +qed
   3.278 +
   3.279 +instantiation nibble :: enum
   3.280 +begin
   3.281 +
   3.282 +definition
   3.283 +  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
   3.284 +    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
   3.285 +
   3.286 +instance proof
   3.287 +qed (simp_all add: enum_nibble_def UNIV_nibble)
   3.288 +
   3.289 +end
   3.290 +
   3.291 +instantiation char :: enum
   3.292 +begin
   3.293 +
   3.294 +definition
   3.295 +  "enum = map (split Char) (product enum enum)"
   3.296 +
   3.297 +lemma enum_chars [code]:
   3.298 +  "enum = chars"
   3.299 +  unfolding enum_char_def chars_def enum_nibble_def by simp
   3.300 +
   3.301 +instance proof
   3.302 +qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
   3.303 +  distinct_map distinct_product enum_distinct)
   3.304 +
   3.305 +end
   3.306 +
   3.307 +instantiation option :: (enum) enum
   3.308 +begin
   3.309 +
   3.310 +definition
   3.311 +  "enum = None # map Some enum"
   3.312 +
   3.313 +instance proof
   3.314 +qed (auto simp add: enum_all enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
   3.315 +
   3.316 +end
   3.317 +
   3.318 +subsection {* Small finite types *}
   3.319 +
   3.320 +text {* We define small finite types for the use in Quickcheck *}
   3.321 +
   3.322 +datatype finite_1 = a\<^isub>1
   3.323 +
   3.324 +instantiation finite_1 :: enum
   3.325 +begin
   3.326 +
   3.327 +definition
   3.328 +  "enum = [a\<^isub>1]"
   3.329 +
   3.330 +instance proof
   3.331 +qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust)
   3.332 +
   3.333 +end
   3.334 +
   3.335 +instantiation finite_1 :: linorder
   3.336 +begin
   3.337 +
   3.338 +definition less_eq_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
   3.339 +where
   3.340 +  "less_eq_finite_1 x y = True"
   3.341 +
   3.342 +definition less_finite_1 :: "finite_1 \<Rightarrow> finite_1 \<Rightarrow> bool"
   3.343 +where
   3.344 +  "less_finite_1 x y = False"
   3.345 +
   3.346 +instance
   3.347 +apply (intro_classes)
   3.348 +apply (auto simp add: less_finite_1_def less_eq_finite_1_def)
   3.349 +apply (metis finite_1.exhaust)
   3.350 +done
   3.351 +
   3.352 +end
   3.353 +
   3.354 +hide_const a\<^isub>1
   3.355 +
   3.356 +datatype finite_2 = a\<^isub>1 | a\<^isub>2
   3.357 +
   3.358 +instantiation finite_2 :: enum
   3.359 +begin
   3.360 +
   3.361 +definition
   3.362 +  "enum = [a\<^isub>1, a\<^isub>2]"
   3.363 +
   3.364 +instance proof
   3.365 +qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust)
   3.366 +
   3.367 +end
   3.368 +
   3.369 +instantiation finite_2 :: linorder
   3.370 +begin
   3.371 +
   3.372 +definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
   3.373 +where
   3.374 +  "less_finite_2 x y = ((x = a\<^isub>1) & (y = a\<^isub>2))"
   3.375 +
   3.376 +definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
   3.377 +where
   3.378 +  "less_eq_finite_2 x y = ((x = y) \<or> (x < y))"
   3.379 +
   3.380 +
   3.381 +instance
   3.382 +apply (intro_classes)
   3.383 +apply (auto simp add: less_finite_2_def less_eq_finite_2_def)
   3.384 +apply (metis finite_2.distinct finite_2.nchotomy)+
   3.385 +done
   3.386 +
   3.387 +end
   3.388 +
   3.389 +hide_const a\<^isub>1 a\<^isub>2
   3.390 +
   3.391 +
   3.392 +datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
   3.393 +
   3.394 +instantiation finite_3 :: enum
   3.395 +begin
   3.396 +
   3.397 +definition
   3.398 +  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
   3.399 +
   3.400 +instance proof
   3.401 +qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust)
   3.402 +
   3.403 +end
   3.404 +
   3.405 +instantiation finite_3 :: linorder
   3.406 +begin
   3.407 +
   3.408 +definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
   3.409 +where
   3.410 +  "less_finite_3 x y = (case x of a\<^isub>1 => (y \<noteq> a\<^isub>1)
   3.411 +     | a\<^isub>2 => (y = a\<^isub>3)| a\<^isub>3 => False)"
   3.412 +
   3.413 +definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
   3.414 +where
   3.415 +  "less_eq_finite_3 x y = ((x = y) \<or> (x < y))"
   3.416 +
   3.417 +
   3.418 +instance proof (intro_classes)
   3.419 +qed (auto simp add: less_finite_3_def less_eq_finite_3_def split: finite_3.split_asm)
   3.420 +
   3.421 +end
   3.422 +
   3.423 +hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3
   3.424 +
   3.425 +
   3.426 +datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
   3.427 +
   3.428 +instantiation finite_4 :: enum
   3.429 +begin
   3.430 +
   3.431 +definition
   3.432 +  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
   3.433 +
   3.434 +instance proof
   3.435 +qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
   3.436 +
   3.437 +end
   3.438 +
   3.439 +hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
   3.440 +
   3.441 +
   3.442 +datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
   3.443 +
   3.444 +instantiation finite_5 :: enum
   3.445 +begin
   3.446 +
   3.447 +definition
   3.448 +  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
   3.449 +
   3.450 +instance proof
   3.451 +qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
   3.452 +
   3.453 +end
   3.454 +
   3.455 +hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
   3.456 +
   3.457 +
   3.458 +hide_type finite_1 finite_2 finite_3 finite_4 finite_5
   3.459 +hide_const (open) enum n_lists product
   3.460 +
   3.461 +end
     4.1 --- a/src/HOL/IsaMakefile	Mon Nov 22 17:46:51 2010 +0100
     4.2 +++ b/src/HOL/IsaMakefile	Mon Nov 22 17:49:12 2010 +0100
     4.3 @@ -246,6 +246,7 @@
     4.4    Divides.thy \
     4.5    DSequence.thy \
     4.6    Equiv_Relations.thy \
     4.7 +  Enum.thy \
     4.8    Groebner_Basis.thy \
     4.9    Hilbert_Choice.thy \
    4.10    Int.thy \
    4.11 @@ -416,7 +417,7 @@
    4.12    Library/Code_Prolog.thy Tools/Predicate_Compile/code_prolog.ML	\
    4.13    Library/ContNotDenum.thy Library/Continuity.thy Library/Convex.thy	\
    4.14    Library/Countable.thy Library/Diagonalize.thy Library/Dlist.thy	\
    4.15 -  Library/Efficient_Nat.thy Library/Enum.thy Library/Eval_Witness.thy	\
    4.16 +  Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
    4.17    Library/Executable_Set.thy Library/Float.thy				\
    4.18    Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
    4.19    Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
    4.20 @@ -1016,7 +1017,8 @@
    4.21  $(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy	\
    4.22    Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
    4.23    ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy	\
    4.24 -  ex/BinEx.thy ex/Binary.thy ex/CTL.thy ex/Chinese.thy			\
    4.25 +  ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy   \
    4.26 +  ex/Chinese.thy \
    4.27    ex/Classical.thy ex/CodegenSML_Test.thy ex/Coercion_Examples.thy	\
    4.28    ex/Coherent.thy ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy	\
    4.29    ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy		\
    4.30 @@ -1294,7 +1296,8 @@
    4.31    Mirabelle/Tools/mirabelle_metis.ML					\
    4.32    Mirabelle/Tools/mirabelle_quickcheck.ML				\
    4.33    Mirabelle/Tools/mirabelle_refute.ML					\
    4.34 -  Mirabelle/Tools/mirabelle_sledgehammer.ML
    4.35 +  Mirabelle/Tools/mirabelle_sledgehammer.ML 				\
    4.36 +  Mirabelle/Tools/sledgehammer_tactic.ML
    4.37  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
    4.38  
    4.39  
     5.1 --- a/src/HOL/Library/Enum.thy	Mon Nov 22 17:46:51 2010 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,308 +0,0 @@
     5.4 -(* Author: Florian Haftmann, TU Muenchen *)
     5.5 -
     5.6 -header {* Finite types as explicit enumerations *}
     5.7 -
     5.8 -theory Enum
     5.9 -imports Map Main
    5.10 -begin
    5.11 -
    5.12 -subsection {* Class @{text enum} *}
    5.13 -
    5.14 -class enum =
    5.15 -  fixes enum :: "'a list"
    5.16 -  assumes UNIV_enum: "UNIV = set enum"
    5.17 -    and enum_distinct: "distinct enum"
    5.18 -begin
    5.19 -
    5.20 -subclass finite proof
    5.21 -qed (simp add: UNIV_enum)
    5.22 -
    5.23 -lemma enum_all: "set enum = UNIV" unfolding UNIV_enum ..
    5.24 -
    5.25 -lemma in_enum [intro]: "x \<in> set enum"
    5.26 -  unfolding enum_all by auto
    5.27 -
    5.28 -lemma enum_eq_I:
    5.29 -  assumes "\<And>x. x \<in> set xs"
    5.30 -  shows "set enum = set xs"
    5.31 -proof -
    5.32 -  from assms UNIV_eq_I have "UNIV = set xs" by auto
    5.33 -  with enum_all show ?thesis by simp
    5.34 -qed
    5.35 -
    5.36 -end
    5.37 -
    5.38 -
    5.39 -subsection {* Equality and order on functions *}
    5.40 -
    5.41 -instantiation "fun" :: (enum, equal) equal
    5.42 -begin
    5.43 -
    5.44 -definition
    5.45 -  "HOL.equal f g \<longleftrightarrow> (\<forall>x \<in> set enum. f x = g x)"
    5.46 -
    5.47 -instance proof
    5.48 -qed (simp_all add: equal_fun_def enum_all fun_eq_iff)
    5.49 -
    5.50 -end
    5.51 -
    5.52 -lemma [code nbe]:
    5.53 -  "HOL.equal (f :: _ \<Rightarrow> _) f \<longleftrightarrow> True"
    5.54 -  by (fact equal_refl)
    5.55 -
    5.56 -lemma order_fun [code]:
    5.57 -  fixes f g :: "'a\<Colon>enum \<Rightarrow> 'b\<Colon>order"
    5.58 -  shows "f \<le> g \<longleftrightarrow> list_all (\<lambda>x. f x \<le> g x) enum"
    5.59 -    and "f < g \<longleftrightarrow> f \<le> g \<and> list_ex (\<lambda>x. f x \<noteq> g x) enum"
    5.60 -  by (simp_all add: list_all_iff list_ex_iff enum_all fun_eq_iff le_fun_def order_less_le)
    5.61 -
    5.62 -
    5.63 -subsection {* Quantifiers *}
    5.64 -
    5.65 -lemma all_code [code]: "(\<forall>x. P x) \<longleftrightarrow> list_all P enum"
    5.66 -  by (simp add: list_all_iff enum_all)
    5.67 -
    5.68 -lemma exists_code [code]: "(\<exists>x. P x) \<longleftrightarrow> list_ex P enum"
    5.69 -  by (simp add: list_ex_iff enum_all)
    5.70 -
    5.71 -
    5.72 -subsection {* Default instances *}
    5.73 -
    5.74 -primrec n_lists :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
    5.75 -  "n_lists 0 xs = [[]]"
    5.76 -  | "n_lists (Suc n) xs = concat (map (\<lambda>ys. map (\<lambda>y. y # ys) xs) (n_lists n xs))"
    5.77 -
    5.78 -lemma n_lists_Nil [simp]: "n_lists n [] = (if n = 0 then [[]] else [])"
    5.79 -  by (induct n) simp_all
    5.80 -
    5.81 -lemma length_n_lists: "length (n_lists n xs) = length xs ^ n"
    5.82 -  by (induct n) (auto simp add: length_concat o_def listsum_triv)
    5.83 -
    5.84 -lemma length_n_lists_elem: "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    5.85 -  by (induct n arbitrary: ys) auto
    5.86 -
    5.87 -lemma set_n_lists: "set (n_lists n xs) = {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    5.88 -proof (rule set_eqI)
    5.89 -  fix ys :: "'a list"
    5.90 -  show "ys \<in> set (n_lists n xs) \<longleftrightarrow> ys \<in> {ys. length ys = n \<and> set ys \<subseteq> set xs}"
    5.91 -  proof -
    5.92 -    have "ys \<in> set (n_lists n xs) \<Longrightarrow> length ys = n"
    5.93 -      by (induct n arbitrary: ys) auto
    5.94 -    moreover have "\<And>x. ys \<in> set (n_lists n xs) \<Longrightarrow> x \<in> set ys \<Longrightarrow> x \<in> set xs"
    5.95 -      by (induct n arbitrary: ys) auto
    5.96 -    moreover have "set ys \<subseteq> set xs \<Longrightarrow> ys \<in> set (n_lists (length ys) xs)"
    5.97 -      by (induct ys) auto
    5.98 -    ultimately show ?thesis by auto
    5.99 -  qed
   5.100 -qed
   5.101 -
   5.102 -lemma distinct_n_lists:
   5.103 -  assumes "distinct xs"
   5.104 -  shows "distinct (n_lists n xs)"
   5.105 -proof (rule card_distinct)
   5.106 -  from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
   5.107 -  have "card (set (n_lists n xs)) = card (set xs) ^ n"
   5.108 -  proof (induct n)
   5.109 -    case 0 then show ?case by simp
   5.110 -  next
   5.111 -    case (Suc n)
   5.112 -    moreover have "card (\<Union>ys\<in>set (n_lists n xs). (\<lambda>y. y # ys) ` set xs)
   5.113 -      = (\<Sum>ys\<in>set (n_lists n xs). card ((\<lambda>y. y # ys) ` set xs))"
   5.114 -      by (rule card_UN_disjoint) auto
   5.115 -    moreover have "\<And>ys. card ((\<lambda>y. y # ys) ` set xs) = card (set xs)"
   5.116 -      by (rule card_image) (simp add: inj_on_def)
   5.117 -    ultimately show ?case by auto
   5.118 -  qed
   5.119 -  also have "\<dots> = length xs ^ n" by (simp add: card_length)
   5.120 -  finally show "card (set (n_lists n xs)) = length (n_lists n xs)"
   5.121 -    by (simp add: length_n_lists)
   5.122 -qed
   5.123 -
   5.124 -lemma map_of_zip_enum_is_Some:
   5.125 -  assumes "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   5.126 -  shows "\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y"
   5.127 -proof -
   5.128 -  from assms have "x \<in> set (enum \<Colon> 'a\<Colon>enum list) \<longleftrightarrow>
   5.129 -    (\<exists>y. map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x = Some y)"
   5.130 -    by (auto intro!: map_of_zip_is_Some)
   5.131 -  then show ?thesis using enum_all by auto
   5.132 -qed
   5.133 -
   5.134 -lemma map_of_zip_enum_inject:
   5.135 -  fixes xs ys :: "'b\<Colon>enum list"
   5.136 -  assumes length: "length xs = length (enum \<Colon> 'a\<Colon>enum list)"
   5.137 -      "length ys = length (enum \<Colon> 'a\<Colon>enum list)"
   5.138 -    and map_of: "the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys)"
   5.139 -  shows "xs = ys"
   5.140 -proof -
   5.141 -  have "map_of (zip (enum \<Colon> 'a list) xs) = map_of (zip (enum \<Colon> 'a list) ys)"
   5.142 -  proof
   5.143 -    fix x :: 'a
   5.144 -    from length map_of_zip_enum_is_Some obtain y1 y2
   5.145 -      where "map_of (zip (enum \<Colon> 'a list) xs) x = Some y1"
   5.146 -        and "map_of (zip (enum \<Colon> 'a list) ys) x = Some y2" by blast
   5.147 -    moreover from map_of have "the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x) = the (map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x)"
   5.148 -      by (auto dest: fun_cong)
   5.149 -    ultimately show "map_of (zip (enum \<Colon> 'a\<Colon>enum list) xs) x = map_of (zip (enum \<Colon> 'a\<Colon>enum list) ys) x"
   5.150 -      by simp
   5.151 -  qed
   5.152 -  with length enum_distinct show "xs = ys" by (rule map_of_zip_inject)
   5.153 -qed
   5.154 -
   5.155 -instantiation "fun" :: (enum, enum) enum
   5.156 -begin
   5.157 -
   5.158 -definition
   5.159 -  "enum = map (\<lambda>ys. the o map_of (zip (enum\<Colon>'a list) ys)) (n_lists (length (enum\<Colon>'a\<Colon>enum list)) enum)"
   5.160 -
   5.161 -instance proof
   5.162 -  show "UNIV = set (enum \<Colon> ('a \<Rightarrow> 'b) list)"
   5.163 -  proof (rule UNIV_eq_I)
   5.164 -    fix f :: "'a \<Rightarrow> 'b"
   5.165 -    have "f = the \<circ> map_of (zip (enum \<Colon> 'a\<Colon>enum list) (map f enum))"
   5.166 -      by (auto simp add: map_of_zip_map fun_eq_iff)
   5.167 -    then show "f \<in> set enum"
   5.168 -      by (auto simp add: enum_fun_def set_n_lists)
   5.169 -  qed
   5.170 -next
   5.171 -  from map_of_zip_enum_inject
   5.172 -  show "distinct (enum \<Colon> ('a \<Rightarrow> 'b) list)"
   5.173 -    by (auto intro!: inj_onI simp add: enum_fun_def
   5.174 -      distinct_map distinct_n_lists enum_distinct set_n_lists enum_all)
   5.175 -qed
   5.176 -
   5.177 -end
   5.178 -
   5.179 -lemma enum_fun_code [code]: "enum = (let enum_a = (enum \<Colon> 'a\<Colon>{enum, equal} list)
   5.180 -  in map (\<lambda>ys. the o map_of (zip enum_a ys)) (n_lists (length enum_a) enum))"
   5.181 -  by (simp add: enum_fun_def Let_def)
   5.182 -
   5.183 -instantiation unit :: enum
   5.184 -begin
   5.185 -
   5.186 -definition
   5.187 -  "enum = [()]"
   5.188 -
   5.189 -instance proof
   5.190 -qed (simp_all add: enum_unit_def UNIV_unit)
   5.191 -
   5.192 -end
   5.193 -
   5.194 -instantiation bool :: enum
   5.195 -begin
   5.196 -
   5.197 -definition
   5.198 -  "enum = [False, True]"
   5.199 -
   5.200 -instance proof
   5.201 -qed (simp_all add: enum_bool_def UNIV_bool)
   5.202 -
   5.203 -end
   5.204 -
   5.205 -primrec product :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   5.206 -  "product [] _ = []"
   5.207 -  | "product (x#xs) ys = map (Pair x) ys @ product xs ys"
   5.208 -
   5.209 -lemma product_list_set:
   5.210 -  "set (product xs ys) = set xs \<times> set ys"
   5.211 -  by (induct xs) auto
   5.212 -
   5.213 -lemma distinct_product:
   5.214 -  assumes "distinct xs" and "distinct ys"
   5.215 -  shows "distinct (product xs ys)"
   5.216 -  using assms by (induct xs)
   5.217 -    (auto intro: inj_onI simp add: product_list_set distinct_map)
   5.218 -
   5.219 -instantiation prod :: (enum, enum) enum
   5.220 -begin
   5.221 -
   5.222 -definition
   5.223 -  "enum = product enum enum"
   5.224 -
   5.225 -instance by default
   5.226 -  (simp_all add: enum_prod_def product_list_set distinct_product enum_all enum_distinct)
   5.227 -
   5.228 -end
   5.229 -
   5.230 -instantiation sum :: (enum, enum) enum
   5.231 -begin
   5.232 -
   5.233 -definition
   5.234 -  "enum = map Inl enum @ map Inr enum"
   5.235 -
   5.236 -instance by default
   5.237 -  (auto simp add: enum_all enum_sum_def, case_tac x, auto intro: inj_onI simp add: distinct_map enum_distinct)
   5.238 -
   5.239 -end
   5.240 -
   5.241 -primrec sublists :: "'a list \<Rightarrow> 'a list list" where
   5.242 -  "sublists [] = [[]]"
   5.243 -  | "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"
   5.244 -
   5.245 -lemma length_sublists:
   5.246 -  "length (sublists xs) = Suc (Suc (0\<Colon>nat)) ^ length xs"
   5.247 -  by (induct xs) (simp_all add: Let_def)
   5.248 -
   5.249 -lemma sublists_powset:
   5.250 -  "set ` set (sublists xs) = Pow (set xs)"
   5.251 -proof -
   5.252 -  have aux: "\<And>x A. set ` Cons x ` A = insert x ` set ` A"
   5.253 -    by (auto simp add: image_def)
   5.254 -  have "set (map set (sublists xs)) = Pow (set xs)"
   5.255 -    by (induct xs)
   5.256 -      (simp_all add: aux Let_def Pow_insert Un_commute comp_def del: map_map)
   5.257 -  then show ?thesis by simp
   5.258 -qed
   5.259 -
   5.260 -lemma distinct_set_sublists:
   5.261 -  assumes "distinct xs"
   5.262 -  shows "distinct (map set (sublists xs))"
   5.263 -proof (rule card_distinct)
   5.264 -  have "finite (set xs)" by rule
   5.265 -  then have "card (Pow (set xs)) = Suc (Suc 0) ^ card (set xs)" by (rule card_Pow)
   5.266 -  with assms distinct_card [of xs]
   5.267 -    have "card (Pow (set xs)) = Suc (Suc 0) ^ length xs" by simp
   5.268 -  then show "card (set (map set (sublists xs))) = length (map set (sublists xs))"
   5.269 -    by (simp add: sublists_powset length_sublists)
   5.270 -qed
   5.271 -
   5.272 -instantiation nibble :: enum
   5.273 -begin
   5.274 -
   5.275 -definition
   5.276 -  "enum = [Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
   5.277 -    Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF]"
   5.278 -
   5.279 -instance proof
   5.280 -qed (simp_all add: enum_nibble_def UNIV_nibble)
   5.281 -
   5.282 -end
   5.283 -
   5.284 -instantiation char :: enum
   5.285 -begin
   5.286 -
   5.287 -definition
   5.288 -  "enum = map (split Char) (product enum enum)"
   5.289 -
   5.290 -lemma enum_chars [code]:
   5.291 -  "enum = chars"
   5.292 -  unfolding enum_char_def chars_def enum_nibble_def by simp
   5.293 -
   5.294 -instance proof
   5.295 -qed (auto intro: char.exhaust injI simp add: enum_char_def product_list_set enum_all full_SetCompr_eq [symmetric]
   5.296 -  distinct_map distinct_product enum_distinct)
   5.297 -
   5.298 -end
   5.299 -
   5.300 -instantiation option :: (enum) enum
   5.301 -begin
   5.302 -
   5.303 -definition
   5.304 -  "enum = None # map Some enum"
   5.305 -
   5.306 -instance proof
   5.307 -qed (auto simp add: enum_all enum_option_def, rule option.exhaust, auto intro: simp add: distinct_map enum_distinct)
   5.308 -
   5.309 -end
   5.310 -
   5.311 -end
     6.1 --- a/src/HOL/Library/FuncSet.thy	Mon Nov 22 17:46:51 2010 +0100
     6.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Nov 22 17:49:12 2010 +0100
     6.3 @@ -1,5 +1,5 @@
     6.4  (*  Title:      HOL/Library/FuncSet.thy
     6.5 -    Author:     Florian Kammueller and Lawrence C Paulson
     6.6 +    Author:     Florian Kammueller and Lawrence C Paulson, Lukas Bulwahn
     6.7  *)
     6.8  
     6.9  header {* Pi and Function Sets *}
    6.10 @@ -251,4 +251,158 @@
    6.11       g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
    6.12  by (blast intro: card_inj order_antisym)
    6.13  
    6.14 +subsection {* Extensional Function Spaces *} 
    6.15 +
    6.16 +definition extensional_funcset
    6.17 +where "extensional_funcset S T = (S -> T) \<inter> (extensional S)"
    6.18 +
    6.19 +lemma extensional_empty[simp]: "extensional {} = {%x. undefined}"
    6.20 +unfolding extensional_def by (auto intro: ext)
    6.21 +
    6.22 +lemma extensional_funcset_empty_domain: "extensional_funcset {} T = {%x. undefined}"
    6.23 +unfolding extensional_funcset_def by simp
    6.24 +
    6.25 +lemma extensional_funcset_empty_range:
    6.26 +  assumes "S \<noteq> {}"
    6.27 +  shows "extensional_funcset S {} = {}"
    6.28 +using assms unfolding extensional_funcset_def by auto
    6.29 +
    6.30 +lemma extensional_funcset_arb:
    6.31 +  assumes "f \<in> extensional_funcset S T" "x \<notin> S"
    6.32 +  shows "f x = undefined"
    6.33 +using assms
    6.34 +unfolding extensional_funcset_def by auto (auto dest!: extensional_arb)
    6.35 +
    6.36 +lemma extensional_funcset_mem: "f \<in> extensional_funcset S T \<Longrightarrow> x \<in> S \<Longrightarrow> f x \<in> T"
    6.37 +unfolding extensional_funcset_def by auto
    6.38 +
    6.39 +lemma extensional_subset: "f : extensional A ==> A <= B ==> f : extensional B"
    6.40 +unfolding extensional_def by auto
    6.41 +
    6.42 +lemma extensional_funcset_extend_domainI: "\<lbrakk> y \<in> T; f \<in> extensional_funcset S T\<rbrakk> \<Longrightarrow> f(x := y) \<in> extensional_funcset (insert x S) T"
    6.43 +unfolding extensional_funcset_def extensional_def by auto
    6.44 +
    6.45 +lemma extensional_funcset_restrict_domain:
    6.46 +  "x \<notin> S \<Longrightarrow> f \<in> extensional_funcset (insert x S) T \<Longrightarrow> f(x := undefined) \<in> extensional_funcset S T"
    6.47 +unfolding extensional_funcset_def extensional_def by auto
    6.48 +
    6.49 +lemma extensional_funcset_extend_domain_eq:
    6.50 +  assumes "x \<notin> S"
    6.51 +  shows
    6.52 +    "extensional_funcset (insert x S) T = (\<lambda>(y, g). g(x := y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S T}"
    6.53 +  using assms
    6.54 +proof -
    6.55 +  {
    6.56 +    fix f
    6.57 +    assume "f : extensional_funcset (insert x S) T"
    6.58 +    from this assms have "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
    6.59 +      unfolding image_iff
    6.60 +      apply (rule_tac x="(f x, f(x := undefined))" in bexI)
    6.61 +    apply (auto intro: extensional_funcset_extend_domainI extensional_funcset_restrict_domain extensional_funcset_mem) done 
    6.62 +  }
    6.63 +  moreover
    6.64 +  {
    6.65 +    fix f
    6.66 +    assume "f : (%(y, g). g(x := y)) ` (T <*> extensional_funcset S T)"
    6.67 +    from this assms have "f : extensional_funcset (insert x S) T"
    6.68 +      by (auto intro: extensional_funcset_extend_domainI)
    6.69 +  }
    6.70 +  ultimately show ?thesis by auto
    6.71 +qed
    6.72 +
    6.73 +lemma extensional_funcset_fun_upd_restricts_rangeI:  "\<forall> y \<in> S. f x \<noteq> f y ==> f : extensional_funcset (insert x S) T ==> f(x := undefined) : extensional_funcset S (T - {f x})"
    6.74 +unfolding extensional_funcset_def extensional_def
    6.75 +apply auto
    6.76 +apply (case_tac "x = xa")
    6.77 +apply auto done
    6.78 +
    6.79 +lemma extensional_funcset_fun_upd_extends_rangeI:
    6.80 +  assumes "a \<in> T" "f : extensional_funcset S (T - {a})"
    6.81 +  shows "f(x := a) : extensional_funcset (insert x S) T"
    6.82 +  using assms unfolding extensional_funcset_def extensional_def by auto
    6.83 +
    6.84 +subsubsection {* Injective Extensional Function Spaces *}
    6.85 +
    6.86 +lemma extensional_funcset_fun_upd_inj_onI:
    6.87 +  assumes "f \<in> extensional_funcset S (T - {a})" "inj_on f S"
    6.88 +  shows "inj_on (f(x := a)) S"
    6.89 +  using assms unfolding extensional_funcset_def by (auto intro!: inj_on_fun_updI)
    6.90 +
    6.91 +lemma extensional_funcset_extend_domain_inj_on_eq:
    6.92 +  assumes "x \<notin> S"
    6.93 +  shows"{f. f \<in> extensional_funcset (insert x S) T \<and> inj_on f (insert x S)} =
    6.94 +    (%(y, g). g(x:=y)) ` {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
    6.95 +proof -
    6.96 +  from assms show ?thesis
    6.97 +    apply auto
    6.98 +    apply (auto intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI)
    6.99 +    apply (auto simp add: image_iff inj_on_def)
   6.100 +    apply (rule_tac x="xa x" in exI)
   6.101 +    apply (auto intro: extensional_funcset_mem)
   6.102 +    apply (rule_tac x="xa(x := undefined)" in exI)
   6.103 +    apply (auto intro!: extensional_funcset_fun_upd_restricts_rangeI)
   6.104 +    apply (auto dest!: extensional_funcset_mem split: split_if_asm)
   6.105 +    done
   6.106 +qed
   6.107 +
   6.108 +lemma extensional_funcset_extend_domain_inj_onI:
   6.109 +  assumes "x \<notin> S"
   6.110 +  shows "inj_on (\<lambda>(y, g). g(x := y)) {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}"
   6.111 +proof -
   6.112 +  from assms show ?thesis
   6.113 +    apply (auto intro!: inj_onI)
   6.114 +    apply (metis fun_upd_same)
   6.115 +    by (metis assms extensional_funcset_arb fun_upd_triv fun_upd_upd)
   6.116 +qed
   6.117 +  
   6.118 +
   6.119 +subsubsection {* Cardinality *}
   6.120 +
   6.121 +lemma card_extensional_funcset:
   6.122 +  assumes "finite S"
   6.123 +  shows "card (extensional_funcset S T) = (card T) ^ (card S)"
   6.124 +using assms
   6.125 +proof (induct rule: finite_induct)
   6.126 +  case empty
   6.127 +  show ?case
   6.128 +    by (auto simp add: extensional_funcset_empty_domain)
   6.129 +next
   6.130 +  case (insert x S)
   6.131 +  {
   6.132 +    fix g g' y y'
   6.133 +    assume assms: "g \<in> extensional_funcset S T"
   6.134 +      "g' \<in> extensional_funcset S T"
   6.135 +      "y \<in> T" "y' \<in> T"
   6.136 +      "g(x := y) = g'(x := y')"
   6.137 +    from this have "y = y'"
   6.138 +      by (metis fun_upd_same)
   6.139 +    have "g = g'"
   6.140 +      by (metis assms(1) assms(2) assms(5) extensional_funcset_arb fun_upd_triv fun_upd_upd insert(2))
   6.141 +  from `y = y'` `g = g'` have "y = y' & g = g'" by simp
   6.142 +  }
   6.143 +  from this have "inj_on (\<lambda>(y, g). g (x := y)) (T \<times> extensional_funcset S T)"
   6.144 +    by (auto intro: inj_onI)
   6.145 +  from this insert.hyps show ?case
   6.146 +    by (simp add: extensional_funcset_extend_domain_eq card_image card_cartesian_product)
   6.147 +qed
   6.148 +
   6.149 +lemma finite_extensional_funcset:
   6.150 +  assumes "finite S" "finite T"
   6.151 +  shows "finite (extensional_funcset S T)"
   6.152 +proof -
   6.153 +  from card_extensional_funcset[OF assms(1), of T] assms(2)
   6.154 +  have "(card (extensional_funcset S T) \<noteq> 0) \<or> (S \<noteq> {} \<and> T = {})"
   6.155 +    by auto
   6.156 +  from this show ?thesis
   6.157 +  proof
   6.158 +    assume "card (extensional_funcset S T) \<noteq> 0"
   6.159 +    from this show ?thesis
   6.160 +      by (auto intro: card_ge_0_finite)
   6.161 +  next
   6.162 +    assume "S \<noteq> {} \<and> T = {}"
   6.163 +    from this show ?thesis
   6.164 +      by (auto simp add: extensional_funcset_empty_range)
   6.165 +  qed
   6.166 +qed
   6.167 +
   6.168  end
     7.1 --- a/src/HOL/Library/Library.thy	Mon Nov 22 17:46:51 2010 +0100
     7.2 +++ b/src/HOL/Library/Library.thy	Mon Nov 22 17:49:12 2010 +0100
     7.3 @@ -14,7 +14,6 @@
     7.4    Countable
     7.5    Diagonalize
     7.6    Dlist
     7.7 -  Enum
     7.8    Eval_Witness
     7.9    Float
    7.10    Formal_Power_Series
     8.1 --- a/src/HOL/Library/Quickcheck_Types.thy	Mon Nov 22 17:46:51 2010 +0100
     8.2 +++ b/src/HOL/Library/Quickcheck_Types.thy	Mon Nov 22 17:49:12 2010 +0100
     8.3 @@ -460,7 +460,7 @@
     8.4  
     8.5  section {* Quickcheck configuration *}
     8.6  
     8.7 -quickcheck_params[default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
     8.8 +quickcheck_params[finite_types = false, default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
     8.9  
    8.10  hide_type non_distrib_lattice flat_complete_lattice bot top
    8.11  
     9.1 --- a/src/HOL/List.thy	Mon Nov 22 17:46:51 2010 +0100
     9.2 +++ b/src/HOL/List.thy	Mon Nov 22 17:49:12 2010 +0100
     9.3 @@ -4877,6 +4877,10 @@
     9.4  definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
     9.5    list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
     9.6  
     9.7 +definition list_ex1
     9.8 +where
     9.9 +  list_ex1_iff: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
    9.10 +
    9.11  text {*
    9.12    Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
    9.13    over @{const list_all} and @{const list_ex} in specifications.
    9.14 @@ -4892,6 +4896,11 @@
    9.15    "list_ex P [] \<longleftrightarrow> False"
    9.16    by (simp_all add: list_ex_iff)
    9.17  
    9.18 +lemma list_ex1_simps [simp, code]:
    9.19 +  "list_ex1 P [] = False"
    9.20 +  "list_ex1 P (x # xs) = (if P x then list_all (\<lambda>y. \<not> P y \<or> x = y) xs else list_ex1 P xs)"
    9.21 +unfolding list_ex1_iff list_all_iff by auto
    9.22 +
    9.23  lemma Ball_set_list_all [code_unfold]:
    9.24    "Ball (set xs) P \<longleftrightarrow> list_all P xs"
    9.25    by (simp add: list_all_iff)
    10.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon Nov 22 17:46:51 2010 +0100
    10.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon Nov 22 17:49:12 2010 +0100
    10.3 @@ -13,6 +13,7 @@
    10.4    "Tools/mirabelle_refute.ML"
    10.5    "Tools/mirabelle_sledgehammer.ML"
    10.6    "Tools/mirabelle_sledgehammer_filter.ML"
    10.7 +  "Tools/sledgehammer_tactic.ML"
    10.8  begin
    10.9  
   10.10  text {*
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Mon Nov 22 17:49:12 2010 +0100
    11.3 @@ -0,0 +1,87 @@
    11.4 +(*  Title:      sledgehammer_tactics.ML
    11.5 +    Author:     Jasmin Blanchette, TU Muenchen
    11.6 +    Copyright   2010
    11.7 +
    11.8 +Sledgehammer as a tactic.
    11.9 +*)
   11.10 +
   11.11 +signature SLEDGEHAMMER_TACTICS =
   11.12 +sig
   11.13 +  val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
   11.14 +  val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
   11.15 +end;
   11.16 +
   11.17 +structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
   11.18 +struct
   11.19 +  
   11.20 +fun run_atp force_full_types timeout i n ctxt goal name =
   11.21 +  let
   11.22 +    val thy = ProofContext.theory_of ctxt
   11.23 +    val params as {full_types, ...} =
   11.24 +      ((if force_full_types then [("full_types", "true")] else [])
   11.25 +       @ [("timeout", Int.toString (Time.toMilliseconds timeout) ^ " ms")])
   11.26 +(*      @ [("overlord", "true")] *)
   11.27 +      |> Sledgehammer_Isar.default_params ctxt
   11.28 +    val prover = Sledgehammer.get_prover thy false name
   11.29 +    val facts = []
   11.30 +    (* Check for constants other than the built-in HOL constants. If none of
   11.31 +       them appear (as should be the case for TPTP problems, unless "auto" or
   11.32 +       "simp" already did its "magic"), we can skip the relevance filter. *)
   11.33 +    val pure_goal =
   11.34 +      not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
   11.35 +                                      not (String.isSubstring "HOL" s))
   11.36 +                        (prop_of goal))
   11.37 +    val problem =
   11.38 +      {state = Proof.init ctxt, goal = goal, subgoal = i, facts = [],
   11.39 +       only = true, subgoal_count = n}
   11.40 +  in
   11.41 +    prover params (K "") problem |> #message
   11.42 +    handle ERROR message => "Error: " ^ message ^ "\n"
   11.43 +  end
   11.44 +
   11.45 +fun to_period ("." :: _) = []
   11.46 +  | to_period ("" :: ss) = to_period ss
   11.47 +  | to_period (s :: ss) = s :: to_period ss
   11.48 +  | to_period [] = []
   11.49 +
   11.50 +val extract_metis_facts =
   11.51 +  space_explode " "
   11.52 +  #> fold (maps o space_explode) ["(", ")", Symbol.ENQ, Symbol.ACK, "\n"]
   11.53 +  #> fst o chop_while (not o member (op =) ["metis", "metisFT"])
   11.54 +  #> (fn _ :: ss => SOME (to_period ss) | _ => NONE)
   11.55 +
   11.56 +val atp = "e" (* or "vampire" *)
   11.57 +
   11.58 +fun thms_of_name ctxt name =
   11.59 +  let
   11.60 +    val lex = Keyword.get_lexicons
   11.61 +    val get = maps (ProofContext.get_fact ctxt o fst)
   11.62 +  in
   11.63 +    Source.of_string name
   11.64 +    |> Symbol.source
   11.65 +    |> Token.source {do_recover=SOME false} lex Position.start
   11.66 +    |> Token.source_proper
   11.67 +    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
   11.68 +    |> Source.exhaust
   11.69 +  end
   11.70 +
   11.71 +fun sledgehammer_with_metis_tac ctxt i th =
   11.72 +  let
   11.73 +    val thy = ProofContext.theory_of ctxt
   11.74 +    val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
   11.75 +    val s = run_atp false timeout i i ctxt th atp
   11.76 +    val xs = these (extract_metis_facts s)
   11.77 +    val ths = maps (thms_of_name ctxt) xs
   11.78 +  in Metis_Tactics.metis_tac ctxt ths i th end
   11.79 +
   11.80 +fun sledgehammer_as_oracle_tac ctxt i th =
   11.81 +  let
   11.82 +    val thy = ProofContext.theory_of ctxt
   11.83 +    val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
   11.84 +    val s = run_atp true timeout i i ctxt th atp
   11.85 +  in
   11.86 +    if is_some (extract_metis_facts s) then Skip_Proof.cheat_tac thy th
   11.87 +    else Seq.empty
   11.88 +  end
   11.89 +
   11.90 +end;
    12.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Nov 22 17:46:51 2010 +0100
    12.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Nov 22 17:49:12 2010 +0100
    12.3 @@ -1,58 +1,144 @@
    12.4  theory MutabelleExtra
    12.5 -imports Complex_Main SML_Quickcheck
    12.6 -(*
    12.7 -  "~/Downloads/Jinja/J/TypeSafe"
    12.8 -  "~/Downloads/Jinja/J/Annotate"
    12.9 -  (* FIXME "Example" *)
   12.10 -  "~/Downloads/Jinja/J/execute_Bigstep"
   12.11 -  "~/Downloads/Jinja/J/execute_WellType"
   12.12 -  "~/Downloads/Jinja/JVM/JVMDefensive"
   12.13 -  "~/Downloads/Jinja/JVM/JVMListExample"
   12.14 -  "~/Downloads/Jinja/BV/BVExec"
   12.15 -  "~/Downloads/Jinja/BV/LBVJVM"
   12.16 -  "~/Downloads/Jinja/BV/BVNoTypeError"
   12.17 -  "~/Downloads/Jinja/BV/BVExample"
   12.18 -  "~/Downloads/Jinja/Compiler/TypeComp"
   12.19 -*)
   12.20 -(*"~/Downloads/NormByEval/NBE"*)
   12.21 -uses "mutabelle.ML"
   12.22 +imports Complex_Main
   12.23 +(*  "~/repos/afp/thys/AVL-Trees/AVL"
   12.24 +  "~/repos/afp/thys/BinarySearchTree/BinaryTree"
   12.25 +  "~/repos/afp/thys/Huffman/Huffman"
   12.26 +  "~/repos/afp/thys/List-Index/List_Index"
   12.27 +  "~/repos/afp/thys/Matrix/Matrix"
   12.28 +  "~/repos/afp/thys/NormByEval/NBE"
   12.29 +  "~/repos/afp/thys/Polynomials/Polynomial"
   12.30 +  "~/repos/afp/thys/Presburger-Automata/Presburger_Automata"
   12.31 +  "~/repos/afp/thys/Abstract-Rewriting/Abstract_Rewriting"*)
   12.32 +uses
   12.33 +     "mutabelle.ML"
   12.34       "mutabelle_extra.ML"
   12.35  begin
   12.36  
   12.37 -(* FIXME !?!?! *)
   12.38 -ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
   12.39 -ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
   12.40 -ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
   12.41 -ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
   12.42 +
   12.43 +section {* configuration *}
   12.44  
   12.45 -quickcheck_params [size = 5, iterations = 1000]
   12.46 +ML {* val log_directory = "" *}
   12.47 +
   12.48 +
   12.49 +quickcheck_params [quiet, finite_types = false, report = false, size = 5, iterations = 1000]
   12.50 +
   12.51  (*
   12.52  nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
   12.53  refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
   12.54  *)
   12.55  ML {* Auto_Tools.time_limit := 10 *}
   12.56  
   12.57 +ML {* val mtds = [
   12.58 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
   12.59 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "random",
   12.60 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "small",
   12.61 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types true) "small"
   12.62 +]
   12.63 +*}
   12.64 +
   12.65 +ML {*
   12.66 +fun mutation_testing_of (name, thy) =
   12.67 +  (MutabelleExtra.random_seed := 1.0;
   12.68 +  MutabelleExtra.thms_of false thy
   12.69 +  |> MutabelleExtra.take_random 200
   12.70 +  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
   12.71 +         @{theory} mtds thms (log_directory ^ "/" ^ name)))
   12.72 +*}
   12.73 +  
   12.74  
   12.75  text {* Uncomment the following ML code to check the counterexample generation with all theorems of Complex_Main. *}
   12.76  
   12.77 +(*
   12.78  ML {*
   12.79 -(*
   12.80 +
   12.81        MutabelleExtra.random_seed := 1.0;
   12.82        MutabelleExtra.thms_of true @{theory Complex_Main}
   12.83        |> MutabelleExtra.take_random 1000000
   12.84        |> (fn thms => List.drop (thms, 1000))
   12.85        |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
   12.86 -             @{theory} [MutabelleExtra.quickcheck_mtd "SML",
   12.87 -                        MutabelleExtra.quickcheck_mtd "code"
   12.88 +             @{theory} [
   12.89 +                        MutabelleExtra.quickcheck_mtd "code",
   12.90 +                        MutabelleExtra.smallcheck_mtd
   12.91                          (*MutabelleExtra.refute_mtd,
   12.92                          MutabelleExtra.nitpick_mtd*)] thms "/tmp/muta.out")
   12.93 +
   12.94 + *}
   12.95  *)
   12.96 +
   12.97 +section {* Mutation testing Isabelle theories *}
   12.98 +
   12.99 +subsection {* List theory *}
  12.100 +
  12.101 +(*
  12.102 +ML {*
  12.103 +mutation_testing_of ("List", @{theory List})
  12.104   *}
  12.105 +*)
  12.106 +
  12.107 +section {* Mutation testing AFP theories *}
  12.108 +
  12.109 +subsection {* AVL-Trees *}
  12.110 +
  12.111 +(*
  12.112 +ML {*
  12.113 +mutation_testing_of ("AVL-Trees", @{theory AVL})
  12.114 + *}
  12.115 +*)
  12.116 +
  12.117 +subsection {* BinaryTree *}
  12.118 +
  12.119 +(*
  12.120 +ML {*
  12.121 +mutation_testing_of ("BinaryTree", @{theory BinaryTree})
  12.122 + *}
  12.123 +*)
  12.124 +
  12.125 +subsection {* Huffman *}
  12.126 +
  12.127 +(*
  12.128 +ML {*
  12.129 +mutation_testing_of ("Huffman", @{theory Huffman})
  12.130 + *}
  12.131 +*)
  12.132  
  12.133 -(* FIXME !?!?! *)
  12.134 -ML {* Output.Private_Hooks.tracing_fn := old_tr *}
  12.135 -ML {* Output.Private_Hooks.writeln_fn := old_wr *}
  12.136 -ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
  12.137 -ML {* Output.Private_Hooks.warning_fn := old_wa *}
  12.138 +subsection {* List_Index *}
  12.139 +
  12.140 +(*
  12.141 +ML {*
  12.142 +mutation_testing_of ("List_Index", @{theory List_Index})
  12.143 + *}
  12.144 +*)
  12.145 +
  12.146 +subsection {* Matrix *}
  12.147 +
  12.148 +(*
  12.149 +ML {*
  12.150 +mutation_testing_of ("Matrix", @{theory Matrix})
  12.151 + *}
  12.152 +*)
  12.153 +
  12.154 +subsection {* NBE *}
  12.155 +
  12.156 +(*
  12.157 +ML {*
  12.158 +mutation_testing_of ("NBE", @{theory NBE})
  12.159 + *}
  12.160 +*)
  12.161 +
  12.162 +subsection {* Polynomial *}
  12.163 +
  12.164 +(*
  12.165 +ML {*
  12.166 +mutation_testing_of ("Polynomial", @{theory Polynomial})
  12.167 + *}
  12.168 +*)
  12.169 +
  12.170 +subsection {* Presburger Automata *}
  12.171 +
  12.172 +(*
  12.173 +ML {*
  12.174 +mutation_testing_of ("Presburger_Automata", @{theory Presburger_Automata})
  12.175 + *}
  12.176 +*)
  12.177  
  12.178  end
    13.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Mon Nov 22 17:46:51 2010 +0100
    13.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Nov 22 17:49:12 2010 +0100
    13.3 @@ -498,7 +498,7 @@
    13.4  
    13.5  fun is_executable thy insts th =
    13.6    ((Quickcheck.test_term
    13.7 -      (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 1)))) (ProofContext.init_global thy))
    13.8 +      ((Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) (ProofContext.init_global thy))
    13.9        (SOME (!testgen_name)) (preprocess thy insts (prop_of th));
   13.10      Output.urgent_message "executable"; true) handle ERROR s =>
   13.11      (Output.urgent_message ("not executable: " ^ s); false));
   13.12 @@ -507,7 +507,7 @@
   13.13   | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 
   13.14       (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs));
   13.15       ((x, pretty (the_default [] (fst (Quickcheck.test_term
   13.16 -       (Context.proof_map (Quickcheck.map_test_params (apfst (K (sz, qciter))))
   13.17 +       ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter)
   13.18           (ProofContext.init_global usedthy))
   13.19         (SOME (!testgen_name)) (preprocess usedthy insts x))))) :: acc))
   13.20            handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
    14.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Nov 22 17:46:51 2010 +0100
    14.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Nov 22 17:49:12 2010 +0100
    14.3 @@ -8,7 +8,7 @@
    14.4  
    14.5  val take_random : int -> 'a list -> 'a list
    14.6  
    14.7 -datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
    14.8 +datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
    14.9  type timing = (string * int) list
   14.10  
   14.11  type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
   14.12 @@ -20,7 +20,10 @@
   14.13  type entry = string * bool * subentry list
   14.14  type report = entry list
   14.15  
   14.16 -val quickcheck_mtd : string -> mtd
   14.17 +val quickcheck_mtd : (Proof.context -> Proof.context) -> string -> mtd
   14.18 +
   14.19 +val solve_direct_mtd : mtd
   14.20 +val try_mtd : mtd
   14.21  (*
   14.22  val refute_mtd : mtd
   14.23  val nitpick_mtd : mtd
   14.24 @@ -45,15 +48,17 @@
   14.25  
   14.26  
   14.27  (* mutation options *)
   14.28 -val max_mutants = 4
   14.29 -val num_mutations = 1
   14.30 +(*val max_mutants = 4
   14.31 +val num_mutations = 1*)
   14.32  (* soundness check: *)
   14.33 -(*val max_mutants = 1
   14.34 -val num_mutations = 0*)
   14.35 +val max_mutants =  10
   14.36 +val num_mutations = 1
   14.37  
   14.38  (* quickcheck options *)
   14.39  (*val quickcheck_generator = "SML"*)
   14.40  
   14.41 +(* Another Random engine *)
   14.42 +
   14.43  exception RANDOM;
   14.44  
   14.45  fun rmod x y = x - y * Real.realFloor (x / y);
   14.46 @@ -73,7 +78,26 @@
   14.47    if h < l orelse l < 0 then raise RANDOM
   14.48    else l + Real.floor (rmod (random ()) (real (h - l + 1)));
   14.49  
   14.50 -datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error
   14.51 +fun take_random 0 _ = []
   14.52 +  | take_random _ [] = []
   14.53 +  | take_random n xs =
   14.54 +    let val j = random_range 0 (length xs - 1) in
   14.55 +      Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
   14.56 +    end
   14.57 +  
   14.58 +(* possible outcomes *)
   14.59 +
   14.60 +datatype outcome = GenuineCex | PotentialCex | NoCex | Donno | Timeout | Error | Solved | Unsolved
   14.61 +
   14.62 +fun string_of_outcome GenuineCex = "GenuineCex"
   14.63 +  | string_of_outcome PotentialCex = "PotentialCex"
   14.64 +  | string_of_outcome NoCex = "NoCex"
   14.65 +  | string_of_outcome Donno = "Donno"
   14.66 +  | string_of_outcome Timeout = "Timeout"
   14.67 +  | string_of_outcome Error = "Error"
   14.68 +  | string_of_outcome Solved = "Solved"
   14.69 +  | string_of_outcome Unsolved = "Unsolved"
   14.70 +
   14.71  type timing = (string * int) list
   14.72  
   14.73  type mtd = string * (theory -> term -> outcome * (timing * (int * Quickcheck.report list) list option))
   14.74 @@ -85,25 +109,49 @@
   14.75  type entry = string * bool * subentry list
   14.76  type report = entry list
   14.77  
   14.78 -fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
   14.79 -  | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T)
   14.80 +(* possible invocations *)
   14.81  
   14.82 -fun preprocess thy insts t = Object_Logic.atomize_term thy
   14.83 - (map_types (inst_type insts) (Mutabelle.freeze t));
   14.84 +(** quickcheck **)
   14.85  
   14.86 -fun invoke_quickcheck quickcheck_generator thy t =
   14.87 +fun invoke_quickcheck change_options quickcheck_generator thy t =
   14.88    TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
   14.89        (fn _ =>
   14.90 -          case Quickcheck.test_term (ProofContext.init_global thy)
   14.91 -              (SOME quickcheck_generator) (preprocess thy [] t) of
   14.92 -            (NONE, (time_report, report)) => (NoCex, (time_report, report))
   14.93 -          | (SOME _, (time_report, report)) => (GenuineCex, (time_report, report))) ()
   14.94 +          case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
   14.95 +              (SOME quickcheck_generator, []) [t] of
   14.96 +            (NONE, _) => (NoCex, ([], NONE))
   14.97 +          | (SOME _, _) => (GenuineCex, ([], NONE))) ()
   14.98    handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
   14.99  
  14.100 -fun quickcheck_mtd quickcheck_generator =
  14.101 -  ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck quickcheck_generator)
  14.102 +fun quickcheck_mtd change_options quickcheck_generator =
  14.103 +  ("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options quickcheck_generator)
  14.104 +
  14.105 +(** solve direct **)
  14.106 + 
  14.107 +fun invoke_solve_direct thy t =
  14.108 +  let
  14.109 +    val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) 
  14.110 +  in
  14.111 +    case Solve_Direct.solve_direct false state of
  14.112 +      (true, _) => (Solved, ([], NONE))
  14.113 +    | (false, _) => (Unsolved, ([], NONE))
  14.114 +  end
  14.115  
  14.116 -  (*
  14.117 +val solve_direct_mtd = ("solve_direct", invoke_solve_direct) 
  14.118 +
  14.119 +(** try **)
  14.120 +
  14.121 +fun invoke_try thy t =
  14.122 +  let
  14.123 +    val state = Proof.theorem NONE (K I) (map (single o rpair []) [t]) (ProofContext.init_global thy) 
  14.124 +  in
  14.125 +    case Try.invoke_try NONE state of
  14.126 +      true => (Solved, ([], NONE))
  14.127 +    | false => (Unsolved, ([], NONE))
  14.128 +  end
  14.129 +
  14.130 +val try_mtd = ("try", invoke_try)
  14.131 +
  14.132 +(*
  14.133  fun invoke_refute thy t =
  14.134    let
  14.135      val res = MyRefute.refute_term thy [] t
  14.136 @@ -185,6 +233,8 @@
  14.137  val nitpick_mtd = ("nitpick", invoke_nitpick)
  14.138  *)
  14.139  
  14.140 +(* filtering forbidden theorems and mutants *)
  14.141 +
  14.142  val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]
  14.143  
  14.144  val forbidden =
  14.145 @@ -200,7 +250,6 @@
  14.146    (@{const_name "top_fun_inst.top_fun"}, "'a"),
  14.147    (@{const_name "Pure.term"}, "'a"),
  14.148    (@{const_name "top_class.top"}, "'a"),
  14.149 -  (@{const_name "HOL.equal"}, "'a"),
  14.150    (@{const_name "Quotient.Quot_True"}, "'a")(*,
  14.151    (@{const_name "uminus"}, "'a"),
  14.152    (@{const_name "Nat.size"}, "'a"),
  14.153 @@ -211,7 +260,7 @@
  14.154    "nibble"]
  14.155  
  14.156  val forbidden_consts =
  14.157 - [@{const_name nibble_pair_of_char}]
  14.158 + [@{const_name nibble_pair_of_char}, @{const_name "TYPE"}]
  14.159  
  14.160  fun is_forbidden_theorem (s, th) =
  14.161    let val consts = Term.add_const_names (prop_of th) [] in
  14.162 @@ -220,7 +269,8 @@
  14.163      length (space_explode "." s) <> 2 orelse
  14.164      String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
  14.165      String.isSuffix "_def" s orelse
  14.166 -    String.isSuffix "_raw" s
  14.167 +    String.isSuffix "_raw" s orelse
  14.168 +    String.isPrefix "term_of" (List.last (space_explode "." s))
  14.169    end
  14.170  
  14.171  val forbidden_mutant_constnames =
  14.172 @@ -235,23 +285,54 @@
  14.173   @{const_name "top_fun_inst.top_fun"},
  14.174   @{const_name "Pure.term"},
  14.175   @{const_name "top_class.top"},
  14.176 - @{const_name "HOL.equal"},
  14.177 - @{const_name "Quotient.Quot_True"}]
  14.178 + (*@{const_name "HOL.equal"},*)
  14.179 + @{const_name "Quotient.Quot_True"}
  14.180 + (*@{const_name "==>"}, @{const_name "=="}*)]
  14.181 +
  14.182 +val forbidden_mutant_consts =
  14.183 +  [
  14.184 +   (@{const_name "Groups.zero_class.zero"}, @{typ "prop => prop => prop"}),
  14.185 +   (@{const_name "Groups.one_class.one"}, @{typ "prop => prop => prop"}),
  14.186 +   (@{const_name "Groups.plus_class.plus"}, @{typ "prop => prop => prop"}),
  14.187 +   (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
  14.188 +   (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
  14.189 +   (@{const_name "Rings.inverse_class.divide"}, @{typ "prop => prop => prop"}),
  14.190 +   (@{const_name "Lattices.semilattice_inf_class.inf"}, @{typ "prop => prop => prop"}),
  14.191 +   (@{const_name "Lattices.semilattice_sup_class.sup"}, @{typ "prop => prop => prop"}),
  14.192 +   (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
  14.193 +   (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
  14.194 +   (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
  14.195 +   (@{const_name "Divides.div_class.mod"}, @{typ "prop => prop => prop"}),
  14.196 +   (@{const_name "Divides.div_class.div"}, @{typ "prop => prop => prop"}),
  14.197 +   (@{const_name "GCD.gcd_class.gcd"}, @{typ "prop => prop => prop"}),
  14.198 +   (@{const_name "GCD.gcd_class.lcm"}, @{typ "prop => prop => prop"}),
  14.199 +   (@{const_name "Orderings.bot_class.bot"}, @{typ "bool => prop"}),
  14.200 +   (@{const_name "Groups.one_class.one"}, @{typ "bool => prop"}),
  14.201 +   (@{const_name "Groups.zero_class.zero"},@{typ "bool => prop"})]
  14.202  
  14.203  fun is_forbidden_mutant t =
  14.204    let
  14.205 -    val consts = Term.add_const_names t []
  14.206 +    val const_names = Term.add_const_names t []
  14.207 +    val consts = Term.add_consts t []
  14.208    in
  14.209 -    exists (String.isPrefix "Nitpick") consts orelse
  14.210 -    exists (String.isSubstring "_sumC") consts orelse
  14.211 -    exists (member (op =) forbidden_mutant_constnames) consts
  14.212 +    exists (String.isPrefix "Nitpick") const_names orelse
  14.213 +    exists (String.isSubstring "_sumC") const_names orelse
  14.214 +    exists (member (op =) forbidden_mutant_constnames) const_names orelse
  14.215 +    exists (member (op =) forbidden_mutant_consts) consts
  14.216    end
  14.217  
  14.218 +(* executable via quickcheck *)
  14.219 +
  14.220  fun is_executable_term thy t =
  14.221 -  can (TimeLimit.timeLimit (seconds 2.0)
  14.222 -    (Quickcheck.test_term
  14.223 -      (Context.proof_map (Quickcheck.map_test_params (apfst (K (1, 0)))) (ProofContext.init_global thy))
  14.224 -      (SOME "SML"))) (preprocess thy [] t)
  14.225 +  let
  14.226 +    val ctxt = ProofContext.init_global thy
  14.227 +  in
  14.228 +    can (TimeLimit.timeLimit (seconds 2.0)
  14.229 +      (Quickcheck.test_goal_terms
  14.230 +        ((Config.put Quickcheck.finite_types true #>
  14.231 +          Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
  14.232 +        (SOME "random" , []))) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
  14.233 +  end
  14.234  
  14.235  fun is_executable_thm thy th = is_executable_term thy (prop_of th)
  14.236  
  14.237 @@ -267,44 +348,47 @@
  14.238  
  14.239  val count = length oo filter o equal
  14.240  
  14.241 -fun take_random 0 _ = []
  14.242 -  | take_random _ [] = []
  14.243 -  | take_random n xs =
  14.244 -    let val j = random_range 0 (length xs - 1) in
  14.245 -      Library.nth xs j :: take_random (n - 1) (nth_drop j xs)
  14.246 -    end
  14.247 -
  14.248  fun cpu_time description f =
  14.249    let
  14.250      val start = start_timing ()
  14.251      val result = Exn.capture f ()
  14.252      val time = Time.toMilliseconds (#cpu (end_timing start))
  14.253    in (Exn.release result, (description, time)) end
  14.254 -
  14.255 +(*
  14.256 +fun unsafe_invoke_mtd thy (mtd_name, invoke_mtd) t =
  14.257 +  let
  14.258 +    val _ = Output.urgent_message ("Invoking " ^ mtd_name)
  14.259 +    val ((res, (timing, reports)), time) = cpu_time "total time" (fn () => invoke_mtd thy t
  14.260 +      handle ERROR s => (tracing s; (Error, ([], NONE))))
  14.261 +    val _ = Output.urgent_message (" Done")
  14.262 +  in (res, (time :: timing, reports)) end
  14.263 +*)  
  14.264  fun safe_invoke_mtd thy (mtd_name, invoke_mtd) t =
  14.265    let
  14.266      val _ = Output.urgent_message ("Invoking " ^ mtd_name)
  14.267 -    val ((res, (timing, reports)), time) = cpu_time "total time"
  14.268 -      (fn () => case try (invoke_mtd thy) t of
  14.269 +    val (res, (timing, reports)) = (*cpu_time "total time"
  14.270 +      (fn () => *)case try (invoke_mtd thy) t of
  14.271            SOME (res, (timing, reports)) => (res, (timing, reports))
  14.272          | NONE => (Output.urgent_message ("**** PROBLEMS WITH " ^ Syntax.string_of_term_global thy t);
  14.273 -           (Error , ([], NONE))))
  14.274 +           (Error, ([], NONE)))
  14.275      val _ = Output.urgent_message (" Done")
  14.276 -  in (res, (time :: timing, reports)) end
  14.277 +  in (res, (timing, reports)) end
  14.278  
  14.279  (* theory -> term list -> mtd -> subentry *)
  14.280 -(*
  14.281 +
  14.282  fun test_mutants_using_one_method thy mutants (mtd_name, invoke_mtd) =
  14.283    let
  14.284 -     val res = map (safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
  14.285 +     val res = map (fst o safe_invoke_mtd thy (mtd_name, invoke_mtd)) mutants
  14.286    in
  14.287      (mtd_name, count GenuineCex res, count PotentialCex res, count NoCex res,
  14.288       count Donno res, count Timeout res, count Error res)
  14.289    end
  14.290  
  14.291 +(* creating entries *)
  14.292 +
  14.293  fun create_entry thy thm exec mutants mtds =
  14.294    (Thm.get_name_hint thm, exec, map (test_mutants_using_one_method thy mutants) mtds)
  14.295 -*)
  14.296 +
  14.297  fun create_detailed_entry thy thm exec mutants mtds =
  14.298    let
  14.299      fun create_mutant_subentry mutant = (mutant,
  14.300 @@ -318,13 +402,14 @@
  14.301  fun mutate_theorem create_entry thy mtds thm =
  14.302    let
  14.303      val exec = is_executable_thm thy thm
  14.304 -    val _ = Output.urgent_message (if exec then "EXEC" else "NOEXEC")
  14.305 +    val _ = Output.tracing (if exec then "EXEC" else "NOEXEC")
  14.306      val mutants =
  14.307            (if num_mutations = 0 then
  14.308               [Thm.prop_of thm]
  14.309             else
  14.310               Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden
  14.311                                    num_mutations)
  14.312 +             |> tap (fn muts => tracing ("mutants: " ^ string_of_int (length muts)))
  14.313               |> filter_out is_forbidden_mutant
  14.314      val mutants =
  14.315        if exec then
  14.316 @@ -344,6 +429,7 @@
  14.317            |> map Mutabelle.freeze |> map freezeT
  14.318  (*          |> filter (not o is_forbidden_mutant) *)
  14.319            |> List.mapPartial (try (Sign.cert_term thy))
  14.320 +          |> List.filter (is_some o try (cterm_of thy))
  14.321      val _ = map (fn t => Output.urgent_message ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants
  14.322    in
  14.323      create_entry thy thm exec mutants mtds
  14.324 @@ -352,13 +438,6 @@
  14.325  (* theory -> mtd list -> thm list -> report *)
  14.326  val mutate_theorems = map ooo mutate_theorem
  14.327  
  14.328 -fun string_of_outcome GenuineCex = "GenuineCex"
  14.329 -  | string_of_outcome PotentialCex = "PotentialCex"
  14.330 -  | string_of_outcome NoCex = "NoCex"
  14.331 -  | string_of_outcome Donno = "Donno"
  14.332 -  | string_of_outcome Timeout = "Timeout"
  14.333 -  | string_of_outcome Error = "Error"
  14.334 -
  14.335  fun string_of_mutant_subentry thy thm_name (t, results) =
  14.336    "mutant: " ^ Syntax.string_of_term_global thy t ^ "\n" ^
  14.337    space_implode "; "
  14.338 @@ -378,12 +457,12 @@
  14.339          cat_lines (map (fn (size, [report]) =>
  14.340            "size " ^ string_of_int size ^ ": " ^ string_of_report report) (rev reports))
  14.341      fun string_of_mtd_result (mtd_name, (outcome, (timing, reports))) =
  14.342 -      mtd_name ^ ": " ^ string_of_outcome outcome ^ "; " ^
  14.343 -      space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing)
  14.344 +      mtd_name ^ ": " ^ string_of_outcome outcome
  14.345 +      (*" with time " ^ " (" ^ space_implode "; " (map (fn (s, t) => (s ^ ": " ^ string_of_int t)) timing) ^ ")"*)
  14.346        (*^ "\n" ^ string_of_reports reports*)
  14.347    in
  14.348      "mutant of " ^ thm_name ^ ":\n"
  14.349 -    ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ cat_lines (map string_of_mtd_result results)
  14.350 +    ^ unyxml (Syntax.string_of_term_global thy t) ^ "\n" ^ space_implode "; " (map string_of_mtd_result results)
  14.351    end
  14.352  
  14.353  fun string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) = 
  14.354 @@ -394,8 +473,7 @@
  14.355  fun theoryfile_string_of_mutant_subentry thy thm_name (i, (t, results)) =
  14.356    "lemma " ^ thm_name ^ "_" ^ string_of_int (i + 1) ^ ":\n" ^
  14.357    "\"" ^ unyxml (Syntax.string_of_term_global thy t) ^
  14.358 -  "\" \nquickcheck[generator = SML]\nquickcheck[generator = predicate_compile_wo_ff]\n" ^
  14.359 -  "quickcheck[generator = predicate_compile_ff_nofs]\noops\n"
  14.360 +  "\" \nquickcheck\noops\n"
  14.361  
  14.362  fun theoryfile_string_of_detailed_entry thy (thm_name, exec, t, mutant_subentries) =
  14.363    "subsubsection {* mutants of " ^ thm_name ^ " *}\n\n" ^
  14.364 @@ -409,10 +487,12 @@
  14.365    Int.toString potential_cex ^ "= " ^ Int.toString no_cex ^ "- " ^
  14.366    Int.toString donno ^ "? " ^ Int.toString timeout ^ "T " ^
  14.367    Int.toString error ^ "!"
  14.368 +
  14.369  (* entry -> string *)
  14.370  fun string_for_entry (thm_name, exec, subentries) =
  14.371    thm_name ^ " " ^ (if exec then "[exe]" else "[noexe]") ^ ":\n" ^
  14.372    cat_lines (map string_for_subentry subentries) ^ "\n"
  14.373 +
  14.374  (* report -> string *)
  14.375  fun string_for_report report = cat_lines (map string_for_entry report)
  14.376  
  14.377 @@ -424,15 +504,16 @@
  14.378  fun mutate_theorems_and_write_report thy mtds thms file_name =
  14.379    let
  14.380      val _ = Output.urgent_message "Starting Mutabelle..."
  14.381 -    val Quickcheck.Test_Params test_params = Quickcheck.test_params_of (ProofContext.init_global thy)
  14.382 +    val ctxt = ProofContext.init_global thy
  14.383      val path = Path.explode file_name
  14.384      (* for normal report: *)
  14.385 -    (*val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)*)
  14.386 -    (*for detailled report: *)
  14.387 -    val (gen_create_entry, gen_string_for_entry) =
  14.388 -      (create_detailed_entry, string_of_detailed_entry thy)
  14.389 -    val (gen_create_entry, gen_string_for_entry) =
  14.390 -      (create_detailed_entry, theoryfile_string_of_detailed_entry thy)
  14.391 +    (*
  14.392 +    val (gen_create_entry, gen_string_for_entry) = (create_entry, string_for_entry)
  14.393 +    *)
  14.394 +    (* for detailled report: *)
  14.395 +    val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, string_of_detailed_entry thy)
  14.396 +    (* for theory creation: *)
  14.397 +    (*val (gen_create_entry, gen_string_for_entry) = (create_detailed_entry, theoryfile_string_of_detailed_entry thy)*)
  14.398    in
  14.399      File.write path (
  14.400      "Mutation options = "  ^
  14.401 @@ -440,8 +521,8 @@
  14.402        "; num_mutations: " ^ string_of_int num_mutations ^ "\n" ^
  14.403      "QC options = " ^
  14.404        (*"quickcheck_generator: " ^ quickcheck_generator ^ ";*)
  14.405 -      "size: " ^ string_of_int (#size test_params) ^
  14.406 -      "; iterations: " ^ string_of_int (#iterations test_params) ^ "\n");
  14.407 +      "size: " ^ string_of_int (Config.get ctxt Quickcheck.size) ^
  14.408 +      "; iterations: " ^ string_of_int (Config.get ctxt Quickcheck.iterations) ^ "\n");
  14.409      map (File.append path o gen_string_for_entry o mutate_theorem gen_create_entry thy mtds) thms;
  14.410      ()
  14.411    end
    15.1 --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Nov 22 17:46:51 2010 +0100
    15.2 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy	Mon Nov 22 17:49:12 2010 +0100
    15.3 @@ -50,8 +50,8 @@
    15.4  
    15.5  lemma
    15.6    "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
    15.7 -quickcheck[generator = small_generators_depth_14, iterations = 1, size = 1, expect = no_counterexample]
    15.8 -quickcheck[generator = small_generators_depth_15, iterations = 1, size = 1, expect = counterexample]
    15.9 +quickcheck[generator = small_generators_depth_14, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = no_counterexample, timeout = 60]
   15.10 +quickcheck[generator = small_generators_depth_15, finite_types = false, iterations = 1, size = 1, timeout = 60.0, expect = counterexample, timeout = 60]
   15.11  oops
   15.12  
   15.13  
    16.1 --- a/src/HOL/Quickcheck.thy	Mon Nov 22 17:46:51 2010 +0100
    16.2 +++ b/src/HOL/Quickcheck.thy	Mon Nov 22 17:49:12 2010 +0100
    16.3 @@ -3,7 +3,7 @@
    16.4  header {* A simple counterexample generator *}
    16.5  
    16.6  theory Quickcheck
    16.7 -imports Random Code_Evaluation
    16.8 +imports Random Code_Evaluation Enum
    16.9  uses ("Tools/quickcheck_generators.ML")
   16.10  begin
   16.11  
    17.1 --- a/src/HOL/Smallcheck.thy	Mon Nov 22 17:46:51 2010 +0100
    17.2 +++ b/src/HOL/Smallcheck.thy	Mon Nov 22 17:49:12 2010 +0100
    17.3 @@ -16,7 +16,7 @@
    17.4  instantiation unit :: small
    17.5  begin
    17.6  
    17.7 -definition "find_first f d = f ()"
    17.8 +definition "small f d = f ()"
    17.9  
   17.10  instance ..
   17.11  
   17.12 @@ -48,6 +48,73 @@
   17.13  
   17.14  end
   17.15  
   17.16 +section {* full small value generator type classes *}
   17.17 +
   17.18 +class full_small = term_of +
   17.19 +fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
   17.20 +
   17.21 +instantiation unit :: full_small
   17.22 +begin
   17.23 +
   17.24 +definition "full_small f d = f (Code_Evaluation.valtermify ())"
   17.25 +
   17.26 +instance ..
   17.27 +
   17.28 +end
   17.29 +
   17.30 +instantiation int :: full_small
   17.31 +begin
   17.32 +
   17.33 +function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option"
   17.34 +  where "full_small' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small' f d (i + 1)))"
   17.35 +by pat_completeness auto
   17.36 +
   17.37 +termination 
   17.38 +  by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto
   17.39 +
   17.40 +definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
   17.41 +
   17.42 +instance ..
   17.43 +
   17.44 +end
   17.45 +
   17.46 +instantiation prod :: (full_small, full_small) full_small
   17.47 +begin
   17.48 +ML {* @{const_name "Pair"} *}
   17.49 +definition
   17.50 +  "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
   17.51 +    %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
   17.52 +
   17.53 +instance ..
   17.54 +
   17.55 +end
   17.56 +
   17.57 +instantiation "fun" :: ("{equal, full_small}", full_small) full_small
   17.58 +begin
   17.59 +
   17.60 +fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
   17.61 +where
   17.62 +  "full_small_fun' f i d = (if i > 1 then
   17.63 +    full_small (%(a, at). full_small (%(b, bt).
   17.64 +      full_small_fun' (%(g, gt). f (g(a := b),
   17.65 +        (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
   17.66 +         
   17.67 +(Code_Evaluation.Const (STR ''Fun.fun_upd'')
   17.68 +
   17.69 +(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
   17.70 +
   17.71 + (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then
   17.72 +  full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
   17.73 +
   17.74 +definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
   17.75 +where
   17.76 +  "full_small_fun f d = full_small_fun' f d d" 
   17.77 +
   17.78 +
   17.79 +instance ..
   17.80 +
   17.81 +end
   17.82 +
   17.83  subsection {* Defining combinators for any first-order data type *}
   17.84  
   17.85  definition catch_match :: "term list option => term list option => term list option"
   17.86 @@ -59,7 +126,7 @@
   17.87  
   17.88  use "Tools/smallvalue_generators.ML"
   17.89  
   17.90 -(* We do not activate smallcheck yet. 
   17.91 +(* We do not activate smallcheck yet.
   17.92  setup {* Smallvalue_Generators.setup *}
   17.93  *)
   17.94  
    18.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Mon Nov 22 17:46:51 2010 +0100
    18.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Nov 22 17:49:12 2010 +0100
    18.3 @@ -12,7 +12,10 @@
    18.4      -> seed -> (('a -> 'b) * (unit -> term)) * seed
    18.5    val perhaps_constrain: theory -> (typ * sort) list -> (string * sort) list
    18.6      -> (string * sort -> string * sort) option
    18.7 -  val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
    18.8 +  val ensure_sort_datatype:
    18.9 +    sort * (Datatype.config -> Datatype.descr -> (string * sort) list -> string list -> string ->
   18.10 +      string list * string list -> typ list * typ list -> theory -> theory)
   18.11 +    -> Datatype.config -> string list -> theory -> theory
   18.12    val compile_generator_expr:
   18.13      Proof.context -> term -> int -> term list option * (bool list * bool)
   18.14    val put_counterexample: (unit -> int -> seed -> term list option * seed)
   18.15 @@ -279,30 +282,29 @@
   18.16    in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
   18.17    end handle Sorts.CLASS_ERROR _ => NONE;
   18.18  
   18.19 -fun ensure_random_datatype config raw_tycos thy =
   18.20 +fun ensure_sort_datatype (sort, instantiate_datatype) config raw_tycos thy =
   18.21    let
   18.22      val algebra = Sign.classes_of thy;
   18.23      val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
   18.24        Datatype.the_descr thy raw_tycos;
   18.25      val typerep_vs = (map o apsnd)
   18.26        (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
   18.27 -    val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
   18.28 +    val sort_insts = (map (rpair sort) o flat o maps snd o maps snd)
   18.29        (Datatype_Aux.interpret_construction descr typerep_vs
   18.30          { atyp = single, dtyp = (K o K o K) [] });
   18.31      val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
   18.32        (Datatype_Aux.interpret_construction descr typerep_vs
   18.33          { atyp = K [], dtyp = K o K });
   18.34      val has_inst = exists (fn tyco =>
   18.35 -      can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
   18.36 +      can (Sorts.mg_domain algebra tyco) sort) tycos;
   18.37    in if has_inst then thy
   18.38 -    else case perhaps_constrain thy (random_insts @ term_of_insts) typerep_vs
   18.39 -     of SOME constrain => instantiate_random_datatype config descr
   18.40 +    else case perhaps_constrain thy (sort_insts @ term_of_insts) typerep_vs
   18.41 +     of SOME constrain => instantiate_datatype config descr
   18.42            (map constrain typerep_vs) tycos prfx (names, auxnames)
   18.43              ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
   18.44        | NONE => thy
   18.45    end;
   18.46  
   18.47 -
   18.48  (** building and compiling generator expressions **)
   18.49  
   18.50  structure Counterexample = Proof_Data (
   18.51 @@ -389,7 +391,7 @@
   18.52    let
   18.53      val Ts = (map snd o fst o strip_abs) t;
   18.54      val thy = ProofContext.theory_of ctxt
   18.55 -  in if Quickcheck.report ctxt then
   18.56 +  in if Config.get ctxt Quickcheck.report then
   18.57      let
   18.58        val t' = mk_reporting_generator_expr thy t Ts;
   18.59        val compile = Code_Runtime.dynamic_value_strict
   18.60 @@ -410,9 +412,9 @@
   18.61  (** setup **)
   18.62  
   18.63  val setup =
   18.64 -  Datatype.interpretation ensure_random_datatype
   18.65 +  Datatype.interpretation (ensure_sort_datatype (@{sort random}, instantiate_random_datatype))
   18.66    #> Code_Target.extend_target (target, (Code_Runtime.target, K I))
   18.67    #> Context.theory_map
   18.68 -    (Quickcheck.add_generator ("code", compile_generator_expr));
   18.69 +    (Quickcheck.add_generator ("random", compile_generator_expr));
   18.70  
   18.71  end;
    19.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 17:46:51 2010 +0100
    19.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 17:49:12 2010 +0100
    19.3 @@ -6,7 +6,6 @@
    19.4  
    19.5  signature SMALLVALUE_GENERATORS =
    19.6  sig
    19.7 -  val ensure_smallvalue_datatype: Datatype.config -> string list -> theory -> theory
    19.8    val compile_generator_expr:
    19.9      Proof.context -> term -> int -> term list option * (bool list * bool)
   19.10    val put_counterexample: (unit -> int -> term list option)
   19.11 @@ -51,10 +50,12 @@
   19.12  
   19.13  (** abstract syntax **)
   19.14  
   19.15 +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
   19.16 +
   19.17  val size = @{term "i :: code_numeral"}
   19.18  val size_pred = @{term "(i :: code_numeral) - 1"}
   19.19  val size_ge_zero = @{term "(i :: code_numeral) > 0"}
   19.20 -fun test_function T = Free ("f", T --> @{typ "term list option"})
   19.21 +fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
   19.22  
   19.23  fun mk_none_continuation (x, y) =
   19.24    let
   19.25 @@ -75,16 +76,23 @@
   19.26  fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral}
   19.27    --> @{typ "Code_Evaluation.term list option"}
   19.28  
   19.29 +val full_smallN = "full_small";
   19.30 +
   19.31 +fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
   19.32 +  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
   19.33 + 
   19.34  fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) =
   19.35    let
   19.36 -    val smallsN = map (prefix (smallN ^ "_")) (names @ auxnames);
   19.37 -    val smalls = map2 (fn name => fn T => Free (name, smallT T))
   19.38 +    val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
   19.39 +    val smalls = map2 (fn name => fn T => Free (name, full_smallT T))
   19.40        smallsN (Ts @ Us)
   19.41      fun mk_small_call T =
   19.42        let
   19.43 -        val small = Const (@{const_name "Smallcheck.small_class.small"}, smallT T)        
   19.44 +        val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)        
   19.45        in
   19.46 -        (T, (fn t => small $ absdummy (T, t) $ size_pred))
   19.47 +        (T, (fn t => small $
   19.48 +          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   19.49 +          $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
   19.50        end
   19.51      fun mk_small_aux_call fTs (k, _) (tyco, Ts) =
   19.52        let
   19.53 @@ -92,14 +100,23 @@
   19.54          val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
   19.55          val small = nth smalls k
   19.56        in
   19.57 -        (T, (fn t => small $ absdummy (T, t) $ size_pred))
   19.58 +       (T, (fn t => small $
   19.59 +          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
   19.60 +            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))  
   19.61        end
   19.62      fun mk_consexpr simpleT (c, xs) =
   19.63        let
   19.64          val (Ts, fns) = split_list xs
   19.65          val constr = Const (c, Ts ---> simpleT)
   19.66 -        val bounds = map Bound (((length xs) - 1) downto 0)
   19.67 -        val start_term = test_function simpleT $ (list_comb (constr, bounds))
   19.68 +        val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
   19.69 +        val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
   19.70 +        val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
   19.71 +        val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
   19.72 +        val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
   19.73 +          bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
   19.74 +        val start_term = test_function simpleT $ 
   19.75 +        (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
   19.76 +          $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
   19.77        in fold_rev (fn f => fn t => f t) fns start_term end
   19.78      fun mk_rhs exprs =
   19.79          @{term "If :: bool => term list option => term list option => term list option"}
   19.80 @@ -117,36 +134,21 @@
   19.81    end
   19.82      
   19.83  val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto}
   19.84 -
   19.85 -fun gen_inst_state_tac ctxt rel st =
   19.86 -  case Term.add_vars (prop_of st) [] of
   19.87 -    [v as (_, T)] =>
   19.88 -      let
   19.89 -        val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
   19.90 -        val rel' = cert rel
   19.91 -        val st' = Thm.incr_indexes (#maxidx (Thm.rep_cterm rel') + 1) st (*FIXME??*)
   19.92 -      in        
   19.93 -        PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
   19.94 -      end
   19.95 -  | _ => Seq.empty;
   19.96 -
   19.97 +  
   19.98  fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   19.99    let
  19.100      val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
  19.101      val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
  19.102 -    fun my_relation_tac ctxt st =
  19.103 +    fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
  19.104 +      Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
  19.105 +    fun mk_termination_measure T =
  19.106        let
  19.107 -        val ((_ $ (_ $ rel)) :: tl) = prems_of st
  19.108 -        val domT = (HOLogic.dest_setT (fastype_of rel))
  19.109 -        fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
  19.110 -            Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
  19.111 -        val measure = mk_measure (mk_sumcases @{typ nat} mk_single_measure domT)
  19.112 +        val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T))
  19.113        in
  19.114 -        (Function_Common.apply_termination_rule ctxt 1
  19.115 -        THEN gen_inst_state_tac ctxt measure) st
  19.116 +        mk_measure (mk_sumcases @{typ nat} mk_single_measure T')
  19.117        end
  19.118      fun termination_tac ctxt = 
  19.119 -      my_relation_tac ctxt
  19.120 +      Function_Relation.relation_tac ctxt mk_termination_measure 1
  19.121        THEN rtac @{thm wf_measure} 1
  19.122        THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac 
  19.123          (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv},
  19.124 @@ -154,12 +156,12 @@
  19.125      fun pat_completeness_auto ctxt =
  19.126        Pat_Completeness.pat_completeness_tac ctxt 1
  19.127        THEN auto_tac (clasimpset_of ctxt)
  19.128 -  in
  19.129 +  in 
  19.130      thy
  19.131 -    |> Class.instantiation (tycos, vs, @{sort small})
  19.132 +    |> Class.instantiation (tycos, vs, @{sort full_small})
  19.133      |> Function.add_function
  19.134        (map (fn (T, (name, _)) =>
  19.135 -          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (smallT T))) eqs)
  19.136 +          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T))) eqs)
  19.137          (map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs)
  19.138          Function_Common.default_config pat_completeness_auto
  19.139      |> snd
  19.140 @@ -167,34 +169,10 @@
  19.141      |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
  19.142      |> snd
  19.143      |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
  19.144 -  end;
  19.145 -
  19.146 -fun ensure_smallvalue_datatype config raw_tycos thy =
  19.147 -  let
  19.148 -    val algebra = Sign.classes_of thy;
  19.149 -    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
  19.150 -      Datatype.the_descr thy raw_tycos;
  19.151 -    val typerep_vs = (map o apsnd)
  19.152 -      (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
  19.153 -    val smallvalue_insts = (map (rpair @{sort small}) o flat o maps snd o maps snd)
  19.154 -      (Datatype_Aux.interpret_construction descr typerep_vs
  19.155 -        { atyp = single, dtyp = (K o K o K) [] });
  19.156 -    (*val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
  19.157 -      (Datatype_Aux.interpret_construction descr typerep_vs
  19.158 -        { atyp = K [], dtyp = K o K });*)
  19.159 -    val has_inst = exists (fn tyco =>
  19.160 -      can (Sorts.mg_domain algebra tyco) @{sort small}) tycos;
  19.161 -  in if has_inst then thy
  19.162 -    else case Quickcheck_Generators.perhaps_constrain thy smallvalue_insts typerep_vs
  19.163 -     of SOME constrain => (instantiate_smallvalue_datatype config descr
  19.164 -          (map constrain typerep_vs) tycos prfx (names, auxnames)
  19.165 -            ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
  19.166 -            handle FUNCTION_TYPE =>
  19.167 -              (Datatype_Aux.message config
  19.168 -                "Creation of smallvalue generators failed because the datatype contains a function type";
  19.169 -              thy))
  19.170 -      | NONE => thy
  19.171 -  end;
  19.172 +  end handle FUNCTION_TYPE =>
  19.173 +    (Datatype_Aux.message config
  19.174 +      "Creation of smallvalue generators failed because the datatype contains a function type";
  19.175 +    thy)
  19.176  
  19.177  (** building and compiling generator expressions **)
  19.178  
  19.179 @@ -209,25 +187,26 @@
  19.180  fun mk_generator_expr thy prop Ts =
  19.181    let
  19.182      val bound_max = length Ts - 1;
  19.183 -    val bounds = map Bound (bound_max downto 0)
  19.184 -    val result = list_comb (prop, bounds);
  19.185 -    val terms = HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of Ts bounds);
  19.186 +    val bounds = map_index (fn (i, ty) =>
  19.187 +      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
  19.188 +    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
  19.189 +    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
  19.190      val check =
  19.191        @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
  19.192          (@{term "If :: bool => term list option => term list option => term list option"}
  19.193 -        $ result $ @{term "None :: term list option"}
  19.194 -        $ (@{term "Some :: term list => term list option"} $ terms))
  19.195 +        $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
  19.196        $ @{term "None :: term list option"};
  19.197 -    fun mk_small_closure (depth, T) t =
  19.198 -      Const (@{const_name "Smallcheck.small_class.small"}, smallT T)
  19.199 -        $ absdummy (T, t) $ depth
  19.200 -  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure (rev bounds ~~ Ts) check) end
  19.201 +    fun mk_small_closure (_, _, i, T) t =
  19.202 +      Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
  19.203 +        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
  19.204 +        $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
  19.205 +  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
  19.206  
  19.207  fun compile_generator_expr ctxt t =
  19.208    let
  19.209      val Ts = (map snd o fst o strip_abs) t;
  19.210      val thy = ProofContext.theory_of ctxt
  19.211 -  in if Quickcheck.report ctxt then
  19.212 +  in if Config.get ctxt Quickcheck.report then
  19.213      error "Compilation with reporting facility is not supported"
  19.214    else
  19.215      let
  19.216 @@ -242,7 +221,8 @@
  19.217  (** setup **)
  19.218  
  19.219  val setup =
  19.220 -  Datatype.interpretation ensure_smallvalue_datatype
  19.221 +  Datatype.interpretation
  19.222 +    (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
  19.223    #> Context.theory_map
  19.224      (Quickcheck.add_generator ("small", compile_generator_expr));
  19.225  
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOL/ex/Birthday_Paradoxon.thy	Mon Nov 22 17:49:12 2010 +0100
    20.3 @@ -0,0 +1,101 @@
    20.4 +(*  Title: HOL/ex/Birthday_Paradoxon.thy
    20.5 +    Author: Lukas Bulwahn, TU Muenchen, 2007
    20.6 +*)
    20.7 +
    20.8 +header {* A Formulation of the Birthday Paradoxon *}
    20.9 +
   20.10 +theory Birthday_Paradoxon
   20.11 +imports Main "~~/src/HOL/Fact" "~~/src/HOL/Library/FuncSet"
   20.12 +begin
   20.13 +
   20.14 +section {* Cardinality *}
   20.15 +
   20.16 +lemma card_product_dependent:
   20.17 +  assumes "finite S"
   20.18 +  assumes "\<forall>x \<in> S. finite (T x)" 
   20.19 +  shows "card {(x, y). x \<in> S \<and> y \<in> T x} = (\<Sum>x \<in> S. card (T x))"
   20.20 +proof -
   20.21 +  note `finite S`
   20.22 +  moreover
   20.23 +  have "{(x, y). x \<in> S \<and> y \<in> T x} = (UN x : S. Pair x ` T x)" by auto
   20.24 +  moreover
   20.25 +  from `\<forall>x \<in> S. finite (T x)` have "ALL x:S. finite (Pair x ` T x)" by auto
   20.26 +  moreover
   20.27 +  have " ALL i:S. ALL j:S. i ~= j --> Pair i ` T i Int Pair j ` T j = {}" by auto
   20.28 +  moreover  
   20.29 +  ultimately have "card {(x, y). x \<in> S \<and> y \<in> T x} = (SUM i:S. card (Pair i ` T i))"
   20.30 +    by (auto, subst card_UN_disjoint) auto
   20.31 +  also have "... = (SUM x:S. card (T x))"
   20.32 +    by (subst card_image) (auto intro: inj_onI)
   20.33 +  finally show ?thesis by auto
   20.34 +qed
   20.35 +
   20.36 +lemma card_extensional_funcset_inj_on:
   20.37 +  assumes "finite S" "finite T" "card S \<le> card T"
   20.38 +  shows "card {f \<in> extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))"
   20.39 +using assms
   20.40 +proof (induct S arbitrary: T rule: finite_induct)
   20.41 +  case empty
   20.42 +  from this show ?case by (simp add: Collect_conv_if extensional_funcset_empty_domain)
   20.43 +next
   20.44 +  case (insert x S)
   20.45 +  { fix x
   20.46 +    from `finite T` have "finite (T - {x})" by auto
   20.47 +    from `finite S` this have "finite (extensional_funcset S (T - {x}))"
   20.48 +      by (rule finite_extensional_funcset)
   20.49 +    moreover
   20.50 +    have "{f : extensional_funcset S (T - {x}). inj_on f S} \<subseteq> (extensional_funcset S (T - {x}))" by auto    
   20.51 +    ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}"
   20.52 +      by (auto intro: finite_subset)
   20.53 +  } note finite_delete = this
   20.54 +  from insert have hyps: "\<forall>y \<in> T. card ({g. g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S}) = fact (card T - 1) div fact ((card T - 1) - card S)"(is "\<forall> _ \<in> T. _ = ?k") by auto
   20.55 +  from extensional_funcset_extend_domain_inj_on_eq[OF `x \<notin> S`]
   20.56 +  have "card {f. f : extensional_funcset (insert x S) T & inj_on f (insert x S)} =
   20.57 +    card ((%(y, g). g(x := y)) ` {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S})"
   20.58 +    by metis
   20.59 +  also from extensional_funcset_extend_domain_inj_onI[OF `x \<notin> S`, of T] have "... =  card {(y, g). y : T & g : extensional_funcset S (T - {y}) & inj_on g S}"
   20.60 +    by (simp add: card_image)
   20.61 +  also have "card {(y, g). y \<in> T \<and> g \<in> extensional_funcset S (T - {y}) \<and> inj_on g S} =
   20.62 +    card {(y, g). y \<in> T \<and> g \<in> {f \<in> extensional_funcset S (T - {y}). inj_on f S}}" by auto
   20.63 +  also from `finite T` finite_delete have "... = (\<Sum>y \<in> T. card {g. g \<in> extensional_funcset S (T - {y}) \<and>  inj_on g S})"
   20.64 +    by (subst card_product_dependent) auto
   20.65 +  also from hyps have "... = (card T) * ?k"
   20.66 +    by auto
   20.67 +  also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))"
   20.68 +    using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"]
   20.69 +    by (simp add: fact_mod)
   20.70 +  also have "... = fact (card T) div fact (card T - card (insert x S))"
   20.71 +    using insert by (simp add: fact_reduce_nat[of "card T"])
   20.72 +  finally show ?case .
   20.73 +qed
   20.74 +
   20.75 +lemma card_extensional_funcset_not_inj_on:
   20.76 +  assumes "finite S" "finite T" "card S \<le> card T"
   20.77 +  shows "card {f \<in> extensional_funcset S T. \<not> inj_on f S} = (card T) ^ (card S) - (fact (card T)) div (fact (card T - card S))"
   20.78 +proof -
   20.79 +  have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto
   20.80 +  from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}"
   20.81 +    by (auto intro!: finite_extensional_funcset)
   20.82 +  have "{f \<in> extensional_funcset S T. \<not> inj_on f S} = extensional_funcset S T - {f \<in> extensional_funcset S T. inj_on f S}" by auto 
   20.83 +  from assms this finite subset show ?thesis
   20.84 +    by (simp add: card_Diff_subset card_extensional_funcset card_extensional_funcset_inj_on)
   20.85 +qed
   20.86 +
   20.87 +lemma setprod_upto_nat_unfold:
   20.88 +  "setprod f {m..(n::nat)} = (if n < m then 1 else (if n = 0 then f 0 else f n * setprod f {m..(n - 1)}))"
   20.89 +  by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv)
   20.90 +
   20.91 +section {* Birthday paradoxon *}
   20.92 +
   20.93 +lemma birthday_paradoxon:
   20.94 +  assumes "card S = 23" "card T = 365"
   20.95 +  shows "2 * card {f \<in> extensional_funcset S T. \<not> inj_on f S} \<ge> card (extensional_funcset S T)"
   20.96 +proof -
   20.97 +  from `card S = 23` `card T = 365` have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite)
   20.98 +  from assms show ?thesis
   20.99 +    using card_extensional_funcset[OF `finite S`, of T]
  20.100 +      card_extensional_funcset_not_inj_on[OF `finite S` `finite T` `card S <= card T`]
  20.101 +    by (simp add: fact_div_fact setprod_upto_nat_unfold)
  20.102 +qed
  20.103 +
  20.104 +end
    21.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Mon Nov 22 17:46:51 2010 +0100
    21.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Mon Nov 22 17:49:12 2010 +0100
    21.3 @@ -1,6 +1,6 @@
    21.4  (*  Title:      HOL/ex/Quickcheck_Examples.thy
    21.5 -    Author:     Stefan Berghofer
    21.6 -    Copyright   2004 TU Muenchen
    21.7 +    Author:     Stefan Berghofer, Lukas Bulwahn
    21.8 +    Copyright   2004 - 2010 TU Muenchen
    21.9  *)
   21.10  
   21.11  header {* Examples for the 'quickcheck' command *}
   21.12 @@ -9,29 +9,41 @@
   21.13  imports Main
   21.14  begin
   21.15  
   21.16 +setup {* Smallvalue_Generators.setup *}
   21.17 +
   21.18  text {*
   21.19  The 'quickcheck' command allows to find counterexamples by evaluating
   21.20 -formulae under an assignment of free variables to random values.
   21.21 -In contrast to 'refute', it can deal with inductive datatypes,
   21.22 -but cannot handle quantifiers.
   21.23 +formulae.
   21.24 +Currently, there are two different exploration schemes:
   21.25 +- random testing: this is incomplete, but explores the search space faster.
   21.26 +- exhaustive testing: this is complete, but increasing the depth leads to
   21.27 +  exponentially many assignments.
   21.28 +
   21.29 +quickcheck can handle quantifiers on finite universes.
   21.30 +
   21.31  *}
   21.32  
   21.33  subsection {* Lists *}
   21.34  
   21.35  theorem "map g (map f xs) = map (g o f) xs"
   21.36 -  quickcheck[expect = no_counterexample]
   21.37 +  quickcheck[size = 3]
   21.38 +  quickcheck[generator = random, expect = no_counterexample]
   21.39 +  quickcheck[generator = small, size = 3, iterations = 1, report = false, expect = no_counterexample]
   21.40    oops
   21.41  
   21.42  theorem "map g (map f xs) = map (f o g) xs"
   21.43 -  quickcheck[expect = counterexample]
   21.44 +  quickcheck[generator = random, expect = counterexample]
   21.45 +  quickcheck[generator = small, report = false]
   21.46    oops
   21.47  
   21.48  theorem "rev (xs @ ys) = rev ys @ rev xs"
   21.49    quickcheck[expect = no_counterexample]
   21.50 +  quickcheck[generator = small, expect = no_counterexample, report = false]
   21.51    oops
   21.52  
   21.53  theorem "rev (xs @ ys) = rev xs @ rev ys"
   21.54 -  quickcheck[expect = counterexample]
   21.55 +  quickcheck[generator = small, expect = counterexample, report = false]
   21.56 +  quickcheck[generator = random, expect = counterexample]
   21.57    oops
   21.58  
   21.59  theorem "rev (rev xs) = xs"
   21.60 @@ -39,6 +51,7 @@
   21.61    oops
   21.62  
   21.63  theorem "rev xs = xs"
   21.64 +  quickcheck[generator = small, report = false]
   21.65    quickcheck[expect = counterexample]
   21.66    oops
   21.67  
   21.68 @@ -49,11 +62,13 @@
   21.69    | "app (f # fs) x = app fs (f x)"
   21.70  
   21.71  lemma "app (fs @ gs) x = app gs (app fs x)"
   21.72 -  quickcheck[expect = no_counterexample]
   21.73 +  quickcheck[generator = random, expect = no_counterexample]
   21.74 +  quickcheck[generator = small, iterations = 1, size = 4, report = false, expect = no_counterexample]
   21.75    by (induct fs arbitrary: x) simp_all
   21.76  
   21.77  lemma "app (fs @ gs) x = app fs (app gs x)"
   21.78 -  quickcheck[expect = counterexample]
   21.79 +  quickcheck[generator = random, expect = counterexample]
   21.80 +  quickcheck[generator = small, report = false, expect = counterexample]
   21.81    oops
   21.82  
   21.83  primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
   21.84 @@ -67,15 +82,18 @@
   21.85  text {* A lemma, you'd think to be true from our experience with delAll *}
   21.86  lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
   21.87    -- {* Wrong. Precondition needed.*}
   21.88 +  quickcheck[generator = small, report = false]
   21.89    quickcheck[expect = counterexample]
   21.90    oops
   21.91  
   21.92  lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
   21.93 +  quickcheck[generator = small, report = false]
   21.94    quickcheck[expect = counterexample]
   21.95      -- {* Also wrong.*}
   21.96    oops
   21.97  
   21.98  lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
   21.99 +  quickcheck[generator = small, report = false]
  21.100    quickcheck[expect = no_counterexample]
  21.101    by (induct xs) auto
  21.102  
  21.103 @@ -85,12 +103,13 @@
  21.104                              else (x#(replace a b xs)))"
  21.105  
  21.106  lemma "occurs a xs = occurs b (replace a b xs)"
  21.107 +  quickcheck[generator = small, report = false]
  21.108    quickcheck[expect = counterexample]
  21.109    -- {* Wrong. Precondition needed.*}
  21.110    oops
  21.111  
  21.112  lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
  21.113 -  quickcheck[expect = no_counterexample]
  21.114 +  quickcheck[expect = no_counterexample, report = false]
  21.115    by (induct xs) simp_all
  21.116  
  21.117  
  21.118 @@ -133,8 +152,106 @@
  21.119    | "root (Node f x y) = f"
  21.120  
  21.121  theorem "hd (inOrder xt) = root xt"
  21.122 +  quickcheck[generator = small, report = false]
  21.123    quickcheck[expect = counterexample]
  21.124      --{* Wrong! *} 
  21.125    oops
  21.126  
  21.127 +
  21.128 +subsection {* Exhaustive Testing beats Random Testing *}
  21.129 +
  21.130 +text {* Here are some examples from mutants from the List theory
  21.131 +where exhaustive testing beats random testing *}
  21.132 +
  21.133 +lemma
  21.134 +  "[] ~= xs ==> hd xs = last (x # xs)"
  21.135 +quickcheck[generator = random, report = false]
  21.136 +quickcheck[generator = small, report = false, expect = counterexample]
  21.137 +oops
  21.138 +
  21.139 +lemma
  21.140 +  assumes "!!i. [| i < n; i < length xs |] ==> P (xs ! i)" "n < length xs ==> ~ P (xs ! n)"
  21.141 +  shows "drop n xs = takeWhile P xs"
  21.142 +quickcheck[generator = random, iterations = 10000, report = false, quiet]
  21.143 +quickcheck[generator = small, iterations = 1, report = false, expect = counterexample]
  21.144 +oops
  21.145 +
  21.146 +lemma
  21.147 +  "i < length (List.transpose (List.transpose xs)) ==> xs ! i = map (%xs. xs ! i) [ys<-xs. i < length ys]"
  21.148 +quickcheck[generator = random, iterations = 10000, report = false, quiet]
  21.149 +quickcheck[generator = small, iterations = 1, report = false, expect = counterexample]
  21.150 +oops
  21.151 +
  21.152 +lemma
  21.153 +  "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
  21.154 +quickcheck[generator = random, iterations = 10000, report = false, quiet]
  21.155 +quickcheck[generator = small, finite_types = false, report = false, expect = counterexample]
  21.156 +oops
  21.157 +
  21.158 +lemma
  21.159 +  "i < n - m ==> f (lcm m i) = map f [m..<n] ! i"
  21.160 +quickcheck[generator = random, iterations = 1000, report = false, quiet]
  21.161 +quickcheck[generator = small, finite_types = false, report = false, expect = counterexample]
  21.162 +oops
  21.163 +
  21.164 +lemma
  21.165 +  "ns ! k < length ns ==> k <= listsum ns"
  21.166 +quickcheck[generator = random, iterations = 10000, report = true, quiet]
  21.167 +quickcheck[generator = small, report = false, expect = counterexample]
  21.168 +oops
  21.169 +
  21.170 +lemma
  21.171 +  "[| ys = x # xs1; zs = xs1 @ xs |] ==> ys @ zs = x # xs"
  21.172 +quickcheck[generator = random, iterations = 10000, report = true]
  21.173 +quickcheck[generator = small, report = false, expect = counterexample]
  21.174 +oops
  21.175 +
  21.176 +lemma
  21.177 +"i < length xs ==> take (Suc i) xs = [] @ xs ! i # take i xs"
  21.178 +quickcheck[generator = random]
  21.179 +quickcheck[generator = small, report = false, expect = counterexample]
  21.180 +oops
  21.181 +
  21.182 +lemma
  21.183 +  "i < length xs ==> take (Suc i) xs = (xs ! i # xs) @ take i []"
  21.184 +quickcheck[generator = random]
  21.185 +quickcheck[generator = small, report = false, expect = counterexample]
  21.186 +oops
  21.187 +
  21.188 +lemma
  21.189 +  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-remdups xs. i < length ys]"
  21.190 +quickcheck[generator = random]
  21.191 +quickcheck[generator = small, report = false]
  21.192 +oops
  21.193 +
  21.194 +lemma
  21.195 +  "[| sorted (rev (map length xs)); i < length xs |] ==> xs ! i = map (%ys. ys ! i) [ys<-List.transpose xs. {..<i} (length ys)]"
  21.196 +quickcheck[generator = random]
  21.197 +quickcheck[generator = small, report = false, expect = counterexample]
  21.198 +oops
  21.199 +
  21.200 +lemma
  21.201 +  "(ys = zs) = (xs @ ys = splice xs zs)"
  21.202 +quickcheck[generator = random]
  21.203 +quickcheck[generator = small, report = false, expect = counterexample]
  21.204 +oops
  21.205 +
  21.206 +section {* Examples with quantifiers *}
  21.207 +
  21.208 +text {*
  21.209 +  These examples show that we can handle quantifiers.
  21.210 +*}
  21.211 +
  21.212 +lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
  21.213 +  quickcheck[expect = counterexample]
  21.214 +oops
  21.215 +
  21.216 +lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
  21.217 +  quickcheck[expect = counterexample]
  21.218 +oops
  21.219 +
  21.220 +lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
  21.221 +  quickcheck[expect = counterexample]
  21.222 +oops
  21.223 +
  21.224  end
    22.1 --- a/src/HOL/ex/ROOT.ML	Mon Nov 22 17:46:51 2010 +0100
    22.2 +++ b/src/HOL/ex/ROOT.ML	Mon Nov 22 17:49:12 2010 +0100
    22.3 @@ -67,7 +67,8 @@
    22.4    "Summation",
    22.5    "Gauge_Integration",
    22.6    "Dedekind_Real",
    22.7 -  "Quicksort"
    22.8 +  "Quicksort",
    22.9 +  "Birthday_Paradoxon"
   22.10  ];
   22.11  
   22.12  HTML.with_charset "utf-8" (no_document use_thys)
    23.1 --- a/src/Pure/Isar/proof.ML	Mon Nov 22 17:46:51 2010 +0100
    23.2 +++ b/src/Pure/Isar/proof.ML	Mon Nov 22 17:49:12 2010 +0100
    23.3 @@ -16,6 +16,7 @@
    23.4    val context_of: state -> context
    23.5    val theory_of: state -> theory
    23.6    val map_context: (context -> context) -> state -> state
    23.7 +  val map_context_result : (context -> 'a * context) -> state -> 'a * state
    23.8    val map_contexts: (context -> context) -> state -> state
    23.9    val propagate_ml_env: state -> state
   23.10    val bind_terms: (indexname * term option) list -> state -> state
    24.1 --- a/src/Tools/quickcheck.ML	Mon Nov 22 17:46:51 2010 +0100
    24.2 +++ b/src/Tools/quickcheck.ML	Mon Nov 22 17:49:12 2010 +0100
    24.3 @@ -10,25 +10,33 @@
    24.4    (* configuration *)
    24.5    val auto: bool Unsynchronized.ref
    24.6    val timing : bool Unsynchronized.ref
    24.7 +  val size : int Config.T
    24.8 +  val iterations : int Config.T
    24.9 +  val no_assms : bool Config.T
   24.10 +  val report : bool Config.T
   24.11 +  val quiet : bool Config.T
   24.12 +  val timeout : real Config.T
   24.13 +  val finite_types : bool Config.T
   24.14 +  val finite_type_size : int Config.T
   24.15    datatype report = Report of
   24.16      { iterations : int, raised_match_errors : int,
   24.17        satisfied_assms : int list, positive_concl_tests : int }
   24.18 -  datatype expectation = No_Expectation | No_Counterexample | Counterexample;
   24.19 -  datatype test_params = Test_Params of
   24.20 -  { size: int, iterations: int, default_type: typ list, no_assms: bool,
   24.21 -    expect : expectation, report: bool, quiet : bool, timeout : real};
   24.22 +  datatype expectation = No_Expectation | No_Counterexample | Counterexample;  
   24.23 +  datatype test_params = Test_Params of {default_type: typ list, expect : expectation};
   24.24    val test_params_of : Proof.context -> test_params
   24.25 -  val report : Proof.context -> bool
   24.26 -  val map_test_params :
   24.27 -    ((int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real)))
   24.28 -      -> (int * int) * ((typ list * bool) * ((expectation * bool) * (bool * real))))
   24.29 +  val map_test_params : (typ list * expectation -> typ list * expectation)
   24.30      -> Context.generic -> Context.generic
   24.31    val add_generator:
   24.32      string * (Proof.context -> term -> int -> term list option * (bool list * bool))
   24.33        -> Context.generic -> Context.generic
   24.34    (* testing terms and proof states *)
   24.35 +  val test_term_small: Proof.context -> term ->
   24.36 +    (string * term) list option * ((string * int) list * ((int * report list) list) option)
   24.37    val test_term: Proof.context -> string option -> term ->
   24.38      (string * term) list option * ((string * int) list * ((int * report list) list) option)
   24.39 +  val test_goal_terms:
   24.40 +    Proof.context -> string option * (string * typ) list -> term list
   24.41 +      -> (string * term) list option * ((string * int) list * ((int * report list) list) option) list
   24.42    val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
   24.43  end;
   24.44  
   24.45 @@ -78,43 +86,39 @@
   24.46    if expect1 = expect2 then expect1 else No_Expectation
   24.47  
   24.48  (* quickcheck configuration -- default parameters, test generators *)
   24.49 +val (size, setup_size) = Attrib.config_int "quickcheck_size" (K 10)
   24.50 +val (iterations, setup_iterations) = Attrib.config_int "quickcheck_iterations" (K 100)
   24.51 +val (no_assms, setup_no_assms) = Attrib.config_bool "quickcheck_no_assms" (K false)
   24.52 +val (report, setup_report) = Attrib.config_bool "quickcheck_report" (K true)
   24.53 +val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
   24.54 +val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
   24.55 +val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true)
   24.56 +val (finite_type_size, setup_finite_type_size) = Attrib.config_int "quickcheck_finite_type_size" (K 3)
   24.57 +
   24.58 +val setup_config =
   24.59 +  setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout
   24.60 +    #> setup_finite_types #> setup_finite_type_size
   24.61  
   24.62  datatype test_params = Test_Params of
   24.63 -  { size: int, iterations: int, default_type: typ list, no_assms: bool,
   24.64 -    expect : expectation, report: bool, quiet : bool, timeout : real};
   24.65 +  {default_type: typ list, expect : expectation};
   24.66  
   24.67 -fun dest_test_params
   24.68 -    (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
   24.69 -  ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout))));
   24.70 +fun dest_test_params (Test_Params {default_type, expect}) = (default_type, expect);
   24.71  
   24.72 -fun make_test_params
   24.73 -    ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))) =
   24.74 -  Test_Params { size = size, iterations = iterations, default_type = default_type,
   24.75 -    no_assms = no_assms, expect = expect, report = report, quiet = quiet, timeout = timeout };
   24.76 +fun make_test_params (default_type, expect) = Test_Params {default_type = default_type, expect = expect};
   24.77  
   24.78 -fun map_test_params' f
   24.79 -    (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
   24.80 -  make_test_params
   24.81 -    (f ((size, iterations), ((default_type, no_assms), ((expect, report), (quiet, timeout)))));
   24.82 +fun map_test_params' f (Test_Params {default_type, expect}) = make_test_params (f (default_type, expect));
   24.83  
   24.84  fun merge_test_params
   24.85 - (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
   24.86 -    no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1, timeout = timeout1 },
   24.87 -  Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
   24.88 -    no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2, timeout = timeout2}) =
   24.89 -  make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
   24.90 -    ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
   24.91 -    ((merge_expectation (expect1, expect2), report1 orelse report2),
   24.92 -    (quiet1 orelse quiet2, Real.min (timeout1, timeout2)))));
   24.93 + (Test_Params {default_type = default_type1, expect = expect1},
   24.94 +  Test_Params {default_type = default_type2, expect = expect2}) =
   24.95 +  make_test_params (merge (op =) (default_type1, default_type2), merge_expectation (expect1, expect2));
   24.96  
   24.97  structure Data = Generic_Data
   24.98  (
   24.99    type T =
  24.100      (string * (Proof.context -> term -> int -> term list option * (bool list * bool))) list
  24.101        * test_params;
  24.102 -  val empty = ([], Test_Params
  24.103 -    { size = 10, iterations = 100, default_type = [], no_assms = false,
  24.104 -      expect = No_Expectation, report = false, quiet = false, timeout = 30.0});
  24.105 +  val empty = ([], Test_Params {default_type = [], expect = No_Expectation});
  24.106    val extend = I;
  24.107    fun merge ((generators1, params1), (generators2, params2)) : T =
  24.108      (AList.merge (op =) (K true) (generators1, generators2),
  24.109 @@ -123,35 +127,9 @@
  24.110  
  24.111  val test_params_of = snd o Data.get o Context.Proof;
  24.112  
  24.113 -val size = fst o fst o dest_test_params o test_params_of
  24.114 -
  24.115 -val iterations = snd o fst o dest_test_params o test_params_of
  24.116 -
  24.117 -val default_type = fst o fst o snd o dest_test_params o test_params_of
  24.118 -
  24.119 -val no_assms = snd o fst o snd o dest_test_params o test_params_of
  24.120 -
  24.121 -val expect = fst o fst o snd o snd o dest_test_params o test_params_of
  24.122 -
  24.123 -val report = snd o fst o snd o snd o dest_test_params o test_params_of
  24.124 -
  24.125 -val quiet = fst o snd o snd o snd o dest_test_params o test_params_of
  24.126 +val default_type = fst o dest_test_params o test_params_of
  24.127  
  24.128 -val timeout = snd o snd o snd o snd o dest_test_params o test_params_of
  24.129 -
  24.130 -fun map_report f
  24.131 -  (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
  24.132 -    make_test_params
  24.133 -      ((size, iterations), ((default_type, no_assms), ((expect, f report), (quiet, timeout))));
  24.134 -
  24.135 -fun map_quiet f
  24.136 -  (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet, timeout }) =
  24.137 -    make_test_params
  24.138 -      ((size, iterations), ((default_type, no_assms), ((expect, report), (f quiet, timeout))));
  24.139 -    
  24.140 -fun set_report report = Data.map (apsnd (map_report (K report)))
  24.141 -
  24.142 -fun set_quiet quiet = Data.map (apsnd (map_quiet (K quiet)))
  24.143 +val expect = snd o dest_test_params o test_params_of
  24.144  
  24.145  val map_test_params = Data.map o apsnd o map_test_params'
  24.146  
  24.147 @@ -197,6 +175,40 @@
  24.148      val time = Time.toMilliseconds (#cpu (end_timing start))
  24.149    in (Exn.release result, (description, time)) end
  24.150  
  24.151 +fun test_term_small ctxt t =
  24.152 +  let
  24.153 +    val (names, t') = prep_test_term t;
  24.154 +    val current_size = Unsynchronized.ref 0
  24.155 +    fun excipit s =
  24.156 +      "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
  24.157 +    val (tester, comp_time) = cpu_time "compilation"
  24.158 +      (fn () => the (AList.lookup (op =) ((fst o Data.get o Context.Proof) ctxt) "small") ctxt t');
  24.159 +    val empty_report = Report { iterations = 0, raised_match_errors = 0,
  24.160 +      satisfied_assms = [], positive_concl_tests = 0 }
  24.161 +    fun with_size k timings =
  24.162 +      if k > Config.get ctxt size then (NONE, timings)
  24.163 +      else
  24.164 +         let
  24.165 +           val _ = if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
  24.166 +           val _ = current_size := k
  24.167 +           val (result, timing) = cpu_time ("size " ^ string_of_int k)
  24.168 +             (fn () => (fst (tester k)) handle Match => (if Config.get ctxt quiet then ()
  24.169 +             else warning "Exception Match raised during quickcheck"; NONE))
  24.170 +        in
  24.171 +          case result of
  24.172 +            NONE => with_size (k + 1) (timing :: timings)
  24.173 +          | SOME q => (SOME q, (timing :: timings))
  24.174 +        end;
  24.175 +     val result = with_size 1 [comp_time]
  24.176 +   in
  24.177 +     apsnd (rpair NONE) (apfst (Option.map (curry (op ~~) names)) result)
  24.178 +   end
  24.179 +
  24.180 +(* we actually assume we know the generators and its behaviour *)
  24.181 +fun is_iteratable "SML" = true
  24.182 +  | is_iteratable "random" = true
  24.183 +  | is_iteratable _ = false
  24.184 +  
  24.185  fun test_term ctxt generator_name t =
  24.186    let
  24.187      val (names, t') = prep_test_term t;
  24.188 @@ -205,12 +217,13 @@
  24.189        "Quickcheck " ^ s ^ " while testing at size " ^ string_of_int (!current_size)
  24.190      val (testers, comp_time) = cpu_time "quickcheck compilation"
  24.191        (fn () => (case generator_name
  24.192 -       of NONE => if quiet ctxt then mk_testers ctxt t' else mk_testers_strict ctxt t'
  24.193 +       of NONE => if Config.get ctxt quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
  24.194          | SOME name => [mk_tester_select name ctxt t']));
  24.195      fun iterate f 0 report = (NONE, report)
  24.196        | iterate f j report =
  24.197          let
  24.198 -          val (test_result, single_report) = apsnd Run (f ()) handle Match => (if quiet ctxt then ()
  24.199 +          val (test_result, single_report) = apsnd Run (f ()) handle Match => 
  24.200 +            (if Config.get ctxt quiet then ()
  24.201               else warning "Exception Match raised during quickcheck"; (NONE, MatchExc))
  24.202            val report = collect_single_report single_report report
  24.203          in
  24.204 @@ -220,20 +233,29 @@
  24.205        satisfied_assms = [], positive_concl_tests = 0 }
  24.206      fun with_testers k [] = (NONE, [])
  24.207        | with_testers k (tester :: testers) =
  24.208 -          case iterate (fn () => tester (k - 1)) (iterations ctxt) empty_report
  24.209 +        let
  24.210 +          val niterations = case generator_name of
  24.211 +            SOME generator_name =>
  24.212 +              if is_iteratable generator_name then Config.get ctxt iterations else 1
  24.213 +          | NONE => Config.get ctxt iterations
  24.214 +          val (result, timing) = cpu_time ("size " ^ string_of_int k)
  24.215 +            (fn () => iterate (fn () => tester (k - 1)) niterations empty_report)
  24.216 +        in
  24.217 +          case result
  24.218             of (NONE, report) => apsnd (cons report) (with_testers k testers)
  24.219 -            | (SOME q, report) => (SOME q, [report]);
  24.220 +            | (SOME q, report) => (SOME q, [report])
  24.221 +        end
  24.222      fun with_size k reports =
  24.223 -      if k > size ctxt then (NONE, reports)
  24.224 +      if k > Config.get ctxt size then (NONE, reports)
  24.225        else
  24.226 -       (if quiet ctxt then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
  24.227 +       (if Config.get ctxt quiet then () else Output.urgent_message ("Test data size: " ^ string_of_int k);
  24.228          let
  24.229 -          val _ = current_size := k  
  24.230 +          val _ = current_size := k
  24.231            val (result, new_report) = with_testers k testers
  24.232            val reports = ((k, new_report) :: reports)
  24.233          in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
  24.234      val ((result, reports), exec_time) =
  24.235 -      TimeLimit.timeLimit (seconds (timeout ctxt)) (fn () => cpu_time "quickcheck execution"
  24.236 +      TimeLimit.timeLimit (seconds (Config.get ctxt timeout)) (fn () => cpu_time "quickcheck execution"
  24.237        (fn () => apfst
  24.238           (fn result => case result of NONE => NONE
  24.239          | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
  24.240 @@ -241,9 +263,14 @@
  24.241          error (excipit "ran out of time")
  24.242       | Exn.Interrupt => error (excipit "was interrupted")  (* FIXME violates Isabelle/ML exception model *)
  24.243    in
  24.244 -    (result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
  24.245 +    (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
  24.246    end;
  24.247  
  24.248 +fun get_finite_types ctxt =
  24.249 +  fst (chop (Config.get ctxt finite_type_size)
  24.250 +    (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
  24.251 +     "Enum.finite_4", "Enum.finite_5"]))  
  24.252 +
  24.253  exception WELLSORTED of string
  24.254  
  24.255  fun monomorphic_term thy insts default_T = 
  24.256 @@ -264,7 +291,32 @@
  24.257  
  24.258  datatype wellsorted_error = Wellsorted_Error of string | Term of term
  24.259  
  24.260 -fun test_goal generator_name insts i state =
  24.261 +fun test_goal_terms lthy (generator_name, insts) check_goals =
  24.262 +  let
  24.263 +    val thy = ProofContext.theory_of lthy 
  24.264 +    val inst_goals =
  24.265 +      if Config.get lthy finite_types then 
  24.266 +        maps (fn check_goal => map (fn T =>
  24.267 +          Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
  24.268 +            handle WELLSORTED s => Wellsorted_Error s) (get_finite_types lthy)) check_goals
  24.269 +      else
  24.270 +        maps (fn check_goal => map (fn T =>
  24.271 +          Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
  24.272 +            handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) check_goals
  24.273 +    val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals)
  24.274 +    val correct_inst_goals =
  24.275 +      case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
  24.276 +        [] => error error_msg
  24.277 +      | xs => xs
  24.278 +    val _ = if Config.get lthy quiet then () else warning error_msg
  24.279 +    fun collect_results f reports [] = (NONE, rev reports)
  24.280 +      | collect_results f reports (t :: ts) =
  24.281 +        case f t of
  24.282 +          (SOME res, report) => (SOME res, rev (report :: reports))
  24.283 +        | (NONE, report) => collect_results f (report :: reports) ts
  24.284 +  in collect_results (test_term lthy generator_name) [] correct_inst_goals end;
  24.285 +
  24.286 +fun test_goal (generator_name, insts) i state =
  24.287    let
  24.288      val lthy = Proof.context_of state;
  24.289      val thy = Proof.theory_of state;
  24.290 @@ -276,7 +328,7 @@
  24.291       of NONE => NONE
  24.292        | SOME "" => NONE
  24.293        | SOME locale => SOME locale;
  24.294 -    val assms = if no_assms lthy then [] else case some_locale
  24.295 +    val assms = if Config.get lthy no_assms then [] else case some_locale
  24.296       of NONE => Assumption.all_assms_of lthy
  24.297        | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
  24.298      val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
  24.299 @@ -284,21 +336,9 @@
  24.300       of NONE => [proto_goal]
  24.301        | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
  24.302          (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
  24.303 -    val inst_goals = maps (fn check_goal => map (fn T =>
  24.304 -      Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
  24.305 -        handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) check_goals
  24.306 -    val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals)
  24.307 -    val correct_inst_goals =
  24.308 -      case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
  24.309 -        [] => error error_msg
  24.310 -      | xs => xs
  24.311 -    val _ = if quiet lthy then () else warning error_msg
  24.312 -    fun collect_results f reports [] = (NONE, rev reports)
  24.313 -      | collect_results f reports (t :: ts) =
  24.314 -        case f t of
  24.315 -          (SOME res, report) => (SOME res, rev (report :: reports))
  24.316 -        | (NONE, report) => collect_results f (report :: reports) ts
  24.317 -  in collect_results (test_term lthy generator_name) [] correct_inst_goals end;
  24.318 +  in
  24.319 +    test_goal_terms lthy (generator_name, insts) check_goals
  24.320 +  end
  24.321  
  24.322  (* pretty printing *)
  24.323  
  24.324 @@ -349,8 +389,8 @@
  24.325        val ctxt = Proof.context_of state;
  24.326        val res =
  24.327          state
  24.328 -        |> Proof.map_context (Context.proof_map (set_report false #> set_quiet true))
  24.329 -        |> try (test_goal NONE [] 1);
  24.330 +        |> Proof.map_context (Config.put report false #> Config.put quiet true)
  24.331 +        |> try (test_goal (NONE, []) 1);
  24.332      in
  24.333        case res of
  24.334          NONE => (false, state)
  24.335 @@ -360,7 +400,7 @@
  24.336      end
  24.337  
  24.338  val setup = Auto_Tools.register_tool ("quickcheck", auto_quickcheck)
  24.339 -
  24.340 +  #> setup_config
  24.341  
  24.342  (* Isar commands *)
  24.343  
  24.344 @@ -383,57 +423,37 @@
  24.345    | read_expectation "counterexample" = Counterexample
  24.346    | read_expectation s = error ("Not an expectation value: " ^ s)  
  24.347  
  24.348 -fun parse_test_param ctxt ("size", [arg]) =
  24.349 -      (apfst o apfst o K) (read_nat arg)
  24.350 -  | parse_test_param ctxt ("iterations", [arg]) =
  24.351 -      (apfst o apsnd o K) (read_nat arg)
  24.352 -  | parse_test_param ctxt ("default_type", arg) =
  24.353 -      (apsnd o apfst o apfst o K) (map (ProofContext.read_typ ctxt) arg)
  24.354 -  | parse_test_param ctxt ("no_assms", [arg]) =
  24.355 -      (apsnd o apfst o apsnd o K) (read_bool arg)
  24.356 -  | parse_test_param ctxt ("expect", [arg]) =
  24.357 -      (apsnd o apsnd o apfst o apfst o K) (read_expectation arg)
  24.358 -  | parse_test_param ctxt ("report", [arg]) =
  24.359 -      (apsnd o apsnd o apfst o apsnd o K) (read_bool arg)
  24.360 -  | parse_test_param ctxt ("quiet", [arg]) =
  24.361 -      (apsnd o apsnd o apsnd o apfst o K) (read_bool arg)
  24.362 -  | parse_test_param ctxt ("timeout", [arg]) =
  24.363 -      (apsnd o apsnd o apsnd o apsnd o K) (read_real arg)
  24.364 -  | parse_test_param ctxt (name, _) =
  24.365 -      error ("Unknown test parameter: " ^ name);
  24.366 +fun parse_test_param ("size", [arg]) = Config.put_generic size (read_nat arg)
  24.367 +  | parse_test_param ("iterations", [arg]) = Config.put_generic iterations (read_nat arg)
  24.368 +  | parse_test_param ("default_type", arg) = (fn gen_ctxt =>
  24.369 +    map_test_params ((apfst o K) (map (ProofContext.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt)
  24.370 +  | parse_test_param ("no_assms", [arg]) = Config.put_generic no_assms (read_bool arg)
  24.371 +  | parse_test_param ("expect", [arg]) = map_test_params ((apsnd o K) (read_expectation arg))
  24.372 +  | parse_test_param ("report", [arg]) = Config.put_generic report (read_bool arg)
  24.373 +  | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg)
  24.374 +  | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
  24.375 +  | parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg)
  24.376 +  | parse_test_param ("finite_type_size", [arg]) = Config.put_generic finite_type_size (read_nat arg)
  24.377 +  | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
  24.378  
  24.379 -fun parse_test_param_inst ctxt ("generator", [arg]) =
  24.380 -      (apsnd o apfst o K o SOME) arg
  24.381 -  | parse_test_param_inst ctxt (name, arg) =
  24.382 +fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) =
  24.383 +      (apfst o apfst o K o SOME) arg ((generator, insts), ctxt)
  24.384 +  | parse_test_param_inst (name, arg) ((generator, insts), ctxt) =
  24.385        case try (ProofContext.read_typ ctxt) name
  24.386 -       of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =))
  24.387 -              (v, ProofContext.read_typ ctxt (the_single arg))
  24.388 -        | _ => (apfst o parse_test_param ctxt) (name, arg);
  24.389 +       of SOME (TFree (v, _)) => (apfst o apsnd o AList.update (op =))
  24.390 +              (v, ProofContext.read_typ ctxt (the_single arg)) ((generator, insts), ctxt)
  24.391 +        | _ => (apsnd o Context.proof_map o parse_test_param) (name, arg) ((generator, insts), ctxt);
  24.392  
  24.393 -fun quickcheck_params_cmd args thy =
  24.394 -  let
  24.395 -    val ctxt = ProofContext.init_global thy
  24.396 -    val f = fold (parse_test_param ctxt) args;
  24.397 -  in
  24.398 -    thy
  24.399 -    |> (Context.theory_map o map_test_params) f
  24.400 -  end;
  24.401 -
  24.402 +fun quickcheck_params_cmd args = Context.theory_map (fold parse_test_param args);
  24.403 +  
  24.404  fun gen_quickcheck args i state =
  24.405 -  let
  24.406 -    val ctxt = Proof.context_of state;
  24.407 -    val default_params = (dest_test_params o snd o Data.get o Context.Proof) ctxt;
  24.408 -    val f = fold (parse_test_param_inst ctxt) args;
  24.409 -    val (test_params, (generator_name, insts)) = f (default_params, (NONE, []));
  24.410 -  in
  24.411 -    state
  24.412 -    |> Proof.map_context (Context.proof_map (map_test_params (K test_params)))
  24.413 -    |> (fn state' => test_goal generator_name insts i state'
  24.414 -      |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
  24.415 -                 error ("quickcheck expected to find no counterexample but found one") else ()
  24.416 -             | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
  24.417 -                 error ("quickcheck expected to find a counterexample but did not find one") else ()))
  24.418 -  end;
  24.419 +  state
  24.420 +  |> Proof.map_context_result (fn ctxt => fold parse_test_param_inst args ((NONE, []), ctxt))
  24.421 +  |> (fn ((generator, insts), state') => test_goal (generator, insts) i state'
  24.422 +  |> tap (fn (SOME x, _) => if expect (Proof.context_of state') = No_Counterexample then
  24.423 +               error ("quickcheck expected to find no counterexample but found one") else ()
  24.424 +           | (NONE, _) => if expect (Proof.context_of state') = Counterexample then
  24.425 +               error ("quickcheck expected to find a counterexample but did not find one") else ()))
  24.426  
  24.427  fun quickcheck args i state = fst (gen_quickcheck args i state);
  24.428