src/Pure/raw_simplifier.ML
changeset 52091 9ec2d47de6a7
parent 52082 559e1398b70e
child 52232 a2d4ae3e04a2
     1.1 --- a/src/Pure/raw_simplifier.ML	Mon May 20 20:47:33 2013 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Mon May 20 20:49:10 2013 +0200
     1.3 @@ -510,10 +510,6 @@
     1.4  fun add_prems ths =
     1.5    map_simpset1 (fn (rules, prems, bounds, depth) => (rules, ths @ prems, bounds, depth));
     1.6  
     1.7 -fun activate_context thy ctxt = ctxt  (* FIXME ?? *)
     1.8 -  |> Context.raw_transfer (Theory.merge (thy, Proof_Context.theory_of ctxt))
     1.9 -  |> Context_Position.set_visible false;
    1.10 -
    1.11  
    1.12  (* maintain simp rules *)
    1.13  
    1.14 @@ -545,7 +541,6 @@
    1.15  
    1.16  fun decomp_simp thm =
    1.17    let
    1.18 -    val thy = Thm.theory_of_thm thm;
    1.19      val prop = Thm.prop_of thm;
    1.20      val prems = Logic.strip_imp_prems prop;
    1.21      val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
    1.22 @@ -557,12 +552,12 @@
    1.23        var_perm (term_of elhs, erhs) andalso
    1.24        not (term_of elhs aconv erhs) andalso
    1.25        not (is_Var (term_of elhs));
    1.26 -  in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
    1.27 +  in (prems, term_of lhs, elhs, term_of rhs, perm) end;
    1.28  
    1.29  end;
    1.30  
    1.31  fun decomp_simp' thm =
    1.32 -  let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
    1.33 +  let val (_, lhs, _, rhs, _) = decomp_simp thm in
    1.34      if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
    1.35      else (lhs, rhs)
    1.36    end;
    1.37 @@ -572,7 +567,7 @@
    1.38      (case mk_eq_True ctxt thm of
    1.39        NONE => []
    1.40      | SOME eq_True =>
    1.41 -        let val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
    1.42 +        let val (_, lhs, elhs, _, _) = decomp_simp eq_True;
    1.43          in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end)
    1.44    end;
    1.45  
    1.46 @@ -586,7 +581,7 @@
    1.47    end;
    1.48  
    1.49  fun mk_rrule ctxt (thm, name) =
    1.50 -  let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
    1.51 +  let val (prems, lhs, elhs, rhs, perm) = decomp_simp thm in
    1.52      if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
    1.53      else
    1.54        (*weak test for loops*)
    1.55 @@ -597,7 +592,7 @@
    1.56  
    1.57  fun orient_rrule ctxt (thm, name) =
    1.58    let
    1.59 -    val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
    1.60 +    val (prems, lhs, elhs, rhs, perm) = decomp_simp thm;
    1.61      val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = simpset_of ctxt;
    1.62    in
    1.63      if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
    1.64 @@ -608,7 +603,7 @@
    1.65          (case mk_sym ctxt thm of
    1.66            NONE => []
    1.67          | SOME thm' =>
    1.68 -            let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
    1.69 +            let val (_, lhs', elhs', rhs', _) = decomp_simp thm'
    1.70              in rrule_eq_True ctxt thm' name lhs' elhs' rhs' thm end)
    1.71      else rrule_eq_True ctxt thm name lhs elhs rhs thm
    1.72    end;
    1.73 @@ -886,7 +881,7 @@
    1.74  (* mk_procrule *)
    1.75  
    1.76  fun mk_procrule ctxt thm =
    1.77 -  let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
    1.78 +  let val (prems, lhs, elhs, rhs, _) = decomp_simp thm in
    1.79      if rewrite_rule_extra_vars prems lhs rhs
    1.80      then (cond_warn_thm ctxt (fn () => "Extra vars on rhs:") thm; [])
    1.81      else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
    1.82 @@ -934,7 +929,7 @@
    1.83    IMPORTANT: rewrite rules must not introduce new Vars or TVars!
    1.84  *)
    1.85  
    1.86 -fun rewritec (prover, thyt, maxt) ctxt t =
    1.87 +fun rewritec (prover, maxt) ctxt t =
    1.88    let
    1.89      val Simpset ({rules, ...}, {congs, procs, termless, ...}) = simpset_of ctxt;
    1.90      val eta_thm = Thm.eta_conversion t;
    1.91 @@ -1007,7 +1002,7 @@
    1.92  
    1.93      fun proc_rews [] = NONE
    1.94        | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
    1.95 -          if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
    1.96 +          if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then
    1.97              (debug_term ctxt false (fn () => "Trying procedure " ^ quote name ^ " on:") eta_t;
    1.98               case proc ctxt eta_t' of
    1.99                 NONE => (debug ctxt false (fn () => "FAILED"); proc_rews ps)
   1.100 @@ -1063,20 +1058,20 @@
   1.101  fun transitive2 thm = transitive1 (SOME thm);
   1.102  fun transitive3 thm = transitive1 thm o SOME;
   1.103  
   1.104 -fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
   1.105 +fun bottomc ((simprem, useprem, mutsimp), prover, maxidx) =
   1.106    let
   1.107      fun botc skel ctxt t =
   1.108            if is_Var skel then NONE
   1.109            else
   1.110            (case subc skel ctxt t of
   1.111               some as SOME thm1 =>
   1.112 -               (case rewritec (prover, thy, maxidx) ctxt (Thm.rhs_of thm1) of
   1.113 +               (case rewritec (prover, maxidx) ctxt (Thm.rhs_of thm1) of
   1.114                    SOME (thm2, skel2) =>
   1.115                      transitive2 (Thm.transitive thm1 thm2)
   1.116                        (botc skel2 ctxt (Thm.rhs_of thm2))
   1.117                  | NONE => some)
   1.118             | NONE =>
   1.119 -               (case rewritec (prover, thy, maxidx) ctxt t of
   1.120 +               (case rewritec (prover, maxidx) ctxt t of
   1.121                    SOME (thm2, skel2) => transitive2 thm2
   1.122                      (botc skel2 ctxt (Thm.rhs_of thm2))
   1.123                  | NONE => NONE))
   1.124 @@ -1197,7 +1192,7 @@
   1.125                Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
   1.126              val dprem = Option.map (disch false prem)
   1.127            in
   1.128 -            (case rewritec (prover, thy, maxidx) ctxt' concl' of
   1.129 +            (case rewritec (prover, maxidx) ctxt' concl' of
   1.130                NONE => rebuild prems concl' rrss asms ctxt (dprem eq)
   1.131              | SOME (eq', _) => transitive2 (fold (disch false)
   1.132                    prems (the (transitive3 (dprem eq) eq')))
   1.133 @@ -1305,10 +1300,18 @@
   1.134  
   1.135  fun rewrite_cterm mode prover raw_ctxt raw_ct =
   1.136    let
   1.137 -    val thy = Thm.theory_of_cterm raw_ct;
   1.138 +    val ctxt =
   1.139 +      raw_ctxt
   1.140 +      |> Context_Position.set_visible false
   1.141 +      |> inc_simp_depth;
   1.142 +    val thy = Proof_Context.theory_of ctxt;
   1.143 +
   1.144      val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
   1.145      val {maxidx, ...} = Thm.rep_cterm ct;
   1.146 -    val ctxt = inc_simp_depth (activate_context thy raw_ctxt);
   1.147 +    val _ =
   1.148 +      Theory.subthy (theory_of_cterm ct, thy) orelse
   1.149 +        raise CTERM ("rewrite_cterm: bad background theory", [ct]);
   1.150 +
   1.151      val depth = simp_depth ctxt;
   1.152      val _ =
   1.153        if depth mod 20 = 0 then
   1.154 @@ -1316,7 +1319,7 @@
   1.155        else ();
   1.156      val _ = trace_cterm ctxt false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ct;
   1.157      val _ = check_bounds ctxt ct;
   1.158 -  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ctxt ct end;
   1.159 +  in bottomc (mode, Option.map Drule.flexflex_unique oo prover, maxidx) ctxt ct end;
   1.160  
   1.161  val simple_prover =
   1.162    SINGLE o (fn ctxt => ALLGOALS (resolve_tac (prems_of ctxt)));