enrich
   string2nat, 
   stringlist
with
   

   
   
   functions  substring : string × nat × nat → string;
             comment: substring(str, offset, length),
                                                      offset is zero-based, 
                                                      unspecified for illegal values.;
              . .last : string → char;
              . .butlast : string → string;
              upcase : char → char;
              downcase : char → char;
              upcase : string → string;
              downcase : string → string;
              upcase : charlist → charlist;
              downcase : charlist → charlist;
              upcaseFirst : string → string;
              downcaseFirst : string → string;
              string-left-trim : string × string → string;
             comment: trim-chars, string-to-trim.;
              string-right-trim : string × string → string;
             comment: trim-chars, string-to-trim.;
              trim-number : string → string;
             comment: right-trim trailing numbers.;
   predicates  . ∈ . : char × string;
               . ⊑ . : string × string;
   
   
   
   

   

   axioms in-def :  ⊦ char ∈ str ↔ char ∈ s→l(str);
          last-def :  ⊦ str.last = s→l(str).last;
          butlast-def :  ⊦ str.butlast = l→s(s→l(str).butlast);
          prefix-def :  ⊦ str ⊑ str0 ↔ s→l(str) ⊑ s→l(str0);
          substring-def :  ⊦ substring(str, m, n) = l→s(sublist(m, n, s→l(str)));
          left-trim-empty :  ⊦ string-left-trim(str1, "") = "";
          used for: s, ls;
          left-trim-done :  ⊦ ¬ str2.char1 ∈ str1 ∧ str2 ≠ "" → string-left-trim(str1, str2) = str2;
          used for: s, ls;
          left-trim-rec :  ⊦ str2.char1 ∈ str1 ∧ str2 ≠ "" → string-left-trim(str1, str2) = string-left-trim(str1, str2.rstring);
          used for: s, ls;
          right-trim-empty :  ⊦ string-right-trim(str1, "") = "";
          used for: s, ls;
          right-trim-done :  ⊦ ¬ str2.last ∈ str1 ∧ str2 ≠ "" → string-right-trim(str1, str2) = str2;
          used for: s, ls;
          right-trim-rec :  ⊦ str2.last ∈ str1 ∧ str2 ≠ "" → string-right-trim(str1, str2) = string-right-trim(str1, str2.butlast);
          used for: s, ls;
          trim-number :  ⊦ trim-number(str) = string-right-trim("0123456789", str);
          Char-downcase-yes
          : ⊦   pos('A', sortedchars) ≤ pos(char, sortedchars) ∧ pos(char, sortedchars) ≤ pos('Z', sortedchars)
              → downcase(char) = s→l(sortedchars)[pos(char, sortedchars) + (pos('a', sortedchars) - pos('A', sortedchars))];
          comment: This definition is not based on actual positions in the sortedchars.
                       (But ASCII ordering is needed.);
          Char-downcase-no
          :  ⊦ ¬(pos('A', sortedchars) ≤ pos(char, sortedchars) ∧ pos(char, sortedchars) ≤ pos('Z', sortedchars)) → downcase(char) = char;
          Char-upcase-yes
          : ⊦   pos('a', sortedchars) ≤ pos(char, sortedchars) ∧ pos(char, sortedchars) ≤ pos('z', sortedchars)
              → upcase(char) = s→l(sortedchars)[pos(char, sortedchars) - (pos('a', sortedchars) - pos('A', sortedchars))];
          comment: This definition is not based on actual positions in the sortedchars.
                       (But ASCII ordering is needed.);
          Char-upcase-no :  ⊦ ¬(pos('a', sortedchars) ≤ pos(char, sortedchars) ∧ pos(char, sortedchars) ≤ pos('z', sortedchars)) → upcase(char) = char;
          String-downcase-empty :  ⊦ downcase("") = "";
          used for: s, ls;
          String-downcase-rec :  ⊦ downcase(char + str) = downcase(char) + downcase(str);
          used for: s, ls;
          String-upcase-empty :  ⊦ upcase("") = "";
          used for: s, ls;
          String-upcase-rec :  ⊦ upcase(char + str) = upcase(char) + upcase(str);
          used for: s, ls;
          String-downcaseFirst-empty :  ⊦ downcaseFirst("") = "";
          used for: s, ls;
          String-downcaseFirst-def :  ⊦ downcaseFirst(char + str) = downcase(char) + str;
          used for: s, ls;
          String-upcaseFirst-empty :  ⊦ upcaseFirst("") = "";
          used for: s, ls;
          String-upcaseFirst-def :  ⊦ upcaseFirst(char + str) = upcase(char) + str;
          used for: s, ls;

   

   
end enrich