Structure pairLib
signature pairLib =
sig
include Abbrev
val add_pair_compset : computeLib.compset -> unit
(* from pairSyntax *)
val mk_prod : hol_type * hol_type -> hol_type
val dest_prod : hol_type -> hol_type * hol_type
val list_mk_prod : hol_type list -> hol_type
val strip_prod : hol_type -> hol_type list
val comma_tm : term
val fst_tm : term
val snd_tm : term
val uncurry_tm : term
val curry_tm : term
val pair_map_tm : term
val mk_pair : term * term -> term
val mk_fst : term -> term
val mk_snd : term -> term
val mk_curry : term * term * term -> term
val mk_uncurry : term * term -> term
val mk_pair_map : term * term -> term
val mk_pabs : term * term -> term
val mk_pforall : term * term -> term
val mk_pexists : term * term -> term
val mk_pexists1 : term * term -> term
val mk_pselect : term * term -> term
val dest_pair : term -> term * term
val dest_fst : term -> term
val dest_snd : term -> term
val dest_curry : term -> term * term * term
val dest_uncurry : term -> term * term
val dest_pair_map : term -> term * term
val dest_pabs : term -> term * term
val pbvar : term -> term
val pbody : term -> term
val dest_pforall : term -> term * term
val dest_pexists : term -> term * term
val dest_pexists1 : term -> term * term
val dest_pselect : term -> term * term
val dest_pbinder : term -> exn -> term -> term * term
val list_mk_pair : term list -> term
val list_mk_pabs : term list * term -> term
val list_mk_pforall : term list * term -> term
val list_mk_pexists : term list * term -> term
val strip_pair : term -> term list
val spine_pair : term -> term list
val unstrip_pair : hol_type -> term list -> term * term list
val strip_pabs : term -> term list * term
val strip_pforall : term -> term list * term
val strip_pexists : term -> term list * term
val is_pair : term -> bool
val is_fst : term -> bool
val is_snd : term -> bool
val is_curry : term -> bool
val is_uncurry : term -> bool
val is_pair_map : term -> bool
val is_pabs : term -> bool
val is_pforall : term -> bool
val is_pexists : term -> bool
val is_pexists1 : term -> bool
val is_pselect : term -> bool
val is_vstruct : term -> bool
val genvarstruct : hol_type -> term
(* From PairedLambda *)
val PAIRED_BETA_CONV : conv
val PAIRED_ETA_CONV : conv
val GEN_BETA_CONV : conv
val let_CONV : conv
val LET_SIMP_CONV : bool -> conv
val GEN_BETA_RULE : thm -> thm
val GEN_BETA_TAC : tactic
(* from Pair_basic *)
(*
val MK_PAIR : thm * thm -> thm
val PABS : term -> thm -> thm
val PABS_CONV : conv -> conv
val PSUB_CONV : conv -> conv
val CURRY_CONV : conv
val UNCURRY_CONV : conv
val PBETA_CONV : conv
val PBETA_RULE : thm -> thm
val PBETA_TAC : tactic
val RIGHT_PBETA : thm -> thm
val LIST_PBETA_CONV : conv
val RIGHT_LIST_PBETA : thm -> thm
val LEFT_PBETA : thm -> thm
val LEFT_LIST_PBETA : thm -> thm
val UNPBETA_CONV : term -> conv
val PETA_CONV : conv
val PALPHA_CONV : term -> conv
val GEN_PALPHA_CONV : term -> conv
val PALPHA : term -> conv
val paconv : term -> term -> bool
val PAIR_CONV : conv -> conv
*)
(* from pairTools *)
val PairCases_on : term quotation -> tactic
val PGEN : term -> term -> thm -> thm
val PGEN_TAC : term -> tactic
val PFUN_EQ_RULE : thm -> thm
val LET_INTRO : thm -> thm
val LET_EQ_TAC : thm list -> tactic
val TUPLE : term -> thm -> thm
val TUPLE_TAC : term -> tactic
val LET_INTRO_TAC : tactic
end
HOL 4, Kananaskis-10