stringScript.sml
1(* =====================================================================*)
2(* FILE : stringScript.sml *)
3(* DESCRIPTION : A theory of 8-bit characters and strings built *)
4(* from them. *)
5(* *)
6(* AUTHOR : Konrad Slind, University of Cambridge, 2001 *)
7(* =====================================================================*)
8
9Theory string
10Ancestors
11 rich_list ternaryComparisons
12 list arithmetic pred_set relation
13Libs
14 numLib numSyntax
15
16(* ---------------------------------------------------------------------*)
17(* Characters are represented by the natural numbers <= 255. *)
18(* ---------------------------------------------------------------------*)
19
20Theorem CHAR_EXISTS[local]:
21 ∃n. (λn. n < 256) n
22Proof Q.EXISTS_TAC `0` THEN REDUCE_TAC
23QED
24
25val CHAR_TYPE = new_type_definition("char", CHAR_EXISTS);
26
27val CHAR_TYPE_FACTS =
28 (define_new_type_bijections
29 {ABS="CHR", REP="ORD",name="char_BIJ", tyax=CHAR_TYPE});
30
31Theorem ORD_11 = prove_rep_fn_one_one CHAR_TYPE_FACTS
32Theorem CHR_11[simp] =
33 BETA_RULE (prove_abs_fn_one_one CHAR_TYPE_FACTS);
34Theorem ORD_ONTO =
35 BETA_RULE (prove_rep_fn_onto CHAR_TYPE_FACTS);
36Theorem CHR_ONTO =
37 BETA_RULE (prove_abs_fn_onto CHAR_TYPE_FACTS);
38
39Theorem CHR_ORD[simp] = CONJUNCT1 CHAR_TYPE_FACTS
40Theorem ORD_CHR = BETA_RULE (CONJUNCT2 CHAR_TYPE_FACTS);
41
42Theorem ORD_CHR_RWT[simp]:
43 !r. r < 256 ==> (ORD (CHR r) = r)
44Proof
45 PROVE_TAC [ORD_CHR]
46QED
47
48Theorem ORD_CHR_COMPUTE[compute]:
49 !n. ORD (CHR n) =
50 if n < 256 then n else FAIL ORD ^(mk_var("> 255", bool)) (CHR n)
51Proof SRW_TAC [] [combinTheory.FAIL_THM]
52QED
53
54Theorem ORD_BOUND:
55 !c. ORD c < 256
56Proof
57 PROVE_TAC [ORD_ONTO]
58QED
59
60Theorem char_nchotomy:
61 !c. ?n. c = CHR n
62Proof
63 STRIP_TAC THEN Q.EXISTS_TAC `ORD c` THEN REWRITE_TAC [CHR_ORD]
64QED
65
66Theorem ranged_char_nchotomy:
67 !c. ?n. (c = CHR n) /\ n < 256
68Proof
69 STRIP_TAC THEN Q.EXISTS_TAC `ORD c` THEN REWRITE_TAC [CHR_ORD, ORD_BOUND]
70QED
71
72val ordn = term_of_int o Char.ord;
73
74Definition isLower_def:
75 isLower c <=> ^(ordn #"a") <= ORD c /\ ORD c <= ^(ordn #"z")
76End
77
78Definition isUpper_def:
79 isUpper c <=> ^(ordn #"A") <= ORD c /\ ORD c <= ^(ordn #"Z")
80End
81
82Definition isDigit_def:
83 isDigit c <=> ^(ordn #"0") <= ORD c /\ ORD c <= ^(ordn #"9")
84End
85
86Definition isAlpha_def: isAlpha c <=> isLower c \/ isUpper c
87End
88
89Definition isHexDigit_def:
90 isHexDigit c <=> ^(ordn #"0") <= ORD c /\ ORD c <= ^(ordn #"9") \/
91 ^(ordn #"a") <= ORD c /\ ORD c <= ^(ordn #"f") \/
92 ^(ordn #"A") <= ORD c /\ ORD c <= ^(ordn #"F")
93End
94
95Definition isAlphaNum_def: isAlphaNum c <=> isAlpha c \/ isDigit c
96End
97
98Definition isPrint_def:
99 isPrint c <=> ^(ordn #" ") <= ORD c /\ ORD c < 127
100End
101
102Theorem isAlphaNum_isPrint:
103 !x. isAlphaNum x ==> isPrint x
104Proof EVAL_TAC \\ rw[]
105QED
106
107Theorem isHexDigit_isAlphaNum:
108 !x. isHexDigit x ==> isAlphaNum x
109Proof EVAL_TAC \\ rw[]
110QED
111
112Theorem isHexDigit_isPrint:
113 !x. isHexDigit x ==> isPrint x
114Proof metis_tac[isAlphaNum_isPrint, isHexDigit_isAlphaNum]
115QED
116
117Definition isSpace_def:
118 isSpace c <=> (ORD c = ^(ordn #" ")) \/ 9 <= ORD c /\ ORD c <= 13
119End
120
121Definition isGraph_def: isGraph c <=> isPrint c /\ ~isSpace c
122End
123
124Definition isPunct_def: isPunct c <=> isGraph c /\ ~isAlphaNum c
125End
126
127Definition isAscii_def: isAscii c <=> ORD c <= 127
128End
129
130Definition isCntrl_def:
131 isCntrl c <=> ORD c < ^(ordn #" ") \/ 127 <= ORD c
132End
133
134Definition toLower_def:
135 toLower c = if isUpper c then CHR (ORD c + 32) else c
136End
137
138Definition toUpper_def:
139 toUpper c = if isLower c then CHR (ORD c - 32) else c
140End
141
142Definition char_lt_def: char_lt a b <=> ORD a < ORD b
143End
144Definition char_le_def: char_le a b <=> ORD a <= ORD b
145End
146Definition char_gt_def: char_gt a b <=> ORD a > ORD b
147End
148Definition char_ge_def: char_ge a b <=> ORD a >= ORD b
149End
150
151Definition char_compare_def:
152 char_compare c1 c2 = num_compare (ORD c1) (ORD c2)
153End
154
155Overload "<"[inferior] = “char_lt”
156Overload ">"[inferior] = “char_gt”
157Overload "<="[inferior] = “char_le”
158Overload ">="[inferior] = “char_ge”
159
160(*---------------------------------------------------------------------------
161 In our development, CHR is not a constructor. Is that really
162 important? We can at least prove the following theorem about
163 equality of chars.
164 ---------------------------------------------------------------------------*)
165
166Theorem CHAR_EQ_THM[compute]:
167 !c1 c2. (c1 = c2) = (ORD c1 = ORD c2)
168Proof REPEAT GEN_TAC THEN EQ_TAC THEN RW_TAC bool_ss [ORD_11]
169QED
170
171Theorem CHAR_INDUCT_THM:
172 !P. (!n. n < 256 ==> P (CHR n)) ==> !c. P c
173Proof
174REPEAT STRIP_TAC
175 THEN STRIP_ASSUME_TAC (Q.SPEC `c` CHR_ONTO)
176 THEN RW_TAC bool_ss []
177QED
178
179Definition char_size_def: char_size (c:char) = 0
180End
181
182val _ = TypeBase.export [
183 TypeBasePure.mk_nondatatype_info (
184 “:char”,
185 {nchotomy = SOME ranged_char_nchotomy,
186 induction = NONE,
187 size = SOME(“char_size”,char_size_def),
188 encode = NONE}
189 )
190 ]
191
192(*---------------------------------------------------------------------------
193 Some facts about the set of all characters and relations between them.
194 ---------------------------------------------------------------------------*)
195
196Theorem UNIV_IMAGE_CHR_count_256:
197 UNIV = IMAGE CHR (count 256)
198Proof
199 rw[EXTENSION]
200 \\ qspec_then`x`FULL_STRUCT_CASES_TAC ranged_char_nchotomy
201 \\ metis_tac[]
202QED
203
204Theorem FINITE_UNIV_char[simp]:
205 FINITE (UNIV:char set)
206Proof
207 simp[UNIV_IMAGE_CHR_count_256]
208QED
209
210Theorem RC_char_lt:
211 RC (char_lt) = char_le
212Proof
213 rw[FUN_EQ_THM, RC_DEF, char_le_def, char_lt_def, arithmeticTheory.LESS_OR_EQ]
214 \\ metis_tac[ORD_11]
215QED
216
217Theorem WF_char_lt[simp]:
218 WF char_lt
219Proof
220 rw[WF_DEF]
221 \\ qexists_tac`CHR (LEAST n. (n < 256) /\ B (CHR n))`
222 \\ numLib.LEAST_ELIM_TAC
223 \\ conj_tac
224 >- (qspec_then`w`FULL_STRUCT_CASES_TAC ranged_char_nchotomy
225 \\ fs[] \\ metis_tac[])
226 \\ rw[] \\ qspec_then`b`FULL_STRUCT_CASES_TAC ranged_char_nchotomy
227 \\ fs[char_lt_def] \\ rfs[]
228QED
229
230(*---------------------------------------------------------------------------
231 Strings are represented as lists of characters. This gives us
232 EXPLODE and IMPLODE as the functions mapping into, and from, the
233 representation.
234 ---------------------------------------------------------------------------*)
235
236Type string[pp] = ``:char list``
237
238Overload STRING[inferior] = “CONS : char -> string -> string”
239Overload EMPTYSTRING[inferior] = “[] : string”
240Overload CONCAT[inferior] = “FLAT : string list -> string”
241
242Definition string_compare_def:
243 string_compare = list_compare char_compare
244End
245
246val _ = new_definition(GrammarSpecials.string_elim_term,
247 “^(mk_var(GrammarSpecials.string_elim_term,
248 “:string -> string”)) s = s”);
249val _ = overload_on(GrammarSpecials.std_stringinjn_name,
250 mk_const(GrammarSpecials.string_elim_term,
251 “:string -> string”))
252
253Definition SUB_def: SUB (s:string, n) = EL n s
254End
255Definition STR_def: STR (c:char) = [c]
256End
257Definition TOCHAR_def: TOCHAR [c] = c: char
258End
259
260Definition SUBSTRING_def: SUBSTRING (s:string,i,n) = SEG n i s
261End
262
263Definition TRANSLATE_def: TRANSLATE f (s:string) = CONCAT (MAP f s)
264End
265
266Theorem SPLITP_MONO[local]:
267 !P l. LENGTH (SND (SPLITP P l)) <= LENGTH l
268Proof
269 Induct_on `l` THEN SRW_TAC [] [SPLITP, DECIDE ``a <= b ==> a <= SUC b``]
270QED
271
272Theorem TAIL_MONO[local]:
273 !l. ~(l = []) ==> LENGTH (TL l) < LENGTH l
274Proof Cases THEN SRW_TAC [] []
275QED
276
277Definition TOKENS_def:
278 (TOKENS P ([]:string) = []) /\
279 (TOKENS P (h::t) =
280 let (l,r) = SPLITP P (h::t) in
281 if NULL l then
282 TOKENS P (TL r)
283 else
284 l::TOKENS P r)
285Termination
286 WF_REL_TAC `measure (LENGTH o SND)`
287 THEN SRW_TAC [] [NULL_EQ_NIL, SPLITP]
288 THEN METIS_TAC [SPLITP_MONO, DECIDE ``a <= b ==> a < SUC b``]
289End
290
291Definition FIELDS_def:
292 (FIELDS P ([]:string) = [[]]) /\
293 (FIELDS P (h::t) =
294 let (l,r) = SPLITP P (h::t) in
295 if NULL l then
296 []::FIELDS P (TL r)
297 else
298 if NULL r then [l] else l::FIELDS P (TL r))
299Termination
300 WF_REL_TAC `measure (LENGTH o SND)`
301 THEN SRW_TAC [] [NULL_EQ_NIL, SPLITP]
302 THEN METIS_TAC [SPLITP_MONO, TAIL_MONO, arithmeticTheory.LESS_TRANS,
303 DECIDE ``a <= b ==> a < 1 + SUC b``]
304End
305
306Definition IMPLODE_def[simp]:
307 (IMPLODE [] = "") /\
308 (IMPLODE (c::cs) = STRING c (IMPLODE cs))
309End
310
311Definition EXPLODE_def[simp]:
312 (EXPLODE "" = []) /\
313 (EXPLODE (STRING c s) = c :: EXPLODE s)
314End
315
316Theorem IMPLODE_EXPLODE_I[compute]:
317 (EXPLODE s = s) /\ (IMPLODE s = s)
318Proof
319 Induct_on `s` THEN SRW_TAC [][]
320QED
321
322Theorem IMPLODE_EXPLODE[simp]:
323 IMPLODE (EXPLODE s) = s
324Proof
325 Induct_on `s` THEN SRW_TAC [][]
326QED
327
328Theorem EXPLODE_IMPLODE[simp]:
329 EXPLODE (IMPLODE cs) = cs
330Proof
331 Induct_on `cs` THEN SRW_TAC [][]
332QED
333
334Theorem EXPLODE_ONTO: !cs. ?s. cs = EXPLODE s
335Proof METIS_TAC [EXPLODE_IMPLODE, IMPLODE_EXPLODE]
336QED
337Theorem IMPLODE_ONTO: !s. ?cs. s = IMPLODE cs
338Proof METIS_TAC [EXPLODE_IMPLODE, IMPLODE_EXPLODE]
339QED
340Theorem EXPLODE_11[simp]: (EXPLODE s1 = EXPLODE s2) = (s1 = s2)
341Proof METIS_TAC [EXPLODE_IMPLODE, IMPLODE_EXPLODE]
342QED
343Theorem IMPLODE_11[simp]: (IMPLODE cs1 = IMPLODE cs2) = (cs1 = cs2)
344Proof METIS_TAC [EXPLODE_IMPLODE, IMPLODE_EXPLODE]
345QED
346
347
348Theorem TOKENS_APPEND:
349 !P l1 x l2.
350 P x ==>
351 (TOKENS P (l1 ++ x::l2) = TOKENS P l1 ++ TOKENS P l2)
352Proof
353 ho_match_mp_tac TOKENS_ind
354 \\ rw[TOKENS_def] >- (fs[SPLITP])
355 \\ pairarg_tac \\ fs[]
356 \\ pairarg_tac \\ fs[]
357 \\ fs[NULL_EQ, SPLITP]
358 \\ Cases_on `P h` \\ full_simp_tac bool_ss []
359 \\ rw[]
360 \\ fs[TL]
361 \\ Cases_on `EXISTS P t` \\ rw[SPLITP_APPEND, SPLITP]
362 \\ fs[NOT_EXISTS] \\ imp_res_tac (GSYM SPLITP_NIL_SND_EVERY) \\ rw[]
363 \\ fs[NOT_EXISTS] \\ imp_res_tac (GSYM SPLITP_NIL_SND_EVERY) \\ rw[]
364QED
365
366Theorem TOKENS_NIL:
367 !ls. (TOKENS f ls = []) <=> EVERY f ls
368Proof
369 Induct \\ rw[TOKENS_def] \\ pairarg_tac
370 \\ fs[NULL_EQ, SPLITP]
371 \\ BasicProvers.EVERY_CASE_TAC \\ fs[] \\ rw[]
372QED
373
374Theorem TOKENS_FRONT:
375 ~NULL ls /\ P (LAST ls) ==>
376 (TOKENS P (FRONT ls) = TOKENS P ls)
377Proof
378 Induct_on`ls` \\ rw[]
379 \\ Cases_on`ls` \\ fs[]
380 >- rw[TOKENS_def,SPLITP]
381 \\ rw[TOKENS_def]
382 \\ pairarg_tac
383 \\ simp[Once SPLITP]
384 \\ CASE_TAC \\ fs[NULL_EQ]
385 >- (
386 imp_res_tac SPLITP_NIL_FST_IMP
387 \\ imp_res_tac SPLITP_IMP
388 \\ rfs[] )
389 \\ imp_res_tac SPLITP_JOIN
390 \\ Cases_on`l` \\ fs[] \\ rpt BasicProvers.VAR_EQ_TAC
391 \\ imp_res_tac SPLITP_IMP
392 \\ CASE_TAC \\ fs[]
393 \\ qmatch_goalsub_rename_tac`SPLITP P (x::xs)`
394 \\ `?y ys. x::xs = SNOC y ys` by metis_tac[SNOC_CASES,list_distinct]
395 \\ full_simp_tac std_ss [FRONT_SNOC,LAST_SNOC] \\ rpt BasicProvers.VAR_EQ_TAC
396 \\ qmatch_goalsub_rename_tac`SPLITP P (SNOC y (w ++ z))`
397 \\ Cases_on`NULL z` \\ fs[NULL_EQ, SNOC_APPEND]
398 >- (
399 simp[SPLITP_APPEND]
400 \\ full_simp_tac std_ss [GSYM NOT_EXISTS]
401 \\ simp[SPLITP,TOKENS_def] )
402 \\ Cases_on`z` \\ fs[]
403 \\ simp[SPLITP_APPEND]
404 \\ full_simp_tac std_ss [GSYM NOT_EXISTS]
405 \\ simp[SPLITP,TOKENS_def]
406 \\ simp[TOKENS_APPEND,TOKENS_NIL]
407QED
408
409(*---------------------------------------------------------------------------
410 Definability of prim. rec. functions over strings.
411 ---------------------------------------------------------------------------*)
412
413Theorem alt_string_Axiom[local]:
414 !b g. ?f. (f (IMPLODE []) = b) /\
415 (!c t. f (IMPLODE (c::t)) = g c t (f (IMPLODE t)))
416Proof
417REPEAT GEN_TAC
418 THEN STRIP_ASSUME_TAC
419 (prove_rec_fn_exists listTheory.list_Axiom
420 ``(list_rec (b:'a) f ([]:char list) = b) /\
421 (list_rec b f (h::t) = f h t (list_rec b f t))``)
422 THEN Q.EXISTS_TAC`list_rec b g o EXPLODE`
423 THEN RW_TAC bool_ss [combinTheory.o_DEF,list_case_def,EXPLODE_IMPLODE]
424QED
425
426
427Theorem STRING_ACYCLIC:
428 !s c. ~(STRING c s = s) /\ ~(s = STRING c s)
429Proof
430 Induct THEN SRW_TAC [][]
431QED
432
433(*---------------------------------------------------------------------------
434 Size of a string.
435 ---------------------------------------------------------------------------*)
436
437Overload STRLEN[inferior] = “LENGTH : string -> num”
438val STRLEN_DEF = listTheory.LENGTH
439
440Definition EXTRACT_def:
441 (EXTRACT (s,i,NONE) = SUBSTRING(s,i,STRLEN s - i)) /\
442 (EXTRACT (s,i,SOME n) = SUBSTRING(s,i,n))
443End
444
445Theorem STRLEN_EXPLODE_THM:
446 STRLEN s = LENGTH (EXPLODE s)
447Proof
448 SRW_TAC [][IMPLODE_EXPLODE_I]
449QED
450
451(*---------------------------------------------------------------------------*)
452(* Destruct a string. This will be used to re-phrase the HOL development *)
453(* with an ML definition of DEST_STRING in terms of the Basis String struct. *)
454(*---------------------------------------------------------------------------*)
455
456Definition DEST_STRING_def[simp]:
457 (DEST_STRING "" = NONE) /\
458 (DEST_STRING (STRING c rst) = SOME(c,rst))
459End
460
461Theorem DEST_STRING_LEMS:
462 !s. ((DEST_STRING s = NONE) = (s = "")) /\
463 ((DEST_STRING s = SOME(c,t)) = (s = STRING c t))
464Proof
465 Cases THEN SRW_TAC [][]
466QED
467
468Theorem EXPLODE_EQNS = EXPLODE_def
469Theorem IMPLODE_EQNS = IMPLODE_def
470
471(* ----------------------------------------------------------------------
472 More rewrites for IMPLODE and EXPLODE
473 ---------------------------------------------------------------------- *)
474
475Theorem IMPLODE_EQ_EMPTYSTRING[simp]:
476 ((IMPLODE l = "") = (l = [])) /\
477 (("" = IMPLODE l) = (l = []))
478Proof
479 Cases_on `l` THEN SRW_TAC [][]
480QED
481
482Theorem EXPLODE_EQ_NIL[simp]:
483 ((EXPLODE s = []) = (s = "")) /\
484 (([] = EXPLODE s) = (s = ""))
485Proof
486 Cases_on `s` THEN SRW_TAC [][]
487QED
488
489Theorem EXPLODE_EQ_THM:
490 !s h t. ((h::t = EXPLODE s) = (s = STRING h (IMPLODE t))) /\
491 ((EXPLODE s = h::t) = (s = STRING h (IMPLODE t)))
492Proof
493 Cases THEN SRW_TAC [][EQ_IMP_THM] THEN SRW_TAC [][]
494QED
495
496Theorem IMPLODE_EQ_THM:
497 !c s l. ((STRING c s = IMPLODE l) = (l = c::EXPLODE s)) /\
498 ((IMPLODE l = STRING c s) = (l = c::EXPLODE s))
499Proof
500 Cases_on `l` THEN SRW_TAC [][EQ_IMP_THM] THEN SRW_TAC [][]
501QED
502
503(*---------------------------------------------------------------------------*)
504(* ML-style recursion equations for EXPLODE and IMPLODE *)
505(*---------------------------------------------------------------------------*)
506
507Theorem EXPLODE_DEST_STRING:
508 !s. EXPLODE s = case DEST_STRING s
509 of NONE => []
510 | SOME(c,t) => c::EXPLODE t
511Proof
512 Cases THEN SRW_TAC [][]
513QED
514
515Theorem IMPLODE_STRING:
516 !clist.IMPLODE clist = FOLDR STRING "" clist
517Proof
518 Induct THEN SRW_TAC [][]
519QED
520
521(*---------------------------------------------------------------------------*)
522(* Main fact about STRLEN *)
523(*---------------------------------------------------------------------------*)
524
525val stringinst = INST_TYPE [alpha |-> ``:char``]
526
527Theorem STRLEN_EQ_0 = stringinst LENGTH_NIL
528Theorem STRLEN_THM = stringinst LENGTH
529Theorem STRLEN_DEF = STRLEN_THM
530
531(*---------------------------------------------------------------------------
532 String concatenation
533 ---------------------------------------------------------------------------*)
534
535Overload STRCAT[inferior] = “list$APPEND : string -> string -> string”
536
537
538Theorem STRCAT_def = stringinst APPEND
539
540Theorem STRCAT:
541 STRCAT s1 s2 = STRCAT s1 s2
542Proof
543 SRW_TAC [][]
544QED
545
546Theorem STRCAT_EQNS:
547 (STRCAT "" s = s) /\
548 (STRCAT s "" = s) /\
549 (STRCAT (STRING c s1) s2 = STRING c (STRCAT s1 s2))
550Proof
551 SRW_TAC [][STRCAT_def]
552QED
553
554Theorem STRCAT_ASSOC = stringinst APPEND_ASSOC
555
556Theorem STRCAT_11 = stringinst APPEND_11
557
558Theorem STRCAT_ACYCLIC:
559 !s s1. ((s = STRCAT s s1) = (s1 = "")) /\
560 ((s = STRCAT s1 s) = (s1 = ""))
561Proof
562 PROVE_TAC [STRCAT_EQNS,STRCAT_11]
563QED
564
565Theorem STRCAT_EXPLODE:
566 !s1 s2. STRCAT s1 s2 = FOLDR STRING s2 (EXPLODE s1)
567Proof
568 Induct THEN SRW_TAC [][]
569QED
570
571Theorem STRCAT_EQ_EMPTY =
572 CONJUNCT2 (stringinst APPEND_eq_NIL)
573(*---------------------------------------------------------------------------
574 String length and concatenation
575 ---------------------------------------------------------------------------*)
576
577Theorem STRLEN_CAT = stringinst LENGTH_APPEND
578
579(*---------------------------------------------------------------------------
580 Is one string a prefix of another?
581 ---------------------------------------------------------------------------*)
582
583Theorem isPREFIX_DEF:
584 !s1 s2.
585 isPREFIX s1 s2 =
586 case (DEST_STRING s1, DEST_STRING s2)
587 of (NONE, _) => T
588 | (SOME __, NONE) => F
589 | (SOME(c1,t1),SOME(c2,t2)) => (c1=c2) /\ isPREFIX t1 t2
590Proof
591 Cases_on `s1` THEN Cases_on `s2` THEN SRW_TAC [][]
592QED
593
594Theorem isPREFIX_IND:
595 !P. (!s1 s2.
596 (!c t1 t2.
597 (DEST_STRING s1 = SOME (c,t1)) /\
598 (DEST_STRING s2 = SOME (c,t2)) ==> P t1 t2) ==> P s1 s2)
599 ==> !v v1. P v v1
600Proof
601 GEN_TAC THEN STRIP_TAC THEN Induct THEN SRW_TAC [][]
602QED
603
604Theorem isPREFIX_STRCAT:
605 !s1 s2. isPREFIX s1 s2 = ?s3. s2 = STRCAT s1 s3
606Proof
607 Induct THEN SRW_TAC [][] THEN Cases_on `s2` THEN SRW_TAC [][] THEN
608 PROVE_TAC []
609QED
610
611(*---------------------------------------------------------------------------
612 Orderings
613 ---------------------------------------------------------------------------*)
614
615Definition string_lt_def:
616 (string_lt s EMPTYSTRING <=> F) /\
617 (string_lt EMPTYSTRING (STRING c s) <=> T) /\
618 (string_lt (STRING c1 s1) (STRING c2 s2) <=>
619 c1 < c2 \/ (c1 = c2) /\ string_lt s1 s2)
620End
621
622Definition string_le_def: string_le s1 s2 <=> (s1 = s2) \/ string_lt s1 s2
623End
624Definition string_gt_def: string_gt s1 s2 <=> string_lt s2 s1
625End
626Definition string_ge_def: string_ge s1 s2 <=> string_le s2 s1
627End
628
629Overload "<"[inferior] = “string_lt”
630Overload ">"[inferior] = “string_gt”
631Overload "<="[inferior] = “string_le”
632Overload ">="[inferior] = “string_ge”
633
634Theorem string_lt_nonrefl:
635 !s:string. ~(s < s)
636Proof
637 Induct THEN ASM_SIMP_TAC std_ss [string_lt_def,char_lt_def]
638QED
639
640Theorem string_lt_antisym:
641 !s t:string. ~(s < t /\ t < s)
642Proof
643 SIMP_TAC std_ss []
644 THEN Induct THEN Cases_on `t` THEN SIMP_TAC std_ss [string_lt_def,char_lt_def]
645 THEN REPEAT STRIP_TAC THEN Cases_on `h = h'` THEN ASM_SIMP_TAC std_ss []
646 THEN FULL_SIMP_TAC std_ss [GSYM ORD_11] THEN DECIDE_TAC
647QED
648
649Theorem string_lt_cases:
650 !s t:string. (s = t) \/ s < t \/ t < s
651Proof
652 Induct THEN Cases_on `t` THEN SIMP_TAC std_ss [string_lt_def,char_lt_def]
653 THEN SIMP_TAC std_ss [CONS_11,GSYM ORD_11] THEN STRIP_TAC
654 THEN Cases_on `ORD h = ORD h'` THEN ASM_SIMP_TAC std_ss [] THEN DECIDE_TAC
655QED
656
657Theorem string_lt_trans:
658 !s1 s2 s3:string. s1 < s2 /\ s2 < s3 ==> s1 < s3
659Proof
660 Induct THEN Cases_on `s2` THEN Cases_on `s3`
661 THEN SIMP_TAC std_ss [string_lt_def,char_lt_def,GSYM ORD_11] THEN STRIP_TAC
662 THEN Cases_on `ORD h'' < ORD h'` THEN ASM_SIMP_TAC std_ss [IMP_CONJ_THM]
663 THEN STRIP_TAC THEN1 (REPEAT STRIP_TAC THEN DECIDE_TAC)
664 THEN REPEAT STRIP_TAC THEN IMP_RES_TAC arithmeticTheory.LESS_TRANS
665 THEN METIS_TAC []
666QED
667
668val string_lt_ind = theorem"string_lt_ind";
669
670Theorem string_lt_LLEX:
671 string_lt = LLEX char_lt
672Proof
673 simp[FUN_EQ_THM]
674 \\ recInduct string_lt_ind
675 \\ rw[string_lt_def]
676QED
677
678Theorem not_WF_string_lt:
679 ~WF string_lt
680Proof
681 rw[string_lt_LLEX]
682 \\ match_mp_tac LLEX_not_WF
683 \\ qexists_tac`CHR 0`
684 \\ qexists_tac`CHR 1`
685 \\ simp[char_lt_def]
686QED
687
688Theorem INFINITE_STR_UNIV :
689 INFINITE univ(:string)
690Proof
691 SRW_TAC [][INFINITE_UNIV] THEN
692 Q.EXISTS_TAC `\st. STRING (CHR 0) st` THEN SRW_TAC [][] THEN
693 Q.EXISTS_TAC `""` THEN SRW_TAC [][]
694QED
695
696(*---------------------------------------------------------------------------
697 Exportation
698 ---------------------------------------------------------------------------*)
699
700val _ = let
701 val ^^ = Path.concat
702 infix ^^
703in
704 export_theory_as_docfiles ("help" ^^ "thms")
705end;