1signature pairLib =
2sig
3 include Abbrev
4
5 val add_pair_compset : computeLib.compset -> unit
6
7 (* from pairSyntax *)
8
9 val mk_prod          : hol_type * hol_type -> hol_type
10 val dest_prod        : hol_type -> hol_type * hol_type
11 val list_mk_prod     : hol_type list -> hol_type
12 val strip_prod       : hol_type -> hol_type list
13
14 val comma_tm         : term
15 val fst_tm           : term
16 val snd_tm           : term
17 val uncurry_tm       : term
18 val curry_tm         : term
19 val pair_map_tm      : term
20
21 val mk_pair          : term * term -> term
22 val mk_fst           : term -> term
23 val mk_snd           : term -> term
24 val mk_curry         : term * term * term -> term
25 val mk_uncurry       : term * term -> term
26 val mk_pair_map      : term * term -> term
27 val mk_pabs          : term * term -> term
28 val mk_pforall       : term * term -> term
29 val mk_pexists       : term * term -> term
30 val mk_pexists1      : term * term -> term
31 val mk_pselect       : term * term -> term
32
33 val dest_pair        : term -> term * term
34 val dest_fst         : term -> term
35 val dest_snd         : term -> term
36 val dest_curry       : term -> term * term * term
37 val dest_uncurry     : term -> term * term
38 val dest_pair_map    : term -> term * term
39 val dest_pabs        : term -> term * term
40 val pbvar            : term -> term
41 val pbody            : term -> term
42 val dest_pforall     : term -> term * term
43 val dest_pexists     : term -> term * term
44 val dest_pexists1    : term -> term * term
45 val dest_pselect     : term -> term * term
46 val dest_pbinder     : term -> exn -> term -> term * term
47
48 val list_mk_pair     : term list -> term
49 val list_mk_pabs     : term list * term -> term
50 val list_mk_pforall  : term list * term -> term
51 val list_mk_pexists  : term list * term -> term
52 val strip_pair       : term -> term list
53 val spine_pair       : term -> term list
54 val unstrip_pair     : hol_type -> term list -> term * term list
55 val strip_pabs       : term -> term list * term
56 val strip_pforall    : term -> term list * term
57 val strip_pexists    : term -> term list * term
58
59 val is_pair          : term -> bool
60 val is_fst           : term -> bool
61 val is_snd           : term -> bool
62 val is_curry         : term -> bool
63 val is_uncurry       : term -> bool
64 val is_pair_map      : term -> bool
65 val is_pabs          : term -> bool
66 val is_pforall       : term -> bool
67 val is_pexists       : term -> bool
68 val is_pexists1      : term -> bool
69 val is_pselect       : term -> bool
70 val is_vstruct       : term -> bool
71
72 val genvarstruct     : hol_type -> term
73
74 (* From PairedLambda *)
75
76 val PAIRED_BETA_CONV : conv
77 val PAIRED_ETA_CONV  : conv
78 val GEN_BETA_CONV    : conv
79 val let_CONV         : conv
80 val LET_SIMP_CONV    : bool -> conv
81 val GEN_BETA_RULE    : thm -> thm
82 val GEN_BETA_TAC     : tactic
83
84 (* from Pair_basic *)
85
86(*
87 val MK_PAIR : thm * thm -> thm
88 val PABS : term -> thm -> thm
89 val PABS_CONV : conv -> conv
90 val PSUB_CONV : conv -> conv
91 val CURRY_CONV : conv
92 val UNCURRY_CONV : conv
93 val PBETA_CONV : conv
94 val PBETA_RULE : thm -> thm
95 val PBETA_TAC : tactic
96 val RIGHT_PBETA : thm -> thm
97 val LIST_PBETA_CONV : conv
98 val RIGHT_LIST_PBETA : thm -> thm
99 val LEFT_PBETA : thm -> thm
100 val LEFT_LIST_PBETA : thm -> thm
101 val UNPBETA_CONV : term -> conv
102 val PETA_CONV : conv
103 val PALPHA_CONV : term -> conv
104 val GEN_PALPHA_CONV : term -> conv
105 val PALPHA : term -> conv
106 val paconv : term -> term -> bool
107 val PAIR_CONV : conv -> conv
108*)
109
110 (* from pairTools *)
111
112 val PairCases        : tactic
113 val PairCases_on     : term quotation -> tactic
114 val PGEN             : term -> term -> thm -> thm
115 val PGEN_TAC         : term -> tactic
116 val PFUN_EQ_RULE     : thm -> thm
117 val LET_INTRO        : thm -> thm
118 val LET_EQ_TAC       : thm list -> tactic
119 val TUPLE            : term -> thm -> thm
120 val TUPLE_TAC        : term -> tactic
121
122 val LET_INTRO_TAC    : tactic
123 val split_uncurry_arg_tac : term -> tactic
124 val pairarg_tac      : tactic
125 val split_pair_case0_tac : term -> tactic
126 val split_pair_case_tac : tactic
127
128 val new_specification : string * string list * thm -> thm
129end
130