src/Pure/meta_simplifier.ML
changeset 16458 4c6fd0c01d28
parent 16380 019ec70774ff
child 16665 b75568de32c6
     1.1 --- a/src/Pure/meta_simplifier.ML	Fri Jun 17 18:33:42 2005 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Fri Jun 17 18:35:27 2005 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4    val merge_ss: simpset * simpset -> simpset
     1.5    type simproc
     1.6    val mk_simproc: string -> cterm list ->
     1.7 -    (Sign.sg -> simpset -> term -> thm option) -> simproc
     1.8 +    (theory -> simpset -> term -> thm option) -> simproc
     1.9    val add_prems: thm list -> simpset -> simpset
    1.10    val prems_of_ss: simpset -> thm list
    1.11    val addsimps: simpset * thm list -> simpset
    1.12 @@ -75,15 +75,15 @@
    1.13    exception SIMPLIFIER of string * thm
    1.14    val clear_ss: simpset -> simpset
    1.15    exception SIMPROC_FAIL of string * exn
    1.16 -  val simproc_i: Sign.sg -> string -> term list
    1.17 -    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
    1.18 -  val simproc: Sign.sg -> string -> string list
    1.19 -    -> (Sign.sg -> simpset -> term -> thm option) -> simproc
    1.20 +  val simproc_i: theory -> string -> term list
    1.21 +    -> (theory -> simpset -> term -> thm option) -> simproc
    1.22 +  val simproc: theory -> string -> string list
    1.23 +    -> (theory -> simpset -> term -> thm option) -> simproc
    1.24    val rewrite_cterm: bool * bool * bool ->
    1.25      (simpset -> thm -> thm option) -> simpset -> cterm -> thm
    1.26    val rewrite_aux: (simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm
    1.27    val simplify_aux: (simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm
    1.28 -  val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term
    1.29 +  val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
    1.30    val rewrite_thm: bool * bool * bool ->
    1.31      (simpset -> thm -> thm option) -> simpset -> thm -> thm
    1.32    val rewrite_goals_rule_aux: (simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.33 @@ -116,7 +116,7 @@
    1.34    else tracing (enclose "[" "]" (string_of_int(!simp_depth)) ^ a);
    1.35  
    1.36  fun prnt warn a = if warn then warning a else println a;
    1.37 -fun prtm warn a sg t = prnt warn (a ^ "\n" ^ Sign.string_of_term sg t);
    1.38 +fun prtm warn a thy t = prnt warn (a ^ "\n" ^ Sign.string_of_term thy t);
    1.39  fun prctm warn a t = prnt warn (a ^ "\n" ^ Display.string_of_cterm t);
    1.40  
    1.41  in
    1.42 @@ -124,8 +124,8 @@
    1.43  fun debug warn a = if ! debug_simp then prnt warn a else ();
    1.44  fun trace warn a = if ! trace_simp then prnt warn a else ();
    1.45  
    1.46 -fun debug_term warn a sign t = if ! debug_simp then prtm warn a sign t else ();
    1.47 -fun trace_term warn a sign t = if ! trace_simp then prtm warn a sign t else ();
    1.48 +fun debug_term warn a thy t = if ! debug_simp then prtm warn a thy t else ();
    1.49 +fun trace_term warn a thy t = if ! trace_simp then prtm warn a thy t else ();
    1.50  fun trace_cterm warn a ct = if ! trace_simp then prctm warn a ct else ();
    1.51  fun trace_thm a th = if ! trace_simp then prctm false a (Thm.cprop_of th) else ();
    1.52  
    1.53 @@ -231,7 +231,7 @@
    1.54    Proc of
    1.55     {name: string,
    1.56      lhs: cterm,
    1.57 -    proc: Sign.sg -> simpset -> term -> thm option,
    1.58 +    proc: theory -> simpset -> term -> thm option,
    1.59      id: stamp};
    1.60  
    1.61  fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = (id1 = id2);
    1.62 @@ -354,8 +354,8 @@
    1.63        Proc {name = name, lhs = lhs, proc = proc, id = id}))
    1.64    end;
    1.65  
    1.66 -fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg o Logic.varify);
    1.67 -fun simproc sg name = simproc_i sg name o map (Sign.simple_read_term sg TypeInfer.logicT);
    1.68 +fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
    1.69 +fun simproc thy name = simproc_i thy name o map (Sign.simple_read_term thy TypeInfer.logicT);
    1.70  
    1.71  
    1.72  
    1.73 @@ -407,7 +407,7 @@
    1.74    not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems)));
    1.75  
    1.76  (*simple test for looping rewrite rules and stupid orientations*)
    1.77 -fun reorient sign prems lhs rhs =
    1.78 +fun reorient thy prems lhs rhs =
    1.79    rewrite_rule_extra_vars prems lhs rhs
    1.80      orelse
    1.81    is_Var (head_of lhs)
    1.82 @@ -420,7 +420,7 @@
    1.83  *)
    1.84    exists (apl (lhs, Logic.occs)) (rhs :: prems)
    1.85      orelse
    1.86 -  null prems andalso Pattern.matches (Sign.tsig_of sign) (lhs, rhs)
    1.87 +  null prems andalso Pattern.matches (Sign.tsig_of thy) (lhs, rhs)
    1.88      (*the condition "null prems" is necessary because conditional rewrites
    1.89        with extra variables in the conditions may terminate although
    1.90        the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
    1.91 @@ -429,7 +429,7 @@
    1.92  
    1.93  fun decomp_simp thm =
    1.94    let
    1.95 -    val {sign, prop, ...} = Thm.rep_thm thm;
    1.96 +    val {thy, prop, ...} = Thm.rep_thm thm;
    1.97      val prems = Logic.strip_imp_prems prop;
    1.98      val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
    1.99      val (lhs, rhs) = Drule.dest_equals concl handle TERM _ =>
   1.100 @@ -441,7 +441,7 @@
   1.101        var_perm (term_of elhs, erhs) andalso
   1.102        not (term_of elhs aconv erhs) andalso
   1.103        not (is_Var (term_of elhs));
   1.104 -  in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end;
   1.105 +  in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
   1.106  
   1.107  fun decomp_simp' thm =
   1.108    let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
   1.109 @@ -476,10 +476,10 @@
   1.110    end;
   1.111  
   1.112  fun orient_rrule ss (thm, name) =
   1.113 -  let val (sign, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
   1.114 +  let val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
   1.115      if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
   1.116 -    else if reorient sign prems lhs rhs then
   1.117 -      if reorient sign prems rhs lhs
   1.118 +    else if reorient thy prems lhs rhs then
   1.119 +      if reorient thy prems rhs lhs
   1.120        then mk_eq_True ss (thm, name)
   1.121        else
   1.122          let val Simpset (_, {mk_rews = {mk_sym, ...}, ...}) = ss in
   1.123 @@ -718,9 +718,9 @@
   1.124        (symmetric (Drule.beta_eta_conversion (lhs_of thm'))) thm')
   1.125    in if msg then trace_thm "SUCCEEDED" thm' else (); SOME thm'' end
   1.126    handle THM _ =>
   1.127 -    let val {sign, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
   1.128 +    let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in
   1.129        trace_thm "Proved wrong thm (Check subgoaler?)" thm';
   1.130 -      trace_term false "Should have proved:" sign prop0;
   1.131 +      trace_term false "Should have proved:" thy prop0;
   1.132        NONE
   1.133      end;
   1.134  
   1.135 @@ -773,16 +773,16 @@
   1.136    IMPORTANT: rewrite rules must not introduce new Vars or TVars!
   1.137  *)
   1.138  
   1.139 -fun rewritec (prover, signt, maxt) ss t =
   1.140 +fun rewritec (prover, thyt, maxt) ss t =
   1.141    let
   1.142      val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
   1.143      val eta_thm = Thm.eta_conversion t;
   1.144      val eta_t' = rhs_of eta_thm;
   1.145      val eta_t = term_of eta_t';
   1.146 -    val tsigt = Sign.tsig_of signt;
   1.147 +    val tsigt = Sign.tsig_of thyt;
   1.148      fun rew {thm, name, lhs, elhs, fo, perm} =
   1.149        let
   1.150 -        val {sign, prop, maxidx, ...} = rep_thm thm;
   1.151 +        val {thy, prop, maxidx, ...} = rep_thm thm;
   1.152          val (rthm, elhs') = if maxt = ~1 then (thm, elhs)
   1.153            else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs);
   1.154          val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t')
   1.155 @@ -837,9 +837,9 @@
   1.156      fun proc_rews [] = NONE
   1.157        | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
   1.158            if Pattern.matches tsigt (Thm.term_of lhs, Thm.term_of t) then
   1.159 -            (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t;
   1.160 +            (debug_term false ("Trying procedure " ^ quote name ^ " on:") thyt eta_t;
   1.161               case transform_failure (curry SIMPROC_FAIL name)
   1.162 -                 (fn () => proc signt ss eta_t) () of
   1.163 +                 (fn () => proc thyt ss eta_t) () of
   1.164                 NONE => (debug false "FAILED"; proc_rews ps)
   1.165               | SOME raw_thm =>
   1.166                   (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm;
   1.167 @@ -859,8 +859,8 @@
   1.168  
   1.169  (* conversion to apply a congruence rule to a term *)
   1.170  
   1.171 -fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t =
   1.172 -  let val sign = Thm.sign_of_thm cong
   1.173 +fun congc (prover,thyt,maxt) {thm=cong,lhs=lhs} t =
   1.174 +  let val thy = Thm.theory_of_thm cong
   1.175        val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong;
   1.176        val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
   1.177        val insts = Thm.cterm_match (rlhs, t)
   1.178 @@ -889,20 +889,20 @@
   1.179  fun transitive2 thm = transitive1 (SOME thm);
   1.180  fun transitive3 thm = transitive1 thm o SOME;
   1.181  
   1.182 -fun bottomc ((simprem, useprem, mutsimp), prover, sign, maxidx) =
   1.183 +fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
   1.184    let
   1.185      fun botc skel ss t =
   1.186            if is_Var skel then NONE
   1.187            else
   1.188            (case subc skel ss t of
   1.189               some as SOME thm1 =>
   1.190 -               (case rewritec (prover, sign, maxidx) ss (rhs_of thm1) of
   1.191 +               (case rewritec (prover, thy, maxidx) ss (rhs_of thm1) of
   1.192                    SOME (thm2, skel2) =>
   1.193                      transitive2 (transitive thm1 thm2)
   1.194                        (botc skel2 ss (rhs_of thm2))
   1.195                  | NONE => some)
   1.196             | NONE =>
   1.197 -               (case rewritec (prover, sign, maxidx) ss t of
   1.198 +               (case rewritec (prover, thy, maxidx) ss t of
   1.199                    SOME (thm2, skel2) => transitive2 thm2
   1.200                      (botc skel2 ss (rhs_of thm2))
   1.201                  | NONE => NONE))
   1.202 @@ -957,7 +957,7 @@
   1.203    (*post processing: some partial applications h t1 ... tj, j <= length ts,
   1.204      may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
   1.205                            (let
   1.206 -                             val thm = congc (prover ss, sign, maxidx) cong t0;
   1.207 +                             val thm = congc (prover ss, thy, maxidx) cong t0;
   1.208                               val t = getOpt (Option.map rhs_of thm, t0);
   1.209                               val (cl, cr) = Thm.dest_comb t
   1.210                               val dVar = Var(("", 0), dummyT)
   1.211 @@ -1012,7 +1012,7 @@
   1.212              val concl' =
   1.213                Drule.mk_implies (prem, getOpt (Option.map rhs_of eq, concl));
   1.214              val dprem = Option.map (curry (disch false) prem)
   1.215 -          in case rewritec (prover, sign, maxidx) ss' concl' of
   1.216 +          in case rewritec (prover, thy, maxidx) ss' concl' of
   1.217                NONE => rebuild prems concl' rrss asms ss (dprem eq)
   1.218              | SOME (eq', _) => transitive2 (Library.foldl (disch false o swap)
   1.219                    (valOf (transitive3 (dprem eq) eq'), prems))
   1.220 @@ -1096,8 +1096,8 @@
   1.221     then warning ("Simplification depth " ^ string_of_int (!simp_depth))
   1.222     else ();
   1.223     trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct;
   1.224 -   let val {sign, t, maxidx, ...} = Thm.rep_cterm ct
   1.225 -       val res = bottomc (mode, prover, sign, maxidx) ss ct
   1.226 +   let val {thy, t, maxidx, ...} = Thm.rep_cterm ct
   1.227 +       val res = bottomc (mode, prover, thy, maxidx) ss ct
   1.228           handle THM (s, _, thms) =>
   1.229           error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^
   1.230             Pretty.string_of (Display.pretty_thms thms))
   1.231 @@ -1115,8 +1115,8 @@
   1.232        Drule.fconv_rule (rewrite_cterm (full, false, false) prover (empty_ss addsimps thms));
   1.233  
   1.234  (*simple term rewriting -- no proof*)
   1.235 -fun rewrite_term sg rules procs =
   1.236 -  Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs;
   1.237 +fun rewrite_term thy rules procs =
   1.238 +  Pattern.rewrite_term (Sign.tsig_of thy) (map decomp_simp' rules) procs;
   1.239  
   1.240  fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss);
   1.241