improved handling of overloaded constants; examples with numerals

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -37,8 +37,7 @@
   map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n"
     ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
 
-(* TODO: *)
-fun overload_const thy s = s
+fun overload_const thy s = the_default s (Option.map fst (AxClass.inst_of_param thy s))
 
 fun map_specs f specs =
   map (fn (s, ths) => (s, f ths)) specs
@@ -87,8 +86,8 @@
     val _ = print_intross options thy''' "Introduction rules with new constants: " intross3
     val intross4 = map_specs (maps remove_pointless_clauses) intross3
     val _ = print_intross options thy''' "After removing pointless clauses: " intross4
-    val intross5 = (*map (fn (s, ths) => (overload_const s, map (AxClass.overload thy''') ths))*) intross4
-    val intross6 = map_specs (map (expand_tuples thy''')) intross4
+    val intross5 = map (fn (s, ths) => (overload_const thy''' s, map (AxClass.overload thy''') ths)) intross4
+    val intross6 = map_specs (map (expand_tuples thy''')) intross5
     val _ = print_intross options thy''' "introduction rules before registering: " intross6
     val _ = print_step options "Registering introduction rules..."
     val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -33,7 +33,8 @@
   
   inductify = false,
   random = false,
-  depth_limited = false
+  depth_limited = false,
+  annotated = false
 }
 
 fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs

--- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy	Fri Nov 06 08:11:58 2009 +0100
@@ -9,7 +9,9 @@
 quickcheck[generator=predicate_compile]
 oops
 
+(* TODO: some error with doubled negation *)
 lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0"
+(*quickcheck[generator=predicate_compile]*)
 oops
 
 lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x = Suc 0"
@@ -23,12 +25,17 @@
 section {* Numerals *}
 
 lemma
-  "x \<in> {1, 2, (3::nat)} ==> x < 3"
+  "x \<in> {1, 2, (3::nat)} ==> x = 1 \<or> x = 2"
+quickcheck[generator=predicate_compile]
+oops
+
+lemma "x \<in> {1, 2, (3::nat)} ==> x < 3"
 (*quickcheck[generator=predicate_compile]*)
 oops
+
 lemma
-  "x \<in> {1, 2} \<union> {3, 4} ==> x > 4"
-(*quickcheck[generator=predicate_compile]*)
+  "x \<in> {1, 2} \<union> {3, 4} ==> x = (1::nat) \<or> x = (2::nat)"
+quickcheck[generator=predicate_compile]
 oops
 
 section {* Context Free Grammar *}

--- a/src/HOL/ex/Predicate_Compile_ex.thy	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Fri Nov 06 08:11:58 2009 +0100
@@ -188,13 +188,23 @@
 (*values "{x. one_or_two x}"*)
 values [random] "{x. one_or_two x}"
 
-definition one_or_two':
-  "one_or_two' == {1, (2::nat)}"
+inductive one_or_two' :: "nat => bool"
+where
+  "one_or_two' 1"
+| "one_or_two' 2"
+
+code_pred one_or_two' .
+thm one_or_two'.equation
 
-code_pred [inductify] one_or_two' .
-thm one_or_two'.equation
-(* TODO: handling numerals *)
-(*values "{x. one_or_two' x}"*)
+values "{x. one_or_two' x}"
+
+definition one_or_two'':
+  "one_or_two'' == {1, (2::nat)}"
+
+code_pred [inductify] one_or_two'' .
+thm one_or_two''.equation
+
+values "{x. one_or_two'' x}"
 
 
 subsection {* even predicate *}