# HG changeset patch # User wenzelm # Date 1408220097 -7200 # Node ID 3dfc1bf3ac3da336e2eea798c8e2fbe89e1b9bba # Parent cb67fac9bd891389b8823667d68de556c6d83089 updated to named_theorems; diff -r cb67fac9bd89 -r 3dfc1bf3ac3d src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Aug 16 21:11:08 2014 +0200 +++ b/src/HOL/HOL.thy Sat Aug 16 22:14:57 2014 +0200 @@ -1921,35 +1921,14 @@ subsubsection {* Nitpick setup *} -ML {* -structure Nitpick_Unfolds = Named_Thms -( - val name = @{binding nitpick_unfold} - val description = "alternative definitions of constants as needed by Nitpick" -) -structure Nitpick_Simps = Named_Thms -( - val name = @{binding nitpick_simp} - val description = "equational specification of constants as needed by Nitpick" -) -structure Nitpick_Psimps = Named_Thms -( - val name = @{binding nitpick_psimp} - val description = "partial equational specification of constants as needed by Nitpick" -) -structure Nitpick_Choice_Specs = Named_Thms -( - val name = @{binding nitpick_choice_spec} - val description = "choice specification of constants as needed by Nitpick" -) -*} - -setup {* - Nitpick_Unfolds.setup - #> Nitpick_Simps.setup - #> Nitpick_Psimps.setup - #> Nitpick_Choice_Specs.setup -*} +named_theorems nitpick_unfold + "alternative definitions of constants as needed by Nitpick" +named_theorems nitpick_simp + "equational specification of constants as needed by Nitpick" +named_theorems nitpick_psimp + "partial equational specification of constants as needed by Nitpick" +named_theorems nitpick_choice_spec + "choice specification of constants as needed by Nitpick" declare if_bool_eq_conj [nitpick_unfold, no_atp] if_bool_eq_disj [no_atp] diff -r cb67fac9bd89 -r 3dfc1bf3ac3d src/HOL/Tools/Datatype/rep_datatype.ML --- a/src/HOL/Tools/Datatype/rep_datatype.ML Sat Aug 16 21:11:08 2014 +0200 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML Sat Aug 16 22:14:57 2014 +0200 @@ -258,7 +258,8 @@ thy2 |> Sign.add_path (space_implode "_" new_type_names) |> Global_Theory.note_thmss "" - [((Binding.name "rec", [Nitpick_Simps.add]), [(rec_thms, [])])] + [((Binding.name "rec", [Named_Theorems.add @{named_theorems nitpick_simp}]), + [(rec_thms, [])])] ||> Sign.parent_path |-> (fn thms => pair (reccomb_names, maps #2 thms)) end; @@ -347,7 +348,8 @@ val case_names = map case_name_of case_thms; in thy2 - |> Context.theory_map ((fold o fold) Nitpick_Simps.add_thm case_thms) + |> Context.theory_map + ((fold o fold) (Named_Theorems.add_thm @{named_theorems nitpick_simp}) case_thms) |> Sign.parent_path |> Datatype_Aux.store_thmss "case" new_type_names case_thms |-> (fn thmss => pair (thmss, case_names)) diff -r cb67fac9bd89 -r 3dfc1bf3ac3d src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Sat Aug 16 21:11:08 2014 +0200 +++ b/src/HOL/Tools/Function/size.ML Sat Aug 16 22:14:57 2014 +0200 @@ -200,7 +200,7 @@ val ([(_, size_thms)], thy'') = thy' |> Global_Theory.note_thmss "" [((Binding.name "size", - [Simplifier.simp_add, Nitpick_Simps.add, + [Simplifier.simp_add, Named_Theorems.add @{named_theorems nitpick_simp}, Thm.declaration_attribute (fn thm => Context.mapping (Code.add_default_eqn thm) I)]), [(size_eqns, [])])]; diff -r cb67fac9bd89 -r 3dfc1bf3ac3d src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Aug 16 21:11:08 2014 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sat Aug 16 22:14:57 2014 +0200 @@ -1927,12 +1927,13 @@ Const (s, _) => (s, t) | t' => raise TERM ("Nitpick_HOL.pair_for_prop", [t, t']) -fun def_table_for get ctxt subst = - ctxt |> get |> map (pair_for_prop o subst_atomic subst) +fun def_table_for ts subst = + ts |> map (pair_for_prop o subst_atomic subst) |> AList.group (op =) |> Symtab.make fun const_def_tables ctxt subst ts = - (def_table_for (map prop_of o Nitpick_Unfolds.get) ctxt subst, + (def_table_for + (map prop_of (rev (Named_Theorems.get ctxt @{named_theorems nitpick_unfold}))) subst, fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) (map pair_for_prop ts) Symtab.empty) @@ -1943,14 +1944,15 @@ fun const_simp_table ctxt = def_table_for (map_filter (equationalize_term ctxt "nitpick_simp" o prop_of) - o Nitpick_Simps.get) ctxt + (rev (Named_Theorems.get ctxt @{named_theorems nitpick_simp}))) fun const_psimp_table ctxt = def_table_for (map_filter (equationalize_term ctxt "nitpick_psimp" o prop_of) - o Nitpick_Psimps.get) ctxt + (rev (Named_Theorems.get ctxt @{named_theorems nitpick_psimp}))) fun const_choice_spec_table ctxt subst = - map (subst_atomic subst o prop_of) (Nitpick_Choice_Specs.get ctxt) + map (subst_atomic subst o prop_of) + (rev (Named_Theorems.get ctxt @{named_theorems nitpick_choice_spec})) |> const_nondef_table fun inductive_intro_table ctxt subst def_tables = @@ -1958,9 +1960,8 @@ def_table_for (maps (map (unfold_mutually_inductive_preds thy def_tables o prop_of) o snd o snd) - o filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse - cat = Spec_Rules.Co_Inductive) - o Spec_Rules.get) ctxt subst + (filter (fn (cat, _) => cat = Spec_Rules.Inductive orelse + cat = Spec_Rules.Co_Inductive) (Spec_Rules.get ctxt))) subst end fun ground_theorem_table thy = diff -r cb67fac9bd89 -r 3dfc1bf3ac3d src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Sat Aug 16 21:11:08 2014 +0200 +++ b/src/HOL/Tools/recdef.ML Sat Aug 16 22:14:57 2014 +0200 @@ -202,7 +202,8 @@ tfl_fn not_permissive ctxt congs wfs name R eqs thy; 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_Simps.add, Code.add_default_eqn_attribute] + if null tcs then [Simplifier.simp_add, + Named_Theorems.add @{named_theorems nitpick_simp}, Code.add_default_eqn_attribute] else []; val ((simps' :: rules', [induct']), thy) = thy