src/HOL/HOL.thy
changeset 51717 9e7d1c139569
parent 51692 ecd34f863242
child 51798 ad3a241def73
     1.1 --- a/src/HOL/HOL.thy	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -1189,7 +1189,7 @@
     1.4  ML_file "Tools/simpdata.ML"
     1.5  ML {* open Simpdata *}
     1.6  
     1.7 -setup {* Simplifier.map_simpset_global (K HOL_basic_ss) *}
     1.8 +setup {* map_theory_simpset (put_simpset HOL_basic_ss) *}
     1.9  
    1.10  simproc_setup defined_Ex ("EX x. P x") = {* fn _ => Quantifier1.rearrange_ex *}
    1.11  simproc_setup defined_All ("ALL x. P x") = {* fn _ => Quantifier1.rearrange_all *}
    1.12 @@ -1241,10 +1241,9 @@
    1.13     case t
    1.14      of Abs (_, _, t') => count_loose t' 0 <= 1
    1.15       | _ => true;
    1.16 -in fn _ => fn ss => fn ct => if is_trivial_let (Thm.term_of ct)
    1.17 +in fn _ => fn ctxt => fn ct => if is_trivial_let (Thm.term_of ct)
    1.18    then SOME @{thm Let_def} (*no or one ocurrence of bound variable*)
    1.19    else let (*Norbert Schirmer's case*)
    1.20 -    val ctxt = Simplifier.the_context ss;
    1.21      val thy = Proof_Context.theory_of ctxt;
    1.22      val t = Thm.term_of ct;
    1.23      val ([t'], ctxt') = Variable.import_terms false [t] ctxt;
    1.24 @@ -1258,7 +1257,7 @@
    1.25            val cx = cterm_of thy x;
    1.26            val {T = xT, ...} = rep_cterm cx;
    1.27            val cf = cterm_of thy f;
    1.28 -          val fx_g = Simplifier.rewrite ss (Thm.apply cf cx);
    1.29 +          val fx_g = Simplifier.rewrite ctxt (Thm.apply cf cx);
    1.30            val (_ $ _ $ g) = prop_of fx_g;
    1.31            val g' = abstract_over (x,g);
    1.32            val abs_g'= Abs (n,xT,g');
    1.33 @@ -1345,7 +1344,7 @@
    1.34  lemmas [cong] = imp_cong simp_implies_cong
    1.35  lemmas [split] = split_if
    1.36  
    1.37 -ML {* val HOL_ss = @{simpset} *}
    1.38 +ML {* val HOL_ss = simpset_of @{context} *}
    1.39  
    1.40  text {* Simplifies x assuming c and y assuming ~c *}
    1.41  lemma if_cong:
    1.42 @@ -1482,13 +1481,13 @@
    1.43      addsimprocs
    1.44        [Simplifier.simproc_global @{theory} "swap_induct_false"
    1.45           ["induct_false ==> PROP P ==> PROP Q"]
    1.46 -         (fn _ => fn _ =>
    1.47 +         (fn _ =>
    1.48              (fn _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>
    1.49                    if P <> Q then SOME Drule.swap_prems_eq else NONE
    1.50                | _ => NONE)),
    1.51         Simplifier.simproc_global @{theory} "induct_equal_conj_curry"
    1.52           ["induct_conj P Q ==> PROP R"]
    1.53 -         (fn _ => fn _ =>
    1.54 +         (fn _ =>
    1.55              (fn _ $ (_ $ P) $ _ =>
    1.56                  let
    1.57                    fun is_conj (@{const induct_conj} $ P $ Q) =
    1.58 @@ -1583,7 +1582,7 @@
    1.59  signature REORIENT_PROC =
    1.60  sig
    1.61    val add : (term -> bool) -> theory -> theory
    1.62 -  val proc : morphism -> simpset -> cterm -> thm option
    1.63 +  val proc : morphism -> Proof.context -> cterm -> thm option
    1.64  end;
    1.65  
    1.66  structure Reorient_Proc : REORIENT_PROC =
    1.67 @@ -1599,9 +1598,8 @@
    1.68    fun matches thy t = exists (fn (m, _) => m t) (Data.get thy);
    1.69  
    1.70    val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
    1.71 -  fun proc phi ss ct =
    1.72 +  fun proc phi ctxt ct =
    1.73      let
    1.74 -      val ctxt = Simplifier.the_context ss;
    1.75        val thy = Proof_Context.theory_of ctxt;
    1.76      in
    1.77        case Thm.term_of ct of
    1.78 @@ -1701,9 +1699,9 @@
    1.79  subsubsection {* Generic code generator preprocessor setup *}
    1.80  
    1.81  setup {*
    1.82 -  Code_Preproc.map_pre (K HOL_basic_ss)
    1.83 -  #> Code_Preproc.map_post (K HOL_basic_ss)
    1.84 -  #> Code_Simp.map_ss (K HOL_basic_ss)
    1.85 +  Code_Preproc.map_pre (put_simpset HOL_basic_ss)
    1.86 +  #> Code_Preproc.map_post (put_simpset HOL_basic_ss)
    1.87 +  #> Code_Simp.map_ss (put_simpset HOL_basic_ss)
    1.88  *}
    1.89  
    1.90  subsubsection {* Equality *}
    1.91 @@ -1728,10 +1726,9 @@
    1.92  declare eq_equal [code]
    1.93  
    1.94  setup {*
    1.95 -  Code_Preproc.map_pre (fn simpset =>
    1.96 -    simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
    1.97 -      (fn thy => fn _ =>
    1.98 -        fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)])
    1.99 +  Code_Preproc.map_pre (fn ctxt =>
   1.100 +    ctxt addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
   1.101 +      (fn _ => fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)])
   1.102  *}
   1.103  
   1.104  
   1.105 @@ -1994,7 +1991,8 @@
   1.106    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
   1.107  end;
   1.108  
   1.109 -val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms nnf_simps});
   1.110 +fun nnf_conv ctxt =
   1.111 +  Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms nnf_simps});
   1.112  *}
   1.113  
   1.114  hide_const (open) eq equal