--- a/src/HOL/Enum.thy Wed Dec 08 16:47:57 2010 +0100
+++ b/src/HOL/Enum.thy Wed Dec 08 18:07:03 2010 +0100
@@ -545,7 +545,7 @@
end
-hide_const a\<^isub>1
+hide_const (open) a\<^isub>1
datatype finite_2 = a\<^isub>1 | a\<^isub>2
@@ -598,7 +598,7 @@
end
-hide_const a\<^isub>1 a\<^isub>2
+hide_const (open) a\<^isub>1 a\<^isub>2
datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
@@ -651,7 +651,7 @@
end
-hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3
+hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
@@ -687,7 +687,7 @@
end
-hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
+hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
@@ -724,10 +724,10 @@
end
-hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
+hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
-hide_type finite_1 finite_2 finite_3 finite_4 finite_5
+hide_type (open) finite_1 finite_2 finite_3 finite_4 finite_5
hide_const (open) enum enum_all enum_ex n_lists all_n_lists ex_n_lists product
end
--- a/src/HOL/Smallcheck.thy Wed Dec 08 16:47:57 2010 +0100
+++ b/src/HOL/Smallcheck.thy Wed Dec 08 18:07:03 2010 +0100
@@ -117,6 +117,92 @@
end
+subsubsection {* A smarter enumeration scheme for functions over finite datatypes *}
+
+
+class check_all = enum + term_of +
+fixes check_all :: "('a * (unit \<Rightarrow> term) \<Rightarrow> term list option) \<Rightarrow> term list option"
+
+fun check_all_n_lists :: "(('a :: check_all) list * (unit \<Rightarrow> term list) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
+where
+ "check_all_n_lists f n =
+ (if n = 0 then f ([], (%_. [])) else check_all (%(x, xt). check_all_n_lists (%(xs, xst). f ((x # xs), (%_. (xt () # xst ())))) (n - 1)))"
+
+instantiation "fun" :: ("{equal, enum, check_all}", "{enum, term_of, check_all}") check_all
+begin
+
+definition mk_map_term :: "'a list \<Rightarrow> (unit \<Rightarrow> term list) \<Rightarrow> (unit \<Rightarrow> typerep) \<Rightarrow> unit \<Rightarrow> term"
+where
+ "mk_map_term domm rng T2 =
+ (%_. let T1 = (Typerep.typerep (TYPE('a)));
+ T2 = T2 ();
+ update_term = (%g (a, b).
+ Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
+ (Code_Evaluation.Const (STR ''Fun.fun_upd'')
+ (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]]]])) g) (Code_Evaluation.term_of a)) b)
+ in
+ List.foldl update_term (Code_Evaluation.Abs (STR ''x'') T1 (Code_Evaluation.Const (STR ''HOL.undefined'') T2)) (zip domm (rng ())))"
+
+definition
+ "check_all f = check_all_n_lists (\<lambda>(ys, yst). f (the o map_of (zip (Enum.enum\<Colon>'a list) ys), mk_map_term (Enum.enum::'a list) yst (%_. Typerep.typerep (TYPE('b))))) (Code_Numeral.of_nat (length (Enum.enum :: 'a list)))"
+
+instance ..
+
+end
+
+instantiation bool :: check_all
+begin
+
+definition
+ "check_all f = (case f (Code_Evaluation.valtermify False) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify True))"
+
+instance ..
+
+end
+
+instantiation prod :: (check_all, check_all) check_all
+begin
+
+definition
+ "check_all f = check_all (%(x, t1). check_all (%(y, t2). f ((x, y), %_. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))))"
+
+instance ..
+
+end
+
+instantiation Enum.finite_1 :: check_all
+begin
+
+definition
+ "check_all f = f (Code_Evaluation.valtermify Enum.finite_1.a\<^isub>1)"
+
+instance ..
+
+end
+
+instantiation Enum.finite_2 :: check_all
+begin
+
+definition
+ "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_2.a\<^isub>2))"
+
+instance ..
+
+end
+
+instantiation Enum.finite_3 :: check_all
+begin
+
+definition
+ "check_all f = (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>1) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> (case f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>2) of Some x' \<Rightarrow> Some x' | None \<Rightarrow> f (Code_Evaluation.valtermify Enum.finite_3.a\<^isub>3)))"
+
+instance ..
+
+end
+
+
+
subsection {* Defining combinators for any first-order data type *}
definition orelse :: "'a option => 'a option => 'a option"
@@ -138,6 +224,6 @@
declare [[quickcheck_tester = exhaustive]]
hide_fact orelse_def catch_match_def
-hide_const (open) orelse catch_match
+hide_const (open) orelse catch_match mk_map_term check_all_n_lists
end
\ No newline at end of file
--- a/src/HOL/Tools/smallvalue_generators.ML Wed Dec 08 16:47:57 2010 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML Wed Dec 08 18:07:03 2010 +0100
@@ -81,7 +81,10 @@
fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
--> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
-
+
+fun check_allT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
+ --> @{typ "Code_Evaluation.term list option"}
+
fun mk_equations thy descr vs tycos smalls (Ts, Us) =
let
fun mk_small_call T =
@@ -217,6 +220,7 @@
fun mk_smart_generator_expr ctxt t =
let
+ val thy = ProofContext.theory_of ctxt
val ((vnames, Ts), t') = apfst split_list (strip_abs t)
val ([depth_name], ctxt') = Variable.variant_fixes ["depth"] ctxt
val (names, ctxt'') = Variable.variant_fixes vnames ctxt'
@@ -229,9 +233,14 @@
val (assms, concl) = strip_imp (subst_bounds (rev frees, t'))
val terms = HOLogic.mk_list @{typ term} (map (fn v => v $ @{term "()"}) term_vars)
fun mk_small_closure (free as Free (_, T), term_var) t =
- Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
- $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
- $ lambda free (lambda term_var t)) $ depth
+ if Sign.of_sort thy (T, @{sort enum}) then
+ Const (@{const_name "Smallcheck.check_all_class.check_all"}, check_allT T)
+ $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
+ $ lambda free (lambda term_var t))
+ else
+ Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
+ $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"})
+ $ lambda free (lambda term_var t)) $ depth
fun lookup v = the (AList.lookup (op =) (names ~~ (frees ~~ term_vars)) v)
val none_t = @{term "None :: term list option"}
fun mk_safe_if (cond, then_t, else_t) =