# HG changeset patch
# User bulwahn
# Date 1290422093 -3600
# Node ID 6e92ca8e981b653c9c70f40e5d04896b484a869f
# Parent  3dfa41e897382b2ee5cb45c91975e20b236200d5
adding prototype for finite_type instantiations

diff -r 3dfa41e89738 -r 6e92ca8e981b src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Mon Nov 22 11:34:52 2010 +0100
+++ b/src/HOL/Library/Enum.thy	Mon Nov 22 11:34:53 2010 +0100
@@ -305,4 +305,75 @@
 
 end
 
+subsection {* Small finite types *}
+
+text {* We define small finite types for the use in Quickcheck *}
+
+datatype finite_1 = a\<^isub>1
+
+instantiation finite_1 :: enum
+begin
+
+definition
+  "enum = [a\<^isub>1]"
+
+instance proof
+qed (auto simp add: enum_finite_1_def intro: finite_1.exhaust)
+
 end
+
+datatype finite_2 = a\<^isub>1 | a\<^isub>2
+
+instantiation finite_2 :: enum
+begin
+
+definition
+  "enum = [a\<^isub>1, a\<^isub>2]"
+
+instance proof
+qed (auto simp add: enum_finite_2_def intro: finite_2.exhaust)
+
+end
+
+datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
+
+instantiation finite_3 :: enum
+begin
+
+definition
+  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
+
+instance proof
+qed (auto simp add: enum_finite_3_def intro: finite_3.exhaust)
+
+end
+
+datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
+
+instantiation finite_4 :: enum
+begin
+
+definition
+  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
+
+instance proof
+qed (auto simp add: enum_finite_4_def intro: finite_4.exhaust)
+
+end
+
+datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
+
+instantiation finite_5 :: enum
+begin
+
+definition
+  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
+
+instance proof
+qed (auto simp add: enum_finite_5_def intro: finite_5.exhaust)
+
+end
+
+hide_type finite_1 finite_2 finite_3 finite_4 finite_5
+
+end
diff -r 3dfa41e89738 -r 6e92ca8e981b src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Mon Nov 22 11:34:52 2010 +0100
+++ b/src/Tools/quickcheck.ML	Mon Nov 22 11:34:53 2010 +0100
@@ -88,10 +88,11 @@
 val (quiet, setup_quiet) = Attrib.config_bool "quickcheck_quiet" (K false)
 val (timeout, setup_timeout) = Attrib.config_real "quickcheck_timeout" (K 30.0)
 val (finite_types, setup_finite_types) = Attrib.config_bool "quickcheck_finite_types" (K true)
+val (finite_type_size, setup_finite_type_size) = Attrib.config_int "quickcheck_finite_type_size" (K 3)
 
 val setup_config =
   setup_size #> setup_iterations #> setup_no_assms #> setup_report #> setup_quiet #> setup_timeout
-    #> setup_finite_types
+    #> setup_finite_types #> setup_finite_type_size
 
 datatype test_params = Test_Params of
   {default_type: typ list, expect : expectation};
@@ -246,6 +247,11 @@
     (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
   end;
 
+fun get_finite_types ctxt =
+  fst (chop (Config.get ctxt finite_type_size)
+    (map (Type o rpair []) ["Enum.finite_1", "Enum.finite_2", "Enum.finite_3",
+     "Enum.finite_4", "Enum.finite_5"]))  
+
 exception WELLSORTED of string
 
 fun monomorphic_term thy insts default_T = 
@@ -286,9 +292,15 @@
      of NONE => [proto_goal]
       | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal)
         (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
-    val inst_goals = maps (fn check_goal => map (fn T =>
-      Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
-        handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) check_goals
+    val inst_goals =
+      if Config.get lthy finite_types then 
+        maps (fn check_goal => map (fn T =>
+          Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
+            handle WELLSORTED s => Wellsorted_Error s) (get_finite_types lthy)) check_goals
+      else
+        maps (fn check_goal => map (fn T =>
+          Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
+            handle WELLSORTED s => Wellsorted_Error s) (default_type lthy)) check_goals
     val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals)
     val correct_inst_goals =
       case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
@@ -395,6 +407,7 @@
   | parse_test_param ("quiet", [arg]) = Config.put_generic quiet (read_bool arg)
   | parse_test_param ("timeout", [arg]) = Config.put_generic timeout (read_real arg)
   | parse_test_param ("finite_types", [arg]) = Config.put_generic finite_types (read_bool arg)
+  | parse_test_param ("finite_type_size", [arg]) = Config.put_generic finite_type_size (read_nat arg)
   | parse_test_param (name, _) = error ("Unknown test parameter: " ^ name);
 
 fun parse_test_param_inst ("generator", [arg]) ((generator, insts), ctxt) =