Simplifier.inherit_context instead of Simplifier.inherit_bounds;
authorwenzelm
Mon Oct 17 23:10:15 2005 +0200 (2005-10-17)
changeset 1787767d5ab1cb0d8
parent 17876 b9c92f384109
child 17878 5b9efe4d6b47
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
src/HOL/Algebra/abstract/Ring.thy
src/HOL/Fun.thy
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/List.thy
src/Provers/Arith/abel_cancel.ML
src/Provers/Arith/assoc_fold.ML
src/Provers/Arith/fast_lin_arith.ML
src/ZF/Datatype.ML
src/ZF/Integ/int_arith.ML
src/ZF/arith_data.ML
     1.1 --- a/src/HOL/Algebra/abstract/Ring.thy	Mon Oct 17 23:10:13 2005 +0200
     1.2 +++ b/src/HOL/Algebra/abstract/Ring.thy	Mon Oct 17 23:10:15 2005 +0200
     1.3 @@ -167,7 +167,7 @@
     1.4        let val rew = Tactic.prove sg [] []
     1.5              (HOLogic.mk_Trueprop
     1.6                (HOLogic.mk_eq (t, Var (("x", Term.maxidx_of_term t + 1), fastype_of t))))
     1.7 -                (fn _ => simp_tac (Simplifier.inherit_bounds ss ring_ss) 1)
     1.8 +                (fn _ => simp_tac (Simplifier.inherit_context ss ring_ss) 1)
     1.9              |> mk_meta_eq;
    1.10            val (t', u) = Logic.dest_equals (Thm.prop_of rew);
    1.11        in if t' aconv u 
     2.1 --- a/src/HOL/Fun.thy	Mon Oct 17 23:10:13 2005 +0200
     2.2 +++ b/src/HOL/Fun.thy	Mon Oct 17 23:10:15 2005 +0200
     2.3 @@ -489,7 +489,7 @@
     2.4    val current_ss = simpset ()
     2.5    fun fun_upd_prover ss =
     2.6      rtac eq_reflection 1 THEN rtac ext 1 THEN
     2.7 -    simp_tac (Simplifier.inherit_bounds ss current_ss) 1
     2.8 +    simp_tac (Simplifier.inherit_context ss current_ss) 1
     2.9  in
    2.10    val fun_upd2_simproc =
    2.11      Simplifier.simproc (Theory.sign_of (the_context ()))
     3.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Mon Oct 17 23:10:13 2005 +0200
     3.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Mon Oct 17 23:10:15 2005 +0200
     3.3 @@ -44,13 +44,13 @@
     3.4    val dest_coeff        = dest_coeff 1
     3.5    val trans_tac         = fn _ => trans_tac
     3.6    fun norm_tac ss =
     3.7 -    let val HOL_ss' = Simplifier.inherit_bounds ss HOL_ss in
     3.8 +    let val HOL_ss' = Simplifier.inherit_context ss HOL_ss in
     3.9        ALLGOALS (simp_tac (HOL_ss' addsimps minus_from_mult_simps @ mult_1s))
    3.10        THEN ALLGOALS (simp_tac (HOL_ss' addsimps bin_simps@mult_minus_simps))
    3.11        THEN ALLGOALS (simp_tac (HOL_ss' addsimps mult_ac))
    3.12      end
    3.13    fun numeral_simp_tac ss =
    3.14 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps rel_number_of @ bin_simps))
    3.15 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps rel_number_of @ bin_simps))
    3.16    val simplify_meta_eq = 
    3.17  	Int_Numeral_Simprocs.simplify_meta_eq
    3.18  	     [add_0, add_0_right,
    3.19 @@ -251,7 +251,7 @@
    3.20    val find_first        = find_first []
    3.21    val trans_tac         = fn _ => trans_tac
    3.22    fun norm_tac ss =
    3.23 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
    3.24 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac))
    3.25    end;
    3.26  
    3.27  (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in
     4.1 --- a/src/HOL/Integ/nat_simprocs.ML	Mon Oct 17 23:10:13 2005 +0200
     4.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Mon Oct 17 23:10:15 2005 +0200
     4.3 @@ -170,13 +170,13 @@
     4.4    val find_first_coeff  = find_first_coeff []
     4.5    val trans_tac         = fn _ => trans_tac
     4.6    fun norm_tac ss =
     4.7 -    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
     4.8 +    let val num_ss' = Simplifier.inherit_context ss num_ss in
     4.9        ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    4.10                                  [Suc_eq_add_numeral_1_left] @ add_ac))
    4.11        THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
    4.12      end
    4.13    fun numeral_simp_tac ss =
    4.14 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
    4.15 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
    4.16    val simplify_meta_eq  = simplify_meta_eq
    4.17    end;
    4.18  
    4.19 @@ -255,13 +255,13 @@
    4.20    val prove_conv        = Bin_Simprocs.prove_conv_nohyps
    4.21    val trans_tac         = fn _ => trans_tac
    4.22    fun norm_tac ss =
    4.23 -    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    4.24 +    let val num_ss' = Simplifier.inherit_context ss num_ss in
    4.25        ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    4.26                                [Suc_eq_add_numeral_1] @ add_ac))
    4.27        THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
    4.28      end
    4.29    fun numeral_simp_tac ss =
    4.30 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps add_0s @ bin_simps))
    4.31 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps add_0s @ bin_simps))
    4.32    val simplify_meta_eq  = simplify_meta_eq
    4.33    end;
    4.34  
    4.35 @@ -279,13 +279,13 @@
    4.36    val dest_coeff        = dest_coeff
    4.37    val trans_tac         = fn _ => trans_tac
    4.38    fun norm_tac ss =
    4.39 -    let val num_ss' = Simplifier.inherit_bounds ss num_ss in
    4.40 +    let val num_ss' = Simplifier.inherit_context ss num_ss in
    4.41        ALLGOALS (simp_tac (num_ss' addsimps numeral_syms @ add_0s @ mult_1s @
    4.42                                  [Suc_eq_add_numeral_1_left] @ add_ac))
    4.43        THEN ALLGOALS (simp_tac (num_ss' addsimps bin_simps @ add_ac @ mult_ac))
    4.44      end
    4.45    fun numeral_simp_tac ss =
    4.46 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps bin_simps))
    4.47 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps bin_simps))
    4.48    val simplify_meta_eq  = simplify_meta_eq
    4.49    end
    4.50  
    4.51 @@ -372,7 +372,7 @@
    4.52    val find_first        = find_first []
    4.53    val trans_tac         = fn _ => trans_tac
    4.54    fun norm_tac ss =
    4.55 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
    4.56 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss HOL_ss addsimps mult_1s @ mult_ac))
    4.57    end;
    4.58  
    4.59  structure EqCancelFactor = ExtractCommonTermFun
     5.1 --- a/src/HOL/List.thy	Mon Oct 17 23:10:13 2005 +0200
     5.2 +++ b/src/HOL/List.thy	Mon Oct 17 23:10:15 2005 +0200
     5.3 @@ -454,7 +454,7 @@
     5.4          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
     5.5          val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
     5.6          val thm = Tactic.prove sg [] [] eq
     5.7 -          (K (simp_tac (Simplifier.inherit_bounds ss rearr_ss) 1));
     5.8 +          (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
     5.9        in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
    5.10  
    5.11    in
     6.1 --- a/src/Provers/Arith/abel_cancel.ML	Mon Oct 17 23:10:13 2005 +0200
     6.2 +++ b/src/Provers/Arith/abel_cancel.ML	Mon Oct 17 23:10:15 2005 +0200
     6.3 @@ -91,7 +91,7 @@
     6.4  fun sum_proc sg ss t =
     6.5     let val t' = cancel sg t
     6.6         val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
     6.7 -                   (fn _ => simp_tac (Simplifier.inherit_bounds ss cancel_ss) 1)
     6.8 +                   (fn _ => simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
     6.9     in SOME thm end
    6.10     handle Cancel => NONE;
    6.11  
    6.12 @@ -113,7 +113,7 @@
    6.13         val thm = Tactic.prove sg [] [] (Logic.mk_equals (t, t'))
    6.14                     (fn _ => rtac eq_reflection 1 THEN
    6.15                              resolve_tac eqI_rules 1 THEN
    6.16 -                            simp_tac (Simplifier.inherit_bounds ss cancel_ss) 1)
    6.17 +                            simp_tac (Simplifier.inherit_context ss cancel_ss) 1)
    6.18     in SOME thm end
    6.19     handle Cancel => NONE;
    6.20  
     7.1 --- a/src/Provers/Arith/assoc_fold.ML	Mon Oct 17 23:10:13 2005 +0200
     7.2 +++ b/src/Provers/Arith/assoc_fold.ML	Mon Oct 17 23:10:15 2005 +0200
     7.3 @@ -56,7 +56,7 @@
     7.4         val _ = if !trace then tracing ("RHS = " ^ show rhs) else ()
     7.5         val th = Tactic.prove thy [] [] (Logic.mk_equals (lhs, rhs))
     7.6                     (fn _ => rtac Data.eq_reflection 1 THEN
     7.7 -                            simp_tac (Simplifier.inherit_bounds ss assoc_ss) 1)
     7.8 +                            simp_tac (Simplifier.inherit_context ss assoc_ss) 1)
     7.9     in SOME th end
    7.10     handle Assoc_fail => NONE;
    7.11  
     8.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Mon Oct 17 23:10:13 2005 +0200
     8.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Oct 17 23:10:15 2005 +0200
     8.3 @@ -417,7 +417,7 @@
     8.4  fun mkthm (sg, ss) asms just =
     8.5    let val {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset, ...} =
     8.6            Data.get sg;
     8.7 -      val simpset' = Simplifier.inherit_bounds ss simpset;
     8.8 +      val simpset' = Simplifier.inherit_context ss simpset;
     8.9        val atoms = Library.foldl (fn (ats,(lhs,_,_,rhs,_,_)) =>
    8.10                              map fst lhs  union  (map fst rhs  union  ats))
    8.11                          ([], List.mapPartial (fn thm => if Thm.no_prems thm
     9.1 --- a/src/ZF/Datatype.ML	Mon Oct 17 23:10:13 2005 +0200
     9.2 +++ b/src/ZF/Datatype.ML	Mon Oct 17 23:10:15 2005 +0200
     9.3 @@ -88,7 +88,7 @@
     9.4                 else ();
     9.5         val goal = Logic.mk_equals (old, new)
     9.6         val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
     9.7 -           simp_tac (Simplifier.inherit_bounds ss datatype_ss addsimps #free_iffs lcon_info) 1)
     9.8 +           simp_tac (Simplifier.inherit_context ss datatype_ss addsimps #free_iffs lcon_info) 1)
     9.9           handle ERROR_MESSAGE msg =>
    9.10           (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
    9.11            raise Match)
    10.1 --- a/src/ZF/Integ/int_arith.ML	Mon Oct 17 23:10:13 2005 +0200
    10.2 +++ b/src/ZF/Integ/int_arith.ML	Mon Oct 17 23:10:15 2005 +0200
    10.3 @@ -231,13 +231,13 @@
    10.4    val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
    10.5                                      zadd_ac@zmult_ac@tc_rules@intifys
    10.6    fun norm_tac ss =
    10.7 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
    10.8 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
    10.9 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss3))
   10.10 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
   10.11 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
   10.12 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss3))
   10.13    fun numeral_simp_tac ss =
   10.14 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
   10.15 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
   10.16        add_0s @ bin_simps @ tc_rules @ intifys))
   10.17 -    THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_bounds ss simpset)))
   10.18 +    THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
   10.19    val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   10.20    end;
   10.21  
   10.22 @@ -307,11 +307,11 @@
   10.23    val norm_tac_ss3 = ZF_ss addsimps int_minus_from_mult_simps@
   10.24                                      zadd_ac@zmult_ac@tc_rules@intifys
   10.25    fun norm_tac ss =
   10.26 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
   10.27 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
   10.28 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss3))
   10.29 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
   10.30 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
   10.31 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss3))
   10.32    fun numeral_simp_tac ss =
   10.33 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
   10.34 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
   10.35        add_0s @ bin_simps @ tc_rules @ intifys))
   10.36    val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
   10.37    end;
   10.38 @@ -344,10 +344,10 @@
   10.39    val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
   10.40                                      bin_simps@zmult_ac@tc_rules@intifys
   10.41    fun norm_tac ss =
   10.42 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
   10.43 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
   10.44 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
   10.45 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
   10.46    fun numeral_simp_tac ss =
   10.47 -    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss ZF_ss addsimps
   10.48 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss ZF_ss addsimps
   10.49        bin_simps @ tc_rules @ intifys))
   10.50    val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s)
   10.51    end;
    11.1 --- a/src/ZF/arith_data.ML	Mon Oct 17 23:10:13 2005 +0200
    11.2 +++ b/src/ZF/arith_data.ML	Mon Oct 17 23:10:15 2005 +0200
    11.3 @@ -130,7 +130,7 @@
    11.4  (*Final simplification: cancel + and **)
    11.5  fun simplify_meta_eq rules ss =
    11.6      mk_meta_eq o
    11.7 -    simplify (Simplifier.inherit_bounds ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
    11.8 +    simplify (Simplifier.inherit_context ss FOL_ss addeqcongs[eq_cong2,iff_cong2]
    11.9                       delsimps iff_simps (*these could erase the whole rule!*)
   11.10                       addsimps rules);
   11.11  
   11.12 @@ -146,11 +146,11 @@
   11.13    val norm_tac_ss1      = ZF_ss addsimps add_0s @ add_succs @ mult_1s @ add_ac
   11.14    val norm_tac_ss2      = ZF_ss addsimps add_0s @ mult_1s @ add_ac @ mult_ac @ tc_rules @ natifys
   11.15    fun norm_tac ss =
   11.16 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss1))
   11.17 -    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss norm_tac_ss2))
   11.18 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss1))
   11.19 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_tac_ss2))
   11.20    val numeral_simp_tac_ss = ZF_ss addsimps add_0s @ tc_rules @ natifys
   11.21    fun numeral_simp_tac ss =
   11.22 -    ALLGOALS (asm_simp_tac (Simplifier.inherit_bounds ss numeral_simp_tac_ss))
   11.23 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss numeral_simp_tac_ss))
   11.24    val simplify_meta_eq  = simplify_meta_eq final_rules
   11.25    end;
   11.26