(*** This file is part of Lem.  eth-isabelle project just uses it.  See lem-license. ***)

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 \<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
