1signature bossLib = 2sig 3 include Abbrev 4 type ssfrag = simpLib.ssfrag 5 type simpset = simpLib.simpset 6 7 (* Make definitions *) 8 9 (* new types *) 10 val Hol_datatype : hol_type quotation -> unit 11 val Datatype : hol_type quotation -> unit 12 13 (* new functions *) 14 val Define : term quotation -> thm 15 val zDefine : term quotation -> thm 16 val xDefine : string -> term quotation -> thm 17 val tDefine : string -> term quotation -> tactic -> thm 18 val WF_REL_TAC : term quotation -> tactic 19 val Hol_defn : string -> term quotation -> DefnBase.defn 20 21 (* new (inductive) relations *) 22 val Hol_reln : term quotation -> thm * thm * thm 23 val Hol_coreln : term quotation -> thm * thm * thm 24 val xHol_reln : string -> term quotation -> thm * thm * thm 25 val xHol_coreln : string -> term quotation -> thm * thm * thm 26 val export_mono : string -> unit 27 28 (* Derived rule for specifying new constants. 29 Should have the same effect as Theory.Definition.new_specification. *) 30 val new_specification : string * string list * thm -> thm 31 32 (* Case-splitting and induction operations *) 33 34 val Cases : tactic 35 val Cases_on : term quotation -> tactic 36 val tmCases_on : term -> string list -> tactic 37 val PairCases : tactic 38 val PairCases_on : term quotation -> tactic 39 val Induct : tactic 40 val Induct_on : term quotation -> tactic 41 val recInduct : thm -> tactic 42 val namedCases : string list -> tactic 43 val namedCases_on : term quotation -> string list -> tactic 44 45 val measureInduct_on : term quotation -> tactic 46 val completeInduct_on : term quotation -> tactic 47 val using : tactic * thm -> tactic (* infix *) 48 val usingA : tactic -> thm -> tactic (* curry of above *) 49 50 val pairarg_tac : tactic 51 val split_pair_case_tac : tactic 52 53 val CASE_TAC : tactic 54 val CaseEq : string -> thm 55 val CaseEqs : string list -> thm 56 val AllCaseEqs : unit -> thm 57 58 (* Proof automation *) 59 60 val PROVE : thm list -> term -> thm (* First order *) 61 val METIS_PROVE : thm list -> term -> thm (* First order *) 62 val DECIDE : term -> thm (* Cooperating dec. procs *) 63 val PROVE_TAC : thm list -> tactic 64 val prove_tac : thm list -> tactic 65 val METIS_TAC : thm list -> tactic 66 val metis_tac : thm list -> tactic 67 val DECIDE_TAC : tactic 68 val decide_tac : tactic 69 70 (* Simplification *) 71 72 val ++ : simpset * ssfrag -> simpset (* infix *) 73 val && : simpset * thm list -> simpset (* infix *) 74 val -* : simpset * string list -> simpset (* infix *) 75 val pure_ss : simpset 76 val bool_ss : simpset 77 val std_ss : simpset (* bool + option + pair + sum *) 78 val arith_ss : simpset 79 val old_arith_ss : simpset 80 val list_ss : simpset 81 val srw_ss : unit -> simpset 82 val QI_ss : ssfrag 83 val SQI_ss : ssfrag 84 val ARITH_ss : ssfrag (* arithmetic d.p. + some rewrites *) 85 val old_ARITH_ss : ssfrag 86 val type_rws : hol_type -> thm list 87 val rewrites : thm list -> ssfrag 88 val augment_srw_ss : ssfrag list -> unit 89 val diminish_srw_ss : string list -> unit 90 val export_rewrites : string list -> unit 91 val delsimps : string list -> unit 92 val temp_delsimps : string list -> unit 93 val limit : int -> simpset -> simpset 94 95 (* use these in simplifier's argument list *) 96 val SimpLHS : thm 97 val SimpRHS : thm 98 val SimpL : term -> thm 99 val SimpR : term -> thm 100 101 val Cong : thm -> thm 102 val AC : thm -> thm -> thm 103 val Excl : string -> thm 104 val Req0 : thm -> thm 105 val ReqD : thm -> thm 106 107 val SIMP_CONV : simpset -> thm list -> conv 108 val SIMP_RULE : simpset -> thm list -> thm -> thm 109 val SIMP_TAC : simpset -> thm list -> tactic 110 val simp_tac : simpset -> thm list -> tactic 111 val ASM_SIMP_TAC : simpset -> thm list -> tactic 112 val asm_simp_tac : simpset -> thm list -> tactic 113 val FULL_SIMP_TAC : simpset -> thm list -> tactic 114 val full_simp_tac : simpset -> thm list -> tactic 115 val REV_FULL_SIMP_TAC : simpset -> thm list -> tactic 116 val rev_full_simp_tac : simpset -> thm list -> tactic 117 val RW_TAC : simpset -> thm list -> tactic 118 val rw_tac : simpset -> thm list -> tactic 119 val SRW_TAC : ssfrag list -> thm list -> tactic 120 val srw_tac : ssfrag list -> thm list -> tactic 121 122 val NO_STRIP_FULL_SIMP_TAC : simpset -> thm list -> tactic 123 val NO_STRIP_REV_FULL_SIMP_TAC : simpset -> thm list -> tactic 124 125 val QI_TAC : tactic 126 val ASM_QI_TAC : tactic 127 val GEN_EXISTS_TAC : string -> Parse.term Lib.frag list -> tactic 128 129 (* Call-by-value evaluation *) 130 val EVAL : conv 131 val EVAL_RULE : thm -> thm 132 val EVAL_TAC : tactic 133 134 (* Automate some routine set theory by reduction to FOL *) 135 val SET_TAC : thm list -> tactic 136 val ASM_SET_TAC : thm list -> tactic 137 val SET_RULE : term -> thm 138 139 (* Miscellaneous *) 140 141 val ZAP_TAC : simpset -> thm list -> tactic 142 val SPOSE_NOT_THEN : (thm -> tactic) -> tactic 143 val spose_not_then : (thm -> tactic) -> tactic 144 val by : term quotation * tactic -> tactic (* infix *) 145 val suffices_by : term quotation * tactic -> tactic (* infix *) 146 val sg : term quotation -> tactic 147 val subgoal : term quotation -> tactic 148 val cheat : tactic 149 val kall_tac : 'a -> tactic 150 151 (* Abbreviations (see also Q structure) *) 152 153 val Abbr : term quotation -> thm 154 val UNABBREV_ALL_TAC : tactic 155 val REABBREV_TAC : tactic 156 val WITHOUT_ABBREVS : tactic -> tactic 157 158 (* name cases of an induction theorem *) 159 val name_ind_cases : term list -> thm -> thm 160 161 (* more simplification variants *) 162 val fsrw_tac : simpLib.ssfrag list -> thm list -> tactic 163 val simp : thm list -> tactic 164 val csimp : thm list -> tactic 165 val dsimp : thm list -> tactic 166 val lrw : thm list -> tactic 167 val lfs : thm list -> tactic 168 val lrfs : thm list -> tactic 169 val rw : thm list -> tactic 170 val fs : thm list -> tactic 171 val rfs : thm list -> tactic 172 val gs : thm list -> tactic 173 val gvs : thm list -> tactic 174 val gns : thm list -> tactic 175 val gnvs : thm list -> tactic 176 177 (* without loss of generality (from wlogLib) *) 178 val wlog_then : term quotation -> 179 term quotation list -> thm_tactic -> tactic 180 val wlog_tac : term quotation -> term quotation list -> tactic 181 182 (* useful quotation-based tactics (from Q) *) 183 val qx_gen_tac : term quotation -> tactic 184 val qx_genl_tac : term quotation list -> tactic 185 val qx_choose_then : term quotation -> thm_tactic -> thm_tactic 186 val qx_choosel_then : term quotation list -> thm_tactic -> thm_tactic 187 val qexists_tac : term quotation -> tactic 188 val qexistsl_tac : term quotation list -> tactic 189 val qsuff_tac : term quotation -> tactic 190 val qid_spec_tac : term quotation -> tactic 191 val qspec_tac : term quotation * term quotation -> tactic 192 val qspec_then : term quotation -> thm_tactic -> thm -> tactic 193 val qspecl_then : term quotation list -> thm_tactic -> thm -> tactic 194 val qhdtm_assum : term quotation -> thm_tactic -> tactic 195 val qhdtm_x_assum : term quotation -> thm_tactic -> tactic 196 val qpat_assum : term quotation -> thm_tactic -> tactic 197 val qpat_x_assum : term quotation -> thm_tactic -> tactic 198 val qpat_abbrev_tac : term quotation -> tactic 199 val qmatch_abbrev_tac : term quotation -> tactic 200 val qho_match_abbrev_tac : term quotation -> tactic 201 val qmatch_rename_tac : term quotation -> tactic 202 val qmatch_assum_abbrev_tac : term quotation -> tactic 203 val qmatch_assum_rename_tac : term quotation -> tactic 204 val qmatch_asmsub_rename_tac : term quotation -> tactic 205 val qmatch_goalsub_rename_tac : term quotation -> tactic 206 val qmatch_asmsub_abbrev_tac : term quotation -> tactic 207 val qmatch_goalsub_abbrev_tac : term quotation -> tactic 208 val rename1 : term quotation -> tactic 209 val rename : term quotation list -> tactic 210 val qabbrev_tac : term quotation -> tactic 211 val qunabbrev_tac : term quotation -> tactic 212 val qunabbrevl_tac : term quotation list -> tactic 213 val unabbrev_all_tac : tactic 214 215 (* Derived search functions *) 216 val find_consts_thy : string list -> hol_type -> term list 217 val find_consts : hol_type -> term list 218end 219