Replaced list of bound variables in simpset by maximal index of bound
authorberghofe
Mon Oct 18 11:43:40 2004 +0200 (2004-10-18)
changeset 152490da6b3075bfa
parent 15248 b436486091a6
child 15250 217bececa2bd
Replaced list of bound variables in simpset by maximal index of bound
variables. This allows new variable names to be generated more quickly
(without calling variant).
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Fri Oct 15 18:49:16 2004 +0200
     1.2 +++ b/src/Pure/meta_simplifier.ML	Mon Oct 18 11:43:40 2004 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4    val rep_ss: simpset ->
     1.5     {rules: rrule Net.net,
     1.6      prems: thm list,
     1.7 -    bounds: string list,
     1.8 +    bounds: int,
     1.9      depth: int} *
    1.10     {congs: (string * cong) list * string list,
    1.11      procs: proc Net.net,
    1.12 @@ -193,7 +193,7 @@
    1.13  (*A simpset contains data required during conversion:
    1.14      rules: discrimination net of rewrite rules;
    1.15      prems: current premises;
    1.16 -    bounds: names of bound variables already used
    1.17 +    bounds: maximal index of bound variables already used
    1.18        (for generating new names when rewriting under lambda abstractions);
    1.19      depth: depth of conditional rewriting;
    1.20      congs: association list of congruence rules and
    1.21 @@ -218,7 +218,7 @@
    1.22    Simpset of
    1.23     {rules: rrule Net.net,
    1.24      prems: thm list,
    1.25 -    bounds: string list,
    1.26 +    bounds: int,
    1.27      depth: int} *
    1.28     {congs: (string * cong) list * string list,
    1.29      procs: proc Net.net,
    1.30 @@ -297,7 +297,7 @@
    1.31  local
    1.32  
    1.33  fun init_ss mk_rews termless subgoal_tac solvers =
    1.34 -  make_simpset ((Net.empty, [], [], 0),
    1.35 +  make_simpset ((Net.empty, [], 0, 0),
    1.36      (([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
    1.37  
    1.38  val basic_mk_rews: mk_rews =
    1.39 @@ -329,7 +329,7 @@
    1.40  
    1.41      val rules' = Net.merge (rules1, rules2, eq_rrule);
    1.42      val prems' = gen_merge_lists Drule.eq_thm_prop prems1 prems2;
    1.43 -    val bounds' = merge_lists bounds1 bounds2;
    1.44 +    val bounds' = Int.max (bounds1, bounds2);
    1.45      val congs' = gen_merge_lists (eq_cong o pairself #2) congs1 congs2;
    1.46      val weak' = merge_lists weak1 weak2;
    1.47      val procs' = Net.merge (procs1, procs2, eq_proc);
    1.48 @@ -363,8 +363,8 @@
    1.49  
    1.50  (* bounds and prems *)
    1.51  
    1.52 -fun add_bound b = map_simpset1 (fn (rules, prems, bounds, depth) =>
    1.53 -  (rules, prems, b :: bounds, depth));
    1.54 +val incr_bounds = map_simpset1 (fn (rules, prems, bounds, depth) =>
    1.55 +  (rules, prems, bounds + 1, depth));
    1.56  
    1.57  fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth) =>
    1.58    (rules, ths @ prems, bounds, depth));
    1.59 @@ -928,9 +928,8 @@
    1.60         (case term_of t0 of
    1.61             Abs (a, T, t) =>
    1.62               let
    1.63 -                 val b = variant bounds a;
    1.64 -                 val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0;
    1.65 -                 val ss' = add_bound b ss;
    1.66 +                 val (v, t') = Thm.dest_abs (Some ("." ^ a ^ "." ^ string_of_int bounds)) t0;
    1.67 +                 val ss' = incr_bounds ss;
    1.68                   val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
    1.69               in case botc skel' ss' t' of
    1.70                    Some thm => Some (abstract_rule a v thm)