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;