Pair (nholz)

Pair Module

Namespace: HOL
Assembly: nholz.dll

This module extends the HOL logic with the theory of ordered pairs. This involves giving theory object definitions for the product type operator, the pairing function and the constants "FST" and "SND", and proving a few basic properties. Syntax functions and equality congruence rules are also provided.

Functions and values

Function or value	Description
`dest_pair tm` Full Usage: `dest_pair tm` Parameters: tm : `term` Returns: `term * term`	tm : `term` Returns: `term * term`
`dest_prod_type ty` Full Usage: `dest_prod_type ty` Parameters: ty : `hol_type` Returns: `hol_type * hol_type`	ty : `hol_type` Returns: `hol_type * hol_type`
`flatstrip_pair tm` Full Usage: `flatstrip_pair tm` Parameters: tm : `term` Returns: `term list`	tm : `term` Returns: `term list`
`fst_def` Full Usage: `fst_def` Returns: `thm`	Selects the first component of a pair \|- FST = (\(p:'a#'b). @x. ?y. p = (x,y)) Returns: `thm`
`fst_snd_thm` Full Usage: `fst_snd_thm` Returns: `thm`	\|- !p. (FST p, SND p) = p Returns: `thm`
`fst_thm` Full Usage: `fst_thm` Returns: `thm`	\|- !x y. FST (x,y) = x Returns: `thm`
`is_pair tm` Full Usage: `is_pair tm` Parameters: tm : `term` Returns: `bool`	tm : `term` Returns: `bool`
`is_pair_rep_def` Full Usage: `is_pair_rep_def` Returns: `thm`	"IsPairRep" is the characteristic function for the product type operator. It takes a boolean-valued binary function and returns whether there is a pair for which this is the concrete representation. \|- IsPairRep = (\(r:'a->'b->bool). ?a b. r = MkPairRep a b) Returns: `thm`
`is_prod_type ty` Full Usage: `is_prod_type ty` Parameters: ty : `hol_type` Returns: `bool`	ty : `hol_type` Returns: `bool`
`list_mk_pair tms` Full Usage: `list_mk_pair tms` Parameters: tms : `term list` Returns: `term`	tms : `term list` Returns: `term`
`list_mk_prod_type tys` Full Usage: `list_mk_prod_type tys` Parameters: tys : `hol_type list` Returns: `hol_type`	tys : `hol_type list` Returns: `hol_type`
`load` Full Usage: `load` Returns: `(string * thm) list`	Force module evaluation Returns: `(string * thm) list`
`mk_pair (tm1, tm2)` Full Usage: `mk_pair (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	tm1 : `term` tm2 : `term` Returns: `term`
`mk_pair1_rule th1 tm` Full Usage: `mk_pair1_rule th1 tm` Parameters: th1 : `thm` tm : `term` Returns: `thm`	This is the equality congruence rule for pair LHS. It takes an equality theorem and a term, and pairs each side of the theorem with the term. A \|- x1 = x2 `y` -------------------- A \|- (x1,y) = (x2,y) See also: mk_pair2_rule, mk_pair_rule, mk_bin1_rule. th1 : `thm` tm : `term` Returns: `thm`
`mk_pair2_rule tm th2` Full Usage: `mk_pair2_rule tm th2` Parameters: tm : `term` th2 : `thm` Returns: `thm`	This is the equality congruence rule for pair RHS. It takes a term and an equality theorem, and pairs the term with each side of the theorem. `x` A \|- y1 = y2 -------------------- A \|- (x,y1) = (x,y2) See also: mk_pair1_rule, mk_pair_rule, mk_bin2_rule. tm : `term` th2 : `thm` Returns: `thm`
`mk_pair_rep_def` Full Usage: `mk_pair_rep_def` Returns: `thm`	The "MkPairRep" function returns the concrete representation for a given pair's two components (i.e. the representation in terms of existing types, before the product type is defined). This representation is a function that takes two arguments and returns `true` for just one combination of its arguments - when each argument is equal to its respective pair component. This is used to define both "IsPairRep" and the pairing function. \|- MkPairRep = (\(x:'a) (y:'b) a b. a = x /\ b = y) Returns: `thm`
`mk_pair_rep_lemma` Full Usage: `mk_pair_rep_lemma` Returns: `thm`	Returns: `thm`
`mk_pair_rule th1 th2` Full Usage: `mk_pair_rule th1 th2` Parameters: th1 : `thm` th2 : `thm` Returns: `thm`	This is the equality congruence rule for pairing. It takes two equality theorems, and pairs corresponding sides of the first theorem with the second, unioning the assumptions. A1 \|- x1 = x2 A2 \|- y1 = y2 ------------------------------ A1 u A2 \|- (x1,y1) = (x2,y2) See also: mk_pair1_rule, mk_pair2_rule, mk_bin_rule. th1 : `thm` th2 : `thm` Returns: `thm`
`mk_prod_type (ty1, ty2)` Full Usage: `mk_prod_type (ty1, ty2)` Parameters: ty1 : `hol_type` ty2 : `hol_type` Returns: `hol_type`	ty1 : `hol_type` ty2 : `hol_type` Returns: `hol_type`
`pair_def` Full Usage: `pair_def` Returns: `thm`	The pairing function, called "PAIR", takes two arguments and returns the corresponding element in the product type. It is simply defined as the product type's abstraction of the "MkPairRep" function. It has special support in the parser/printer, so that the quotation `(t1,t2)` is parsed/ printed for the internal term `PAIR t1 t2`. \|- PAIR = (\(x:'a) (y:'b). PairAbs (MkPairRep x y)) Returns: `thm`
`pair_eq_thm` Full Usage: `pair_eq_thm` Returns: `thm`	Returns: `thm`
`pair_rep_exists_lemma` Full Usage: `pair_rep_exists_lemma` Returns: `thm`	Returns: `thm`
`pair_surjective_thm` Full Usage: `pair_surjective_thm` Returns: `thm`	\|- !p. ?x y. p = (x,y) Returns: `thm`
`prod_bij_def1` Full Usage: `prod_bij_def1` Returns: `thm`	Returns: `thm`
`prod_bij_def2` Full Usage: `prod_bij_def2` Returns: `thm`	Returns: `thm`
`prod_def` Full Usage: `prod_def` Returns: `thm`	\|- ?(f:'a#'b->'a->'b->bool). TYPE_DEFINITION IsPairRep '#' is the product type operator: it denotes the cartesian product operation Returns: `thm`
`rep_abs_pair_lemma` Full Usage: `rep_abs_pair_lemma` Returns: `thm`	Returns: `thm`
`snd_def` Full Usage: `snd_def` Returns: `thm`	Selects the second component of a pair \|- SND = (\(p:'a#'b). @y. ?x. p = (x,y)) Returns: `thm`
`snd_thm` Full Usage: `snd_thm` Returns: `thm`	\|- !x y. SND (x,y) = y Returns: `thm`
`strip_pair tm` Full Usage: `strip_pair tm` Parameters: tm : `term` Returns: `term list`	tm : `term` Returns: `term list`
`strip_prod_type ty` Full Usage: `strip_prod_type ty` Parameters: ty : `hol_type` Returns: `hol_type list`	ty : `hol_type` Returns: `hol_type list`