updated to named_theorems;
authorwenzelm
Sat Aug 16 22:14:57 2014 +0200 (2014-08-16)
changeset 579643dfc1bf3ac3d
parent 57963 cb67fac9bd89
child 57965 a18a351132b7
updated to named_theorems;
src/HOL/HOL.thy
src/HOL/Tools/Datatype/rep_datatype.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/recdef.ML
     1.1 --- a/src/HOL/HOL.thy	Sat Aug 16 21:11:08 2014 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Aug 16 22:14:57 2014 +0200
     1.3 @@ -1921,35 +1921,14 @@
     1.4  
     1.5  subsubsection {* Nitpick setup *}
     1.6  
     1.7 -ML {*
     1.8 -structure Nitpick_Unfolds = Named_Thms
     1.9 -(
    1.10 -  val name = @{binding nitpick_unfold}
    1.11 -  val description = "alternative definitions of constants as needed by Nitpick"
    1.12 -)
    1.13 -structure Nitpick_Simps = Named_Thms
    1.14 -(
    1.15 -  val name = @{binding nitpick_simp}
    1.16 -  val description = "equational specification of constants as needed by Nitpick"
    1.17 -)
    1.18 -structure Nitpick_Psimps = Named_Thms
    1.19 -(
    1.20 -  val name = @{binding nitpick_psimp}
    1.21 -  val description = "partial equational specification of constants as needed by Nitpick"
    1.22 -)
    1.23 -structure Nitpick_Choice_Specs = Named_Thms
    1.24 -(
    1.25 -  val name = @{binding nitpick_choice_spec}
    1.26 -  val description = "choice specification of constants as needed by Nitpick"
    1.27 -)
    1.28 -*}
    1.29 -
    1.30 -setup {*
    1.31 -  Nitpick_Unfolds.setup
    1.32 -  #> Nitpick_Simps.setup
    1.33 -  #> Nitpick_Psimps.setup
    1.34 -  #> Nitpick_Choice_Specs.setup
    1.35 -*}
    1.36 +named_theorems nitpick_unfold
    1.37 +  "alternative definitions of constants as needed by Nitpick"
    1.38 +named_theorems nitpick_simp
    1.39 +  "equational specification of constants as needed by Nitpick"
    1.40 +named_theorems nitpick_psimp
    1.41 +  "partial equational specification of constants as needed by Nitpick"
    1.42 +named_theorems nitpick_choice_spec
    1.43 +  "choice specification of constants as needed by Nitpick"
    1.44  
    1.45  declare if_bool_eq_conj [nitpick_unfold, no_atp]
    1.46          if_bool_eq_disj [no_atp]
     2.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Aug 16 21:11:08 2014 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Sat Aug 16 22:14:57 2014 +0200
     2.3 @@ -258,7 +258,8 @@
     2.4      thy2
     2.5      |> Sign.add_path (space_implode "_" new_type_names)
     2.6      |> Global_Theory.note_thmss ""
     2.7 -      [((Binding.name "rec", [Nitpick_Simps.add]), [(rec_thms, [])])]
     2.8 +      [((Binding.name "rec", [Named_Theorems.add @{named_theorems nitpick_simp}]),
     2.9 +          [(rec_thms, [])])]
    2.10      ||> Sign.parent_path
    2.11      |-> (fn thms => pair (reccomb_names, maps #2 thms))
    2.12    end;
    2.13 @@ -347,7 +348,8 @@
    2.14      val case_names = map case_name_of case_thms;
    2.15    in
    2.16      thy2
    2.17 -    |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms)
    2.18 +    |> Context.theory_map
    2.19 +        ((fold o fold) (Named_Theorems.add_thm @{named_theorems nitpick_simp}) case_thms)
    2.20      |> Sign.parent_path
    2.21      |> Datatype_Aux.store_thmss "case" new_type_names case_thms
    2.22      |-> (fn thmss => pair (thmss, case_names))
     3.1 --- a/src/HOL/Tools/Function/size.ML	Sat Aug 16 21:11:08 2014 +0200
     3.2 +++ b/src/HOL/Tools/Function/size.ML	Sat Aug 16 22:14:57 2014 +0200
     3.3 @@ -200,7 +200,7 @@
     3.4          val ([(_, size_thms)], thy'') = thy'
     3.5            |> Global_Theory.note_thmss ""
     3.6              [((Binding.name "size",
     3.7 -                [Simplifier.simp_add, Nitpick_Simps.add,
     3.8 +                [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp},
     3.9                   Thm.declaration_attribute (fn thm =>
    3.10                     Context.mapping (Code.add_default_eqn thm) I)]),
    3.11                [(size_eqns, [])])];
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Aug 16 21:11:08 2014 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Aug 16 22:14:57 2014 +0200
     4.3 @@ -1927,12 +1927,13 @@
     4.4      Const (s, _) => (s, t)
     4.5    | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t'])
     4.6  
     4.7 -fun def_table_for get ctxt subst =
     4.8 -  ctxt |> get |> map (pair_for_prop o subst_atomic subst)
     4.9 +fun def_table_for ts subst =
    4.10 +  ts |> map (pair_for_prop o subst_atomic subst)
    4.11         |> AList.group (op =) |> Symtab.make
    4.12  
    4.13  fun const_def_tables ctxt subst ts =
    4.14 -  (def_table_for (map prop_of o Nitpick_Unfolds.get) ctxt subst,
    4.15 +  (def_table_for
    4.16 +    (map prop_of (rev (Named_Theorems.get ctxt @{named_theorems nitpick_unfold}))) subst,
    4.17     fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
    4.18          (map pair_for_prop ts) Symtab.empty)
    4.19  
    4.20 @@ -1943,14 +1944,15 @@
    4.21  
    4.22  fun const_simp_table ctxt =
    4.23    def_table_for (map_filter (equationalize_term ctxt "nitpick_simp" o prop_of)
    4.24 -                 o Nitpick_Simps.get) ctxt
    4.25 +    (rev (Named_Theorems.get ctxt @{named_theorems nitpick_simp})))
    4.26  
    4.27  fun const_psimp_table ctxt =
    4.28    def_table_for (map_filter (equationalize_term ctxt "nitpick_psimp" o prop_of)
    4.29 -                 o Nitpick_Psimps.get) ctxt
    4.30 +    (rev (Named_Theorems.get ctxt @{named_theorems nitpick_psimp})))
    4.31  
    4.32  fun const_choice_spec_table ctxt subst =
    4.33 -  map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt)
    4.34 +  map (subst_atomic subst o prop_of)
    4.35 +    (rev (Named_Theorems.get ctxt @{named_theorems nitpick_choice_spec}))
    4.36    |> const_nondef_table
    4.37  
    4.38  fun inductive_intro_table ctxt subst def_tables =
    4.39 @@ -1958,9 +1960,8 @@
    4.40      def_table_for
    4.41          (maps (map (unfold_mutually_inductive_preds thy def_tables o prop_of)
    4.42                 o snd o snd)
    4.43 -         o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
    4.44 -                                  cat = Spec_Rules.Co_Inductive)
    4.45 -         o Spec_Rules.get) ctxt subst
    4.46 +         (filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse
    4.47 +                                 cat = Spec_Rules.Co_Inductive) (Spec_Rules.get ctxt))) subst
    4.48    end
    4.49  
    4.50  fun ground_theorem_table thy =
     5.1 --- a/src/HOL/Tools/recdef.ML	Sat Aug 16 21:11:08 2014 +0200
     5.2 +++ b/src/HOL/Tools/recdef.ML	Sat Aug 16 22:14:57 2014 +0200
     5.3 @@ -202,7 +202,8 @@
     5.4        tfl_fn not_permissive ctxt congs wfs name R eqs thy;
     5.5      val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
     5.6      val simp_att =
     5.7 -      if null tcs then [Simplifier.simp_add, Nitpick_Simps.add, Code.add_default_eqn_attribute]
     5.8 +      if null tcs then [Simplifier.simp_add,
     5.9 +        Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute]
    5.10        else [];
    5.11      val ((simps' :: rules', [induct']), thy) =
    5.12        thy