--- a/src/HOL/Algebra/abstract/Ring.thy Mon Oct 17 23:10:13 2005 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy Mon Oct 17 23:10:15 2005 +0200
@@ -167,7 +167,7 @@
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 (Simplifier.inherit_bounds ss ring_ss) 1)
+ (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
|> mk_meta_eq;
val (t', u) = Logic.dest_equals (Thm.prop_of rew);
in if t' aconv u
--- a/src/HOL/Fun.thy Mon Oct 17 23:10:13 2005 +0200
+++ b/src/HOL/Fun.thy Mon Oct 17 23:10:15 2005 +0200
@@ -489,7 +489,7 @@
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
+ simp_tac (Simplifier.inherit_context ss current_ss) 1
in
val fun_upd2_simproc =
Simplifier.simproc (Theory.sign_of (the_context ()))
--- a/src/HOL/Integ/int_factor_simprocs.ML Mon Oct 17 23:10:13 2005 +0200
+++ b/src/HOL/Integ/int_factor_simprocs.ML Mon Oct 17 23:10:15 2005 +0200
@@ -44,13 +44,13 @@
val dest_coeff = dest_coeff 1
val trans_tac = fn _ => trans_tac
fun norm_tac ss =
- let val HOL_ss' = Simplifier.inherit_bounds ss HOL_ss in
+ let val HOL_ss' = Simplifier.inherit_context 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))
+ ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rel_number_of @ bin_simps))
val simplify_meta_eq =
Int_Numeral_Simprocs.simplify_meta_eq
[add_0, add_0_right,
@@ -251,7 +251,7 @@
val find_first = find_first []
val trans_tac = fn _ => trans_tac
fun norm_tac ss =
- ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
+ ALLGOALS (simp_tac (Simplifier.inherit_context 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 Oct 17 23:10:13 2005 +0200
+++ b/src/HOL/Integ/nat_simprocs.ML Mon Oct 17 23:10:15 2005 +0200
@@ -170,13 +170,13 @@
val find_first_coeff = find_first_coeff []
val trans_tac = fn _ => trans_tac
fun norm_tac ss =
- let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+ let val num_ss' = Simplifier.inherit_context 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))
end
fun numeral_simp_tac ss =
- ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
+ ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
val simplify_meta_eq = simplify_meta_eq
end;
@@ -255,13 +255,13 @@
val prove_conv = Bin_Simprocs.prove_conv_nohyps
val trans_tac = fn _ => trans_tac
fun norm_tac ss =
- let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+ let val num_ss' = Simplifier.inherit_context 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))
end
fun numeral_simp_tac ss =
- ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
+ ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
val simplify_meta_eq = simplify_meta_eq
end;
@@ -279,13 +279,13 @@
val dest_coeff = dest_coeff
val trans_tac = fn _ => trans_tac
fun norm_tac ss =
- let val num_ss' = Simplifier.inherit_bounds ss num_ss in
+ let val num_ss' = Simplifier.inherit_context 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))
end
fun numeral_simp_tac ss =
- ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps bin_simps))
+ ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps bin_simps))
val simplify_meta_eq = simplify_meta_eq
end
@@ -372,7 +372,7 @@
val find_first = find_first []
val trans_tac = fn _ => trans_tac
fun norm_tac ss =
- ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
+ ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac))
end;
structure EqCancelFactor = ExtractCommonTermFun
--- a/src/HOL/List.thy Mon Oct 17 23:10:13 2005 +0200
+++ b/src/HOL/List.thy Mon Oct 17 23:10:15 2005 +0200
@@ -454,7 +454,7 @@
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 (simp_tac (Simplifier.inherit_bounds ss rearr_ss) 1));
+ (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
in
--- a/src/Provers/Arith/abel_cancel.ML Mon Oct 17 23:10:13 2005 +0200
+++ b/src/Provers/Arith/abel_cancel.ML Mon Oct 17 23:10:15 2005 +0200
@@ -91,7 +91,7 @@
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 (Simplifier.inherit_bounds ss cancel_ss) 1)
+ (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
in SOME thm end
handle Cancel => NONE;
@@ -113,7 +113,7 @@
val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
(fn _ => rtac eq_reflection 1 THEN
resolve_tac eqI_rules 1 THEN
- simp_tac (Simplifier.inherit_bounds ss cancel_ss) 1)
+ simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
in SOME thm end
handle Cancel => NONE;
--- a/src/Provers/Arith/assoc_fold.ML Mon Oct 17 23:10:13 2005 +0200
+++ b/src/Provers/Arith/assoc_fold.ML Mon Oct 17 23:10:15 2005 +0200
@@ -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 (Simplifier.inherit_bounds ss assoc_ss) 1)
+ simp_tac (Simplifier.inherit_context ss assoc_ss) 1)
in SOME th end
handle Assoc_fail => NONE;
--- a/src/Provers/Arith/fast_lin_arith.ML Mon Oct 17 23:10:13 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Mon Oct 17 23:10:15 2005 +0200
@@ -417,7 +417,7 @@
fun mkthm (sg, ss) asms just =
let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
Data.get sg;
- val simpset' = Simplifier.inherit_bounds ss simpset;
+ val simpset' = Simplifier.inherit_context ss simpset;
val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
map fst lhs union (map fst rhs union ats))
([], List.mapPartial (fn thm => if Thm.no_prems thm
--- a/src/ZF/Datatype.ML Mon Oct 17 23:10:13 2005 +0200
+++ b/src/ZF/Datatype.ML Mon Oct 17 23:10:15 2005 +0200
@@ -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 (Simplifier.inherit_bounds ss datatype_ss addsimps #free_iffs lcon_info) 1)
+ simp_tac (Simplifier.inherit_context 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)
--- a/src/ZF/Integ/int_arith.ML Mon Oct 17 23:10:13 2005 +0200
+++ b/src/ZF/Integ/int_arith.ML Mon Oct 17 23:10:15 2005 +0200
@@ -231,13 +231,13 @@
val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
zadd_ac@zmult_ac@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))
+ ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss3))
fun numeral_simp_tac ss =
- ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
+ ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
add_0s @ bin_simps @ tc_rules @ intifys))
- THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_bounds ss simpset)))
+ THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s)
end;
@@ -307,11 +307,11 @@
val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
zadd_ac@zmult_ac@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))
+ ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss3))
fun numeral_simp_tac ss =
- ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
+ ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
add_0s @ bin_simps @ tc_rules @ intifys))
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s@mult_1s)
end;
@@ -344,10 +344,10 @@
val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
bin_simps@zmult_ac@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))
+ ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
fun numeral_simp_tac ss =
- ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
+ ALLGOALS (simp_tac (Simplifier.inherit_context 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 Oct 17 23:10:13 2005 +0200
+++ b/src/ZF/arith_data.ML Mon Oct 17 23:10:15 2005 +0200
@@ -130,7 +130,7 @@
(*Final simplification: cancel + and **)
fun simplify_meta_eq rules ss =
mk_meta_eq o
- simplify (Simplifier.inherit_bounds ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
+ simplify (Simplifier.inherit_context ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
delsimps iff_simps (*these could erase the whole rule!*)
addsimps rules);
@@ -146,11 +146,11 @@
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))
+ ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
+ THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context 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))
+ ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_tac_ss))
val simplify_meta_eq = simplify_meta_eq final_rules
end;