modernized setup;
authorwenzelm
Wed Oct 29 14:40:14 2014 +0100 (2014-10-29)
changeset 588203ad2759acc52
parent 58819 aa43c6f05bca
child 58821 11e226e8a095
modernized setup;
src/HOL/Nat.thy
src/HOL/Presburger.thy
src/HOL/Product_Type.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/split_rule.ML
     1.1 --- a/src/HOL/Nat.thy	Wed Oct 29 14:14:36 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Oct 29 14:40:14 2014 +0100
     1.3 @@ -1599,8 +1599,6 @@
     1.4    shows "u = s"
     1.5    using 2 1 by (rule trans)
     1.6  
     1.7 -setup Arith_Data.setup
     1.8 -
     1.9  ML_file "Tools/nat_arith.ML"
    1.10  
    1.11  simproc_setup nateq_cancel_sums
     2.1 --- a/src/HOL/Presburger.thy	Wed Oct 29 14:14:36 2014 +0100
     2.2 +++ b/src/HOL/Presburger.thy	Wed Oct 29 14:40:14 2014 +0100
     2.3 @@ -390,7 +390,6 @@
     2.4    by (simp cong: conj_cong)
     2.5  
     2.6  ML_file "Tools/Qelim/cooper.ML"
     2.7 -setup Cooper.setup
     2.8  
     2.9  method_setup presburger = {*
    2.10    let
     3.1 --- a/src/HOL/Product_Type.thy	Wed Oct 29 14:14:36 2014 +0100
     3.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 29 14:40:14 2014 +0100
     3.3 @@ -784,7 +784,6 @@
     3.4    by (simp only: internal_split_def split_conv)
     3.5  
     3.6  ML_file "Tools/split_rule.ML"
     3.7 -setup Split_Rule.setup
     3.8  
     3.9  hide_const internal_split
    3.10  
     4.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 29 14:14:36 2014 +0100
     4.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 29 14:40:14 2014 +0100
     4.3 @@ -13,7 +13,6 @@
     4.4    exception COOPER of string
     4.5    val conv: Proof.context -> conv
     4.6    val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
     4.7 -  val setup: theory -> theory
     4.8  end;
     4.9  
    4.10  structure Cooper: COOPER =
    4.11 @@ -835,6 +834,7 @@
    4.12        [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, 
    4.13         @{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
    4.14  in
    4.15 +
    4.16  fun nat_to_int_tac ctxt = 
    4.17    simp_tac (put_simpset ss1 ctxt) THEN_ALL_NEW
    4.18    simp_tac (put_simpset ss2 ctxt) THEN_ALL_NEW
    4.19 @@ -842,16 +842,17 @@
    4.20  
    4.21  fun div_mod_tac ctxt = simp_tac (put_simpset div_mod_ss ctxt);
    4.22  fun splits_tac ctxt = simp_tac (put_simpset splits_ss ctxt);
    4.23 +
    4.24  end;
    4.25  
    4.26  fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
    4.27     let
    4.28 -    val cpth = 
    4.29 +     val cpth = 
    4.30         if Config.get ctxt quick_and_dirty
    4.31         then oracle (ctxt, Envir.beta_norm (Envir.eta_long [] (term_of (Thm.dest_arg p))))
    4.32         else Conv.arg_conv (conv ctxt) p
    4.33 -    val p' = Thm.rhs_of cpth
    4.34 -    val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
    4.35 +     val p' = Thm.rhs_of cpth
    4.36 +     val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
    4.37     in rtac th i end
    4.38     handle COOPER _ => no_tac);
    4.39  
    4.40 @@ -881,7 +882,7 @@
    4.41    end 1);
    4.42  
    4.43  
    4.44 -(* theory setup *)
    4.45 +(* attribute syntax *)
    4.46  
    4.47  local
    4.48  
    4.49 @@ -896,11 +897,12 @@
    4.50  
    4.51  in
    4.52  
    4.53 -val setup =
    4.54 -  Attrib.setup @{binding presburger}
    4.55 -    ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
    4.56 -      optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
    4.57 -  #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] []));
    4.58 +val _ =
    4.59 +  Theory.setup
    4.60 +    (Attrib.setup @{binding presburger}
    4.61 +      ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
    4.62 +        optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
    4.63 +    #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] [])));
    4.64  
    4.65  end;
    4.66  
     5.1 --- a/src/HOL/Tools/arith_data.ML	Wed Oct 29 14:14:36 2014 +0100
     5.2 +++ b/src/HOL/Tools/arith_data.ML	Wed Oct 29 14:40:14 2014 +0100
     5.3 @@ -20,8 +20,6 @@
     5.4    val prove_conv2: tactic -> (Proof.context -> tactic) -> Proof.context -> term * term -> thm
     5.5    val simp_all_tac: thm list -> Proof.context -> tactic
     5.6    val simplify_meta_eq: thm list -> Proof.context -> thm -> thm
     5.7 -
     5.8 -  val setup: theory -> theory
     5.9  end;
    5.10  
    5.11  structure Arith_Data: ARITH_DATA =
    5.12 @@ -48,14 +46,15 @@
    5.13  val arith_tac = gen_arith_tac false;
    5.14  val verbose_arith_tac = gen_arith_tac true;
    5.15  
    5.16 -val setup =
    5.17 -  Method.setup @{binding arith}
    5.18 -    (Scan.succeed (fn ctxt =>
    5.19 -      METHOD (fn facts =>
    5.20 -        HEADGOAL
    5.21 -        (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
    5.22 -          THEN' verbose_arith_tac ctxt))))
    5.23 -    "various arithmetic decision procedures";
    5.24 +val _ =
    5.25 +  Theory.setup
    5.26 +    (Method.setup @{binding arith}
    5.27 +      (Scan.succeed (fn ctxt =>
    5.28 +        METHOD (fn facts =>
    5.29 +          HEADGOAL
    5.30 +          (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
    5.31 +            THEN' verbose_arith_tac ctxt))))
    5.32 +      "various arithmetic decision procedures");
    5.33  
    5.34  
    5.35  (* some specialized syntactic operations *)
     6.1 --- a/src/HOL/Tools/split_rule.ML	Wed Oct 29 14:14:36 2014 +0100
     6.2 +++ b/src/HOL/Tools/split_rule.ML	Wed Oct 29 14:40:14 2014 +0100
     6.3 @@ -9,7 +9,6 @@
     6.4    val split_rule_var: Proof.context -> term -> thm -> thm
     6.5    val split_rule: Proof.context -> thm -> thm
     6.6    val complete_split_rule: Proof.context -> thm -> thm
     6.7 -  val setup: theory -> theory
     6.8  end;
     6.9  
    6.10  structure Split_Rule: SPLIT_RULE =
    6.11 @@ -110,14 +109,15 @@
    6.12  
    6.13  (* attribute syntax *)
    6.14  
    6.15 -val setup =
    6.16 -  Attrib.setup @{binding split_format}
    6.17 -    (Scan.lift (Args.parens (Args.$$$ "complete")
    6.18 -      >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
    6.19 -    "split pair-typed subterms in premises, or function arguments" #>
    6.20 -  Attrib.setup @{binding split_rule}
    6.21 -    (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
    6.22 -    "curries ALL function variables occurring in a rule's conclusion";
    6.23 +val _ =
    6.24 +  Theory.setup
    6.25 +   (Attrib.setup @{binding split_format}
    6.26 +      (Scan.lift (Args.parens (Args.$$$ "complete")
    6.27 +        >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
    6.28 +      "split pair-typed subterms in premises, or function arguments" #>
    6.29 +    Attrib.setup @{binding split_rule}
    6.30 +      (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
    6.31 +      "curries ALL function variables occurring in a rule's conclusion");
    6.32  
    6.33  end;
    6.34