simprocs: Simplifier.inherit_bounds;
authorwenzelm
Tue Aug 02 19:47:12 2005 +0200 (2005-08-02)
changeset 17002fb9261990ffe
parent 17001 51ff2bc32774
child 17003 b902e11b3df1
simprocs: Simplifier.inherit_bounds;
src/FOL/simpdata.ML
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/Provers/quantifier1.ML
src/ZF/OrdQuant.thy
src/ZF/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Tue Aug 02 19:47:11 2005 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Tue Aug 02 19:47:12 2005 +0200
     1.3 @@ -267,11 +267,11 @@
     1.4  end;
     1.5  
     1.6  val defEX_regroup =
     1.7 -  Simplifier.simproc (Theory.sign_of (the_context ()))
     1.8 +  Simplifier.simproc (the_context ())
     1.9      "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex;
    1.10  
    1.11  val defALL_regroup =
    1.12 -  Simplifier.simproc (Theory.sign_of (the_context ()))
    1.13 +  Simplifier.simproc (the_context ())
    1.14      "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all;
    1.15  
    1.16  
    1.17 @@ -337,6 +337,10 @@
    1.18    setmksimps (mksimps mksimps_pairs)
    1.19    setmkcong mk_meta_cong;
    1.20  
    1.21 +fun unfold_tac ss ths =
    1.22 +  ALLGOALS (full_simp_tac
    1.23 +    (Simplifier.inherit_bounds ss (Simplifier.clear_ss FOL_basic_ss) addsimps ths));
    1.24 +
    1.25  
    1.26  (*intuitionistic simprules only*)
    1.27  val IFOL_ss = FOL_basic_ss
     2.1 --- a/src/HOL/Product_Type.thy	Tue Aug 02 19:47:11 2005 +0200
     2.2 +++ b/src/HOL/Product_Type.thy	Tue Aug 02 19:47:12 2005 +0200
     2.3 @@ -412,9 +412,9 @@
     2.4    fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE
     2.5    |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
     2.6    |   split_pat tp i _ = NONE;
     2.7 -  fun metaeq sg lhs rhs = mk_meta_eq (Tactic.prove sg [] []
     2.8 +  fun metaeq thy ss lhs rhs = mk_meta_eq (Tactic.prove thy [] []
     2.9          (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
    2.10 -        (K (simp_tac (HOL_basic_ss addsimps [cond_split_eta]) 1)));
    2.11 +        (K (simp_tac (Simplifier.inherit_bounds ss HOL_basic_ss addsimps [cond_split_eta]) 1)));
    2.12  
    2.13    fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
    2.14    |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
    2.15 @@ -426,14 +426,14 @@
    2.16    |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
    2.17                                else (subst arg k i t $ subst arg k i u)
    2.18    |   subst arg k i t = t;
    2.19 -  fun beta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
    2.20 +  fun beta_proc thy ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
    2.21          (case split_pat beta_term_pat 1 t of
    2.22 -        SOME (i,f) => SOME (metaeq sg s (subst arg 0 i f))
    2.23 +        SOME (i,f) => SOME (metaeq thy ss s (subst arg 0 i f))
    2.24          | NONE => NONE)
    2.25    |   beta_proc _ _ _ = NONE;
    2.26 -  fun eta_proc sg _ (s as Const ("split", _) $ Abs (_, _, t)) =
    2.27 +  fun eta_proc thy ss (s as Const ("split", _) $ Abs (_, _, t)) =
    2.28          (case split_pat eta_term_pat 1 t of
    2.29 -          SOME (_,ft) => SOME (metaeq sg s (let val (f $ arg) = ft in f end))
    2.30 +          SOME (_,ft) => SOME (metaeq thy ss s (let val (f $ arg) = ft in f end))
    2.31          | NONE => NONE)
    2.32    |   eta_proc _ _ _ = NONE;
    2.33  in
     3.1 --- a/src/HOL/Set.thy	Tue Aug 02 19:47:11 2005 +0200
     3.2 +++ b/src/HOL/Set.thy	Tue Aug 02 19:47:12 2005 +0200
     3.3 @@ -424,12 +424,16 @@
     3.4      val Ball_def = thm "Ball_def";
     3.5      val Bex_def = thm "Bex_def";
     3.6  
     3.7 -    val prove_bex_tac =
     3.8 -      rewrite_goals_tac [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
     3.9 +    val simpset = Simplifier.clear_ss HOL_basic_ss;
    3.10 +    fun unfold_tac ss th =
    3.11 +      ALLGOALS (full_simp_tac (Simplifier.inherit_bounds ss simpset addsimps [th]));
    3.12 +
    3.13 +    fun prove_bex_tac ss =
    3.14 +      unfold_tac ss Bex_def THEN Quantifier1.prove_one_point_ex_tac;
    3.15      val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    3.16  
    3.17 -    val prove_ball_tac =
    3.18 -      rewrite_goals_tac [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
    3.19 +    fun prove_ball_tac ss =
    3.20 +      unfold_tac ss Ball_def THEN Quantifier1.prove_one_point_all_tac;
    3.21      val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    3.22    in
    3.23      val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
     4.1 --- a/src/Provers/quantifier1.ML	Tue Aug 02 19:47:11 2005 +0200
     4.2 +++ b/src/Provers/quantifier1.ML	Tue Aug 02 19:47:12 2005 +0200
     4.3 @@ -57,10 +57,10 @@
     4.4  sig
     4.5    val prove_one_point_all_tac: tactic
     4.6    val prove_one_point_ex_tac: tactic
     4.7 -  val rearrange_all: Sign.sg -> simpset -> term -> thm option
     4.8 -  val rearrange_ex:  Sign.sg -> simpset -> term -> thm option
     4.9 -  val rearrange_ball: tactic -> Sign.sg -> simpset -> term -> thm option
    4.10 -  val rearrange_bex:  tactic -> Sign.sg -> simpset -> term -> thm option
    4.11 +  val rearrange_all: theory -> simpset -> term -> thm option
    4.12 +  val rearrange_ex:  theory -> simpset -> term -> thm option
    4.13 +  val rearrange_ball: (simpset -> tactic) -> theory -> simpset -> term -> thm option
    4.14 +  val rearrange_bex:  (simpset -> tactic) -> theory -> simpset -> term -> thm option
    4.15  end;
    4.16  
    4.17  functor Quantifier1Fun(Data: QUANTIFIER1_DATA): QUANTIFIER1 =
    4.18 @@ -103,8 +103,8 @@
    4.19          | exqu xs P = extract xs P
    4.20    in exqu end;
    4.21  
    4.22 -fun prove_conv tac sg tu =
    4.23 -  Tactic.prove sg [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
    4.24 +fun prove_conv tac thy tu =
    4.25 +  Tactic.prove thy [] [] (Logic.mk_equals tu) (K (rtac iff_reflection 1 THEN tac));
    4.26  
    4.27  fun qcomm_tac qcomm qI i = REPEAT_DETERM (rtac qcomm i THEN rtac qI i) 
    4.28  
    4.29 @@ -145,35 +145,35 @@
    4.30        val Q = if n=0 then P else renumber 0 n P
    4.31    in quant xs (qC $ Abs(x,T,Q)) end;
    4.32  
    4.33 -fun rearrange_all sg _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
    4.34 +fun rearrange_all thy _ (F as (all as Const(q,_)) $ Abs(x,T, P)) =
    4.35       (case extract_quant extract_imp q [] P of
    4.36          NONE => NONE
    4.37        | SOME(xs,eq,Q) =>
    4.38            let val R = quantify all x T xs (imp $ eq $ Q)
    4.39 -          in SOME(prove_conv prove_one_point_all_tac sg (F,R)) end)
    4.40 +          in SOME(prove_conv prove_one_point_all_tac thy (F,R)) end)
    4.41    | rearrange_all _ _ _ = NONE;
    4.42  
    4.43 -fun rearrange_ball tac sg _ (F as Ball $ A $ Abs(x,T,P)) =
    4.44 +fun rearrange_ball tac thy ss (F as Ball $ A $ Abs(x,T,P)) =
    4.45       (case extract_imp [] P of
    4.46          NONE => NONE
    4.47        | SOME(xs,eq,Q) => if not(null xs) then NONE else
    4.48            let val R = imp $ eq $ Q
    4.49 -          in SOME(prove_conv tac sg (F,Ball $ A $ Abs(x,T,R))) end)
    4.50 +          in SOME(prove_conv (tac ss) thy (F,Ball $ A $ Abs(x,T,R))) end)
    4.51    | rearrange_ball _ _ _ _ = NONE;
    4.52  
    4.53 -fun rearrange_ex sg _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
    4.54 +fun rearrange_ex thy _ (F as (ex as Const(q,_)) $ Abs(x,T,P)) =
    4.55       (case extract_quant extract_conj q [] P of
    4.56          NONE => NONE
    4.57        | SOME(xs,eq,Q) =>
    4.58            let val R = quantify ex x T xs (conj $ eq $ Q)
    4.59 -          in SOME(prove_conv prove_one_point_ex_tac sg (F,R)) end)
    4.60 +          in SOME(prove_conv prove_one_point_ex_tac thy (F,R)) end)
    4.61    | rearrange_ex _ _ _ = NONE;
    4.62  
    4.63 -fun rearrange_bex tac sg _ (F as Bex $ A $ Abs(x,T,P)) =
    4.64 +fun rearrange_bex tac thy ss (F as Bex $ A $ Abs(x,T,P)) =
    4.65       (case extract_conj [] P of
    4.66          NONE => NONE
    4.67        | SOME(xs,eq,Q) => if not(null xs) then NONE else
    4.68 -          SOME(prove_conv tac sg (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
    4.69 +          SOME(prove_conv (tac ss) thy (F,Bex $ A $ Abs(x,T,conj$eq$Q))))
    4.70    | rearrange_bex _ _ _ _ = NONE;
    4.71  
    4.72  end;
     5.1 --- a/src/ZF/OrdQuant.thy	Tue Aug 02 19:47:11 2005 +0200
     5.2 +++ b/src/ZF/OrdQuant.thy	Tue Aug 02 19:47:12 2005 +0200
     5.3 @@ -400,17 +400,17 @@
     5.4  ML_setup {*
     5.5  local
     5.6  
     5.7 -val prove_rex_tac = rewtac rex_def THEN Quantifier1.prove_one_point_ex_tac;
     5.8 +fun prove_rex_tac ss = unfold_tac ss [rex_def] THEN Quantifier1.prove_one_point_ex_tac;
     5.9  val rearrange_bex = Quantifier1.rearrange_bex prove_rex_tac;
    5.10  
    5.11 -val prove_rall_tac = rewtac rall_def THEN Quantifier1.prove_one_point_all_tac;
    5.12 +fun prove_rall_tac ss = unfold_tac ss [rall_def] THEN Quantifier1.prove_one_point_all_tac;
    5.13  val rearrange_ball = Quantifier1.rearrange_ball prove_rall_tac;
    5.14  
    5.15  in
    5.16  
    5.17 -val defREX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
    5.18 +val defREX_regroup = Simplifier.simproc (the_context ())
    5.19    "defined REX" ["EX x[M]. P(x) & Q(x)"] rearrange_bex;
    5.20 -val defRALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
    5.21 +val defRALL_regroup = Simplifier.simproc (the_context ())
    5.22    "defined RALL" ["ALL x[M]. P(x) --> Q(x)"] rearrange_ball;
    5.23  
    5.24  end;
     6.1 --- a/src/ZF/simpdata.ML	Tue Aug 02 19:47:11 2005 +0200
     6.2 +++ b/src/ZF/simpdata.ML	Tue Aug 02 19:47:12 2005 +0200
     6.3 @@ -53,22 +53,20 @@
     6.4    addcongs [if_weak_cong]
     6.5    setSolver type_solver;
     6.6  
     6.7 -
     6.8 -
     6.9  local
    6.10  
    6.11 -val prove_bex_tac = rewtac Bex_def THEN Quantifier1.prove_one_point_ex_tac;
    6.12 +fun prove_bex_tac ss = unfold_tac ss [Bex_def] THEN Quantifier1.prove_one_point_ex_tac;
    6.13  val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    6.14  
    6.15 -val prove_ball_tac = rewtac Ball_def THEN Quantifier1.prove_one_point_all_tac;
    6.16 +fun prove_ball_tac ss = unfold_tac ss [Ball_def] THEN Quantifier1.prove_one_point_all_tac;
    6.17  val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    6.18  
    6.19  in
    6.20  
    6.21 -val defBEX_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
    6.22 +val defBEX_regroup = Simplifier.simproc (the_context ())
    6.23    "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
    6.24  
    6.25 -val defBALL_regroup = Simplifier.simproc (Theory.sign_of (the_context ()))
    6.26 +val defBALL_regroup = Simplifier.simproc (the_context ())
    6.27    "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
    6.28  
    6.29  end;