Theory "quote"

Signature

Definitions

varmap_TY_DEF

⊢ ∃rep.
      TYPE_DEFINITION
        (λa0'.
             ∀ $var$('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) ∧ $var$('varmap') a1 ∧
                           $var$('varmap') a2) ⇒
                      $var$('varmap') a0') ⇒
                 $var$('varmap') a0') rep

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

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

index_TY_DEF

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

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)

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

Theorems

varmap_nchotomy

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

varmap_induction

⊢ ∀P. P Empty_vm ∧ (∀v v0. P v ∧ P v0 ⇒ ∀a. P (Node_vm a v v0)) ⇒ ∀v. P 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

varmap_distinct

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

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

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

index_nchotomy

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

index_induction

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

index_distinct

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

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

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

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

datatype_varmap

⊢ DATATYPE (varmap Empty_vm Node_vm)

datatype_index

⊢ DATATYPE (index Left_idx Right_idx End_idx)

compare_list_index

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

compare_index_equal

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