Structure pairTheory


Source File Identifier index Theory binding index

signature pairTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val ABS_REP_prod : thm
    val COMMA_DEF : thm
    val CURRY_DEF : thm
    val LEX_DEF : thm
    val PAIR : thm
    val PAIR_MAP : thm
    val RPROD_DEF : thm
    val SWAP_def : thm
    val UNCURRY : thm
    val pair_CASE_def : thm
    val prod_TY_DEF : thm

  (*  Theorems  *)
    val ABS_PAIR_THM : thm
    val CLOSED_PAIR_EQ : thm
    val CURRY_ONE_ONE_THM : thm
    val CURRY_UNCURRY_THM : thm
    val C_UNCURRY_L : thm
    val ELIM_PEXISTS : thm
    val ELIM_PEXISTS_EVAL : thm
    val ELIM_PFORALL : thm
    val ELIM_PFORALL_EVAL : thm
    val ELIM_UNCURRY : thm
    val EXISTS_PROD : thm
    val FORALL_PROD : thm
    val FORALL_UNCURRY : thm
    val FST : thm
    val FST_PAIR_MAP : thm
    val LAMBDA_PROD : thm
    val LET2_RAND : thm
    val LET2_RATOR : thm
    val LEX_DEF_THM : thm
    val PAIR_EQ : thm
    val PAIR_FST_SND_EQ : thm
    val PAIR_FUN_THM : thm
    val PAIR_MAP_THM : thm
    val PEXISTS_THM : thm
    val PFORALL_THM : thm
    val SND : thm
    val SND_PAIR_MAP : thm
    val S_UNCURRY_R : thm
    val UNCURRY_CONG : thm
    val UNCURRY_CURRY_THM : thm
    val UNCURRY_DEF : thm
    val UNCURRY_ONE_ONE_THM : thm
    val UNCURRY_VAR : thm
    val WF_LEX : thm
    val WF_RPROD : thm
    val datatype_pair : thm
    val o_UNCURRY_R : thm
    val pair_Axiom : thm
    val pair_CASES : thm
    val pair_case_cong : thm
    val pair_case_def : thm
    val pair_case_thm : thm
    val pair_induction : thm
    val reflexive_LEX : thm
    val symmetric_LEX : thm
    val total_LEX : thm
    val transitive_LEX : thm

  val pair_grammars : type_grammar.grammar * term_grammar.grammar

  val pair_rws : thm list


  type hol_type = Abbrev.hol_type
  type term     = Abbrev.term
  type conv     = Abbrev.conv

  val uncurry_tm       : term
  val comma_tm         : term
  val dest_pair        : term -> term * term
  val strip_pair       : term -> term list
  val spine_pair       : term -> term list
  val is_vstruct       : term -> bool
  val mk_pabs          : term * term -> term
  val PAIRED_BETA_CONV : conv

