# HG changeset patch # User wenzelm # Date 1243681935 -7200 # Node ID 952d2d0c44466df4d9e0c10c492e33efce026b8a # Parent 40fa39d9bce7910b8f41b1da131f5c09d7599c36 minimal signature cleanup; modernized method setup; diff -r 40fa39d9bce7 -r 952d2d0c4446 src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Sat May 30 12:53:11 2009 +0200 +++ b/src/Tools/eqsubst.ML Sat May 30 13:12:15 2009 +0200 @@ -20,25 +20,25 @@ * Zipper.T (* focusterm to search under *) exception eqsubst_occL_exp of - string * int list * Thm.thm list * int * Thm.thm + string * int list * thm list * int * thm (* low level substitution functions *) val apply_subst_in_asm : int -> - Thm.thm -> - Thm.thm -> - (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq + thm -> + thm -> + (cterm list * int * 'a * thm) * match -> thm Seq.seq val apply_subst_in_concl : int -> - Thm.thm -> - Thm.cterm list * Thm.thm -> - Thm.thm -> match -> Thm.thm Seq.seq + thm -> + cterm list * thm -> + thm -> match -> thm Seq.seq (* matching/unification within zippers *) val clean_match_z : - Context.theory -> Term.term -> Zipper.T -> match option + theory -> term -> Zipper.T -> match option val clean_unify_z : - Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq + theory -> int -> term -> Zipper.T -> match Seq.seq (* skipping things in seq seq's *) @@ -57,65 +57,64 @@ (* tactics *) val eqsubst_asm_tac : Proof.context -> - int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq + int list -> thm list -> int -> tactic val eqsubst_asm_tac' : Proof.context -> - (searchinfo -> int -> Term.term -> match skipseq) -> - int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq + (searchinfo -> int -> term -> match skipseq) -> + int -> thm -> int -> tactic val eqsubst_tac : Proof.context -> int list -> (* list of occurences to rewrite, use [0] for any *) - Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq + thm list -> int -> tactic val eqsubst_tac' : Proof.context -> (* proof context *) - (searchinfo -> Term.term -> match Seq.seq) (* search function *) - -> Thm.thm (* equation theorem to rewrite with *) + (searchinfo -> term -> match Seq.seq) (* search function *) + -> thm (* equation theorem to rewrite with *) -> int (* subgoal number in goal theorem *) - -> Thm.thm (* goal theorem *) - -> Thm.thm Seq.seq (* rewritten goal theorem *) + -> thm (* goal theorem *) + -> thm Seq.seq (* rewritten goal theorem *) val fakefree_badbounds : - (string * Term.typ) list -> - Term.term -> - (string * Term.typ) list * (string * Term.typ) list * Term.term + (string * typ) list -> + term -> + (string * typ) list * (string * typ) list * term val mk_foo_match : - (Term.term -> Term.term) -> - ('a * Term.typ) list -> Term.term -> Term.term + (term -> term) -> + ('a * typ) list -> term -> term (* preparing substitution *) - val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list + val prep_meta_eq : Proof.context -> thm -> thm list val prep_concl_subst : - int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo + int -> thm -> (cterm list * thm) * searchinfo val prep_subst_in_asm : - int -> Thm.thm -> int -> - (Thm.cterm list * int * int * Thm.thm) * searchinfo + int -> thm -> int -> + (cterm list * int * int * thm) * searchinfo val prep_subst_in_asms : - int -> Thm.thm -> - ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list + int -> thm -> + ((cterm list * int * int * thm) * searchinfo) list val prep_zipper_match : - Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term) + Zipper.T -> term * ((string * typ) list * (string * typ) list * term) (* search for substitutions *) val valid_match_start : Zipper.T -> bool val search_lr_all : Zipper.T -> Zipper.T Seq.seq val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq val searchf_lr_unify_all : - searchinfo -> Term.term -> match Seq.seq Seq.seq + searchinfo -> term -> match Seq.seq Seq.seq val searchf_lr_unify_valid : - searchinfo -> Term.term -> match Seq.seq Seq.seq + searchinfo -> term -> match Seq.seq Seq.seq val searchf_bt_unify_valid : - searchinfo -> Term.term -> match Seq.seq Seq.seq + searchinfo -> term -> match Seq.seq Seq.seq (* syntax tools *) val ith_syntax : int list parser val options_syntax : bool parser (* Isar level hooks *) - val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method - val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method - val subst_meth : Method.src -> Proof.context -> Proof.method + val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method + val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method val setup : theory -> theory end; @@ -560,15 +559,13 @@ Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0]; (* combination method that takes a flag (true indicates that subst -should be done to an assumption, false = apply to the conclusion of -the goal) as well as the theorems to use *) -fun subst_meth src = - Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src - #> (fn (((asmflag, occL), inthms), ctxt) => - (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms); - - + should be done to an assumption, false = apply to the conclusion of + the goal) as well as the theorems to use *) val setup = - Method.add_method ("subst", subst_meth, "single-step substitution"); + Method.setup @{binding subst} + (Scan.lift (options_syntax -- ith_syntax) -- Attrib.thms >> + (fn ((asmflag, occL), inthms) => fn ctxt => + (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms)) + "single-step substitution"; end;