src/Tools/eqsubst.ML
author wenzelm
Wed, 29 May 2013 18:25:11 +0200
changeset 52223 5bb6ae8acb87
parent 51717 9e7d1c139569
child 52234 6ffcce211047
permissions -rw-r--r--
tuned signature -- more explicit flags for low-level Thm.bicompose;
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
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
     4
A proof method to perform a substiution using an equation.
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
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 27809
diff changeset
     9
  (* a type abbreviation for match information *)
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    10
  type match =
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    11
       ((indexname * (sort * typ)) list (* type instantiations *)
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    12
        * (indexname * (typ * term)) list) (* term instantiations *)
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    13
       * (string * typ) list (* fake named type abs env *)
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    14
       * (string * typ) list (* type abs env *)
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    15
       * term (* outer term *)
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    16
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    17
  type searchinfo =
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    18
       theory
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    19
       * int (* maxidx *)
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    20
       * Zipper.T (* focusterm to search under *)
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    21
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    22
  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
    23
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    24
  val skip_first_asm_occs_search :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    25
     ('a -> 'b -> 'c Seq.seq Seq.seq) ->
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    26
     'a -> int -> 'b -> 'c skipseq
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    27
  val skip_first_occs_search :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    28
     int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    29
  val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    30
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    31
  (* tactics *)
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    32
  val eqsubst_asm_tac :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    33
     Proof.context ->
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    34
     int list -> thm list -> int -> tactic
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    35
  val eqsubst_asm_tac' :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    36
     Proof.context ->
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    37
     (searchinfo -> int -> term -> match skipseq) ->
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    38
     int -> thm -> int -> tactic
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    39
  val eqsubst_tac :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    40
     Proof.context ->
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    41
     int list -> (* list of occurences to rewrite, use [0] for any *)
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    42
     thm list -> int -> tactic
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    43
  val eqsubst_tac' :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    44
     Proof.context -> (* proof context *)
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    45
     (searchinfo -> term -> match Seq.seq) (* search function *)
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    46
     -> thm (* equation theorem to rewrite with *)
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    47
     -> int (* subgoal number in goal theorem *)
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    48
     -> thm (* goal theorem *)
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    49
     -> thm Seq.seq (* rewritten goal theorem *)
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    50
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    51
  (* search for substitutions *)
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    52
  val valid_match_start : Zipper.T -> bool
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    53
  val search_lr_all : Zipper.T -> Zipper.T Seq.seq
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    54
  val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    55
  val searchf_lr_unify_all :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    56
     searchinfo -> term -> match Seq.seq Seq.seq
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    57
  val searchf_lr_unify_valid :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    58
     searchinfo -> term -> match Seq.seq Seq.seq
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    59
  val searchf_bt_unify_valid :
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    60
     searchinfo -> term -> match Seq.seq Seq.seq
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    61
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    62
  val setup : theory -> theory
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
    63
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    64
end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    65
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
    66
structure EqSubst: EQSUBST =
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
    67
struct
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    68
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    69
(* 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
    70
fun prep_meta_eq ctxt =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49340
diff changeset
    71
  Simplifier.mksimps ctxt #> map Drule.zero_var_indexes;
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    72
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    73
15915
b0e8b37642a4 lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents: 15855
diff changeset
    74
  (* a type abriviation for match information *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    75
  type match =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    76
       ((indexname * (sort * typ)) list (* type instantiations *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    77
        * (indexname * (typ * term)) list) (* term instantiations *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    78
       * (string * typ) list (* fake named type abs env *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    79
       * (string * typ) list (* type abs env *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    80
       * term (* outer term *)
15550
806214035275 lucas - added more comments and an extra type to clarify the code.
dixon
parents: 15538
diff changeset
    81
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    82
  type searchinfo =
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    83
       theory
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
    84
       * int (* maxidx *)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    85
       * Zipper.T (* focusterm to search under *)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    86
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    87
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    88
(* skipping non-empty sub-sequences but when we reach the end
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    89
   of the seq, remembering how much we have left to skip. *)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    90
datatype 'a skipseq = SkipMore of int
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    91
  | SkipSeq of 'a Seq.seq Seq.seq;
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    92
(* 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
    93
fun skipto_skipseq m s =
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    94
    let
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    95
      fun skip_occs n sq =
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    96
          case Seq.pull sq of
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    97
            NONE => SkipMore n
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
    98
          | SOME (h,t) =>
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
    99
            (case Seq.pull h of NONE => skip_occs n t
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   100
             | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   101
                         else skip_occs (n - 1) t)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   102
    in (skip_occs m s) end;
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   103
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   104
(* note: outerterm is the taget with the match replaced by a bound
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   105
         variable : ie: "P lhs" beocmes "%x. P x"
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   106
         insts is the types of instantiations of vars in lhs
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   107
         and typinsts is the type instantiations of types in the lhs
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   108
         Note: Final rule is the rule lifted into the ontext of the
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   109
         taget thm. *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   110
fun mk_foo_match mkuptermfunc Ts t =
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   111
    let
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   112
      val ty = Term.type_of t
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   113
      val bigtype = (rev (map snd Ts)) ---> ty
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   114
      fun mk_foo 0 t = t
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   115
        | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   116
      val num_of_bnds = (length Ts)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   117
      (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   118
      val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   119
    in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   120
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   121
(* 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
   122
(* 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
   123
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
   124
fun fakefree_badbounds Ts t =
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   125
    let val (FakeTs,Ts,newnames) =
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   126
            List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
43324
2b47822868e4 discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents: 41164
diff changeset
   127
                           let val newname = singleton (Name.variant_list usednames) n
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   128
                           in ((mk_fake_bound_name newname,ty)::FakeTs,
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   129
                               (newname,ty)::Ts,
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   130
                               newname::usednames) end)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   131
                       ([],[],[])
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   132
                       Ts
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   133
    in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   134
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   135
(* before matching we need to fake the bound vars that are missing an
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   136
abstraction. In this function we additionally construct the
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   137
abstraction environment, and an outer context term (with the focus
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   138
abstracted out) for use in rewriting with RWInst.rw *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   139
fun prep_zipper_match z =
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   140
    let
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   141
      val t = Zipper.trm z
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   142
      val c = Zipper.ctxt z
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   143
      val Ts = Zipper.C.nty_ctxt c
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   144
      val (FakeTs', Ts', t') = fakefree_badbounds Ts t
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   145
      val absterm = mk_foo_match (Zipper.C.apply c) Ts' t'
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   146
    in
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   147
      (t', (FakeTs', Ts', absterm))
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   148
    end;
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   149
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   150
(* Unification with exception handled *)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   151
(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
27033
6ef5134fc631 fixed bug: maxidx was wrongly calculuated from term, now calculated
dixon
parents: 23064
diff changeset
   152
fun clean_unify thry ix (a as (pat, tgt)) =
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   153
    let
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   154
      (* type info will be re-derived, maybe this can be cached
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   155
         for efficiency? *)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   156
      val pat_ty = Term.type_of pat;
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   157
      val tgt_ty = Term.type_of tgt;
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   158
      (* is it OK to ignore the type instantiation info?
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   159
         or should I be using it? *)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   160
      val typs_unify =
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents: 27809
diff changeset
   161
          SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   162
            handle Type.TUNIFY => NONE;
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   163
    in
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   164
      case typs_unify of
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   165
        SOME (typinsttab, ix2) =>
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   166
        let
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   167
      (* is it right to throw away the flexes?
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   168
         or should I be using them somehow? *)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   169
          fun mk_insts env =
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   170
            (Vartab.dest (Envir.type_env env),
32032
a6a6e8031c14 tuned/modernized Envir operations;
wenzelm
parents: 31301
diff changeset
   171
             Vartab.dest (Envir.term_env env));
a6a6e8031c14 tuned/modernized Envir operations;
wenzelm
parents: 31301
diff changeset
   172
          val initenv =
a6a6e8031c14 tuned/modernized Envir operations;
wenzelm
parents: 31301
diff changeset
   173
            Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
27033
6ef5134fc631 fixed bug: maxidx was wrongly calculuated from term, now calculated
dixon
parents: 23064
diff changeset
   174
          val useq = Unify.smash_unifiers thry [a] initenv
40722
441260986b63 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents: 36960
diff changeset
   175
              handle ListPair.UnequalLengths => Seq.empty
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 32740
diff changeset
   176
                   | Term.TERM _ => Seq.empty;
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   177
          fun clean_unify' useq () =
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   178
              (case (Seq.pull useq) of
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   179
                 NONE => NONE
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   180
               | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
40722
441260986b63 make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
wenzelm
parents: 36960
diff changeset
   181
              handle ListPair.UnequalLengths => NONE
27033
6ef5134fc631 fixed bug: maxidx was wrongly calculuated from term, now calculated
dixon
parents: 23064
diff changeset
   182
                   | Term.TERM _ => NONE
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   183
        in
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   184
          (Seq.make (clean_unify' useq))
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   185
        end
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   186
      | NONE => Seq.empty
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   187
    end;
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   188
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   189
(* Unification for zippers *)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   190
(* Note: Ts is a modified version of the original names of the outer
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   191
bound variables. New names have been introduced to make sure they are
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   192
unique w.r.t all names in the term and each other. usednames' is
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   193
oldnames + new names. *)
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   194
(* ix = max var index *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   195
fun clean_unify_z sgn ix pat z =
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   196
    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
   197
    Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   198
            (clean_unify sgn ix (t, pat)) end;
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   199
15550
806214035275 lucas - added more comments and an extra type to clarify the code.
dixon
parents: 15538
diff changeset
   200
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   201
fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   202
  | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   203
  | 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
   204
19975
ecd684d62808 fix to subst in order to allow subst when head of a term is a bound variable.
dixon
parents: 19871
diff changeset
   205
(* 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
   206
   they always succeed trivially, and uninterestingly. *)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   207
fun valid_match_start z =
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   208
    (case bot_left_leaf_of (Zipper.trm z) of
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   209
      Var _ => false
19975
ecd684d62808 fix to subst in order to allow subst when head of a term is a bound variable.
dixon
parents: 19871
diff changeset
   210
      | _ => true);
ecd684d62808 fix to subst in order to allow subst when head of a term is a bound variable.
dixon
parents: 19871
diff changeset
   211
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   212
(* search from top, left to right, then down *)
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
   213
val search_lr_all = ZipperSearch.all_bl_ur;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   214
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   215
(* search from top, left to right, then down *)
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
   216
fun search_lr_valid validf =
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   217
    let
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   218
      fun sf_valid_td_lr z =
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   219
          let val here = if validf z then [Zipper.Here z] else [] in
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   220
            case Zipper.trm z
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   221
             of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)]
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   222
                         @ here
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   223
                         @ [Zipper.LookIn (Zipper.move_down_right z)]
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   224
              | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   225
              | _ => here
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   226
          end;
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   227
    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
   228
23064
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   229
(* search from bottom to top, left to right *)
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   230
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   231
fun search_bt_valid validf =
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   232
    let
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   233
      fun sf_valid_td_lr z =
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   234
          let val here = if validf z then [Zipper.Here z] else [] in
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   235
            case Zipper.trm z
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   236
             of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z),
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   237
                          Zipper.LookIn (Zipper.move_down_right z)] @ here
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   238
              | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
23064
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   239
              | _ => here
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   240
          end;
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   241
    in Zipper.lzy_search sf_valid_td_lr end;
23064
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   242
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   243
fun searchf_unify_gen f (sgn, maxidx, z) lhs =
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   244
    Seq.map (clean_unify_z sgn maxidx lhs)
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   245
            (Zipper.limit_apply f z);
23064
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   246
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   247
(* search all unifications *)
23064
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   248
val searchf_lr_unify_all =
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   249
    searchf_unify_gen search_lr_all;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   250
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   251
(* search only for 'valid' unifiers (non abs subterms and non vars) *)
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   252
val searchf_lr_unify_valid =
23064
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   253
    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
   254
23064
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   255
val searchf_bt_unify_valid =
6ee131d1a618 add a bottom up search function
narboux
parents: 22727
diff changeset
   256
    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
   257
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
(* apply a substitution in the conclusion of the theorem th *)
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
   259
(* 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
   260
(* 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
   261
(* 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
   262
(* rule is the equation for substitution *)
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
   263
fun apply_subst_in_concl ctxt i th (cfvs, conclthm) rule m =
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
   264
    (RWInst.rw ctxt m rule conclthm)
15855
55e443aa711d lucas - updated to reflect isand.ML update
dixon
parents: 15814
diff changeset
   265
      |> IsaND.unfix_frees cfvs
15915
b0e8b37642a4 lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents: 15855
diff changeset
   266
      |> RWInst.beta_eta_contract
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
   267
      |> (fn r => Tactic.rtac r i th);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   268
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   269
(* 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
   270
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
   271
fun prep_concl_subst ctxt i gth =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   272
    let
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   273
      val th = Thm.incr_indexes 1 gth;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   274
      val tgt_term = Thm.prop_of th;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   275
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 21879
diff changeset
   276
      val sgn = Thm.theory_of_thm th;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   277
      val ctermify = Thm.cterm_of sgn;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   278
      val trivify = Thm.trivial o ctermify;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   279
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
   280
      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   281
      val cfvs = rev (map ctermify fvs);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   282
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
   283
      val conclterm = Logic.strip_imp_concl fixedbody;
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
   284
      val conclthm = trivify conclterm;
27033
6ef5134fc631 fixed bug: maxidx was wrongly calculuated from term, now calculated
dixon
parents: 23064
diff changeset
   285
      val maxidx = Thm.maxidx_of th;
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   286
      val ft = ((Zipper.move_down_right (* ==> *)
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   287
                 o Zipper.move_down_left (* Trueprop *)
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   288
                 o Zipper.mktop
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   289
                 o Thm.prop_of) conclthm)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   290
    in
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   291
      ((cfvs, conclthm), (sgn, maxidx, ft))
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   292
    end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   293
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   294
(* substitute using an object or meta level equality *)
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   295
fun eqsubst_tac' ctxt searchf instepthm i th =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   296
    let
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
   297
      val (cvfsconclthm, searchinfo) = prep_concl_subst ctxt i th;
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   298
      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
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
   299
      fun rewrite_with_thm r =
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
   300
          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   301
          in searchf searchinfo lhs
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
   302
             |> Seq.maps (apply_subst_in_concl ctxt i th cvfsconclthm r) end;
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   303
    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
   304
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
   305
19047
670ce193b618 used Tactic.distinct_subgoals_tac;
wenzelm
parents: 18988
diff changeset
   306
(* distinct subgoals *)
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
   307
fun distinct_subgoals th =
19047
670ce193b618 used Tactic.distinct_subgoals_tac;
wenzelm
parents: 18988
diff changeset
   308
  the_default th (SINGLE distinct_subgoals_tac 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
   309
19047
670ce193b618 used Tactic.distinct_subgoals_tac;
wenzelm
parents: 18988
diff changeset
   310
(* General substitution of multiple occurances using one of
15936
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   311
   the given theorems*)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   312
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   313
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   314
fun skip_first_occs_search occ srchf sinfo lhs =
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   315
    case (skipto_skipseq occ (srchf sinfo lhs)) of
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   316
      SkipMore _ => Seq.empty
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   317
    | SkipSeq ss => Seq.flat ss;
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   318
22727
473c7f67c64f Improved comments.
dixon
parents: 22578
diff changeset
   319
(* The occL is a list of integers indicating which occurence
473c7f67c64f Improved comments.
dixon
parents: 22578
diff changeset
   320
w.r.t. the search order, to rewrite. Backtracking will also find later
473c7f67c64f Improved comments.
dixon
parents: 22578
diff changeset
   321
occurences, but all earlier ones are skipped. Thus you can use [0] to
473c7f67c64f Improved comments.
dixon
parents: 22578
diff changeset
   322
just find all rewrites. *)
473c7f67c64f Improved comments.
dixon
parents: 22578
diff changeset
   323
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   324
fun eqsubst_tac ctxt occL thms i th =
15936
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   325
    let val nprems = Thm.nprems_of th in
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   326
      if nprems < i then Seq.empty else
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   327
      let val thmseq = (Seq.of_list thms)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   328
        fun apply_occ occ th =
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   329
            thmseq |> Seq.maps
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   330
                    (fn r => eqsubst_tac'
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   331
                               ctxt
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   332
                               (skip_first_occs_search
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
   333
                                  occ searchf_lr_unify_valid) r
15936
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   334
                                 (i + ((Thm.nprems_of th) - nprems))
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   335
                                 th);
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   336
        val sortedoccL =
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   337
            Library.sort (Library.rev_order o Library.int_ord) occL;
15936
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   338
      in
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   339
        Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
15936
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   340
      end
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   341
    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
   342
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   343
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   344
(* inthms are the given arguments in Isar, and treated as eqstep with
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   345
   the first one, then the second etc *)
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   346
fun eqsubst_meth ctxt occL inthms =
30510
4120fc59dd85 unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents: 30318
diff changeset
   347
    SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   348
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   349
(* apply a substitution inside assumption j, keeps asm in the same place *)
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
   350
fun apply_subst_in_asm ctxt i th rule ((cfvs, j, ngoalprems, pth),m) =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   351
    let
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   352
      val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   353
      val preelimrule =
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
   354
          (RWInst.rw ctxt m rule pth)
21708
45e7491bea47 reorganized structure Tactic vs. MetaSimplifier;
wenzelm
parents: 21588
diff changeset
   355
            |> (Seq.hd o prune_params_tac)
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   356
            |> Thm.permute_prems 0 ~1 (* put old asm first *)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   357
            |> IsaND.unfix_frees cfvs (* unfix any global params *)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   358
            |> RWInst.beta_eta_contract; (* normal form *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   359
  (*    val elimrule =
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   360
          preelimrule
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   361
            |> Tactic.make_elim (* make into elim rule *)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   362
            |> Thm.lift_rule (th2, i); (* lift into context *)
16007
4dcccaa11a13 lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents: 16004
diff changeset
   363
   *)
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   364
    in
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   365
      (* ~j because new asm starts at back, thus we subtract 1 *)
16007
4dcccaa11a13 lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents: 16004
diff changeset
   366
      Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
4dcccaa11a13 lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents: 16004
diff changeset
   367
      (Tactic.dtac preelimrule i th2)
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   368
    end;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   369
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   370
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
   371
(* 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
   372
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
   373
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
   374
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
   375
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
   376
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
   377
fun prep_subst_in_asm ctxt i gth j =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   378
    let
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   379
      val th = Thm.incr_indexes 1 gth;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   380
      val tgt_term = Thm.prop_of th;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   381
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 21879
diff changeset
   382
      val sgn = Thm.theory_of_thm th;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   383
      val ctermify = Thm.cterm_of sgn;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   384
      val trivify = Thm.trivial o ctermify;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   385
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
   386
      val (fixedbody, fvs) = IsaND.fix_alls_term ctxt i tgt_term;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   387
      val cfvs = rev (map ctermify fvs);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   388
18011
685d95c793ff cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents: 17795
diff changeset
   389
      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
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
   390
      val asm_nprems = length (Logic.strip_imp_prems asmt);
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
   391
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
   392
      val pth = trivify asmt;
27033
6ef5134fc631 fixed bug: maxidx was wrongly calculuated from term, now calculated
dixon
parents: 23064
diff changeset
   393
      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
   394
41164
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   395
      val ft = ((Zipper.move_down_right (* trueprop *)
6854e9a40edc avoid ML structure aliases (especially single-letter abbreviations);
wenzelm
parents: 40722
diff changeset
   396
                 o Zipper.mktop
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   397
                 o Thm.prop_of) pth)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   398
    in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   399
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
   400
(* 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
   401
fun prep_subst_in_asms ctxt i gth =
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
   402
    map (prep_subst_in_asm ctxt i gth)
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   403
        ((fn l => Library.upto (1, length l))
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   404
           (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
   405
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
   406
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
   407
(* substitute in an assumption using an object or meta level equality *)
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   408
fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   409
    let
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
   410
      val asmpreps = prep_subst_in_asms ctxt i th;
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   411
      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   412
      fun rewrite_with_thm r =
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   413
          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   414
            fun occ_search occ [] = Seq.empty
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   415
              | occ_search occ ((asminfo, searchinfo)::moreasms) =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   416
                (case searchf searchinfo occ lhs of
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   417
                   SkipMore i => occ_search i moreasms
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   418
                 | SkipSeq ss =>
19861
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19835
diff changeset
   419
                   Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
620d90091788 tuned Seq/Envir/Unify interfaces;
wenzelm
parents: 19835
diff changeset
   420
                               (occ_search 1 moreasms))
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   421
                              (* find later substs also *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   422
          in
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
   423
            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm ctxt i th r)
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   424
          end;
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   425
    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
   426
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   427
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   428
fun skip_first_asm_occs_search searchf sinfo occ lhs =
19835
81d6dc597559 added updated version of IsaPlanner and substitution.
dixon
parents: 19473
diff changeset
   429
    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
   430
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   431
fun eqsubst_asm_tac ctxt occL thms i th =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   432
    let val nprems = Thm.nprems_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
   433
    in
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   434
      if nprems < i then Seq.empty else
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   435
      let val thmseq = (Seq.of_list thms)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   436
        fun apply_occ occK th =
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   437
            thmseq |> Seq.maps
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   438
                    (fn r =>
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   439
                        eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
19871
88e8f6173bab Corrected search order for zippers.
dixon
parents: 19861
diff changeset
   440
                                            searchf_lr_unify_valid) occK r
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   441
                                         (i + ((Thm.nprems_of th) - nprems))
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   442
                                         th);
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   443
        val sortedoccs =
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   444
            Library.sort (Library.rev_order o Library.int_ord) occL
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   445
      in
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   446
        Seq.map distinct_subgoals
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   447
                (Seq.EVERY (map apply_occ sortedoccs) th)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   448
      end
49339
d1fcb4de8349 eliminated some old material that is unused in the visible universe;
wenzelm
parents: 44095
diff changeset
   449
    end;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   450
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   451
(* inthms are the given arguments in Isar, and treated as eqstep with
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   452
   the first one, then the second etc *)
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   453
fun eqsubst_asm_meth ctxt occL inthms =
30510
4120fc59dd85 unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents: 30318
diff changeset
   454
    SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   455
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   456
(* combination method that takes a flag (true indicates that subst
31301
952d2d0c4446 minimal signature cleanup;
wenzelm
parents: 30513
diff changeset
   457
   should be done to an assumption, false = apply to the conclusion of
952d2d0c4446 minimal signature cleanup;
wenzelm
parents: 30513
diff changeset
   458
   the goal) as well as the theorems to use *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   459
val setup =
31301
952d2d0c4446 minimal signature cleanup;
wenzelm
parents: 30513
diff changeset
   460
  Method.setup @{binding subst}
44095
3ea5fae095dc misc tuning and simplification;
wenzelm
parents: 43324
diff changeset
   461
    (Args.mode "asm" -- Scan.lift (Scan.optional (Args.parens (Scan.repeat Parse.nat)) [0]) --
3ea5fae095dc misc tuning and simplification;
wenzelm
parents: 43324
diff changeset
   462
        Attrib.thms >>
3ea5fae095dc misc tuning and simplification;
wenzelm
parents: 43324
diff changeset
   463
      (fn ((asm, occL), inthms) => fn ctxt =>
3ea5fae095dc misc tuning and simplification;
wenzelm
parents: 43324
diff changeset
   464
        (if asm then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
31301
952d2d0c4446 minimal signature cleanup;
wenzelm
parents: 30513
diff changeset
   465
    "single-step substitution";
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   466
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   467
end;