Structure sumTheory

signature sumTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val INL_DEF : thm
    val INR_DEF : thm
    val ISL : thm
    val ISR : thm
    val IS_SUM_REP : thm
    val OUTL : thm
    val OUTR : thm
    val SUM_ALL_def : thm
    val SUM_FIN_def : thm
    val SUM_MAP_def : thm
    val SUM_REL_def : thm
    val SUM_SET_def : thm
    val sum_ISO_DEF : thm
    val sum_TY_DEF : thm
    val sum_case_def : thm
  
  (*  Theorems  *)
    val EXISTS_SUM : thm
    val FORALL_SUM : thm
    val INL : thm
    val INL_11 : thm
    val INL_PRS : thm
    val INL_RSP : thm
    val INR : thm
    val INR_11 : thm
    val INR_INL_11 : thm
    val INR_PRS : thm
    val INR_RSP : thm
    val INR_neq_INL : thm
    val IN_SUM_FIN_THM : thm
    val ISL_OR_ISR : thm
    val ISL_PRS : thm
    val ISL_RSP : thm
    val ISR_PRS : thm
    val ISR_RSP : thm
    val NOT_ISL_ISR : thm
    val NOT_ISR_ISL : thm
    val SUM_ALL_CONG : thm
    val SUM_ALL_MONO : thm
    val SUM_ALL_SET : thm
    val SUM_EQUIV : thm
    val SUM_MAP : thm
    val SUM_MAP_CASE : thm
    val SUM_MAP_CONG : thm
    val SUM_MAP_I : thm
    val SUM_MAP_PRS : thm
    val SUM_MAP_RSP : thm
    val SUM_MAP_SET : thm
    val SUM_MAP_o : thm
    val SUM_QUOTIENT : thm
    val SUM_REL_EQ : thm
    val SUM_REL_REFL : thm
    val SUM_REL_SYM : thm
    val SUM_REL_THM : thm
    val SUM_REL_TRANS : thm
    val SUM_SETLR_THM : thm
    val cond_sum_expand : thm
    val datatype_sum : thm
    val sum_Axiom : thm
    val sum_CASES : thm
    val sum_INDUCT : thm
    val sum_axiom : thm
    val sum_case_cong : thm
    val sum_distinct : thm
    val sum_distinct1 : thm
  
  val sum_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [pair] Parent theory of "sum"
   
   [INL_DEF]  Definition
      
      ⊢ ∀e. INL e = ABS_sum (λb x y. x = e ∧ b)
   
   [INR_DEF]  Definition
      
      ⊢ ∀e. INR e = ABS_sum (λb x y. y = e ∧ ¬b)
   
   [ISL]  Definition
      
      ⊢ (∀x. ISL (INL x) ⇔ T) ∧ ∀y. ISL (INR y) ⇔ F
   
   [ISR]  Definition
      
      ⊢ (∀x. ISR (INR x) ⇔ T) ∧ ∀y. ISR (INL y) ⇔ F
   
   [IS_SUM_REP]  Definition
      
      ⊢ ∀f. IS_SUM_REP f ⇔
            ∃v1 v2. f = (λb x y. x = v1 ∧ b) ∨ f = (λb x y. y = v2 ∧ ¬b)
   
   [OUTL]  Definition
      
      ⊢ ∀x. OUTL (INL x) = x
   
   [OUTR]  Definition
      
      ⊢ ∀x. OUTR (INR x) = x
   
   [SUM_ALL_def]  Definition
      
      ⊢ (∀P Q x. SUM_ALL P Q (INL x) ⇔ P x) ∧
        ∀P Q y. SUM_ALL P Q (INR y) ⇔ Q y
   
   [SUM_FIN_def]  Definition
      
      ⊢ ∀A B.
          SUM_FIN A B = (λab. case ab of INL a => a ∈ A | INR b => b ∈ B)
   
   [SUM_MAP_def]  Definition
      
      ⊢ (∀f g a. SUM_MAP f g (INL a) = INL (f a)) ∧
        ∀f g b. SUM_MAP f g (INR b) = INR (g b)
   
   [SUM_REL_def]  Definition
      
      ⊢ (∀R1 R2 x ab. (R1 +++ R2) (INL x) ab ⇔ ISL ab ∧ R1 x (OUTL ab)) ∧
        ∀R1 R2 y ab. (R1 +++ R2) (INR y) ab ⇔ ISR ab ∧ R2 y (OUTR ab)
   
   [SUM_SET_def]  Definition
      
      ⊢ (∀f1 f2 a. sum$SUM_SET f1 f2 (INL a) = f1 a) ∧
        ∀f1 f2 b. sum$SUM_SET f1 f2 (INR b) = f2 b
   
   [sum_ISO_DEF]  Definition
      
      ⊢ (∀a. ABS_sum (REP_sum a) = a) ∧
        ∀r. IS_SUM_REP r ⇔ REP_sum (ABS_sum r) = r
   
   [sum_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION IS_SUM_REP rep
   
   [sum_case_def]  Definition
      
      ⊢ (∀x f f1. sum_CASE (INL x) f f1 = f x) ∧
        ∀y f f1. sum_CASE (INR y) f f1 = f1 y
   
   [EXISTS_SUM]  Theorem
      
      ⊢ ∀P. (∃s. P s) ⇔ (∃x. P (INL x)) ∨ ∃y. P (INR y)
   
   [FORALL_SUM]  Theorem
      
      ⊢ (∀s. P s) ⇔ (∀x. P (INL x)) ∧ ∀y. P (INR y)
   
   [INL]  Theorem
      
      ⊢ ∀x. ISL x ⇒ INL (OUTL x) = x
   
   [INL_11]  Theorem
      
      ⊢ INL x = INL y ⇔ x = y
   
   [INL_PRS]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀a. INL a = SUM_MAP abs1 abs2 (INL (rep1 a))
   
   [INL_RSP]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀a1 a2. R1 a1 a2 ⇒ (R1 +++ R2) (INL a1) (INL a2)
   
   [INR]  Theorem
      
      ⊢ ∀x. ISR x ⇒ INR (OUTR x) = x
   
   [INR_11]  Theorem
      
      ⊢ INR x = INR y ⇔ x = y
   
   [INR_INL_11]  Theorem
      
      ⊢ (∀y x. INL x = INL y ⇔ x = y) ∧ ∀y x. INR x = INR y ⇔ x = y
   
   [INR_PRS]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀b. INR b = SUM_MAP abs1 abs2 (INR (rep2 b))
   
   [INR_RSP]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀b1 b2. R2 b1 b2 ⇒ (R1 +++ R2) (INR b1) (INR b2)
   
   [INR_neq_INL]  Theorem
      
      ⊢ ∀v1 v2. INR v2 ≠ INL v1
   
   [IN_SUM_FIN_THM]  Theorem
      
      ⊢ (INL a ∈ SUM_FIN A B ⇔ a ∈ A) ∧ (INR b ∈ SUM_FIN A B ⇔ b ∈ B)
   
   [ISL_OR_ISR]  Theorem
      
      ⊢ ∀x. ISL x ∨ ISR x
   
   [ISL_PRS]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒ ∀a. ISL a ⇔ ISL (SUM_MAP rep1 rep2 a)
   
   [ISL_RSP]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀a1 a2. (R1 +++ R2) a1 a2 ⇒ (ISL a1 ⇔ ISL a2)
   
   [ISR_PRS]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒ ∀a. ISR a ⇔ ISR (SUM_MAP rep1 rep2 a)
   
   [ISR_RSP]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            ∀a1 a2. (R1 +++ R2) a1 a2 ⇒ (ISR a1 ⇔ ISR a2)
   
   [NOT_ISL_ISR]  Theorem
      
      ⊢ ∀x. ¬ISL x ⇔ ISR x
   
   [NOT_ISR_ISL]  Theorem
      
      ⊢ ∀x. ¬ISR x ⇔ ISL x
   
   [SUM_ALL_CONG]  Theorem
      
      ⊢ ∀s s' P P' Q Q'.
          s = s' ∧ (∀a. s' = INL a ⇒ (P a ⇔ P' a)) ∧
          (∀b. s' = INR b ⇒ (Q b ⇔ Q' b)) ⇒
          (SUM_ALL P Q s ⇔ SUM_ALL P' Q' s')
   
   [SUM_ALL_MONO]  Theorem
      
      ⊢ (∀x. P x ⇒ P' x) ∧ (∀y. Q y ⇒ Q' y) ⇒
        SUM_ALL P Q s ⇒
        SUM_ALL P' Q' s
   
   [SUM_ALL_SET]  Theorem
      
      ⊢ SUM_ALL P Q ab ⇔ (∀a. a ∈ setL ab ⇒ P a) ∧ ∀b. b ∈ setR ab ⇒ Q b
   
   [SUM_EQUIV]  Theorem
      
      ⊢ ∀R1 R2. EQUIV R1 ⇒ EQUIV R2 ⇒ EQUIV (R1 +++ R2)
   
   [SUM_MAP]  Theorem
      
      ⊢ ∀f g z.
          SUM_MAP f g z =
          if ISL z then INL (f (OUTL z)) else INR (g (OUTR z))
   
   [SUM_MAP_CASE]  Theorem
      
      ⊢ ∀f g z. SUM_MAP f g z = sum_CASE z (INL ∘ f) (INR ∘ g)
   
   [SUM_MAP_CONG]  Theorem
      
      ⊢ (∀a. a ∈ setL ab ⇒ f1 a = f2 a) ∧ (∀b. b ∈ setR ab ⇒ g1 b = g2 b) ⇒
        SUM_MAP f1 g1 ab = SUM_MAP f2 g2 ab
   
   [SUM_MAP_I]  Theorem
      
      ⊢ SUM_MAP I I = I
   
   [SUM_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.
                  SUM_MAP f g =
                  (SUM_MAP rep1 rep3 --> SUM_MAP abs2 abs4)
                    (SUM_MAP ((abs1 --> rep2) f) ((abs3 --> rep4) g))
   
   [SUM_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)) (SUM_MAP f1 g1)
                    (SUM_MAP f2 g2)
   
   [SUM_MAP_SET]  Theorem
      
      ⊢ (c ∈ setL (SUM_MAP f g ab) ⇔ ∃a. c = f a ∧ a ∈ setL ab) ∧
        (d ∈ setR (SUM_MAP f g ab) ⇔ ∃b. d = g b ∧ b ∈ setR ab)
   
   [SUM_MAP_o]  Theorem
      
      ⊢ SUM_MAP f g ∘ SUM_MAP h k = SUM_MAP (f ∘ h) (g ∘ k)
   
   [SUM_QUOTIENT]  Theorem
      
      ⊢ ∀R1 abs1 rep1.
          QUOTIENT R1 abs1 rep1 ⇒
          ∀R2 abs2 rep2.
            QUOTIENT R2 abs2 rep2 ⇒
            QUOTIENT (R1 +++ R2) (SUM_MAP abs1 abs2) (SUM_MAP rep1 rep2)
   
   [SUM_REL_EQ]  Theorem
      
      ⊢ $= +++ $= = $=
   
   [SUM_REL_REFL]  Theorem
      
      ⊢ (∀x. R1 x x) ∧ (∀a. R2 a a) ⇒ ∀xy. (R1 +++ R2) xy xy
   
   [SUM_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
   
   [SUM_REL_THM]  Theorem
      
      ⊢ ((R1 +++ R2) (INL x) (INL a) ⇔ R1 x a) ∧
        ((R1 +++ R2) (INL x) (INR b) ⇔ F) ∧
        ((R1 +++ R2) (INR y) (INL a) ⇔ F) ∧
        ((R1 +++ R2) (INR y) (INR b) ⇔ R2 y b)
   
   [SUM_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
   
   [SUM_SETLR_THM]  Theorem
      
      ⊢ (a1 ∈ setL (INL a2) ⇔ a1 = a2) ∧ (a ∈ setL (INR b) ⇔ F) ∧
        (b ∈ setR (INL a) ⇔ F) ∧ (b1 ∈ setR (INR b2) ⇔ b1 = b2)
   
   [cond_sum_expand]  Theorem
      
      ⊢ (∀x y z. (if P then INR x else INL y) = INR z ⇔ P ∧ z = x) ∧
        (∀x y z. (if P then INR x else INL y) = INL z ⇔ ¬P ∧ z = y) ∧
        (∀x y z. (if P then INL x else INR y) = INL z ⇔ P ∧ z = x) ∧
        ∀x y z. (if P then INL x else INR y) = INR z ⇔ ¬P ∧ z = y
   
   [datatype_sum]  Theorem
      
      ⊢ DATATYPE (sum INL INR)
   
   [sum_Axiom]  Theorem
      
      ⊢ ∀f g. ∃h. (∀x. h (INL x) = f x) ∧ ∀y. h (INR y) = g y
   
   [sum_CASES]  Theorem
      
      ⊢ ∀ss. (∃x. ss = INL x) ∨ ∃y. ss = INR y
   
   [sum_INDUCT]  Theorem
      
      ⊢ ∀P. (∀x. P (INL x)) ∧ (∀y. P (INR y)) ⇒ ∀s. P s
   
   [sum_axiom]  Theorem
      
      ⊢ ∀f g. ∃!h. h ∘ INL = f ∧ h ∘ INR = g
   
   [sum_case_cong]  Theorem
      
      ⊢ ∀M M' f f1.
          M = M' ∧ (∀x. M' = INL x ⇒ f x = f' x) ∧
          (∀y. M' = INR y ⇒ f1 y = f1' y) ⇒
          sum_CASE M f f1 = sum_CASE M' f' f1'
   
   [sum_distinct]  Theorem
      
      ⊢ ∀x y. INL x ≠ INR y
   
   [sum_distinct1]  Theorem
      
      ⊢ ∀x y. INR y ≠ INL x
   
   
*)
end

HOL 4, Trindemossen-1