1signature RW = 2sig 3 include Abbrev 4 5 (* Simplification sets *) 6 type simpls 7 val empty_simpls : simpls 8 val dest_simpls : simpls -> {congs:thm list, rws:thm list} 9 val mk_simpls : (thm -> thm) -> thm -> thm list 10 val MK_RULES : thm -> thm list 11 val add_rws : simpls -> thm list -> simpls 12 val add_congs : simpls -> thm list -> simpls 13 val join_simpls : simpls -> simpls -> simpls 14 val std_simpls : simpls 15 val pp_simpls : simpls PP.pprinter 16 val embedded_ref : (term -> term -> bool) ref 17 18 (* The implicit simplification set *) 19 val add_implicit_congs : thm list -> unit 20 val add_implicit_rws : thm list -> unit 21 val add_implicit_simpls : simpls -> unit 22 val implicit_simpls : unit -> simpls 23 val set_implicit_simpls : simpls -> unit 24 25 (* Solvers and monitoring *) 26 val solver_err : unit -> 'a 27 val rw_solver : simpls -> thm list -> term -> thm 28 val std_solver : 'a -> thm list -> term -> thm 29 val always_fails : 'a -> 'b -> 'c -> 'd 30 31 (* Tells whether to add context to the simpls as term is traversed *) 32 datatype context_policy = ADD | DONT_ADD 33 34 (* The atomic conditional term rewriter. *) 35 val RW_STEP:{context:'a * context_policy, simpls:simpls, 36 prover:simpls -> 'a -> term -> thm} 37 -> term -> thm 38 39 type cntxt_solver = {context:thm list * context_policy, 40 simpls:simpls, 41 prover:simpls -> thm list -> term -> thm}; 42 43 type strategy = (cntxt_solver -> term -> thm) 44 -> (cntxt_solver -> term -> thm) 45 46 val DEPTH : strategy 47 val REDEPTH : strategy 48 val TOP_DEPTH : strategy 49 val ONCE_DEPTH : strategy 50 val RATOR : strategy 51 val RAND : strategy 52 val ABST : strategy 53 54 datatype repetitions = Once | Fully | Special of strategy 55 datatype rules = Default of thm list 56 | Pure of thm list 57 | Simpls of simpls * thm list 58 datatype context = Context of thm list * context_policy 59 datatype congs = Congs of thm list 60 datatype solver = Solver of simpls -> thm list -> term -> thm 61 62 (* Parameterized rewriters for terms, theorems, and goals *) 63 val Rewrite :repetitions -> rules*context*congs*solver -> conv 64 val REWRITE_RULE :repetitions -> rules*context*congs*solver -> thm -> thm 65 val ASM_REWRITE_RULE:repetitions -> rules*context*congs*solver -> thm -> thm 66 val REWRITE_TAC :repetitions -> rules*context*congs*solver -> tactic 67 val ASM_REWRITE_TAC :repetitions -> rules*context*congs*solver -> tactic 68 69 70 (* Specialized rewriters for different types *) 71 (* Terms *) 72 73 val CRW_CONV : thm list -> term -> thm 74 val RW_CONV : thm list -> term -> thm 75 val PURE_RW_CONV : thm list -> term -> thm 76 val ONCE_RW_CONV : thm list -> term -> thm 77 val PURE_ONCE_RW_CONV : thm list -> term -> thm 78 79 80 (* Theorems *) 81 val CRW_RULE : thm list -> thm -> thm 82 val RW_RULE : thm list -> thm -> thm 83 val PURE_RW_RULE : thm list -> thm -> thm 84 val ONCE_RW_RULE : thm list -> thm -> thm 85 val PURE_ONCE_RW_RULE : thm list -> thm -> thm 86 87 val ASM_CRW_RULE : thm list -> thm -> thm 88 val ASM_RW_RULE : thm list -> thm -> thm 89 val PURE_ASM_RW_RULE : thm list -> thm -> thm 90 val ONCE_ASM_RW_RULE : thm list -> thm -> thm 91 val PURE_ONCE_ASM_RW_RULE : thm list -> thm -> thm 92 93 94 (* Goals *) 95 val RW_TAC : thm list -> tactic 96 val CRW_TAC : thm list -> tactic 97 val PURE_RW_TAC : thm list -> tactic 98 val ONCE_RW_TAC : thm list -> tactic 99 val PURE_ONCE_RW_TAC: thm list -> tactic 100 101 val ASM_RW_TAC : thm list -> tactic 102 val ASM_CRW_TAC : thm list -> tactic 103 val PURE_ASM_RW_TAC : thm list -> tactic 104 val ONCE_ASM_RW_TAC : thm list -> tactic 105 val PURE_ONCE_ASM_RW_TAC : thm list -> tactic 106 107 (* Folding in beta-conversion and a user-given standard simpset *) 108 val Simpl : tactic -> thm list -> thm list -> tactic 109 110end 111