lexing: thys/Paper/Paper.thy@6adda4a667b1 (annotated)

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
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	10	Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [78,77] 73) and
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	11	ZERO ("\<^raw:\textrm{0}>" 78) and
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	12	ONE ("\<^raw:\textrm{1}>" 78) and
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	13	CHAR ("_" [1000] 10) and
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	14	ALT ("_ + _" [1000,1000] 78) and
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	15	SEQ ("_ \<cdot> _" [1000,1000] 78) and
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	16	STAR ("_\<^sup>\<star>" [1000] 78) and
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	17	val.Char ("Char _" [1000] 78) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	18	val.Left ("Left _" [1000] 78) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	19	val.Right ("Right _" [1000] 78) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	20	L ("L _" [1000] 0) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	21	flat ("\|_\|" [70] 73) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	22	Sequ ("_ @ _" [78,77] 63) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	23	injval ("inj _ _ _" [1000,77,1000] 77) and
102 7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	24	projval ("proj _ _ _" [1000,77,1000] 77) and
105 80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 103 diff changeset	25	length ("len _" [78] 73)
80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 103 diff changeset	26	(* and 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	27	(>)
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	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	30
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	31	text {*
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	32
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	33
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	34	Sulzmann and Lu \cite{Sulzmann2014}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	35
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	36	there are two commonly used
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	37	disambiguation strategies to create a unique matching tree:
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	38	one is called \emph{greedy} matching \cite{Frisch2004} and the
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	39	other is \emph{POSIX} matching~\cite{Kuklewicz,Sulzmann2014}.
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	40	For the latter there are two rough rules:
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	41
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	42	\begin{itemize}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	43	\item The Longest Match Rule (or ``maximal munch rule''):\smallskip\\ The
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	44	longest initial substring matched by any regular
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	45	expression is taken as next token.
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	46
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	47	\item Rule Priority:\smallskip\\ For a particular longest initial
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	48	substring, the first regular expression that can match
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	49	determines the token.
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	50	\end{itemize}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	51
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	52	\noindent In the context of lexing, POSIX is the more
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	53	interesting disambiguation strategy as it produces longest
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	54	matches, which is necessary for tokenising programs. For
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	55	example the string \textit{iffoo} should not match the keyword
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	56	\textit{if} and the rest, but as one string \textit{iffoo},
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	57	which might be a variable name in a program. As another
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	58	example consider the string $xy$ and the regular expression
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	59	\mbox{$(x + y + xy)^*$}. Either the input string can be
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	60	matched in two `iterations' by the single letter-regular
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	61	expressions $x$ and $y$, or directly in one iteration by $xy$.
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	62	The first case corresponds to greedy matching, which first
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	63	matches with the left-most symbol and only matches the next
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	64	symbol in case of a mismatch. The second case is POSIX
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	65	matching, which prefers the longest match. In case more than
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	66	one (longest) matches exist, only then it prefers the
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	67	left-most match. While POSIX matching seems natural, it turns
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	68	out to be much more subtle than greedy matching in terms of
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	69	implementations and in terms of proving properties about it.
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	70	If POSIX matching is implemented using automata, then one has
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	71	to follow transitions (according to the input string) until
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	72	one finds an accepting state, record this state and look for
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	73	further transition which might lead to another accepting state
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	74	that represents a longer input initial substring to be
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	75	matched. Only if none can be found, the last accepting state
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	76	is returned.
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	77
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	78
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	79	Sulzmann and Lu's paper \cite{Sulzmann2014} targets POSIX
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	80	regular expression matching. They write that it is known to be
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	81	to be a non-trivial problem and nearly all POSIX matching
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	82	implementations are ``buggy'' \cite[Page 203]{Sulzmann2014}.
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	83	For this they cite a study by Kuklewicz \cite{Kuklewicz}. My
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	84	current work is about formalising the proofs in the paper by
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	85	Sulzmann and Lu. Specifically, they propose in this paper a
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	86	POSIX matching algorithm and give some details of a
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	87	correctness proof for this algorithm inside the paper and some
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	88	more details in an appendix. This correctness proof is
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	89	unformalised, meaning it is just a ``pencil-and-paper'' proof,
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	90	not done in a theorem prover. Though, the paper and presumably
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	91	the proof have been peer-reviewed. Unfortunately their proof
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	92	does not give enough details such that it can be
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	93	straightforwardly implemented in a theorem prover, say
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	94	Isabelle. In fact, the purported proof they outline does not
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	95	work in central places. We discovered this when filling in
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	96	many gaps and attempting to formalise the proof in Isabelle.
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	97
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	98
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	99
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	100	{\bf Contributions:}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	101
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	102	*}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	103
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	104	section {* Preliminaries *}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	105
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	106	text {* \noindent Strings in Isabelle/HOL are lists of characters with
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	107	the empty string being represented by the empty list, written @{term
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	108	"[]"}, and list-cons being written as @{term "DUMMY # DUMMY"}. By
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	109	using the type char we have a supply of finitely many characters
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	110	roughly corresponding to the ASCII character set.
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	111	Regular exprtessions
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	112
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	113	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	114	@{text "r :="}
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	115	@{const "ZERO"} $\mid$
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	116	@{const "ONE"} $\mid$
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	117	@{term "CHAR c"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	118	@{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	119	@{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	120	@{term "STAR r"}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	121	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	122
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	123	*}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	124
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	125	section {* POSIX Regular Expression Matching *}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	126
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	127	section {* The Argument by Sulzmmann and Lu *}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	128
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	129	section {* Conclusion *}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	130
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	131	text {*
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	132
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	133	Nipkow lexer from 2000
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	134
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	135	*}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	136
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	137
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	138	text {*
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	139
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	140
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	141
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	142
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	143	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	144	Values
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	145
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	146	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	147	@{text "v :="}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	148	@{const "Void"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	149	@{term "val.Char c"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	150	@{term "Left v"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	151	@{term "Right v"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	152	@{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	153	@{term "Stars vs"}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	154	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	155
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	156	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	157	The language of a regular expression
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	158
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	159	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	160	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	161	@{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	162	@{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	163	@{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	164	@{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	165	@{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	166	@{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	167	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	168	\end{center}
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	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	171	The nullable function
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	172
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	173	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	174	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	175	@{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	176	@{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	177	@{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	178	@{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	179	@{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	180	@{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	181	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	182	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	183
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	184	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	185	The derivative function for characters and strings
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	186
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	187	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	188	\begin{tabular}{lcp{7.5cm}}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	189	@{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	190	@{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	191	@{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	192	@{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	193	@{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	194	@{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	195
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	196	@{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	197	@{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	198	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	199	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	200
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	201	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	202	The @{const flat} function for values
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	203
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	204	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	205	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	206	@{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	207	@{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	208	@{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	209	@{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	210	@{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	211	@{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	212	@{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	213	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	214	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	215
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	216	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	217	The @{const mkeps} function
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	218
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	219	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	220	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	221	@{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	222	@{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	223	@{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	224	@{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	225	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	226	\end{center}
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	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	229	The @{text inj} function
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	230
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	231	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	232	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	233	@{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	234	@{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	235	@{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	236	@{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	237	@{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	238	@{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	239	& @{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	240	@{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	241	& @{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	242	@{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	243	& @{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	244	@{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	245	& @{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	246	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	247	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	248
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	249	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	250	The inhabitation relation:
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	251
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	252	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	253	\begin{tabular}{c}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	254	@{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	255	@{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	256	@{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	257	@{thm[mode=Axiom] Prf.intros(4)} \qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	258	@{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	259	@{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	260	@{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	261	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	262	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	263
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	264	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	265	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	266	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	267	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	268	\bigskip
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	269
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	270
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	271	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	272	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	273
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	274	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	275	\begin{tabular}{c}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	276	@{thm[mode=Axiom] PMatch.intros(1)} \qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	277	@{thm[mode=Axiom] PMatch.intros(2)}\medskip\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	278	@{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	279	@{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	280	\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	281	@{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	282	@{thm[mode=Axiom] PMatch.intros(7)}\medskip\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	283	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	284	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	285
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	286	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	287	Our version of Sulzmann's ordering relation
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	288
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	289	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	290	\begin{tabular}{c}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	291	@{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	292	@{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	293	@{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	294	@{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	295	@{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	296	@{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	297	@{thm[mode=Axiom] ValOrd.intros(7)}\qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	298	@{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	299	@{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	300	@{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	301	@{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	302	@{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	303	@{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	304	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	305	\end{center}
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	306
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	307	\noindent
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	308	A prefix of a string s
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	309
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	310	\begin{center}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	311	\begin{tabular}{c}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	312	@{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	313	\end{tabular}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	314	\end{center}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	315
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	316	\noindent
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	317	Values and non-problematic values
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	318
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	319	\begin{center}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	320	\begin{tabular}{c}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	321	@{thm Values_def}\medskip\\
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	322	\end{tabular}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	323	\end{center}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	324
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	325
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	326	\noindent
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	327	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	328	non-problematic values.
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	329	*}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	330
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	331	text {*
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	332	\noindent
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	333	Some lemmas we have proved:\bigskip
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	334
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	335	@{thm L_flat_Prf}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	336
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	337	@{thm L_flat_NPrf}
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	338
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	339	@{thm[mode=IfThen] mkeps_nullable}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	340
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	341	@{thm[mode=IfThen] mkeps_flat}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	342
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	343	@{thm[mode=IfThen] Prf_injval}
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	344
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	345	@{thm[mode=IfThen] Prf_injval_flat}
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	346
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	347	@{thm[mode=IfThen] PMatch_mkeps}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	348
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	349	@{thm[mode=IfThen] PMatch1(2)}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	350
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	351	@{thm[mode=IfThen] PMatch1N}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	352
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	353	@{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	354
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	355	\medskip
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	356	\noindent
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	357	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	358	@{term "s \<in> r \<rightarrow> v"}:
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	359
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	360	@{thm[mode=IfThen] PMatch2}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	361
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	362	\mbox{}\bigskip
102 7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	363
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	364	\noindent {\bf Proof} The proof is by induction on the definition of
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	365	@{const der}. Other inductions would go through as well. The
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	366	interesting case is for @{term "SEQ r\<^sub>1 r\<^sub>2"}. First we analyse the
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	367	case where @{term "nullable r\<^sub>1"}. We have by induction hypothesis
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	368
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	369	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	370	\begin{array}{l}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	371	(IH1)\quad @{text "\<forall>s v."} \text{\;if\;} @{term "s \<in> der c r\<^sub>1 \<rightarrow> v"}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	372	\text{\;then\;} @{term "(c # s) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v"}\\
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	373	(IH2)\quad @{text "\<forall>s v."} \text{\;if\;} @{term "s \<in> der c r\<^sub>2 \<rightarrow> v"}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	374	\text{\;then\;} @{term "(c # s) \<in> r\<^sub>2 \<rightarrow> injval r\<^sub>2 c v"}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	375	\end{array}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	376	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	377
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	378	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	379	and have
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	380
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	381	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	382	@{term "s \<in> ALT (SEQ (der c r\<^sub>1) r\<^sub>2) (der c r\<^sub>2) \<rightarrow> v"}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	383	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	384
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	385	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	386	There are two cases what @{term v} can be: (1) @{term "Left v'"} and (2) @{term "Right v'"}.
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	387
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	388	\begin{itemize}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	389	\item[(1)] We know @{term "s \<in> SEQ (der c r\<^sub>1) r\<^sub>2 \<rightarrow> v'"} holds, from which we
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	390	can infer that there are @{text "s\<^sub>1"}, @{term "s\<^sub>2"}, @{text "v\<^sub>1"}, @{term "v\<^sub>2"}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	391	with
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	392
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	393	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	394	@{term "s\<^sub>1 \<in> der c r\<^sub>1 \<rightarrow> v\<^sub>1"} \qquad\text{and}\qquad @{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	395	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	396
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	397	and also
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	398
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	399	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	400	@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) \<and> s\<^sub>4 \<in> L r\<^sub>2)"}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	401	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	402
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	403	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	404	and have to prove
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	405
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	406	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	407	@{term "((c # s\<^sub>1) @ s\<^sub>2) \<in> SEQ r\<^sub>1 r\<^sub>2 \<rightarrow> Seq (injval r\<^sub>1 c v\<^sub>1) v\<^sub>2"}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	408	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	409
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	410	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	411	The two requirements @{term "(c # s\<^sub>1) \<in> r\<^sub>1 \<rightarrow> injval r\<^sub>1 c v\<^sub>1"} and
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	412	@{term "s\<^sub>2 \<in> r\<^sub>2 \<rightarrow> v\<^sub>2"} can be proved by the induction hypothese (IH1) and the
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	413	fact above.
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	414
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	415	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	416	This leaves to prove
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	417
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	418	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	419	@{term "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s\<^sub>2 \<and> (c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 \<and> s\<^sub>4 \<in> L r\<^sub>2)"}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	420	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	421
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	422	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	423	which holds because @{term "(c # s\<^sub>1) @ s\<^sub>3 \<in> L r\<^sub>1 "} implies @{term "s\<^sub>1 @ s\<^sub>3 \<in> L (der c r\<^sub>1) "}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	424
103 ffe5d850df62 added some slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 102 diff changeset	425	\item[(2)] This case is similar.
102 7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	426	\end{itemize}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	427
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	428	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	429	The final case is that @{term " \<not> nullable r\<^sub>1"} holds. This case again similar
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	430	to the cases above.
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	431	*}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	432
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	433
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	434	text {*
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	435	%\noindent
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	436	%{\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	437	%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	438	%referees.
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	439
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	440	\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	441	\bibliography{root}
101 7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	442
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	443	\section{Roy's Rules}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	444
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	445	\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	446	%%\newcommand{\mts}{\textit{``''}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	447	\newcommand{\tl}{\ \triangleleft\ }
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	448	$$\inferrule[]{Void \tl \epsilon}{}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	449	\quad\quad
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	450	\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	451	$$
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	452	$$\inferrule
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	453	{v_1 \tl r_1}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	454	{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	455	\quad\quad
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	456	\inferrule[]
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	457	{ 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	458	{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	459	$$
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	460	$$
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	461	\inferrule
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	462	{v_1 \tl r_1\\
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	463	v_2 \tl r_2\\
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	464	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	465	\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	466	\ \Rightarrow\ s = []
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	467	}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	468	{(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	469	$$
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	470	$$\inferrule
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	471	{ 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	472	{ (v :: vs) \tl r^* }
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	473	\quad\quad
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	474	\inferrule{}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	475	{ [] \tl r^* }
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	476	$$
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	477
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	478	*}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	479
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	480
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	481	(<)
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	482	end
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	483	(>)

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Sun, 28 Feb 2016 14:01:12 +0000
changeset 107	6adda4a667b1
parent 105	80218dddbb15
child 108	73f7dc60c285
permissions	-rw-r--r--