modernized setup;
authorwenzelm
Wed Oct 29 17:01:44 2014 +0100 (2014-10-29)
changeset 588252065f49da190
parent 58824 d480d1d7c544
child 58826 2ed2eaabe3df
modernized setup;
src/HOL/Library/Old_Recdef.thy
src/HOL/Library/Old_SMT.thy
src/HOL/Library/Old_SMT/old_smt_real.ML
src/HOL/Library/Old_SMT/old_smt_word.ML
src/HOL/Library/Refute.thy
src/HOL/Library/refute.ML
src/HOL/NSA/StarDef.thy
src/HOL/NSA/transfer.ML
src/HOL/Statespace/StateSpaceLocale.thy
src/HOL/Statespace/state_fun.ML
src/HOL/Tools/recdef.ML
     1.1 --- a/src/HOL/Library/Old_Recdef.thy	Wed Oct 29 15:28:27 2014 +0100
     1.2 +++ b/src/HOL/Library/Old_Recdef.thy	Wed Oct 29 17:01:44 2014 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  ML_file "~~/src/HOL/Tools/TFL/tfl.ML"
     1.5  ML_file "~~/src/HOL/Tools/TFL/post.ML"
     1.6  ML_file "~~/src/HOL/Tools/recdef.ML"
     1.7 -setup Recdef.setup
     1.8 +
     1.9  
    1.10  subsection {* Rule setup *}
    1.11  
     2.1 --- a/src/HOL/Library/Old_SMT.thy	Wed Oct 29 15:28:27 2014 +0100
     2.2 +++ b/src/HOL/Library/Old_SMT.thy	Wed Oct 29 17:01:44 2014 +0100
     2.3 @@ -420,10 +420,7 @@
     2.4    by auto
     2.5  
     2.6  ML_file "Old_SMT/old_smt_real.ML"
     2.7 -setup Old_SMT_Real.setup
     2.8 -
     2.9  ML_file "Old_SMT/old_smt_word.ML"
    2.10 -setup Old_SMT_Word.setup
    2.11  
    2.12  hide_type (open) pattern
    2.13  hide_const fun_app term_true term_false z3div z3mod
     3.1 --- a/src/HOL/Library/Old_SMT/old_smt_real.ML	Wed Oct 29 15:28:27 2014 +0100
     3.2 +++ b/src/HOL/Library/Old_SMT/old_smt_real.ML	Wed Oct 29 17:01:44 2014 +0100
     3.3 @@ -4,12 +4,7 @@
     3.4  SMT setup for reals.
     3.5  *)
     3.6  
     3.7 -signature OLD_SMT_REAL =
     3.8 -sig
     3.9 -  val setup: theory -> theory
    3.10 -end
    3.11 -
    3.12 -structure Old_SMT_Real: OLD_SMT_REAL =
    3.13 +structure Old_SMT_Real: sig end =
    3.14  struct
    3.15  
    3.16  
    3.17 @@ -125,12 +120,13 @@
    3.18  
    3.19  (* setup *)
    3.20  
    3.21 -val setup =
    3.22 -  Context.theory_map (
    3.23 -    Old_SMTLIB_Interface.add_logic (10, smtlib_logic) #>
    3.24 -    setup_builtins #>
    3.25 -    Old_Z3_Interface.add_mk_builtins z3_mk_builtins #>
    3.26 -    fold Old_Z3_Proof_Reconstruction.add_z3_rule real_rules #>
    3.27 -    Old_Z3_Proof_Tools.add_simproc real_linarith_proc)
    3.28 +val _ =
    3.29 +  Theory.setup
    3.30 +   (Context.theory_map (
    3.31 +      Old_SMTLIB_Interface.add_logic (10, smtlib_logic) #>
    3.32 +      setup_builtins #>
    3.33 +      Old_Z3_Interface.add_mk_builtins z3_mk_builtins #>
    3.34 +      fold Old_Z3_Proof_Reconstruction.add_z3_rule real_rules #>
    3.35 +      Old_Z3_Proof_Tools.add_simproc real_linarith_proc))
    3.36  
    3.37  end
     4.1 --- a/src/HOL/Library/Old_SMT/old_smt_word.ML	Wed Oct 29 15:28:27 2014 +0100
     4.2 +++ b/src/HOL/Library/Old_SMT/old_smt_word.ML	Wed Oct 29 17:01:44 2014 +0100
     4.3 @@ -4,12 +4,7 @@
     4.4  SMT setup for words.
     4.5  *)
     4.6  
     4.7 -signature OLD_SMT_WORD =
     4.8 -sig
     4.9 -  val setup: theory -> theory
    4.10 -end
    4.11 -
    4.12 -structure Old_SMT_Word: OLD_SMT_WORD =
    4.13 +structure Old_SMT_Word: sig end =
    4.14  struct
    4.15  
    4.16  open Word_Lib
    4.17 @@ -143,9 +138,9 @@
    4.18  
    4.19  (* setup *)
    4.20  
    4.21 -val setup = 
    4.22 -  Context.theory_map (
    4.23 -    Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #>
    4.24 -    setup_builtins)
    4.25 +val _ = 
    4.26 +  Theory.setup
    4.27 +    (Context.theory_map
    4.28 +      (Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #> setup_builtins))
    4.29  
    4.30  end
     5.1 --- a/src/HOL/Library/Refute.thy	Wed Oct 29 15:28:27 2014 +0100
     5.2 +++ b/src/HOL/Library/Refute.thy	Wed Oct 29 17:01:44 2014 +0100
     5.3 @@ -13,7 +13,6 @@
     5.4  begin
     5.5  
     5.6  ML_file "refute.ML"
     5.7 -setup Refute.setup
     5.8  
     5.9  refute_params
    5.10   [itself = 1,
     6.1 --- a/src/HOL/Library/refute.ML	Wed Oct 29 15:28:27 2014 +0100
     6.2 +++ b/src/HOL/Library/refute.ML	Wed Oct 29 17:01:44 2014 +0100
     6.3 @@ -52,8 +52,6 @@
     6.4    val refute_goal :
     6.5      Proof.context -> (string * string) list -> thm -> int -> string
     6.6  
     6.7 -  val setup : theory -> theory
     6.8 -
     6.9  (* ------------------------------------------------------------------------- *)
    6.10  (* Additional functions used by Nitpick (to be factored out)                 *)
    6.11  (* ------------------------------------------------------------------------- *)
    6.12 @@ -2926,37 +2924,33 @@
    6.13  
    6.14  
    6.15  (* ------------------------------------------------------------------------- *)
    6.16 -(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
    6.17 -(* structure                                                                 *)
    6.18 -(* ------------------------------------------------------------------------- *)
    6.19 -
    6.20 -(* ------------------------------------------------------------------------- *)
    6.21  (* Note: the interpreters and printers are used in reverse order; however,   *)
    6.22  (*       an interpreter that can handle non-atomic terms ends up being       *)
    6.23  (*       applied before the 'stlc_interpreter' breaks the term apart into    *)
    6.24  (*       subterms that are then passed to other interpreters!                *)
    6.25  (* ------------------------------------------------------------------------- *)
    6.26  (* FIXME formal @{const_name} for some entries (!??) *)
    6.27 -val setup =
    6.28 -   add_interpreter "stlc"    stlc_interpreter #>
    6.29 -   add_interpreter "Pure"    Pure_interpreter #>
    6.30 -   add_interpreter "HOLogic" HOLogic_interpreter #>
    6.31 -   add_interpreter "set"     set_interpreter #>
    6.32 -   add_interpreter "IDT"             IDT_interpreter #>
    6.33 -   add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
    6.34 -   add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>
    6.35 -   add_interpreter "Finite_Set.card"    Finite_Set_card_interpreter #>
    6.36 -   add_interpreter "Finite_Set.finite"  Finite_Set_finite_interpreter #>
    6.37 -   add_interpreter "Nat_Orderings.less" Nat_less_interpreter #>
    6.38 -   add_interpreter "Nat_HOL.plus"       Nat_plus_interpreter #>
    6.39 -   add_interpreter "Nat_HOL.minus"      Nat_minus_interpreter #>
    6.40 -   add_interpreter "Nat_HOL.times"      Nat_times_interpreter #>
    6.41 -   add_interpreter "List.append" List_append_interpreter #>
    6.42 -   add_interpreter "Product_Type.prod.fst" Product_Type_fst_interpreter #>
    6.43 -   add_interpreter "Product_Type.prod.snd" Product_Type_snd_interpreter #>
    6.44 -   add_printer "stlc" stlc_printer #>
    6.45 -   add_printer "set" set_printer #>
    6.46 -   add_printer "IDT"  IDT_printer;
    6.47 +val _ =
    6.48 +  Theory.setup
    6.49 +   (add_interpreter "stlc"    stlc_interpreter #>
    6.50 +    add_interpreter "Pure"    Pure_interpreter #>
    6.51 +    add_interpreter "HOLogic" HOLogic_interpreter #>
    6.52 +    add_interpreter "set"     set_interpreter #>
    6.53 +    add_interpreter "IDT"             IDT_interpreter #>
    6.54 +    add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
    6.55 +    add_interpreter "IDT_recursion"   IDT_recursion_interpreter #>
    6.56 +    add_interpreter "Finite_Set.card"    Finite_Set_card_interpreter #>
    6.57 +    add_interpreter "Finite_Set.finite"  Finite_Set_finite_interpreter #>
    6.58 +    add_interpreter "Nat_Orderings.less" Nat_less_interpreter #>
    6.59 +    add_interpreter "Nat_HOL.plus"       Nat_plus_interpreter #>
    6.60 +    add_interpreter "Nat_HOL.minus"      Nat_minus_interpreter #>
    6.61 +    add_interpreter "Nat_HOL.times"      Nat_times_interpreter #>
    6.62 +    add_interpreter "List.append" List_append_interpreter #>
    6.63 +    add_interpreter "Product_Type.prod.fst" Product_Type_fst_interpreter #>
    6.64 +    add_interpreter "Product_Type.prod.snd" Product_Type_snd_interpreter #>
    6.65 +    add_printer "stlc" stlc_printer #>
    6.66 +    add_printer "set" set_printer #>
    6.67 +    add_printer "IDT"  IDT_printer);
    6.68  
    6.69  
    6.70  
     7.1 --- a/src/HOL/NSA/StarDef.thy	Wed Oct 29 15:28:27 2014 +0100
     7.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Oct 29 17:01:44 2014 +0100
     7.3 @@ -88,7 +88,6 @@
     7.4  
     7.5  text {*Initialize transfer tactic.*}
     7.6  ML_file "transfer.ML"
     7.7 -setup Transfer_Principle.setup
     7.8  
     7.9  method_setup transfer = {*
    7.10    Attrib.thms >> (fn ths => fn ctxt =>
     8.1 --- a/src/HOL/NSA/transfer.ML	Wed Oct 29 15:28:27 2014 +0100
     8.2 +++ b/src/HOL/NSA/transfer.ML	Wed Oct 29 17:01:44 2014 +0100
     8.3 @@ -8,7 +8,6 @@
     8.4  sig
     8.5    val transfer_tac: Proof.context -> thm list -> int -> tactic
     8.6    val add_const: string -> theory -> theory
     8.7 -  val setup: theory -> theory
     8.8  end;
     8.9  
    8.10  structure Transfer_Principle: TRANSFER_PRINCIPLE =
    8.11 @@ -106,12 +105,13 @@
    8.12    (fn {intros,unfolds,refolds,consts} =>
    8.13      {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
    8.14  
    8.15 -val setup =
    8.16 -  Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
    8.17 -    "declaration of transfer introduction rule" #>
    8.18 -  Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
    8.19 -    "declaration of transfer unfolding rule" #>
    8.20 -  Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
    8.21 -    "declaration of transfer refolding rule"
    8.22 +val _ =
    8.23 +  Theory.setup
    8.24 +   (Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
    8.25 +      "declaration of transfer introduction rule" #>
    8.26 +    Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
    8.27 +      "declaration of transfer unfolding rule" #>
    8.28 +    Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
    8.29 +      "declaration of transfer refolding rule")
    8.30  
    8.31  end;
     9.1 --- a/src/HOL/Statespace/StateSpaceLocale.thy	Wed Oct 29 15:28:27 2014 +0100
     9.2 +++ b/src/HOL/Statespace/StateSpaceLocale.thy	Wed Oct 29 17:01:44 2014 +0100
     9.3 @@ -10,7 +10,6 @@
     9.4  
     9.5  ML_file "state_space.ML"
     9.6  ML_file "state_fun.ML"
     9.7 -setup StateFun.setup
     9.8  
     9.9  text {* For every type that is to be stored in a state space, an
    9.10  instance of this locale is imported in order convert the abstract and
    10.1 --- a/src/HOL/Statespace/state_fun.ML	Wed Oct 29 15:28:27 2014 +0100
    10.2 +++ b/src/HOL/Statespace/state_fun.ML	Wed Oct 29 17:01:44 2014 +0100
    10.3 @@ -16,8 +16,6 @@
    10.4    val ex_lookup_ss : simpset
    10.5    val lazy_conj_simproc : simproc
    10.6    val string_eq_simp_tac : Proof.context -> int -> tactic
    10.7 -
    10.8 -  val setup : theory -> theory
    10.9  end;
   10.10  
   10.11  structure StateFun: STATE_FUN =
   10.12 @@ -107,8 +105,7 @@
   10.13      (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
   10.14  );
   10.15  
   10.16 -val init_state_fun_data =
   10.17 -  Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false));
   10.18 +val _ = Theory.setup (Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false)));
   10.19  
   10.20  val lookup_simproc =
   10.21    Simplifier.simproc_global @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
   10.22 @@ -370,29 +367,27 @@
   10.23  val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ a $ b) "";
   10.24  val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ b $ a) "the_";
   10.25  
   10.26 -
   10.27 -val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn context =>
   10.28 -  let
   10.29 -    val ctxt = Context.proof_of context;
   10.30 -    val (lookup_ss, ex_lookup_ss, simprocs_active) = Data.get context;
   10.31 -    val (lookup_ss', ex_lookup_ss') =
   10.32 -      (case concl_of thm of
   10.33 -        (_ $ ((Const (@{const_name Ex}, _) $ _))) =>
   10.34 -          (lookup_ss, simpset_map ctxt (Simplifier.add_simp thm) ex_lookup_ss)
   10.35 -      | _ =>
   10.36 -          (simpset_map ctxt (Simplifier.add_simp thm) lookup_ss, ex_lookup_ss));
   10.37 -    val activate_simprocs =
   10.38 -      if simprocs_active then I
   10.39 -      else Simplifier.map_ss (fn ctxt => ctxt addsimprocs [lookup_simproc, update_simproc]);
   10.40 -  in
   10.41 -    context
   10.42 -    |> activate_simprocs
   10.43 -    |> Data.put (lookup_ss', ex_lookup_ss', true)
   10.44 -  end);
   10.45 -
   10.46 -val setup =
   10.47 -  init_state_fun_data #>
   10.48 -  Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr)
   10.49 -    "simplification in statespaces";
   10.50 +val _ =
   10.51 +  Theory.setup
   10.52 +    (Attrib.setup @{binding statefun_simp}
   10.53 +      (Scan.succeed (Thm.declaration_attribute (fn thm => fn context =>
   10.54 +        let
   10.55 +          val ctxt = Context.proof_of context;
   10.56 +          val (lookup_ss, ex_lookup_ss, simprocs_active) = Data.get context;
   10.57 +          val (lookup_ss', ex_lookup_ss') =
   10.58 +            (case concl_of thm of
   10.59 +              (_ $ ((Const (@{const_name Ex}, _) $ _))) =>
   10.60 +                (lookup_ss, simpset_map ctxt (Simplifier.add_simp thm) ex_lookup_ss)
   10.61 +            | _ =>
   10.62 +                (simpset_map ctxt (Simplifier.add_simp thm) lookup_ss, ex_lookup_ss));
   10.63 +          val activate_simprocs =
   10.64 +            if simprocs_active then I
   10.65 +            else Simplifier.map_ss (fn ctxt => ctxt addsimprocs [lookup_simproc, update_simproc]);
   10.66 +        in
   10.67 +          context
   10.68 +          |> activate_simprocs
   10.69 +          |> Data.put (lookup_ss', ex_lookup_ss', true)
   10.70 +        end)))
   10.71 +      "simplification in statespaces");
   10.72  
   10.73  end;
    11.1 --- a/src/HOL/Tools/recdef.ML	Wed Oct 29 15:28:27 2014 +0100
    11.2 +++ b/src/HOL/Tools/recdef.ML	Wed Oct 29 17:01:44 2014 +0100
    11.3 @@ -27,7 +27,6 @@
    11.4      local_theory -> Proof.state
    11.5    val recdef_tc_i: bstring * Token.src list -> string -> int option -> bool ->
    11.6      local_theory -> Proof.state
    11.7 -  val setup: theory -> theory
    11.8  end;
    11.9  
   11.10  structure Recdef: RECDEF =
   11.11 @@ -278,13 +277,14 @@
   11.12  
   11.13  (* setup theory *)
   11.14  
   11.15 -val setup =
   11.16 -  Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
   11.17 -    "declaration of recdef simp rule" #>
   11.18 -  Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
   11.19 -    "declaration of recdef cong rule" #>
   11.20 -  Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
   11.21 -    "declaration of recdef wf rule";
   11.22 +val _ =
   11.23 +  Theory.setup
   11.24 +   (Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
   11.25 +      "declaration of recdef simp rule" #>
   11.26 +    Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
   11.27 +      "declaration of recdef cong rule" #>
   11.28 +    Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
   11.29 +      "declaration of recdef wf rule");
   11.30  
   11.31  
   11.32  (* outer syntax *)