Structure pairTheory

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 PAIR_SET_def : thm
    val PROD_ALL_def : 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 COMMA_PRS : thm
    val COMMA_RSP : thm
    val CURRY_ONE_ONE_THM : thm
    val CURRY_PRS : thm
    val CURRY_RSP : 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_EQ_EQUIV : thm
    val FST_PAIR_MAP : thm
    val FST_PRS : thm
    val FST_RSP : thm
    val IN_PAIR_SET : thm
    val IN_UNCURRY_R : thm
    val IN_setFSTSND : thm
    val LAMBDA_PROD : thm
    val LET2_RAND : thm
    val LET2_RATOR : thm
    val LEX_CONG : thm
    val LEX_DEF_THM : thm
    val LEX_MONO : thm
    val PAIR_EQ : thm
    val PAIR_EQUIV : thm
    val PAIR_FST_SND_EQ : thm
    val PAIR_FUN_THM : thm
    val PAIR_MAP_CONG : thm
    val PAIR_MAP_I : thm
    val PAIR_MAP_PRS : thm
    val PAIR_MAP_RSP : thm
    val PAIR_MAP_SET : thm
    val PAIR_MAP_THM : thm
    val PAIR_QUOTIENT : thm
    val PAIR_REL : thm
    val PAIR_REL_EQ : thm
    val PAIR_REL_REFL : thm
    val PAIR_REL_SYM : thm
    val PAIR_REL_THM : thm
    val PAIR_REL_TRANS : thm
    val PEXISTS_THM : thm
    val PFORALL_THM : thm
    val PROD_ALL_CONG : thm
    val PROD_ALL_MONO : thm
    val PROD_ALL_THM : thm
    val SND : thm
    val SND_EQ_EQUIV : thm
    val SND_PAIR_MAP : thm
    val SND_PRS : thm
    val SND_RSP : thm
    val SWAP_SWAP : 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_PRS : thm
    val UNCURRY_RSP : 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_eq : thm
    val pair_case_ho_elim : 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
  
