# HG changeset patch # User wenzelm # Date 1369916276 -7200 # Node ID 6aff6b8bec13c11849e1e50ab34003c29d0276c2 # Parent 6ffcce2110474e30f7d2a6b0e315f67d68058785 tuned; diff -r 6ffcce211047 -r 6aff6b8bec13 src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Thu May 30 13:59:38 2013 +0200 +++ b/src/Tools/eqsubst.ML Thu May 30 14:17:56 2013 +0200 @@ -1,7 +1,7 @@ (* Title: Tools/eqsubst.ML Author: Lucas Dixon, University of Edinburgh -A proof method to perform a substiution using an equation. +Perform a substitution using an equation. *) signature EQSUBST = @@ -58,16 +58,16 @@ type match = - ((indexname * (sort * typ)) list (* type instantiations *) - * (indexname * (typ * term)) list) (* term instantiations *) - * (string * typ) list (* fake named type abs env *) - * (string * typ) list (* type abs env *) - * term; (* outer term *) + ((indexname * (sort * typ)) list (* type instantiations *) + * (indexname * (typ * term)) list) (* term instantiations *) + * (string * typ) list (* fake named type abs env *) + * (string * typ) list (* type abs env *) + * term; (* outer term *) type searchinfo = - theory - * int (* maxidx *) - * Zipper.T; (* focusterm to search under *) + theory + * int (* maxidx *) + * Zipper.T; (* focusterm to search under *) (* skipping non-empty sub-sequences but when we reach the end @@ -97,10 +97,10 @@ fun mk_foo_match mkuptermfunc Ts t = let val ty = Term.type_of t - val bigtype = (rev (map snd Ts)) ---> ty + val bigtype = rev (map snd Ts) ---> ty fun mk_foo 0 t = t | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1))) - val num_of_bnds = (length Ts) + val num_of_bnds = length Ts (* foo_term = "fooabs y0 ... yn" where y's are local bounds *) val foo_term = mk_foo num_of_bnds (Bound num_of_bnds) in Abs ("fooabs", bigtype, mkuptermfunc foo_term) end; @@ -121,9 +121,9 @@ in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end; (* before matching we need to fake the bound vars that are missing an -abstraction. In this function we additionally construct the -abstraction environment, and an outer context term (with the focus -abstracted out) for use in rewriting with RWInst.rw *) + abstraction. In this function we additionally construct the + abstraction environment, and an outer context term (with the focus + abstracted out) for use in rewriting with RWInst.rw *) fun prep_zipper_match z = let val t = Zipper.trm z @@ -137,16 +137,16 @@ (* Unification with exception handled *) (* given theory, max var index, pat, tgt; returns Seq of instantiations *) -fun clean_unify thry ix (a as (pat, tgt)) = +fun clean_unify thy ix (a as (pat, tgt)) = let (* type info will be re-derived, maybe this can be cached for efficiency? *) val pat_ty = Term.type_of pat; val tgt_ty = Term.type_of tgt; - (* is it OK to ignore the type instantiation info? + (* FIXME is it OK to ignore the type instantiation info? or should I be using it? *) val typs_unify = - SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix)) + SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix)) handle Type.TUNIFY => NONE; in (case typs_unify of @@ -159,7 +159,7 @@ Vartab.dest (Envir.term_env env)); val initenv = Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab}; - val useq = Unify.smash_unifiers thry [a] initenv + val useq = Unify.smash_unifiers thy [a] initenv handle ListPair.UnequalLengths => Seq.empty | Term.TERM _ => Seq.empty; fun clean_unify' useq () = @@ -176,14 +176,13 @@ (* Unification for zippers *) (* Note: Ts is a modified version of the original names of the outer -bound variables. New names have been introduced to make sure they are -unique w.r.t all names in the term and each other. usednames' is -oldnames + new names. *) -(* ix = max var index *) -fun clean_unify_z sgn ix pat z = - let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in + bound variables. New names have been introduced to make sure they are + unique w.r.t all names in the term and each other. usednames' is + oldnames + new names. *) +fun clean_unify_z thy maxidx pat z = + let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) - (clean_unify sgn ix (t, pat)) + (clean_unify thy maxidx (t, pat)) end; @@ -229,8 +228,8 @@ end; in Zipper.lzy_search sf_valid_td_lr end; -fun searchf_unify_gen f (sgn, maxidx, z) lhs = - Seq.map (clean_unify_z sgn maxidx lhs) (Zipper.limit_apply f z); +fun searchf_unify_gen f (thy, maxidx, z) lhs = + Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z); (* search all unifications *) val searchf_lr_unify_all = searchf_unify_gen search_lr_all; @@ -258,15 +257,14 @@ val th = Thm.incr_indexes 1 gth; val tgt_term = Thm.prop_of th; - val sgn = Thm.theory_of_thm th; - val ctermify = Thm.cterm_of sgn; - val trivify = Thm.trivial o ctermify; + val thy = Thm.theory_of_thm th; + val cert = Thm.cterm_of thy; val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term; - val cfvs = rev (map ctermify fvs); + val cfvs = rev (map cert fvs); val conclterm = Logic.strip_imp_concl fixedbody; - val conclthm = trivify conclterm; + val conclthm = Thm.trivial (cert conclterm); val maxidx = Thm.maxidx_of th; val ft = (Zipper.move_down_right (* ==> *) @@ -274,7 +272,7 @@ o Zipper.mktop o Thm.prop_of) conclthm in - ((cfvs, conclthm), (sgn, maxidx, ft)) + ((cfvs, conclthm), (thy, maxidx, ft)) end; (* substitute using an object or meta level equality *) @@ -295,7 +293,7 @@ (* General substitution of multiple occurances using one of - the given theorems*) + the given theorems *) fun skip_first_occs_search occ srchf sinfo lhs = (case (skipto_skipseq occ (srchf sinfo lhs)) of @@ -316,7 +314,7 @@ thmseq |> Seq.maps (fn r => eqsubst_tac' ctxt (skip_first_occs_search occ searchf_lr_unify_valid) r - (i + ((Thm.nprems_of th) - nprems)) th); + (i + (Thm.nprems_of th - nprems)) th); val sortedoccL = Library.sort (rev_order o int_ord) occL; in Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th) @@ -340,7 +338,7 @@ |> RWInst.beta_eta_contract; (* normal form *) in (* ~j because new asm starts at back, thus we subtract 1 *) - Seq.map (Thm.rotate_rule (~ j) ((Thm.nprems_of rule) + i)) + Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (Tactic.dtac preelimrule i th2) end; @@ -356,24 +354,23 @@ val th = Thm.incr_indexes 1 gth; val tgt_term = Thm.prop_of th; - val sgn = Thm.theory_of_thm th; - val ctermify = Thm.cterm_of sgn; - val trivify = Thm.trivial o ctermify; + val thy = Thm.theory_of_thm th; + val cert = Thm.cterm_of thy; val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term; - val cfvs = rev (map ctermify fvs); + val cfvs = rev (map cert fvs); val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1); val asm_nprems = length (Logic.strip_imp_prems asmt); - val pth = trivify asmt; + val pth = Thm.trivial (cert asmt); val maxidx = Thm.maxidx_of th; val ft = (Zipper.move_down_right (* trueprop *) o Zipper.mktop o Thm.prop_of) pth - in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end; + in ((cfvs, j, asm_nprems, pth), (thy, maxidx, ft)) end; (* prepare subst in every possible assumption *) fun prep_subst_in_asms ctxt i gth = @@ -416,7 +413,7 @@ thmseq |> Seq.maps (fn r => eqsubst_asm_tac' ctxt (skip_first_asm_occs_search searchf_lr_unify_valid) occK r - (i + ((Thm.nprems_of th) - nprems)) th); + (i + (Thm.nprems_of th - nprems)) th); val sortedoccs = Library.sort (rev_order o int_ord) occL; in Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccs) th)