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