blob: 9df246c471e75c288e0da4e56a103903192f6e77 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
|
chapter \<open>Generated by Lem from string.lem.\<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
|
