--- a/src/HOL/Algebra/abstract/Ring.thy Sat Jul 08 12:54:29 2006 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy Sat Jul 08 12:54:30 2006 +0200
@@ -163,8 +163,8 @@
"t - u::'a::ring",
"t * u::'a::ring",
"- t::'a::ring"];
- fun proc sg ss t =
- let val rew = Goal.prove sg [] []
+ fun proc ss t =
+ let val rew = Goal.prove (Simplifier.the_context ss) [] []
(HOLogic.mk_Trueprop
(HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
(fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
@@ -175,7 +175,7 @@
else SOME rew
end;
in
- val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss proc;
+ val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc);
end;
*}
--- a/src/HOL/Divides.thy Sat Jul 08 12:54:29 2006 +0200
+++ b/src/HOL/Divides.thy Sat Jul 08 12:54:30 2006 +0200
@@ -208,7 +208,7 @@
structure CancelDivMod = CancelDivModFun(CancelDivModData);
val cancel_div_mod_proc = NatArithUtils.prep_simproc
- ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
+ ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);
Addsimprocs[cancel_div_mod_proc];
*}
--- a/src/HOL/Fun.thy Sat Jul 08 12:54:29 2006 +0200
+++ b/src/HOL/Fun.thy Sat Jul 08 12:54:30 2006 +0200
@@ -494,10 +494,11 @@
val fun_upd2_simproc =
Simplifier.simproc (Theory.sign_of (the_context ()))
"fun_upd2" ["f(v := w, x := y)"]
- (fn sg => fn ss => fn t =>
+ (fn _ => fn ss => fn t =>
case find_double t of (T, NONE) => NONE
| (T, SOME rhs) =>
- SOME (Goal.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
+ SOME (Goal.prove (Simplifier.the_context ss) [] []
+ (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
end;
Addsimprocs[fun_upd2_simproc];
--- a/src/HOL/Integ/IntDiv_setup.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/HOL/Integ/IntDiv_setup.ML Sat Jul 08 12:54:30 2006 +0200
@@ -32,6 +32,6 @@
structure CancelDivMod = CancelDivModFun(CancelDivModData);
val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc
- ("cancel_zdiv_zmod", ["(m::int) + n"], CancelDivMod.proc);
+ ("cancel_zdiv_zmod", ["(m::int) + n"], K CancelDivMod.proc);
Addsimprocs[cancel_zdiv_zmod_proc];
--- a/src/HOL/Integ/int_factor_simprocs.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML Sat Jul 08 12:54:30 2006 +0200
@@ -123,18 +123,18 @@
[("ring_eq_cancel_numeral_factor",
["(l::'a::{ordered_idom,number_ring}) * m = n",
"(l::'a::{ordered_idom,number_ring}) = m * n"],
- EqCancelNumeralFactor.proc),
+ K EqCancelNumeralFactor.proc),
("ring_less_cancel_numeral_factor",
["(l::'a::{ordered_idom,number_ring}) * m < n",
"(l::'a::{ordered_idom,number_ring}) < m * n"],
- LessCancelNumeralFactor.proc),
+ K LessCancelNumeralFactor.proc),
("ring_le_cancel_numeral_factor",
["(l::'a::{ordered_idom,number_ring}) * m <= n",
"(l::'a::{ordered_idom,number_ring}) <= m * n"],
- LeCancelNumeralFactor.proc),
+ K LeCancelNumeralFactor.proc),
("int_div_cancel_numeral_factors",
["((l::int) * m) div n", "(l::int) div (m * n)"],
- DivCancelNumeralFactor.proc)];
+ K DivCancelNumeralFactor.proc)];
val field_cancel_numeral_factors =
@@ -142,12 +142,12 @@
[("field_eq_cancel_numeral_factor",
["(l::'a::{field,number_ring}) * m = n",
"(l::'a::{field,number_ring}) = m * n"],
- FieldEqCancelNumeralFactor.proc),
+ K FieldEqCancelNumeralFactor.proc),
("field_cancel_numeral_factor",
["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
"(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
"((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
- FieldDivCancelNumeralFactor.proc)]
+ K FieldDivCancelNumeralFactor.proc)]
end;
@@ -280,9 +280,9 @@
val int_cancel_factor =
map Bin_Simprocs.prep_simproc
[("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"],
- EqCancelFactor.proc),
+ K EqCancelFactor.proc),
("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
- DivideCancelFactor.proc)];
+ K DivideCancelFactor.proc)];
(** Versions for all fields, including unordered ones (type complex).*)
@@ -309,11 +309,11 @@
[("field_eq_cancel_factor",
["(l::'a::{field,number_ring}) * m = n",
"(l::'a::{field,number_ring}) = m * n"],
- FieldEqCancelFactor.proc),
+ K FieldEqCancelFactor.proc),
("field_divide_cancel_factor",
["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
"(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
- FieldDivideCancelFactor.proc)];
+ K FieldDivideCancelFactor.proc)];
end;
--- a/src/HOL/Integ/nat_simprocs.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Sat Jul 08 12:54:30 2006 +0200
@@ -223,22 +223,22 @@
["(l::nat) + m = n", "(l::nat) = m + n",
"(l::nat) * m = n", "(l::nat) = m * n",
"Suc m = n", "m = Suc n"],
- EqCancelNumerals.proc),
+ K EqCancelNumerals.proc),
("natless_cancel_numerals",
["(l::nat) + m < n", "(l::nat) < m + n",
"(l::nat) * m < n", "(l::nat) < m * n",
"Suc m < n", "m < Suc n"],
- LessCancelNumerals.proc),
+ K LessCancelNumerals.proc),
("natle_cancel_numerals",
["(l::nat) + m <= n", "(l::nat) <= m + n",
"(l::nat) * m <= n", "(l::nat) <= m * n",
"Suc m <= n", "m <= Suc n"],
- LeCancelNumerals.proc),
+ K LeCancelNumerals.proc),
("natdiff_cancel_numerals",
["((l::nat) + m) - n", "(l::nat) - (m + n)",
"(l::nat) * m - n", "(l::nat) - m * n",
"Suc m - n", "m - Suc n"],
- DiffCancelNumerals.proc)];
+ K DiffCancelNumerals.proc)];
(*** Applying CombineNumeralsFun ***)
@@ -268,7 +268,7 @@
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
val combine_numerals =
- prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], CombineNumerals.proc);
+ prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
(*** Applying CancelNumeralFactorFun ***)
@@ -331,16 +331,16 @@
map prep_simproc
[("nateq_cancel_numeral_factors",
["(l::nat) * m = n", "(l::nat) = m * n"],
- EqCancelNumeralFactor.proc),
+ K EqCancelNumeralFactor.proc),
("natless_cancel_numeral_factors",
["(l::nat) * m < n", "(l::nat) < m * n"],
- LessCancelNumeralFactor.proc),
+ K LessCancelNumeralFactor.proc),
("natle_cancel_numeral_factors",
["(l::nat) * m <= n", "(l::nat) <= m * n"],
- LeCancelNumeralFactor.proc),
+ K LeCancelNumeralFactor.proc),
("natdiv_cancel_numeral_factors",
["((l::nat) * m) div n", "(l::nat) div (m * n)"],
- DivCancelNumeralFactor.proc)];
+ K DivCancelNumeralFactor.proc)];
@@ -413,16 +413,16 @@
map prep_simproc
[("nat_eq_cancel_factor",
["(l::nat) * m = n", "(l::nat) = m * n"],
- EqCancelFactor.proc),
+ K EqCancelFactor.proc),
("nat_less_cancel_factor",
["(l::nat) * m < n", "(l::nat) < m * n"],
- LessCancelFactor.proc),
+ K LessCancelFactor.proc),
("nat_le_cancel_factor",
["(l::nat) * m <= n", "(l::nat) <= m * n"],
- LeCancelFactor.proc),
+ K LeCancelFactor.proc),
("nat_divide_cancel_factor",
["((l::nat) * m) div n", "(l::nat) div (m * n)"],
- DivideCancelFactor.proc)];
+ K DivideCancelFactor.proc)];
end;
--- a/src/HOL/List.thy Sat Jul 08 12:54:29 2006 +0200
+++ b/src/HOL/List.thy Sat Jul 08 12:54:30 2006 +0200
@@ -449,7 +449,7 @@
val rearr_ss = HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons];
-fun list_eq sg ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
+fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
let
val lastl = last lhs and lastr = last rhs;
fun rearr conv =
@@ -460,7 +460,7 @@
val app = Const("List.op @",appT)
val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
- val thm = Goal.prove sg [] [] eq
+ val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
(K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
@@ -473,7 +473,7 @@
in
val list_eq_simproc =
- Simplifier.simproc (Theory.sign_of (the_context ())) "list_eq" ["(xs::'a list) = ys"] list_eq;
+ Simplifier.simproc (Theory.sign_of (the_context ())) "list_eq" ["(xs::'a list) = ys"] (K list_eq);
end;
--- a/src/HOL/Product_Type.thy Sat Jul 08 12:54:29 2006 +0200
+++ b/src/HOL/Product_Type.thy Sat Jul 08 12:54:30 2006 +0200
@@ -407,7 +407,7 @@
fun split_pat tp i (Abs (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE
| split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
| split_pat tp i _ = NONE;
- fun metaeq thy ss lhs rhs = mk_meta_eq (Goal.prove thy [] []
+ fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
(K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1)));
@@ -421,21 +421,21 @@
| subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
else (subst arg k i t $ subst arg k i u)
| subst arg k i t = t;
- fun beta_proc thy ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
+ fun beta_proc ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
(case split_pat beta_term_pat 1 t of
- SOME (i,f) => SOME (metaeq thy ss s (subst arg 0 i f))
+ SOME (i,f) => SOME (metaeq ss s (subst arg 0 i f))
| NONE => NONE)
- | beta_proc _ _ _ = NONE;
- fun eta_proc thy ss (s as Const ("split", _) $ Abs (_, _, t)) =
+ | beta_proc _ _ = NONE;
+ fun eta_proc ss (s as Const ("split", _) $ Abs (_, _, t)) =
(case split_pat eta_term_pat 1 t of
- SOME (_,ft) => SOME (metaeq thy ss s (let val (f $ arg) = ft in f end))
+ SOME (_,ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
| NONE => NONE)
- | eta_proc _ _ _ = NONE;
+ | eta_proc _ _ = NONE;
in
val split_beta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
- "split_beta" ["split f z"] beta_proc;
+ "split_beta" ["split f z"] (K beta_proc);
val split_eta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
- "split_eta" ["split f"] eta_proc;
+ "split_eta" ["split f"] (K eta_proc);
end;
Addsimprocs [split_beta_proc, split_eta_proc];
--- a/src/HOL/arith_data.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/HOL/arith_data.ML Sat Jul 08 12:54:30 2006 +0200
@@ -49,8 +49,9 @@
(* prove conversions *)
-fun prove_conv expand_tac norm_tac sg ss tu = (* FIXME avoid standard *)
- mk_meta_eq (standard (Goal.prove sg [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
+fun prove_conv expand_tac norm_tac ss tu = (* FIXME avoid standard *)
+ mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
+ (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
(K (EVERY [expand_tac, norm_tac ss]))));
val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
@@ -148,15 +149,15 @@
val nat_cancel_sums_add = map prep_simproc
[("nateq_cancel_sums",
- ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], EqCancelSums.proc),
+ ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"], K EqCancelSums.proc),
("natless_cancel_sums",
- ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], LessCancelSums.proc),
+ ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"], K LessCancelSums.proc),
("natle_cancel_sums",
- ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], LeCancelSums.proc)];
+ ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"], K LeCancelSums.proc)];
val nat_cancel_sums = nat_cancel_sums_add @
[prep_simproc ("natdiff_cancel_sums",
- ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], DiffCancelSums.proc)];
+ ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"], K DiffCancelSums.proc)];
end;
--- a/src/Provers/Arith/cancel_div_mod.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/Provers/Arith/cancel_div_mod.ML Sat Jul 08 12:54:30 2006 +0200
@@ -22,13 +22,13 @@
val div_mod_eqs: thm list
(* (n*(m div n) + m mod n) + k == m + k and
((m div n)*n + m mod n) + k == m + k *)
- val prove_eq_sums: theory -> simpset -> term * term -> thm
+ val prove_eq_sums: simpset -> term * term -> thm
(* must prove ac0-equivalence of sums *)
end;
signature CANCEL_DIV_MOD =
sig
- val proc: theory -> simpset -> term -> thm option
+ val proc: simpset -> term -> thm option
end;
@@ -67,15 +67,15 @@
val m = Data.mk_binop Data.mod_name pq
in mk_plus(mk_plus(d,m),Data.mk_sum(ts \ d \ m)) end
-fun cancel thy ss t pq =
- let val teqt' = Data.prove_eq_sums thy ss (t, rearrange t pq)
+fun cancel ss t pq =
+ let val teqt' = Data.prove_eq_sums ss (t, rearrange t pq)
in hd(Data.div_mod_eqs RL [teqt' RS transitive_thm]) end;
-fun proc thy ss t =
+fun proc ss t =
let val (divs,mods) = coll_div_mod t ([],[])
in if null divs orelse null mods then NONE
else case divs inter mods of
- pq :: _ => SOME(cancel thy ss t pq)
+ pq :: _ => SOME (cancel ss t pq)
| [] => NONE
end
--- a/src/Provers/Arith/cancel_factor.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/Provers/Arith/cancel_factor.ML Sat Jul 08 12:54:30 2006 +0200
@@ -13,14 +13,14 @@
val mk_bal: term * term -> term
val dest_bal: term -> term * term
(*rules*)
- val prove_conv: tactic -> tactic -> theory -> term * term -> thm
+ val prove_conv: tactic -> tactic -> Proof.context -> term * term -> thm
val norm_tac: tactic (*AC0 etc.*)
val multiply_tac: IntInf.int -> tactic (*apply a ~~ b == k * a ~~ k * b (for k > 0)*)
end;
signature CANCEL_FACTOR =
sig
- val proc: theory -> thm list -> term -> thm option
+ val proc: simpset -> term -> thm option
end;
@@ -54,7 +54,7 @@
(* the simplification procedure *)
-fun proc sg _ t =
+fun proc ss t =
(case try Data.dest_bal t of
NONE => NONE
| SOME bal =>
@@ -68,7 +68,7 @@
in
if d = 0 orelse d = 1 then NONE
else SOME
- (Data.prove_conv (Data.multiply_tac d) Data.norm_tac sg
+ (Data.prove_conv (Data.multiply_tac d) Data.norm_tac (Simplifier.the_context ss)
(t, Data.mk_bal (div_sum d tks, div_sum d uks)))
end));
--- a/src/Provers/Arith/cancel_numeral_factor.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Sat Jul 08 12:54:30 2006 +0200
@@ -29,7 +29,7 @@
val neg_exchanges: bool (*true if a negative coeff swaps the two operands,
as with < and <= but not = and div*)
(*proof tools*)
- val prove_conv: tactic list -> theory ->
+ val prove_conv: tactic list -> Proof.context ->
thm list -> string list -> term * term -> thm option
val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: simpset -> tactic (*proves the initial lemma*)
@@ -40,14 +40,15 @@
functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
sig
- val proc: theory -> simpset -> term -> thm option
+ val proc: simpset -> term -> thm option
end
=
struct
(*the simplification procedure*)
-fun proc thy ss t =
+fun proc ss t =
let
+ val ctxt = Simplifier.the_context ss;
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;
@@ -67,13 +68,13 @@
else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2'))
val reshape = (*Move d to the front and put the rest into standard form
i * #m * j == #d * (#n * (j * k)) *)
- Data.prove_conv [Data.norm_tac ss] thy hyps xs
+ Data.prove_conv [Data.norm_tac ss] ctxt hyps xs
(t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
in
Option.map (Data.simplify_meta_eq ss)
(Data.prove_conv
[Data.trans_tac ss reshape, rtac Data.cancel 1,
- Data.numeral_simp_tac ss] thy hyps xs (t', rhs))
+ Data.numeral_simp_tac ss] ctxt hyps xs (t', rhs))
end
handle TERM _ => NONE
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral)
--- a/src/Provers/Arith/cancel_numerals.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Sat Jul 08 12:54:30 2006 +0200
@@ -36,7 +36,7 @@
val bal_add1: thm
val bal_add2: thm
(*proof tools*)
- val prove_conv: tactic list -> theory ->
+ val prove_conv: tactic list -> Proof.context ->
thm list -> string list -> term * term -> thm option
val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: simpset -> tactic (*proves the initial lemma*)
@@ -47,7 +47,7 @@
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
sig
- val proc: theory -> simpset -> term -> thm option
+ val proc: simpset -> term -> thm option
end
=
struct
@@ -67,8 +67,9 @@
in seek terms1 end;
(*the simplification procedure*)
-fun proc thy ss t =
+fun proc ss t =
let
+ val ctxt = Simplifier.the_context ss;
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;
@@ -84,7 +85,7 @@
i + #m + j + k == #m + i + (j + k) *)
if n1=0 orelse n2=0 then (*trivial, so do nothing*)
raise TERM("cancel_numerals", [])
- else Data.prove_conv [Data.norm_tac ss] thy hyps xs
+ else Data.prove_conv [Data.norm_tac ss] ctxt hyps xs
(t',
Data.mk_bal (newshape(n1,terms1'),
newshape(n2,terms2')))
@@ -93,13 +94,13 @@
(if n2<=n1 then
Data.prove_conv
[Data.trans_tac ss reshape, rtac Data.bal_add1 1,
- Data.numeral_simp_tac ss] thy hyps xs
+ Data.numeral_simp_tac ss] ctxt hyps xs
(t', Data.mk_bal (newshape(n1-n2,terms1'),
Data.mk_sum T terms2'))
else
Data.prove_conv
[Data.trans_tac ss reshape, rtac Data.bal_add2 1,
- Data.numeral_simp_tac ss] thy hyps xs
+ Data.numeral_simp_tac ss] ctxt hyps xs
(t', Data.mk_bal (Data.mk_sum T terms1',
newshape(n2-n1,terms2'))))
end
--- a/src/Provers/Arith/cancel_sums.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/Provers/Arith/cancel_sums.ML Sat Jul 08 12:54:30 2006 +0200
@@ -17,14 +17,14 @@
val mk_bal: term * term -> term
val dest_bal: term -> term * term
(*rules*)
- val prove_conv: tactic -> (simpset -> tactic) -> theory -> simpset -> term * term -> thm
+ val prove_conv: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
val norm_tac: simpset -> tactic (*AC0 etc.*)
val uncancel_tac: cterm -> tactic (*apply A ~~ B == x + A ~~ x + B*)
end;
signature CANCEL_SUMS =
sig
- val proc: theory -> simpset -> term -> thm option
+ val proc: simpset -> term -> thm option
end;
@@ -58,19 +58,19 @@
(* the simplification procedure *)
-fun proc thy ss t =
+fun proc ss t =
(case try Data.dest_bal t of
NONE => NONE
| SOME bal =>
let
+ val thy = ProofContext.theory_of (Simplifier.the_context ss);
val (ts, us) = pairself (sort Term.term_ord o Data.dest_sum) bal;
val (ts', us', vs) = cancel ts us [];
in
if null vs then NONE
else SOME
- (Data.prove_conv (uncancel_sums_tac thy vs) Data.norm_tac thy ss
+ (Data.prove_conv (uncancel_sums_tac thy vs) Data.norm_tac ss
(t, Data.mk_bal (Data.mk_sum ts', Data.mk_sum us')))
end);
-
end;
--- a/src/Provers/Arith/combine_numerals.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/Provers/Arith/combine_numerals.ML Sat Jul 08 12:54:30 2006 +0200
@@ -27,7 +27,7 @@
(*rules*)
val left_distrib: thm
(*proof tools*)
- val prove_conv: tactic list -> theory -> string list -> term * term -> thm option
+ val prove_conv: tactic list -> Proof.context -> string list -> term * term -> thm option
val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*)
val norm_tac: simpset -> tactic (*proves the initial lemma*)
val numeral_simp_tac: simpset -> tactic (*proves the final theorem*)
@@ -37,7 +37,7 @@
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
sig
- val proc: theory -> simpset -> term -> thm option
+ val proc: simpset -> term -> thm option
end
=
struct
@@ -64,8 +64,10 @@
| NONE => find_repeated (tab, t::past, terms);
(*the simplification procedure*)
-fun proc thy ss t =
- let (*first freeze any Vars in the term to prevent flex-flex problems*)
+fun proc ss t =
+ let
+ val ctxt = Simplifier.the_context ss;
+ (*first freeze any Vars in the term to prevent flex-flex problems*)
val (t', xs) = Term.adhoc_freeze_vars t
val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t')
val T = Term.fastype_of u
@@ -73,7 +75,7 @@
i + #m + j + k == #m + i + (j + k) *)
if m=0 orelse n=0 then (*trivial, so do nothing*)
raise TERM("combine_numerals", [])
- else Data.prove_conv [Data.norm_tac ss] thy xs
+ else Data.prove_conv [Data.norm_tac ss] ctxt xs
(t',
Data.mk_sum T ([Data.mk_coeff(m,u),
Data.mk_coeff(n,u)] @ terms))
@@ -81,7 +83,7 @@
Option.map (Data.simplify_meta_eq ss)
(Data.prove_conv
[Data.trans_tac ss reshape, rtac Data.left_distrib 1,
- Data.numeral_simp_tac ss] thy xs
+ Data.numeral_simp_tac ss] ctxt xs
(t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms)))
end
handle TERM _ => NONE
--- a/src/Provers/Arith/extract_common_term.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/Provers/Arith/extract_common_term.ML Sat Jul 08 12:54:30 2006 +0200
@@ -23,7 +23,7 @@
val dest_bal: term -> term * term
val find_first: term -> term list -> term list
(*proof tools*)
- val prove_conv: tactic list -> theory ->
+ val prove_conv: tactic list -> Proof.context ->
thm list -> string list -> term * term -> thm option
val norm_tac: simpset -> tactic (*proves the result*)
val simplify_meta_eq: simpset -> thm -> thm (*simplifies the result*)
@@ -32,7 +32,7 @@
functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
sig
- val proc: theory -> simpset -> term -> thm option
+ val proc: simpset -> term -> thm option
end
=
struct
@@ -47,8 +47,9 @@
in seek terms1 end;
(*the simplification procedure*)
-fun proc thy ss t =
+fun proc ss t =
let
+ val ctxt = Simplifier.the_context ss;
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;
@@ -60,7 +61,7 @@
and terms2' = Data.find_first u terms2
and T = Term.fastype_of u
val reshape =
- Data.prove_conv [Data.norm_tac ss] thy hyps xs
+ Data.prove_conv [Data.norm_tac ss] ctxt hyps xs
(t',
Data.mk_bal (Data.mk_sum T (u::terms1'),
Data.mk_sum T (u::terms2')))
--- a/src/ZF/Integ/int_arith.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/ZF/Integ/int_arith.ML Sat Jul 08 12:54:30 2006 +0200
@@ -275,17 +275,17 @@
["l $+ m = n", "l = m $+ n",
"l $- m = n", "l = m $- n",
"l $* m = n", "l = m $* n"],
- EqCancelNumerals.proc),
+ K EqCancelNumerals.proc),
("intless_cancel_numerals",
["l $+ m $< n", "l $< m $+ n",
"l $- m $< n", "l $< m $- n",
"l $* m $< n", "l $< m $* n"],
- LessCancelNumerals.proc),
+ K LessCancelNumerals.proc),
("intle_cancel_numerals",
["l $+ m $<= n", "l $<= m $+ n",
"l $- m $<= n", "l $<= m $- n",
"l $* m $<= n", "l $<= m $* n"],
- LeCancelNumerals.proc)];
+ K LeCancelNumerals.proc)];
(*version without the hyps argument*)
@@ -319,7 +319,7 @@
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
val combine_numerals =
- prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], CombineNumerals.proc);
+ prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
@@ -358,7 +358,7 @@
structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
val combine_numerals_prod =
- prep_simproc ("int_combine_numerals_prod", ["i $* j"], CombineNumeralsProd.proc);
+ prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
end;
--- a/src/ZF/arith_data.ML Sat Jul 08 12:54:29 2006 +0200
+++ b/src/ZF/arith_data.ML Sat Jul 08 12:54:30 2006 +0200
@@ -12,7 +12,7 @@
val nat_cancel: simproc list
(*tools for use in similar applications*)
val gen_trans_tac: thm -> thm option -> tactic
- val prove_conv: string -> tactic list -> theory ->
+ val prove_conv: string -> tactic list -> Proof.context ->
thm list -> string list -> term * term -> thm option
val simplify_meta_eq: thm list -> simpset -> thm -> thm
(*debugging*)
@@ -68,13 +68,13 @@
fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
-fun prove_conv name tacs sg hyps xs (t,u) =
+fun prove_conv name tacs ctxt hyps xs (t,u) =
if t aconv u then NONE
else
let val hyps' = List.filter (not o is_eq_thm) hyps
val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
- in SOME (hyps' MRS Goal.prove sg xs [] goal (K (EVERY tacs)))
+ in SOME (hyps' MRS Goal.prove ctxt xs [] goal (K (EVERY tacs)))
handle ERROR msg =>
(warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
end;
@@ -205,17 +205,17 @@
["l #+ m = n", "l = m #+ n",
"l #* m = n", "l = m #* n",
"succ(m) = n", "m = succ(n)"],
- EqCancelNumerals.proc),
+ (K EqCancelNumerals.proc)),
("natless_cancel_numerals",
["l #+ m < n", "l < m #+ n",
"l #* m < n", "l < m #* n",
"succ(m) < n", "m < succ(n)"],
- LessCancelNumerals.proc),
+ (K LessCancelNumerals.proc)),
("natdiff_cancel_numerals",
["(l #+ m) #- n", "l #- (m #+ n)",
"(l #* m) #- n", "l #- (m #* n)",
"succ(m) #- n", "m #- succ(n)"],
- DiffCancelNumerals.proc)];
+ (K DiffCancelNumerals.proc))];
end;