tuned;
authorwenzelm
Thu May 30 14:17:56 2013 +0200 (2013-05-30)
changeset 522356aff6b8bec13
parent 52234 6ffcce211047
child 52236 fb82b42eb498
tuned;
src/Tools/eqsubst.ML
     1.1 --- a/src/Tools/eqsubst.ML	Thu May 30 13:59:38 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 14:17:56 2013 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Tools/eqsubst.ML
     1.5      Author:     Lucas Dixon, University of Edinburgh
     1.6  
     1.7 -A proof method to perform a substiution using an equation.
     1.8 +Perform a substitution using an equation.
     1.9  *)
    1.10  
    1.11  signature EQSUBST =
    1.12 @@ -58,16 +58,16 @@
    1.13  
    1.14  
    1.15  type match =
    1.16 -     ((indexname * (sort * typ)) list (* type instantiations *)
    1.17 -      * (indexname * (typ * term)) list) (* term instantiations *)
    1.18 -     * (string * typ) list (* fake named type abs env *)
    1.19 -     * (string * typ) list (* type abs env *)
    1.20 -     * term; (* outer term *)
    1.21 +  ((indexname * (sort * typ)) list (* type instantiations *)
    1.22 +   * (indexname * (typ * term)) list) (* term instantiations *)
    1.23 +  * (string * typ) list (* fake named type abs env *)
    1.24 +  * (string * typ) list (* type abs env *)
    1.25 +  * term; (* outer term *)
    1.26  
    1.27  type searchinfo =
    1.28 -     theory
    1.29 -     * int (* maxidx *)
    1.30 -     * Zipper.T; (* focusterm to search under *)
    1.31 +  theory
    1.32 +  * int (* maxidx *)
    1.33 +  * Zipper.T; (* focusterm to search under *)
    1.34  
    1.35  
    1.36  (* skipping non-empty sub-sequences but when we reach the end
    1.37 @@ -97,10 +97,10 @@
    1.38  fun mk_foo_match mkuptermfunc Ts t =
    1.39    let
    1.40      val ty = Term.type_of t
    1.41 -    val bigtype = (rev (map snd Ts)) ---> ty
    1.42 +    val bigtype = rev (map snd Ts) ---> ty
    1.43      fun mk_foo 0 t = t
    1.44        | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
    1.45 -    val num_of_bnds = (length Ts)
    1.46 +    val num_of_bnds = length Ts
    1.47      (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
    1.48      val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
    1.49    in Abs ("fooabs", bigtype, mkuptermfunc foo_term) end;
    1.50 @@ -121,9 +121,9 @@
    1.51    in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
    1.52  
    1.53  (* before matching we need to fake the bound vars that are missing an
    1.54 -abstraction. In this function we additionally construct the
    1.55 -abstraction environment, and an outer context term (with the focus
    1.56 -abstracted out) for use in rewriting with RWInst.rw *)
    1.57 +   abstraction. In this function we additionally construct the
    1.58 +   abstraction environment, and an outer context term (with the focus
    1.59 +   abstracted out) for use in rewriting with RWInst.rw *)
    1.60  fun prep_zipper_match z =
    1.61    let
    1.62      val t = Zipper.trm z
    1.63 @@ -137,16 +137,16 @@
    1.64  
    1.65  (* Unification with exception handled *)
    1.66  (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
    1.67 -fun clean_unify thry ix (a as (pat, tgt)) =
    1.68 +fun clean_unify thy ix (a as (pat, tgt)) =
    1.69    let
    1.70      (* type info will be re-derived, maybe this can be cached
    1.71         for efficiency? *)
    1.72      val pat_ty = Term.type_of pat;
    1.73      val tgt_ty = Term.type_of tgt;
    1.74 -    (* is it OK to ignore the type instantiation info?
    1.75 +    (* FIXME is it OK to ignore the type instantiation info?
    1.76         or should I be using it? *)
    1.77      val typs_unify =
    1.78 -      SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
    1.79 +      SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix))
    1.80          handle Type.TUNIFY => NONE;
    1.81    in
    1.82      (case typs_unify of
    1.83 @@ -159,7 +159,7 @@
    1.84               Vartab.dest (Envir.term_env env));
    1.85            val initenv =
    1.86              Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
    1.87 -          val useq = Unify.smash_unifiers thry [a] initenv
    1.88 +          val useq = Unify.smash_unifiers thy [a] initenv
    1.89              handle ListPair.UnequalLengths => Seq.empty
    1.90                | Term.TERM _ => Seq.empty;
    1.91            fun clean_unify' useq () =
    1.92 @@ -176,14 +176,13 @@
    1.93  
    1.94  (* Unification for zippers *)
    1.95  (* Note: Ts is a modified version of the original names of the outer
    1.96 -bound variables. New names have been introduced to make sure they are
    1.97 -unique w.r.t all names in the term and each other. usednames' is
    1.98 -oldnames + new names. *)
    1.99 -(* ix = max var index *)
   1.100 -fun clean_unify_z sgn ix pat z =
   1.101 -  let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
   1.102 +   bound variables. New names have been introduced to make sure they are
   1.103 +   unique w.r.t all names in the term and each other. usednames' is
   1.104 +   oldnames + new names. *)
   1.105 +fun clean_unify_z thy maxidx pat z =
   1.106 +  let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in
   1.107      Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
   1.108 -      (clean_unify sgn ix (t, pat))
   1.109 +      (clean_unify thy maxidx (t, pat))
   1.110    end;
   1.111  
   1.112  
   1.113 @@ -229,8 +228,8 @@
   1.114        end;
   1.115    in Zipper.lzy_search sf_valid_td_lr end;
   1.116  
   1.117 -fun searchf_unify_gen f (sgn, maxidx, z) lhs =
   1.118 -  Seq.map (clean_unify_z sgn maxidx lhs) (Zipper.limit_apply f z);
   1.119 +fun searchf_unify_gen f (thy, maxidx, z) lhs =
   1.120 +  Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z);
   1.121  
   1.122  (* search all unifications *)
   1.123  val searchf_lr_unify_all = searchf_unify_gen search_lr_all;
   1.124 @@ -258,15 +257,14 @@
   1.125      val th = Thm.incr_indexes 1 gth;
   1.126      val tgt_term = Thm.prop_of th;
   1.127  
   1.128 -    val sgn = Thm.theory_of_thm th;
   1.129 -    val ctermify = Thm.cterm_of sgn;
   1.130 -    val trivify = Thm.trivial o ctermify;
   1.131 +    val thy = Thm.theory_of_thm th;
   1.132 +    val cert = Thm.cterm_of thy;
   1.133  
   1.134      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
   1.135 -    val cfvs = rev (map ctermify fvs);
   1.136 +    val cfvs = rev (map cert fvs);
   1.137  
   1.138      val conclterm = Logic.strip_imp_concl fixedbody;
   1.139 -    val conclthm = trivify conclterm;
   1.140 +    val conclthm = Thm.trivial (cert conclterm);
   1.141      val maxidx = Thm.maxidx_of th;
   1.142      val ft =
   1.143        (Zipper.move_down_right (* ==> *)
   1.144 @@ -274,7 +272,7 @@
   1.145         o Zipper.mktop
   1.146         o Thm.prop_of) conclthm
   1.147    in
   1.148 -    ((cfvs, conclthm), (sgn, maxidx, ft))
   1.149 +    ((cfvs, conclthm), (thy, maxidx, ft))
   1.150    end;
   1.151  
   1.152  (* substitute using an object or meta level equality *)
   1.153 @@ -295,7 +293,7 @@
   1.154  
   1.155  
   1.156  (* General substitution of multiple occurances using one of
   1.157 -   the given theorems*)
   1.158 +   the given theorems *)
   1.159  
   1.160  fun skip_first_occs_search occ srchf sinfo lhs =
   1.161    (case (skipto_skipseq occ (srchf sinfo lhs)) of
   1.162 @@ -316,7 +314,7 @@
   1.163          thmseq |> Seq.maps (fn r =>
   1.164            eqsubst_tac' ctxt
   1.165              (skip_first_occs_search occ searchf_lr_unify_valid) r
   1.166 -            (i + ((Thm.nprems_of th) - nprems)) th);
   1.167 +            (i + (Thm.nprems_of th - nprems)) th);
   1.168        val sortedoccL = Library.sort (rev_order o int_ord) occL;
   1.169      in
   1.170        Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
   1.171 @@ -340,7 +338,7 @@
   1.172        |> RWInst.beta_eta_contract; (* normal form *)
   1.173    in
   1.174      (* ~j because new asm starts at back, thus we subtract 1 *)
   1.175 -    Seq.map (Thm.rotate_rule (~ j) ((Thm.nprems_of rule) + i))
   1.176 +    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i))
   1.177        (Tactic.dtac preelimrule i th2)
   1.178    end;
   1.179  
   1.180 @@ -356,24 +354,23 @@
   1.181      val th = Thm.incr_indexes 1 gth;
   1.182      val tgt_term = Thm.prop_of th;
   1.183  
   1.184 -    val sgn = Thm.theory_of_thm th;
   1.185 -    val ctermify = Thm.cterm_of sgn;
   1.186 -    val trivify = Thm.trivial o ctermify;
   1.187 +    val thy = Thm.theory_of_thm th;
   1.188 +    val cert = Thm.cterm_of thy;
   1.189  
   1.190      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
   1.191 -    val cfvs = rev (map ctermify fvs);
   1.192 +    val cfvs = rev (map cert fvs);
   1.193  
   1.194      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
   1.195      val asm_nprems = length (Logic.strip_imp_prems asmt);
   1.196  
   1.197 -    val pth = trivify asmt;
   1.198 +    val pth = Thm.trivial (cert asmt);
   1.199      val maxidx = Thm.maxidx_of th;
   1.200  
   1.201      val ft =
   1.202        (Zipper.move_down_right (* trueprop *)
   1.203           o Zipper.mktop
   1.204           o Thm.prop_of) pth
   1.205 -  in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   1.206 +  in ((cfvs, j, asm_nprems, pth), (thy, maxidx, ft)) end;
   1.207  
   1.208  (* prepare subst in every possible assumption *)
   1.209  fun prep_subst_in_asms ctxt i gth =
   1.210 @@ -416,7 +413,7 @@
   1.211            thmseq |> Seq.maps (fn r =>
   1.212              eqsubst_asm_tac' ctxt
   1.213                (skip_first_asm_occs_search searchf_lr_unify_valid) occK r
   1.214 -              (i + ((Thm.nprems_of th) - nprems)) th);
   1.215 +              (i + (Thm.nprems_of th - nprems)) th);
   1.216          val sortedoccs = Library.sort (rev_order o int_ord) occL;
   1.217        in
   1.218          Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccs) th)