1.1 --- a/src/Tools/eqsubst.ML Thu May 30 13:20:04 2013 +0200
1.2 +++ b/src/Tools/eqsubst.ML Thu May 30 13:59:38 2013 +0200
1.3 @@ -6,61 +6,47 @@
1.4
1.5 signature EQSUBST =
1.6 sig
1.7 - (* a type abbreviation for match information *)
1.8 type match =
1.9 - ((indexname * (sort * typ)) list (* type instantiations *)
1.10 - * (indexname * (typ * term)) list) (* term instantiations *)
1.11 - * (string * typ) list (* fake named type abs env *)
1.12 - * (string * typ) list (* type abs env *)
1.13 - * term (* outer term *)
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 + theory
1.25 + * int (* maxidx *)
1.26 + * Zipper.T (* focusterm to search under *)
1.27
1.28 datatype 'a skipseq = SkipMore of int | SkipSeq of 'a Seq.seq Seq.seq
1.29
1.30 - val skip_first_asm_occs_search :
1.31 - ('a -> 'b -> 'c Seq.seq Seq.seq) ->
1.32 - 'a -> int -> 'b -> 'c skipseq
1.33 - val skip_first_occs_search :
1.34 - int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
1.35 - val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
1.36 + val skip_first_asm_occs_search: ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> int -> 'b -> 'c skipseq
1.37 + val skip_first_occs_search: int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
1.38 + val skipto_skipseq: int -> 'a Seq.seq Seq.seq -> 'a skipseq
1.39
1.40 (* tactics *)
1.41 - val eqsubst_asm_tac :
1.42 - Proof.context ->
1.43 - int list -> thm list -> int -> tactic
1.44 - val eqsubst_asm_tac' :
1.45 - Proof.context ->
1.46 - (searchinfo -> int -> term -> match skipseq) ->
1.47 - int -> thm -> int -> tactic
1.48 - val eqsubst_tac :
1.49 - Proof.context ->
1.50 - int list -> (* list of occurences to rewrite, use [0] for any *)
1.51 - thm list -> int -> tactic
1.52 - val eqsubst_tac' :
1.53 - Proof.context -> (* proof context *)
1.54 - (searchinfo -> term -> match Seq.seq) (* search function *)
1.55 - -> thm (* equation theorem to rewrite with *)
1.56 - -> int (* subgoal number in goal theorem *)
1.57 - -> thm (* goal theorem *)
1.58 - -> thm Seq.seq (* rewritten goal theorem *)
1.59 + val eqsubst_asm_tac: Proof.context -> int list -> thm list -> int -> tactic
1.60 + val eqsubst_asm_tac': Proof.context ->
1.61 + (searchinfo -> int -> term -> match skipseq) -> int -> thm -> int -> tactic
1.62 + val eqsubst_tac: Proof.context ->
1.63 + int list -> (* list of occurences to rewrite, use [0] for any *)
1.64 + thm list -> int -> tactic
1.65 + val eqsubst_tac': Proof.context ->
1.66 + (searchinfo -> term -> match Seq.seq) (* search function *)
1.67 + -> thm (* equation theorem to rewrite with *)
1.68 + -> int (* subgoal number in goal theorem *)
1.69 + -> thm (* goal theorem *)
1.70 + -> thm Seq.seq (* rewritten goal theorem *)
1.71
1.72 (* search for substitutions *)
1.73 - val valid_match_start : Zipper.T -> bool
1.74 - val search_lr_all : Zipper.T -> Zipper.T Seq.seq
1.75 - val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
1.76 - val searchf_lr_unify_all :
1.77 - searchinfo -> term -> match Seq.seq Seq.seq
1.78 - val searchf_lr_unify_valid :
1.79 - searchinfo -> term -> match Seq.seq Seq.seq
1.80 - val searchf_bt_unify_valid :
1.81 - searchinfo -> term -> match Seq.seq Seq.seq
1.82 + val valid_match_start: Zipper.T -> bool
1.83 + val search_lr_all: Zipper.T -> Zipper.T Seq.seq
1.84 + val search_lr_valid: (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
1.85 + val searchf_lr_unify_all: searchinfo -> term -> match Seq.seq Seq.seq
1.86 + val searchf_lr_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
1.87 + val searchf_bt_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
1.88
1.89 val setup : theory -> theory
1.90 -
1.91 end;
1.92
1.93 structure EqSubst: EQSUBST =
1.94 @@ -71,120 +57,122 @@
1.95 Simplifier.mksimps ctxt #> map Drule.zero_var_indexes;
1.96
1.97
1.98 - (* a type abriviation for match information *)
1.99 - type match =
1.100 - ((indexname * (sort * typ)) list (* type instantiations *)
1.101 - * (indexname * (typ * term)) list) (* term instantiations *)
1.102 - * (string * typ) list (* fake named type abs env *)
1.103 - * (string * typ) list (* type abs env *)
1.104 - * term (* outer term *)
1.105 +type match =
1.106 + ((indexname * (sort * typ)) list (* type instantiations *)
1.107 + * (indexname * (typ * term)) list) (* term instantiations *)
1.108 + * (string * typ) list (* fake named type abs env *)
1.109 + * (string * typ) list (* type abs env *)
1.110 + * term; (* outer term *)
1.111
1.112 - type searchinfo =
1.113 - theory
1.114 - * int (* maxidx *)
1.115 - * Zipper.T (* focusterm to search under *)
1.116 +type searchinfo =
1.117 + theory
1.118 + * int (* maxidx *)
1.119 + * Zipper.T; (* focusterm to search under *)
1.120
1.121
1.122 (* skipping non-empty sub-sequences but when we reach the end
1.123 of the seq, remembering how much we have left to skip. *)
1.124 -datatype 'a skipseq = SkipMore of int
1.125 - | SkipSeq of 'a Seq.seq Seq.seq;
1.126 +datatype 'a skipseq =
1.127 + SkipMore of int |
1.128 + SkipSeq of 'a Seq.seq Seq.seq;
1.129 +
1.130 (* given a seqseq, skip the first m non-empty seq's, note deficit *)
1.131 fun skipto_skipseq m s =
1.132 - let
1.133 - fun skip_occs n sq =
1.134 - case Seq.pull sq of
1.135 - NONE => SkipMore n
1.136 - | SOME (h,t) =>
1.137 - (case Seq.pull h of NONE => skip_occs n t
1.138 - | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
1.139 - else skip_occs (n - 1) t)
1.140 - in (skip_occs m s) end;
1.141 + let
1.142 + fun skip_occs n sq =
1.143 + (case Seq.pull sq of
1.144 + NONE => SkipMore n
1.145 + | SOME (h,t) =>
1.146 + (case Seq.pull h of
1.147 + NONE => skip_occs n t
1.148 + | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) else skip_occs (n - 1) t))
1.149 + in skip_occs m s end;
1.150
1.151 (* note: outerterm is the taget with the match replaced by a bound
1.152 - variable : ie: "P lhs" beocmes "%x. P x"
1.153 - insts is the types of instantiations of vars in lhs
1.154 - and typinsts is the type instantiations of types in the lhs
1.155 - Note: Final rule is the rule lifted into the ontext of the
1.156 - taget thm. *)
1.157 + variable : ie: "P lhs" beocmes "%x. P x"
1.158 + insts is the types of instantiations of vars in lhs
1.159 + and typinsts is the type instantiations of types in the lhs
1.160 + Note: Final rule is the rule lifted into the ontext of the
1.161 + taget thm. *)
1.162 fun mk_foo_match mkuptermfunc Ts t =
1.163 - let
1.164 - val ty = Term.type_of t
1.165 - val bigtype = (rev (map snd Ts)) ---> ty
1.166 - fun mk_foo 0 t = t
1.167 - | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
1.168 - val num_of_bnds = (length Ts)
1.169 - (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
1.170 - val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
1.171 - in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
1.172 + let
1.173 + val ty = Term.type_of t
1.174 + val bigtype = (rev (map snd Ts)) ---> ty
1.175 + fun mk_foo 0 t = t
1.176 + | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
1.177 + val num_of_bnds = (length Ts)
1.178 + (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
1.179 + val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
1.180 + in Abs ("fooabs", bigtype, mkuptermfunc foo_term) end;
1.181
1.182 (* T is outer bound vars, n is number of locally bound vars *)
1.183 (* THINK: is order of Ts correct...? or reversed? *)
1.184 fun mk_fake_bound_name n = ":b_" ^ n;
1.185 fun fakefree_badbounds Ts t =
1.186 - let val (FakeTs,Ts,newnames) =
1.187 - List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
1.188 - let val newname = singleton (Name.variant_list usednames) n
1.189 - in ((mk_fake_bound_name newname,ty)::FakeTs,
1.190 - (newname,ty)::Ts,
1.191 - newname::usednames) end)
1.192 - ([],[],[])
1.193 - Ts
1.194 - in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
1.195 + let val (FakeTs, Ts, newnames) =
1.196 + List.foldr (fn ((n, ty), (FakeTs, Ts, usednames)) =>
1.197 + let
1.198 + val newname = singleton (Name.variant_list usednames) n
1.199 + in
1.200 + ((mk_fake_bound_name newname, ty) :: FakeTs,
1.201 + (newname, ty) :: Ts,
1.202 + newname :: usednames)
1.203 + end) ([], [], []) Ts
1.204 + in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
1.205
1.206 (* before matching we need to fake the bound vars that are missing an
1.207 abstraction. In this function we additionally construct the
1.208 abstraction environment, and an outer context term (with the focus
1.209 abstracted out) for use in rewriting with RWInst.rw *)
1.210 fun prep_zipper_match z =
1.211 - let
1.212 - val t = Zipper.trm z
1.213 - val c = Zipper.ctxt z
1.214 - val Ts = Zipper.C.nty_ctxt c
1.215 - val (FakeTs', Ts', t') = fakefree_badbounds Ts t
1.216 - val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
1.217 - in
1.218 - (t', (FakeTs', Ts', absterm))
1.219 - end;
1.220 + let
1.221 + val t = Zipper.trm z
1.222 + val c = Zipper.ctxt z
1.223 + val Ts = Zipper.C.nty_ctxt c
1.224 + val (FakeTs', Ts', t') = fakefree_badbounds Ts t
1.225 + val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
1.226 + in
1.227 + (t', (FakeTs', Ts', absterm))
1.228 + end;
1.229
1.230 (* Unification with exception handled *)
1.231 (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
1.232 fun clean_unify thry ix (a as (pat, tgt)) =
1.233 - let
1.234 - (* type info will be re-derived, maybe this can be cached
1.235 - for efficiency? *)
1.236 - val pat_ty = Term.type_of pat;
1.237 - val tgt_ty = Term.type_of tgt;
1.238 - (* is it OK to ignore the type instantiation info?
1.239 - or should I be using it? *)
1.240 - val typs_unify =
1.241 - SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
1.242 - handle Type.TUNIFY => NONE;
1.243 - in
1.244 - case typs_unify of
1.245 - SOME (typinsttab, ix2) =>
1.246 + let
1.247 + (* type info will be re-derived, maybe this can be cached
1.248 + for efficiency? *)
1.249 + val pat_ty = Term.type_of pat;
1.250 + val tgt_ty = Term.type_of tgt;
1.251 + (* is it OK to ignore the type instantiation info?
1.252 + or should I be using it? *)
1.253 + val typs_unify =
1.254 + SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
1.255 + handle Type.TUNIFY => NONE;
1.256 + in
1.257 + (case typs_unify of
1.258 + SOME (typinsttab, ix2) =>
1.259 let
1.260 - (* is it right to throw away the flexes?
1.261 - or should I be using them somehow? *)
1.262 + (* FIXME is it right to throw away the flexes?
1.263 + or should I be using them somehow? *)
1.264 fun mk_insts env =
1.265 (Vartab.dest (Envir.type_env env),
1.266 Vartab.dest (Envir.term_env env));
1.267 val initenv =
1.268 Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
1.269 val useq = Unify.smash_unifiers thry [a] initenv
1.270 - handle ListPair.UnequalLengths => Seq.empty
1.271 - | Term.TERM _ => Seq.empty;
1.272 + handle ListPair.UnequalLengths => Seq.empty
1.273 + | Term.TERM _ => Seq.empty;
1.274 fun clean_unify' useq () =
1.275 - (case (Seq.pull useq) of
1.276 - NONE => NONE
1.277 - | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
1.278 - handle ListPair.UnequalLengths => NONE
1.279 - | Term.TERM _ => NONE
1.280 + (case (Seq.pull useq) of
1.281 + NONE => NONE
1.282 + | SOME (h, t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
1.283 + handle ListPair.UnequalLengths => NONE
1.284 + | Term.TERM _ => NONE;
1.285 in
1.286 (Seq.make (clean_unify' useq))
1.287 end
1.288 - | NONE => Seq.empty
1.289 - end;
1.290 + | NONE => Seq.empty)
1.291 + end;
1.292
1.293 (* Unification for zippers *)
1.294 (* Note: Ts is a modified version of the original names of the outer
1.295 @@ -193,67 +181,64 @@
1.296 oldnames + new names. *)
1.297 (* ix = max var index *)
1.298 fun clean_unify_z sgn ix pat z =
1.299 - let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
1.300 + let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
1.301 Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
1.302 - (clean_unify sgn ix (t, pat)) end;
1.303 + (clean_unify sgn ix (t, pat))
1.304 + end;
1.305
1.306
1.307 -fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
1.308 - | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
1.309 +fun bot_left_leaf_of (l $ _) = bot_left_leaf_of l
1.310 + | bot_left_leaf_of (Abs (_, _, t)) = bot_left_leaf_of t
1.311 | bot_left_leaf_of x = x;
1.312
1.313 (* Avoid considering replacing terms which have a var at the head as
1.314 they always succeed trivially, and uninterestingly. *)
1.315 fun valid_match_start z =
1.316 - (case bot_left_leaf_of (Zipper.trm z) of
1.317 - Var _ => false
1.318 - | _ => true);
1.319 + (case bot_left_leaf_of (Zipper.trm z) of
1.320 + Var _ => false
1.321 + | _ => true);
1.322
1.323 (* search from top, left to right, then down *)
1.324 val search_lr_all = ZipperSearch.all_bl_ur;
1.325
1.326 (* search from top, left to right, then down *)
1.327 fun search_lr_valid validf =
1.328 - let
1.329 - fun sf_valid_td_lr z =
1.330 - let val here = if validf z then [Zipper.Here z] else [] in
1.331 - case Zipper.trm z
1.332 - of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)]
1.333 - @ here
1.334 - @ [Zipper.LookIn (Zipper.move_down_right z)]
1.335 - | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
1.336 - | _ => here
1.337 - end;
1.338 - in Zipper.lzy_search sf_valid_td_lr end;
1.339 + let
1.340 + fun sf_valid_td_lr z =
1.341 + let val here = if validf z then [Zipper.Here z] else [] in
1.342 + (case Zipper.trm z of
1.343 + _ $ _ =>
1.344 + [Zipper.LookIn (Zipper.move_down_left z)] @ here @
1.345 + [Zipper.LookIn (Zipper.move_down_right z)]
1.346 + | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
1.347 + | _ => here)
1.348 + end;
1.349 + in Zipper.lzy_search sf_valid_td_lr end;
1.350
1.351 (* search from bottom to top, left to right *)
1.352 -
1.353 fun search_bt_valid validf =
1.354 - let
1.355 - fun sf_valid_td_lr z =
1.356 - let val here = if validf z then [Zipper.Here z] else [] in
1.357 - case Zipper.trm z
1.358 - of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z),
1.359 - Zipper.LookIn (Zipper.move_down_right z)] @ here
1.360 - | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
1.361 - | _ => here
1.362 - end;
1.363 - in Zipper.lzy_search sf_valid_td_lr end;
1.364 + let
1.365 + fun sf_valid_td_lr z =
1.366 + let val here = if validf z then [Zipper.Here z] else [] in
1.367 + (case Zipper.trm z of
1.368 + _ $ _ =>
1.369 + [Zipper.LookIn (Zipper.move_down_left z),
1.370 + Zipper.LookIn (Zipper.move_down_right z)] @ here
1.371 + | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
1.372 + | _ => here)
1.373 + end;
1.374 + in Zipper.lzy_search sf_valid_td_lr end;
1.375
1.376 fun searchf_unify_gen f (sgn, maxidx, z) lhs =
1.377 - Seq.map (clean_unify_z sgn maxidx lhs)
1.378 - (Zipper.limit_apply f z);
1.379 + Seq.map (clean_unify_z sgn maxidx lhs) (Zipper.limit_apply f z);
1.380
1.381 (* search all unifications *)
1.382 -val searchf_lr_unify_all =
1.383 - searchf_unify_gen search_lr_all;
1.384 +val searchf_lr_unify_all = searchf_unify_gen search_lr_all;
1.385
1.386 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
1.387 -val searchf_lr_unify_valid =
1.388 - searchf_unify_gen (search_lr_valid valid_match_start);
1.389 +val searchf_lr_unify_valid = searchf_unify_gen (search_lr_valid valid_match_start);
1.390
1.391 -val searchf_bt_unify_valid =
1.392 - searchf_unify_gen (search_bt_valid valid_match_start);
1.393 +val searchf_bt_unify_valid = searchf_unify_gen (search_bt_valid valid_match_start);
1.394
1.395 (* apply a substitution in the conclusion of the theorem th *)
1.396 (* cfvs are certified free var placeholders for goal params *)
1.397 @@ -261,60 +246,61 @@
1.398 (* m is instantiation/match information *)
1.399 (* rule is the equation for substitution *)
1.400 fun apply_subst_in_concl ctxt i th (cfvs, conclthm) rule m =
1.401 - (RWInst.rw ctxt m rule conclthm)
1.402 - |> IsaND.unfix_frees cfvs
1.403 - |> RWInst.beta_eta_contract
1.404 - |> (fn r => Tactic.rtac r i th);
1.405 + RWInst.rw ctxt m rule conclthm
1.406 + |> IsaND.unfix_frees cfvs
1.407 + |> RWInst.beta_eta_contract
1.408 + |> (fn r => Tactic.rtac r i th);
1.409
1.410 (* substitute within the conclusion of goal i of gth, using a meta
1.411 equation rule. Note that we assume rule has var indicies zero'd *)
1.412 fun prep_concl_subst ctxt i gth =
1.413 - let
1.414 - val th = Thm.incr_indexes 1 gth;
1.415 - val tgt_term = Thm.prop_of th;
1.416 + let
1.417 + val th = Thm.incr_indexes 1 gth;
1.418 + val tgt_term = Thm.prop_of th;
1.419
1.420 - val sgn = Thm.theory_of_thm th;
1.421 - val ctermify = Thm.cterm_of sgn;
1.422 - val trivify = Thm.trivial o ctermify;
1.423 + val sgn = Thm.theory_of_thm th;
1.424 + val ctermify = Thm.cterm_of sgn;
1.425 + val trivify = Thm.trivial o ctermify;
1.426
1.427 - val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
1.428 - val cfvs = rev (map ctermify fvs);
1.429 + val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
1.430 + val cfvs = rev (map ctermify fvs);
1.431
1.432 - val conclterm = Logic.strip_imp_concl fixedbody;
1.433 - val conclthm = trivify conclterm;
1.434 - val maxidx = Thm.maxidx_of th;
1.435 - val ft = ((Zipper.move_down_right (* ==> *)
1.436 - o Zipper.move_down_left (* Trueprop *)
1.437 - o Zipper.mktop
1.438 - o Thm.prop_of) conclthm)
1.439 - in
1.440 - ((cfvs, conclthm), (sgn, maxidx, ft))
1.441 - end;
1.442 + val conclterm = Logic.strip_imp_concl fixedbody;
1.443 + val conclthm = trivify conclterm;
1.444 + val maxidx = Thm.maxidx_of th;
1.445 + val ft =
1.446 + (Zipper.move_down_right (* ==> *)
1.447 + o Zipper.move_down_left (* Trueprop *)
1.448 + o Zipper.mktop
1.449 + o Thm.prop_of) conclthm
1.450 + in
1.451 + ((cfvs, conclthm), (sgn, maxidx, ft))
1.452 + end;
1.453
1.454 (* substitute using an object or meta level equality *)
1.455 fun eqsubst_tac' ctxt searchf instepthm i th =
1.456 - let
1.457 - val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i th;
1.458 - val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
1.459 - fun rewrite_with_thm r =
1.460 - let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
1.461 - in searchf searchinfo lhs
1.462 - |> Seq.maps (apply_subst_in_concl ctxt i th cvfsconclthm r) end;
1.463 - in stepthms |> Seq.maps rewrite_with_thm end;
1.464 + let
1.465 + val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i th;
1.466 + val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
1.467 + fun rewrite_with_thm r =
1.468 + let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) in
1.469 + searchf searchinfo lhs
1.470 + |> Seq.maps (apply_subst_in_concl ctxt i th cvfsconclthm r)
1.471 + end;
1.472 + in stepthms |> Seq.maps rewrite_with_thm end;
1.473
1.474
1.475 (* distinct subgoals *)
1.476 -fun distinct_subgoals th =
1.477 - the_default th (SINGLE distinct_subgoals_tac th);
1.478 +fun distinct_subgoals th = the_default th (SINGLE distinct_subgoals_tac th);
1.479 +
1.480
1.481 (* General substitution of multiple occurances using one of
1.482 the given theorems*)
1.483
1.484 -
1.485 fun skip_first_occs_search occ srchf sinfo lhs =
1.486 - case (skipto_skipseq occ (srchf sinfo lhs)) of
1.487 - SkipMore _ => Seq.empty
1.488 - | SkipSeq ss => Seq.flat ss;
1.489 + (case (skipto_skipseq occ (srchf sinfo lhs)) of
1.490 + SkipMore _ => Seq.empty
1.491 + | SkipSeq ss => Seq.flat ss);
1.492
1.493 (* The occL is a list of integers indicating which occurence
1.494 w.r.t. the search order, to rewrite. Backtracking will also find later
1.495 @@ -322,50 +308,41 @@
1.496 just find all rewrites. *)
1.497
1.498 fun eqsubst_tac ctxt occL thms i th =
1.499 - let val nprems = Thm.nprems_of th in
1.500 - if nprems < i then Seq.empty else
1.501 - let val thmseq = (Seq.of_list thms)
1.502 - fun apply_occ occ th =
1.503 - thmseq |> Seq.maps
1.504 - (fn r => eqsubst_tac'
1.505 - ctxt
1.506 - (skip_first_occs_search
1.507 - occ searchf_lr_unify_valid) r
1.508 - (i + ((Thm.nprems_of th) - nprems))
1.509 - th);
1.510 - val sortedoccL =
1.511 - Library.sort (Library.rev_order o Library.int_ord) occL;
1.512 - in
1.513 - Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
1.514 - end
1.515 - end;
1.516 + let val nprems = Thm.nprems_of th in
1.517 + if nprems < i then Seq.empty else
1.518 + let
1.519 + val thmseq = (Seq.of_list thms);
1.520 + fun apply_occ occ th =
1.521 + thmseq |> Seq.maps (fn r =>
1.522 + eqsubst_tac' ctxt
1.523 + (skip_first_occs_search occ searchf_lr_unify_valid) r
1.524 + (i + ((Thm.nprems_of th) - nprems)) th);
1.525 + val sortedoccL = Library.sort (rev_order o int_ord) occL;
1.526 + in
1.527 + Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
1.528 + end
1.529 + end;
1.530
1.531
1.532 (* inthms are the given arguments in Isar, and treated as eqstep with
1.533 the first one, then the second etc *)
1.534 -fun eqsubst_meth ctxt occL inthms =
1.535 - SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
1.536 +fun eqsubst_meth ctxt occL inthms = SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
1.537
1.538 (* apply a substitution inside assumption j, keeps asm in the same place *)
1.539 -fun apply_subst_in_asm ctxt i th rule ((cfvs, j, ngoalprems, pth),m) =
1.540 - let
1.541 - val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
1.542 - val preelimrule =
1.543 - (RWInst.rw ctxt m rule pth)
1.544 - |> (Seq.hd o prune_params_tac)
1.545 - |> Thm.permute_prems 0 ~1 (* put old asm first *)
1.546 - |> IsaND.unfix_frees cfvs (* unfix any global params *)
1.547 - |> RWInst.beta_eta_contract; (* normal form *)
1.548 - (* val elimrule =
1.549 - preelimrule
1.550 - |> Tactic.make_elim (* make into elim rule *)
1.551 - |> Thm.lift_rule (th2, i); (* lift into context *)
1.552 - *)
1.553 - in
1.554 - (* ~j because new asm starts at back, thus we subtract 1 *)
1.555 - Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
1.556 +fun apply_subst_in_asm ctxt i th rule ((cfvs, j, _, pth),m) =
1.557 + let
1.558 + val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
1.559 + val preelimrule =
1.560 + RWInst.rw ctxt m rule pth
1.561 + |> (Seq.hd o prune_params_tac)
1.562 + |> Thm.permute_prems 0 ~1 (* put old asm first *)
1.563 + |> IsaND.unfix_frees cfvs (* unfix any global params *)
1.564 + |> RWInst.beta_eta_contract; (* normal form *)
1.565 + in
1.566 + (* ~j because new asm starts at back, thus we subtract 1 *)
1.567 + Seq.map (Thm.rotate_rule (~ j) ((Thm.nprems_of rule) + i))
1.568 (Tactic.dtac preelimrule i th2)
1.569 - end;
1.570 + end;
1.571
1.572
1.573 (* prepare to substitute within the j'th premise of subgoal i of gth,
1.574 @@ -375,83 +352,81 @@
1.575 assumption, i.e. this can be made more efficient for search over
1.576 multiple assumptions. *)
1.577 fun prep_subst_in_asm ctxt i gth j =
1.578 - let
1.579 - val th = Thm.incr_indexes 1 gth;
1.580 - val tgt_term = Thm.prop_of th;
1.581 + let
1.582 + val th = Thm.incr_indexes 1 gth;
1.583 + val tgt_term = Thm.prop_of th;
1.584
1.585 - val sgn = Thm.theory_of_thm th;
1.586 - val ctermify = Thm.cterm_of sgn;
1.587 - val trivify = Thm.trivial o ctermify;
1.588 + val sgn = Thm.theory_of_thm th;
1.589 + val ctermify = Thm.cterm_of sgn;
1.590 + val trivify = Thm.trivial o ctermify;
1.591
1.592 - val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
1.593 - val cfvs = rev (map ctermify fvs);
1.594 + val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
1.595 + val cfvs = rev (map ctermify fvs);
1.596
1.597 - val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
1.598 - val asm_nprems = length (Logic.strip_imp_prems asmt);
1.599 + val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
1.600 + val asm_nprems = length (Logic.strip_imp_prems asmt);
1.601
1.602 - val pth = trivify asmt;
1.603 - val maxidx = Thm.maxidx_of th;
1.604 + val pth = trivify asmt;
1.605 + val maxidx = Thm.maxidx_of th;
1.606
1.607 - val ft = ((Zipper.move_down_right (* trueprop *)
1.608 - o Zipper.mktop
1.609 - o Thm.prop_of) pth)
1.610 - in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
1.611 + val ft =
1.612 + (Zipper.move_down_right (* trueprop *)
1.613 + o Zipper.mktop
1.614 + o Thm.prop_of) pth
1.615 + in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
1.616
1.617 (* prepare subst in every possible assumption *)
1.618 fun prep_subst_in_asms ctxt i gth =
1.619 - map (prep_subst_in_asm ctxt i gth)
1.620 - ((fn l => Library.upto (1, length l))
1.621 - (Logic.prems_of_goal (Thm.prop_of gth) i));
1.622 + map (prep_subst_in_asm ctxt i gth)
1.623 + ((fn l => Library.upto (1, length l))
1.624 + (Logic.prems_of_goal (Thm.prop_of gth) i));
1.625
1.626
1.627 (* substitute in an assumption using an object or meta level equality *)
1.628 fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
1.629 - let
1.630 - val asmpreps = prep_subst_in_asms ctxt i th;
1.631 - val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
1.632 - fun rewrite_with_thm r =
1.633 - let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
1.634 - fun occ_search occ [] = Seq.empty
1.635 - | occ_search occ ((asminfo, searchinfo)::moreasms) =
1.636 - (case searchf searchinfo occ lhs of
1.637 - SkipMore i => occ_search i moreasms
1.638 - | SkipSeq ss =>
1.639 - Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
1.640 - (occ_search 1 moreasms))
1.641 - (* find later substs also *)
1.642 - in
1.643 - occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i th r)
1.644 - end;
1.645 - in stepthms |> Seq.maps rewrite_with_thm end;
1.646 + let
1.647 + val asmpreps = prep_subst_in_asms ctxt i th;
1.648 + val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
1.649 + fun rewrite_with_thm r =
1.650 + let
1.651 + val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
1.652 + fun occ_search occ [] = Seq.empty
1.653 + | occ_search occ ((asminfo, searchinfo)::moreasms) =
1.654 + (case searchf searchinfo occ lhs of
1.655 + SkipMore i => occ_search i moreasms
1.656 + | SkipSeq ss =>
1.657 + Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
1.658 + (occ_search 1 moreasms)) (* find later substs also *)
1.659 + in
1.660 + occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i th r)
1.661 + end;
1.662 + in stepthms |> Seq.maps rewrite_with_thm end;
1.663
1.664
1.665 fun skip_first_asm_occs_search searchf sinfo occ lhs =
1.666 - skipto_skipseq occ (searchf sinfo lhs);
1.667 + skipto_skipseq occ (searchf sinfo lhs);
1.668
1.669 fun eqsubst_asm_tac ctxt occL thms i th =
1.670 - let val nprems = Thm.nprems_of th
1.671 - in
1.672 - if nprems < i then Seq.empty else
1.673 - let val thmseq = (Seq.of_list thms)
1.674 + let val nprems = Thm.nprems_of th in
1.675 + if nprems < i then Seq.empty
1.676 + else
1.677 + let
1.678 + val thmseq = Seq.of_list thms;
1.679 fun apply_occ occK th =
1.680 - thmseq |> Seq.maps
1.681 - (fn r =>
1.682 - eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
1.683 - searchf_lr_unify_valid) occK r
1.684 - (i + ((Thm.nprems_of th) - nprems))
1.685 - th);
1.686 - val sortedoccs =
1.687 - Library.sort (Library.rev_order o Library.int_ord) occL
1.688 + thmseq |> Seq.maps (fn r =>
1.689 + eqsubst_asm_tac' ctxt
1.690 + (skip_first_asm_occs_search searchf_lr_unify_valid) occK r
1.691 + (i + ((Thm.nprems_of th) - nprems)) th);
1.692 + val sortedoccs = Library.sort (rev_order o int_ord) occL;
1.693 in
1.694 - Seq.map distinct_subgoals
1.695 - (Seq.EVERY (map apply_occ sortedoccs) th)
1.696 + Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccs) th)
1.697 end
1.698 - end;
1.699 + end;
1.700
1.701 (* inthms are the given arguments in Isar, and treated as eqstep with
1.702 the first one, then the second etc *)
1.703 fun eqsubst_asm_meth ctxt occL inthms =
1.704 - SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
1.705 + SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
1.706
1.707 (* combination method that takes a flag (true indicates that subst
1.708 should be done to an assumption, false = apply to the conclusion of