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