Theory: string

Parents

• ascii

Types

• string(Arity = 0)

Constants

• ii_internal_mk_string  :ascii recspace -> string
• string_size  :string -> num
• ii_internal_dest_string  :string -> ascii recspace
• emptystring  :string
• ii_internalstring0  :string
• ii_internalstring1  :ascii -> string -> string
• STRING  :ascii -> string -> string
• string_case  :'a -> (ascii -> string -> 'a) -> string -> 'a

Definitions

emptystring

|- "" = ii_internalstring0

ii_internalstring0_def

|- ii_internalstring0 = ii_internal_mk_string (CONSTR 0 (@v. T) (\n. BOTTOM))

ii_internalstring1_def

|- ii_internalstring1 =
   (\a0 a1.
      ii_internal_mk_string
        ((\a0 a1. CONSTR (SUC 0) a0 (FCONS a1 (\n. BOTTOM))) a0
           (ii_internal_dest_string a1)))

STRING

|- STRING = ii_internalstring1

string_case_def

|- (!v f. string_case v f "" = v) /\
   !v f a0 a1. string_case v f (STRING a0 a1) = f a0 a1

string_repfns

|- (!a. ii_internal_mk_string (ii_internal_dest_string a) = a) /\
   !r.
     (\a0'.
        !'string'.
          (!a0'.
             (a0' = CONSTR 0 (@v. T) (\n. BOTTOM)) \/
             (?a0 a1.
                (a0' =
                 (\a0 a1. CONSTR (SUC 0) a0 (FCONS a1 (\n. BOTTOM))) a0 a1) /\
                'string' a1) ==>
             'string' a0') ==>
          'string' a0') r =
     (ii_internal_dest_string (ii_internal_mk_string r) = r)

string_size_def

|- (string_size "" = 0) /\
   !a0 a1. string_size (STRING a0 a1) = 1 + (ascii_size a0 + string_size a1)

string_TY_DEF

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

Theorems

string_11

|- !a0 a1 a0' a1'. (STRING a0 a1 = STRING a0' a1') = (a0 = a0') /\ (a1 = a1')

string_Axiom

|- !f0 f1. ?fn. (fn "" = f0) /\ !a0 a1. fn (STRING a0 a1) = f1 a0 a1 (fn a1)

string_case_cong

|- !f' f v' v M' M.
     (M = M') /\ ((M' = "") ==> (v = v')) /\
     (!a0 a1. (M' = STRING a0 a1) ==> (f a0 a1 = f' a0 a1)) ==>
     (string_case v f M = string_case v' f' M')

string_distinct

|- !a1 a0. ~("" = STRING a0 a1)

string_induction

|- !P. P "" /\ (!s. P s ==> !a. P (STRING a s)) ==> !s. P s

string_nchotomy

|- !s. (s = "") \/ ?a s'. s = STRING a s'