--- a/src/HOL/Algebra/abstract/Ring.thy Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy Mon Aug 01 19:20:26 2005 +0200
@@ -163,11 +163,11 @@
"t - u::'a::ring",
"t * u::'a::ring",
"- t::'a::ring"];
- fun proc sg _ t =
+ fun proc sg ss t =
let val rew = Tactic.prove sg [] []
(HOLogic.mk_Trueprop
(HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
- (fn _ => simp_tac ring_ss 1)
+ (fn _ => simp_tac (Simplifier.inherit_bounds ss ring_ss) 1)
|> mk_meta_eq;
val (t', u) = Logic.dest_equals (Thm.prop_of rew);
in if t' aconv u
@@ -175,7 +175,7 @@
else SOME rew
end;
in
- val ring_simproc = Simplifier.simproc (sign_of (the_context ())) "ring" lhss proc;
+ val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss proc;
end;
*}
--- a/src/HOL/Fun.thy Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Fun.thy Mon Aug 01 19:20:26 2005 +0200
@@ -486,15 +486,18 @@
| find t = NONE
in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
- val ss = simpset ()
- val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1)
+ val current_ss = simpset ()
+ fun fun_upd_prover ss =
+ rtac eq_reflection 1 THEN rtac ext 1 THEN
+ simp_tac (Simplifier.inherit_bounds ss current_ss) 1
in
val fun_upd2_simproc =
Simplifier.simproc (Theory.sign_of (the_context ()))
"fun_upd2" ["f(v := w, x := y)"]
- (fn sg => fn _ => fn t =>
+ (fn sg => fn ss => fn t =>
case find_double t of (T, NONE) => NONE
- | (T, SOME rhs) => SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover))
+ | (T, SOME rhs) =>
+ SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
end;
Addsimprocs[fun_upd2_simproc];
--- a/src/HOL/Integ/int_arith1.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Integ/int_arith1.ML Mon Aug 01 19:20:26 2005 +0200
@@ -150,7 +150,7 @@
ordering is not well-founded.*)
fun num_ord (i,j) =
(case IntInf.compare (IntInf.abs i, IntInf.abs j) of
- EQUAL => Int.compare (IntInf.sign i, IntInf.sign j)
+ EQUAL => int_ord (IntInf.sign i, IntInf.sign j)
| ord => ord);
(*This resembles Term.term_ord, but it puts binary numerals before other
@@ -165,7 +165,7 @@
| numterm_ord (Const("Numeral.number_of", _) $ _, _) = LESS
| numterm_ord (_, Const("Numeral.number_of", _) $ _) = GREATER
| numterm_ord (t, u) =
- (case Int.compare (size_of_term t, size_of_term u) of
+ (case int_ord (size_of_term t, size_of_term u) of
EQUAL =>
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
(case hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord)
@@ -308,8 +308,8 @@
fun trans_tac NONE = all_tac
| trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
-fun simplify_meta_eq rules =
- simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
+fun simplify_meta_eq rules ss =
+ simplify (Simplifier.inherit_bounds ss HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
o mk_meta_eq;
structure CancelNumeralsCommon =
@@ -319,15 +319,17 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val find_first_coeff = find_first_coeff []
- val trans_tac = trans_tac
- val norm_tac =
- ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
- diff_simps@minus_simps@add_ac))
- THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
- THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
- add_ac@mult_ac))
- val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
- val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s)
+ val trans_tac = fn _ => trans_tac
+ fun norm_tac ss =
+ let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+ ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
+ diff_simps @ minus_simps @ add_ac))
+ THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
+ THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
+ end
+ fun numeral_simp_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
+ val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
end;
@@ -395,16 +397,17 @@
val dest_coeff = dest_coeff 1
val left_distrib = combine_common_factor RS trans
val prove_conv = Bin_Simprocs.prove_conv_nohyps
- val trans_tac = trans_tac
- val norm_tac =
- ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
- diff_simps@minus_simps@add_ac))
- THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
- THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
- add_ac@mult_ac))
- val numeral_simp_tac = ALLGOALS
- (simp_tac (HOL_ss addsimps add_0s@bin_simps))
- val simplify_meta_eq = simplify_meta_eq (add_0s@mult_1s)
+ val trans_tac = fn _ => trans_tac
+ fun norm_tac ss =
+ let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+ ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
+ diff_simps @ minus_simps @ add_ac))
+ THEN ALLGOALS (simp_tac (num_ss' addsimps non_add_bin_simps @ mult_minus_simps))
+ THEN ALLGOALS (simp_tac (num_ss' addsimps minus_from_mult_simps @ add_ac @ mult_ac))
+ end
+ fun numeral_simp_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
+ val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
end;
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
--- a/src/HOL/Integ/int_factor_simprocs.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML Mon Aug 01 19:20:26 2005 +0200
@@ -42,14 +42,16 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
- val trans_tac = trans_tac
- val norm_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
- val numeral_simp_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
- val simplify_meta_eq =
+ val trans_tac = fn _ => trans_tac
+ fun norm_tac ss =
+ let val HOL_ss' = Simplifier.inherit_bounds ss HOL_ss in
+ ALLGOALS (simp_tac (HOL_ss' addsimps minus_from_mult_simps @ mult_1s))
+ THEN ALLGOALS (simp_tac (HOL_ss' addsimps bin_simps@mult_minus_simps))
+ THEN ALLGOALS (simp_tac (HOL_ss' addsimps mult_ac))
+ end
+ fun numeral_simp_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps rel_number_of @ bin_simps))
+ val simplify_meta_eq =
Int_Numeral_Simprocs.simplify_meta_eq
[add_0, add_0_right,
mult_zero_left, mult_zero_right, mult_1, mult_1_right];
@@ -235,8 +237,8 @@
Int_Numeral_Simprocs.simplify_meta_eq
[mult_1_left, mult_1_right, zdiv_1, numeral_1_eq_1];
-fun cancel_simplify_meta_eq cancel_th th =
- simplify_one (([th, cancel_th]) MRS trans);
+fun cancel_simplify_meta_eq cancel_th ss th =
+ simplify_one ss (([th, cancel_th]) MRS trans);
(*At present, long_mk_prod creates Numeral1, so this requires the axclass
number_ring*)
@@ -247,8 +249,9 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first []
- val trans_tac = trans_tac
- val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
+ val trans_tac = fn _ => trans_tac
+ fun norm_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
end;
(*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in
--- a/src/HOL/Integ/nat_simprocs.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Mon Aug 01 19:20:26 2005 +0200
@@ -168,14 +168,15 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first_coeff = find_first_coeff []
- val trans_tac = trans_tac
- val norm_tac = ALLGOALS
- (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
+ val trans_tac = fn _ => trans_tac
+ fun norm_tac ss =
+ let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+ ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
[Suc_eq_add_numeral_1_left] @ add_ac))
- THEN ALLGOALS (simp_tac
- (num_ss addsimps bin_simps@add_ac@mult_ac))
- val numeral_simp_tac = ALLGOALS
- (simp_tac (HOL_ss addsimps add_0s@bin_simps))
+ THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
+ end
+ fun numeral_simp_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
val simplify_meta_eq = simplify_meta_eq
end;
@@ -252,14 +253,15 @@
val dest_coeff = dest_coeff
val left_distrib = left_add_mult_distrib RS trans
val prove_conv = Bin_Simprocs.prove_conv_nohyps
- val trans_tac = trans_tac
- val norm_tac = ALLGOALS
- (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
+ val trans_tac = fn _ => trans_tac
+ fun norm_tac ss =
+ let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+ ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
[Suc_eq_add_numeral_1] @ add_ac))
- THEN ALLGOALS (simp_tac
- (num_ss addsimps bin_simps@add_ac@mult_ac))
- val numeral_simp_tac = ALLGOALS
- (simp_tac (HOL_ss addsimps add_0s@bin_simps))
+ THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
+ end
+ fun numeral_simp_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
val simplify_meta_eq = simplify_meta_eq
end;
@@ -275,13 +277,15 @@
struct
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
- val trans_tac = trans_tac
- val norm_tac = ALLGOALS
- (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
+ val trans_tac = fn _ => trans_tac
+ fun norm_tac ss =
+ let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+ ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
[Suc_eq_add_numeral_1_left] @ add_ac))
- THEN ALLGOALS (simp_tac
- (num_ss addsimps bin_simps@add_ac@mult_ac))
- val numeral_simp_tac = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
+ THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
+ end
+ fun numeral_simp_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps bin_simps))
val simplify_meta_eq = simplify_meta_eq
end
@@ -356,8 +360,8 @@
Int_Numeral_Simprocs.simplify_meta_eq
[mult_1_left, mult_1_right, div_1, numeral_1_eq_Suc_0];
-fun cancel_simplify_meta_eq cancel_th th =
- simplify_one (([th, cancel_th]) MRS trans);
+fun cancel_simplify_meta_eq cancel_th ss th =
+ simplify_one ss (([th, cancel_th]) MRS trans);
structure CancelFactorCommon =
struct
@@ -366,8 +370,9 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first = find_first []
- val trans_tac = trans_tac
- val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
+ val trans_tac = fn _ => trans_tac
+ fun norm_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
end;
structure EqCancelFactor = ExtractCommonTermFun
--- a/src/HOL/List.thy Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/List.thy Mon Aug 01 19:20:26 2005 +0200
@@ -415,10 +415,9 @@
| butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
| butlast xs = Const("List.list.Nil",fastype_of xs);
-val rearr_tac =
- simp_tac (HOL_basic_ss addsimps [append_assoc, append_Nil, append_Cons]);
-
-fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
+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) =
let
val lastl = last lhs and lastr = last rhs;
fun rearr conv =
@@ -429,7 +428,8 @@
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 = Tactic.prove sg [] [] eq (K (rearr_tac 1));
+ val thm = Tactic.prove sg [] [] eq
+ (K (simp_tac (Simplifier.inherit_bounds ss rearr_ss) 1));
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
in
--- a/src/HOL/Real/RealDef.thy Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Real/RealDef.thy Mon Aug 01 19:20:26 2005 +0200
@@ -425,9 +425,9 @@
linorder_not_le [where 'a = preal]
real_zero_def real_le real_mult)
--{*Reduce to the (simpler) @{text "\<le>"} relation *}
-apply (auto dest!: less_add_left_Ex
+apply (auto dest!: less_add_left_Ex
simp add: preal_add_ac preal_mult_ac
- preal_add_mult_distrib2 preal_cancels preal_self_less_add_right)
+ preal_add_mult_distrib2 preal_cancels preal_self_less_add_left)
done
lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y"
@@ -478,7 +478,6 @@
apply (auto simp add: real_minus preal_add_ac)
apply (cut_tac x = x and y = y in linorder_less_linear)
apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc [symmetric])
-apply (auto simp add: preal_add_commute)
done
lemma real_of_preal_leD:
--- a/src/HOL/Tools/datatype_package.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Mon Aug 01 19:20:26 2005 +0200
@@ -326,7 +326,7 @@
exception ConstrDistinct of term;
-fun distinct_proc sg _ (t as Const ("op =", _) $ t1 $ t2) =
+fun distinct_proc sg ss (t as Const ("op =", _) $ t1 $ t2) =
(case (stripC (0, t1), stripC (0, t2)) of
((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
(case (stripT (0, T1), stripT (0, T2)) of
@@ -347,9 +347,9 @@
| FewConstrs thms => SOME (Tactic.prove sg [] [] eq_t (K
(EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
atac 2, resolve_tac thms 1, etac FalseE 1])))
- | ManyConstrs (thm, ss) => SOME (Tactic.prove sg [] [] eq_t (K
+ | ManyConstrs (thm, simpset) => SOME (Tactic.prove sg [] [] eq_t (K
(EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
- full_simp_tac ss 1,
+ full_simp_tac (Simplifier.inherit_bounds ss simpset) 1,
REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
etac FalseE 1]))))
--- a/src/HOL/Tools/record_package.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/HOL/Tools/record_package.ML Mon Aug 01 19:20:26 2005 +0200
@@ -833,7 +833,7 @@
else opt ();
-fun prove_split_simp sg T prop =
+fun prove_split_simp sg ss T prop =
let
val {sel_upd={simpset,...},extsplit,...} = RecordsData.get sg;
val extsplits =
@@ -844,7 +844,9 @@
all_thm::(case extsplits of [thm] => [] | _ => extsplits)
(* [thm] is the same as all_thm *)
| NONE => extsplits)
- in (quick_and_dirty_prove true sg [] prop (fn _ => (simp_tac (simpset addsimps thms) 1)))
+ in
+ quick_and_dirty_prove true sg [] prop
+ (fn _ => simp_tac (Simplifier.inherit_bounds ss simpset addsimps thms) 1)
end;
@@ -868,7 +870,7 @@
*)
val record_simproc =
Simplifier.simproc (Theory.sign_of HOL.thy) "record_simp" ["s (u k r)"]
- (fn sg => fn _ => fn t =>
+ (fn sg => fn ss => fn t =>
(case t of (sel as Const (s, Type (_,[domS,rangeS])))$
((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=>
(case get_selectors sg s of SOME () =>
@@ -908,9 +910,9 @@
(case mk_eq_terms (upd$k$r) of
SOME (trm,trm',vars,update_s)
=> if update_s
- then SOME (prove_split_simp sg domS
+ then SOME (prove_split_simp sg ss domS
(list_all(vars,(equals rangeS$(sel$trm)$trm'))))
- else SOME (prove_split_simp sg domS
+ else SOME (prove_split_simp sg ss domS
(list_all(vars,(equals rangeS$(sel$trm)$(sel$trm')))))
| NONE => NONE)
end
@@ -929,7 +931,7 @@
*)
val record_upd_simproc =
Simplifier.simproc (Theory.sign_of HOL.thy) "record_upd_simp" ["(u k r)"]
- (fn sg => fn _ => fn t =>
+ (fn sg => fn ss => fn t =>
(case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
let datatype ('a,'b) calc = Init of 'b | Inter of 'a
val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get sg;
@@ -1020,7 +1022,7 @@
in (case mk_updterm updates [] t of
Inter (trm,trm',vars,_)
- => SOME (prove_split_simp sg rT
+ => SOME (prove_split_simp sg ss rT
(list_all(vars,(equals rT$trm$trm'))))
| _ => NONE)
end
@@ -1083,11 +1085,12 @@
val record_ex_sel_eq_simproc =
Simplifier.simproc (Theory.sign_of HOL.thy) "record_ex_sel_eq_simproc" ["Ex t"]
- (fn sg => fn _ => fn t =>
+ (fn sg => fn ss => fn t =>
let
- fun prove prop = (quick_and_dirty_prove true sg [] prop
- (fn _ => (simp_tac ((get_simpset sg) addsimps simp_thms
- addsimprocs [record_split_simproc (K ~1)]) 1)));
+ fun prove prop =
+ quick_and_dirty_prove true sg [] prop
+ (fn _ => simp_tac (Simplifier.inherit_bounds ss (get_simpset sg)
+ addsimps simp_thms addsimprocs [record_split_simproc (K ~1)]) 1);
fun mkeq (lr,Teq,(sel,Tsel),x) i =
(case get_selectors sg sel of SOME () =>
--- a/src/Provers/Arith/abel_cancel.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/abel_cancel.ML Mon Aug 01 19:20:26 2005 +0200
@@ -88,10 +88,10 @@
(* A simproc to cancel complementary terms in arbitrary sums. *)
-fun sum_proc sg _ t =
+fun sum_proc sg ss t =
let val t' = cancel sg t
val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
- (fn _ => simp_tac cancel_ss 1)
+ (fn _ => simp_tac (Simplifier.inherit_bounds ss cancel_ss) 1)
in SOME thm end
handle Cancel => NONE;
@@ -108,12 +108,12 @@
Reduces the problem to subtraction.
*)
- fun rel_proc sg _ t =
+ fun rel_proc sg ss t =
let val t' = cancel sg t
val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
(fn _ => rtac eq_reflection 1 THEN
resolve_tac eqI_rules 1 THEN
- simp_tac cancel_ss 1)
+ simp_tac (Simplifier.inherit_bounds ss cancel_ss) 1)
in SOME thm end
handle Cancel => NONE;
--- a/src/Provers/Arith/assoc_fold.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/assoc_fold.ML Mon Aug 01 19:20:26 2005 +0200
@@ -42,7 +42,7 @@
val trace = ref false;
(*Make a simproc to combine all literals in a associative nest*)
- fun proc thy _ lhs =
+ fun proc thy ss lhs =
let fun show t = string_of_cterm (Thm.cterm_of thy t)
val _ = if !trace then tracing ("assoc_fold simproc: LHS = " ^ show lhs)
else ()
@@ -56,7 +56,7 @@
val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
val th = Tactic.prove thy [] [] (Logic.mk_equals (lhs, rhs))
(fn _ => rtac Data.eq_reflection 1 THEN
- simp_tac assoc_ss 1)
+ simp_tac (Simplifier.inherit_bounds ss assoc_ss) 1)
in SOME th end
handle Assoc_fail => NONE;
--- a/src/Provers/Arith/cancel_numeral_factor.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Mon Aug 01 19:20:26 2005 +0200
@@ -29,24 +29,24 @@
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 -> Sign.sg ->
+ val prove_conv: tactic list -> theory ->
thm list -> string list -> term * term -> thm option
- val trans_tac: thm option -> tactic (*applies the initial lemma*)
- val norm_tac: tactic (*proves the initial lemma*)
- val numeral_simp_tac: tactic (*proves the final theorem*)
- val simplify_meta_eq: thm -> thm (*simplifies the final theorem*)
+ 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*)
+ val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*)
end;
functor CancelNumeralFactorFun(Data: CANCEL_NUMERAL_FACTOR_DATA):
sig
- val proc: Sign.sg -> simpset -> term -> thm option
+ val proc: theory -> simpset -> term -> thm option
end
=
struct
(*the simplification procedure*)
-fun proc sg ss t =
+fun proc thy ss t =
let
val hyps = prems_of_ss ss;
(*first freeze any Vars in the term to prevent flex-flex problems*)
@@ -67,13 +67,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] sg hyps xs
+ Data.prove_conv [Data.norm_tac ss] thy hyps xs
(t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2')))
in
- Option.map Data.simplify_meta_eq
+ Option.map (Data.simplify_meta_eq ss)
(Data.prove_conv
- [Data.trans_tac reshape, rtac Data.cancel 1,
- Data.numeral_simp_tac] sg hyps xs (t', rhs))
+ [Data.trans_tac ss reshape, rtac Data.cancel 1,
+ Data.numeral_simp_tac ss] thy hyps xs (t', rhs))
end
handle TERM _ => NONE
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral)
--- a/src/Provers/Arith/cancel_numerals.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Mon Aug 01 19:20:26 2005 +0200
@@ -36,18 +36,18 @@
val bal_add1: thm
val bal_add2: thm
(*proof tools*)
- val prove_conv: tactic list -> Sign.sg ->
+ val prove_conv: tactic list -> theory ->
thm list -> string list -> term * term -> thm option
- val trans_tac: thm option -> tactic (*applies the initial lemma*)
- val norm_tac: tactic (*proves the initial lemma*)
- val numeral_simp_tac: tactic (*proves the final theorem*)
- val simplify_meta_eq: thm -> thm (*simplifies the final theorem*)
+ 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*)
+ val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*)
end;
functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
sig
- val proc: Sign.sg -> simpset -> term -> thm option
+ val proc: theory -> simpset -> term -> thm option
end
=
struct
@@ -69,7 +69,7 @@
in seek terms1 end;
(*the simplification procedure*)
-fun proc sg ss t =
+fun proc thy ss t =
let
val hyps = prems_of_ss ss;
(*first freeze any Vars in the term to prevent flex-flex problems*)
@@ -86,22 +86,22 @@
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] sg hyps xs
+ else Data.prove_conv [Data.norm_tac ss] thy hyps xs
(t',
Data.mk_bal (newshape(n1,terms1'),
newshape(n2,terms2')))
in
- Option.map Data.simplify_meta_eq
+ Option.map (Data.simplify_meta_eq ss)
(if n2<=n1 then
Data.prove_conv
- [Data.trans_tac reshape, rtac Data.bal_add1 1,
- Data.numeral_simp_tac] sg hyps xs
+ [Data.trans_tac ss reshape, rtac Data.bal_add1 1,
+ Data.numeral_simp_tac ss] thy hyps xs
(t', Data.mk_bal (newshape(n1-n2,terms1'),
Data.mk_sum T terms2'))
else
Data.prove_conv
- [Data.trans_tac reshape, rtac Data.bal_add2 1,
- Data.numeral_simp_tac] sg hyps xs
+ [Data.trans_tac ss reshape, rtac Data.bal_add2 1,
+ Data.numeral_simp_tac ss] thy hyps xs
(t', Data.mk_bal (Data.mk_sum T terms1',
newshape(n2-n1,terms2'))))
end
--- a/src/Provers/Arith/combine_numerals.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/combine_numerals.ML Mon Aug 01 19:20:26 2005 +0200
@@ -27,17 +27,17 @@
(*rules*)
val left_distrib: thm
(*proof tools*)
- val prove_conv: tactic list -> Sign.sg -> string list -> term * term -> thm option
- val trans_tac: thm option -> tactic (*applies the initial lemma*)
- val norm_tac: tactic (*proves the initial lemma*)
- val numeral_simp_tac: tactic (*proves the final theorem*)
- val simplify_meta_eq: thm -> thm (*simplifies the final theorem*)
+ val prove_conv: tactic list -> theory -> 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*)
+ val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*)
end;
functor CombineNumeralsFun(Data: COMBINE_NUMERALS_DATA):
sig
- val proc: Sign.sg -> simpset -> term -> thm option
+ val proc: theory -> simpset -> term -> thm option
end
=
struct
@@ -64,7 +64,7 @@
| NONE => find_repeated (tab, t::past, terms);
(*the simplification procedure*)
-fun proc sg _ t =
+fun proc thy ss t =
let (*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')
@@ -73,15 +73,15 @@
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] sg xs
+ else Data.prove_conv [Data.norm_tac ss] thy xs
(t',
Data.mk_sum T ([Data.mk_coeff(m,u),
Data.mk_coeff(n,u)] @ terms))
in
- Option.map Data.simplify_meta_eq
+ Option.map (Data.simplify_meta_eq ss)
(Data.prove_conv
- [Data.trans_tac reshape, rtac Data.left_distrib 1,
- Data.numeral_simp_tac] sg xs
+ [Data.trans_tac ss reshape, rtac Data.left_distrib 1,
+ Data.numeral_simp_tac ss] thy 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 Mon Aug 01 19:20:25 2005 +0200
+++ b/src/Provers/Arith/extract_common_term.ML Mon Aug 01 19:20:26 2005 +0200
@@ -23,34 +23,34 @@
val dest_bal: term -> term * term
val find_first: term -> term list -> term list
(*proof tools*)
- val prove_conv: tactic list -> Sign.sg ->
+ val prove_conv: tactic list -> theory ->
thm list -> string list -> term * term -> thm option
- val norm_tac: tactic (*proves the result*)
- val simplify_meta_eq: thm -> thm (*simplifies the result*)
+ val norm_tac: simpset -> tactic (*proves the result*)
+ val simplify_meta_eq: simpset -> thm -> thm (*simplifies the result*)
end;
functor ExtractCommonTermFun(Data: EXTRACT_COMMON_TERM_DATA):
sig
- val proc: Sign.sg -> simpset -> term -> thm option
+ val proc: theory -> simpset -> term -> thm option
end
=
struct
(*Store the term t in the table*)
-fun update_by_coeff (tab, t) = Termtab.update ((t, ()), tab);
+fun update_by_coeff t tab = Termtab.update ((t, ()), tab);
(*a left-to-right scan of terms1, seeking a term u that is also in terms2*)
fun find_common (terms1,terms2) =
- let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2)
+ let val tab2 = fold update_by_coeff terms2 Termtab.empty
fun seek [] = raise TERM("find_common", [])
| seek (u::terms) =
- if isSome (Termtab.lookup (tab2, u)) then u
+ if Termtab.defined tab2 u then u
else seek terms
- in seek terms1 end;
+ in seek terms1 end;
(*the simplification procedure*)
-fun proc sg ss t =
+fun proc thy ss t =
let
val hyps = prems_of_ss ss;
(*first freeze any Vars in the term to prevent flex-flex problems*)
@@ -63,12 +63,12 @@
and terms2' = Data.find_first u terms2
and T = Term.fastype_of u
val reshape =
- Data.prove_conv [Data.norm_tac] sg hyps xs
+ Data.prove_conv [Data.norm_tac ss] thy hyps xs
(t',
Data.mk_bal (Data.mk_sum T (u::terms1'),
Data.mk_sum T (u::terms2')))
in
- Option.map Data.simplify_meta_eq reshape
+ Option.map (Data.simplify_meta_eq ss) reshape
end
handle TERM _ => NONE
| TYPE _ => NONE; (*Typically (if thy doesn't include Numeral)
--- a/src/ZF/Datatype.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/ZF/Datatype.ML Mon Aug 01 19:20:26 2005 +0200
@@ -62,9 +62,9 @@
fold_bal FOLogic.mk_conj
(map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
- val datatype_ss = simpset_of (the_context ());
+ val datatype_ss = simpset ();
- fun proc sg _ old =
+ fun proc sg ss old =
let val _ = if !trace then writeln ("data_free: OLD = " ^
string_of_cterm (cterm_of sg old))
else ()
@@ -88,7 +88,7 @@
else ();
val goal = Logic.mk_equals (old, new)
val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
- simp_tac (datatype_ss addsimps #free_iffs lcon_info) 1)
+ simp_tac (Simplifier.inherit_bounds ss datatype_ss addsimps #free_iffs lcon_info) 1)
handle ERROR_MESSAGE msg =>
(warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
raise Match)
@@ -96,9 +96,8 @@
handle Match => NONE;
- val conv =
- Simplifier.simproc (Theory.sign_of (theory "ZF")) "data_free"
- ["(x::i) = y"] proc;
+ val conv = Simplifier.simproc (theory "ZF") "data_free" ["(x::i) = y"] proc;
+
end;
--- a/src/ZF/Induct/Multiset.thy Mon Aug 01 19:20:25 2005 +0200
+++ b/src/ZF/Induct/Multiset.thy Mon Aug 01 19:20:26 2005 +0200
@@ -483,14 +483,12 @@
apply (rule int_of_diff, auto)
done
-(*FIXME: we should not have to rename x to x' below! There's a bug in the
- interaction between simproc inteq_cancel_numerals and the simplifier.*)
lemma setsum_decr2:
"Finite(A)
==> \<forall>M. multiset(M) --> (\<forall>a \<in> mset_of(M).
- setsum(%x'. $# mcount(funrestrict(M, mset_of(M)-{a}), x'), A) =
- (if a \<in> A then setsum(%x'. $# mcount(M, x'), A) $- $# M`a
- else setsum(%x'. $# mcount(M, x'), A)))"
+ setsum(%x. $# mcount(funrestrict(M, mset_of(M)-{a}), x), A) =
+ (if a \<in> A then setsum(%x. $# mcount(M, x), A) $- $# M`a
+ else setsum(%x. $# mcount(M, x), A)))"
apply (simp add: multiset_def)
apply (erule Finite_induct)
apply (auto simp add: multiset_fun_iff mcount_def mset_of_def)
--- a/src/ZF/Integ/int_arith.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/ZF/Integ/int_arith.ML Mon Aug 01 19:20:26 2005 +0200
@@ -224,19 +224,21 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff 1
val find_first_coeff = find_first_coeff []
- val trans_tac = ArithData.gen_trans_tac iff_trans
+ fun trans_tac _ = ArithData.gen_trans_tac iff_trans
val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
zminus_simps@zadd_ac
val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys
val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
zadd_ac@zmult_ac@tc_rules@intifys
- val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss3)
- val numeral_simp_tac =
- ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
- THEN ALLGOALS Asm_simp_tac
- val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s@mult_1s)
+ fun norm_tac ss =
+ ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss3))
+ fun numeral_simp_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
+ add_0s @ bin_simps @ tc_rules @ intifys))
+ THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_bounds ss simpset)))
+ val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s)
end;
@@ -298,17 +300,19 @@
val dest_coeff = dest_coeff 1
val left_distrib = left_zadd_zmult_distrib RS trans
val prove_conv = prove_conv_nohyps "int_combine_numerals"
- val trans_tac = ArithData.gen_trans_tac trans
+ fun trans_tac _ = ArithData.gen_trans_tac trans
val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
zminus_simps@zadd_ac@intifys
val norm_tac_ss2 = ZF_ss addsimps bin_simps@int_mult_minus_simps@intifys
val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
zadd_ac@zmult_ac@tc_rules@intifys
- val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss3)
- val numeral_simp_tac =
- ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
+ fun norm_tac ss =
+ ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss3))
+ fun numeral_simp_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
+ add_0s @ bin_simps @ tc_rules @ intifys))
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s@mult_1s)
end;
@@ -335,14 +339,16 @@
fun dest_coeff t = (dest_numeral t, one) (*We ONLY want pure numerals.*)
val left_distrib = zmult_assoc RS sym RS trans
val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
- val trans_tac = ArithData.gen_trans_tac trans
+ fun trans_tac _ = ArithData.gen_trans_tac trans
val norm_tac_ss1 = ZF_ss addsimps mult_1s@diff_simps@zminus_simps
val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
bin_simps@zmult_ac@tc_rules@intifys
- val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
- val numeral_simp_tac =
- ALLGOALS (simp_tac (ZF_ss addsimps bin_simps@tc_rules@intifys))
+ fun norm_tac ss =
+ ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
+ fun numeral_simp_tac ss =
+ ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
+ bin_simps @ tc_rules @ intifys))
val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s)
end;
--- a/src/ZF/arith_data.ML Mon Aug 01 19:20:25 2005 +0200
+++ b/src/ZF/arith_data.ML Mon Aug 01 19:20:26 2005 +0200
@@ -14,7 +14,7 @@
val gen_trans_tac: thm -> thm option -> tactic
val prove_conv: string -> tactic list -> Sign.sg ->
thm list -> string list -> term * term -> thm option
- val simplify_meta_eq: thm list -> thm -> thm
+ val simplify_meta_eq: thm list -> simpset -> thm -> thm
(*debugging*)
structure EqCancelNumeralsData : CANCEL_NUMERALS_DATA
structure LessCancelNumeralsData : CANCEL_NUMERALS_DATA
@@ -128,9 +128,9 @@
diff_natify1, diff_natify2];
(*Final simplification: cancel + and **)
-fun simplify_meta_eq rules =
+fun simplify_meta_eq rules ss =
mk_meta_eq o
- simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2]
+ simplify (Simplifier.inherit_bounds ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
delsimps iff_simps (*these could erase the whole rule!*)
addsimps rules);
@@ -143,13 +143,14 @@
val mk_coeff = mk_coeff
val dest_coeff = dest_coeff
val find_first_coeff = find_first_coeff []
- val norm_tac_ss1 = ZF_ss addsimps add_0s@add_succs@mult_1s@add_ac
- val norm_tac_ss2 = ZF_ss addsimps add_0s@mult_1s@
- add_ac@mult_ac@tc_rules@natifys
- val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
- THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
- val numeral_simp_tac_ss = ZF_ss addsimps add_0s@tc_rules@natifys
- val numeral_simp_tac = ALLGOALS (asm_simp_tac numeral_simp_tac_ss)
+ val norm_tac_ss1 = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ add_ac
+ val norm_tac_ss2 = ZF_ss addsimps add_0s @ mult_1s @ add_ac @ mult_ac @ tc_rules @ natifys
+ fun norm_tac ss =
+ ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
+ val numeral_simp_tac_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys
+ fun numeral_simp_tac ss =
+ ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss numeral_simp_tac_ss))
val simplify_meta_eq = simplify_meta_eq final_rules
end;
@@ -164,7 +165,7 @@
val dest_bal = FOLogic.dest_eq
val bal_add1 = eq_add_iff RS iff_trans
val bal_add2 = eq_add_iff RS iff_trans
- val trans_tac = gen_trans_tac iff_trans
+ fun trans_tac _ = gen_trans_tac iff_trans
end;
structure EqCancelNumerals = CancelNumeralsFun(EqCancelNumeralsData);
@@ -177,7 +178,7 @@
val dest_bal = FOLogic.dest_bin "Ordinal.lt" iT
val bal_add1 = less_add_iff RS iff_trans
val bal_add2 = less_add_iff RS iff_trans
- val trans_tac = gen_trans_tac iff_trans
+ fun trans_tac _ = gen_trans_tac iff_trans
end;
structure LessCancelNumerals = CancelNumeralsFun(LessCancelNumeralsData);
@@ -190,7 +191,7 @@
val dest_bal = FOLogic.dest_bin "Arith.diff" iT
val bal_add1 = diff_add_eq RS trans
val bal_add2 = diff_add_eq RS trans
- val trans_tac = gen_trans_tac trans
+ fun trans_tac _ = gen_trans_tac trans
end;
structure DiffCancelNumerals = CancelNumeralsFun(DiffCancelNumeralsData);