# HG changeset patch
# User bulwahn
# Date 1242480232 -7200
# Node ID 74d72ba262fb58068f2ba91346bb55b3e9060844
# Parent  beb26c5901f3172d2df7a2a10633236fe5393ab6
added collection of simplification rules of recursive functions for quickcheck

diff -r beb26c5901f3 -r 74d72ba262fb src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat May 16 10:19:01 2009 +0200
+++ b/src/HOL/HOL.thy	Sat May 16 15:23:52 2009 +0200
@@ -1988,6 +1988,18 @@
 
 subsubsection {* Quickcheck *}
 
+ML {*
+structure Quickcheck_RecFun_Simp_Thms = NamedThmsFun
+(
+  val name = "quickcheck_recfun_simp"
+  val description = "simplification rules of recursive functions as needed by Quickcheck"
+)
+*}
+
+setup {*
+  Quickcheck_RecFun_Simp_Thms.setup
+*}
+
 setup {*
   Quickcheck.add_generator ("SML", Codegen.test_term)
 *}
diff -r beb26c5901f3 -r 74d72ba262fb src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sat May 16 10:19:01 2009 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat May 16 15:23:52 2009 +0200
@@ -37,7 +37,8 @@
 val simp_attribs = map (Attrib.internal o K)
     [Simplifier.simp_add,
      Code.add_default_eqn_attribute,
-     Nitpick_Const_Simp_Thms.add]
+     Nitpick_Const_Simp_Thms.add,
+     Quickcheck_RecFun_Simp_Thms.add]
 
 val psimp_attribs = map (Attrib.internal o K)
     [Simplifier.simp_add,
diff -r beb26c5901f3 -r 74d72ba262fb src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Sat May 16 10:19:01 2009 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Sat May 16 15:23:52 2009 +0200
@@ -247,7 +247,7 @@
     val spec' = (map o apfst)
       (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
     val simp_atts = map (Attrib.internal o K)
-      [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add];
+      [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add];
   in
     lthy
     |> set_group ? LocalTheory.set_group (serial_string ())
diff -r beb26c5901f3 -r 74d72ba262fb src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sat May 16 10:19:01 2009 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sat May 16 15:23:52 2009 +0200
@@ -208,7 +208,7 @@
                congs wfs name R eqs;
     val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
-      Code.add_default_eqn_attribute] else [];
+      Code.add_default_eqn_attribute, Quickcheck_RecFun_Simp_Thms.add] else [];
 
     val ((simps' :: rules', [induct']), thy) =
       thy