src/Tools/eqsubst.ML
changeset 30160 5f7b17941730
parent 29269 5c25a2012975
child 30318 3d03190d2864
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/eqsubst.ML	Sat Feb 28 14:02:12 2009 +0100
     1.3 @@ -0,0 +1,575 @@
     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 +*)
     1.9 +
    1.10 +signature EQSUBST =
    1.11 +sig
    1.12 +  (* a type abbreviation for match information *)
    1.13 +  type match =
    1.14 +       ((indexname * (sort * typ)) list (* type instantiations *)
    1.15 +        * (indexname * (typ * term)) list) (* term instantiations *)
    1.16 +       * (string * typ) list (* fake named type abs env *)
    1.17 +       * (string * typ) list (* type abs env *)
    1.18 +       * term (* outer term *)
    1.19 +
    1.20 +  type searchinfo =
    1.21 +       theory
    1.22 +       * int (* maxidx *)
    1.23 +       * Zipper.T (* focusterm to search under *)
    1.24 +
    1.25 +    exception eqsubst_occL_exp of
    1.26 +       string * int list * Thm.thm list * int * Thm.thm
    1.27 +    
    1.28 +    (* low level substitution functions *)
    1.29 +    val apply_subst_in_asm :
    1.30 +       int ->
    1.31 +       Thm.thm ->
    1.32 +       Thm.thm ->
    1.33 +       (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq
    1.34 +    val apply_subst_in_concl :
    1.35 +       int ->
    1.36 +       Thm.thm ->
    1.37 +       Thm.cterm list * Thm.thm ->
    1.38 +       Thm.thm -> match -> Thm.thm Seq.seq
    1.39 +
    1.40 +    (* matching/unification within zippers *)
    1.41 +    val clean_match_z :
    1.42 +       Context.theory -> Term.term -> Zipper.T -> match option
    1.43 +    val clean_unify_z :
    1.44 +       Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq
    1.45 +
    1.46 +    (* skipping things in seq seq's *)
    1.47 +
    1.48 +   (* skipping non-empty sub-sequences but when we reach the end
    1.49 +      of the seq, remembering how much we have left to skip. *)
    1.50 +    datatype 'a skipseq = SkipMore of int
    1.51 +      | SkipSeq of 'a Seq.seq Seq.seq;
    1.52 +
    1.53 +    val skip_first_asm_occs_search :
    1.54 +       ('a -> 'b -> 'c Seq.seq Seq.seq) ->
    1.55 +       'a -> int -> 'b -> 'c skipseq
    1.56 +    val skip_first_occs_search :
    1.57 +       int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
    1.58 +    val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
    1.59 +
    1.60 +    (* tactics *)
    1.61 +    val eqsubst_asm_tac :
    1.62 +       Proof.context ->
    1.63 +       int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    1.64 +    val eqsubst_asm_tac' :
    1.65 +       Proof.context ->
    1.66 +       (searchinfo -> int -> Term.term -> match skipseq) ->
    1.67 +       int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
    1.68 +    val eqsubst_tac :
    1.69 +       Proof.context ->
    1.70 +       int list -> (* list of occurences to rewrite, use [0] for any *)
    1.71 +       Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    1.72 +    val eqsubst_tac' :
    1.73 +       Proof.context -> (* proof context *)
    1.74 +       (searchinfo -> Term.term -> match Seq.seq) (* search function *)
    1.75 +       -> Thm.thm (* equation theorem to rewrite with *)
    1.76 +       -> int (* subgoal number in goal theorem *)
    1.77 +       -> Thm.thm (* goal theorem *)
    1.78 +       -> Thm.thm Seq.seq (* rewritten goal theorem *)
    1.79 +
    1.80 +
    1.81 +    val fakefree_badbounds :
    1.82 +       (string * Term.typ) list ->
    1.83 +       Term.term ->
    1.84 +       (string * Term.typ) list * (string * Term.typ) list * Term.term
    1.85 +
    1.86 +    val mk_foo_match :
    1.87 +       (Term.term -> Term.term) ->
    1.88 +       ('a * Term.typ) list -> Term.term -> Term.term
    1.89 +
    1.90 +    (* preparing substitution *)
    1.91 +    val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list
    1.92 +    val prep_concl_subst :
    1.93 +       int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo
    1.94 +    val prep_subst_in_asm :
    1.95 +       int -> Thm.thm -> int ->
    1.96 +       (Thm.cterm list * int * int * Thm.thm) * searchinfo
    1.97 +    val prep_subst_in_asms :
    1.98 +       int -> Thm.thm ->
    1.99 +       ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list
   1.100 +    val prep_zipper_match :
   1.101 +       Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term)
   1.102 +
   1.103 +    (* search for substitutions *)
   1.104 +    val valid_match_start : Zipper.T -> bool
   1.105 +    val search_lr_all : Zipper.T -> Zipper.T Seq.seq
   1.106 +    val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
   1.107 +    val searchf_lr_unify_all :
   1.108 +       searchinfo -> Term.term -> match Seq.seq Seq.seq
   1.109 +    val searchf_lr_unify_valid :
   1.110 +       searchinfo -> Term.term -> match Seq.seq Seq.seq
   1.111 +    val searchf_bt_unify_valid :
   1.112 +       searchinfo -> Term.term -> match Seq.seq Seq.seq
   1.113 +
   1.114 +    (* syntax tools *)
   1.115 +    val ith_syntax : Args.T list -> int list * Args.T list
   1.116 +    val options_syntax : Args.T list -> bool * Args.T list
   1.117 +
   1.118 +    (* Isar level hooks *)
   1.119 +    val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   1.120 +    val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   1.121 +    val subst_meth : Method.src -> Proof.context -> Proof.method
   1.122 +    val setup : theory -> theory
   1.123 +
   1.124 +end;
   1.125 +
   1.126 +structure EqSubst
   1.127 +: EQSUBST
   1.128 += struct
   1.129 +
   1.130 +structure Z = Zipper;
   1.131 +
   1.132 +(* changes object "=" to meta "==" which prepares a given rewrite rule *)
   1.133 +fun prep_meta_eq ctxt =
   1.134 +  let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
   1.135 +  in mk #> map Drule.zero_var_indexes end;
   1.136 +
   1.137 +
   1.138 +  (* a type abriviation for match information *)
   1.139 +  type match =
   1.140 +       ((indexname * (sort * typ)) list (* type instantiations *)
   1.141 +        * (indexname * (typ * term)) list) (* term instantiations *)
   1.142 +       * (string * typ) list (* fake named type abs env *)
   1.143 +       * (string * typ) list (* type abs env *)
   1.144 +       * term (* outer term *)
   1.145 +
   1.146 +  type searchinfo =
   1.147 +       theory
   1.148 +       * int (* maxidx *)
   1.149 +       * Zipper.T (* focusterm to search under *)
   1.150 +
   1.151 +
   1.152 +(* skipping non-empty sub-sequences but when we reach the end
   1.153 +   of the seq, remembering how much we have left to skip. *)
   1.154 +datatype 'a skipseq = SkipMore of int
   1.155 +  | SkipSeq of 'a Seq.seq Seq.seq;
   1.156 +(* given a seqseq, skip the first m non-empty seq's, note deficit *)
   1.157 +fun skipto_skipseq m s = 
   1.158 +    let 
   1.159 +      fun skip_occs n sq = 
   1.160 +          case Seq.pull sq of 
   1.161 +            NONE => SkipMore n
   1.162 +          | SOME (h,t) => 
   1.163 +            (case Seq.pull h of NONE => skip_occs n t
   1.164 +             | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
   1.165 +                         else skip_occs (n - 1) t)
   1.166 +    in (skip_occs m s) end;
   1.167 +
   1.168 +(* note: outerterm is the taget with the match replaced by a bound 
   1.169 +         variable : ie: "P lhs" beocmes "%x. P x" 
   1.170 +         insts is the types of instantiations of vars in lhs
   1.171 +         and typinsts is the type instantiations of types in the lhs
   1.172 +         Note: Final rule is the rule lifted into the ontext of the 
   1.173 +         taget thm. *)
   1.174 +fun mk_foo_match mkuptermfunc Ts t = 
   1.175 +    let 
   1.176 +      val ty = Term.type_of t
   1.177 +      val bigtype = (rev (map snd Ts)) ---> ty
   1.178 +      fun mk_foo 0 t = t
   1.179 +        | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
   1.180 +      val num_of_bnds = (length Ts)
   1.181 +      (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
   1.182 +      val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
   1.183 +    in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
   1.184 +
   1.185 +(* T is outer bound vars, n is number of locally bound vars *)
   1.186 +(* THINK: is order of Ts correct...? or reversed? *)
   1.187 +fun fakefree_badbounds Ts t = 
   1.188 +    let val (FakeTs,Ts,newnames) = 
   1.189 +            List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
   1.190 +                           let val newname = Name.variant usednames n
   1.191 +                           in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
   1.192 +                               (newname,ty)::Ts, 
   1.193 +                               newname::usednames) end)
   1.194 +                       ([],[],[])
   1.195 +                       Ts
   1.196 +    in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
   1.197 +
   1.198 +(* before matching we need to fake the bound vars that are missing an
   1.199 +abstraction. In this function we additionally construct the
   1.200 +abstraction environment, and an outer context term (with the focus
   1.201 +abstracted out) for use in rewriting with RWInst.rw *)
   1.202 +fun prep_zipper_match z = 
   1.203 +    let 
   1.204 +      val t = Z.trm z  
   1.205 +      val c = Z.ctxt z
   1.206 +      val Ts = Z.C.nty_ctxt c
   1.207 +      val (FakeTs', Ts', t') = fakefree_badbounds Ts t
   1.208 +      val absterm = mk_foo_match (Z.C.apply c) Ts' t'
   1.209 +    in
   1.210 +      (t', (FakeTs', Ts', absterm))
   1.211 +    end;
   1.212 +
   1.213 +(* Matching and Unification with exception handled *)
   1.214 +fun clean_match thy (a as (pat, t)) =
   1.215 +  let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
   1.216 +  in SOME (Vartab.dest tyenv, Vartab.dest tenv)
   1.217 +  end handle Pattern.MATCH => NONE;
   1.218 +
   1.219 +(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
   1.220 +fun clean_unify thry ix (a as (pat, tgt)) =
   1.221 +    let
   1.222 +      (* type info will be re-derived, maybe this can be cached
   1.223 +         for efficiency? *)
   1.224 +      val pat_ty = Term.type_of pat;
   1.225 +      val tgt_ty = Term.type_of tgt;
   1.226 +      (* is it OK to ignore the type instantiation info?
   1.227 +         or should I be using it? *)
   1.228 +      val typs_unify =
   1.229 +          SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
   1.230 +            handle Type.TUNIFY => NONE;
   1.231 +    in
   1.232 +      case typs_unify of
   1.233 +        SOME (typinsttab, ix2) =>
   1.234 +        let
   1.235 +      (* is it right to throw away the flexes?
   1.236 +         or should I be using them somehow? *)
   1.237 +          fun mk_insts env =
   1.238 +            (Vartab.dest (Envir.type_env env),
   1.239 +             Envir.alist_of env);
   1.240 +          val initenv = Envir.Envir {asol = Vartab.empty,
   1.241 +                                     iTs = typinsttab, maxidx = ix2};
   1.242 +          val useq = Unify.smash_unifiers thry [a] initenv
   1.243 +	            handle UnequalLengths => Seq.empty
   1.244 +		               | Term.TERM _ => Seq.empty;
   1.245 +          fun clean_unify' useq () =
   1.246 +              (case (Seq.pull useq) of
   1.247 +                 NONE => NONE
   1.248 +               | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
   1.249 +	            handle UnequalLengths => NONE
   1.250 +                   | Term.TERM _ => NONE
   1.251 +        in
   1.252 +          (Seq.make (clean_unify' useq))
   1.253 +        end
   1.254 +      | NONE => Seq.empty
   1.255 +    end;
   1.256 +
   1.257 +(* Matching and Unification for zippers *)
   1.258 +(* Note: Ts is a modified version of the original names of the outer
   1.259 +bound variables. New names have been introduced to make sure they are
   1.260 +unique w.r.t all names in the term and each other. usednames' is
   1.261 +oldnames + new names. *)
   1.262 +fun clean_match_z thy pat z = 
   1.263 +    let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
   1.264 +      case clean_match thy (pat, t) of 
   1.265 +        NONE => NONE 
   1.266 +      | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
   1.267 +(* ix = max var index *)
   1.268 +fun clean_unify_z sgn ix pat z = 
   1.269 +    let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
   1.270 +    Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) 
   1.271 +            (clean_unify sgn ix (t, pat)) end;
   1.272 +
   1.273 +
   1.274 +(* FOR DEBUGGING...
   1.275 +type trace_subst_errT = int (* subgoal *)
   1.276 +        * thm (* thm with all goals *)
   1.277 +        * (Thm.cterm list (* certified free var placeholders for vars *)
   1.278 +           * thm)  (* trivial thm of goal concl *)
   1.279 +            (* possible matches/unifiers *)
   1.280 +        * thm (* rule *)
   1.281 +        * (((indexname * typ) list (* type instantiations *)
   1.282 +              * (indexname * term) list ) (* term instantiations *)
   1.283 +             * (string * typ) list (* Type abs env *)
   1.284 +             * term) (* outer term *);
   1.285 +
   1.286 +val trace_subst_err = (ref NONE : trace_subst_errT option ref);
   1.287 +val trace_subst_search = ref false;
   1.288 +exception trace_subst_exp of trace_subst_errT;
   1.289 +*)
   1.290 +
   1.291 +
   1.292 +fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
   1.293 +  | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
   1.294 +  | bot_left_leaf_of x = x;
   1.295 +
   1.296 +(* Avoid considering replacing terms which have a var at the head as
   1.297 +   they always succeed trivially, and uninterestingly. *)
   1.298 +fun valid_match_start z =
   1.299 +    (case bot_left_leaf_of (Z.trm z) of 
   1.300 +      Var _ => false 
   1.301 +      | _ => true);
   1.302 +
   1.303 +(* search from top, left to right, then down *)
   1.304 +val search_lr_all = ZipperSearch.all_bl_ur;
   1.305 +
   1.306 +(* search from top, left to right, then down *)
   1.307 +fun search_lr_valid validf =
   1.308 +    let 
   1.309 +      fun sf_valid_td_lr z = 
   1.310 +          let val here = if validf z then [Z.Here z] else [] in
   1.311 +            case Z.trm z 
   1.312 +             of _ $ _ => [Z.LookIn (Z.move_down_left z)] 
   1.313 +                         @ here 
   1.314 +                         @ [Z.LookIn (Z.move_down_right z)]
   1.315 +              | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
   1.316 +              | _ => here
   1.317 +          end;
   1.318 +    in Z.lzy_search sf_valid_td_lr end;
   1.319 +
   1.320 +(* search from bottom to top, left to right *)
   1.321 +
   1.322 +fun search_bt_valid validf =
   1.323 +    let 
   1.324 +      fun sf_valid_td_lr z = 
   1.325 +          let val here = if validf z then [Z.Here z] else [] in
   1.326 +            case Z.trm z 
   1.327 +             of _ $ _ => [Z.LookIn (Z.move_down_left z), 
   1.328 +                          Z.LookIn (Z.move_down_right z)] @ here
   1.329 +              | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here
   1.330 +              | _ => here
   1.331 +          end;
   1.332 +    in Z.lzy_search sf_valid_td_lr end;
   1.333 +
   1.334 +fun searchf_unify_gen f (sgn, maxidx, z) lhs =
   1.335 +    Seq.map (clean_unify_z sgn maxidx lhs) 
   1.336 +            (Z.limit_apply f z);
   1.337 +
   1.338 +(* search all unifications *)
   1.339 +val searchf_lr_unify_all =
   1.340 +    searchf_unify_gen search_lr_all;
   1.341 +
   1.342 +(* search only for 'valid' unifiers (non abs subterms and non vars) *)
   1.343 +val searchf_lr_unify_valid = 
   1.344 +    searchf_unify_gen (search_lr_valid valid_match_start);
   1.345 +
   1.346 +val searchf_bt_unify_valid =
   1.347 +    searchf_unify_gen (search_bt_valid valid_match_start);
   1.348 +
   1.349 +(* apply a substitution in the conclusion of the theorem th *)
   1.350 +(* cfvs are certified free var placeholders for goal params *)
   1.351 +(* conclthm is a theorem of for just the conclusion *)
   1.352 +(* m is instantiation/match information *)
   1.353 +(* rule is the equation for substitution *)
   1.354 +fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
   1.355 +    (RWInst.rw m rule conclthm)
   1.356 +      |> IsaND.unfix_frees cfvs
   1.357 +      |> RWInst.beta_eta_contract
   1.358 +      |> (fn r => Tactic.rtac r i th);
   1.359 +
   1.360 +(* substitute within the conclusion of goal i of gth, using a meta
   1.361 +equation rule. Note that we assume rule has var indicies zero'd *)
   1.362 +fun prep_concl_subst i gth =
   1.363 +    let
   1.364 +      val th = Thm.incr_indexes 1 gth;
   1.365 +      val tgt_term = Thm.prop_of th;
   1.366 +
   1.367 +      val sgn = Thm.theory_of_thm th;
   1.368 +      val ctermify = Thm.cterm_of sgn;
   1.369 +      val trivify = Thm.trivial o ctermify;
   1.370 +
   1.371 +      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   1.372 +      val cfvs = rev (map ctermify fvs);
   1.373 +
   1.374 +      val conclterm = Logic.strip_imp_concl fixedbody;
   1.375 +      val conclthm = trivify conclterm;
   1.376 +      val maxidx = Thm.maxidx_of th;
   1.377 +      val ft = ((Z.move_down_right (* ==> *)
   1.378 +                 o Z.move_down_left (* Trueprop *)
   1.379 +                 o Z.mktop
   1.380 +                 o Thm.prop_of) conclthm)
   1.381 +    in
   1.382 +      ((cfvs, conclthm), (sgn, maxidx, ft))
   1.383 +    end;
   1.384 +
   1.385 +(* substitute using an object or meta level equality *)
   1.386 +fun eqsubst_tac' ctxt searchf instepthm i th =
   1.387 +    let
   1.388 +      val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
   1.389 +      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   1.390 +      fun rewrite_with_thm r =
   1.391 +          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
   1.392 +          in searchf searchinfo lhs
   1.393 +             |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
   1.394 +    in stepthms |> Seq.maps rewrite_with_thm end;
   1.395 +
   1.396 +
   1.397 +(* distinct subgoals *)
   1.398 +fun distinct_subgoals th =
   1.399 +  the_default th (SINGLE distinct_subgoals_tac th);
   1.400 +
   1.401 +(* General substitution of multiple occurances using one of
   1.402 +   the given theorems*)
   1.403 +
   1.404 +
   1.405 +exception eqsubst_occL_exp of
   1.406 +          string * (int list) * (thm list) * int * thm;
   1.407 +fun skip_first_occs_search occ srchf sinfo lhs =
   1.408 +    case (skipto_skipseq occ (srchf sinfo lhs)) of
   1.409 +      SkipMore _ => Seq.empty
   1.410 +    | SkipSeq ss => Seq.flat ss;
   1.411 +
   1.412 +(* The occL is a list of integers indicating which occurence
   1.413 +w.r.t. the search order, to rewrite. Backtracking will also find later
   1.414 +occurences, but all earlier ones are skipped. Thus you can use [0] to
   1.415 +just find all rewrites. *)
   1.416 +
   1.417 +fun eqsubst_tac ctxt occL thms i th =
   1.418 +    let val nprems = Thm.nprems_of th in
   1.419 +      if nprems < i then Seq.empty else
   1.420 +      let val thmseq = (Seq.of_list thms)
   1.421 +        fun apply_occ occ th =
   1.422 +            thmseq |> Seq.maps
   1.423 +                    (fn r => eqsubst_tac' 
   1.424 +                               ctxt 
   1.425 +                               (skip_first_occs_search
   1.426 +                                  occ searchf_lr_unify_valid) r
   1.427 +                                 (i + ((Thm.nprems_of th) - nprems))
   1.428 +                                 th);
   1.429 +        val sortedoccL =
   1.430 +            Library.sort (Library.rev_order o Library.int_ord) occL;
   1.431 +      in
   1.432 +        Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
   1.433 +      end
   1.434 +    end
   1.435 +    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   1.436 +
   1.437 +
   1.438 +(* inthms are the given arguments in Isar, and treated as eqstep with
   1.439 +   the first one, then the second etc *)
   1.440 +fun eqsubst_meth ctxt occL inthms =
   1.441 +    Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
   1.442 +
   1.443 +(* apply a substitution inside assumption j, keeps asm in the same place *)
   1.444 +fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
   1.445 +    let
   1.446 +      val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
   1.447 +      val preelimrule =
   1.448 +          (RWInst.rw m rule pth)
   1.449 +            |> (Seq.hd o prune_params_tac)
   1.450 +            |> Thm.permute_prems 0 ~1 (* put old asm first *)
   1.451 +            |> IsaND.unfix_frees cfvs (* unfix any global params *)
   1.452 +            |> RWInst.beta_eta_contract; (* normal form *)
   1.453 +  (*    val elimrule =
   1.454 +          preelimrule
   1.455 +            |> Tactic.make_elim (* make into elim rule *)
   1.456 +            |> Thm.lift_rule (th2, i); (* lift into context *)
   1.457 +   *)
   1.458 +    in
   1.459 +      (* ~j because new asm starts at back, thus we subtract 1 *)
   1.460 +      Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
   1.461 +      (Tactic.dtac preelimrule i th2)
   1.462 +
   1.463 +      (* (Thm.bicompose
   1.464 +                 false (* use unification *)
   1.465 +                 (true, (* elim resolution *)
   1.466 +                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
   1.467 +                 i th2) *)
   1.468 +    end;
   1.469 +
   1.470 +
   1.471 +(* prepare to substitute within the j'th premise of subgoal i of gth,
   1.472 +using a meta-level equation. Note that we assume rule has var indicies
   1.473 +zero'd. Note that we also assume that premt is the j'th premice of
   1.474 +subgoal i of gth. Note the repetition of work done for each
   1.475 +assumption, i.e. this can be made more efficient for search over
   1.476 +multiple assumptions.  *)
   1.477 +fun prep_subst_in_asm i gth j =
   1.478 +    let
   1.479 +      val th = Thm.incr_indexes 1 gth;
   1.480 +      val tgt_term = Thm.prop_of th;
   1.481 +
   1.482 +      val sgn = Thm.theory_of_thm th;
   1.483 +      val ctermify = Thm.cterm_of sgn;
   1.484 +      val trivify = Thm.trivial o ctermify;
   1.485 +
   1.486 +      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   1.487 +      val cfvs = rev (map ctermify fvs);
   1.488 +
   1.489 +      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
   1.490 +      val asm_nprems = length (Logic.strip_imp_prems asmt);
   1.491 +
   1.492 +      val pth = trivify asmt;
   1.493 +      val maxidx = Thm.maxidx_of th;
   1.494 +
   1.495 +      val ft = ((Z.move_down_right (* trueprop *)
   1.496 +                 o Z.mktop
   1.497 +                 o Thm.prop_of) pth)
   1.498 +    in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   1.499 +
   1.500 +(* prepare subst in every possible assumption *)
   1.501 +fun prep_subst_in_asms i gth =
   1.502 +    map (prep_subst_in_asm i gth)
   1.503 +        ((fn l => Library.upto (1, length l))
   1.504 +           (Logic.prems_of_goal (Thm.prop_of gth) i));
   1.505 +
   1.506 +
   1.507 +(* substitute in an assumption using an object or meta level equality *)
   1.508 +fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
   1.509 +    let
   1.510 +      val asmpreps = prep_subst_in_asms i th;
   1.511 +      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   1.512 +      fun rewrite_with_thm r =
   1.513 +          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
   1.514 +            fun occ_search occ [] = Seq.empty
   1.515 +              | occ_search occ ((asminfo, searchinfo)::moreasms) =
   1.516 +                (case searchf searchinfo occ lhs of
   1.517 +                   SkipMore i => occ_search i moreasms
   1.518 +                 | SkipSeq ss =>
   1.519 +                   Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
   1.520 +                               (occ_search 1 moreasms))
   1.521 +                              (* find later substs also *)
   1.522 +          in
   1.523 +            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
   1.524 +          end;
   1.525 +    in stepthms |> Seq.maps rewrite_with_thm end;
   1.526 +
   1.527 +
   1.528 +fun skip_first_asm_occs_search searchf sinfo occ lhs =
   1.529 +    skipto_skipseq occ (searchf sinfo lhs);
   1.530 +
   1.531 +fun eqsubst_asm_tac ctxt occL thms i th =
   1.532 +    let val nprems = Thm.nprems_of th
   1.533 +    in
   1.534 +      if nprems < i then Seq.empty else
   1.535 +      let val thmseq = (Seq.of_list thms)
   1.536 +        fun apply_occ occK th =
   1.537 +            thmseq |> Seq.maps
   1.538 +                    (fn r =>
   1.539 +                        eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
   1.540 +                                            searchf_lr_unify_valid) occK r
   1.541 +                                         (i + ((Thm.nprems_of th) - nprems))
   1.542 +                                         th);
   1.543 +        val sortedoccs =
   1.544 +            Library.sort (Library.rev_order o Library.int_ord) occL
   1.545 +      in
   1.546 +        Seq.map distinct_subgoals
   1.547 +                (Seq.EVERY (map apply_occ sortedoccs) th)
   1.548 +      end
   1.549 +    end
   1.550 +    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   1.551 +
   1.552 +(* inthms are the given arguments in Isar, and treated as eqstep with
   1.553 +   the first one, then the second etc *)
   1.554 +fun eqsubst_asm_meth ctxt occL inthms =
   1.555 +    Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
   1.556 +
   1.557 +(* syntax for options, given "(asm)" will give back true, without
   1.558 +   gives back false *)
   1.559 +val options_syntax =
   1.560 +    (Args.parens (Args.$$$ "asm") >> (K true)) ||
   1.561 +     (Scan.succeed false);
   1.562 +
   1.563 +val ith_syntax =
   1.564 +    Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
   1.565 +
   1.566 +(* combination method that takes a flag (true indicates that subst
   1.567 +should be done to an assumption, false = apply to the conclusion of
   1.568 +the goal) as well as the theorems to use *)
   1.569 +fun subst_meth src =
   1.570 +  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
   1.571 +  #> (fn (((asmflag, occL), inthms), ctxt) =>
   1.572 +    (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
   1.573 +
   1.574 +
   1.575 +val setup =
   1.576 +  Method.add_method ("subst", subst_meth, "single-step substitution");
   1.577 +
   1.578 +end;