Structure quotient_sumTheory

signature quotient_sumTheory =
sig
  type thm = Thm.thm
  
  (*  Theorems  *)
    val INL_PRS : thm
    val INL_RSP : thm
    val INR_PRS : thm
    val INR_RSP : thm
    val ISL_PRS : thm
    val ISL_RSP : thm
    val ISR_PRS : thm
    val ISR_RSP : thm
    val SUM_EQUIV : thm
    val SUM_MAP_PRS : thm
    val SUM_MAP_RSP : thm
    val SUM_QUOTIENT : thm
    val SUM_REL_EQ : thm
    val SUM_REL_def : thm
    val SUM_REL_ind : thm
  
  val quotient_sum_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [quotient] Parent theory of "quotient_sum"
   
   [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_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)
   
   [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)
   
   [SUM_EQUIV]  Theorem
      
      ⊢ ∀R1 R2. EQUIV R1 ⇒ EQUIV R2 ⇒ EQUIV (R1 +++ R2)
   
   [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_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_def]  Theorem
      
      ⊢ ((R1 +++ R2) (INL a1) (INL a2) ⇔ R1 a1 a2) ∧
        ((R1 +++ R2) (INR b1) (INR b2) ⇔ R2 b1 b2) ∧
        ((R1 +++ R2) (INL a1) (INR b2) ⇔ F) ∧
        ((R1 +++ R2) (INR b1) (INL a2) ⇔ F)
   
   [SUM_REL_ind]  Theorem
      
      ⊢ ∀P.
            (∀R1 R2 a1 a2. P R1 R2 (INL a1) (INL a2)) ∧
            (∀R1 R2 b1 b2. P R1 R2 (INR b1) (INR b2)) ∧
            (∀R1 R2 a1 b2. P R1 R2 (INL a1) (INR b2)) ∧
            (∀R1 R2 b1 a2. P R1 R2 (INR b1) (INL a2)) ⇒
            ∀v v1 v2 v3. P v v1 v2 v3
   
   
*)
end

HOL 4, Kananaskis-13