(*
   [relation] Parent theory of "pair"

   [ABS_REP_prod]  Definition

      |- (∀a. ABS_prod (REP_prod a) = a) ∧
         ∀r.
           (λp. ∃x y. p = (λa b. (a = x) ∧ (b = y))) r ⇔
           (REP_prod (ABS_prod r) = r)

   [COMMA_DEF]  Definition

      |- ∀x y. (x,y) = ABS_prod (λa b. (a = x) ∧ (b = y))

   [CURRY_DEF]  Definition

      |- ∀f x y. CURRY f x y = f (x,y)

   [LEX_DEF]  Definition

      |- ∀R1 R2. R1 LEX R2 = (λ(s,t) (u,v). R1 s u ∨ (s = u) ∧ R2 t v)

   [PAIR]  Definition

      |- ∀x. (FST x,SND x) = x

   [PAIR_MAP]  Definition

      |- ∀f g p. (f ## g) p = (f (FST p),g (SND p))

   [RPROD_DEF]  Definition

      |- ∀R1 R2. RPROD R1 R2 = (λ(s,t) (u,v). R1 s u ∧ R2 t v)

   [SWAP_def]  Definition

      |- ∀a. SWAP a = (SND a,FST a)

   [UNCURRY]  Definition

      |- ∀f v. UNCURRY f v = f (FST v) (SND v)

   [pair_CASE_def]  Definition

      |- ∀p f. pair_CASE p f = f (FST p) (SND p)

   [prod_TY_DEF]  Definition

      |- ∃rep.
           TYPE_DEFINITION (λp. ∃x y. p = (λa b. (a = x) ∧ (b = y))) rep

   [ABS_PAIR_THM]  Theorem

      |- ∀x. ∃q r. x = (q,r)

   [CLOSED_PAIR_EQ]  Theorem

      |- ∀x y a b. ((x,y) = (a,b)) ⇔ (x = a) ∧ (y = b)

   [CURRY_ONE_ONE_THM]  Theorem

      |- (CURRY f = CURRY g) ⇔ (f = g)

   [CURRY_UNCURRY_THM]  Theorem

      |- ∀f. CURRY (UNCURRY f) = f

   [C_UNCURRY_L]  Theorem

      |- combin$C (UNCURRY f) x = UNCURRY (combin$C (combin$C o f) x)

   [ELIM_PEXISTS]  Theorem

      |- (∃p. P (FST p) (SND p)) ⇔ ∃p1 p2. P p1 p2

   [ELIM_PEXISTS_EVAL]  Theorem

      |- $? (UNCURRY (λx. P x)) ⇔ ∃x. $? (P x)

   [ELIM_PFORALL]  Theorem

      |- (∀p. P (FST p) (SND p)) ⇔ ∀p1 p2. P p1 p2

   [ELIM_PFORALL_EVAL]  Theorem

      |- $! (UNCURRY (λx. P x)) ⇔ ∀x. $! (P x)

   [ELIM_UNCURRY]  Theorem

      |- ∀f. UNCURRY f = (λx. f (FST x) (SND x))

   [EXISTS_PROD]  Theorem

      |- (∃p. P p) ⇔ ∃p_1 p_2. P (p_1,p_2)

   [FORALL_PROD]  Theorem

      |- (∀p. P p) ⇔ ∀p_1 p_2. P (p_1,p_2)

   [FORALL_UNCURRY]  Theorem

      |- $! (UNCURRY f) ⇔ $! ($! o f)

   [FST]  Theorem

      |- ∀x y. FST (x,y) = x

   [FST_PAIR_MAP]  Theorem

      |- ∀p f g. FST ((f ## g) p) = f (FST p)

   [LAMBDA_PROD]  Theorem

      |- ∀P. (λp. P p) = (λ(p1,p2). P (p1,p2))

   [LET2_RAND]  Theorem

      |- ∀P M N. P (let (x,y) = M in N x y) = (let (x,y) = M in P (N x y))

   [LET2_RATOR]  Theorem

      |- ∀M N b. (let (x,y) = M in N x y) b = (let (x,y) = M in N x y b)

   [LEX_DEF_THM]  Theorem

      |- (R1 LEX R2) (a,b) (c,d) ⇔ R1 a c ∨ (a = c) ∧ R2 b d

   [PAIR_EQ]  Theorem

      |- ((x,y) = (a,b)) ⇔ (x = a) ∧ (y = b)

   [PAIR_FST_SND_EQ]  Theorem

      |- ∀p q. (p = q) ⇔ (FST p = FST q) ∧ (SND p = SND q)

   [PAIR_FUN_THM]  Theorem

      |- ∀P. (∃!f. P f) ⇔ ∃!p. P (λa. (FST p a,SND p a))

   [PAIR_MAP_THM]  Theorem

      |- ∀f g x y. (f ## g) (x,y) = (f x,g y)

   [PEXISTS_THM]  Theorem

      |- ∀P. (∃x y. P x y) ⇔ ∃(x,y). P x y

   [PFORALL_THM]  Theorem

      |- ∀P. (∀x y. P x y) ⇔ ∀(x,y). P x y

   [SND]  Theorem

      |- ∀x y. SND (x,y) = y

   [SND_PAIR_MAP]  Theorem

      |- ∀p f g. SND ((f ## g) p) = g (SND p)

   [S_UNCURRY_R]  Theorem

      |- S f (UNCURRY g) = UNCURRY (S (S o $o f o $,) g)

   [UNCURRY_CONG]  Theorem

      |- ∀f' f M' M.
           (M = M') ∧ (∀x y. (M' = (x,y)) ⇒ (f x y = f' x y)) ⇒
           (UNCURRY f M = UNCURRY f' M')

   [UNCURRY_CURRY_THM]  Theorem

      |- ∀f. UNCURRY (CURRY f) = f

   [UNCURRY_DEF]  Theorem

      |- ∀f x y. UNCURRY f (x,y) = f x y

   [UNCURRY_ONE_ONE_THM]  Theorem

      |- (UNCURRY f = UNCURRY g) ⇔ (f = g)

   [UNCURRY_VAR]  Theorem

      |- ∀f v. UNCURRY f v = f (FST v) (SND v)

   [WF_LEX]  Theorem

      |- ∀R Q. WF R ∧ WF Q ⇒ WF (R LEX Q)

   [WF_RPROD]  Theorem

      |- ∀R Q. WF R ∧ WF Q ⇒ WF (RPROD R Q)

   [datatype_pair]  Theorem

      |- DATATYPE (pair $,)

   [o_UNCURRY_R]  Theorem

      |- f o UNCURRY g = UNCURRY ($o f o g)

   [pair_Axiom]  Theorem

      |- ∀f. ∃fn. ∀x y. fn (x,y) = f x y

   [pair_CASES]  Theorem

      |- ∀x. ∃q r. x = (q,r)

   [pair_case_cong]  Theorem

      |- ∀M M' f.
           (M = M') ∧ (∀x y. (M' = (x,y)) ⇒ (f x y = f' x y)) ⇒
           (pair_CASE M f = pair_CASE M' f')

   [pair_case_def]  Theorem

      |- pair_CASE (x,y) f = f x y

   [pair_case_thm]  Theorem

      |- pair_CASE (x,y) f = f x y

   [pair_induction]  Theorem

      |- (∀p_1 p_2. P (p_1,p_2)) ⇒ ∀p. P p

   [reflexive_LEX]  Theorem

      |- reflexive (R1 LEX R2) ⇔ reflexive R1 ∨ reflexive R2

   [symmetric_LEX]  Theorem

      |- symmetric R1 ∧ symmetric R2 ⇒ symmetric (R1 LEX R2)

   [total_LEX]  Theorem

      |- total R1 ∧ total R2 ⇒ total (R1 LEX R2)

   [transitive_LEX]  Theorem

      |- transitive R1 ∧ transitive R2 ⇒ transitive (R1 LEX R2)


*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-10