src/Provers/eqsubst.ML
author paulson
Tue Feb 01 18:01:57 2005 +0100 (2005-02-01)
changeset 15481 fc075ae929e4
child 15486 06a32fe35ec3
permissions -rw-r--r--
the new subst tactic, by Lucas Dixon
paulson@15481
     1
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
paulson@15481
     2
(*  Title:      sys/eqsubst_tac.ML
paulson@15481
     3
    Author:     Lucas Dixon, University of Edinburgh
paulson@15481
     4
                lucas.dixon@ed.ac.uk
paulson@15481
     5
    Created:    29 Jan 2005
paulson@15481
     6
*)
paulson@15481
     7
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
paulson@15481
     8
(*  DESCRIPTION:
paulson@15481
     9
paulson@15481
    10
    A Tactic to perform a substiution using an equation.
paulson@15481
    11
paulson@15481
    12
*)
paulson@15481
    13
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
paulson@15481
    14
paulson@15481
    15
(* Logic specific data *)
paulson@15481
    16
signature EQRULE_DATA =
paulson@15481
    17
sig
paulson@15481
    18
  (* to make a meta equality theorem in the current logic *)
paulson@15481
    19
  val prep_meta_eq : thm -> thm list
paulson@15481
    20
end;
paulson@15481
    21
paulson@15481
    22
(* the signature of an instance of the SQSUBST tactic *)
paulson@15481
    23
signature EQSUBST_TAC = 
paulson@15481
    24
sig
paulson@15481
    25
  val eqsubst_asm_meth : Thm.thm list -> Proof.method
paulson@15481
    26
  val eqsubst_asm_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
paulson@15481
    27
  val eqsubst_asm_tac' : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
paulson@15481
    28
  val eqsubst_meth : Thm.thm list -> Proof.method
paulson@15481
    29
  val eqsubst_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
paulson@15481
    30
  val eqsubst_tac' : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
paulson@15481
    31
  val meth : bool * Thm.thm list -> Proof.context -> Proof.method
paulson@15481
    32
  val subst : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
paulson@15481
    33
  val subst_asm : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
paulson@15481
    34
paulson@15481
    35
  val setup : (Theory.theory -> Theory.theory) list
paulson@15481
    36
end;
paulson@15481
    37
paulson@15481
    38
functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA) 
paulson@15481
    39
(* : EQSUBST_TAC *)
paulson@15481
    40
= struct
paulson@15481
    41
paulson@15481
    42
fun search_tb_lr_f f ft = 
paulson@15481
    43
    let
paulson@15481
    44
      fun maux ft = 
paulson@15481
    45
          let val t' = (IsaFTerm.focus_of_fcterm ft) 
paulson@15481
    46
     (*   val _ = writeln ("Examining: " ^ (TermLib.string_of_term t')) *)
paulson@15481
    47
          in 
paulson@15481
    48
          (case t' of 
paulson@15481
    49
            (_ $ _) => Seq.append(f ft, 
paulson@15481
    50
                       Seq.append(maux (IsaFTerm.focus_left ft), 
paulson@15481
    51
                                  maux (IsaFTerm.focus_right ft)))
paulson@15481
    52
          | (Abs _) => Seq.append (f ft, maux (IsaFTerm.focus_abs ft))
paulson@15481
    53
          | leaf => f ft) end
paulson@15481
    54
    in maux ft end;
paulson@15481
    55
paulson@15481
    56
fun search_for_match sgn lhs maxidx = 
paulson@15481
    57
    IsaFTerm.find_fcterm_matches 
paulson@15481
    58
      search_tb_lr_f 
paulson@15481
    59
      (IsaFTerm.clean_unify_ft sgn maxidx lhs);
paulson@15481
    60
paulson@15481
    61
paulson@15481
    62
(* CLEANUP: lots of duplication of code for substituting in
paulson@15481
    63
assumptions and conclusion - this could be cleaned up a little. *)
paulson@15481
    64
paulson@15481
    65
fun subst_concl rule cfvs i th (conclthm, concl_matches)= 
paulson@15481
    66
    let 
paulson@15481
    67
      fun apply_subst m = 
paulson@15481
    68
          (RWInst.rw m rule conclthm)
paulson@15481
    69
            |> IsaND.schemify_frees_to_vars cfvs
paulson@15481
    70
            |> RWInst.beta_eta_contract_tac
paulson@15481
    71
            |> (fn r => Tactic.rtac r i th)
paulson@15481
    72
            |> Seq.map Drule.zero_var_indexes
paulson@15481
    73
    in
paulson@15481
    74
      Seq.flat (Seq.map apply_subst concl_matches)
paulson@15481
    75
    end;
paulson@15481
    76
paulson@15481
    77
paulson@15481
    78
(* substitute within the conclusion of goal i of gth, using a meta
paulson@15481
    79
equation rule *)
paulson@15481
    80
fun subst rule i gth = 
paulson@15481
    81
    let 
paulson@15481
    82
      val th = Thm.incr_indexes 1 gth;
paulson@15481
    83
      val tgt_term = Thm.prop_of th;
paulson@15481
    84
      val maxidx = Term.maxidx_of_term tgt_term;
paulson@15481
    85
paulson@15481
    86
      val rule' = Drule.zero_var_indexes rule;
paulson@15481
    87
      val (lhs,_) = Logic.dest_equals (Thm.concl_of rule');
paulson@15481
    88
paulson@15481
    89
      val sgn = Thm.sign_of_thm th;
paulson@15481
    90
      val ctermify = Thm.cterm_of sgn;
paulson@15481
    91
      val trivify = Thm.trivial o ctermify;
paulson@15481
    92
paulson@15481
    93
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
paulson@15481
    94
      val cfvs = rev (map ctermify fvs);
paulson@15481
    95
paulson@15481
    96
      val conclthm = trivify (Logic.strip_imp_concl fixedbody);
paulson@15481
    97
      val concl_matches = 
paulson@15481
    98
          search_for_match sgn lhs maxidx 
paulson@15481
    99
                           ((IsaFTerm.focus_right  
paulson@15481
   100
                             o IsaFTerm.focus_left
paulson@15481
   101
                             o IsaFTerm.fcterm_of_term 
paulson@15481
   102
                             o Thm.prop_of) conclthm);
paulson@15481
   103
    in
paulson@15481
   104
      subst_concl rule' cfvs i th (conclthm, concl_matches)
paulson@15481
   105
    end;
paulson@15481
   106
paulson@15481
   107
(* substitute using an object or meta level equality *)
paulson@15481
   108
fun eqsubst_tac' instepthm i th = 
paulson@15481
   109
    let val stepthms = Seq.of_list (EqRuleData.prep_meta_eq instepthm) in
paulson@15481
   110
      Seq.flat (Seq.map (fn rule => subst rule i th) stepthms)
paulson@15481
   111
    end;
paulson@15481
   112
(* substitute using one of the given theorems *)
paulson@15481
   113
fun eqsubst_tac instepthms i th = 
paulson@15481
   114
    Seq.flat (Seq.map (fn r => eqsubst_tac' r i th) (Seq.of_list instepthms));
paulson@15481
   115
paulson@15481
   116
(* inthms are the given arguments in Isar, and treated as eqstep with
paulson@15481
   117
   the first one, then the second etc *)
paulson@15481
   118
fun eqsubst_meth inthms =
paulson@15481
   119
    Method.METHOD 
paulson@15481
   120
      (fn facts =>
paulson@15481
   121
          HEADGOAL (eqsubst_tac inthms THEN' Method.insert_tac facts));
paulson@15481
   122
paulson@15481
   123
paulson@15481
   124
fun apply_subst_in_asm rule cfvs i th matchseq = 
paulson@15481
   125
    let 
paulson@15481
   126
      fun apply_subst ((j, pth), mseq) = 
paulson@15481
   127
          Seq.flat (Seq.map 
paulson@15481
   128
             (fn m =>
paulson@15481
   129
                 (RWInst.rw m rule pth)
paulson@15481
   130
                   |> Thm.permute_prems 0 ~1
paulson@15481
   131
                   |> IsaND.schemify_frees_to_vars cfvs
paulson@15481
   132
                   |> RWInst.beta_eta_contract_tac
paulson@15481
   133
                   |> (fn r => Tactic.dtac r i th)
paulson@15481
   134
                   |> Seq.map Drule.zero_var_indexes)
paulson@15481
   135
             mseq)
paulson@15481
   136
    in
paulson@15481
   137
      Seq.flat (Seq.map apply_subst matchseq)
paulson@15481
   138
    end;
paulson@15481
   139
paulson@15481
   140
paulson@15481
   141
(* substitute within an assumption of goal i of gth, using a meta
paulson@15481
   142
equation rule *)
paulson@15481
   143
fun subst_asm rule i gth = 
paulson@15481
   144
    let 
paulson@15481
   145
      val th = Thm.incr_indexes 1 gth;
paulson@15481
   146
      val tgt_term = Thm.prop_of th;
paulson@15481
   147
      val maxidx = Term.maxidx_of_term tgt_term;
paulson@15481
   148
paulson@15481
   149
      val rule' = Drule.zero_var_indexes rule;
paulson@15481
   150
      val (lhs,_) = Logic.dest_equals (Thm.concl_of rule');
paulson@15481
   151
paulson@15481
   152
      val sgn = Thm.sign_of_thm th;
paulson@15481
   153
      val ctermify = Thm.cterm_of sgn;
paulson@15481
   154
      val trivify = Thm.trivial o ctermify;
paulson@15481
   155
paulson@15481
   156
      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
paulson@15481
   157
      val cfvs = rev (map ctermify fvs);
paulson@15481
   158
paulson@15481
   159
      val premthms = Seq.of_list (IsaPLib.number_list 1
paulson@15481
   160
                       (map trivify (Logic.strip_imp_prems fixedbody)));
paulson@15481
   161
      val prem_matches = 
paulson@15481
   162
          Seq.map (fn (i, pth) => 
paulson@15481
   163
                  ((i, pth), search_for_match sgn lhs maxidx 
paulson@15481
   164
                                              ((IsaFTerm.focus_right 
paulson@15481
   165
                                                o IsaFTerm.fcterm_of_term 
paulson@15481
   166
                                                o Thm.prop_of) pth)))
paulson@15481
   167
              premthms;
paulson@15481
   168
    in
paulson@15481
   169
      apply_subst_in_asm rule' cfvs i th prem_matches
paulson@15481
   170
    end;
paulson@15481
   171
paulson@15481
   172
(* substitute using an object or meta level equality *)
paulson@15481
   173
fun eqsubst_asm_tac' instepthm i th = 
paulson@15481
   174
    let val stepthms = Seq.of_list (EqRuleData.prep_meta_eq instepthm) in
paulson@15481
   175
      Seq.flat (Seq.map (fn rule => subst_asm rule i th) stepthms)
paulson@15481
   176
    end;
paulson@15481
   177
paulson@15481
   178
(* substitute using one of the given theorems *)
paulson@15481
   179
fun eqsubst_asm_tac instepthms i th = 
paulson@15481
   180
    Seq.flat (Seq.map (fn r => eqsubst_asm_tac' r i th) 
paulson@15481
   181
                      (Seq.of_list instepthms));
paulson@15481
   182
paulson@15481
   183
(* inthms are the given arguments in Isar, and treated as eqstep with
paulson@15481
   184
   the first one, then the second etc *)
paulson@15481
   185
fun eqsubst_asm_meth inthms =
paulson@15481
   186
    Method.METHOD 
paulson@15481
   187
      (fn facts =>
paulson@15481
   188
          HEADGOAL (eqsubst_asm_tac inthms THEN' Method.insert_tac facts));
paulson@15481
   189
paulson@15481
   190
(* combination method that takes a flag (true indicates that subst
paulson@15481
   191
should be done to an assumption, false = apply to the conclusion of
paulson@15481
   192
the goal) as well as the theorems to use *)
paulson@15481
   193
fun meth (asmflag, inthms) ctxt = 
paulson@15481
   194
    if asmflag then eqsubst_asm_meth inthms else eqsubst_meth inthms;
paulson@15481
   195
paulson@15481
   196
(* syntax for options, given "(asm)" will give back true, without
paulson@15481
   197
   gives back false *)
paulson@15481
   198
val options_syntax =
paulson@15481
   199
    (Args.parens (Args.$$$ "asm") >> (K true)) ||
paulson@15481
   200
     (Scan.succeed false);
paulson@15481
   201
paulson@15481
   202
(* method syntax, first take options, then theorems *)
paulson@15481
   203
fun meth_syntax meth src ctxt =
paulson@15481
   204
    meth (snd (Method.syntax ((Scan.lift options_syntax) 
paulson@15481
   205
                                -- Attrib.local_thms) src ctxt)) 
paulson@15481
   206
         ctxt;
paulson@15481
   207
paulson@15481
   208
(* setup function for adding method to theory. *)
paulson@15481
   209
val setup = 
paulson@15481
   210
    [Method.add_method ("subst", meth_syntax meth, "Substiution with an equation. Use \"(asm)\" option to substitute in an assumption.")];
paulson@15481
   211
paulson@15481
   212
end;