Simplifier.theory_context;
authorwenzelm
Tue Oct 18 17:59:25 2005 +0200 (2005-10-18)
changeset 1789262c397c17d18
parent 17891 7a6c4d60a913
child 17893 aef5a6d11c2a
Simplifier.theory_context;
TFL/rules.ML
src/FOL/simpdata.ML
src/HOL/Import/shuffler.ML
src/HOL/Prolog/HOHH.ML
src/HOL/Tools/record_package.ML
src/HOL/simpdata.ML
src/Provers/Arith/fast_lin_arith.ML
src/Pure/tactic.ML
src/Sequents/simpdata.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/TFL/rules.ML	Tue Oct 18 17:59:24 2005 +0200
     1.2 +++ b/TFL/rules.ML	Tue Oct 18 17:59:25 2005 +0200
     1.3 @@ -664,7 +664,8 @@
     1.4  
     1.5  fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
     1.6   let val globals = func::G
     1.7 -     val pbeta_reduce = simpl_conv empty_ss [split_conv RS eq_reflection];
     1.8 +     val ss0 = Simplifier.theory_context (Thm.theory_of_thm th) empty_ss
     1.9 +     val pbeta_reduce = simpl_conv ss0 [split_conv RS eq_reflection];
    1.10       val tc_list = ref[]: term list ref
    1.11       val dummy = term_ref := []
    1.12       val dummy = thm_ref  := []
    1.13 @@ -805,7 +806,7 @@
    1.14      val ctm = cprop_of th
    1.15      val names = add_term_names (term_of ctm, [])
    1.16      val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
    1.17 -      (prover names) (empty_ss addsimps [cut_lemma'] addeqcongs congs) ctm
    1.18 +      (prover names) (ss0 addsimps [cut_lemma'] addeqcongs congs) ctm
    1.19      val th2 = equal_elim th1 th
    1.20   in
    1.21   (th2, List.filter (not o restricted) (!tc_list))
     2.1 --- a/src/FOL/simpdata.ML	Tue Oct 18 17:59:24 2005 +0200
     2.2 +++ b/src/FOL/simpdata.ML	Tue Oct 18 17:59:25 2005 +0200
     2.3 @@ -330,7 +330,8 @@
     2.4                                   eq_assume_tac, ematch_tac [FalseE]];
     2.5  
     2.6  (*No simprules, but basic infastructure for simplification*)
     2.7 -val FOL_basic_ss = empty_ss
     2.8 +val FOL_basic_ss =
     2.9 +  Simplifier.theory_context (the_context ()) empty_ss
    2.10    setsubgoaler asm_simp_tac
    2.11    setSSolver (mk_solver "FOL safe" safe_solver)
    2.12    setSolver (mk_solver "FOL unsafe" unsafe_solver)
     3.1 --- a/src/HOL/Import/shuffler.ML	Tue Oct 18 17:59:24 2005 +0200
     3.2 +++ b/src/HOL/Import/shuffler.ML	Tue Oct 18 17:59:25 2005 +0200
     3.3 @@ -490,8 +490,9 @@
     3.4  	val sg = sign_of thy
     3.5  
     3.6  	val norms = ShuffleData.get thy
     3.7 -	val ss = empty_ss setmksimps single
     3.8 -			  addsimps (map (Thm.transfer sg) norms)
     3.9 +	val ss = Simplifier.theory_context thy empty_ss
    3.10 +          setmksimps single
    3.11 +	  addsimps (map (Thm.transfer sg) norms)
    3.12  	fun chain f th =
    3.13  	    let
    3.14                  val rhs = snd (dest_equals (cprop_of th))
     4.1 --- a/src/HOL/Prolog/HOHH.ML	Tue Oct 18 17:59:24 2005 +0200
     4.2 +++ b/src/HOL/Prolog/HOHH.ML	Tue Oct 18 17:59:25 2005 +0200
     4.3 @@ -54,7 +54,10 @@
     4.4      | _                             => [thm]
     4.5  in map zero_var_indexes (at thm) end;
     4.6  
     4.7 -val atomize_ss = empty_ss setmksimps (mksimps mksimps_pairs) addsimps [
     4.8 +val atomize_ss =
     4.9 +  Simplifier.theory_context (the_context ()) empty_ss
    4.10 +  setmksimps (mksimps mksimps_pairs)
    4.11 +  addsimps [
    4.12          all_conj_distrib, (* "(! x. P x & Q x) = ((! x. P x) & (! x. Q x))" *)
    4.13          imp_conjL RS sym, (* "(D :- G1 :- G2) = (D :- G1 & G2)" *)
    4.14          imp_conjR,        (* "(D1 & D2 :- G) = ((D1 :- G) & (D2 :- G))" *)
     5.1 --- a/src/HOL/Tools/record_package.ML	Tue Oct 18 17:59:24 2005 +0200
     5.2 +++ b/src/HOL/Tools/record_package.ML	Tue Oct 18 17:59:25 2005 +0200
     5.3 @@ -317,7 +317,7 @@
     5.4  
     5.5  val is_selector = Symtab.defined o #selectors o get_sel_upd;
     5.6  val get_updates = Symtab.lookup o #updates o get_sel_upd;
     5.7 -val get_simpset = #simpset o get_sel_upd;
     5.8 +fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
     5.9  
    5.10  fun put_sel_upd names simps thy =
    5.11    let
    5.12 @@ -1119,8 +1119,6 @@
    5.13  fun record_split_simp_tac thms P i st =
    5.14    let
    5.15      val sg = Thm.sign_of_thm st;
    5.16 -    val {sel_upd={simpset,...},...}
    5.17 -            = RecordsData.get sg;
    5.18  
    5.19      val has_rec = exists_Const
    5.20        (fn (s, Type (_, [Type (_, [T, _]), _])) =>
    5.21 @@ -1158,7 +1156,7 @@
    5.22      val simprocs = if has_rec goal then [record_split_simproc P] else [];
    5.23  
    5.24    in st |> ((EVERY split_frees_tacs)
    5.25 -           THEN (Simplifier.full_simp_tac (simpset addsimps thms addsimprocs simprocs) i))
    5.26 +           THEN (Simplifier.full_simp_tac (get_simpset sg addsimps thms addsimprocs simprocs) i))
    5.27    end handle Empty => Seq.empty;
    5.28  end;
    5.29  
     6.1 --- a/src/HOL/simpdata.ML	Tue Oct 18 17:59:24 2005 +0200
     6.2 +++ b/src/HOL/simpdata.ML	Tue Oct 18 17:59:25 2005 +0200
     6.3 @@ -341,7 +341,8 @@
     6.4  val safe_solver = mk_solver "HOL safe" safe_solver_tac;
     6.5  
     6.6  val HOL_basic_ss =
     6.7 -  empty_ss setsubgoaler asm_simp_tac
     6.8 +  Simplifier.theory_context (the_context ()) empty_ss
     6.9 +    setsubgoaler asm_simp_tac
    6.10      setSSolver safe_solver
    6.11      setSolver unsafe_solver
    6.12      setmksimps (mksimps mksimps_pairs)
    6.13 @@ -460,14 +461,13 @@
    6.14  *)
    6.15  
    6.16  local
    6.17 -  val nnf_simps =
    6.18 -        [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
    6.19 -         not_all,not_ex,not_not];
    6.20    val nnf_simpset =
    6.21 -        empty_ss setmkeqTrue mk_eq_True
    6.22 -                 setmksimps (mksimps mksimps_pairs)
    6.23 -                 addsimps nnf_simps;
    6.24 -  val prem_nnf_tac = full_simp_tac nnf_simpset
    6.25 +    empty_ss setmkeqTrue mk_eq_True
    6.26 +    setmksimps (mksimps mksimps_pairs)
    6.27 +    addsimps [imp_conv_disj,iff_conv_conj_imp,de_Morgan_disj,de_Morgan_conj,
    6.28 +      not_all,not_ex,not_not];
    6.29 +  fun prem_nnf_tac i st =
    6.30 +    full_simp_tac (Simplifier.theory_context (Thm.theory_of_thm st) nnf_simpset) i st;
    6.31  in
    6.32  fun refute_tac test prep_tac ref_tac =
    6.33    let val refute_prems_tac =
     7.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 18 17:59:24 2005 +0200
     7.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Tue Oct 18 17:59:25 2005 +0200
     7.3 @@ -79,7 +79,7 @@
     7.4    val trace           : bool ref
     7.5    val fast_arith_neq_limit: int ref
     7.6    val lin_arith_prover: theory -> simpset -> term -> thm option
     7.7 -  val     lin_arith_tac:     bool -> int -> tactic
     7.8 +  val     lin_arith_tac:    bool -> int -> tactic
     7.9    val cut_lin_arith_tac: simpset -> int -> tactic
    7.10  end;
    7.11  
    7.12 @@ -665,7 +665,9 @@
    7.13       | SOME js => (trace_msg "Refutation succeeded."; refute_tac ss (i,js))
    7.14    end) i st;
    7.15  
    7.16 -val lin_arith_tac = simpset_lin_arith_tac Simplifier.empty_ss;
    7.17 +fun lin_arith_tac ex i st =
    7.18 +  simpset_lin_arith_tac (Simplifier.theory_context (Thm.theory_of_thm st) Simplifier.empty_ss)
    7.19 +    ex i st;
    7.20  
    7.21  fun cut_lin_arith_tac ss i =
    7.22    cut_facts_tac (Simplifier.prems_of_ss ss) i THEN
     8.1 --- a/src/Pure/tactic.ML	Tue Oct 18 17:59:24 2005 +0200
     8.2 +++ b/src/Pure/tactic.ML	Tue Oct 18 17:59:25 2005 +0200
     8.3 @@ -535,8 +535,10 @@
     8.4  val rewrite_goals_rule = MetaSimplifier.rewrite_goals_rule_aux simple_prover;
     8.5  
     8.6  fun rewrite_goal_tac rews =
     8.7 -  MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac)
     8.8 -    (MetaSimplifier.empty_ss addsimps rews);
     8.9 +  let val ss = MetaSimplifier.empty_ss addsimps rews in
    8.10 +    fn i => fn st => MetaSimplifier.asm_rewrite_goal_tac (true, false, false) (K no_tac)
    8.11 +      (MetaSimplifier.theory_context (Thm.theory_of_thm st) ss) i st
    8.12 +  end;
    8.13  
    8.14  (*Rewrite throughout proof state. *)
    8.15  fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs);
     9.1 --- a/src/Sequents/simpdata.ML	Tue Oct 18 17:59:24 2005 +0200
     9.2 +++ b/src/Sequents/simpdata.ML	Tue Oct 18 17:59:25 2005 +0200
     9.3 @@ -235,7 +235,8 @@
     9.4  
     9.5  (*No simprules, but basic infrastructure for simplification*)
     9.6  val LK_basic_ss =
     9.7 -  empty_ss setsubgoaler asm_simp_tac
     9.8 +  Simplifier.theory_context (the_context ()) empty_ss
     9.9 +    setsubgoaler asm_simp_tac
    9.10      setSSolver (mk_solver "safe" safe_solver)
    9.11      setSolver (mk_solver "unsafe" unsafe_solver)
    9.12      setmksimps (map mk_meta_eq o atomize o gen_all)
    10.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Oct 18 17:59:24 2005 +0200
    10.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Oct 18 17:59:25 2005 +0200
    10.3 @@ -339,7 +339,7 @@
    10.4  
    10.5       (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
    10.6         If the premises get simplified, then the proofs could fail.*)
    10.7 -     val min_ss = empty_ss
    10.8 +     val min_ss = Simplifier.theory_context thy empty_ss
    10.9             setmksimps (map mk_eq o ZF_atomize o gen_all)
   10.10             setSolver (mk_solver "minimal"
   10.11                        (fn prems => resolve_tac (triv_rls@prems)