updated to named_theorems;
authorwenzelm
Sat Aug 16 14:32:26 2014 +0200 (2014-08-16)
changeset 579521a9a6dfc255f
parent 57951 7896762b638b
child 57953 69728243a614
updated to named_theorems;
src/HOL/Nat.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/arith_data.ML
src/HOL/Tools/lin_arith.ML
     1.1 --- a/src/HOL/Nat.thy	Sat Aug 16 14:27:41 2014 +0200
     1.2 +++ b/src/HOL/Nat.thy	Sat Aug 16 14:32:26 2014 +0200
     1.3 @@ -12,6 +12,8 @@
     1.4  begin
     1.5  
     1.6  ML_file "~~/src/Tools/rat.ML"
     1.7 +
     1.8 +named_theorems arith "arith facts -- only ground formulas"
     1.9  ML_file "Tools/arith_data.ML"
    1.10  ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
    1.11  
     2.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 16 14:27:41 2014 +0200
     2.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 16 14:32:26 2014 +0200
     2.3 @@ -862,9 +862,8 @@
     2.4    let
     2.5      val simpset_ctxt =
     2.6        put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths
     2.7 -    val aprems = Arith_Data.get_arith_facts ctxt
     2.8    in
     2.9 -    Method.insert_tac aprems
    2.10 +    Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith})
    2.11      THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
    2.12      THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    2.13      THEN_ALL_NEW simp_tac simpset_ctxt
     3.1 --- a/src/HOL/Tools/arith_data.ML	Sat Aug 16 14:27:41 2014 +0200
     3.2 +++ b/src/HOL/Tools/arith_data.ML	Sat Aug 16 14:32:26 2014 +0200
     3.3 @@ -9,7 +9,6 @@
     3.4    val arith_tac: Proof.context -> int -> tactic
     3.5    val verbose_arith_tac: Proof.context -> int -> tactic
     3.6    val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
     3.7 -  val get_arith_facts: Proof.context -> thm list
     3.8  
     3.9    val mk_number: typ -> int -> term
    3.10    val mk_sum: typ -> term list -> term
    3.11 @@ -28,15 +27,7 @@
    3.12  structure Arith_Data: ARITH_DATA =
    3.13  struct
    3.14  
    3.15 -(* slots for plugging in arithmetic facts and tactics *)
    3.16 -
    3.17 -structure Arith_Facts = Named_Thms
    3.18 -(
    3.19 -  val name = @{binding arith}
    3.20 -  val description = "arith facts -- only ground formulas"
    3.21 -);
    3.22 -
    3.23 -val get_arith_facts = Arith_Facts.get;
    3.24 +(* slot for plugging in tactics *)
    3.25  
    3.26  structure Arith_Tactics = Theory_Data
    3.27  (
    3.28 @@ -58,11 +49,12 @@
    3.29  val verbose_arith_tac = gen_arith_tac true;
    3.30  
    3.31  val setup =
    3.32 -  Arith_Facts.setup #>
    3.33    Method.setup @{binding arith}
    3.34      (Scan.succeed (fn ctxt =>
    3.35 -      METHOD (fn facts => HEADGOAL (Method.insert_tac (get_arith_facts ctxt @ facts)
    3.36 -        THEN' verbose_arith_tac ctxt))))
    3.37 +      METHOD (fn facts =>
    3.38 +        HEADGOAL
    3.39 +        (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
    3.40 +          THEN' verbose_arith_tac ctxt))))
    3.41      "various arithmetic decision procedures";
    3.42  
    3.43  
     4.1 --- a/src/HOL/Tools/lin_arith.ML	Sat Aug 16 14:27:41 2014 +0200
     4.2 +++ b/src/HOL/Tools/lin_arith.ML	Sat Aug 16 14:32:26 2014 +0200
     4.3 @@ -796,7 +796,7 @@
     4.4  
     4.5  (* FIXME !?? *)
     4.6  fun add_arith_facts ctxt =
     4.7 -  Simplifier.add_prems (Arith_Data.get_arith_facts ctxt) ctxt;
     4.8 +  Simplifier.add_prems (Named_Theorems.get ctxt @{named_theorems arith}) ctxt;
     4.9  
    4.10  val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
    4.11  
    4.12 @@ -889,7 +889,7 @@
    4.13    Method.setup @{binding linarith}
    4.14      (Scan.succeed (fn ctxt =>
    4.15        METHOD (fn facts =>
    4.16 -        HEADGOAL (Method.insert_tac (Arith_Data.get_arith_facts ctxt @ facts)
    4.17 +        HEADGOAL (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
    4.18            THEN' tac ctxt)))) "linear arithmetic" #>
    4.19    Arith_Data.add_tactic "linear arithmetic" gen_tac;
    4.20