# HG changeset patch # User wenzelm # Date 1152356070 -7200 # Node ID 92cc2f4c733519e6b90fdad44ced57ea0da3a631 # Parent 03612801317824925cf436eddcfc93469e1fe05d simprocs: no theory argument -- use simpset context instead; diff -r 036128013178 -r 92cc2f4c7335 src/HOL/Algebra/abstract/Ring.thy --- 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; *} diff -r 036128013178 -r 92cc2f4c7335 src/HOL/Divides.thy --- 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]; *} diff -r 036128013178 -r 92cc2f4c7335 src/HOL/Fun.thy --- 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]; diff -r 036128013178 -r 92cc2f4c7335 src/HOL/Integ/IntDiv_setup.ML --- 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]; diff -r 036128013178 -r 92cc2f4c7335 src/HOL/Integ/int_factor_simprocs.ML --- 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; diff -r 036128013178 -r 92cc2f4c7335 src/HOL/Integ/nat_simprocs.ML --- 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; diff -r 036128013178 -r 92cc2f4c7335 src/HOL/List.thy --- 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; diff -r 036128013178 -r 92cc2f4c7335 src/HOL/Product_Type.thy --- 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]; diff -r 036128013178 -r 92cc2f4c7335 src/HOL/arith_data.ML --- 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; diff -r 036128013178 -r 92cc2f4c7335 src/Provers/Arith/cancel_div_mod.ML --- 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 diff -r 036128013178 -r 92cc2f4c7335 src/Provers/Arith/cancel_factor.ML --- 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)); diff -r 036128013178 -r 92cc2f4c7335 src/Provers/Arith/cancel_numeral_factor.ML --- 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) diff -r 036128013178 -r 92cc2f4c7335 src/Provers/Arith/cancel_numerals.ML --- 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 diff -r 036128013178 -r 92cc2f4c7335 src/Provers/Arith/cancel_sums.ML --- 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; diff -r 036128013178 -r 92cc2f4c7335 src/Provers/Arith/combine_numerals.ML --- 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 diff -r 036128013178 -r 92cc2f4c7335 src/Provers/Arith/extract_common_term.ML --- 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'))) diff -r 036128013178 -r 92cc2f4c7335 src/ZF/Integ/int_arith.ML --- 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; diff -r 036128013178 -r 92cc2f4c7335 src/ZF/arith_data.ML --- 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;