Theory "quote"

Signature

Definitions

index_TY_DEF

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

index_case_def

⊢ (∀a f f1 v. index_CASE (Left_idx a) f f1 v = f a) ∧
  (∀a f f1 v. index_CASE (Right_idx a) f f1 v = f1 a) ∧
  ∀f f1 v. index_CASE End_idx f f1 v = v

index_size_def

⊢ (∀a. index_size (Left_idx a) = 1 + index_size a) ∧
  (∀a. index_size (Right_idx a) = 1 + index_size a) ∧ index_size End_idx = 0

index_lt_def

⊢ ∀i1 i2. index_lt i1 i2 ⇔ index_compare i1 i2 = Less

varmap_TY_DEF

⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀'varmap' .
                 (∀a0'.
                      a0' = ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM) ∨
                      (∃a0 a1 a2.
                           a0' =
                           (λa0 a1 a2.
                                ind_type$CONSTR (SUC 0) a0
                                  (ind_type$FCONS a1
                                     (ind_type$FCONS a2 (λn. ind_type$BOTTOM))))
                             a0 a1 a2 ∧ 'varmap' a1 ∧ 'varmap' a2) ⇒
                      'varmap' a0') ⇒
                 'varmap' a0') rep

varmap_case_def

⊢ (∀v f. varmap_CASE Empty_vm v f = v) ∧
  ∀a0 a1 a2 v f. varmap_CASE (Node_vm a0 a1 a2) v f = f a0 a1 a2

varmap_size_def

⊢ (∀f. varmap_size f Empty_vm = 0) ∧
  ∀f a0 a1 a2.
      varmap_size f (Node_vm a0 a1 a2) =
      1 + (f a0 + (varmap_size f a1 + varmap_size f a2))

Theorems

datatype_index

⊢ DATATYPE (index Left_idx Right_idx End_idx)

index_11

⊢ (∀a a'. Left_idx a = Left_idx a' ⇔ a = a') ∧
  ∀a a'. Right_idx a = Right_idx a' ⇔ a = a'

index_distinct

⊢ (∀a' a. Left_idx a ≠ Right_idx a') ∧ (∀a. Left_idx a ≠ End_idx) ∧
  ∀a. Right_idx a ≠ End_idx

index_nchotomy

⊢ ∀ii. (∃i. ii = Left_idx i) ∨ (∃i. ii = Right_idx i) ∨ ii = End_idx

index_Axiom

⊢ ∀f0 f1 f2.
      ∃fn.
          (∀a. fn (Left_idx a) = f0 a (fn a)) ∧
          (∀a. fn (Right_idx a) = f1 a (fn a)) ∧ fn End_idx = f2

index_induction

⊢ ∀P.
      (∀i. P i ⇒ P (Left_idx i)) ∧ (∀i. P i ⇒ P (Right_idx i)) ∧ P End_idx ⇒
      ∀i. P i

index_case_cong

⊢ ∀M M' f f1 v.
      M = M' ∧ (∀a. M' = Left_idx a ⇒ f a = f' a) ∧
      (∀a. M' = Right_idx a ⇒ f1 a = f1' a) ∧ (M' = End_idx ⇒ v = v') ⇒
      index_CASE M f f1 v = index_CASE M' f' f1' v'

index_case_eq

⊢ index_CASE x f f1 v = v' ⇔
  (∃i. x = Left_idx i ∧ f i = v') ∨ (∃i. x = Right_idx i ∧ f1 i = v') ∨
  x = End_idx ∧ v = v'

index_compare_ind

⊢ ∀P.
      P End_idx End_idx ∧ (∀v10. P End_idx (Left_idx v10)) ∧
      (∀v11. P End_idx (Right_idx v11)) ∧ (∀v2. P (Left_idx v2) End_idx) ∧
      (∀v3. P (Right_idx v3) End_idx) ∧
      (∀n' m'. P n' m' ⇒ P (Left_idx n') (Left_idx m')) ∧
      (∀n' m'. P (Left_idx n') (Right_idx m')) ∧
      (∀n' m'. P n' m' ⇒ P (Right_idx n') (Right_idx m')) ∧
      (∀n' m'. P (Right_idx n') (Left_idx m')) ⇒
      ∀v v1. P v v1

index_compare_def

⊢ index_compare End_idx End_idx = Equal ∧
  (∀v10. index_compare End_idx (Left_idx v10) = Less) ∧
  (∀v11. index_compare End_idx (Right_idx v11) = Less) ∧
  (∀v2. index_compare (Left_idx v2) End_idx = Greater) ∧
  (∀v3. index_compare (Right_idx v3) End_idx = Greater) ∧
  (∀n' m'. index_compare (Left_idx n') (Left_idx m') = index_compare n' m') ∧
  (∀n' m'. index_compare (Left_idx n') (Right_idx m') = Less) ∧
  (∀n' m'. index_compare (Right_idx n') (Right_idx m') = index_compare n' m') ∧
  ∀n' m'. index_compare (Right_idx n') (Left_idx m') = Greater

compare_index_equal

⊢ ∀i1 i2. index_compare i1 i2 = Equal ⇔ i1 = i2

compare_list_index

⊢ ∀l1 l2. list_cmp index_compare l1 l2 = Equal ⇔ l1 = l2

datatype_varmap

⊢ DATATYPE (varmap Empty_vm Node_vm)

varmap_11

⊢ ∀a0 a1 a2 a0' a1' a2'.
      Node_vm a0 a1 a2 = Node_vm a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'

varmap_distinct

⊢ ∀a2 a1 a0. Empty_vm ≠ Node_vm a0 a1 a2

varmap_nchotomy

⊢ ∀vv. vv = Empty_vm ∨ ∃a v v0. vv = Node_vm a v v0

varmap_Axiom

⊢ ∀f0 f1.
      ∃fn.
          fn Empty_vm = f0 ∧
          ∀a0 a1 a2. fn (Node_vm a0 a1 a2) = f1 a0 a1 a2 (fn a1) (fn a2)

varmap_induction

⊢ ∀P. P Empty_vm ∧ (∀v v0. P v ∧ P v0 ⇒ ∀a. P (Node_vm a v v0)) ⇒ ∀v. P v

varmap_case_cong

⊢ ∀M M' v f.
      M = M' ∧ (M' = Empty_vm ⇒ v = v') ∧
      (∀a0 a1 a2. M' = Node_vm a0 a1 a2 ⇒ f a0 a1 a2 = f' a0 a1 a2) ⇒
      varmap_CASE M v f = varmap_CASE M' v' f'

varmap_case_eq

⊢ varmap_CASE x v f = v' ⇔
  x = Empty_vm ∧ v = v' ∨ ∃a v'' v0. x = Node_vm a v'' v0 ∧ f a v'' v0 = v'

varmap_find_ind

⊢ ∀P.
      (∀x v1 v2. P End_idx (Node_vm x v1 v2)) ∧
      (∀i1 x v1 v2. P i1 v2 ⇒ P (Right_idx i1) (Node_vm x v1 v2)) ∧
      (∀i1 x v1 v2. P i1 v1 ⇒ P (Left_idx i1) (Node_vm x v1 v2)) ∧
      (∀i. P i Empty_vm) ⇒
      ∀v v1. P v v1

varmap_find_def

⊢ (∀x v2 v1. varmap_find End_idx (Node_vm x v1 v2) = x) ∧
  (∀x v2 v1 i1.
       varmap_find (Right_idx i1) (Node_vm x v1 v2) = varmap_find i1 v2) ∧
  (∀x v2 v1 i1.
       varmap_find (Left_idx i1) (Node_vm x v1 v2) = varmap_find i1 v1) ∧
  ∀i. varmap_find i Empty_vm = @x. T