(*Generated by Lem from string.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_boolTheory lem_basic_classesTheory lem_listTheory lemTheory stringTheory;

val _ = numLib.prefer_num();



val _ = new_theory "lem_string"



(*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*)
 val concat_defn = Defn.Hol_multi_defns `
 ((concat:string ->(string)list -> string) sep ([])=  "")
/\ ((concat:string ->(string)list -> string) sep (s :: ss')=
       ((case ss' of
        [] => s
      | _ =>  STRCAT s  (STRCAT sep (concat sep ss'))
      )))`;

val _ = Lib.with_flag (computeLib.auto_import_definitions, false) (List.map Defn.save_defn) concat_defn;
val _ = export_theory()