1(* ===================================================================== *) 2(* VERSION : 1.0 *) 3(* FILE : tactics.sml *) 4(* DESCRIPTION : General purpose tactics for obj library. *) 5(* *) 6(* AUTHOR : Peter Vincent Homeier *) 7(* DATE : October 19, 2000 *) 8(* COPYRIGHT : Copyright (c) 2000 by Peter Vincent Homeier *) 9(* *) 10(* ===================================================================== *) 11 12(* --------------------------------------------------------------------- *) 13(* This file contains new tactics of general usefulness. *) 14(* --------------------------------------------------------------------- *) 15 16signature tactics = 17sig 18 19type term = Term.term 20type thm = Thm.thm 21type hol_type = Type.hol_type 22type tactic = Abbrev.tactic 23type conv = Abbrev.conv 24type thm_tactic = Abbrev.thm_tactic 25 26 27 28 29val print_newline : unit -> unit 30val print_theorem : thm -> unit 31val print_terms : term list -> unit 32val print_all_thm : thm -> unit 33val print_theorems : thm list -> unit 34val print_goal : (term list * term) -> unit 35 36val print_theory_size : unit -> unit 37 38val pthm : thm -> thm 39 40val pairf : ('a -> 'b) -> ('c -> 'd) -> ('a * 'c) -> ('b * 'd) 41val test : ('a -> 'b) -> 'a -> 'a 42val try : ('a -> 'a) -> 'a -> 'a 43 44 45 46val ONE_ONE_DEF : thm 47val ONTO_DEF : thm 48 49(* These operators transform implications to collect antecedents into 50 a single conjunction, or else to reverse this and spread them into 51 a sequence of individual implications. Each has type thm->thm. 52*) 53 54val AND2IMP : thm -> thm 55val IMP2AND : thm -> thm 56 57(* 58val TACTIC_ERR{function,message} = 59 Exception.HOL_ERR{origin_structure = "Tactic", 60 origin_function = function, 61 message = message}; 62*) 63 64val failwith : string -> 'a 65val fail : unit -> 'a 66 67 68(* Here are some useful tactics, that are not included in the standard HOL: *) 69 70val PRINT_TAC : tactic 71val POP_TAC : tactic 72val ETA_TAC : term -> tactic 73val EXT_TAC : term -> tactic 74val CHECK_TAC : tactic 75val FALSE_TAC : tactic 76val MP_IMP_TAC : thm -> tactic 77val UNASSUME_THEN : thm_tactic -> term -> tactic 78val CONTRAPOS_TAC : tactic 79val FORALL_EQ_TAC : tactic 80val EXISTS_EQ_TAC : tactic 81val EXISTS_VAR : (term * term) -> thm -> thm 82val FIND_EXISTS_TAC : tactic 83val UNBETA_TAC : term -> tactic 84 85val UNDISCH_ALL_TAC : tactic 86val UNDISCH_LAST_TAC : tactic 87val DEFINE_NEW_VAR : term -> tactic 88 89val LIST_INDUCT_TAC : tactic 90val DOUBLE_LIST_INDUCT_TAC : tactic 91val LENGTH_LIST_INDUCT_TAC : tactic 92val FORALL_SYM_CONV : conv 93 94val NOT_AP_TERM_TAC : term -> tactic 95 96val APP_let_CONV : conv 97val LIFT_let_TAC : tactic 98val STRIP_let_TAC : tactic 99val USE_IMP_EQ_matches 100 : thm -> term -> (term * term) list * (hol_type * hol_type) list 101val USE_IMP_matches 102 : thm -> term -> (term * term) list * (hol_type * hol_type) list 103val SUB_matches : (term -> 'a) -> term -> 'a 104val ONCE_DEPTH_matches : (term -> 'a) -> term -> 'a 105val ONCE_DEPTH_USE_IMP_EQ_matches 106 : thm -> term -> (term * term) list * (hol_type * hol_type) list 107val ONCE_DEPTH_USE_IMP_matches 108 : thm -> term -> (term * term) list * (hol_type * hol_type) list 109val USE_IMP_THEN : thm_tactic -> thm -> tactic 110val USE_IMP_TAC : thm -> tactic 111val USE_IMP_AND_THEN : thm_tactic -> thm -> tactic -> tactic 112val USE_THEN : thm_tactic -> thm -> tactic 113val USE_TAC : thm -> tactic 114val USE_AND_THEN : thm_tactic -> thm -> tactic -> tactic 115 116val RES2_THEN : thm_tactic -> tactic 117val IMP_RES2_THEN : thm_tactic -> thm -> tactic 118val IMP_RES_M_THEN : thm_tactic -> thm -> tactic 119val RES_M_THEN : thm_tactic -> tactic 120 121val REWRITE_THM : thm -> tactic 122val ASM_REWRITE_THM : thm -> tactic 123val ONCE_REWRITE_THM : thm -> tactic 124val IMP_RES_REWRITE_TAC : thm -> tactic 125val RES_REWRITE_TAC : tactic 126 127val REWRITE_ASSUM_TAC : thm list -> tactic 128val REWRITE_ALL_TAC : thm list -> tactic 129val ASM_REWRITE_ALL_TAC : thm list -> tactic 130val ONCE_REWRITE_ASSUM_TAC : thm list -> tactic 131val ONCE_REWRITE_ALL_TAC : thm list -> tactic 132val ONCE_ASM_REWRITE_ALL_TAC : thm list -> tactic 133 134val REWRITE_ALL_THM : thm -> tactic 135val ASM_REWRITE_ALL_THM : thm -> tactic 136val ONCE_REWRITE_ALL_THM : thm -> tactic 137val ONCE_ASM_REWRITE_ALL_THM : thm -> tactic 138 139val UNIFY_VARS_TAC : tactic 140 141val EVERY1 : tactic list -> tactic 142 143end (* sig *) 144