Theory: inftree

Type operators

inftree : (α, β, γ) inftree

Constants

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

iLf_def iNd_def inftree_TY_DEF inftree_bijections inftree_case_def inftree_rec_def

Theorems

iNd_is_tree inftree_11 inftree_Axiom inftree_distinct inftree_ind inftree_nchotomy is_tree_cases is_tree_ind is_tree_rules is_tree_strongind relrec_cases relrec_ind relrec_rules relrec_strongind

Definitions

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))

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

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

inftree_rec_def

⊢ ∀lf nd t. inftree_rec lf nd t = @r. relrec lf nd t r

Theorems

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_Axiom

⊢ ∀lf nd. ∃f. (∀a. f (iLf a) = lf a) ∧ ∀b d. f (iNd b d) = nd b d (f ∘ d)

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

inftree_nchotomy

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

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)

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_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_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

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)

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_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_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

Theory inftree

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems