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;