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