lexing: thys/Paper/Paper.thy@2c38f10643ae (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
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	8	abbreviation
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	9	"der_syn r c \<equiv> der c r"
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	10
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	11	notation (latex output)
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	12	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	13	Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [78,77] 73) and
109 2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	14	ZERO ("\<^bold>0" 80) and
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	15	ONE ("\<^bold>1" 80) and
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	16	CHAR ("_" [1000] 80) and
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	17	ALT ("_ + _" [77,77] 78) and
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	18	SEQ ("_ \<cdot> _" [77,77] 78) and
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	19	STAR ("_\<^sup>\<star>" [1000] 78) and
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	20	val.Char ("Char _" [1000] 78) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	21	val.Left ("Left _" [1000] 78) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	22	val.Right ("Right _" [1000] 78) and
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	23	L ("L'(_')" [10] 78) and
109 2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	24	der_syn ("_\\_" [79, 1000] 76) and
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	25	flat ("\|_\|" [70] 73) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	26	Sequ ("_ @ _" [78,77] 63) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	27	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	28	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	29	length ("len _" [78] 73)
80218dddbb15 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 103 diff changeset	30	(* 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	31	(>)
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	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	34
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	35	text {*
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	36
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	37	Brzozowski \cite{Brzozowski1964} introduced the notion of the {\em
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	38	derivative} @{term "der c r"} of a regular expression @{text r} w.r.t.\ a
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	39	character~@{text c}, and showed that it gave a simple solution to the
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	40	problem of matching a string @{term s} with a regular expression @{term r}:
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	41	if the derivative of @{term r} w.r.t.\ (in succession) all the characters of
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	42	the string matches the empty string $\mts$, then @{term r} matches @{term s}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	43	(and {\em vice versa}). The derivative has the property (which may be
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	44	regarded as its specification) that, for every string @{term s} and regular
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	45	expression @{term r} and character @{term c}, one has @{term "cs \<in> L(r)"} if
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	46	and only if \mbox{@{term "s \<in> L(der c r)"}}. The beauty of Brzozowski's
109 2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	47	derivatives is that they are neatly expressible in any functional language,
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	48	and easily definable and reasoned about in theorem provers---the definitions
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	49	just consist of inductive datatypes and simple recursive functions. A
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	50	completely formalised correctness proof of this matcher in for example HOL4
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	51	has been given in~\cite{Owens2008}.
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	52
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	53	One limitation of Brzozowski's matcher is that it only generates a YES/NO
109 2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	54	answer for whether a string is being matched by a regular expression.
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	55	Sulzmann and Lu \cite{Sulzmann2014} extended this matcher to allow
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	56	generation not just of a YES/NO answer but of an actual matching, called a
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	57	[lexical] {\em value}. They give a simple algorithm to calculate a value
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	58	that appears to be the value associated with POSIX lexing
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	59	\cite{Kuklewicz,Vansummeren2006}. The challenge then is to specify that
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	60	value, in an algorithm-independent fashion, and to show that Sulzamann and
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	61	Lu's derivative-based algorithm does indeed calculate a value that is
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	62	correct according to the specification.
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	63
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	64	The answer given by Sulzmann and Lu \cite{Sulzmann2014} is to define a
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	65	relation (called an ``Order Relation'') on the set of values of @{term r},
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	66	and to show that (once a string to be matched is chosen) there is a maximum
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	67	element and that it is computed by their derivative-based algorithm. This
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	68	proof idea is inspired by work of Frisch and Cardelli \cite{Frisch2004} on a
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	69	GREEDY regular expression matching algorithm. Beginning with our
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	70	observations that, without evidence that it is transitive, it cannot be
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	71	called an ``order relation'', and that the relation is called a ``total
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	72	order'' despite being evidently not total\footnote{\textcolor{green}{We
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	73	should give an argument as footnote}}, we identify problems with this
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	74	approach (of which some of the proofs are not published in
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	75	\cite{Sulzmann2014}); perhaps more importantly, we give a simple inductive
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	76	(and algorithm-independent) definition of what we call being a {\em POSIX
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	77	value} for a regular expression @{term r} and a string @{term s}; we show
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	78	that the algorithm computes such a value and that such a value is unique.
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	79	Proofs are both done by hand and checked in {\em Isabelle/HOL}. The
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	80	experience of doing our proofs has been that this mechanical checking was
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	81	absolutely essential: this subject area has hidden snares. This was also
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	82	noted by Kuklewitz \cite{Kuklewicz} who found that nearly all POSIX matching
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	83	implementations are ``buggy'' \cite[Page 203]{Sulzmann2014}.
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	84
109 2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	85	If a regular expression matches a string, then in general there are more
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	86	than one possibility of how the string is matched. There are two commonly
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	87	used disambiguation strategies to generate a unique answer: one is called
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	88	GREEDY matching \cite{Frisch2004} and the other is POSIX
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	89	matching~\cite{Kuklewicz,Sulzmann2014}. For example consider the string
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	90	@{term xy} and the regular expression @{term "STAR (ALT (ALT x y) xy)"}.
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	91	Either the string can be matched in two `iterations' by the single
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	92	letter-regular expressions @{term x} and @{term y}, or directly in one
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	93	iteration by @{term xy}. The first case corresponds to GREEDY matching,
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	94	which first matches with the left-most symbol and only matches the next
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	95	symbol in case of a mismatch. The second case is POSIX matching, which
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	96	prefers the longest match.
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	97
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	98	In the context of lexing, where an input string is separated into a sequence
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	99	of tokens, POSIX is the more natural disambiguation strategy for what
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	100	programmers consider basic syntactic building blocks in their programs.
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	101	There are two underlying rules behind tokenising using POSIX matching:
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	102
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	103	\begin{itemize}
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	104	\item[$\bullet$] \underline{The Longest Match Rule (or ``maximal munch rule''):}
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	105
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	106	The longest initial substring matched by any regular expression is taken as
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	107	next token.\smallskip
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	108
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	109	\item[$\bullet$] \underline{Rule Priority:}
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	110
109 2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	111	For a particular longest initial substring, the first regular expression
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	112	that can match determines the token.
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	113	\end{itemize}
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	114
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	115	\noindent Consider for example a regular expression @{text
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	116	"r\<^bsub>key\<^esub>"} that can recognise keywords, like @{text "if"},
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	117	@{text "then"} and so on; and another regular expression @{text
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	118	"r\<^bsub>id\<^esub>"} that can recognise identifiers (such as single
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	119	characters followed by characters or numbers). Then we can form the regular
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	120	expression @{text "(r\<^bsub>key\<^esub> + r\<^bsub>id\<^esub>)\<^sup>\<star>"} and
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	121	use POSIX matching to, for example, tokenise the strings @{text "iffoo"} and
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	122	@{text "if"}. In the first case we obtain by the longest match rule a
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	123	single identifier token, not a keyword and identifier. In the second case we
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	124	obtain by rule priority a keyword token, not an identifier token.
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	125	\bigskip
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	126
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	127	\noindent\textcolor{green}{Not Done Yet}
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	128
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	129
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	130	\medskip\noindent
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	131	{\bf Contributions:}
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	132
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	133	Derivatives as calculated by Brzozowski's method are usually more complex
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	134	regular expressions than the initial one; various optimisations are
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	135	possible, such as the simplifications of @{term "ALT ZERO r"}, @{term "ALT r
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	136	ZERO"}, @{term "SEQ ONE r"} and @{term "SEQ r ONE"} to @{term r}. One of the
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	137	advantages of having a simple specification and correctness proof is that
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	138	the latter can be refined to allow for such optimisations and simple
2c38f10643ae updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 108 diff changeset	139	correctness proof.
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	140
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	141	An extended version of \cite{Sulzmann2014} is available at the website
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	142	of its first author; this includes some ``proofs'', claimed in
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	143	\cite{Sulzmann2014} to be ``rigorous''. Since these are evidently not in
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	144	final form, we make no comment thereon, preferring to give general
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	145	reasons for our belief that the approach of \cite{Sulzmann2014} is
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	146	problematic rather than to discuss details of unpublished work.
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	147
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	148
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	149	*}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	150
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	151	section {* Preliminaries *}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	152
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	153	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	154	the empty string being represented by the empty list, written @{term
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	155	"[]"}, and list-cons being written as @{term "DUMMY # DUMMY"}.
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	156	Often we use the usual bracket notation for strings; for example a
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	157	string consiting of a single character is written @{term "[c]"}. By
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	158	using the type @{type char} for characters we have a supply of
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	159	finitely many characters roughly corresponding to the ASCII
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	160	character set. Regular expression are as usual and defined as the
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	161	following inductive datatype:
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	162
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	163	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	164	@{text "r :="}
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	165	@{const "ZERO"} $\mid$
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	166	@{const "ONE"} $\mid$
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	167	@{term "CHAR c"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	168	@{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	169	@{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	170	@{term "STAR r"}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	171	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	172
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	173	\noindent where @{const ZERO} stands for the regular expression that
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	174	does not macth any string and @{const ONE} for the regular
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	175	expression that matches only the empty string. The language of a regular expression
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	176	is again defined as usual by the following clauses
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	177
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	178	\begin{center}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	179	\begin{tabular}{rcl}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	180	@{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	181	@{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	182	@{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	183	@{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"]}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	184	@{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"]}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	185	@{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	186	\end{tabular}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	187	\end{center}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	188
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	189	\noindent We use the star-notation for regular expressions and sets of strings.
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	190	The Kleene-star on sets is defined inductively.
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	191
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	192	\emph{Semantic derivatives} of sets of strings are defined as
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	193
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	194	\begin{center}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	195	\begin{tabular}{lcl}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	196	@{thm (lhs) Der_def} & $\dn$ & @{thm (rhs) Der_def}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	197	@{thm (lhs) Ders_def} & $\dn$ & @{thm (rhs) Ders_def}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	198	\end{tabular}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	199	\end{center}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	200
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	201	\noindent where the second definitions lifts the notion of semantic
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	202	derivatives from characters to strings.
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	203
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	204	\noindent
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	205	The nullable function
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	206
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	207	\begin{center}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	208	\begin{tabular}{lcl}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	209	@{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	210	@{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	211	@{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	212	@{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"]}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	213	@{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"]}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	214	@{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	215	\end{tabular}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	216	\end{center}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	217
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	218	\noindent
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	219	The derivative function for characters and strings
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	220
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	221	\begin{center}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	222	\begin{tabular}{lcp{7.5cm}}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	223	@{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	224	@{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	225	@{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	226	@{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"]}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	227	@{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"]}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	228	@{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}\medskip\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	229
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	230	@{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	231	@{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	232	\end{tabular}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	233	\end{center}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	234
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	235	It is a relatively easy exercise to prove that
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	236
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	237	\begin{center}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	238	\begin{tabular}{l}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	239	@{thm[mode=IfThen] nullable_correctness}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	240	@{thm[mode=IfThen] der_correctness}\\
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	241	\end{tabular}
73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	242	\end{center}
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	243	*}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	244
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	245	section {* POSIX Regular Expression Matching *}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	246
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	247	section {* The Argument by Sulzmmann and Lu *}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	248
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	249	section {* Conclusion *}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	250
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	251	text {*
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	252
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	253	Nipkow lexer from 2000
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	254
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	255	*}
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	256
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	257
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	258	text {*
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	259
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	260
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	261
6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	262
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	263	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	264	Values
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	265
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	266	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	267	@{text "v :="}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	268	@{const "Void"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	269	@{term "val.Char c"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	270	@{term "Left v"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	271	@{term "Right v"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	272	@{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	273	@{term "Stars vs"}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	274	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	275
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	276	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	277	The language of a regular expression
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	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	280	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	281	@{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	282	@{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	283	@{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	284	@{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	285	@{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	286	@{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	287	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	288	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	289
108 73f7dc60c285 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 107 diff changeset	290
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	291
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	292	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	293	The @{const flat} function for values
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	294
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	295	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	296	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	297	@{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	298	@{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	299	@{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	300	@{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	301	@{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	302	@{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	303	@{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	304	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	305	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	306
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	307	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	308	The @{const mkeps} function
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	309
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	310	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	311	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	312	@{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	313	@{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	314	@{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	315	@{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	316	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	317	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	318
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	319	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	320	The @{text inj} function
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	321
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	322	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	323	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	324	@{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	325	@{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	326	@{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	327	@{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	328	@{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	329	@{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	330	& @{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	331	@{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	332	& @{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	333	@{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	334	& @{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	335	@{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	336	& @{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	337	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	338	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	339
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	340	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	341	The inhabitation relation:
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	342
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	343	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	344	\begin{tabular}{c}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	345	@{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	346	@{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	347	@{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	348	@{thm[mode=Axiom] Prf.intros(4)} \qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	349	@{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	350	@{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	351	@{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	352	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	353	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	354
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	355	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	356	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	357	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	358	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	359	\bigskip
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	360
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	361
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	362	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	363	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	364
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	365	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	366	\begin{tabular}{c}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	367	@{thm[mode=Axiom] PMatch.intros(1)} \qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	368	@{thm[mode=Axiom] PMatch.intros(2)}\medskip\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	369	@{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	370	@{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	371	\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	372	@{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	373	@{thm[mode=Axiom] PMatch.intros(7)}\medskip\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	374	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	375	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	376
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	377	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	378	Our version of Sulzmann's ordering relation
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	379
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	380	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	381	\begin{tabular}{c}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	382	@{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	383	@{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	384	@{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	385	@{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	386	@{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	387	@{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	388	@{thm[mode=Axiom] ValOrd.intros(7)}\qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	389	@{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	390	@{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	391	@{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	392	@{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	393	@{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	394	@{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	395	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	396	\end{center}
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	397
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	398	\noindent
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	399	A prefix of a string s
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	400
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	401	\begin{center}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	402	\begin{tabular}{c}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	403	@{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	404	\end{tabular}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	405	\end{center}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	406
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	407	\noindent
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	408	Values and non-problematic values
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	409
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	410	\begin{center}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	411	\begin{tabular}{c}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	412	@{thm Values_def}\medskip\\
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	413	\end{tabular}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	414	\end{center}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	415
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	416
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	417	\noindent
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	418	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	419	non-problematic values.
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	420	*}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	421
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	422	text {*
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	423	\noindent
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	424	Some lemmas we have proved:\bigskip
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	425
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	426	@{thm L_flat_Prf}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	427
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	428	@{thm L_flat_NPrf}
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	429
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	430	@{thm[mode=IfThen] mkeps_nullable}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	431
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	432	@{thm[mode=IfThen] mkeps_flat}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	433
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	434	@{thm[mode=IfThen] Prf_injval}
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	435
107 6adda4a667b1 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 105 diff changeset	436	@{thm[mode=IfThen] Prf_injval_flat}
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	437
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	438	@{thm[mode=IfThen] PMatch_mkeps}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	439
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	440	@{thm[mode=IfThen] PMatch1(2)}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	441
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	442	@{thm[mode=IfThen] PMatch1N}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	443
100 8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	444	@{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	445
8b919b3d753e strengthened PMatch to get determ Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 99 diff changeset	446	\medskip
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	447	\noindent
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	448	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	449	@{term "s \<in> r \<rightarrow> v"}:
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	450
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	451	@{thm[mode=IfThen] PMatch2}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	452
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	453	\mbox{}\bigskip
102 7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	454
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	455	\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	456	@{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	457	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	458	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	459
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	460	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	461	\begin{array}{l}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	462	(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	463	\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	464	(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	465	\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	466	\end{array}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	467	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	468
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	469	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	470	and have
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	471
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	472	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	473	@{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	474	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	475
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	476	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	477	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	478
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	479	\begin{itemize}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	480	\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	481	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	482	with
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	483
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	484	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	485	@{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	486	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	487
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	488	and also
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	489
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	490	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	491	@{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	492	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	493
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	494	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	495	and have to prove
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	496
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	497	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	498	@{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	499	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	500
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	501	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	502	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	503	@{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	504	fact above.
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	505
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	506	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	507	This leaves to prove
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	508
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	509	\[
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	510	@{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	511	\]
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	512
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	513	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	514	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	515
103 ffe5d850df62 added some slides Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 102 diff changeset	516	\item[(2)] This case is similar.
102 7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	517	\end{itemize}
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	518
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	519	\noindent
7f589bfecffa updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 101 diff changeset	520	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	521	to the cases above.
98 8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	522	*}
8b4c8cdd0b51 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 97 diff changeset	523
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	524
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	525	text {*
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	526	%\noindent
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	527	%{\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	528	%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	529	%referees.
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	530
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	531	\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	532	\bibliography{root}
101 7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	533
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	534	\section{Roy's Rules}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	535
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	536	\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	537	%%\newcommand{\mts}{\textit{``''}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	538	\newcommand{\tl}{\ \triangleleft\ }
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	539	$$\inferrule[]{Void \tl \epsilon}{}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	540	\quad\quad
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	541	\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	542	$$
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	543	$$\inferrule
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	544	{v_1 \tl r_1}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	545	{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	546	\quad\quad
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	547	\inferrule[]
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	548	{ 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	549	{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	550	$$
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	551	$$
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	552	\inferrule
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	553	{v_1 \tl r_1\\
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	554	v_2 \tl r_2\\
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	555	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	556	\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	557	\ \Rightarrow\ s = []
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	558	}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	559	{(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	560	$$
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	561	$$\inferrule
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	562	{ 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	563	{ (v :: vs) \tl r^* }
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	564	\quad\quad
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	565	\inferrule{}
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	566	{ [] \tl r^* }
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	567	$$
7f4f8c34da95 fixed inj function Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 100 diff changeset	568
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	569	*}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	570
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	571
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	572	(<)
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	573	end
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	574	(>)

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Wed, 02 Mar 2016 04:13:25 +0000
changeset 109	2c38f10643ae
parent 108	73f7dc60c285
child 110	267afb7fb700
permissions	-rw-r--r--