--- a/src/HOL/Arith_Tools.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Arith_Tools.thy Tue Jul 31 00:56:26 2007 +0200
@@ -17,7 +17,7 @@
subsection {* Simprocs for the Naturals *}
-setup nat_simprocs_setup
+declaration {* K nat_simprocs_setup *}
subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*}
--- a/src/HOL/Complex/ex/BinEx.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Complex/ex/BinEx.thy Tue Jul 31 00:56:26 2007 +0200
@@ -338,38 +338,38 @@
by arith
lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
-by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac @{context} 1")
lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
-by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac @{context} 1")
lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
-by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac @{context} 1")
lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
-by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac @{context} 1")
lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
-by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac @{context} 1")
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"
by arith
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
-by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac @{context} 1")
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
-by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac @{context} 1")
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
-by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac @{context} 1")
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
==> 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"
-by (tactic "fast_arith_tac 1")
+by (tactic "fast_arith_tac @{context} 1")
subsection{*Complex Arithmetic*}
--- a/src/HOL/HoareParallel/OG_Examples.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Tue Jul 31 00:56:26 2007 +0200
@@ -443,7 +443,7 @@
--{* 32 subgoals left *}
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
-apply(tactic {* TRYALL simple_arith_tac *})
+apply(tactic {* TRYALL (simple_arith_tac @{context}) *})
--{* 9 subgoals left *}
apply (force simp add:less_Suc_eq)
apply(drule sym)
--- a/src/HOL/Hyperreal/HyperDef.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Tue Jul 31 00:56:26 2007 +0200
@@ -340,8 +340,7 @@
*)
use "hypreal_arith.ML"
-
-setup hypreal_arith_setup
+declaration {* K hypreal_arith_setup *}
subsection {* Exponentials on the Hyperreals *}
--- a/src/HOL/Hyperreal/hypreal_arith.ML Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Hyperreal/hypreal_arith.ML Tue Jul 31 00:56:26 2007 +0200
@@ -30,7 +30,7 @@
Simplifier.simproc (the_context ())
"fast_hypreal_arith"
["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
- Fast_Arith.lin_arith_prover;
+ (K Fast_Arith.lin_arith_simproc);
val hypreal_arith_setup =
Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
@@ -41,6 +41,6 @@
neqE = neqE,
simpset = simpset addsimps simps}) #>
arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
- (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy));
+ Simplifier.map_ss (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]);
end;
--- a/src/HOL/IntArith.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/IntArith.thy Tue Jul 31 00:56:26 2007 +0200
@@ -115,7 +115,7 @@
min_def[of "number_of u" "1::int", standard, simp]
use "int_arith1.ML"
-setup int_arith_setup
+declaration {* K int_arith_setup *}
subsection{*Lemmas About Small Numerals*}
--- a/src/HOL/Nat.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Nat.thy Tue Jul 31 00:56:26 2007 +0200
@@ -1092,7 +1092,7 @@
using 2 1 by (rule trans)
use "arith_data.ML"
-setup arith_setup
+declaration {* K arith_setup *}
text{*The following proofs may rely on the arithmetic proof procedures.*}
--- a/src/HOL/NatBin.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/NatBin.thy Tue Jul 31 00:56:26 2007 +0200
@@ -666,7 +666,7 @@
neg_number_of_Min,neg_number_of_BIT]})
*}
-setup nat_bin_arith_setup
+declaration {* K nat_bin_arith_setup *}
(* Enable arith to deal with div/mod k where k is a numeral: *)
declare split_div[of _ _ "number_of k", standard, arith_split]
--- a/src/HOL/Presburger.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Presburger.thy Tue Jul 31 00:56:26 2007 +0200
@@ -439,8 +439,8 @@
use "Tools/Qelim/presburger.ML"
-setup {*
- arith_tactic_add
+declaration {* fn _ =>
+ arith_tactic_add
(mk_arith_tactic "presburger" (fn i => fn st =>
(warning "Trying Presburger arithmetic ...";
Presburger.cooper_tac true [] [] ((ProofContext.init o theory_of_thm) st) i st)))
--- a/src/HOL/Real/Rational.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Real/Rational.thy Tue Jul 31 00:56:26 2007 +0200
@@ -469,7 +469,7 @@
by default (simp add: rat_number_of_def)
use "rat_arith.ML"
-setup rat_arith_setup
+declaration {* K rat_arith_setup *}
subsection {* Embedding from Rationals to other Fields *}
--- a/src/HOL/Real/RealDef.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Real/RealDef.thy Tue Jul 31 00:56:26 2007 +0200
@@ -832,8 +832,7 @@
use "real_arith.ML"
-
-setup real_arith_setup
+declaration {* K real_arith_setup *}
subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}
--- a/src/HOL/Tools/Qelim/cooper.ML Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Tue Jul 31 00:56:26 2007 +0200
@@ -173,7 +173,7 @@
(* Canonical linear form for terms, formulae etc.. *)
fun provelin ctxt t = Goal.prove ctxt [] [] t
- (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac 1)]);
+ (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac ctxt 1)]);
fun linear_cmul 0 tm = zero
| linear_cmul n tm =
case tm of
--- a/src/HOL/Tools/TFL/post.ML Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Tools/TFL/post.ML Tue Jul 31 00:56:26 2007 +0200
@@ -68,7 +68,7 @@
Prim.postprocess strict
{wf_tac = REPEAT (ares_tac wfs 1),
terminator = asm_simp_tac ss 1
- THEN TRY (silent_arith_tac 1 ORELSE
+ THEN TRY (silent_arith_tac (Simplifier.the_context ss) 1 ORELSE
fast_tac (cs addSDs [@{thm not0_implies_Suc}] addss ss) 1),
simplifier = Rules.simpl_conv ss []};
--- a/src/HOL/ex/Arith_Examples.thy Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/ex/Arith_Examples.thy Tue Jul 31 00:56:26 2007 +0200
@@ -20,7 +20,7 @@
as well. This is the one that you should use in your proofs!
An @{text arith}-based simproc is available as well
- (see @{ML Fast_Arith.lin_arith_prover}),
+ (see @{ML Fast_Arith.lin_arith_simproc}),
which---for performance reasons---however
does even less splitting than @{ML fast_arith_tac} at the moment (namely
inequalities only). (On the other hand, it does take apart conjunctions,
@@ -36,159 +36,159 @@
@{term Divides.div} *}
lemma "(i::nat) <= max i j"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(i::int) <= max i j"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "min i j <= (i::nat)"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "min i j <= (i::int)"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "min (i::nat) j <= max i j"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "min (i::int) j <= max i j"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "min (i::nat) j + max i j = i + j"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "min (i::int) j + max i j = i + j"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(i::nat) < j ==> min i j < max i j"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(i::int) < j ==> min i j < max i j"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(0::int) <= abs i"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(i::int) <= abs i"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "abs (abs (i::int)) = abs i"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
text {* Also testing subgoals with bound variables. *}
lemma "!!x. (x::nat) <= y ==> x - y = 0"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "!!x. (x::nat) - y = 0 ==> x <= y"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
- by (tactic {* simple_arith_tac 1 *})
+ by (tactic {* simple_arith_tac @{context} 1 *})
lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "[| (x::nat) < y; d < 1 |] ==> x - y - x = d - x"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(x::int) < y ==> x - y < 0"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "nat (i + j) <= nat i + nat j"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "i < j ==> nat (i - j) = 0"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(i::nat) mod 0 = i"
(* FIXME: need to replace 0 by its numeral representation *)
apply (subst nat_numeral_0_eq_0 [symmetric])
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(i::nat) mod 1 = 0"
(* FIXME: need to replace 1 by its numeral representation *)
apply (subst nat_numeral_1_eq_1 [symmetric])
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(i::nat) mod 42 <= 41"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(i::int) mod 0 = i"
(* FIXME: need to replace 0 by its numeral representation *)
apply (subst numeral_0_eq_0 [symmetric])
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(i::int) mod 1 = 0"
(* FIXME: need to replace 1 by its numeral representation *)
apply (subst numeral_1_eq_1 [symmetric])
(* FIXME: arith does not know about iszero *)
- apply (tactic {* LA_Data_Ref.pre_tac 1 *})
+ apply (tactic {* LA_Data_Ref.pre_tac @{context} 1 *})
oops
lemma "(i::int) mod 42 <= 41"
(* FIXME: arith does not know about iszero *)
- apply (tactic {* LA_Data_Ref.pre_tac 1 *})
+ apply (tactic {* LA_Data_Ref.pre_tac @{context} 1 *})
oops
subsection {* Meta-Logic *}
lemma "x < Suc y == x <= y"
- by (tactic {* simple_arith_tac 1 *})
+ by (tactic {* simple_arith_tac @{context} 1 *})
lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
- by (tactic {* simple_arith_tac 1 *})
+ by (tactic {* simple_arith_tac @{context} 1 *})
subsection {* Various Other Examples *}
lemma "(x < Suc y) = (x <= y)"
- by (tactic {* simple_arith_tac 1 *})
+ by (tactic {* simple_arith_tac @{context} 1 *})
lemma "[| (x::nat) < y; y < z |] ==> x < z"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(x::nat) < y & y < z ==> x < z"
- by (tactic {* simple_arith_tac 1 *})
+ by (tactic {* simple_arith_tac @{context} 1 *})
text {* This example involves no arithmetic at all, but is solved by
preprocessing (i.e. NNF normalization) alone. *}
lemma "(P::bool) = Q ==> Q = P"
- by (tactic {* simple_arith_tac 1 *})
+ by (tactic {* simple_arith_tac @{context} 1 *})
lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
- by (tactic {* simple_arith_tac 1 *})
+ by (tactic {* simple_arith_tac @{context} 1 *})
lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
- by (tactic {* simple_arith_tac 1 *})
+ by (tactic {* simple_arith_tac @{context} 1 *})
lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "[| (x::nat) > y; y > z; z > x |] ==> False"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(x::nat) - 5 > y ==> y < x"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(x::nat) ~= 0 ==> 0 < x"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
- by (tactic {* simple_arith_tac 1 *})
+ by (tactic {* simple_arith_tac @{context} 1 *})
lemma "(x - y) - (x::nat) = (x - x) - y"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "[| (a::nat) < b; c < d |] ==> (a - b) = (c - d)"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
(n = n' & n' < m) | (n = m & m < n') |
@@ -213,28 +213,28 @@
text {* Constants. *}
lemma "(0::nat) < 1"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(0::int) < 1"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(47::nat) + 11 < 08 * 15"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
lemma "(47::int) + 11 < 08 * 15"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
text {* Splitting of inequalities of different type. *}
lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
a + b <= nat (max (abs i) (abs j))"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
text {* Again, but different order. *}
lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
a + b <= nat (max (abs i) (abs j))"
- by (tactic {* fast_arith_tac 1 *})
+ by (tactic {* fast_arith_tac @{context} 1 *})
(*
ML {* reset trace_arith; *}
--- a/src/HOL/int_arith1.ML Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/int_arith1.ML Tue Jul 31 00:56:26 2007 +0200
@@ -610,6 +610,6 @@
"fast_int_arith"
["(m::'a::{ordered_idom,number_ring}) < n",
"(m::'a::{ordered_idom,number_ring}) <= n",
- "(m::'a::{ordered_idom,number_ring}) = n"] Fast_Arith.lin_arith_prover;
+ "(m::'a::{ordered_idom,number_ring}) = n"] (K Fast_Arith.lin_arith_simproc);
Addsimprocs [fast_int_arith_simproc];