Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
authorblanchet
Fri Feb 06 15:57:47 2009 +0100 (2009-02-06)
changeset 29863dadad1831e9d
parent 29820 07f53494cf20
child 29864 be53632b7f8d
Added "nitpick_const_simps" and "nitpick_ind_intros" attributes for theorems;
these will be used by Nitpick, which will be released independently of Isabelle
2009, but they need to be in.
src/HOL/HOL.thy
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/primrec_package.ML
     1.1 --- a/src/HOL/HOL.thy	Fri Feb 06 13:43:19 2009 +0100
     1.2 +++ b/src/HOL/HOL.thy	Fri Feb 06 15:57:47 2009 +0100
     1.3 @@ -1701,6 +1701,23 @@
     1.4  *}
     1.5  
     1.6  
     1.7 +subsection {* Nitpick theorem store *}
     1.8 +
     1.9 +ML {*
    1.10 +structure Nitpick_Const_Simps_Thms = NamedThmsFun
    1.11 +(
    1.12 +  val name = "nitpick_const_simps"
    1.13 +  val description = "Equational specification of constants as needed by Nitpick"
    1.14 +)
    1.15 +structure Nitpick_Ind_Intros_Thms = NamedThmsFun
    1.16 +(
    1.17 +  val name = "nitpick_ind_intros"
    1.18 +  val description = "Introduction rules for inductive predicate as needed by Nitpick"
    1.19 +)
    1.20 +*}
    1.21 +setup {* Nitpick_Const_Simps_Thms.setup
    1.22 +         o Nitpick_Ind_Intros_Thms.setup *}
    1.23 +
    1.24  subsection {* Legacy tactics and ML bindings *}
    1.25  
    1.26  ML {*
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Feb 06 13:43:19 2009 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Feb 06 15:57:47 2009 +0100
     2.3 @@ -42,7 +42,8 @@
     2.4  
     2.5  fun add_simps fnames post sort extra_qualify label moreatts simps lthy =
     2.6      let
     2.7 -      val atts = Attrib.internal (K Simplifier.simp_add) :: moreatts
     2.8 +      val atts = Attrib.internal (K Simplifier.simp_add) ::
     2.9 +                 Attrib.internal (K Nitpick_Const_Simps_Thms.add) :: moreatts
    2.10        val spec = post simps
    2.11                     |> map (apfst (apsnd (append atts)))
    2.12                     |> map (apfst (apfst extra_qualify))
     3.1 --- a/src/HOL/Tools/function_package/size.ML	Fri Feb 06 13:43:19 2009 +0100
     3.2 +++ b/src/HOL/Tools/function_package/size.ML	Fri Feb 06 15:57:47 2009 +0100
     3.3 @@ -209,8 +209,9 @@
     3.4  
     3.5      val ([size_thms], thy'') =  PureThy.add_thmss
     3.6        [((Binding.name "size", size_eqns),
     3.7 -        [Simplifier.simp_add, Thm.declaration_attribute
     3.8 -              (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
     3.9 +        [Simplifier.simp_add, Nitpick_Const_Simps_Thms.add,
    3.10 +         Thm.declaration_attribute
    3.11 +             (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy'
    3.12  
    3.13    in
    3.14      SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
     4.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Feb 06 13:43:19 2009 +0100
     4.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Feb 06 15:57:47 2009 +0100
     4.3 @@ -691,7 +691,8 @@
     4.4        ctxt |>
     4.5        LocalTheory.notes kind
     4.6          (map rec_qualified intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
     4.7 -           [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>>
     4.8 +           [Attrib.internal (K (ContextRules.intro_query NONE)),
     4.9 +            Attrib.internal (K Nitpick_Ind_Intros_Thms.add)])]) intrs) |>>
    4.10        map (hd o snd);
    4.11      val (((_, elims'), (_, [induct'])), ctxt2) =
    4.12        ctxt1 |>
     5.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Feb 06 13:43:19 2009 +0100
     5.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Feb 06 15:57:47 2009 +0100
     5.3 @@ -251,7 +251,8 @@
     5.4        (space_implode "_" (map (Sign.base_name o #1) defs));
     5.5      val spec' = (map o apfst o apfst) qualify spec;
     5.6      val simp_atts = map (Attrib.internal o K)
     5.7 -      [Simplifier.simp_add, Code.add_default_eqn_attribute];
     5.8 +      [Simplifier.simp_add, Code.add_default_eqn_attribute,
     5.9 +       Nitpick_Const_Simps_Thms.add];
    5.10    in
    5.11      lthy
    5.12      |> set_group ? LocalTheory.set_group (serial_string ())