125 The @{text inj} function |
125 The @{text inj} function |
126 |
126 |
127 \begin{center} |
127 \begin{center} |
128 \begin{tabular}{lcl} |
128 \begin{tabular}{lcl} |
129 @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ |
129 @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ |
130 @{thm (lhs) injval.simps(2)} & $\dn$ & @{thm (rhs) injval.simps(2)}\\ |
130 @{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
131 @{thm (lhs) injval.simps(3)} & $\dn$ & @{thm (rhs) injval.simps(3)}\\ |
131 @{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
132 @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & |
132 @{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
133 @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ |
133 @{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
134 @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & |
134 @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
135 @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
135 & @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
136 @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ |
136 @{thm (lhs) injval.simps(5)[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" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
137 & @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "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$ |
138 @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ |
139 & @{thm (rhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ |
139 & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
140 @{thm (lhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ |
140 @{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$ |
141 & @{thm (rhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ |
141 & @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\ |
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} |
142 \end{tabular} |
145 \end{center} |
143 \end{center} |
146 |
144 |
147 \noindent |
145 \noindent |
148 The inhabitation relation: |
146 The inhabitation relation: |
266 Things we have proved about our version of the Sulzmann ordering |
264 Things we have proved about our version of the Sulzmann ordering |
267 |
265 |
268 \begin{center} |
266 \begin{center} |
269 \begin{tabular}{c} |
267 \begin{tabular}{c} |
270 @{thm[mode=IfThen] ValOrd_refl[of "v" "r"]}\medskip\\ |
268 @{thm[mode=IfThen] ValOrd_refl[of "v" "r"]}\medskip\\ |
271 @{thm[mode=IfThen] ValOrd_total[of "v\<^sub>1" "r" "v\<^sub>2"]} |
269 %@ {thm[mode=IfThen] ValOrd_total[of "v\<^sub>1" "r" "v\<^sub>2"]} |
272 \end{tabular} |
270 \end{tabular} |
273 \end{center}\bigskip |
271 \end{center}\bigskip |
274 |
272 |
275 \noindent |
273 \noindent |
276 Things we like to prove, but cannot:\bigskip |
274 Things we like to prove, but cannot:\bigskip |
286 %We are grateful for the comments we received from anonymous |
284 %We are grateful for the comments we received from anonymous |
287 %referees. |
285 %referees. |
288 |
286 |
289 \bibliographystyle{plain} |
287 \bibliographystyle{plain} |
290 \bibliography{root} |
288 \bibliography{root} |
|
289 |
|
290 \section{Roy's Rules} |
|
291 |
|
292 \newcommand{\abs}[1]{\mid\!\! #1\!\! \mid} |
|
293 %%\newcommand{\mts}{\textit{``''} |
|
294 \newcommand{\tl}{\ \triangleleft\ } |
|
295 $$\inferrule[]{Void \tl \epsilon}{} |
|
296 \quad\quad |
|
297 \inferrule[]{Char\ c \tl Lit\ c}{} |
|
298 $$ |
|
299 $$\inferrule |
|
300 {v_1 \tl r_1} |
|
301 {Left\ v_1 \tl r_1 + r_2} |
|
302 \quad\quad |
|
303 \inferrule[] |
|
304 { v_2 \tl r_2 \\ \abs{v_2}\ \not\in\ L(r_1)} |
|
305 {Right\ v_2 \tl r_1 + r_2} |
|
306 $$ |
|
307 $$ |
|
308 \inferrule |
|
309 {v_1 \tl r_1\\ |
|
310 v_2 \tl r_2\\ |
|
311 s \in\ L(r_1\backslash\! \abs{v_1}) \ \land\ |
|
312 \abs{v_2}\!\backslash s\ \epsilon\ L(r_2) |
|
313 \ \Rightarrow\ s = [] |
|
314 } |
|
315 {(v_1, v_2) \tl r_1 \cdot r_2} |
|
316 $$ |
|
317 $$\inferrule |
|
318 { v \tl r \\ vs \tl r^* \\ \abs{v}\ \not=\ []} |
|
319 { (v :: vs) \tl r^* } |
|
320 \quad\quad |
|
321 \inferrule{} |
|
322 { [] \tl r^* } |
|
323 $$ |
|
324 |
291 *} |
325 *} |
292 |
326 |
293 |
327 |
294 (*<*) |
328 (*<*) |
295 end |
329 end |