--- a/src/FOL/simpdata.ML Tue Aug 02 19:47:11 2005 +0200
+++ b/src/FOL/simpdata.ML Tue Aug 02 19:47:12 2005 +0200
@@ -267,11 +267,11 @@
end;
val defEX_regroup =
- Simplifier.simproc (Theory.sign_of (the_context ()))
+ Simplifier.simproc (the_context ())
"defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
val defALL_regroup =
- Simplifier.simproc (Theory.sign_of (the_context ()))
+ Simplifier.simproc (the_context ())
"defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
@@ -337,6 +337,10 @@
setmksimps (mksimps mksimps_pairs)
setmkcong mk_meta_cong;
+fun unfold_tac ss ths =
+ ALLGOALS (full_simp_tac
+ (Simplifier.inherit_bounds ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
+
(*intuitionistic simprules only*)
val IFOL_ss = FOL_basic_ss
--- a/src/HOL/Product_Type.thy Tue Aug 02 19:47:11 2005 +0200
+++ b/src/HOL/Product_Type.thy Tue Aug 02 19:47:12 2005 +0200
@@ -412,9 +412,9 @@
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 sg lhs rhs = mk_meta_eq (Tactic.prove sg [] []
+ fun metaeq thy ss lhs rhs = mk_meta_eq (Tactic.prove thy [] []
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
- (K (simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1)));
+ (K (simp_tac (Simplifier.inherit_bounds ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
| beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
@@ -426,14 +426,14 @@
| 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 sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
+ fun beta_proc thy ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
(case split_pat beta_term_pat 1 t of
- SOME (i,f) => SOME (metaeq sg s (subst arg 0 i f))
+ SOME (i,f) => SOME (metaeq thy ss s (subst arg 0 i f))
| NONE => NONE)
| beta_proc _ _ _ = NONE;
- fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) =
+ fun eta_proc thy ss (s as Const ("split", _) $ Abs (_, _, t)) =
(case split_pat eta_term_pat 1 t of
- SOME (_,ft) => SOME (metaeq sg s (let val (f $ arg) = ft in f end))
+ SOME (_,ft) => SOME (metaeq thy ss s (let val (f $ arg) = ft in f end))
| NONE => NONE)
| eta_proc _ _ _ = NONE;
in
--- a/src/HOL/Set.thy Tue Aug 02 19:47:11 2005 +0200
+++ b/src/HOL/Set.thy Tue Aug 02 19:47:12 2005 +0200
@@ -424,12 +424,16 @@
val Ball_def = thm "Ball_def";
val Bex_def = thm "Bex_def";
- val prove_bex_tac =
- rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
+ val simpset = Simplifier.clear_ss HOL_basic_ss;
+ fun unfold_tac ss th =
+ ALLGOALS (full_simp_tac (Simplifier.inherit_bounds ss simpset addsimps [th]));
+
+ fun prove_bex_tac ss =
+ unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac;
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
- val prove_ball_tac =
- rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
+ fun prove_ball_tac ss =
+ unfold_tac ss Ball_def THEN Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
in
val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
--- a/src/Provers/quantifier1.ML Tue Aug 02 19:47:11 2005 +0200
+++ b/src/Provers/quantifier1.ML Tue Aug 02 19:47:12 2005 +0200
@@ -57,10 +57,10 @@
sig
val prove_one_point_all_tac: tactic
val prove_one_point_ex_tac: tactic
- val rearrange_all: Sign.sg -> simpset -> term -> thm option
- val rearrange_ex: Sign.sg -> simpset -> term -> thm option
- val rearrange_ball: tactic -> Sign.sg -> simpset -> term -> thm option
- val rearrange_bex: tactic -> Sign.sg -> simpset -> term -> thm option
+ val rearrange_all: theory -> simpset -> term -> thm option
+ val rearrange_ex: theory -> simpset -> term -> thm option
+ val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
+ val rearrange_bex: (simpset -> tactic) -> theory -> simpset -> term -> thm option
end;
functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
@@ -103,8 +103,8 @@
| exqu xs P = extract xs P
in exqu end;
-fun prove_conv tac sg tu =
- Tactic.prove sg [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
+fun prove_conv tac thy tu =
+ Tactic.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i)
@@ -145,35 +145,35 @@
val Q = if n=0 then P else renumber 0 n P
in quant xs (qC $ Abs(x,T,Q)) end;
-fun rearrange_all sg _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
+fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
(case extract_quant extract_imp q [] P of
NONE => NONE
| SOME(xs,eq,Q) =>
let val R = quantify all x T xs (imp $ eq $ Q)
- in SOME(prove_conv prove_one_point_all_tac sg (F,R)) end)
+ in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
| rearrange_all _ _ _ = NONE;
-fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
+fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) =
(case extract_imp [] P of
NONE => NONE
| SOME(xs,eq,Q) => if not(null xs) then NONE else
let val R = imp $ eq $ Q
- in SOME(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
+ in SOME(prove_conv (tac ss) thy (F,Ball $ A $ Abs(x,T,R))) end)
| rearrange_ball _ _ _ _ = NONE;
-fun rearrange_ex sg _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
+fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
(case extract_quant extract_conj q [] P of
NONE => NONE
| SOME(xs,eq,Q) =>
let val R = quantify ex x T xs (conj $ eq $ Q)
- in SOME(prove_conv prove_one_point_ex_tac sg (F,R)) end)
+ in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
| rearrange_ex _ _ _ = NONE;
-fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
+fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) =
(case extract_conj [] P of
NONE => NONE
| SOME(xs,eq,Q) => if not(null xs) then NONE else
- SOME(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
+ SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
| rearrange_bex _ _ _ _ = NONE;
end;
--- a/src/ZF/OrdQuant.thy Tue Aug 02 19:47:11 2005 +0200
+++ b/src/ZF/OrdQuant.thy Tue Aug 02 19:47:12 2005 +0200
@@ -400,17 +400,17 @@
ML_setup {*
local
-val prove_rex_tac = rewtac rex_def THEN Quantifier1.prove_one_point_ex_tac;
+fun prove_rex_tac ss = unfold_tac ss [rex_def] THEN Quantifier1.prove_one_point_ex_tac;
val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
-val prove_rall_tac = rewtac rall_def THEN Quantifier1.prove_one_point_all_tac;
+fun prove_rall_tac ss = unfold_tac ss [rall_def] THEN Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
in
-val defREX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+val defREX_regroup = Simplifier.simproc (the_context ())
"defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
-val defRALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+val defRALL_regroup = Simplifier.simproc (the_context ())
"defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
end;
--- a/src/ZF/simpdata.ML Tue Aug 02 19:47:11 2005 +0200
+++ b/src/ZF/simpdata.ML Tue Aug 02 19:47:12 2005 +0200
@@ -53,22 +53,20 @@
addcongs [if_weak_cong]
setSolver type_solver;
-
-
local
-val prove_bex_tac = rewtac Bex_def THEN Quantifier1.prove_one_point_ex_tac;
+fun prove_bex_tac ss = unfold_tac ss [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
-val prove_ball_tac = rewtac Ball_def THEN Quantifier1.prove_one_point_all_tac;
+fun prove_ball_tac ss = unfold_tac ss [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
in
-val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+val defBEX_regroup = Simplifier.simproc (the_context ())
"defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
-val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
+val defBALL_regroup = Simplifier.simproc (the_context ())
"defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
end;