Structure ind_typeTheory

signature ind_typeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BOTTOM : thm
    val CONSTR : thm
    val FCONS : thm
    val FNIL : thm
    val INJA : thm
    val INJF : thm
    val INJN : thm
    val INJP : thm
    val ISO : thm
    val NUMPAIR : thm
    val NUMPAIR_DEST : thm
    val NUMSUM : thm
    val NUMSUM_DEST : thm
    val ZBOT : thm
    val ZCONSTR : thm
    val ZRECSPACE_def : thm
    val recspace_TY_DEF : thm
    val recspace_repfns : thm
  
  (*  Theorems  *)
    val CONSTR_BOT : thm
    val CONSTR_IND : thm
    val CONSTR_INJ : thm
    val CONSTR_REC : thm
    val DEST_REC_INJ : thm
    val FCONS_DEST : thm
    val INJA_INJ : thm
    val INJF_INJ : thm
    val INJN_INJ : thm
    val INJP_INJ : thm
    val INJ_INVERSE2 : thm
    val ISO_FUN : thm
    val ISO_REFL : thm
    val ISO_USAGE : thm
    val MK_REC_INJ : thm
    val NUMPAIR_INJ : thm
    val NUMPAIR_INJ_LEMMA : thm
    val NUMSUM_INJ : thm
    val ZCONSTR_ZBOT : thm
    val ZRECSPACE_cases : thm
    val ZRECSPACE_ind : thm
    val ZRECSPACE_rules : thm
    val ZRECSPACE_strongind : thm
  
  val ind_type_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [numeral] Parent theory of "ind_type"
   
   [while] Parent theory of "ind_type"
   
   [BOTTOM]  Definition
      
      ⊢ ind_type$BOTTOM = mk_rec ind_type$ZBOT
   
   [CONSTR]  Definition
      
      ⊢ ∀c i r.
            ind_type$CONSTR c i r =
            mk_rec (ind_type$ZCONSTR c i (λn. dest_rec (r n)))
   
   [FCONS]  Definition
      
      ⊢ (∀a f. ind_type$FCONS a f 0 = a) ∧
        ∀a f n. ind_type$FCONS a f (SUC n) = f n
   
   [FNIL]  Definition
      
      ⊢ ∀n. ind_type$FNIL n = ARB
   
   [INJA]  Definition
      
      ⊢ ∀a. ind_type$INJA a = (λn b. b = a)
   
   [INJF]  Definition
      
      ⊢ ∀f. ind_type$INJF f = (λn. f (NUMFST n) (NUMSND n))
   
   [INJN]  Definition
      
      ⊢ ∀m. ind_type$INJN m = (λn a. n = m)
   
   [INJP]  Definition
      
      ⊢ ∀f1 f2.
            ind_type$INJP f1 f2 =
            (λn a.
                 if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a)
   
   [ISO]  Definition
      
      ⊢ ∀f g. ind_type$ISO f g ⇔ (∀x. f (g x) = x) ∧ ∀y. g (f y) = y
   
   [NUMPAIR]  Definition
      
      ⊢ ∀x y. ind_type$NUMPAIR x y = 2 ** x * (2 * y + 1)
   
   [NUMPAIR_DEST]  Definition
      
      ⊢ ∀x y.
            NUMFST (ind_type$NUMPAIR x y) = x ∧
            NUMSND (ind_type$NUMPAIR x y) = y
   
   [NUMSUM]  Definition
      
      ⊢ ∀b x. ind_type$NUMSUM b x = if b then SUC (2 * x) else 2 * x
   
   [NUMSUM_DEST]  Definition
      
      ⊢ ∀x y.
            (NUMLEFT (ind_type$NUMSUM x y) ⇔ x) ∧
            NUMRIGHT (ind_type$NUMSUM x y) = y
   
   [ZBOT]  Definition
      
      ⊢ ind_type$ZBOT = ind_type$INJP (ind_type$INJN 0) (@z. T)
   
   [ZCONSTR]  Definition
      
      ⊢ ∀c i r.
            ind_type$ZCONSTR c i r =
            ind_type$INJP (ind_type$INJN (SUC c))
              (ind_type$INJP (ind_type$INJA i) (ind_type$INJF r))
   
   [ZRECSPACE_def]  Definition
      
      ⊢ ZRECSPACE =
        (λa0.
             ∀ZRECSPACE'.
                 (∀a0.
                      a0 = ind_type$ZBOT ∨
                      (∃c i r.
                           a0 = ind_type$ZCONSTR c i r ∧
                           ∀n. ZRECSPACE' (r n)) ⇒
                      ZRECSPACE' a0) ⇒
                 ZRECSPACE' a0)
   
   [recspace_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION ZRECSPACE rep
   
   [recspace_repfns]  Definition
      
      ⊢ (∀a. mk_rec (dest_rec a) = a) ∧
        ∀r. ZRECSPACE r ⇔ dest_rec (mk_rec r) = r
   
   [CONSTR_BOT]  Theorem
      
      ⊢ ∀c i r. ind_type$CONSTR c i r ≠ ind_type$BOTTOM
   
   [CONSTR_IND]  Theorem
      
      ⊢ ∀P.
            P ind_type$BOTTOM ∧
            (∀c i r. (∀n. P (r n)) ⇒ P (ind_type$CONSTR c i r)) ⇒
            ∀x. P x
   
   [CONSTR_INJ]  Theorem
      
      ⊢ ∀c1 i1 r1 c2 i2 r2.
            ind_type$CONSTR c1 i1 r1 = ind_type$CONSTR c2 i2 r2 ⇔
            c1 = c2 ∧ i1 = i2 ∧ r1 = r2
   
   [CONSTR_REC]  Theorem
      
      ⊢ ∀Fn. ∃f. ∀c i r. f (ind_type$CONSTR c i r) = Fn c i r (λn. f (r n))
   
   [DEST_REC_INJ]  Theorem
      
      ⊢ ∀x y. dest_rec x = dest_rec y ⇔ x = y
   
   [FCONS_DEST]  Theorem
      
      ⊢ ind_type$FCONS a f n = if n = 0 then a else f (n − 1)
   
   [INJA_INJ]  Theorem
      
      ⊢ ∀a1 a2. ind_type$INJA a1 = ind_type$INJA a2 ⇔ a1 = a2
   
   [INJF_INJ]  Theorem
      
      ⊢ ∀f1 f2. ind_type$INJF f1 = ind_type$INJF f2 ⇔ f1 = f2
   
   [INJN_INJ]  Theorem
      
      ⊢ ∀n1 n2. ind_type$INJN n1 = ind_type$INJN n2 ⇔ n1 = n2
   
   [INJP_INJ]  Theorem
      
      ⊢ ∀f1 f1' f2 f2'.
            ind_type$INJP f1 f2 = ind_type$INJP f1' f2' ⇔
            f1 = f1' ∧ f2 = f2'
   
   [INJ_INVERSE2]  Theorem
      
      ⊢ ∀P.
            (∀x1 y1 x2 y2. P x1 y1 = P x2 y2 ⇔ x1 = x2 ∧ y1 = y2) ⇒
            ∃X Y. ∀x y. X (P x y) = x ∧ Y (P x y) = y
   
   [ISO_FUN]  Theorem
      
      ⊢ ind_type$ISO f f' ∧ ind_type$ISO g g' ⇒
        ind_type$ISO (λh a'. g (h (f' a'))) (λh a. g' (h (f a)))
   
   [ISO_REFL]  Theorem
      
      ⊢ ind_type$ISO (λx. x) (λx. x)
   
   [ISO_USAGE]  Theorem
      
      ⊢ ind_type$ISO f g ⇒
        (∀P. (∀x. P x) ⇔ ∀x. P (g x)) ∧ (∀P. (∃x. P x) ⇔ ∃x. P (g x)) ∧
        ∀a b. a = g b ⇔ f a = b
   
   [MK_REC_INJ]  Theorem
      
      ⊢ ∀x y. mk_rec x = mk_rec y ⇒ ZRECSPACE x ∧ ZRECSPACE y ⇒ x = y
   
   [NUMPAIR_INJ]  Theorem
      
      ⊢ ∀x1 y1 x2 y2.
            ind_type$NUMPAIR x1 y1 = ind_type$NUMPAIR x2 y2 ⇔
            x1 = x2 ∧ y1 = y2
   
   [NUMPAIR_INJ_LEMMA]  Theorem
      
      ⊢ ∀x1 y1 x2 y2.
            ind_type$NUMPAIR x1 y1 = ind_type$NUMPAIR x2 y2 ⇒ x1 = x2
   
   [NUMSUM_INJ]  Theorem
      
      ⊢ ∀b1 x1 b2 x2.
            ind_type$NUMSUM b1 x1 = ind_type$NUMSUM b2 x2 ⇔
            (b1 ⇔ b2) ∧ x1 = x2
   
   [ZCONSTR_ZBOT]  Theorem
      
      ⊢ ∀c i r. ind_type$ZCONSTR c i r ≠ ind_type$ZBOT
   
   [ZRECSPACE_cases]  Theorem
      
      ⊢ ∀a0.
            ZRECSPACE a0 ⇔
            a0 = ind_type$ZBOT ∨
            ∃c i r. a0 = ind_type$ZCONSTR c i r ∧ ∀n. ZRECSPACE (r n)
   
   [ZRECSPACE_ind]  Theorem
      
      ⊢ ∀ZRECSPACE'.
            ZRECSPACE' ind_type$ZBOT ∧
            (∀c i r.
                 (∀n. ZRECSPACE' (r n)) ⇒
                 ZRECSPACE' (ind_type$ZCONSTR c i r)) ⇒
            ∀a0. ZRECSPACE a0 ⇒ ZRECSPACE' a0
   
   [ZRECSPACE_rules]  Theorem
      
      ⊢ ZRECSPACE ind_type$ZBOT ∧
        ∀c i r. (∀n. ZRECSPACE (r n)) ⇒ ZRECSPACE (ind_type$ZCONSTR c i r)
   
   [ZRECSPACE_strongind]  Theorem
      
      ⊢ ∀ZRECSPACE'.
            ZRECSPACE' ind_type$ZBOT ∧
            (∀c i r.
                 (∀n. ZRECSPACE (r n) ∧ ZRECSPACE' (r n)) ⇒
                 ZRECSPACE' (ind_type$ZCONSTR c i r)) ⇒
            ∀a0. ZRECSPACE a0 ⇒ ZRECSPACE' a0
   
   
*)
end

HOL 4, Kananaskis-13