src/Tools/eqsubst.ML
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 58318 f95754ca7082
child 58826 2ed2eaabe3df
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30160
5f7b17941730 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
wenzelm
parents: 29269
diff changeset
     1
(*  Title:      Tools/eqsubst.ML
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 27809
diff changeset
     2
    Author:     Lucas Dixon, University of Edinburgh
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     3
52235
wenzelm
parents: 52234
diff changeset
     4
Perform a substitution using an equation.
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
     5
*)
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
     6
18591
04b9f2bf5a48 tuned EqSubst setup;
wenzelm
parents: 18011
diff changeset
     7
signature EQSUBST =
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     8
sig
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
     9
  type match =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    10
    ((indexname * (sort * typ)) list (* type instantiations *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    11
      * (indexname * (typ * term)) list) (* term instantiations *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    12
    * (string * typ) list (* fake named type abs env *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    13
    * (string * typ) list (* type abs env *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    14
    * term (* outer term *)
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    15
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    16
  type searchinfo =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    17
    theory
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    18
    * int (* maxidx *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    19
    * Zipper.T (* focusterm to search under *)
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    20
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    21
  datatype 'a skipseq = SkipMore of int | SkipSeq of 'a Seq.seq Seq.seq
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    22
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    23
  val skip_first_asm_occs_search: ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> int -> 'b -> 'c skipseq
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    24
  val skip_first_occs_search: int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    25
  val skipto_skipseq: int -> 'a Seq.seq Seq.seq -> 'a skipseq
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    26
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    27
  (* tactics *)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    28
  val eqsubst_asm_tac: Proof.context -> int list -> thm list -> int -> tactic
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    29
  val eqsubst_asm_tac': Proof.context ->
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    30
    (searchinfo -> int -> term -> match skipseq) -> int -> thm -> int -> tactic
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    31
  val eqsubst_tac: Proof.context ->
58318
f95754ca7082 fixed some spelling mistakes
blanchet
parents: 54742
diff changeset
    32
    int list -> (* list of occurrences to rewrite, use [0] for any *)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    33
    thm list -> int -> tactic
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    34
  val eqsubst_tac': Proof.context ->
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    35
    (searchinfo -> term -> match Seq.seq) (* search function *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    36
    -> thm (* equation theorem to rewrite with *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    37
    -> int (* subgoal number in goal theorem *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    38
    -> thm (* goal theorem *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    39
    -> thm Seq.seq (* rewritten goal theorem *)
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    40
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    41
  (* search for substitutions *)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    42
  val valid_match_start: Zipper.T -> bool
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    43
  val search_lr_all: Zipper.T -> Zipper.T Seq.seq
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    44
  val search_lr_valid: (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    45
  val searchf_lr_unify_all: searchinfo -> term -> match Seq.seq Seq.seq
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    46
  val searchf_lr_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    47
  val searchf_bt_unify_valid: searchinfo -> term -> match Seq.seq Seq.seq
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    48
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    49
  val setup : theory -> theory
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    50
end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    51
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
    52
structure EqSubst: EQSUBST =
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
    53
struct
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    54
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    55
(* changes object "=" to meta "==" which prepares a given rewrite rule *)
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    56
fun prep_meta_eq ctxt =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49340
diff changeset
    57
  Simplifier.mksimps ctxt #> map Drule.zero_var_indexes;
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    58
52246
54c0d4128b30 tuned signature;
wenzelm
parents: 52242
diff changeset
    59
(* make free vars into schematic vars with index zero *)
54c0d4128b30 tuned signature;
wenzelm
parents: 52242
diff changeset
    60
fun unfix_frees frees =
54c0d4128b30 tuned signature;
wenzelm
parents: 52242
diff changeset
    61
   fold (K (Thm.forall_elim_var 0)) frees o Drule.forall_intr_list frees;
54c0d4128b30 tuned signature;
wenzelm
parents: 52242
diff changeset
    62
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    63
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    64
type match =
52235
wenzelm
parents: 52234
diff changeset
    65
  ((indexname * (sort * typ)) list (* type instantiations *)
wenzelm
parents: 52234
diff changeset
    66
   * (indexname * (typ * term)) list) (* term instantiations *)
wenzelm
parents: 52234
diff changeset
    67
  * (string * typ) list (* fake named type abs env *)
wenzelm
parents: 52234
diff changeset
    68
  * (string * typ) list (* type abs env *)
wenzelm
parents: 52234
diff changeset
    69
  * term; (* outer term *)
15550
806214035275 lucas - added more comments and an extra type to clarify the code.
dixon
parents: 15538
diff changeset
    70
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    71
type searchinfo =
52235
wenzelm
parents: 52234
diff changeset
    72
  theory
wenzelm
parents: 52234
diff changeset
    73
  * int (* maxidx *)
wenzelm
parents: 52234
diff changeset
    74
  * Zipper.T; (* focusterm to search under *)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    75
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    76
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    77
(* skipping non-empty sub-sequences but when we reach the end
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    78
   of the seq, remembering how much we have left to skip. *)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    79
datatype 'a skipseq =
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    80
  SkipMore of int |
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    81
  SkipSeq of 'a Seq.seq Seq.seq;
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    82
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    83
(* given a seqseq, skip the first m non-empty seq's, note deficit *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    84
fun skipto_skipseq m s =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    85
  let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    86
    fun skip_occs n sq =
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    87
      (case Seq.pull sq of
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    88
        NONE => SkipMore n
52237
ab3ba550cbe7 simplified method setup;
wenzelm
parents: 52236
diff changeset
    89
      | SOME (h, t) =>
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    90
        (case Seq.pull h of
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    91
          NONE => skip_occs n t
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    92
        | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) else skip_occs (n - 1) t))
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    93
  in skip_occs m s end;
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    94
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    95
(* note: outerterm is the taget with the match replaced by a bound
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    96
   variable : ie: "P lhs" beocmes "%x. P x"
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    97
   insts is the types of instantiations of vars in lhs
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    98
   and typinsts is the type instantiations of types in the lhs
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
    99
   Note: Final rule is the rule lifted into the ontext of the
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   100
   taget thm. *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   101
fun mk_foo_match mkuptermfunc Ts t =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   102
  let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   103
    val ty = Term.type_of t
52235
wenzelm
parents: 52234
diff changeset
   104
    val bigtype = rev (map snd Ts) ---> ty
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   105
    fun mk_foo 0 t = t
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   106
      | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
52235
wenzelm
parents: 52234
diff changeset
   107
    val num_of_bnds = length Ts
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   108
    (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   109
    val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   110
  in Abs ("fooabs", bigtype, mkuptermfunc foo_term) end;
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   111
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   112
(* T is outer bound vars, n is number of locally bound vars *)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   113
(* THINK: is order of Ts correct...? or reversed? *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   114
fun mk_fake_bound_name n = ":b_" ^ n;
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   115
fun fakefree_badbounds Ts t =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   116
  let val (FakeTs, Ts, newnames) =
52242
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   117
    fold_rev (fn (n, ty) => fn (FakeTs, Ts, usednames) =>
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   118
      let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   119
        val newname = singleton (Name.variant_list usednames) n
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   120
      in
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   121
        ((mk_fake_bound_name newname, ty) :: FakeTs,
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   122
          (newname, ty) :: Ts,
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   123
          newname :: usednames)
52242
2d634bfa1bbf more standard fold/fold_rev;
wenzelm
parents: 52240
diff changeset
   124
      end) Ts ([], [], [])
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   125
  in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   126
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   127
(* before matching we need to fake the bound vars that are missing an
52235
wenzelm
parents: 52234
diff changeset
   128
   abstraction. In this function we additionally construct the
wenzelm
parents: 52234
diff changeset
   129
   abstraction environment, and an outer context term (with the focus
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   130
   abstracted out) for use in rewriting with RW_Inst.rw *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   131
fun prep_zipper_match z =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   132
  let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   133
    val t = Zipper.trm z
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   134
    val c = Zipper.ctxt z
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   135
    val Ts = Zipper.C.nty_ctxt c
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   136
    val (FakeTs', Ts', t') = fakefree_badbounds Ts t
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   137
    val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   138
  in
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   139
    (t', (FakeTs', Ts', absterm))
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   140
  end;
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   141
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   142
(* Unification with exception handled *)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   143
(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
52235
wenzelm
parents: 52234
diff changeset
   144
fun clean_unify thy ix (a as (pat, tgt)) =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   145
  let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   146
    (* type info will be re-derived, maybe this can be cached
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   147
       for efficiency? *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   148
    val pat_ty = Term.type_of pat;
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   149
    val tgt_ty = Term.type_of tgt;
52235
wenzelm
parents: 52234
diff changeset
   150
    (* FIXME is it OK to ignore the type instantiation info?
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   151
       or should I be using it? *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   152
    val typs_unify =
52235
wenzelm
parents: 52234
diff changeset
   153
      SOME (Sign.typ_unify thy (pat_ty, tgt_ty) (Vartab.empty, ix))
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   154
        handle Type.TUNIFY => NONE;
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   155
  in
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   156
    (case typs_unify of
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   157
      SOME (typinsttab, ix2) =>
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   158
        let
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   159
          (* FIXME is it right to throw away the flexes?
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   160
             or should I be using them somehow? *)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   161
          fun mk_insts env =
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   162
            (Vartab.dest (Envir.type_env env),
32032
a6a6e8031c14 tuned/modernized Envir operations;
wenzelm
parents: 31301
diff changeset
   163
             Vartab.dest (Envir.term_env env));
a6a6e8031c14 tuned/modernized Envir operations;
wenzelm
parents: 31301
diff changeset
   164
          val initenv =
a6a6e8031c14 tuned/modernized Envir operations;
wenzelm
parents: 31301
diff changeset
   165
            Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
52235
wenzelm
parents: 52234
diff changeset
   166
          val useq = Unify.smash_unifiers thy [a] initenv
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   167
            handle ListPair.UnequalLengths => Seq.empty
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   168
              | Term.TERM _ => Seq.empty;
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   169
          fun clean_unify' useq () =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   170
            (case (Seq.pull useq) of
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   171
               NONE => NONE
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   172
             | SOME (h, t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   173
            handle ListPair.UnequalLengths => NONE
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   174
              | Term.TERM _ => NONE;
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   175
        in
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   176
          (Seq.make (clean_unify' useq))
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   177
        end
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   178
    | NONE => Seq.empty)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   179
  end;
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   180
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   181
(* Unification for zippers *)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   182
(* Note: Ts is a modified version of the original names of the outer
52235
wenzelm
parents: 52234
diff changeset
   183
   bound variables. New names have been introduced to make sure they are
wenzelm
parents: 52234
diff changeset
   184
   unique w.r.t all names in the term and each other. usednames' is
wenzelm
parents: 52234
diff changeset
   185
   oldnames + new names. *)
wenzelm
parents: 52234
diff changeset
   186
fun clean_unify_z thy maxidx pat z =
wenzelm
parents: 52234
diff changeset
   187
  let val (t, (FakeTs, Ts, absterm)) = prep_zipper_match z in
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   188
    Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
52235
wenzelm
parents: 52234
diff changeset
   189
      (clean_unify thy maxidx (t, pat))
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   190
  end;
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   191
15550
806214035275 lucas - added more comments and an extra type to clarify the code.
dixon
parents: 15538
diff changeset
   192
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   193
fun bot_left_leaf_of (l $ _) = bot_left_leaf_of l
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   194
  | bot_left_leaf_of (Abs (_, _, t)) = bot_left_leaf_of t
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   195
  | bot_left_leaf_of x = x;
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   196
19975
ecd684d62808 fix to subst in order to allow subst when head of a term is a bound variable.
dixon
parents: 19871
diff changeset
   197
(* Avoid considering replacing terms which have a var at the head as
ecd684d62808 fix to subst in order to allow subst when head of a term is a bound variable.
dixon
parents: 19871
diff changeset
   198
   they always succeed trivially, and uninterestingly. *)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   199
fun valid_match_start z =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   200
  (case bot_left_leaf_of (Zipper.trm z) of
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   201
    Var _ => false
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   202
  | _ => true);
19975
ecd684d62808 fix to subst in order to allow subst when head of a term is a bound variable.
dixon
parents: 19871
diff changeset
   203
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   204
(* search from top, left to right, then down *)
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
   205
val search_lr_all = ZipperSearch.all_bl_ur;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   206
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   207
(* search from top, left to right, then down *)
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
   208
fun search_lr_valid validf =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   209
  let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   210
    fun sf_valid_td_lr z =
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   211
      let val here = if validf z then [Zipper.Here z] else [] in
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   212
        (case Zipper.trm z of
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   213
          _ $ _ =>
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   214
            [Zipper.LookIn (Zipper.move_down_left z)] @ here @
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   215
            [Zipper.LookIn (Zipper.move_down_right z)]
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   216
        | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   217
        | _ => here)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   218
      end;
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   219
  in Zipper.lzy_search sf_valid_td_lr end;
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   220
23064
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   221
(* search from bottom to top, left to right *)
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   222
fun search_bt_valid validf =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   223
  let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   224
    fun sf_valid_td_lr z =
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   225
      let val here = if validf z then [Zipper.Here z] else [] in
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   226
        (case Zipper.trm z of
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   227
          _ $ _ =>
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   228
            [Zipper.LookIn (Zipper.move_down_left z),
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   229
             Zipper.LookIn (Zipper.move_down_right z)] @ here
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   230
        | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   231
        | _ => here)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   232
      end;
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   233
  in Zipper.lzy_search sf_valid_td_lr end;
23064
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   234
52235
wenzelm
parents: 52234
diff changeset
   235
fun searchf_unify_gen f (thy, maxidx, z) lhs =
wenzelm
parents: 52234
diff changeset
   236
  Seq.map (clean_unify_z thy maxidx lhs) (Zipper.limit_apply f z);
23064
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   237
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   238
(* search all unifications *)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   239
val searchf_lr_unify_all = searchf_unify_gen search_lr_all;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   240
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   241
(* search only for 'valid' unifiers (non abs subterms and non vars) *)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   242
val searchf_lr_unify_valid = searchf_unify_gen (search_lr_valid valid_match_start);
15929
68bd1e16552a lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents: 15915
diff changeset
   243
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   244
val searchf_bt_unify_valid = searchf_unify_gen (search_bt_valid valid_match_start);
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   245
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   246
(* apply a substitution in the conclusion of the theorem *)
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   247
(* cfvs are certified free var placeholders for goal params *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   248
(* conclthm is a theorem of for just the conclusion *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   249
(* m is instantiation/match information *)
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   250
(* rule is the equation for substitution *)
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   251
fun apply_subst_in_concl ctxt i st (cfvs, conclthm) rule m =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   252
  RW_Inst.rw ctxt m rule conclthm
52246
54c0d4128b30 tuned signature;
wenzelm
parents: 52242
diff changeset
   253
  |> unfix_frees cfvs
52239
6a6033fa507c prefer existing beta_eta_conversion;
wenzelm
parents: 52238
diff changeset
   254
  |> Conv.fconv_rule Drule.beta_eta_conversion
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52246
diff changeset
   255
  |> (fn r => rtac r i st);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   256
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   257
(* substitute within the conclusion of goal i of gth, using a meta
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   258
equation rule. Note that we assume rule has var indicies zero'd *)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
   259
fun prep_concl_subst ctxt i gth =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   260
  let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   261
    val th = Thm.incr_indexes 1 gth;
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   262
    val tgt_term = Thm.prop_of th;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   263
52235
wenzelm
parents: 52234
diff changeset
   264
    val thy = Thm.theory_of_thm th;
wenzelm
parents: 52234
diff changeset
   265
    val cert = Thm.cterm_of thy;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   266
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   267
    val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
52235
wenzelm
parents: 52234
diff changeset
   268
    val cfvs = rev (map cert fvs);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   269
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   270
    val conclterm = Logic.strip_imp_concl fixedbody;
52235
wenzelm
parents: 52234
diff changeset
   271
    val conclthm = Thm.trivial (cert conclterm);
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   272
    val maxidx = Thm.maxidx_of th;
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   273
    val ft =
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   274
      (Zipper.move_down_right (* ==> *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   275
       o Zipper.move_down_left (* Trueprop *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   276
       o Zipper.mktop
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   277
       o Thm.prop_of) conclthm
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   278
  in
52235
wenzelm
parents: 52234
diff changeset
   279
    ((cfvs, conclthm), (thy, maxidx, ft))
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   280
  end;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   281
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   282
(* substitute using an object or meta level equality *)
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   283
fun eqsubst_tac' ctxt searchf instepthm i st =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   284
  let
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   285
    val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i st;
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   286
    val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   287
    fun rewrite_with_thm r =
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   288
      let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) in
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   289
        searchf searchinfo lhs
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   290
        |> Seq.maps (apply_subst_in_concl ctxt i st cvfsconclthm r)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   291
      end;
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   292
  in stepthms |> Seq.maps rewrite_with_thm end;
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   293
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   294
58318
f95754ca7082 fixed some spelling mistakes
blanchet
parents: 54742
diff changeset
   295
(* General substitution of multiple occurrences using one of
52235
wenzelm
parents: 52234
diff changeset
   296
   the given theorems *)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   297
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   298
fun skip_first_occs_search occ srchf sinfo lhs =
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   299
  (case skipto_skipseq occ (srchf sinfo lhs) of
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   300
    SkipMore _ => Seq.empty
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   301
  | SkipSeq ss => Seq.flat ss);
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   302
58318
f95754ca7082 fixed some spelling mistakes
blanchet
parents: 54742
diff changeset
   303
(* The "occs" argument is a list of integers indicating which occurrence
22727
473c7f67c64f Improved comments.
dixon
parents: 22578
diff changeset
   304
w.r.t. the search order, to rewrite. Backtracking will also find later
58318
f95754ca7082 fixed some spelling mistakes
blanchet
parents: 54742
diff changeset
   305
occurrences, but all earlier ones are skipped. Thus you can use [0] to
22727
473c7f67c64f Improved comments.
dixon
parents: 22578
diff changeset
   306
just find all rewrites. *)
473c7f67c64f Improved comments.
dixon
parents: 22578
diff changeset
   307
52238
d84ff5a93764 more standard names;
wenzelm
parents: 52237
diff changeset
   308
fun eqsubst_tac ctxt occs thms i st =
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   309
  let val nprems = Thm.nprems_of st in
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   310
    if nprems < i then Seq.empty else
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   311
    let
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   312
      val thmseq = Seq.of_list thms;
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   313
      fun apply_occ occ st =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   314
        thmseq |> Seq.maps (fn r =>
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   315
          eqsubst_tac' ctxt
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   316
            (skip_first_occs_search occ searchf_lr_unify_valid) r
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   317
            (i + (Thm.nprems_of st - nprems)) st);
52238
d84ff5a93764 more standard names;
wenzelm
parents: 52237
diff changeset
   318
      val sorted_occs = Library.sort (rev_order o int_ord) occs;
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   319
    in
52238
d84ff5a93764 more standard names;
wenzelm
parents: 52237
diff changeset
   320
      Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   321
    end
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   322
  end;
15959
366d39e95d3c lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents: 15936
diff changeset
   323
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   324
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   325
(* apply a substitution inside assumption j, keeps asm in the same place *)
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   326
fun apply_subst_in_asm ctxt i st rule ((cfvs, j, _, pth),m) =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   327
  let
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   328
    val st2 = Thm.rotate_rule (j - 1) i st; (* put premice first *)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   329
    val preelimrule =
52240
066c2ff17f7c misc tuning;
wenzelm
parents: 52239
diff changeset
   330
      RW_Inst.rw ctxt m rule pth
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 53168
diff changeset
   331
      |> (Seq.hd o prune_params_tac ctxt)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   332
      |> Thm.permute_prems 0 ~1 (* put old asm first *)
52246
54c0d4128b30 tuned signature;
wenzelm
parents: 52242
diff changeset
   333
      |> unfix_frees cfvs (* unfix any global params *)
52239
6a6033fa507c prefer existing beta_eta_conversion;
wenzelm
parents: 52238
diff changeset
   334
      |> Conv.fconv_rule Drule.beta_eta_conversion; (* normal form *)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   335
  in
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   336
    (* ~j because new asm starts at back, thus we subtract 1 *)
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52246
diff changeset
   337
    Seq.map (Thm.rotate_rule (~ j) (Thm.nprems_of rule + i)) (dtac preelimrule i st2)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   338
  end;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   339
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   340
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   341
(* prepare to substitute within the j'th premise of subgoal i of gth,
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   342
using a meta-level equation. Note that we assume rule has var indicies
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   343
zero'd. Note that we also assume that premt is the j'th premice of
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   344
subgoal i of gth. Note the repetition of work done for each
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   345
assumption, i.e. this can be made more efficient for search over
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   346
multiple assumptions.  *)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
   347
fun prep_subst_in_asm ctxt i gth j =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   348
  let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   349
    val th = Thm.incr_indexes 1 gth;
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   350
    val tgt_term = Thm.prop_of th;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   351
52235
wenzelm
parents: 52234
diff changeset
   352
    val thy = Thm.theory_of_thm th;
wenzelm
parents: 52234
diff changeset
   353
    val cert = Thm.cterm_of thy;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   354
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   355
    val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
52235
wenzelm
parents: 52234
diff changeset
   356
    val cfvs = rev (map cert fvs);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   357
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   358
    val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   359
    val asm_nprems = length (Logic.strip_imp_prems asmt);
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   360
52235
wenzelm
parents: 52234
diff changeset
   361
    val pth = Thm.trivial (cert asmt);
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   362
    val maxidx = Thm.maxidx_of th;
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   363
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   364
    val ft =
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   365
      (Zipper.move_down_right (* trueprop *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   366
         o Zipper.mktop
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   367
         o Thm.prop_of) pth
52235
wenzelm
parents: 52234
diff changeset
   368
  in ((cfvs, j, asm_nprems, pth), (thy, maxidx, ft)) end;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   369
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   370
(* prepare subst in every possible assumption *)
49340
25fc6e0da459 observe context more carefully when producing "fresh" variables -- for increased chances that method "subst" works in local context (including that of forked proofs);
wenzelm
parents: 49339
diff changeset
   371
fun prep_subst_in_asms ctxt i gth =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   372
  map (prep_subst_in_asm ctxt i gth)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   373
    ((fn l => Library.upto (1, length l))
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   374
      (Logic.prems_of_goal (Thm.prop_of gth) i));
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   375
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   376
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   377
(* substitute in an assumption using an object or meta level equality *)
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   378
fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i st =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   379
  let
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   380
    val asmpreps = prep_subst_in_asms ctxt i st;
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   381
    val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   382
    fun rewrite_with_thm r =
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   383
      let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   384
        val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   385
        fun occ_search occ [] = Seq.empty
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   386
          | occ_search occ ((asminfo, searchinfo)::moreasms) =
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   387
              (case searchf searchinfo occ lhs of
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   388
                SkipMore i => occ_search i moreasms
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   389
              | SkipSeq ss =>
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   390
                  Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   391
                    (occ_search 1 moreasms)) (* find later substs also *)
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   392
      in
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   393
        occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i st r)
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   394
      end;
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   395
  in stepthms |> Seq.maps rewrite_with_thm end;
15538
d8edf54cc28c lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents: 15486
diff changeset
   396
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   397
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   398
fun skip_first_asm_occs_search searchf sinfo occ lhs =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   399
  skipto_skipseq occ (searchf sinfo lhs);
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   400
52238
d84ff5a93764 more standard names;
wenzelm
parents: 52237
diff changeset
   401
fun eqsubst_asm_tac ctxt occs thms i st =
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   402
  let val nprems = Thm.nprems_of st in
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   403
    if nprems < i then Seq.empty
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   404
    else
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   405
      let
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   406
        val thmseq = Seq.of_list thms;
52238
d84ff5a93764 more standard names;
wenzelm
parents: 52237
diff changeset
   407
        fun apply_occ occ st =
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   408
          thmseq |> Seq.maps (fn r =>
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   409
            eqsubst_asm_tac' ctxt
52238
d84ff5a93764 more standard names;
wenzelm
parents: 52237
diff changeset
   410
              (skip_first_asm_occs_search searchf_lr_unify_valid) occ r
52236
fb82b42eb498 tuned -- prefer terminology of tactic / goal state;
wenzelm
parents: 52235
diff changeset
   411
              (i + (Thm.nprems_of st - nprems)) st);
52238
d84ff5a93764 more standard names;
wenzelm
parents: 52237
diff changeset
   412
        val sorted_occs = Library.sort (rev_order o int_ord) occs;
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   413
      in
52238
d84ff5a93764 more standard names;
wenzelm
parents: 52237
diff changeset
   414
        Seq.maps distinct_subgoals_tac (Seq.EVERY (map apply_occ sorted_occs) st)
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   415
      end
52234
6ffcce211047 misc tuning;
wenzelm
parents: 52223
diff changeset
   416
  end;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   417
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   418
(* combination method that takes a flag (true indicates that subst
31301
952d2d0c4446 minimal signature cleanup;
wenzelm
parents: 30513
diff changeset
   419
   should be done to an assumption, false = apply to the conclusion of
952d2d0c4446 minimal signature cleanup;
wenzelm
parents: 30513
diff changeset
   420
   the goal) as well as the theorems to use *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   421
val setup =
31301
952d2d0c4446 minimal signature cleanup;
wenzelm
parents: 30513
diff changeset
   422
  Method.setup @{binding subst}
53168
d998de7f0efc tuned signature;
wenzelm
parents: 52732
diff changeset
   423
    (Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
44095
3ea5fae095dc misc tuning and simplification;
wenzelm
parents: 43324
diff changeset
   424
        Attrib.thms >>
52238
d84ff5a93764 more standard names;
wenzelm
parents: 52237
diff changeset
   425
      (fn ((asm, occs), inthms) => fn ctxt =>
d84ff5a93764 more standard names;
wenzelm
parents: 52237
diff changeset
   426
        SIMPLE_METHOD' ((if asm then eqsubst_asm_tac else eqsubst_tac) ctxt occs inthms)))
31301
952d2d0c4446 minimal signature cleanup;
wenzelm
parents: 30513
diff changeset
   427
    "single-step substitution";
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   428
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   429
end;