| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Wed, 10 Feb 2016 17:38:29 +0000 | |
| changeset 101 | 7f4f8c34da95 |
| parent 100 | 8b919b3d753e |
| child 102 | 7f589bfecffa |
| permissions | -rw-r--r-- |
|
95
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
(*<*) |
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
theory Paper |
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
imports "../ReStar" "~~/src/HOL/Library/LaTeXsugar" |
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
begin |
|
97
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
5 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
6 |
declare [[show_question_marks = false]] |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
7 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
8 |
notation (latex output) |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
9 |
If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
10 |
Cons ("_::_" [78,77] 73) and
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
11 |
val.Char ("Char _" [1000] 78) and
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
12 |
val.Left ("Left _" [1000] 78) and
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
13 |
val.Right ("Right _" [1000] 78) and
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
14 |
L ("L _" [1000] 0) and
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
15 |
flat ("|_|" [70] 73) and
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
16 |
Sequ ("_ @ _" [78,77] 63) and
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
17 |
injval ("inj _ _ _" [1000,77,1000] 77) and
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
18 |
length ("len _" [78] 73) and
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
19 |
ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73)
|
|
95
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
20 |
(*>*) |
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
21 |
|
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
22 |
section {* Introduction *}
|
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
23 |
|
|
97
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
24 |
text {*
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
25 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
26 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
27 |
Regular exprtessions |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
28 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
29 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
30 |
@{text "r :="}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
31 |
@{const "NULL"} $\mid$
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
32 |
@{const "EMPTY"} $\mid$
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
33 |
@{term "CHAR c"} $\mid$
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
34 |
@{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
35 |
@{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
36 |
@{term "STAR r"}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
37 |
\end{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
38 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
39 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
40 |
Values |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
41 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
42 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
43 |
@{text "v :="}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
44 |
@{const "Void"} $\mid$
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
45 |
@{term "val.Char c"} $\mid$
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
46 |
@{term "Left v"} $\mid$
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
47 |
@{term "Right v"} $\mid$
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
48 |
@{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
49 |
@{term "Stars vs"}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
50 |
\end{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
51 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
52 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
53 |
The language of a regular expression |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
54 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
55 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
56 |
\begin{tabular}{lcl}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
57 |
@{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
58 |
@{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
59 |
@{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
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"]}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
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"]}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
62 |
@{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
63 |
\end{tabular}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
64 |
\end{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
65 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
66 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
67 |
The nullable function |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
68 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
69 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
70 |
\begin{tabular}{lcl}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
71 |
@{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
72 |
@{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
73 |
@{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
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"]}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
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"]}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
76 |
@{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
77 |
\end{tabular}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
78 |
\end{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
79 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
80 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
81 |
The derivative function for characters and strings |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
82 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
83 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
84 |
\begin{tabular}{lcp{7.5cm}}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
85 |
@{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
86 |
@{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
87 |
@{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
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"]}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
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"]}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
90 |
@{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
91 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
92 |
@{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
93 |
@{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
94 |
\end{tabular}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
95 |
\end{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
96 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
97 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
98 |
The @{const flat} function for values
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
99 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
100 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
101 |
\begin{tabular}{lcl}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
102 |
@{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
103 |
@{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
104 |
@{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
105 |
@{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
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"]}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
107 |
@{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
108 |
@{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
109 |
\end{tabular}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
110 |
\end{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
111 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
112 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
113 |
The @{const mkeps} function
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
114 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
115 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
116 |
\begin{tabular}{lcl}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
117 |
@{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
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"]}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
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"]}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
120 |
@{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
121 |
\end{tabular}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
122 |
\end{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
123 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
124 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
125 |
The @{text inj} function
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
126 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
127 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
128 |
\begin{tabular}{lcl}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
129 |
@{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
|
|
101
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
130 |
@{thm (lhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ &
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
131 |
@{thm (rhs) injval.simps(2)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
132 |
@{thm (lhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ &
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
133 |
@{thm (rhs) injval.simps(3)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
134 |
@{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
135 |
& @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
136 |
@{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
137 |
& @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
138 |
@{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
139 |
& @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
140 |
@{thm (lhs) injval.simps(7)[of "r" "c" "v" "vs"]} & $\dn$
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
141 |
& @{thm (rhs) injval.simps(7)[of "r" "c" "v" "vs"]}\\
|
|
97
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
142 |
\end{tabular}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
143 |
\end{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
144 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
145 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
146 |
The inhabitation relation: |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
147 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
148 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
149 |
\begin{tabular}{c}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
150 |
@{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
151 |
@{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
152 |
@{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
153 |
@{thm[mode=Axiom] Prf.intros(4)} \qquad
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
154 |
@{thm[mode=Axiom] Prf.intros(5)[of "c"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
155 |
@{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
156 |
@{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
157 |
\end{tabular}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
158 |
\end{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
159 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
160 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
161 |
We have also introduced a slightly restricted version of this relation |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
162 |
where the last rule is restricted so that @{term "flat v \<noteq> []"}.
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
163 |
This relation for \emph{non-problematic} is written @{term "\<Turnstile> v : r"}.
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
164 |
\bigskip |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
165 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
166 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
167 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
168 |
Our Posix relation @{term "s \<in> r \<rightarrow> v"}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
169 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
170 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
171 |
\begin{tabular}{c}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
172 |
@{thm[mode=Axiom] PMatch.intros(1)} \qquad
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
173 |
@{thm[mode=Axiom] PMatch.intros(2)}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
174 |
@{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\qquad
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
175 |
@{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
176 |
\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\\
|
|
100
8b919b3d753e
strengthened PMatch to get determ
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
99
diff
changeset
|
177 |
@{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}\medskip\\
|
|
97
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
178 |
@{thm[mode=Axiom] PMatch.intros(7)}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
179 |
\end{tabular}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
180 |
\end{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
181 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
182 |
\noindent |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
183 |
Our version of Sulzmann's ordering relation |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
184 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
185 |
\begin{center}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
186 |
\begin{tabular}{c}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
187 |
@{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
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
188 |
@{thm[mode=Rule] ValOrd.intros(1)[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "v\<^sub>1" "r\<^sub>1"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
189 |
@{thm[mode=Rule] ValOrd.intros(3)[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]} \qquad
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
190 |
@{thm[mode=Rule] ValOrd.intros(4)[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
191 |
@{thm[mode=Rule] ValOrd.intros(5)[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "r\<^sub>1"]} \qquad
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
192 |
@{thm[mode=Rule] ValOrd.intros(6)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "r\<^sub>2"]} \medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
193 |
@{thm[mode=Axiom] ValOrd.intros(7)}\qquad
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
194 |
@{thm[mode=Axiom] ValOrd.intros(8)[of "c"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
195 |
@{thm[mode=Rule] ValOrd.intros(9)[of "v" "vs" "r"]}\qquad
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
196 |
@{thm[mode=Rule] ValOrd.intros(10)[of "v" "vs" "r"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
197 |
@{thm[mode=Rule] ValOrd.intros(11)[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
198 |
@{thm[mode=Rule] ValOrd.intros(12)[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\qquad
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
199 |
@{thm[mode=Axiom] ValOrd.intros(13)[of "r"]}\medskip\\
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
200 |
\end{tabular}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
201 |
\end{center}
|
|
98
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
202 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
203 |
\noindent |
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
204 |
A prefix of a string s |
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
205 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
206 |
\begin{center}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
207 |
\begin{tabular}{c}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
208 |
@{thm prefix_def[of "s\<^sub>1" "s\<^sub>2"]}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
209 |
\end{tabular}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
210 |
\end{center}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
211 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
212 |
\noindent |
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
213 |
Values and non-problematic values |
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
214 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
215 |
\begin{center}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
216 |
\begin{tabular}{c}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
217 |
@{thm Values_def}\medskip\\
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
218 |
@{thm NValues_def}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
219 |
\end{tabular}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
220 |
\end{center}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
221 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
222 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
223 |
\noindent |
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
224 |
The point is that for a given @{text s} and @{text r} there are only finitely many
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
225 |
non-problematic values. |
|
97
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
226 |
*} |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
227 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
228 |
text {*
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
229 |
\noindent |
|
98
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
230 |
Some lemmas we have proved:\bigskip |
|
97
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
231 |
|
|
98
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
232 |
@{thm L_flat_Prf}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
233 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
234 |
@{thm L_flat_NPrf}
|
|
97
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
235 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
236 |
@{thm[mode=IfThen] mkeps_nullable}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
237 |
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
238 |
@{thm[mode=IfThen] mkeps_flat}
|
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
239 |
|
|
98
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
240 |
@{thm[mode=IfThen] v3}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
241 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
242 |
@{thm[mode=IfThen] v4}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
243 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
244 |
@{thm[mode=IfThen] PMatch_mkeps}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
245 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
246 |
@{thm[mode=IfThen] PMatch1(2)}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
247 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
248 |
@{thm[mode=IfThen] PMatch1N}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
249 |
|
|
100
8b919b3d753e
strengthened PMatch to get determ
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
99
diff
changeset
|
250 |
@{thm[mode=IfThen] PMatch_determ(1)[of "s" "r" "v\<^sub>1" "v\<^sub>2"]}
|
|
8b919b3d753e
strengthened PMatch to get determ
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
99
diff
changeset
|
251 |
|
|
8b919b3d753e
strengthened PMatch to get determ
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
99
diff
changeset
|
252 |
\medskip |
|
98
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
253 |
\noindent |
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
254 |
This is the main theorem that lets us prove that the algorithm is correct according to |
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
255 |
@{term "s \<in> r \<rightarrow> v"}:
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
256 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
257 |
@{thm[mode=IfThen] PMatch2}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
258 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
259 |
\mbox{}\bigskip
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
260 |
*} |
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
261 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
262 |
text {*
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
263 |
\noindent |
|
99
f76c250906d5
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
98
diff
changeset
|
264 |
Things we have proved about our version of the Sulzmann ordering |
|
f76c250906d5
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
98
diff
changeset
|
265 |
|
|
f76c250906d5
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
98
diff
changeset
|
266 |
\begin{center}
|
|
f76c250906d5
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
98
diff
changeset
|
267 |
\begin{tabular}{c}
|
|
f76c250906d5
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
98
diff
changeset
|
268 |
@{thm[mode=IfThen] ValOrd_refl[of "v" "r"]}\medskip\\
|
|
101
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
269 |
%@ {thm[mode=IfThen] ValOrd_total[of "v\<^sub>1" "r" "v\<^sub>2"]}
|
|
99
f76c250906d5
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
98
diff
changeset
|
270 |
\end{tabular}
|
|
f76c250906d5
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
98
diff
changeset
|
271 |
\end{center}\bigskip
|
|
f76c250906d5
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
98
diff
changeset
|
272 |
|
|
f76c250906d5
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
98
diff
changeset
|
273 |
\noindent |
|
98
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
274 |
Things we like to prove, but cannot:\bigskip |
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
275 |
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
276 |
If @{term "s \<in> r \<rightarrow> v\<^sub>1"}, @{term "\<turnstile> v\<^sub>2 : r"}, then @{term "v\<^sub>1 \<succ>r v\<^sub>2"}
|
|
8b4c8cdd0b51
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
97
diff
changeset
|
277 |
|
|
97
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
278 |
*} |
|
38696f516c6b
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
95
diff
changeset
|
279 |
|
|
95
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
280 |
|
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
281 |
text {*
|
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
282 |
%\noindent |
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
283 |
%{\bf Acknowledgements:}
|
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
284 |
%We are grateful for the comments we received from anonymous |
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
285 |
%referees. |
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
286 |
|
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
287 |
\bibliographystyle{plain}
|
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
288 |
\bibliography{root}
|
|
101
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
289 |
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
290 |
\section{Roy's Rules}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
291 |
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
292 |
\newcommand{\abs}[1]{\mid\!\! #1\!\! \mid}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
293 |
%%\newcommand{\mts}{\textit{``''}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
294 |
\newcommand{\tl}{\ \triangleleft\ }
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
295 |
$$\inferrule[]{Void \tl \epsilon}{}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
296 |
\quad\quad |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
297 |
\inferrule[]{Char\ c \tl Lit\ c}{}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
298 |
$$ |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
299 |
$$\inferrule |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
300 |
{v_1 \tl r_1}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
301 |
{Left\ v_1 \tl r_1 + r_2}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
302 |
\quad\quad |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
303 |
\inferrule[] |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
304 |
{ v_2 \tl r_2 \\ \abs{v_2}\ \not\in\ L(r_1)}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
305 |
{Right\ v_2 \tl r_1 + r_2}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
306 |
$$ |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
307 |
$$ |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
308 |
\inferrule |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
309 |
{v_1 \tl r_1\\
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
310 |
v_2 \tl r_2\\ |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
311 |
s \in\ L(r_1\backslash\! \abs{v_1}) \ \land\
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
312 |
\abs{v_2}\!\backslash s\ \epsilon\ L(r_2)
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
313 |
\ \Rightarrow\ s = [] |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
314 |
} |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
315 |
{(v_1, v_2) \tl r_1 \cdot r_2}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
316 |
$$ |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
317 |
$$\inferrule |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
318 |
{ v \tl r \\ vs \tl r^* \\ \abs{v}\ \not=\ []}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
319 |
{ (v :: vs) \tl r^* }
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
320 |
\quad\quad |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
321 |
\inferrule{}
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
322 |
{ [] \tl r^* }
|
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
323 |
$$ |
|
7f4f8c34da95
fixed inj function
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
100
diff
changeset
|
324 |
|
|
95
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
325 |
*} |
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
326 |
|
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
327 |
|
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
328 |
(*<*) |
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
329 |
end |
|
a33d3040bf7e
started a paper and moved cruft to Attic
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
330 |
(*>*) |