1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "../ReStar" "~~/src/HOL/Library/LaTeXsugar" |
3 imports "../ReStar" "~~/src/HOL/Library/LaTeXsugar" |
4 begin |
4 begin |
|
5 |
|
6 declare [[show_question_marks = false]] |
|
7 |
|
8 notation (latex output) |
|
9 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
|
10 Cons ("_::_" [78,77] 73) and |
|
11 val.Char ("Char _" [1000] 78) and |
|
12 val.Left ("Left _" [1000] 78) and |
|
13 val.Right ("Right _" [1000] 78) and |
|
14 L ("L _" [1000] 0) and |
|
15 flat ("|_|" [70] 73) and |
|
16 Sequ ("_ @ _" [78,77] 63) and |
|
17 injval ("inj _ _ _" [1000,77,1000] 77) and |
|
18 length ("len _" [78] 73) and |
|
19 ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) |
5 (*>*) |
20 (*>*) |
6 |
21 |
7 section {* Introduction *} |
22 section {* Introduction *} |
8 |
23 |
9 |
24 text {* |
|
25 |
|
26 \noindent |
|
27 Regular exprtessions |
|
28 |
|
29 \begin{center} |
|
30 @{text "r :="} |
|
31 @{const "NULL"} $\mid$ |
|
32 @{const "EMPTY"} $\mid$ |
|
33 @{term "CHAR c"} $\mid$ |
|
34 @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$ |
|
35 @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$ |
|
36 @{term "STAR r"} |
|
37 \end{center} |
|
38 |
|
39 \noindent |
|
40 Values |
|
41 |
|
42 \begin{center} |
|
43 @{text "v :="} |
|
44 @{const "Void"} $\mid$ |
|
45 @{term "val.Char c"} $\mid$ |
|
46 @{term "Left v"} $\mid$ |
|
47 @{term "Right v"} $\mid$ |
|
48 @{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$ |
|
49 @{term "Stars vs"} |
|
50 \end{center} |
|
51 |
|
52 \noindent |
|
53 The language of a regular expression |
|
54 |
|
55 \begin{center} |
|
56 \begin{tabular}{lcl} |
|
57 @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\ |
|
58 @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\ |
|
59 @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\ |
|
60 @{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
61 @{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
62 @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\ |
|
63 \end{tabular} |
|
64 \end{center} |
|
65 |
|
66 \noindent |
|
67 The nullable function |
|
68 |
|
69 \begin{center} |
|
70 \begin{tabular}{lcl} |
|
71 @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\ |
|
72 @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\ |
|
73 @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\ |
|
74 @{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
75 @{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
76 @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\\ |
|
77 \end{tabular} |
|
78 \end{center} |
|
79 |
|
80 \noindent |
|
81 The derivative function for characters and strings |
|
82 |
|
83 \begin{center} |
|
84 \begin{tabular}{lcp{7.5cm}} |
|
85 @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\ |
|
86 @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\ |
|
87 @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\ |
|
88 @{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\ |
|
89 @{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\ |
|
90 @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}\medskip\\ |
|
91 |
|
92 @{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\ |
|
93 @{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\ |
|
94 \end{tabular} |
|
95 \end{center} |
|
96 |
|
97 \noindent |
|
98 The @{const flat} function for values |
|
99 |
|
100 \begin{center} |
|
101 \begin{tabular}{lcl} |
|
102 @{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\ |
|
103 @{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\ |
|
104 @{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\ |
|
105 @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}\\ |
|
106 @{thm (lhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ |
|
107 @{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\ |
|
108 @{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\ |
|
109 \end{tabular} |
|
110 \end{center} |
|
111 |
|
112 \noindent |
|
113 The @{const mkeps} function |
|
114 |
|
115 \begin{center} |
|
116 \begin{tabular}{lcl} |
|
117 @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\ |
|
118 @{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
119 @{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\ |
|
120 @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\ |
|
121 \end{tabular} |
|
122 \end{center} |
|
123 |
|
124 \noindent |
|
125 The @{text inj} function |
|
126 |
|
127 \begin{center} |
|
128 \begin{tabular}{lcl} |
|
129 @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ |
|
130 @{thm (lhs) injval.simps(2)} & $\dn$ & @{thm (rhs) injval.simps(2)}\\ |
|
131 @{thm (lhs) injval.simps(3)} & $\dn$ & @{thm (rhs) injval.simps(3)}\\ |
|
132 @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
|
133 @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
|
134 @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
|
135 @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
|
136 @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
|
137 & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
|
138 @{thm (lhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
|
139 & @{thm (rhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
|
140 @{thm (lhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ |
|
141 & @{thm (rhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
|
142 @{thm (lhs) injval.simps(9)[of "r" "c" "v" "vs"]} & $\dn$ |
|
143 & @{thm (rhs) injval.simps(9)[of "r" "c" "v" "vs"]}\\ |
|
144 \end{tabular} |
|
145 \end{center} |
|
146 |
|
147 \noindent |
|
148 The inhabitation relation: |
|
149 |
|
150 \begin{center} |
|
151 \begin{tabular}{c} |
|
152 @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\medskip\\ |
|
153 @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad |
|
154 @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\medskip\\ |
|
155 @{thm[mode=Axiom] Prf.intros(4)} \qquad |
|
156 @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\medskip\\ |
|
157 @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad |
|
158 @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}\medskip\\ |
|
159 \end{tabular} |
|
160 \end{center} |
|
161 |
|
162 \noindent |
|
163 We have also introduced a slightly restricted version of this relation |
|
164 where the last rule is restricted so that @{term "flat v \<noteq> []"}. |
|
165 This relation for \emph{non-problematic} is written @{term "\<Turnstile> v : r"}. |
|
166 \bigskip |
|
167 |
|
168 |
|
169 \noindent |
|
170 Our Posix relation @{term "s \<in> r \<rightarrow> v"} |
|
171 |
|
172 \begin{center} |
|
173 \begin{tabular}{c} |
|
174 @{thm[mode=Axiom] PMatch.intros(1)} \qquad |
|
175 @{thm[mode=Axiom] PMatch.intros(2)}\medskip\\ |
|
176 @{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\qquad |
|
177 @{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\medskip\\ |
|
178 \multicolumn{1}{p{5cm}}{@{thm[mode=Rule] PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}\medskip\\ |
|
179 @{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad |
|
180 @{thm[mode=Axiom] PMatch.intros(7)}\medskip\\ |
|
181 \end{tabular} |
|
182 \end{center} |
|
183 |
|
184 \noindent |
|
185 Our version of Sulzmann's ordering relation |
|
186 |
|
187 \begin{center} |
|
188 \begin{tabular}{c} |
|
189 @{thm[mode=Rule] ValOrd.intros(2)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'"]} \qquad |
|
190 @{thm[mode=Rule] ValOrd.intros(1)[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "v\<^sub>1" "r\<^sub>1"]}\medskip\\ |
|
191 @{thm[mode=Rule] ValOrd.intros(3)[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]} \qquad |
|
192 @{thm[mode=Rule] ValOrd.intros(4)[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\medskip\\ |
|
193 @{thm[mode=Rule] ValOrd.intros(5)[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "r\<^sub>1"]} \qquad |
|
194 @{thm[mode=Rule] ValOrd.intros(6)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "r\<^sub>2"]} \medskip\\ |
|
195 @{thm[mode=Axiom] ValOrd.intros(7)}\qquad |
|
196 @{thm[mode=Axiom] ValOrd.intros(8)[of "c"]}\medskip\\ |
|
197 @{thm[mode=Rule] ValOrd.intros(9)[of "v" "vs" "r"]}\qquad |
|
198 @{thm[mode=Rule] ValOrd.intros(10)[of "v" "vs" "r"]}\medskip\\ |
|
199 @{thm[mode=Rule] ValOrd.intros(11)[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\medskip\\ |
|
200 @{thm[mode=Rule] ValOrd.intros(12)[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\qquad |
|
201 @{thm[mode=Axiom] ValOrd.intros(13)[of "r"]}\medskip\\ |
|
202 \end{tabular} |
|
203 \end{center} |
|
204 *} |
|
205 |
|
206 text {* |
|
207 \noindent |
|
208 Some lemmas |
|
209 |
|
210 |
|
211 @{thm[mode=IfThen] mkeps_nullable} |
|
212 |
|
213 @{thm[mode=IfThen] mkeps_flat} |
|
214 |
|
215 \ldots |
|
216 *} |
|
217 |
10 |
218 |
11 text {* |
219 text {* |
12 %\noindent |
220 %\noindent |
13 %{\bf Acknowledgements:} |
221 %{\bf Acknowledgements:} |
14 %We are grateful for the comments we received from anonymous |
222 %We are grateful for the comments we received from anonymous |