added collection of simplification rules of recursive functions for quickcheck
authorbulwahn
Sat May 16 15:23:52 2009 +0200 (2009-05-16)
changeset 3117274d72ba262fb
parent 31171 beb26c5901f3
child 31173 bbe9e29b9672
added collection of simplification rules of recursive functions for quickcheck
src/HOL/HOL.thy
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
     1.1 --- a/src/HOL/HOL.thy	Sat May 16 10:19:01 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat May 16 15:23:52 2009 +0200
     1.3 @@ -1988,6 +1988,18 @@
     1.4  
     1.5  subsubsection {* Quickcheck *}
     1.6  
     1.7 +ML {*
     1.8 +structure Quickcheck_RecFun_Simp_Thms = NamedThmsFun
     1.9 +(
    1.10 +  val name = "quickcheck_recfun_simp"
    1.11 +  val description = "simplification rules of recursive functions as needed by Quickcheck"
    1.12 +)
    1.13 +*}
    1.14 +
    1.15 +setup {*
    1.16 +  Quickcheck_RecFun_Simp_Thms.setup
    1.17 +*}
    1.18 +
    1.19  setup {*
    1.20    Quickcheck.add_generator ("SML", Codegen.test_term)
    1.21  *}
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat May 16 10:19:01 2009 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat May 16 15:23:52 2009 +0200
     2.3 @@ -37,7 +37,8 @@
     2.4  val simp_attribs = map (Attrib.internal o K)
     2.5      [Simplifier.simp_add,
     2.6       Code.add_default_eqn_attribute,
     2.7 -     Nitpick_Const_Simp_Thms.add]
     2.8 +     Nitpick_Const_Simp_Thms.add,
     2.9 +     Quickcheck_RecFun_Simp_Thms.add]
    2.10  
    2.11  val psimp_attribs = map (Attrib.internal o K)
    2.12      [Simplifier.simp_add,
     3.1 --- a/src/HOL/Tools/primrec_package.ML	Sat May 16 10:19:01 2009 +0200
     3.2 +++ b/src/HOL/Tools/primrec_package.ML	Sat May 16 15:23:52 2009 +0200
     3.3 @@ -247,7 +247,7 @@
     3.4      val spec' = (map o apfst)
     3.5        (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
     3.6      val simp_atts = map (Attrib.internal o K)
     3.7 -      [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add];
     3.8 +      [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add, Quickcheck_RecFun_Simp_Thms.add];
     3.9    in
    3.10      lthy
    3.11      |> set_group ? LocalTheory.set_group (serial_string ())
     4.1 --- a/src/HOL/Tools/recdef_package.ML	Sat May 16 10:19:01 2009 +0200
     4.2 +++ b/src/HOL/Tools/recdef_package.ML	Sat May 16 15:23:52 2009 +0200
     4.3 @@ -208,7 +208,7 @@
     4.4                 congs wfs name R eqs;
     4.5      val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     4.6      val simp_att = if null tcs then [Simplifier.simp_add, Nitpick_Const_Simp_Thms.add,
     4.7 -      Code.add_default_eqn_attribute] else [];
     4.8 +      Code.add_default_eqn_attribute, Quickcheck_RecFun_Simp_Thms.add] else [];
     4.9  
    4.10      val ((simps' :: rules', [induct']), thy) =
    4.11        thy