chapter \<open>Generated by Lem from \<open>string.lem\<close>.\<close>

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 \<Rightarrow>(string)list \<Rightarrow> string "  where 
     " concat sep ([]) = ( (''''))"
|" concat sep (s # ss') = (
      (case  ss' of
        [] => s
      | _ => s @ (sep @ concat sep ss')
      ))" 
by pat_completeness auto

end