(*
   [quotient] Parent theory of "pair"
   
   [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))
   
   [PAIR_SET_def]  Definition
      
      ⊢ ∀f g. PAIR_SET f g = (λ(a,b) c. c ∈ f a ∨ c ∈ g b)
   
   [PROD_ALL_def]  Definition
      
      ⊢ ∀P Q p. PROD_ALL P Q p ⇔ P (FST p) ∧ Q (SND p)
   
   [RPROD_DEF]  Definition
      
      ⊢ ∀R1 R2. 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
   
   [COMMA_PRS]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀a b. (a,b) = (abs1 ## abs2) (rep1 a,rep2 b)
   
   [COMMA_RSP]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀a1 a2 b1 b2. R1 a1 b1 ∧ R2 a2 b2 ⇒ (R1 ### R2) (a1,a2) (b1,b2)
   
   [CURRY_ONE_ONE_THM]  Theorem
      
      ⊢ CURRY f = CURRY g ⇔ f = g
   
   [CURRY_PRS]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀f a b.
                CURRY f a b =
                abs3
                  (CURRY (((abs1 ## abs2) --> rep3) f) (rep1 a) (rep2 b))
   
   [CURRY_RSP]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀f1 f2.
                ((R1 ### R2) ===> R3) f1 f2 ⇒
                (R1 ===> R2 ===> R3) (CURRY f1) (CURRY f2)
   
   [CURRY_UNCURRY_THM]  Theorem
      
      ⊢ ∀f. CURRY (UNCURRY f) = f
   
   [C_UNCURRY_L]  Theorem
      
      ⊢ flip (UNCURRY f) x = UNCURRY (flip (flip ∘ 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) ⇔ $! ($! ∘ f)
   
   [FST]  Theorem
      
      ⊢ ∀x y. FST (x,y) = x
   
   [FST_EQ_EQUIV]  Theorem
      
      ⊢ FST p = x ⇔ ∃y. p = (x,y)
   
   [FST_PAIR_MAP]  Theorem
      
      ⊢ ∀p f g. FST ((f ## g) p) = f (FST p)
   
   [FST_PRS]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀p. FST p = abs1 (FST ((rep1 ## rep2) p))
   
   [FST_RSP]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀p1 p2. (R1 ### R2) p1 p2 ⇒ R1 (FST p1) (FST p2)
   
   [IN_PAIR_SET]  Theorem
      
      ⊢ c ∈ PAIR_SET f g (a,b) ⇔ c ∈ f a ∨ c ∈ g b
   
   [IN_UNCURRY_R]  Theorem
      
      ⊢ (x,y) ∈ UNCURRY R ⇔ R x y
   
   [IN_setFSTSND]  Theorem
      
      ⊢ (a ∈ setFST ab ⇔ FST ab = a) ∧ (b ∈ setSND ab ⇔ SND ab = b)
   
   [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_CONG]  Theorem
      
      ⊢ ∀R1 R2 v1 v2 R1' R2' v1' v2'.
          v1 = v1' ∧ v2 = v2' ∧
          (∀a b c d. v1' = (a,b) ∧ v2' = (c,d) ⇒ (R1 a c ⇔ R1' a c)) ∧
          (∀a b c d. v1' = (a,b) ∧ v2' = (c,d) ∧ a = c ⇒ (R2 b d ⇔ R2' b d)) ⇒
          ((R1 LEX R2) v1 v2 ⇔ (R1' LEX R2') v1' v2')
   
   [LEX_DEF_THM]  Theorem
      
      ⊢ (R1 LEX R2) (a,b) (c,d) ⇔ R1 a c ∨ a = c ∧ R2 b d
   
   [LEX_MONO]  Theorem
      
      ⊢ (∀x y. R1 x y ⇒ R2 x y) ∧ (∀x y. R3 x y ⇒ R4 x y) ⇒
        (R1 LEX R3) x y ⇒
        (R2 LEX R4) x y
   
   [PAIR_EQ]  Theorem
      
      ⊢ (x,y) = (a,b) ⇔ x = a ∧ y = b
   
   [PAIR_EQUIV]  Theorem
      
      ⊢ ∀R1 R2. EQUIV R1 ⇒ EQUIV R2 ⇒ EQUIV (R1 ### R2)
   
   [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_CONG]  Theorem
      
      ⊢ (∀a. a ∈ setFST ab ⇒ f1 a = f2 a) ∧
        (∀b. b ∈ setSND ab ⇒ g1 b = g2 b) ⇒
        (f1 ## g1) ab = (f2 ## g2) ab
   
   [PAIR_MAP_I]  Theorem
      
      ⊢ I ## I = I
   
   [PAIR_MAP_PRS]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀R4 abs4 rep4.
                QUOTIENT R4 abs4 rep4 ⇒
                ∀f g.
                  f ## g =
                  ((rep1 ## rep3) --> (abs2 ## abs4))
                    ((abs1 --> rep2) f ## (abs3 --> rep4) g)
   
   [PAIR_MAP_RSP]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀R4 abs4 rep4.
                QUOTIENT R4 abs4 rep4 ⇒
                ∀f1 f2 g1 g2.
                  (R1 ===> R2) f1 f2 ∧ (R3 ===> R4) g1 g2 ⇒
                  ((R1 ### R3) ===> R2 ### R4) (f1 ## g1) (f2 ## g2)
   
   [PAIR_MAP_SET]  Theorem
      
      ⊢ (c ∈ setFST ((f ## g) ab) ⇔ ∃a. c = f a ∧ a ∈ setFST ab) ∧
        (d ∈ setSND ((f ## g) ab) ⇔ ∃b. d = g b ∧ b ∈ setSND ab)
   
   [PAIR_MAP_THM]  Theorem
      
      ⊢ ∀f g x y. (f ## g) (x,y) = (f x,g y)
   
   [PAIR_QUOTIENT]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            QUOTIENT (R1 ### R2) (abs1 ## abs2) (rep1 ## rep2)
   
   [PAIR_REL]  Theorem
      
      ⊢ ∀R1 R2. R1 ### R2 = (λ(s,t) (u,v). R1 s u ∧ R2 t v)
   
   [PAIR_REL_EQ]  Theorem
      
      ⊢ $= ### $= = $=
   
   [PAIR_REL_REFL]  Theorem
      
      ⊢ (∀x. R1 x x) ∧ (∀y. R2 y y) ⇒ ∀xy. (R1 ### R2) xy xy
   
   [PAIR_REL_SYM]  Theorem
      
      ⊢ (∀x y. R1 x y ⇔ R1 y x) ∧ (∀a b. R2 a b ⇔ R2 b a) ⇒
        ∀xy ab. (R1 ### R2) xy ab ⇔ (R1 ### R2) ab xy
   
   [PAIR_REL_THM]  Theorem
      
      ⊢ (R1 ### R2) (a,b) (c,d) ⇔ R1 a c ∧ R2 b d
   
   [PAIR_REL_TRANS]  Theorem
      
      ⊢ (∀x y z. R1 x y ∧ R1 y z ⇒ R1 x z) ∧
        (∀a b c. R2 a b ∧ R2 b c ⇒ R2 a c) ⇒
        ∀xy ab uv.
          (R1 ### R2) xy ab ∧ (R1 ### R2) ab uv ⇒ (R1 ### R2) xy uv
   
   [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
   
   [PROD_ALL_CONG]  Theorem
      
      ⊢ ∀p p' P P' Q Q'.
          p = p' ∧ (∀x y. p' = (x,y) ⇒ (P x ⇔ P' x)) ∧
          (∀x y. p' = (x,y) ⇒ (Q y ⇔ Q' y)) ⇒
          (PROD_ALL P Q p ⇔ PROD_ALL P' Q' p')
   
   [PROD_ALL_MONO]  Theorem
      
      ⊢ (∀x. P x ⇒ P' x) ∧ (∀y. Q y ⇒ Q' y) ⇒
        PROD_ALL P Q p ⇒
        PROD_ALL P' Q' p
   
   [PROD_ALL_THM]  Theorem
      
      ⊢ PROD_ALL P Q (x,y) ⇔ P x ∧ Q y
   
   [SND]  Theorem
      
      ⊢ ∀x y. SND (x,y) = y
   
   [SND_EQ_EQUIV]  Theorem
      
      ⊢ SND p = y ⇔ ∃x. p = (x,y)
   
   [SND_PAIR_MAP]  Theorem
      
      ⊢ ∀p f g. SND ((f ## g) p) = g (SND p)
   
   [SND_PRS]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀p. SND p = abs2 (SND ((rep1 ## rep2) p))
   
   [SND_RSP]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀p1 p2. (R1 ### R2) p1 p2 ⇒ R2 (SND p1) (SND p2)
   
   [SWAP_SWAP]  Theorem
      
      ⊢ ∀x. SWAP (SWAP x) = x
   
   [S_UNCURRY_R]  Theorem
      
      ⊢ S f (UNCURRY g) = UNCURRY (S (S ∘ $o f ∘ $,) 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_PRS]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀f p.
                UNCURRY f p =
                abs3
                  (UNCURRY ((abs1 --> abs2 --> rep3) f) ((rep1 ## rep2) p))
   
   [UNCURRY_RSP]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀R3 abs3 rep3.
              QUOTIENT R3 abs3 rep3 ⇒
              ∀f1 f2.
                (R1 ===> R2 ===> R3) f1 f2 ⇒
                ((R1 ### R2) ===> R3) (UNCURRY f1) (UNCURRY f2)
   
   [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 (R ### Q)
   
   [datatype_pair]  Theorem
      
      ⊢ DATATYPE (pair $,)
   
   [o_UNCURRY_R]  Theorem
      
      ⊢ f ∘ UNCURRY g = UNCURRY ($o f ∘ 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_eq]  Theorem
      
      ⊢ pair_CASE p f = v ⇔ ∃x y. p = (x,y) ∧ f x y = v
   
   [pair_case_ho_elim]  Theorem
      
      ⊢ ∀f'. f' (pair_CASE p f) ⇔ ∃x y. p = (x,y) ∧ f' (f x y)
   
   [pair_case_thm]  Theorem
      
      ⊢ pair_CASE (x,y) f = f x y
   
   [pair_induction]  Theorem
      
      ⊢ ∀P. (∀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

HOL 4, Trindemossen-1