Theory Lem_string

chapter ‹Generated by Lem from ‹string.lem›.›

theory "Lem_string" 

imports
  Main
  "Lem_bool"
  "Lem_basic_classes"
  "Lem_list"

begin 



― ‹‹open import Bool Basic_classes List››
― ‹‹open import {ocaml} `Xstring`››
― ‹‹open import {hol} `lemTheory` `stringTheory`››
― ‹‹open import {coq} `Coq.Strings.Ascii` `Coq.Strings.String`››

― ‹‹ ------------------------------------------- ››
― ‹‹ translations between strings and char lists ››
― ‹‹ ------------------------------------------- ››

― ‹‹val toCharList : string -> list char››

― ‹‹val toString : list char -> string››


― ‹‹ ----------------------- ››
― ‹‹ generating strings      ››
― ‹‹ ----------------------- ››

― ‹‹val makeString : nat -> char -> string››
― ‹‹let makeString len c=  toString (replicate len c)››

― ‹‹ ----------------------- ››
― ‹‹ length                  ››
― ‹‹ ----------------------- ››

― ‹‹val stringLength : string -> nat››

― ‹‹ ----------------------- ››
― ‹‹ string concatenation    ››
― ‹‹ ----------------------- ››

― ‹‹val ^ [stringAppend] : string -> string -> string››


― ‹‹ ----------------------------››
― ‹‹ setting up pattern matching ››
― ‹‹ --------------------------- ››

― ‹‹val string_case : forall 'a. string -> 'a -> (char -> string -> 'a) -> 'a››

― ‹‹let string_case s c_empty c_cons=
   match (toCharList s) with
    | [] -> c_empty
    | c :: cs -> c_cons c (toString cs)
  end››

― ‹‹val empty_string : string››

― ‹‹val cons_string : char -> string -> string››

― ‹‹val concat : string -> list string -> string››
function (sequential,domintros)  concat  :: " string ⇒(string)list ⇒ string "  where 
     " concat sep ([]) = ( (''''))"
|" concat sep (s # ss') = (
      (case  ss' of
        [] => s
      | _ => s @ (sep @ concat sep ss')
      ))" 
by pat_completeness auto

end