Theory: quote

Parents

• prelim

Types

• varmap(Arity = 1)
• index(Arity = 0)

Constants

• index_lt  :index -> index -> bool
• Empty_vm  :'a varmap
• Left_idx  :index -> index
• ii_internal_mk_varmap  :'a recspace -> 'a varmap
• index_case  :(index -> 'a) -> (index -> 'a) -> 'a -> index -> 'a
• varmap_size  :('a -> num) -> 'a varmap -> num
• Right_idx  :index -> index
• index_compare_tupled  :index # index -> ordering
• ii_internal_dest_index  :index -> bool recspace
• index_compare  :index -> index -> ordering
• varmap_case  :'b -> ('a -> 'a varmap -> 'a varmap -> 'b) -> 'a varmap -> 'b
• ii_internal_dest_varmap  :'a varmap -> 'a recspace
• End_idx  :index
• ii_internalquote0  :index -> index
• ii_internalquote1  :index -> index
• ii_internalquote2  :index
• ii_internalquote3  :'a varmap
• ii_internalquote4  :'a -> 'a varmap -> 'a varmap -> 'a varmap
• varmap_find  :index -> 'a varmap -> 'a
• index_size  :index -> num
• varmap_find_tupled  :index # 'a varmap -> 'a
• Node_vm  :'a -> 'a varmap -> 'a varmap -> 'a varmap
• ii_internal_mk_index  :bool recspace -> index

Definitions

Empty_vm

|- Empty_vm = ii_internalquote3

End_idx

|- End_idx = ii_internalquote2

ii_internalquote0_def

|- ii_internalquote0 =
   (\a.
      ii_internal_mk_index
        ((\a. CONSTR 0 (@x. T) (FCONS a (\n. BOTTOM)))
           (ii_internal_dest_index a)))

ii_internalquote1_def

|- ii_internalquote1 =
   (\a.
      ii_internal_mk_index
        ((\a. CONSTR (SUC 0) (@x. T) (FCONS a (\n. BOTTOM)))
           (ii_internal_dest_index a)))

ii_internalquote2_def

|- ii_internalquote2 =
   ii_internal_mk_index (CONSTR (SUC (SUC 0)) (@x. T) (\n. BOTTOM))

ii_internalquote3_def

|- ii_internalquote3 = ii_internal_mk_varmap (CONSTR 0 (@v. T) (\n. BOTTOM))

ii_internalquote4_def

|- ii_internalquote4 =
   (\a0 a1 a2.
      ii_internal_mk_varmap
        ((\a0 a1 a2. CONSTR (SUC 0) a0 (FCONS a1 (FCONS a2 (\n. BOTTOM)))) a0
           (ii_internal_dest_varmap a1) (ii_internal_dest_varmap a2)))

index_case_def

|- (!f f1 v a. index_case f f1 v (Left_idx a) = f a) /\
   (!f f1 v a. index_case f f1 v (Right_idx a) = f1 a) /\
   !f f1 v. index_case f f1 v End_idx = v

index_compare_arg_munge_def

|- !x x1. index_compare x x1 = index_compare_tupled (x,x1)

index_compare_tupled_primitive_def

|- index_compare_tupled =
   WFREC
     (@R.
        WF R /\ (!m' n'. R (n',m') (Left_idx n',Left_idx m')) /\
        !m' n'. R (n',m') (Right_idx n',Right_idx m'))
     (\index_compare_tupled' a.
        pair_case
          (\v v1.
             index_case
               (\v4.
                  index_case (\v6. index_compare_tupled' (v4,v6)) (\v7. LESS)
                    GREATER v1)
               (\v5.
                  index_case (\v8. GREATER)
                    (\v9. index_compare_tupled' (v5,v9)) GREATER v1)
               (index_case (\v12. LESS) (\v13. LESS) EQUAL v1) v) a)

index_lt_def

|- !i1 i2. index_lt i1 i2 = (index_compare i1 i2 = LESS)

index_repfns

|- (!a. ii_internal_mk_index (ii_internal_dest_index a) = a) /\
   !r.
     (\a0.
        !'index'.
          (!a0.
             (?a.
                (a0 = (\a. CONSTR 0 (@x. T) (FCONS a (\n. BOTTOM))) a) /\
                'index' a) \/
             (?a.
                (a0 =
                 (\a. CONSTR (SUC 0) (@x. T) (FCONS a (\n. BOTTOM))) a) /\
                'index' a) \/
             (a0 = CONSTR (SUC (SUC 0)) (@x. T) (\n. BOTTOM)) ==>
             'index' a0) ==>
          'index' a0) r =
     (ii_internal_dest_index (ii_internal_mk_index r) = r)

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_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0.
          !'index'.
            (!a0.
               (?a.
                  (a0 = (\a. CONSTR 0 (@x. T) (FCONS a (\n. BOTTOM))) a) /\
                  'index' a) \/
               (?a.
                  (a0 =
                   (\a. CONSTR (SUC 0) (@x. T) (FCONS a (\n. BOTTOM))) a) /\
                  'index' a) \/
               (a0 = CONSTR (SUC (SUC 0)) (@x. T) (\n. BOTTOM)) ==>
               'index' a0) ==>
            'index' a0) rep

Left_idx

|- Left_idx = ii_internalquote0

Node_vm

|- Node_vm = ii_internalquote4

Right_idx

|- Right_idx = ii_internalquote1

varmap_case_def

|- (!v f. varmap_case v f Empty_vm = v) /\
   !v f a0 a1 a2. varmap_case v f (Node_vm a0 a1 a2) = f a0 a1 a2

varmap_find_arg_munge_def

|- !x x1. varmap_find x x1 = varmap_find_tupled (x,x1)

varmap_find_tupled_primitive_def

|- varmap_find_tupled =
   WFREC
     (@R.
        WF R /\ (!v1 x v2 i1. R (i1,v2) (Right_idx i1,Node_vm x v1 v2)) /\
        !v2 x v1 i1. R (i1,v1) (Left_idx i1,Node_vm x v1 v2))
     (\varmap_find_tupled' a.
        pair_case
          (\v v3.
             index_case
               (\v6.
                  varmap_case (@x. T)
                    (\v11 v12 v13. varmap_find_tupled' (v6,v12)) v3)
               (\v7.
                  varmap_case (@x. T)
                    (\v17 v18 v19. varmap_find_tupled' (v7,v19)) v3)
               (varmap_case (@x. T) (\v23 v24 v25. v23) v3) v) a)

varmap_repfns

|- (!a. ii_internal_mk_varmap (ii_internal_dest_varmap a) = a) /\
   !r.
     (\a0'.
        !'varmap'.
          (!a0'.
             (a0' = CONSTR 0 (@v. T) (\n. BOTTOM)) \/
             (?a0 a1 a2.
                (a0' =
                 (\a0 a1 a2.
                    CONSTR (SUC 0) a0 (FCONS a1 (FCONS a2 (\n. BOTTOM)))) a0
                   a1 a2) /\ 'varmap' a1 /\ 'varmap' a2) ==>
             'varmap' a0') ==>
          'varmap' a0') r =
     (ii_internal_dest_varmap (ii_internal_mk_varmap r) = r)

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_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'varmap'.
            (!a0'.
               (a0' = CONSTR 0 (@v. T) (\n. BOTTOM)) \/
               (?a0 a1 a2.
                  (a0' =
                   (\a0 a1 a2.
                      CONSTR (SUC 0) a0 (FCONS a1 (FCONS a2 (\n. BOTTOM)))) a0
                     a1 a2) /\ 'varmap' a1 /\ 'varmap' a2) ==>
               'varmap' a0') ==>
            'varmap' a0') rep

Theorems

compare_index_equal

|- !i1 i2. (index_compare i1 i2 = EQUAL) = (i1 = i2)

compare_list_index

|- !l1 l2. (list_compare index_compare l1 l2 = EQUAL) = (l1 = l2)

index_11

|- (!a a'. (Left_idx a = Left_idx a') = (a = a')) /\
   !a a'. (Right_idx a = Right_idx a') = (a = a')

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_case_cong

|- !v' v f1' f1 f' f M' M.
     (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 f f1 v M = index_case f' f1' v' M')

index_compare_def

|- (index_compare End_idx End_idx = EQUAL) /\
   (index_compare End_idx (Right_idx v11) = LESS) /\
   (index_compare End_idx (Left_idx v10) = LESS) /\
   (index_compare (Right_idx v3) End_idx = GREATER) /\
   (index_compare (Left_idx v2) End_idx = GREATER) /\
   (index_compare (Left_idx n') (Left_idx m') = index_compare n' m') /\
   (index_compare (Left_idx n') (Right_idx m') = LESS) /\
   (index_compare (Right_idx n') (Right_idx m') = index_compare n' m') /\
   (index_compare (Right_idx n') (Left_idx m') = GREATER)

index_compare_ind

|- !P.
     P End_idx End_idx /\ (!v11. P End_idx (Right_idx v11)) /\
     (!v10. P End_idx (Left_idx v10)) /\ (!v3. P (Right_idx v3) End_idx) /\
     (!v2. P (Left_idx v2) 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_distinct

|- (!a' a. ~(Left_idx a = Right_idx a')) /\ (!a. ~(Left_idx a = End_idx)) /\
   !a. ~(Right_idx a = 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_nchotomy

|- !i. (?i'. i = Left_idx i') \/ (?i'. i = Right_idx i') \/ (i = End_idx)

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

|- !f' f v' v M' M.
     (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 v f M = varmap_case v' f' M')

varmap_distinct

|- !a2 a1 a0. ~(Empty_vm = Node_vm a0 a1 a2)

varmap_find_def

|- (varmap_find End_idx (Node_vm x v1 v2) = x) /\
   (varmap_find (Right_idx i1) (Node_vm x v1 v2) = varmap_find i1 v2) /\
   (varmap_find (Left_idx i1) (Node_vm x v1 v2) = varmap_find i1 v1) /\
   (varmap_find End_idx Empty_vm = @x. T) /\
   (varmap_find (Right_idx v5) Empty_vm = @x. T) /\
   (varmap_find (Left_idx v4) Empty_vm = @x. T)

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)) /\
     P End_idx Empty_vm /\ (!v5. P (Right_idx v5) Empty_vm) /\
     (!v4. P (Left_idx v4) Empty_vm) ==>
     !v v1. P v v1

varmap_induction

|- !P.
     P Empty_vm /\ (!v v0. P v /\ P v0 ==> !a. P (Node_vm a v v0)) ==> !v. P v

varmap_nchotomy

|- !v. (v = Empty_vm) \/ ?a v' v0. v = Node_vm a v' v0