1signature pairSyntax =
2sig
3 include Abbrev
4
5 val mk_prod         : hol_type * hol_type -> hol_type
6 val dest_prod       : hol_type -> hol_type * hol_type
7 val list_mk_prod    : hol_type list -> hol_type
8 val strip_prod      : hol_type -> hol_type list
9 val spine_prod      : hol_type -> hol_type list
10
11 val comma_tm        : term
12 val fst_tm          : term
13 val snd_tm          : term
14 val swap_tm         : term
15 val uncurry_tm      : term
16 val curry_tm        : term
17 val pair_map_tm     : term
18 val lex_tm          : term
19 val pair_case_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_swap         : term -> term
25 val mk_curry        : term * term * term -> term
26 val mk_uncurry      : term * term -> term
27 val mk_pair_map     : term * term -> term
28 val mk_lex          : term * term -> term
29 val mk_pabs         : term * term -> term
30 val mk_pforall      : term * term -> term
31 val mk_pexists      : term * term -> term
32 val mk_pexists1     : term * term -> term
33 val mk_pselect      : term * term -> term
34 val mk_plet         : term * term * term -> term
35 val mk_anylet       : (term * term) list * term -> term
36 val mk_pair_case    : {pairtm : term, ftm : term} -> term
37
38 val dest_pair       : term -> term * term
39 val dest_fst        : term -> term
40 val dest_snd        : term -> term
41 val dest_swap       : term -> term
42 val dest_curry      : term -> term * term * term
43 val dest_uncurry    : term -> term * term
44 val dest_pair_map   : term -> term * term
45 val dest_lex        : term -> term * term
46 val dest_pabs       : term -> term * term
47 val pbvar           : term -> term
48 val pbody           : term -> term
49 val dest_plet       : term -> term * term * term
50 val dest_anylet     : term -> (term * term) list * term
51 val dest_pforall    : term -> term * term
52 val dest_pexists    : term -> term * term
53 val dest_pexists1   : term -> term * term
54 val dest_pselect    : term -> term * term
55 val dest_pbinder    : term -> exn -> term -> term * term
56 val dest_pair_case  : term -> {pairtm : term, ftm: term}
57
58
59 val list_mk_pair    : term list -> term
60 val list_mk_pabs    : term list * term -> term
61 val list_mk_anylet  : (term * term) list list * term -> term
62 val list_mk_pforall : term list * term -> term
63 val list_mk_pexists : term list * term -> term
64 val strip_pair      : term -> term list
65 val spine_pair      : term -> term list
66 val unstrip_pair    : hol_type -> term list -> term * term list
67 val strip_pabs      : term -> term list * term
68 val strip_anylet    : term -> (term * term) list list * term
69 val strip_pforall   : term -> term list * term
70 val strip_pexists   : term -> term list * term
71
72
73 val is_pair         : term -> bool
74 val is_pair_case    : term -> bool
75 val is_fst          : term -> bool
76 val is_snd          : term -> bool
77 val is_swap         : term -> bool
78 val is_curry        : term -> bool
79 val is_uncurry      : term -> bool
80 val is_pair_map     : term -> bool
81 val is_lex          : term -> bool
82 val is_pabs         : term -> bool
83 val is_plet         : term -> bool
84 val is_pforall      : term -> bool
85 val is_pexists      : term -> bool
86 val is_pexists1     : term -> bool
87 val is_pselect      : term -> bool
88 val is_vstruct      : term -> bool
89
90 val genvarstruct    : hol_type -> term
91
92 val  lift_prod      : hol_type -> ('a -> term ) -> ('b -> term)
93                                -> 'a * 'b -> term
94end
95