# HG changeset patch # User wenzelm # Date 1414598504 -3600 # Node ID 2065f49da190d694868e13ba64d606294fd2e5ad # Parent d480d1d7c544f5fea824b675e9bdf873ec3b4486 modernized setup; diff -r d480d1d7c544 -r 2065f49da190 src/HOL/Library/Old_Recdef.thy --- a/src/HOL/Library/Old_Recdef.thy Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Library/Old_Recdef.thy Wed Oct 29 17:01:44 2014 +0100 @@ -68,7 +68,7 @@ ML_file "~~/src/HOL/Tools/TFL/tfl.ML" ML_file "~~/src/HOL/Tools/TFL/post.ML" ML_file "~~/src/HOL/Tools/recdef.ML" -setup Recdef.setup + subsection {* Rule setup *} diff -r d480d1d7c544 -r 2065f49da190 src/HOL/Library/Old_SMT.thy --- a/src/HOL/Library/Old_SMT.thy Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Library/Old_SMT.thy Wed Oct 29 17:01:44 2014 +0100 @@ -420,10 +420,7 @@ by auto ML_file "Old_SMT/old_smt_real.ML" -setup Old_SMT_Real.setup - ML_file "Old_SMT/old_smt_word.ML" -setup Old_SMT_Word.setup hide_type (open) pattern hide_const fun_app term_true term_false z3div z3mod diff -r d480d1d7c544 -r 2065f49da190 src/HOL/Library/Old_SMT/old_smt_real.ML --- a/src/HOL/Library/Old_SMT/old_smt_real.ML Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Library/Old_SMT/old_smt_real.ML Wed Oct 29 17:01:44 2014 +0100 @@ -4,12 +4,7 @@ SMT setup for reals. *) -signature OLD_SMT_REAL = -sig - val setup: theory -> theory -end - -structure Old_SMT_Real: OLD_SMT_REAL = +structure Old_SMT_Real: sig end = struct @@ -125,12 +120,13 @@ (* setup *) -val setup = - Context.theory_map ( - Old_SMTLIB_Interface.add_logic (10, smtlib_logic) #> - setup_builtins #> - Old_Z3_Interface.add_mk_builtins z3_mk_builtins #> - fold Old_Z3_Proof_Reconstruction.add_z3_rule real_rules #> - Old_Z3_Proof_Tools.add_simproc real_linarith_proc) +val _ = + Theory.setup + (Context.theory_map ( + Old_SMTLIB_Interface.add_logic (10, smtlib_logic) #> + setup_builtins #> + Old_Z3_Interface.add_mk_builtins z3_mk_builtins #> + fold Old_Z3_Proof_Reconstruction.add_z3_rule real_rules #> + Old_Z3_Proof_Tools.add_simproc real_linarith_proc)) end diff -r d480d1d7c544 -r 2065f49da190 src/HOL/Library/Old_SMT/old_smt_word.ML --- a/src/HOL/Library/Old_SMT/old_smt_word.ML Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Library/Old_SMT/old_smt_word.ML Wed Oct 29 17:01:44 2014 +0100 @@ -4,12 +4,7 @@ SMT setup for words. *) -signature OLD_SMT_WORD = -sig - val setup: theory -> theory -end - -structure Old_SMT_Word: OLD_SMT_WORD = +structure Old_SMT_Word: sig end = struct open Word_Lib @@ -143,9 +138,9 @@ (* setup *) -val setup = - Context.theory_map ( - Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #> - setup_builtins) +val _ = + Theory.setup + (Context.theory_map + (Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #> setup_builtins)) end diff -r d480d1d7c544 -r 2065f49da190 src/HOL/Library/Refute.thy --- a/src/HOL/Library/Refute.thy Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Library/Refute.thy Wed Oct 29 17:01:44 2014 +0100 @@ -13,7 +13,6 @@ begin ML_file "refute.ML" -setup Refute.setup refute_params [itself = 1, diff -r d480d1d7c544 -r 2065f49da190 src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Library/refute.ML Wed Oct 29 17:01:44 2014 +0100 @@ -52,8 +52,6 @@ val refute_goal : Proof.context -> (string * string) list -> thm -> int -> string - val setup : theory -> theory - (* ------------------------------------------------------------------------- *) (* Additional functions used by Nitpick (to be factored out) *) (* ------------------------------------------------------------------------- *) @@ -2926,37 +2924,33 @@ (* ------------------------------------------------------------------------- *) -(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *) -(* structure *) -(* ------------------------------------------------------------------------- *) - -(* ------------------------------------------------------------------------- *) (* Note: the interpreters and printers are used in reverse order; however, *) (* an interpreter that can handle non-atomic terms ends up being *) (* applied before the 'stlc_interpreter' breaks the term apart into *) (* subterms that are then passed to other interpreters! *) (* ------------------------------------------------------------------------- *) (* FIXME formal @{const_name} for some entries (!??) *) -val setup = - add_interpreter "stlc" stlc_interpreter #> - add_interpreter "Pure" Pure_interpreter #> - add_interpreter "HOLogic" HOLogic_interpreter #> - add_interpreter "set" set_interpreter #> - add_interpreter "IDT" IDT_interpreter #> - add_interpreter "IDT_constructor" IDT_constructor_interpreter #> - add_interpreter "IDT_recursion" IDT_recursion_interpreter #> - add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #> - add_interpreter "Finite_Set.finite" Finite_Set_finite_interpreter #> - add_interpreter "Nat_Orderings.less" Nat_less_interpreter #> - add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #> - add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #> - add_interpreter "Nat_HOL.times" Nat_times_interpreter #> - add_interpreter "List.append" List_append_interpreter #> - add_interpreter "Product_Type.prod.fst" Product_Type_fst_interpreter #> - add_interpreter "Product_Type.prod.snd" Product_Type_snd_interpreter #> - add_printer "stlc" stlc_printer #> - add_printer "set" set_printer #> - add_printer "IDT" IDT_printer; +val _ = + Theory.setup + (add_interpreter "stlc" stlc_interpreter #> + add_interpreter "Pure" Pure_interpreter #> + add_interpreter "HOLogic" HOLogic_interpreter #> + add_interpreter "set" set_interpreter #> + add_interpreter "IDT" IDT_interpreter #> + add_interpreter "IDT_constructor" IDT_constructor_interpreter #> + add_interpreter "IDT_recursion" IDT_recursion_interpreter #> + add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #> + add_interpreter "Finite_Set.finite" Finite_Set_finite_interpreter #> + add_interpreter "Nat_Orderings.less" Nat_less_interpreter #> + add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #> + add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #> + add_interpreter "Nat_HOL.times" Nat_times_interpreter #> + add_interpreter "List.append" List_append_interpreter #> + add_interpreter "Product_Type.prod.fst" Product_Type_fst_interpreter #> + add_interpreter "Product_Type.prod.snd" Product_Type_snd_interpreter #> + add_printer "stlc" stlc_printer #> + add_printer "set" set_printer #> + add_printer "IDT" IDT_printer); diff -r d480d1d7c544 -r 2065f49da190 src/HOL/NSA/StarDef.thy --- a/src/HOL/NSA/StarDef.thy Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/NSA/StarDef.thy Wed Oct 29 17:01:44 2014 +0100 @@ -88,7 +88,6 @@ text {*Initialize transfer tactic.*} ML_file "transfer.ML" -setup Transfer_Principle.setup method_setup transfer = {* Attrib.thms >> (fn ths => fn ctxt => diff -r d480d1d7c544 -r 2065f49da190 src/HOL/NSA/transfer.ML --- a/src/HOL/NSA/transfer.ML Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/NSA/transfer.ML Wed Oct 29 17:01:44 2014 +0100 @@ -8,7 +8,6 @@ sig val transfer_tac: Proof.context -> thm list -> int -> tactic val add_const: string -> theory -> theory - val setup: theory -> theory end; structure Transfer_Principle: TRANSFER_PRINCIPLE = @@ -106,12 +105,13 @@ (fn {intros,unfolds,refolds,consts} => {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts})) -val setup = - Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del) - "declaration of transfer introduction rule" #> - Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del) - "declaration of transfer unfolding rule" #> - Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del) - "declaration of transfer refolding rule" +val _ = + Theory.setup + (Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del) + "declaration of transfer introduction rule" #> + Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del) + "declaration of transfer unfolding rule" #> + Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del) + "declaration of transfer refolding rule") end; diff -r d480d1d7c544 -r 2065f49da190 src/HOL/Statespace/StateSpaceLocale.thy --- a/src/HOL/Statespace/StateSpaceLocale.thy Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Statespace/StateSpaceLocale.thy Wed Oct 29 17:01:44 2014 +0100 @@ -10,7 +10,6 @@ ML_file "state_space.ML" ML_file "state_fun.ML" -setup StateFun.setup text {* For every type that is to be stored in a state space, an instance of this locale is imported in order convert the abstract and diff -r d480d1d7c544 -r 2065f49da190 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Statespace/state_fun.ML Wed Oct 29 17:01:44 2014 +0100 @@ -16,8 +16,6 @@ val ex_lookup_ss : simpset val lazy_conj_simproc : simproc val string_eq_simp_tac : Proof.context -> int -> tactic - - val setup : theory -> theory end; structure StateFun: STATE_FUN = @@ -107,8 +105,7 @@ (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2); ); -val init_state_fun_data = - Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false)); +val _ = Theory.setup (Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false))); val lookup_simproc = Simplifier.simproc_global @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"] @@ -370,29 +367,27 @@ val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ a $ b) ""; val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ b $ a) "the_"; - -val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn context => - let - val ctxt = Context.proof_of context; - val (lookup_ss, ex_lookup_ss, simprocs_active) = Data.get context; - val (lookup_ss', ex_lookup_ss') = - (case concl_of thm of - (_ $ ((Const (@{const_name Ex}, _) $ _))) => - (lookup_ss, simpset_map ctxt (Simplifier.add_simp thm) ex_lookup_ss) - | _ => - (simpset_map ctxt (Simplifier.add_simp thm) lookup_ss, ex_lookup_ss)); - val activate_simprocs = - if simprocs_active then I - else Simplifier.map_ss (fn ctxt => ctxt addsimprocs [lookup_simproc, update_simproc]); - in - context - |> activate_simprocs - |> Data.put (lookup_ss', ex_lookup_ss', true) - end); - -val setup = - init_state_fun_data #> - Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr) - "simplification in statespaces"; +val _ = + Theory.setup + (Attrib.setup @{binding statefun_simp} + (Scan.succeed (Thm.declaration_attribute (fn thm => fn context => + let + val ctxt = Context.proof_of context; + val (lookup_ss, ex_lookup_ss, simprocs_active) = Data.get context; + val (lookup_ss', ex_lookup_ss') = + (case concl_of thm of + (_ $ ((Const (@{const_name Ex}, _) $ _))) => + (lookup_ss, simpset_map ctxt (Simplifier.add_simp thm) ex_lookup_ss) + | _ => + (simpset_map ctxt (Simplifier.add_simp thm) lookup_ss, ex_lookup_ss)); + val activate_simprocs = + if simprocs_active then I + else Simplifier.map_ss (fn ctxt => ctxt addsimprocs [lookup_simproc, update_simproc]); + in + context + |> activate_simprocs + |> Data.put (lookup_ss', ex_lookup_ss', true) + end))) + "simplification in statespaces"); end; diff -r d480d1d7c544 -r 2065f49da190 src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Wed Oct 29 15:28:27 2014 +0100 +++ b/src/HOL/Tools/recdef.ML Wed Oct 29 17:01:44 2014 +0100 @@ -27,7 +27,6 @@ local_theory -> Proof.state val recdef_tc_i: bstring * Token.src list -> string -> int option -> bool -> local_theory -> Proof.state - val setup: theory -> theory end; structure Recdef: RECDEF = @@ -278,13 +277,14 @@ (* setup theory *) -val setup = - Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del) - "declaration of recdef simp rule" #> - Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del) - "declaration of recdef cong rule" #> - Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del) - "declaration of recdef wf rule"; +val _ = + Theory.setup + (Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del) + "declaration of recdef simp rule" #> + Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del) + "declaration of recdef cong rule" #> + Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del) + "declaration of recdef wf rule"); (* outer syntax *)