arith method setup: proper context;
authorwenzelm
Tue Jul 31 00:56:26 2007 +0200 (2007-07-31)
changeset 24075366d4d234814
parent 24074 40f414b87655
child 24076 ae946f751c44
arith method setup: proper context;
src/HOL/Arith_Tools.thy
src/HOL/Complex/ex/BinEx.thy
src/HOL/HoareParallel/OG_Examples.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/hypreal_arith.ML
src/HOL/IntArith.thy
src/HOL/Nat.thy
src/HOL/NatBin.thy
src/HOL/Presburger.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/TFL/post.ML
src/HOL/ex/Arith_Examples.thy
src/HOL/int_arith1.ML
     1.1 --- a/src/HOL/Arith_Tools.thy	Mon Jul 30 19:46:15 2007 +0200
     1.2 +++ b/src/HOL/Arith_Tools.thy	Tue Jul 31 00:56:26 2007 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  subsection {* Simprocs for the Naturals *}
     1.6  
     1.7 -setup nat_simprocs_setup
     1.8 +declaration {* K nat_simprocs_setup *}
     1.9  
    1.10  subsubsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}
    1.11  
     2.1 --- a/src/HOL/Complex/ex/BinEx.thy	Mon Jul 30 19:46:15 2007 +0200
     2.2 +++ b/src/HOL/Complex/ex/BinEx.thy	Tue Jul 31 00:56:26 2007 +0200
     2.3 @@ -338,38 +338,38 @@
     2.4  by arith
     2.5  
     2.6  lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
     2.7 -by (tactic "fast_arith_tac 1")
     2.8 +by (tactic "fast_arith_tac @{context} 1")
     2.9  
    2.10  lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
    2.11 -by (tactic "fast_arith_tac 1")
    2.12 +by (tactic "fast_arith_tac @{context} 1")
    2.13  
    2.14  lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
    2.15 -by (tactic "fast_arith_tac 1")
    2.16 +by (tactic "fast_arith_tac @{context} 1")
    2.17  
    2.18  lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
    2.19 -by (tactic "fast_arith_tac 1")
    2.20 +by (tactic "fast_arith_tac @{context} 1")
    2.21  
    2.22  lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
    2.23 -by (tactic "fast_arith_tac 1")
    2.24 +by (tactic "fast_arith_tac @{context} 1")
    2.25  
    2.26  lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"
    2.27  by arith
    2.28  
    2.29  lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
    2.30      ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
    2.31 -by (tactic "fast_arith_tac 1")
    2.32 +by (tactic "fast_arith_tac @{context} 1")
    2.33  
    2.34  lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
    2.35      ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
    2.36 -by (tactic "fast_arith_tac 1")
    2.37 +by (tactic "fast_arith_tac @{context} 1")
    2.38  
    2.39  lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
    2.40      ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
    2.41 -by (tactic "fast_arith_tac 1")
    2.42 +by (tactic "fast_arith_tac @{context} 1")
    2.43  
    2.44  lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
    2.45      ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"
    2.46 -by (tactic "fast_arith_tac 1")
    2.47 +by (tactic "fast_arith_tac @{context} 1")
    2.48  
    2.49  
    2.50  subsection{*Complex Arithmetic*}
     3.1 --- a/src/HOL/HoareParallel/OG_Examples.thy	Mon Jul 30 19:46:15 2007 +0200
     3.2 +++ b/src/HOL/HoareParallel/OG_Examples.thy	Tue Jul 31 00:56:26 2007 +0200
     3.3 @@ -443,7 +443,7 @@
     3.4  --{* 32 subgoals left *}
     3.5  apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
     3.6  
     3.7 -apply(tactic {* TRYALL simple_arith_tac *})
     3.8 +apply(tactic {* TRYALL (simple_arith_tac @{context}) *})
     3.9  --{* 9 subgoals left *}
    3.10  apply (force simp add:less_Suc_eq)
    3.11  apply(drule sym)
     4.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Mon Jul 30 19:46:15 2007 +0200
     4.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Jul 31 00:56:26 2007 +0200
     4.3 @@ -340,8 +340,7 @@
     4.4  *)
     4.5  
     4.6  use "hypreal_arith.ML"
     4.7 -
     4.8 -setup hypreal_arith_setup
     4.9 +declaration {* K hypreal_arith_setup *}
    4.10  
    4.11  
    4.12  subsection {* Exponentials on the Hyperreals *}
     5.1 --- a/src/HOL/Hyperreal/hypreal_arith.ML	Mon Jul 30 19:46:15 2007 +0200
     5.2 +++ b/src/HOL/Hyperreal/hypreal_arith.ML	Tue Jul 31 00:56:26 2007 +0200
     5.3 @@ -30,7 +30,7 @@
     5.4      Simplifier.simproc (the_context ())
     5.5        "fast_hypreal_arith" 
     5.6        ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
     5.7 -    Fast_Arith.lin_arith_prover;
     5.8 +    (K Fast_Arith.lin_arith_simproc);
     5.9  
    5.10  val hypreal_arith_setup =
    5.11    Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
    5.12 @@ -41,6 +41,6 @@
    5.13      neqE = neqE,
    5.14      simpset = simpset addsimps simps}) #>
    5.15    arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
    5.16 -  (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy));
    5.17 +  Simplifier.map_ss (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]);
    5.18  
    5.19  end;
     6.1 --- a/src/HOL/IntArith.thy	Mon Jul 30 19:46:15 2007 +0200
     6.2 +++ b/src/HOL/IntArith.thy	Tue Jul 31 00:56:26 2007 +0200
     6.3 @@ -115,7 +115,7 @@
     6.4   min_def[of "number_of u" "1::int", standard, simp]
     6.5  
     6.6  use "int_arith1.ML"
     6.7 -setup int_arith_setup
     6.8 +declaration {* K int_arith_setup *}
     6.9  
    6.10  
    6.11  subsection{*Lemmas About Small Numerals*}
     7.1 --- a/src/HOL/Nat.thy	Mon Jul 30 19:46:15 2007 +0200
     7.2 +++ b/src/HOL/Nat.thy	Tue Jul 31 00:56:26 2007 +0200
     7.3 @@ -1092,7 +1092,7 @@
     7.4    using 2 1 by (rule trans)
     7.5  
     7.6  use "arith_data.ML"
     7.7 -setup arith_setup
     7.8 +declaration {* K arith_setup *}
     7.9  
    7.10  text{*The following proofs may rely on the arithmetic proof procedures.*}
    7.11  
     8.1 --- a/src/HOL/NatBin.thy	Mon Jul 30 19:46:15 2007 +0200
     8.2 +++ b/src/HOL/NatBin.thy	Tue Jul 31 00:56:26 2007 +0200
     8.3 @@ -666,7 +666,7 @@
     8.4                                    neg_number_of_Min,neg_number_of_BIT]})
     8.5  *}
     8.6  
     8.7 -setup nat_bin_arith_setup
     8.8 +declaration {* K nat_bin_arith_setup *}
     8.9  
    8.10  (* Enable arith to deal with div/mod k where k is a numeral: *)
    8.11  declare split_div[of _ _ "number_of k", standard, arith_split]
     9.1 --- a/src/HOL/Presburger.thy	Mon Jul 30 19:46:15 2007 +0200
     9.2 +++ b/src/HOL/Presburger.thy	Tue Jul 31 00:56:26 2007 +0200
     9.3 @@ -439,8 +439,8 @@
     9.4  
     9.5  use "Tools/Qelim/presburger.ML"
     9.6  
     9.7 -setup {* 
     9.8 -  arith_tactic_add 
     9.9 +declaration {* fn _ =>
    9.10 +  arith_tactic_add
    9.11      (mk_arith_tactic "presburger" (fn i => fn st =>
    9.12         (warning "Trying Presburger arithmetic ...";   
    9.13      Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st)))
    10.1 --- a/src/HOL/Real/Rational.thy	Mon Jul 30 19:46:15 2007 +0200
    10.2 +++ b/src/HOL/Real/Rational.thy	Tue Jul 31 00:56:26 2007 +0200
    10.3 @@ -469,7 +469,7 @@
    10.4    by default (simp add: rat_number_of_def) 
    10.5  
    10.6  use "rat_arith.ML"
    10.7 -setup rat_arith_setup
    10.8 +declaration {* K rat_arith_setup *}
    10.9  
   10.10  
   10.11  subsection {* Embedding from Rationals to other Fields *}
    11.1 --- a/src/HOL/Real/RealDef.thy	Mon Jul 30 19:46:15 2007 +0200
    11.2 +++ b/src/HOL/Real/RealDef.thy	Tue Jul 31 00:56:26 2007 +0200
    11.3 @@ -832,8 +832,7 @@
    11.4   
    11.5  
    11.6  use "real_arith.ML"
    11.7 -
    11.8 -setup real_arith_setup
    11.9 +declaration {* K real_arith_setup *}
   11.10  
   11.11  
   11.12  subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
    12.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Jul 30 19:46:15 2007 +0200
    12.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Jul 31 00:56:26 2007 +0200
    12.3 @@ -173,7 +173,7 @@
    12.4  
    12.5      (* Canonical linear form for terms, formulae etc.. *)
    12.6  fun provelin ctxt t = Goal.prove ctxt [] [] t 
    12.7 -                          (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac 1)]);
    12.8 +  (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac ctxt 1)]);
    12.9  fun linear_cmul 0 tm =  zero 
   12.10    | linear_cmul n tm = 
   12.11      case tm of  
    13.1 --- a/src/HOL/Tools/TFL/post.ML	Mon Jul 30 19:46:15 2007 +0200
    13.2 +++ b/src/HOL/Tools/TFL/post.ML	Tue Jul 31 00:56:26 2007 +0200
    13.3 @@ -68,7 +68,7 @@
    13.4    Prim.postprocess strict
    13.5     {wf_tac     = REPEAT (ares_tac wfs 1),
    13.6      terminator = asm_simp_tac ss 1
    13.7 -                 THEN TRY (silent_arith_tac 1 ORELSE
    13.8 +                 THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE
    13.9                             fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1),
   13.10      simplifier = Rules.simpl_conv ss []};
   13.11  
    14.1 --- a/src/HOL/ex/Arith_Examples.thy	Mon Jul 30 19:46:15 2007 +0200
    14.2 +++ b/src/HOL/ex/Arith_Examples.thy	Tue Jul 31 00:56:26 2007 +0200
    14.3 @@ -20,7 +20,7 @@
    14.4    as well.  This is the one that you should use in your proofs!
    14.5  
    14.6    An @{text arith}-based simproc is available as well
    14.7 -  (see @{ML Fast_Arith.lin_arith_prover}),
    14.8 +  (see @{ML Fast_Arith.lin_arith_simproc}),
    14.9    which---for performance reasons---however
   14.10    does even less splitting than @{ML fast_arith_tac} at the moment (namely
   14.11    inequalities only).  (On the other hand, it does take apart conjunctions,
   14.12 @@ -36,159 +36,159 @@
   14.13             @{term Divides.div} *}
   14.14  
   14.15  lemma "(i::nat) <= max i j"
   14.16 -  by (tactic {* fast_arith_tac 1 *})
   14.17 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.18  
   14.19  lemma "(i::int) <= max i j"
   14.20 -  by (tactic {* fast_arith_tac 1 *})
   14.21 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.22  
   14.23  lemma "min i j <= (i::nat)"
   14.24 -  by (tactic {* fast_arith_tac 1 *})
   14.25 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.26  
   14.27  lemma "min i j <= (i::int)"
   14.28 -  by (tactic {* fast_arith_tac 1 *})
   14.29 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.30  
   14.31  lemma "min (i::nat) j <= max i j"
   14.32 -  by (tactic {* fast_arith_tac 1 *})
   14.33 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.34  
   14.35  lemma "min (i::int) j <= max i j"
   14.36 -  by (tactic {* fast_arith_tac 1 *})
   14.37 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.38  
   14.39  lemma "min (i::nat) j + max i j = i + j"
   14.40 -  by (tactic {* fast_arith_tac 1 *})
   14.41 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.42  
   14.43  lemma "min (i::int) j + max i j = i + j"
   14.44 -  by (tactic {* fast_arith_tac 1 *})
   14.45 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.46  
   14.47  lemma "(i::nat) < j ==> min i j < max i j"
   14.48 -  by (tactic {* fast_arith_tac 1 *})
   14.49 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.50  
   14.51  lemma "(i::int) < j ==> min i j < max i j"
   14.52 -  by (tactic {* fast_arith_tac 1 *})
   14.53 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.54  
   14.55  lemma "(0::int) <= abs i"
   14.56 -  by (tactic {* fast_arith_tac 1 *})
   14.57 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.58  
   14.59  lemma "(i::int) <= abs i"
   14.60 -  by (tactic {* fast_arith_tac 1 *})
   14.61 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.62  
   14.63  lemma "abs (abs (i::int)) = abs i"
   14.64 -  by (tactic {* fast_arith_tac 1 *})
   14.65 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.66  
   14.67  text {* Also testing subgoals with bound variables. *}
   14.68  
   14.69  lemma "!!x. (x::nat) <= y ==> x - y = 0"
   14.70 -  by (tactic {* fast_arith_tac 1 *})
   14.71 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.72  
   14.73  lemma "!!x. (x::nat) - y = 0 ==> x <= y"
   14.74 -  by (tactic {* fast_arith_tac 1 *})
   14.75 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.76  
   14.77  lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
   14.78 -  by (tactic {* simple_arith_tac 1 *})
   14.79 +  by (tactic {* simple_arith_tac @{context} 1 *})
   14.80  
   14.81  lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
   14.82 -  by (tactic {* fast_arith_tac 1 *})
   14.83 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.84  
   14.85  lemma "[| (x::nat) < y; d < 1 |] ==> x - y - x = d - x"
   14.86 -  by (tactic {* fast_arith_tac 1 *})
   14.87 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.88  
   14.89  lemma "(x::int) < y ==> x - y < 0"
   14.90 -  by (tactic {* fast_arith_tac 1 *})
   14.91 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.92  
   14.93  lemma "nat (i + j) <= nat i + nat j"
   14.94 -  by (tactic {* fast_arith_tac 1 *})
   14.95 +  by (tactic {* fast_arith_tac @{context} 1 *})
   14.96  
   14.97  lemma "i < j ==> nat (i - j) = 0"
   14.98 -  by (tactic {* fast_arith_tac 1 *})
   14.99 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.100  
  14.101  lemma "(i::nat) mod 0 = i"
  14.102    (* FIXME: need to replace 0 by its numeral representation *)
  14.103    apply (subst nat_numeral_0_eq_0 [symmetric])
  14.104 -  by (tactic {* fast_arith_tac 1 *})
  14.105 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.106  
  14.107  lemma "(i::nat) mod 1 = 0"
  14.108    (* FIXME: need to replace 1 by its numeral representation *)
  14.109    apply (subst nat_numeral_1_eq_1 [symmetric])
  14.110 -  by (tactic {* fast_arith_tac 1 *})
  14.111 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.112  
  14.113  lemma "(i::nat) mod 42 <= 41"
  14.114 -  by (tactic {* fast_arith_tac 1 *})
  14.115 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.116  
  14.117  lemma "(i::int) mod 0 = i"
  14.118    (* FIXME: need to replace 0 by its numeral representation *)
  14.119    apply (subst numeral_0_eq_0 [symmetric])
  14.120 -  by (tactic {* fast_arith_tac 1 *})
  14.121 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.122  
  14.123  lemma "(i::int) mod 1 = 0"
  14.124    (* FIXME: need to replace 1 by its numeral representation *)
  14.125    apply (subst numeral_1_eq_1 [symmetric])
  14.126    (* FIXME: arith does not know about iszero *)
  14.127 -  apply (tactic {* LA_Data_Ref.pre_tac 1 *})
  14.128 +  apply (tactic {* LA_Data_Ref.pre_tac @{context} 1 *})
  14.129  oops
  14.130  
  14.131  lemma "(i::int) mod 42 <= 41"
  14.132    (* FIXME: arith does not know about iszero *)
  14.133 -  apply (tactic {* LA_Data_Ref.pre_tac 1 *})
  14.134 +  apply (tactic {* LA_Data_Ref.pre_tac @{context} 1 *})
  14.135  oops
  14.136  
  14.137  
  14.138  subsection {* Meta-Logic *}
  14.139  
  14.140  lemma "x < Suc y == x <= y"
  14.141 -  by (tactic {* simple_arith_tac 1 *})
  14.142 +  by (tactic {* simple_arith_tac @{context} 1 *})
  14.143  
  14.144  lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
  14.145 -  by (tactic {* simple_arith_tac 1 *})
  14.146 +  by (tactic {* simple_arith_tac @{context} 1 *})
  14.147  
  14.148  
  14.149  subsection {* Various Other Examples *}
  14.150  
  14.151  lemma "(x < Suc y) = (x <= y)"
  14.152 -  by (tactic {* simple_arith_tac 1 *})
  14.153 +  by (tactic {* simple_arith_tac @{context} 1 *})
  14.154  
  14.155  lemma "[| (x::nat) < y; y < z |] ==> x < z"
  14.156 -  by (tactic {* fast_arith_tac 1 *})
  14.157 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.158  
  14.159  lemma "(x::nat) < y & y < z ==> x < z"
  14.160 -  by (tactic {* simple_arith_tac 1 *})
  14.161 +  by (tactic {* simple_arith_tac @{context} 1 *})
  14.162  
  14.163  text {* This example involves no arithmetic at all, but is solved by
  14.164    preprocessing (i.e. NNF normalization) alone. *}
  14.165  
  14.166  lemma "(P::bool) = Q ==> Q = P"
  14.167 -  by (tactic {* simple_arith_tac 1 *})
  14.168 +  by (tactic {* simple_arith_tac @{context} 1 *})
  14.169  
  14.170  lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
  14.171 -  by (tactic {* simple_arith_tac 1 *})
  14.172 +  by (tactic {* simple_arith_tac @{context} 1 *})
  14.173  
  14.174  lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
  14.175 -  by (tactic {* simple_arith_tac 1 *})
  14.176 +  by (tactic {* simple_arith_tac @{context} 1 *})
  14.177  
  14.178  lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
  14.179 -  by (tactic {* fast_arith_tac 1 *})
  14.180 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.181  
  14.182  lemma "[| (x::nat) > y; y > z; z > x |] ==> False"
  14.183 -  by (tactic {* fast_arith_tac 1 *})
  14.184 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.185  
  14.186  lemma "(x::nat) - 5 > y ==> y < x"
  14.187 -  by (tactic {* fast_arith_tac 1 *})
  14.188 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.189  
  14.190  lemma "(x::nat) ~= 0 ==> 0 < x"
  14.191 -  by (tactic {* fast_arith_tac 1 *})
  14.192 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.193  
  14.194  lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
  14.195 -  by (tactic {* fast_arith_tac 1 *})
  14.196 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.197  
  14.198  lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
  14.199 -  by (tactic {* simple_arith_tac 1 *})
  14.200 +  by (tactic {* simple_arith_tac @{context} 1 *})
  14.201  
  14.202  lemma "(x - y) - (x::nat) = (x - x) - y"
  14.203 -  by (tactic {* fast_arith_tac 1 *})
  14.204 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.205  
  14.206  lemma "[| (a::nat) < b; c < d |] ==> (a - b) = (c - d)"
  14.207 -  by (tactic {* fast_arith_tac 1 *})
  14.208 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.209  
  14.210  lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
  14.211 -  by (tactic {* fast_arith_tac 1 *})
  14.212 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.213  
  14.214  lemma "(n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
  14.215    (n = n' & n' < m) | (n = m & m < n') |
  14.216 @@ -213,28 +213,28 @@
  14.217  text {* Constants. *}
  14.218  
  14.219  lemma "(0::nat) < 1"
  14.220 -  by (tactic {* fast_arith_tac 1 *})
  14.221 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.222  
  14.223  lemma "(0::int) < 1"
  14.224 -  by (tactic {* fast_arith_tac 1 *})
  14.225 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.226  
  14.227  lemma "(47::nat) + 11 < 08 * 15"
  14.228 -  by (tactic {* fast_arith_tac 1 *})
  14.229 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.230  
  14.231  lemma "(47::int) + 11 < 08 * 15"
  14.232 -  by (tactic {* fast_arith_tac 1 *})
  14.233 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.234  
  14.235  text {* Splitting of inequalities of different type. *}
  14.236  
  14.237  lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
  14.238    a + b <= nat (max (abs i) (abs j))"
  14.239 -  by (tactic {* fast_arith_tac 1 *})
  14.240 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.241  
  14.242  text {* Again, but different order. *}
  14.243  
  14.244  lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
  14.245    a + b <= nat (max (abs i) (abs j))"
  14.246 -  by (tactic {* fast_arith_tac 1 *})
  14.247 +  by (tactic {* fast_arith_tac @{context} 1 *})
  14.248  
  14.249  (*
  14.250  ML {* reset trace_arith; *}
    15.1 --- a/src/HOL/int_arith1.ML	Mon Jul 30 19:46:15 2007 +0200
    15.2 +++ b/src/HOL/int_arith1.ML	Tue Jul 31 00:56:26 2007 +0200
    15.3 @@ -610,6 +610,6 @@
    15.4    "fast_int_arith" 
    15.5       ["(m::'a::{ordered_idom,number_ring}) < n",
    15.6        "(m::'a::{ordered_idom,number_ring}) <= n",
    15.7 -      "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover;
    15.8 +      "(m::'a::{ordered_idom,number_ring}) = n"] (K Fast_Arith.lin_arith_simproc);
    15.9  
   15.10  Addsimprocs [fast_int_arith_simproc];