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 -> 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 Induct : tactic 36 val recInduct : thm -> tactic 37 val Cases_on : term quotation -> tactic 38 val Induct_on : term quotation -> tactic 39 val PairCases_on : term quotation -> tactic 40 val measureInduct_on : term quotation -> tactic 41 val completeInduct_on : term quotation -> tactic 42 val CASE_TAC : tactic 43 val pairarg_tac : tactic 44 val split_pair_case_tac : tactic 45 val CaseEq : string -> thm 46 val CaseEqs : string list -> thm 47 val AllCaseEqs : unit -> thm 48 49 (* Proof automation *) 50 51 val PROVE : thm list -> term -> thm (* First order *) 52 val METIS_PROVE : thm list -> term -> thm (* First order *) 53 val DECIDE : term -> thm (* Cooperating dec. procs *) 54 val PROVE_TAC : thm list -> tactic 55 val prove_tac : thm list -> tactic 56 val METIS_TAC : thm list -> tactic 57 val metis_tac : thm list -> tactic 58 val DECIDE_TAC : tactic 59 val decide_tac : tactic 60 61 (* Simplification *) 62 63 val ++ : simpset * ssfrag -> simpset (* infix *) 64 val && : simpset * thm list -> simpset (* infix *) 65 val pure_ss : simpset 66 val bool_ss : simpset 67 val std_ss : simpset (* bool + option + pair + sum *) 68 val arith_ss : simpset 69 val old_arith_ss : simpset 70 val list_ss : simpset 71 val srw_ss : unit -> simpset 72 val QI_ss : ssfrag 73 val SQI_ss : ssfrag 74 val ARITH_ss : ssfrag (* arithmetic d.p. + some rewrites *) 75 val old_ARITH_ss : ssfrag 76 val type_rws : hol_type -> thm list 77 val rewrites : thm list -> ssfrag 78 val augment_srw_ss : ssfrag list -> unit 79 val diminish_srw_ss : string list -> ssfrag list 80 val export_rewrites : string list -> unit 81 val limit : int -> simpset -> simpset 82 83 (* use these in simplifier's argument list *) 84 val SimpLHS : thm 85 val SimpRHS : thm 86 val SimpL : term -> thm 87 val SimpR : term -> thm 88 89 val Cong : thm -> thm 90 val AC : thm -> thm -> thm 91 92 val SIMP_CONV : simpset -> thm list -> conv 93 val SIMP_RULE : simpset -> thm list -> thm -> thm 94 val SIMP_TAC : simpset -> thm list -> tactic 95 val simp_tac : simpset -> thm list -> tactic 96 val ASM_SIMP_TAC : simpset -> thm list -> tactic 97 val asm_simp_tac : simpset -> thm list -> tactic 98 val FULL_SIMP_TAC : simpset -> thm list -> tactic 99 val full_simp_tac : simpset -> thm list -> tactic 100 val REV_FULL_SIMP_TAC : simpset -> thm list -> tactic 101 val rev_full_simp_tac : simpset -> thm list -> tactic 102 val RW_TAC : simpset -> thm list -> tactic 103 val rw_tac : simpset -> thm list -> tactic 104 val SRW_TAC : ssfrag list -> thm list -> tactic 105 val srw_tac : ssfrag list -> thm list -> tactic 106 107 val NO_STRIP_FULL_SIMP_TAC : simpset -> thm list -> tactic 108 val NO_STRIP_REV_FULL_SIMP_TAC : simpset -> thm list -> tactic 109 110 val QI_TAC : tactic 111 val ASM_QI_TAC : tactic 112 val GEN_EXISTS_TAC : string -> Parse.term Lib.frag list -> tactic 113 114 (* Call-by-value evaluation *) 115 val EVAL : conv 116 val EVAL_RULE : thm -> thm 117 val EVAL_TAC : tactic 118 119 (* Miscellaneous *) 120 121 val ZAP_TAC : simpset -> thm list -> tactic 122 val SPOSE_NOT_THEN : (thm -> tactic) -> tactic 123 val spose_not_then : (thm -> tactic) -> tactic 124 val by : term quotation * tactic -> tactic (* infix *) 125 val suffices_by : term quotation * tactic -> tactic (* infix *) 126 val sg : term quotation -> tactic 127 val subgoal : term quotation -> tactic 128 val cheat : tactic 129 val kall_tac : 'a -> tactic 130 131 (* Abbreviations (see also Q structure) *) 132 133 val Abbr : term quotation -> thm 134 val UNABBREV_ALL_TAC : tactic 135 val REABBREV_TAC : tactic 136 val WITHOUT_ABBREVS : tactic -> tactic 137 138 (* more simplification variants *) 139 val fsrw_tac : simpLib.ssfrag list -> thm list -> tactic 140 val simp : thm list -> tactic 141 val csimp : thm list -> tactic 142 val dsimp : thm list -> tactic 143 val lrw : thm list -> tactic 144 val lfs : thm list -> tactic 145 val lrfs : thm list -> tactic 146 val rw : thm list -> tactic 147 val fs : thm list -> tactic 148 val rfs : thm list -> tactic 149 150 (* without loss of generality (from wlogLib) *) 151 val wlog_then : term quotation -> 152 term quotation list -> thm_tactic -> tactic 153 val wlog_tac : term quotation -> term quotation list -> tactic 154 155 (* useful quotation-based tactics (from Q) *) 156 val qx_gen_tac : term quotation -> tactic 157 val qx_choose_then : term quotation -> thm_tactic -> thm_tactic 158 val qexists_tac : term quotation -> tactic 159 val qsuff_tac : term quotation -> tactic 160 val qid_spec_tac : term quotation -> tactic 161 val qspec_tac : term quotation * term quotation -> tactic 162 val qspec_then : term quotation -> thm_tactic -> thm -> tactic 163 val qspecl_then : term quotation list -> thm_tactic -> thm -> tactic 164 val qhdtm_assum : term quotation -> thm_tactic -> tactic 165 val qhdtm_x_assum : term quotation -> thm_tactic -> tactic 166 val qpat_assum : term quotation -> thm_tactic -> tactic 167 val qpat_x_assum : term quotation -> thm_tactic -> tactic 168 val qpat_abbrev_tac : term quotation -> tactic 169 val qmatch_abbrev_tac : term quotation -> tactic 170 val qho_match_abbrev_tac : term quotation -> tactic 171 val qmatch_rename_tac : term quotation -> tactic 172 val qmatch_assum_abbrev_tac : term quotation -> tactic 173 val qmatch_assum_rename_tac : term quotation -> tactic 174 val qmatch_asmsub_rename_tac : term quotation -> tactic 175 val qmatch_goalsub_rename_tac : term quotation -> tactic 176 val qmatch_asmsub_abbrev_tac : term quotation -> tactic 177 val qmatch_goalsub_abbrev_tac : term quotation -> tactic 178 val rename1 : term quotation -> tactic 179 val rename : term quotation list -> tactic 180 val qabbrev_tac : term quotation -> tactic 181 val qunabbrev_tac : term quotation -> tactic 182 val unabbrev_all_tac : tactic 183 val qx_genl_tac : term quotation list -> tactic 184 val qx_choosel_then : term quotation list -> thm_tactic -> thm_tactic 185 186end 187