-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathregexpScript.sml
executable file
·166 lines (128 loc) · 5.4 KB
/
regexpScript.sml
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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
(* A theory about regular expressions *)
open HolKernel boolLib bossLib Parse
open stringTheory listTheory;
open pred_setTheory ;
val _ = new_theory "regexp";
val _ = Hol_datatype `symbol = TS of string| NTS of string`;
(* ??_ case in HOL? *)
(* ??using case construct in HOL *)
val isTmnlSym_def = Define `(isTmnlSym sym = (?s.sym = (TS s)))`;
(* val isTmnlSym_def = Define `isTmnlSym sym = case sym of (TS s) -> T
|| _ -> F`; *)
val isNonTmnlSym_def = Define `isNonTmnlSym sym = (?s.sym = (NTS s)) \/ F`;
val tmnlSym_def = Define `tmnlSym (TS tmnl) = tmnl`;
val nonTmnlSym_def = Define `nonTmnlSym (NTS ntmnl) = ntmnl`;
val nts2str = Define `nts2str (NTS s) = s`
val ts2str = Define `ts2str (TS s) = s`
val symToStr_def = Define `(symToStr (TS s) = s) /\ (symToStr (NTS s) = s)`;
val sym_r1a = store_thm ("sym_r1a",
``isTmnlSym e ==> ~ isNonTmnlSym e``,
SRW_TAC [] [isTmnlSym_def,isNonTmnlSym_def] THEN
Cases_on `e` THEN
METIS_TAC [isTmnlSym_def,isNonTmnlSym_def]
);
val sym_r1b = store_thm ("sym_r1b",
``~isTmnlSym e = isNonTmnlSym e``,
SRW_TAC [] [EQ_IMP_THM] THENL[
Cases_on `e` THENL[
METIS_TAC [isTmnlSym_def,isNonTmnlSym_def],
FULL_SIMP_TAC (srw_ss()) [isNonTmnlSym_def,isTmnlSym_def]],
Cases_on `e` THENL[
FULL_SIMP_TAC (srw_ss())[isTmnlSym_def,isNonTmnlSym_def],
FULL_SIMP_TAC (srw_ss()) [isNonTmnlSym_def,isTmnlSym_def]]
]);
val sym_r2 = store_thm ("sym_r2",
``isTmnlSym e ==> ~(?n.e=NTS n)``,
SRW_TAC [] [] THEN
Cases_on `e=NTS n` THEN
FULL_SIMP_TAC (srw_ss()) [isTmnlSym_def]
);
val sym_r3 = store_thm ("sym_r3",
``!v.EVERY isTmnlSym v ==> ~(?n s1 s2.(v=s1++[n]++s2) /\ isNonTmnlSym n)``,
SRW_TAC [] [] THEN
FULL_SIMP_TAC (srw_ss()) [EVERY_MEM]THEN
Cases_on `n` THENL[
SRW_TAC [] [isTmnlSym_def, isNonTmnlSym_def],
CCONTR_TAC THEN
FULL_SIMP_TAC (srw_ss()) [isTmnlSym_def,isNonTmnlSym_def] THEN
METIS_TAC [MEM_SPLIT_APPEND_last,isTmnlSym_def,isNonTmnlSym_def,sym_r1b,EQ_IMP_THM]]);
val sym_r3b = store_thm ("sym_r3b",
``!v.EVERY isNonTmnlSym v ==> ~(?n s1 s2.(v=s1++[n]++s2) /\ isTmnlSym n)``,
SRW_TAC [] [] THEN
FULL_SIMP_TAC (srw_ss()) [EVERY_MEM]THEN
Cases_on `n` THENL[
CCONTR_TAC THEN
FULL_SIMP_TAC (srw_ss()) [isTmnlSym_def,isNonTmnlSym_def] THEN
METIS_TAC [MEM_SPLIT_APPEND_last,isTmnlSym_def,isNonTmnlSym_def,sym_r1b,EQ_IMP_THM],
FULL_SIMP_TAC (srw_ss()) [isTmnlSym_def,isNonTmnlSym_def] THEN
METIS_TAC [isTmnlSym_def,isNonTmnlSym_def,sym_r1b,EQ_IMP_THM]]
);
val sym_r4 = store_thm ("sym_r4",
``!v.EVERY isTmnlSym v ==> ~(?n. MEM n v /\ ~isTmnlSym n)``,
SRW_TAC [] [] THEN
FULL_SIMP_TAC (srw_ss()) [EVERY_MEM] THEN
Cases_on `n` THEN
METIS_TAC [isTmnlSym_def,isNonTmnlSym_def,MEM]
);
val sym_r4b = store_thm ("sym_r4b",
``!v.~EVERY isTmnlSym v ==> (?n. MEM n v /\ isNonTmnlSym n)``,
REPEAT STRIP_TAC THEN
FULL_SIMP_TAC (srw_ss()) [EVERY_MEM,EXISTS_MEM] THEN
METIS_TAC [isTmnlSym_def,isNonTmnlSym_def,MEM,sym_r1b]
);
val sym_r5 = store_thm ("sym_r5",
``!v.~(?n s1 s2.(v=s1++[n]++s2) /\ isNonTmnlSym n) ==> EVERY isTmnlSym v``,
SRW_TAC [] [] THEN
FULL_SIMP_TAC (srw_ss()) [EVERY_MEM] THEN
SRW_TAC [] [] THEN
Cases_on `e` THENL[
SRW_TAC [] [isTmnlSym_def, isNonTmnlSym_def],
CCONTR_TAC THEN
FULL_SIMP_TAC (srw_ss()) [isTmnlSym_def,isNonTmnlSym_def] THEN
METIS_TAC [MEM_SPLIT_APPEND_last,isTmnlSym_def,isNonTmnlSym_def,sym_r1b,EQ_IMP_THM]]
);
val sym_r6 = store_thm ("sym_r6",
``!v.EVERY isTmnlSym v = (~(?n s1 s2.(v=s1++[n]++s2) /\ isNonTmnlSym n))``,
SRW_TAC [] [EQ_IMP_THM] THENL[
METIS_TAC [sym_r3], METIS_TAC [sym_r5]
]
);
val sym_r7 = store_thm ("sym_r7",
``!v.~(EVERY isTmnlSym v) ==> ?n s1 s2.(v=s1++[n]++s2) /\ isNonTmnlSym n``,
SRW_TAC [] [] THEN
FULL_SIMP_TAC (srw_ss()) [EXISTS_MEM,sym_r1b, Once MEM_SPLIT_APPEND_last] THEN
MAP_EVERY Q.EXISTS_TAC [`e`,`pfx`,`sfx`] THEN
SRW_TAC [] []
);
val sym_r7b = store_thm ("sym_r7b",
``!v.~(EVERY isNonTmnlSym v) ==> ?n s1 s2.(v=s1++[n]++s2) /\ isTmnlSym n``,
SRW_TAC [] [] THEN
FULL_SIMP_TAC (srw_ss()) [EXISTS_MEM,sym_r1b, Once MEM_SPLIT_APPEND_last] THEN
MAP_EVERY Q.EXISTS_TAC [`e`,`pfx`,`sfx`] THEN
METIS_TAC [sym_r1b]
);
(* Regular Expressions *)
(* Definition of a regexp *)
val _ = Hol_datatype `rexp = EmptyLang | Atom of symbol | Union of rexp => rexp | Conc of rexp => rexp | Star of rexp`;
(* Concatenation *)
(* conc :: a list set => a list set => a list set
val conc_def = Define `(conc [] (b::bs) = (b::bs)) /\ (conc (a::as) (b::bs) = (MAP (STRCAT a) (b::bs)) ++ (conc as (b::bs)))`;
*)
val conc_def = Define `conc as bs = {s | ?u v. u IN as /\ v IN bs /\ (s = u ++ v)}`;
(* Union *)
val union_def = Define `union as bs = {s | s IN as \/ s IN bs}`;
(*
Star
(defined inductively)
star :: a list set => a list set
[] <- star A
a <- A and as <- star A => a++as <- star A
*)
val starn_def = Define `(starn l 0 = {[]}) /\ (starn l n = {s | ?u v. u IN l /\ v IN (starn l (n-1)) /\ (s = u ++ v)})`;
(* Define A* + prove alternate defn of * *)
val (star_rules, star_ind, star_cases) = Hol_reln` (star A []) /\ (!s. s IN A ==> star A s) /\ (!s1 s2. s1 IN A /\ s2 IN A ==> star A (s1 ++ s2))`;
(* Language denoted by a rexp *)
(* lang :: a rexp => a list set *)
(* Includes nonterms as well *)
val lang_def = Define `(lang EmptyLang = {}) /\ (lang (Atom tmnl) = {[symToStr tmnl]}) /\ (lang (Union r s) = lang r UNION lang s) /\ (lang (Conc r s) = conc (lang r) (lang s)) /\ (lang (Star r) = star (lang r))`;
val _ = export_theory ();