--- a/doc-src/Ref/simplifier.tex Thu Jul 08 19:34:18 2004 +0200
+++ b/doc-src/Ref/simplifier.tex Thu Jul 08 19:34:56 2004 +0200
@@ -1143,9 +1143,9 @@
\section{*Coding simplification procedures}
\begin{ttbox}
val Simplifier.simproc: Sign.sg -> string -> string list
- -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+ -> (Sign.sg -> simpset -> term -> thm option) -> simproc
val Simplifier.simproc_i: Sign.sg -> string -> term list
- -> (Sign.sg -> thm list -> term -> thm option) -> simproc
+ -> (Sign.sg -> simpset -> term -> thm option) -> simproc
\end{ttbox}
\begin{ttdescription}
--- a/src/Provers/Arith/abel_cancel.ML Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/abel_cancel.ML Thu Jul 08 19:34:56 2004 +0200
@@ -125,7 +125,7 @@
val sum_conv =
Simplifier.mk_simproc "cancel_sums"
- (map (Thm.read_cterm (Sign.deref sg_ref))
+ (map (Thm.cterm_fun Logic.varify o Thm.read_cterm (Sign.deref sg_ref))
[("x + y", Data.T), ("x - y", Data.T)]) (* FIXME depends on concrete syntax !???!!??! *)
sum_proc;
--- a/src/Provers/Arith/cancel_div_mod.ML Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML Thu Jul 08 19:34:56 2004 +0200
@@ -28,7 +28,7 @@
signature CANCEL_DIV_MOD =
sig
- val proc: Sign.sg -> thm list -> term -> thm option
+ val proc: Sign.sg -> simpset -> term -> thm option
end;
--- a/src/Provers/Arith/cancel_numeral_factor.ML Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Thu Jul 08 19:34:56 2004 +0200
@@ -40,7 +40,7 @@
functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
sig
- val proc: Sign.sg -> thm list -> term -> thm option
+ val proc: Sign.sg -> simpset -> term -> thm option
end
=
struct
@@ -51,8 +51,10 @@
| gcd (m, n) = gcd (n mod m, m);
(*the simplification procedure*)
-fun proc sg hyps t =
- let (*first freeze any Vars in the term to prevent flex-flex problems*)
+fun proc sg ss t =
+ let
+ val hyps = prems_of_ss ss;
+ (*first freeze any Vars in the term to prevent flex-flex problems*)
val (t', xs) = Term.adhoc_freeze_vars t;
val (t1,t2) = Data.dest_bal t'
val (m1, t1') = Data.dest_coeff t1
--- a/src/Provers/Arith/cancel_numerals.ML Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Thu Jul 08 19:34:56 2004 +0200
@@ -47,7 +47,7 @@
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
sig
- val proc: Sign.sg -> thm list -> term -> thm option
+ val proc: Sign.sg -> simpset -> term -> thm option
end
=
struct
@@ -69,8 +69,10 @@
in seek terms1 end;
(*the simplification procedure*)
-fun proc sg hyps t =
- let (*first freeze any Vars in the term to prevent flex-flex problems*)
+fun proc sg ss t =
+ let
+ val hyps = prems_of_ss ss;
+ (*first freeze any Vars in the term to prevent flex-flex problems*)
val (t', xs) = Term.adhoc_freeze_vars t;
val (t1,t2) = Data.dest_bal t'
val terms1 = Data.dest_sum t1
--- a/src/Provers/Arith/cancel_sums.ML Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/cancel_sums.ML Thu Jul 08 19:34:56 2004 +0200
@@ -24,7 +24,7 @@
signature CANCEL_SUMS =
sig
- val proc: Sign.sg -> thm list -> term -> thm option
+ val proc: Sign.sg -> simpset -> term -> thm option
end;
--- a/src/Provers/Arith/combine_numerals.ML Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/combine_numerals.ML Thu Jul 08 19:34:56 2004 +0200
@@ -37,7 +37,7 @@
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
sig
- val proc: Sign.sg -> thm list -> term -> thm option
+ val proc: Sign.sg -> simpset -> term -> thm option
end
=
struct
--- a/src/Provers/Arith/extract_common_term.ML Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/extract_common_term.ML Thu Jul 08 19:34:56 2004 +0200
@@ -32,7 +32,7 @@
functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
sig
- val proc: Sign.sg -> thm list -> term -> thm option
+ val proc: Sign.sg -> simpset -> term -> thm option
end
=
struct
@@ -50,8 +50,10 @@
in seek terms1 end;
(*the simplification procedure*)
-fun proc sg hyps t =
- let (*first freeze any Vars in the term to prevent flex-flex problems*)
+fun proc sg ss t =
+ let
+ val hyps = prems_of_ss ss;
+ (*first freeze any Vars in the term to prevent flex-flex problems*)
val (t', xs) = Term.adhoc_freeze_vars t;
val (t1,t2) = Data.dest_bal t'
val terms1 = Data.dest_sum t1
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Jul 08 19:34:56 2004 +0200
@@ -11,7 +11,7 @@
and a simplification procedure
- lin_arith_prover: Sign.sg -> thm list -> term -> thm option
+ lin_arith_prover: Sign.sg -> simpset -> term -> thm option
Only take premises and conclusions into account that are already (negated)
(in)equations. lin_arith_prover tries to prove or disprove the term.
@@ -78,7 +78,7 @@
-> theory -> theory
val trace : bool ref
val fast_arith_neq_limit: int ref
- val lin_arith_prover: Sign.sg -> thm list -> term -> thm option
+ val lin_arith_prover: Sign.sg -> simpset -> term -> thm option
val lin_arith_tac: bool -> int -> tactic
val cut_lin_arith_tac: thm list -> int -> tactic
end;
@@ -714,8 +714,10 @@
2. lin_arith_prover is applied by the simplifier which
dives into terms and will thus try the non-negated concl anyway.
*)
-fun lin_arith_prover sg thms concl =
-let val Hs = map (#prop o rep_thm) thms
+fun lin_arith_prover sg ss concl =
+let
+ val thms = prems_of_ss ss;
+ val Hs = map (#prop o rep_thm) thms
val Tconcl = LA_Logic.mk_Trueprop concl
in case prove sg ([],[]) false Hs Tconcl of (* concl provable? *)
Some js => prover sg thms Tconcl js true
--- a/src/Provers/quantifier1.ML Thu Jul 08 19:34:18 2004 +0200
+++ b/src/Provers/quantifier1.ML Thu Jul 08 19:34:56 2004 +0200
@@ -57,10 +57,10 @@
sig
val prove_one_point_all_tac: tactic
val prove_one_point_ex_tac: tactic
- val rearrange_all: Sign.sg -> thm list -> term -> thm option
- val rearrange_ex: Sign.sg -> thm list -> term -> thm option
- val rearrange_ball: tactic -> Sign.sg -> thm list -> term -> thm option
- val rearrange_bex: tactic -> Sign.sg -> thm list -> term -> thm option
+ val rearrange_all: Sign.sg -> simpset -> term -> thm option
+ val rearrange_ex: Sign.sg -> simpset -> term -> thm option
+ val rearrange_ball: tactic -> Sign.sg -> simpset -> term -> thm option
+ val rearrange_bex: tactic -> Sign.sg -> simpset -> term -> thm option
end;
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =