src/Provers/eqsubst.ML
author wenzelm
Fri, 06 Jan 2006 18:18:16 +0100
changeset 18598 94d658871c98
parent 18591 04b9f2bf5a48
child 18708 4b3dadb4fe33
permissions -rw-r--r--
prep_meta_eq: reuse mk_rews of local simpset; adapted ML code to common conventions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
     1
(*  Title:      Provers/eqsubst.ML
16434
d17817dd61e9 added Id;
wenzelm
parents: 16007
diff changeset
     2
    ID:         $Id$
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
     3
    Author:     Lucas Dixon, University of Edinburgh, lucas.dixon@ed.ac.uk
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     4
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
     5
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
     6
*)
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
     7
18591
04b9f2bf5a48 tuned EqSubst setup;
wenzelm
parents: 18011
diff changeset
     8
signature EQSUBST =
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
     9
sig
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    10
  val setup : (Theory.theory -> Theory.theory) list
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    11
end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    12
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    13
structure EqSubst: EQSUBST =
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    14
struct
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
    15
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    16
fun prep_meta_eq ctxt =
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    17
  let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    18
  in mk #> map Drule.zero_var_indexes end;
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    19
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    20
15915
b0e8b37642a4 lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents: 15855
diff changeset
    21
  (* a type abriviation for match information *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    22
  type match =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    23
       ((indexname * (sort * typ)) list (* type instantiations *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    24
        * (indexname * (typ * term)) list) (* term instantiations *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    25
       * (string * typ) list (* fake named type abs env *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    26
       * (string * typ) list (* type abs env *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    27
       * term (* outer term *)
15550
806214035275 lucas - added more comments and an extra type to clarify the code.
dixon
parents: 15538
diff changeset
    28
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    29
  type searchinfo =
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
    30
       theory
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
    31
       * int (* maxidx *)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
    32
       * BasicIsaFTerm.FcTerm (* focusterm to search under *)
15550
806214035275 lucas - added more comments and an extra type to clarify the code.
dixon
parents: 15538
diff changeset
    33
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
    34
(* FOR DEBUGGING...
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
    35
type trace_subst_errT = int (* subgoal *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    36
        * thm (* thm with all goals *)
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
    37
        * (Thm.cterm list (* certified free var placeholders for vars *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    38
           * thm)  (* trivial thm of goal concl *)
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
    39
            (* possible matches/unifiers *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    40
        * thm (* rule *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    41
        * (((indexname * typ) list (* type instantiations *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    42
              * (indexname * term) list ) (* term instantiations *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    43
             * (string * typ) list (* Type abs env *)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    44
             * term) (* outer term *);
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
    45
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
    46
val trace_subst_err = (ref NONE : trace_subst_errT option ref);
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
    47
val trace_subst_search = ref false;
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
    48
exception trace_subst_exp of trace_subst_errT;
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
    49
 *)
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
    50
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
    51
(* search from top, left to right, then down *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    52
fun search_tlr_all_f f ft =
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    53
    let
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    54
      fun maux ft =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    55
          let val t' = (IsaFTerm.focus_of_fcterm ft)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    56
            (* val _ =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    57
                if !trace_subst_search then
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
    58
                  (writeln ("Examining: " ^ (TermLib.string_of_term t'));
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
    59
                   TermLib.writeterm t'; ())
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
    60
                else (); *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    61
          in
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    62
          (case t' of
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    63
            (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    64
                       Seq.cons(f ft,
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    65
                                  maux (IsaFTerm.focus_right ft)))
15929
68bd1e16552a lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents: 15915
diff changeset
    66
          | (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft))
68bd1e16552a lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents: 15915
diff changeset
    67
          | leaf => Seq.single (f ft)) end
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    68
    in maux ft end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    69
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
    70
(* search from top, left to right, then down *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    71
fun search_tlr_valid_f f ft =
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
    72
    let
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    73
      fun maux ft =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    74
          let
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
    75
            val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    76
          in
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    77
          (case (IsaFTerm.focus_of_fcterm ft) of
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    78
            (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    79
                       Seq.cons(hereseq,
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
    80
                                  maux (IsaFTerm.focus_right ft)))
15929
68bd1e16552a lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents: 15915
diff changeset
    81
          | (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft))
68bd1e16552a lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents: 15915
diff changeset
    82
          | leaf => Seq.single (hereseq))
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
    83
          end
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
    84
    in maux ft end;
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
    85
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
    86
(* search all unifications *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    87
fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    88
    IsaFTerm.find_fcterm_matches
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    89
      search_tlr_all_f
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
    90
      (IsaFTerm.clean_unify_ft sgn maxidx lhs)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
    91
      ft;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
    92
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
    93
(* search only for 'valid' unifiers (non abs subterms and non vars) *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    94
fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs  =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    95
    IsaFTerm.find_fcterm_matches
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
    96
      search_tlr_valid_f
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
    97
      (IsaFTerm.clean_unify_ft sgn maxidx lhs)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
    98
      ft;
15929
68bd1e16552a lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents: 15915
diff changeset
    99
15814
d65f461c8672 lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents: 15550
diff changeset
   100
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
   101
(* 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
   102
(* 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
   103
(* 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
   104
(* 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
   105
(* rule is the equation for substitution *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   106
fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
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
   107
    (RWInst.rw m rule conclthm)
15855
55e443aa711d lucas - updated to reflect isand.ML update
dixon
parents: 15814
diff changeset
   108
      |> 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
   109
      |> 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
   110
      |> (fn r => Tactic.rtac r i th);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   111
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   112
(* 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
   113
equation rule. Note that we assume rule has var indicies zero'd *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   114
fun prep_concl_subst i gth =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   115
    let
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   116
      val th = Thm.incr_indexes 1 gth;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   117
      val tgt_term = Thm.prop_of th;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   118
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   119
      val sgn = Thm.sign_of_thm th;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   120
      val ctermify = Thm.cterm_of sgn;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   121
      val trivify = Thm.trivial o ctermify;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   122
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   123
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   124
      val cfvs = rev (map ctermify fvs);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   125
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
   126
      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
   127
      val conclthm = trivify conclterm;
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
   128
      val maxidx = Term.maxidx_of_term conclterm;
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   129
      val ft = ((IsaFTerm.focus_right
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   130
                 o IsaFTerm.focus_left
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   131
                 o IsaFTerm.fcterm_of_term
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   132
                 o Thm.prop_of) conclthm)
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   133
    in
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   134
      ((cfvs, conclthm), (sgn, maxidx, ft))
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   135
    end;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   136
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   137
(* substitute using an object or meta level equality *)
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   138
fun eqsubst_tac' ctxt searchf instepthm i th =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   139
    let
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   140
      val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   141
      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
   142
      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
   143
          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
   144
          in searchf searchinfo lhs
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   145
             |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   146
    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
   147
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
   148
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   149
(* Tactic.distinct_subgoals_tac -- fails to free type variables *)
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
   150
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   151
(* custom version of distinct subgoals that works with term and
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   152
   type variables. Asssumes th is in beta-eta normal form.
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
   153
   Also, does nothing if flexflex contraints are present. *)
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
   154
fun distinct_subgoals th =
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
   155
    if List.null (Thm.tpairs_of th) then
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
   156
      let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th
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
   157
        val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm
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
   158
      in
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   159
        IsaND.unfix_frees_and_tfrees
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
   160
          fixes
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   161
          (Drule.implies_intr_list
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   162
             (Library.gen_distinct
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
   163
                (fn (x, y) => Thm.term_of x = Thm.term_of y)
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
   164
                cprems) fixedthconcl)
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
   165
      end
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
   166
    else 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
   167
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   168
(* General substiuttion 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
   169
   the given theorems*)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   170
exception eqsubst_occL_exp of
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   171
          string * (int list) * (thm list) * int * thm;
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   172
fun skip_first_occs_search occ srchf sinfo lhs =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   173
    case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   174
      IsaPLib.skipmore _ => Seq.empty
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   175
    | IsaPLib.skipseq ss => Seq.flat ss;
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   176
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   177
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
   178
    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
   179
      if nprems < i then Seq.empty else
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   180
      let val thmseq = (Seq.of_list thms)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   181
        fun apply_occ occ th =
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   182
            thmseq |> Seq.maps
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   183
                    (fn r => eqsubst_tac' ctxt (skip_first_occs_search
15936
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   184
                                    occ searchf_tlr_unify_valid) r
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   185
                                 (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
   186
                                 th);
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   187
        val sortedoccL =
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   188
            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
   189
      in
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   190
        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
   191
      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
   192
    end
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
   193
    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
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
   194
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   195
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   196
(* inthms are the given arguments in Isar, and treated as eqstep with
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   197
   the first one, then the second etc *)
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   198
fun eqsubst_meth ctxt occL inthms =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   199
    Method.METHOD
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
   200
      (fn facts =>
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   201
          HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac ctxt occL inthms));
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   202
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   203
(* apply a substitution inside assumption j, keeps asm in the same place *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   204
fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   205
    let
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   206
      val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   207
      val preelimrule =
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   208
          (RWInst.rw m rule pth)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   209
            |> (Seq.hd o Tactic.prune_params_tac)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   210
            |> 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
   211
            |> 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
   212
            |> RWInst.beta_eta_contract; (* normal form *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   213
  (*    val elimrule =
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   214
          preelimrule
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   215
            |> 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
   216
            |> 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
   217
   *)
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   218
    in
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   219
      (* ~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
   220
      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
   221
      (Tactic.dtac preelimrule i th2)
4dcccaa11a13 lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents: 16004
diff changeset
   222
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   223
      (* (Thm.bicompose
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   224
                 false (* use unification *)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   225
                 (true, (* elim resolution *)
16007
4dcccaa11a13 lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents: 16004
diff changeset
   226
                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
4dcccaa11a13 lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents: 16004
diff changeset
   227
                 i th2) *)
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   228
    end;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   229
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   230
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
   231
(* 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
   232
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
   233
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
   234
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
   235
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
   236
multiple assumptions.  *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   237
fun prep_subst_in_asm i gth j =
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   238
    let
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   239
      val th = Thm.incr_indexes 1 gth;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   240
      val tgt_term = Thm.prop_of th;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   241
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   242
      val sgn = Thm.sign_of_thm th;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   243
      val ctermify = Thm.cterm_of sgn;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   244
      val trivify = Thm.trivial o ctermify;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   245
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   246
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   247
      val cfvs = rev (map ctermify fvs);
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   248
18011
685d95c793ff cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents: 17795
diff changeset
   249
      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
   250
      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
   251
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
   252
      val pth = trivify 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
   253
      val maxidx = Term.maxidx_of_term 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
   254
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   255
      val ft = ((IsaFTerm.focus_right
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   256
                 o IsaFTerm.fcterm_of_term
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   257
                 o Thm.prop_of) pth)
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   258
    in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   259
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
   260
(* prepare subst in every possible assumption *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   261
fun prep_subst_in_asms i gth =
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   262
    map (prep_subst_in_asm i gth)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   263
        ((rev o IsaPLib.mk_num_list o length)
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   264
           (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
   265
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
   266
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
(* 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
   268
fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   269
    let
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   270
      val asmpreps = prep_subst_in_asms i th;
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   271
      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
   272
      fun rewrite_with_thm r =
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   273
          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
   274
            fun occ_search occ [] = Seq.empty
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   275
              | occ_search occ ((asminfo, searchinfo)::moreasms) =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   276
                (case searchf searchinfo occ lhs of
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   277
                   IsaPLib.skipmore i => occ_search i moreasms
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   278
                 | IsaPLib.skipseq ss =>
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   279
                   Seq.append (Seq.map (Library.pair asminfo)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   280
                                       (Seq.flat ss),
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   281
                               occ_search 1 moreasms))
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   282
                              (* find later substs also *)
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   283
          in
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   284
            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   285
          end;
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   286
    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
   287
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   288
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   289
fun skip_first_asm_occs_search searchf sinfo occ lhs =
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   290
    IsaPLib.skipto_seqseq occ (searchf sinfo lhs);
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   291
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   292
fun eqsubst_asm_tac ctxt occL thms i th =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   293
    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
   294
    in
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   295
      if nprems < i then Seq.empty else
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   296
      let val thmseq = (Seq.of_list thms)
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   297
        fun apply_occ occK th =
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   298
            thmseq |> Seq.maps
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   299
                    (fn r =>
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   300
                        eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   301
                                            searchf_tlr_unify_valid) occK r
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   302
                                         (i + ((Thm.nprems_of th) - nprems))
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   303
                                         th);
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   304
        val sortedoccs =
16004
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   305
            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
   306
      in
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   307
        Seq.map distinct_subgoals
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   308
                (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
   309
      end
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   310
    end
031f56012483 lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents: 15959
diff changeset
   311
    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   312
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   313
(* inthms are the given arguments in Isar, and treated as eqstep with
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   314
   the first one, then the second etc *)
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   315
fun eqsubst_asm_meth ctxt occL inthms =
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   316
    Method.METHOD
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
   317
      (fn facts =>
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   318
          HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac ctxt occL inthms ));
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   319
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   320
(* syntax for options, given "(asm)" will give back true, without
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   321
   gives back false *)
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   322
val options_syntax =
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   323
    (Args.parens (Args.$$$ "asm") >> (K true)) ||
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   324
     (Scan.succeed false);
15936
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   325
15929
68bd1e16552a lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents: 15915
diff changeset
   326
val ith_syntax =
15936
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   327
    (Args.parens (Scan.repeat Args.nat))
817ac93ee786 lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents: 15929
diff changeset
   328
      || (Scan.succeed [0]);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   329
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   330
(* combination method that takes a flag (true indicates that subst
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   331
should be done to an assumption, false = apply to the conclusion of
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   332
the goal) as well as the theorems to use *)
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   333
fun subst_meth src =
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   334
  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.local_thms) src
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   335
  #> (fn (ctxt, ((asmflag, occL), inthms)) =>
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   336
    (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   337
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   338
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   339
val setup =
18598
94d658871c98 prep_meta_eq: reuse mk_rews of local simpset;
wenzelm
parents: 18591
diff changeset
   340
  [Method.add_method ("subst", subst_meth, "substiution with an equation")];
15481
fc075ae929e4 the new subst tactic, by Lucas Dixon
paulson
parents:
diff changeset
   341
16978
e35b518bffc9 tuned signature;
wenzelm
parents: 16434
diff changeset
   342
end;