Theory "fcp"

Signature

Type	Arity
bit0	1
bit1	1
cart	2
finite_image	1
Constant	Type
:+	:num -> α -> α[β] -> α[β]
BIT0A	:α -> α bit0
BIT0B	:α -> α bit0
BIT1A	:α -> α bit1
BIT1B	:α -> α bit1
BIT1C	:α bit1
FCP	:(num -> α) -> α[β]
FCP_CONCAT	:α[β] -> α[γ] -> α[β + γ]
FCP_CONS	:α -> α[β] -> α[γ]
FCP_EVERY	:(β -> bool) -> β[α] -> bool
FCP_EXISTS	:(β -> bool) -> β[α] -> bool
FCP_FOLD	:(β -> α -> β) -> β -> α[γ] -> β
FCP_FST	:α[β + γ] -> α[β]
FCP_HD	:α[β] -> α
FCP_MAP	:(α -> β) -> α[γ] -> β[γ]
FCP_SND	:α[β + γ] -> α[γ]
FCP_TL	:α[γ] -> α[β]
FCP_ZIP	:α[β] -> γ[β] -> (α # γ)[β]
L2V	:α list -> α[β]
V2L	:α[β] -> α list
bit0_CASE	:α bit0 -> (α -> β) -> (α -> β) -> β
bit0_size	:(α -> num) -> α bit0 -> num
bit1_CASE	:α bit1 -> (α -> β) -> (α -> β) -> β -> β
bit1_size	:(α -> num) -> α bit1 -> num
dest_cart	:α[β] -> β finite_image -> α
dest_finite_image	:α finite_image -> α
dimindex	:α itself -> num
fcp_CASE	:α[β] -> ((β finite_image -> α) -> γ) -> γ
fcp_index	:α[β] -> num -> α
finite_index	:num -> α
mk_cart	:(β finite_image -> α) -> α[β]
mk_finite_image	:α -> α finite_image

Definitions

FCP

⊢ $FCP = (λg. @f. ∀i. i < dimindex (:β) ⇒ (f ' i = g i))

FCP_CONCAT_def

⊢ ∀a b.
    FCP_CONCAT a b =
    FCP i. if i < dimindex (:γ) then b ' i else a ' (i − dimindex (:γ))

FCP_CONS_def

⊢ ∀h v. FCP_CONS h v = (0 :+ h) (FCP i. v ' (PRE i))

FCP_EVERY_def

⊢ ∀P v. FCP_EVERY P v ⇔ ∀i. dimindex (:α) ≤ i ∨ P (v ' i)

FCP_EXISTS_def

⊢ ∀P v. FCP_EXISTS P v ⇔ ∃i. i < dimindex (:α) ∧ P (v ' i)

FCP_FOLD_def

⊢ ∀f i v. FCP_FOLD f i v = FOLDL f i (V2L v)

FCP_FST_def

⊢ ∀a. FCP_FST a = FCP i. a ' (i + dimindex (:γ))

FCP_HD_def

⊢ ∀v. FCP_HD v = v ' 0

FCP_MAP_def

⊢ ∀f v. FCP_MAP f v = FCP i. f (v ' i)

FCP_SND_def

⊢ ∀b. FCP_SND b = FCP i. b ' i

FCP_TL_def

⊢ ∀v. FCP_TL v = FCP i. v ' (SUC i)

FCP_UPDATE_def

⊢ ∀a b. a :+ b = (λm. FCP c. if a = c then b else m ' c)

FCP_ZIP_def

⊢ ∀a b. FCP_ZIP a b = FCP i. (a ' i,b ' i)

L2V_def

⊢ ∀L. L2V L = FCP i. EL i L

V2L_def

⊢ ∀v. V2L v = GENLIST ($' v) (dimindex (:β))

bit0_TY_DEF

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0.
           ∀ $var$('bit0').
             (∀a0.
                (∃a. a0 = (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM)) a) ∨
                (∃a. a0 =
                     (λa. ind_type$CONSTR (SUC 0) a (λn. ind_type$BOTTOM)) a) ⇒
                $var$('bit0') a0) ⇒
             $var$('bit0') a0) rep

bit0_case_def

⊢ (∀a f f1. bit0_CASE (BIT0A a) f f1 = f a) ∧
  ∀a f f1. bit0_CASE (BIT0B a) f f1 = f1 a

bit0_size_def

⊢ (∀f a. bit0_size f (BIT0A a) = 1 + f a) ∧
  ∀f a. bit0_size f (BIT0B a) = 1 + f a

bit1_TY_DEF

⊢ ∃rep.
    TYPE_DEFINITION
      (λa0.
           ∀ $var$('bit1').
             (∀a0.
                (∃a. a0 = (λa. ind_type$CONSTR 0 a (λn. ind_type$BOTTOM)) a) ∨
                (∃a. a0 =
                     (λa. ind_type$CONSTR (SUC 0) a (λn. ind_type$BOTTOM)) a) ∨
                (a0 = ind_type$CONSTR (SUC (SUC 0)) ARB (λn. ind_type$BOTTOM)) ⇒
                $var$('bit1') a0) ⇒
             $var$('bit1') a0) rep

bit1_case_def

⊢ (∀a f f1 v. bit1_CASE (BIT1A a) f f1 v = f a) ∧
  (∀a f f1 v. bit1_CASE (BIT1B a) f f1 v = f1 a) ∧
  ∀f f1 v. bit1_CASE BIT1C f f1 v = v

bit1_size_def

⊢ (∀f a. bit1_size f (BIT1A a) = 1 + f a) ∧
  (∀f a. bit1_size f (BIT1B a) = 1 + f a) ∧ ∀f. bit1_size f BIT1C = 0

cart_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λf. T) rep

cart_tybij

⊢ (∀a. mk_cart (dest_cart a) = a) ∧
  ∀r. (λf. T) r ⇔ (dest_cart (mk_cart r) = r)

dimindex_def

⊢ dimindex (:α) = if FINITE 𝕌(:α) then CARD 𝕌(:α) else 1

fcp_case_def

⊢ ∀h f. fcp_CASE (mk_cart h) f = f h

fcp_index

⊢ ∀x i. x ' i = dest_cart x (finite_index i)

finite_image_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λx. (x = ARB) ∨ FINITE 𝕌(:α)) rep

finite_image_tybij

⊢ (∀a. mk_finite_image (dest_finite_image a) = a) ∧
  ∀r. (λx. (x = ARB) ∨ FINITE 𝕌(:α)) r ⇔
      (dest_finite_image (mk_finite_image r) = r)

finite_index_def

⊢ finite_index = @f. ∀x. ∃!n. n < dimindex (:α) ∧ (f n = x)

Theorems

APPLY_FCP_UPDATE_ID

⊢ ∀m a. (a :+ m ' a) m = m

CART_EQ

⊢ ∀x y. (x = y) ⇔ ∀i. i < dimindex (:β) ⇒ (x ' i = y ' i)

DIMINDEX_GE_1

⊢ 1 ≤ dimindex (:α)

EL_V2L

⊢ ∀i v. i < dimindex (:β) ⇒ (EL i (V2L v) = v ' i)

FCP_APPLY_UPDATE_THM

⊢ ∀m a w b.
    (a :+ w) m ' b =
    if b < dimindex (:β) then if a = b then w else m ' b
    else FAIL $' $var$(index out of range) ((a :+ w) m) b

FCP_BETA

⊢ ∀i. i < dimindex (:β) ⇒ ($FCP g ' i = g i)

FCP_CONCAT_11

⊢ ∀a b c d.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ∧ (FCP_CONCAT a b = FCP_CONCAT c d) ⇒
    (a = c) ∧ (b = d)

FCP_CONCAT_THM

⊢ ∀a b.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
    (FCP_FST (FCP_CONCAT a b) = a) ∧ (FCP_SND (FCP_CONCAT a b) = b)

FCP_CONS

⊢ ∀a v. FCP_CONS a v = L2V (a::V2L v)

FCP_ETA

⊢ ∀g. (FCP i. g ' i) = g

FCP_EVERY

⊢ ∀P v. FCP_EVERY P v ⇔ EVERY P (V2L v)

FCP_EXISTS

⊢ ∀P v. FCP_EXISTS P v ⇔ EXISTS P (V2L v)

FCP_HD

⊢ ∀v. FCP_HD v = HD (V2L v)

FCP_MAP

⊢ ∀f v. FCP_MAP f v = L2V (MAP f (V2L v))

FCP_TL

⊢ ∀v. 1 < dimindex (:β) ∧ (dimindex (:γ) = dimindex (:β) − 1) ⇒
      (FCP_TL v = L2V (TL (V2L v)))

FCP_UNIQUE

⊢ ∀f g. (∀i. i < dimindex (:β) ⇒ (f ' i = g i)) ⇔ ($FCP g = f)

FCP_UPDATE_COMMUTES

⊢ ∀m a b c d. a ≠ b ⇒ ((a :+ c) ((b :+ d) m) = (b :+ d) ((a :+ c) m))

FCP_UPDATE_EQ

⊢ ∀m a b c. (a :+ c) ((a :+ b) m) = (a :+ c) m

FCP_UPDATE_IMP_ID

⊢ ∀m a v. (m ' a = v) ⇒ ((a :+ v) m = m)

LENGTH_V2L

⊢ ∀v. LENGTH (V2L v) = dimindex (:β)

NOT_FINITE_IMP_dimindex_1

⊢ INFINITE 𝕌(:α) ⇒ (dimindex (:α) = 1)

NULL_V2L

⊢ ∀v. ¬NULL (V2L v)

READ_L2V

⊢ ∀i a. i < dimindex (:β) ⇒ (L2V a ' i = EL i a)

READ_TL

⊢ ∀i a. i < dimindex (:β) ⇒ (FCP_TL a ' i = a ' (SUC i))

V2L_L2V

⊢ ∀x. (dimindex (:β) = LENGTH x) ⇒ (V2L (L2V x) = x)

bit0_11

⊢ (∀a a'. (BIT0A a = BIT0A a') ⇔ (a = a')) ∧
  ∀a a'. (BIT0B a = BIT0B a') ⇔ (a = a')

bit0_Axiom

⊢ ∀f0 f1. ∃fn. (∀a. fn (BIT0A a) = f0 a) ∧ ∀a. fn (BIT0B a) = f1 a

bit0_case_cong

⊢ ∀M M' f f1.
    (M = M') ∧ (∀a. (M' = BIT0A a) ⇒ (f a = f' a)) ∧
    (∀a. (M' = BIT0B a) ⇒ (f1 a = f1' a)) ⇒
    (bit0_CASE M f f1 = bit0_CASE M' f' f1')

bit0_case_eq

⊢ (bit0_CASE x f f1 = v) ⇔
  (∃a. (x = BIT0A a) ∧ (f a = v)) ∨ ∃a. (x = BIT0B a) ∧ (f1 a = v)

bit0_distinct

⊢ ∀a' a. BIT0A a ≠ BIT0B a'

bit0_induction

⊢ ∀P. (∀a. P (BIT0A a)) ∧ (∀a. P (BIT0B a)) ⇒ ∀b. P b

bit0_nchotomy

⊢ ∀bb. (∃a. bb = BIT0A a) ∨ ∃a. bb = BIT0B a

bit1_11

⊢ (∀a a'. (BIT1A a = BIT1A a') ⇔ (a = a')) ∧
  ∀a a'. (BIT1B a = BIT1B a') ⇔ (a = a')

bit1_Axiom

⊢ ∀f0 f1 f2. ∃fn.
    (∀a. fn (BIT1A a) = f0 a) ∧ (∀a. fn (BIT1B a) = f1 a) ∧ (fn BIT1C = f2)

bit1_case_cong

⊢ ∀M M' f f1 v.
    (M = M') ∧ (∀a. (M' = BIT1A a) ⇒ (f a = f' a)) ∧
    (∀a. (M' = BIT1B a) ⇒ (f1 a = f1' a)) ∧ ((M' = BIT1C) ⇒ (v = v')) ⇒
    (bit1_CASE M f f1 v = bit1_CASE M' f' f1' v')

bit1_case_eq

⊢ (bit1_CASE x f f1 v = v') ⇔
  (∃a. (x = BIT1A a) ∧ (f a = v')) ∨ (∃a. (x = BIT1B a) ∧ (f1 a = v')) ∨
  (x = BIT1C) ∧ (v = v')

bit1_distinct

⊢ (∀a' a. BIT1A a ≠ BIT1B a') ∧ (∀a. BIT1A a ≠ BIT1C) ∧ ∀a. BIT1B a ≠ BIT1C

bit1_induction

⊢ ∀P. (∀a. P (BIT1A a)) ∧ (∀a. P (BIT1B a)) ∧ P BIT1C ⇒ ∀b. P b

bit1_nchotomy

⊢ ∀bb. (∃a. bb = BIT1A a) ∨ (∃a. bb = BIT1B a) ∨ (bb = BIT1C)

card_dimindex

⊢ FINITE 𝕌(:α) ⇒ (CARD 𝕌(:α) = dimindex (:α))

datatype_bit0

⊢ DATATYPE (bit0 BIT0A BIT0B)

datatype_bit1

⊢ DATATYPE (bit1 BIT1A BIT1B BIT1C)

fcp_Axiom

⊢ ∀f. ∃g. ∀h. g (mk_cart h) = f h

fcp_ind

⊢ ∀P. (∀f. P (mk_cart f)) ⇒ ∀a. P a

fcp_subst_comp

⊢ ∀a b f. (x :+ y) ($FCP f) = FCP c. if x = c then y else f c

finite_bit0

⊢ FINITE 𝕌(:α bit0) ⇔ FINITE 𝕌(:α)

finite_bit1

⊢ FINITE 𝕌(:α bit1) ⇔ FINITE 𝕌(:α)

finite_one

⊢ FINITE 𝕌(:unit)

finite_sum

⊢ FINITE 𝕌(:α + β) ⇔ FINITE 𝕌(:α) ∧ FINITE 𝕌(:β)

index_bit0

⊢ dimindex (:α bit0) = if FINITE 𝕌(:α) then 2 * dimindex (:α) else 1

index_bit1

⊢ dimindex (:α bit1) = if FINITE 𝕌(:α) then 2 * dimindex (:α) + 1 else 1

index_comp

⊢ ∀f n.
    $FCP f ' n =
    if n < dimindex (:β) then f n
    else FAIL $' $var$(FCP out of bounds) ($FCP f) n

index_one

⊢ dimindex (:unit) = 1

index_sum

⊢ dimindex (:α + β) =
  if FINITE 𝕌(:α) ∧ FINITE 𝕌(:β) then dimindex (:α) + dimindex (:β) else 1