src/Tools/eqsubst.ML
changeset 31301 952d2d0c4446
parent 30513 1796b8ea88aa
child 32032 a6a6e8031c14
     1.1 --- a/src/Tools/eqsubst.ML	Sat May 30 12:53:11 2009 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Sat May 30 13:12:15 2009 +0200
     1.3 @@ -20,25 +20,25 @@
     1.4         * Zipper.T (* focusterm to search under *)
     1.5  
     1.6      exception eqsubst_occL_exp of
     1.7 -       string * int list * Thm.thm list * int * Thm.thm
     1.8 +       string * int list * thm list * int * thm
     1.9      
    1.10      (* low level substitution functions *)
    1.11      val apply_subst_in_asm :
    1.12         int ->
    1.13 -       Thm.thm ->
    1.14 -       Thm.thm ->
    1.15 -       (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq
    1.16 +       thm ->
    1.17 +       thm ->
    1.18 +       (cterm list * int * 'a * thm) * match -> thm Seq.seq
    1.19      val apply_subst_in_concl :
    1.20         int ->
    1.21 -       Thm.thm ->
    1.22 -       Thm.cterm list * Thm.thm ->
    1.23 -       Thm.thm -> match -> Thm.thm Seq.seq
    1.24 +       thm ->
    1.25 +       cterm list * thm ->
    1.26 +       thm -> match -> thm Seq.seq
    1.27  
    1.28      (* matching/unification within zippers *)
    1.29      val clean_match_z :
    1.30 -       Context.theory -> Term.term -> Zipper.T -> match option
    1.31 +       theory -> term -> Zipper.T -> match option
    1.32      val clean_unify_z :
    1.33 -       Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq
    1.34 +       theory -> int -> term -> Zipper.T -> match Seq.seq
    1.35  
    1.36      (* skipping things in seq seq's *)
    1.37  
    1.38 @@ -57,65 +57,64 @@
    1.39      (* tactics *)
    1.40      val eqsubst_asm_tac :
    1.41         Proof.context ->
    1.42 -       int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    1.43 +       int list -> thm list -> int -> tactic
    1.44      val eqsubst_asm_tac' :
    1.45         Proof.context ->
    1.46 -       (searchinfo -> int -> Term.term -> match skipseq) ->
    1.47 -       int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
    1.48 +       (searchinfo -> int -> term -> match skipseq) ->
    1.49 +       int -> thm -> int -> tactic
    1.50      val eqsubst_tac :
    1.51         Proof.context ->
    1.52         int list -> (* list of occurences to rewrite, use [0] for any *)
    1.53 -       Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    1.54 +       thm list -> int -> tactic
    1.55      val eqsubst_tac' :
    1.56         Proof.context -> (* proof context *)
    1.57 -       (searchinfo -> Term.term -> match Seq.seq) (* search function *)
    1.58 -       -> Thm.thm (* equation theorem to rewrite with *)
    1.59 +       (searchinfo -> term -> match Seq.seq) (* search function *)
    1.60 +       -> thm (* equation theorem to rewrite with *)
    1.61         -> int (* subgoal number in goal theorem *)
    1.62 -       -> Thm.thm (* goal theorem *)
    1.63 -       -> Thm.thm Seq.seq (* rewritten goal theorem *)
    1.64 +       -> thm (* goal theorem *)
    1.65 +       -> thm Seq.seq (* rewritten goal theorem *)
    1.66  
    1.67  
    1.68      val fakefree_badbounds :
    1.69 -       (string * Term.typ) list ->
    1.70 -       Term.term ->
    1.71 -       (string * Term.typ) list * (string * Term.typ) list * Term.term
    1.72 +       (string * typ) list ->
    1.73 +       term ->
    1.74 +       (string * typ) list * (string * typ) list * term
    1.75  
    1.76      val mk_foo_match :
    1.77 -       (Term.term -> Term.term) ->
    1.78 -       ('a * Term.typ) list -> Term.term -> Term.term
    1.79 +       (term -> term) ->
    1.80 +       ('a * typ) list -> term -> term
    1.81  
    1.82      (* preparing substitution *)
    1.83 -    val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list
    1.84 +    val prep_meta_eq : Proof.context -> thm -> thm list
    1.85      val prep_concl_subst :
    1.86 -       int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo
    1.87 +       int -> thm -> (cterm list * thm) * searchinfo
    1.88      val prep_subst_in_asm :
    1.89 -       int -> Thm.thm -> int ->
    1.90 -       (Thm.cterm list * int * int * Thm.thm) * searchinfo
    1.91 +       int -> thm -> int ->
    1.92 +       (cterm list * int * int * thm) * searchinfo
    1.93      val prep_subst_in_asms :
    1.94 -       int -> Thm.thm ->
    1.95 -       ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list
    1.96 +       int -> thm ->
    1.97 +       ((cterm list * int * int * thm) * searchinfo) list
    1.98      val prep_zipper_match :
    1.99 -       Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term)
   1.100 +       Zipper.T -> term * ((string * typ) list * (string * typ) list * term)
   1.101  
   1.102      (* search for substitutions *)
   1.103      val valid_match_start : Zipper.T -> bool
   1.104      val search_lr_all : Zipper.T -> Zipper.T Seq.seq
   1.105      val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
   1.106      val searchf_lr_unify_all :
   1.107 -       searchinfo -> Term.term -> match Seq.seq Seq.seq
   1.108 +       searchinfo -> term -> match Seq.seq Seq.seq
   1.109      val searchf_lr_unify_valid :
   1.110 -       searchinfo -> Term.term -> match Seq.seq Seq.seq
   1.111 +       searchinfo -> term -> match Seq.seq Seq.seq
   1.112      val searchf_bt_unify_valid :
   1.113 -       searchinfo -> Term.term -> match Seq.seq Seq.seq
   1.114 +       searchinfo -> term -> match Seq.seq Seq.seq
   1.115  
   1.116      (* syntax tools *)
   1.117      val ith_syntax : int list parser
   1.118      val options_syntax : bool parser
   1.119  
   1.120      (* Isar level hooks *)
   1.121 -    val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   1.122 -    val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   1.123 -    val subst_meth : Method.src -> Proof.context -> Proof.method
   1.124 +    val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
   1.125 +    val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
   1.126      val setup : theory -> theory
   1.127  
   1.128  end;
   1.129 @@ -560,15 +559,13 @@
   1.130      Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
   1.131  
   1.132  (* combination method that takes a flag (true indicates that subst
   1.133 -should be done to an assumption, false = apply to the conclusion of
   1.134 -the goal) as well as the theorems to use *)
   1.135 -fun subst_meth src =
   1.136 -  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
   1.137 -  #> (fn (((asmflag, occL), inthms), ctxt) =>
   1.138 -    (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
   1.139 -
   1.140 -
   1.141 +   should be done to an assumption, false = apply to the conclusion of
   1.142 +   the goal) as well as the theorems to use *)
   1.143  val setup =
   1.144 -  Method.add_method ("subst", subst_meth, "single-step substitution");
   1.145 +  Method.setup @{binding subst}
   1.146 +    (Scan.lift (options_syntax -- ith_syntax) -- Attrib.thms >>
   1.147 +      (fn ((asmflag, occL), inthms) => fn ctxt =>
   1.148 +        (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms))
   1.149 +    "single-step substitution";
   1.150  
   1.151  end;