Theory "inftree"

Parents list

Signature

Type	Arity
inftree	3
Constant	Type
from_inftree	:(α, β, δ) inftree -> δ list -> α + β
iLf	:α -> (α, β, γ) inftree
iNd	:β -> (γ -> (α, β, γ) inftree) -> (α, β, γ) inftree
inftree_CASE	:(α, β, γ) inftree -> (α -> δ) -> (β -> (γ -> (α, β, γ) inftree) -> δ) -> δ
inftree_rec	:(β -> α) -> (γ -> (δ -> α) -> α) -> (β, γ, δ) inftree -> α
is_tree	:(δ list -> α + β) -> bool
relrec	:(α -> β) -> (γ -> (δ -> β) -> β) -> (α, γ, δ) inftree -> β -> bool
to_inftree	:(δ list -> α + β) -> (α, β, δ) inftree

Definitions

is_tree_def

|- is_tree =
   (λa0.
      ∀is_tree'.
        (∀a0.
           (∃a. a0 = (λp. INL a)) ∨
           (∃f b.
              (a0 = (λp. if p = [] then INR b else f (HD p) (TL p))) ∧
              ∀d. is_tree' (f d)) ⇒
           is_tree' a0) ⇒
        is_tree' a0)

inftree_TY_DEF

|- ∃rep. TYPE_DEFINITION is_tree rep

inftree_bijections

|- (∀a. to_inftree (from_inftree a) = a) ∧
   ∀r. is_tree r ⇔ (from_inftree (to_inftree r) = r)

iLf_def

|- ∀a. iLf a = to_inftree (λp. INL a)

iNd_def

|- ∀b f.
     iNd b f =
     to_inftree (λp. if p = [] then INR b else from_inftree (f (HD p)) (TL p))

relrec_def

|- relrec =
   (λa0 a1 a2 a3.
      ∀relrec'.
        (∀a0 a1 a2 a3.
           (∃a. (a2 = iLf a) ∧ (a3 = a0 a)) ∨
           (∃b df g.
              (a2 = iNd b df) ∧ (a3 = a1 b g) ∧
              ∀d. relrec' a0 a1 (df d) (g d)) ⇒
           relrec' a0 a1 a2 a3) ⇒
        relrec' a0 a1 a2 a3)

inftree_rec_def

|- ∀lf nd t. inftree_rec lf nd t = @r. relrec lf nd t r

inftree_case_def

|- (∀a f f1. inftree_CASE (iLf a) f f1 = f a) ∧
   ∀b d f f1. inftree_CASE (iNd b d) f f1 = f1 b d

Theorems

is_tree_rules

|- (∀a. is_tree (λp. INL a)) ∧
   ∀f b.
     (∀d. is_tree (f d)) ⇒
     is_tree (λp. if p = [] then INR b else f (HD p) (TL p))

is_tree_ind

|- ∀is_tree'.
     (∀a. is_tree' (λp. INL a)) ∧
     (∀f b.
        (∀d. is_tree' (f d)) ⇒
        is_tree' (λp. if p = [] then INR b else f (HD p) (TL p))) ⇒
     ∀a0. is_tree a0 ⇒ is_tree' a0

is_tree_strongind

|- ∀is_tree'.
     (∀a. is_tree' (λp. INL a)) ∧
     (∀f b.
        (∀d. is_tree (f d) ∧ is_tree' (f d)) ⇒
        is_tree' (λp. if p = [] then INR b else f (HD p) (TL p))) ⇒
     ∀a0. is_tree a0 ⇒ is_tree' a0

is_tree_cases

|- ∀a0.
     is_tree a0 ⇔
     (∃a. a0 = (λp. INL a)) ∨
     ∃f b.
       (a0 = (λp. if p = [] then INR b else f (HD p) (TL p))) ∧
       ∀d. is_tree (f d)

iNd_is_tree

|- ∀b f.
     is_tree (λp. if p = [] then INR b else from_inftree (f (HD p)) (TL p))

inftree_11

|- ((iLf a1 = iLf a2) ⇔ (a1 = a2)) ∧
   ((iNd b1 f1 = iNd b2 f2) ⇔ (b1 = b2) ∧ (f1 = f2))

inftree_distinct

|- iLf a ≠ iNd b f

inftree_ind

|- ∀P. (∀a. P (iLf a)) ∧ (∀b f. (∀d. P (f d)) ⇒ P (iNd b f)) ⇒ ∀t. P t

relrec_rules

|- (∀lf nd a. relrec lf nd (iLf a) (lf a)) ∧
   ∀lf nd b df g.
     (∀d. relrec lf nd (df d) (g d)) ⇒ relrec lf nd (iNd b df) (nd b g)

relrec_ind

|- ∀relrec'.
     (∀lf nd a. relrec' lf nd (iLf a) (lf a)) ∧
     (∀lf nd b df g.
        (∀d. relrec' lf nd (df d) (g d)) ⇒
        relrec' lf nd (iNd b df) (nd b g)) ⇒
     ∀a0 a1 a2 a3. relrec a0 a1 a2 a3 ⇒ relrec' a0 a1 a2 a3

relrec_strongind

|- ∀relrec'.
     (∀lf nd a. relrec' lf nd (iLf a) (lf a)) ∧
     (∀lf nd b df g.
        (∀d. relrec lf nd (df d) (g d) ∧ relrec' lf nd (df d) (g d)) ⇒
        relrec' lf nd (iNd b df) (nd b g)) ⇒
     ∀a0 a1 a2 a3. relrec a0 a1 a2 a3 ⇒ relrec' a0 a1 a2 a3

relrec_cases

|- ∀a0 a1 a2 a3.
     relrec a0 a1 a2 a3 ⇔
     (∃a. (a2 = iLf a) ∧ (a3 = a0 a)) ∨
     ∃b df g. (a2 = iNd b df) ∧ (a3 = a1 b g) ∧ ∀d. relrec a0 a1 (df d) (g d)

inftree_Axiom

|- ∀lf nd. ∃f. (∀a. f (iLf a) = lf a) ∧ ∀b d. f (iNd b d) = nd b d (f o d)

inftree_nchotomy

|- ∀t. (∃a. t = iLf a) ∨ ∃b d. t = iNd b d