lexing: thys/Paper/Paper.thy@38696f516c6b (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
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	10	Cons ("_::_" [78,77] 73) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	11	val.Char ("Char _" [1000] 78) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	12	val.Left ("Left _" [1000] 78) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	13	val.Right ("Right _" [1000] 78) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	14	L ("L _" [1000] 0) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	15	flat ("\|_\|" [70] 73) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	16	Sequ ("_ @ _" [78,77] 63) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	17	injval ("inj _ _ _" [1000,77,1000] 77) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	18	length ("len _" [78] 73) and
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	19	ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73)
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	(>)
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	section {* Introduction *}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23
97 38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	24	text {*
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	25
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	26	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	27	Regular exprtessions
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	28
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	29	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	30	@{text "r :="}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	31	@{const "NULL"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	32	@{const "EMPTY"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	33	@{term "CHAR c"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	34	@{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	35	@{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	36	@{term "STAR r"}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	37	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	38
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	39	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	40	Values
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	41
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	42	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	43	@{text "v :="}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	44	@{const "Void"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	45	@{term "val.Char c"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	46	@{term "Left v"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	47	@{term "Right v"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	48	@{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	49	@{term "Stars vs"}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	50	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	51
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	52	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	53	The language of a regular expression
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	54
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	55	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	56	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	57	@{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	58	@{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	59	@{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	60	@{thm (lhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	61	@{thm (lhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) L.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	62	@{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	63	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	64	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	65
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	66	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	67	The nullable function
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	68
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	69	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	70	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	71	@{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	72	@{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	73	@{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	74	@{thm (lhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	75	@{thm (lhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) nullable.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	76	@{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	77	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	78	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	79
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	80	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	81	The derivative function for characters and strings
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	82
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	83	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	84	\begin{tabular}{lcp{7.5cm}}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	85	@{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	86	@{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	87	@{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	88	@{thm (lhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(4)[of c "r\<^sub>1" "r\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	89	@{thm (lhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) der.simps(5)[of c "r\<^sub>1" "r\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	90	@{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}\medskip\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	91
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	92	@{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	93	@{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	94	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	95	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	96
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	97	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	98	The @{const flat} function for values
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	99
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	100	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	101	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	102	@{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	103	@{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	104	@{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	105	@{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	106	@{thm (lhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) flat.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	107	@{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	108	@{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	109	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	110	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	111
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	112	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	113	The @{const mkeps} function
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	114
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	115	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	116	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	117	@{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	118	@{thm (lhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(2)[of "r\<^sub>1" "r\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	119	@{thm (lhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) mkeps.simps(3)[of "r\<^sub>1" "r\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	120	@{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	121	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	122	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	123
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	124	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	125	The @{text inj} function
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	126
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	127	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	128	\begin{tabular}{lcl}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	129	@{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	130	@{thm (lhs) injval.simps(2)} & $\dn$ & @{thm (rhs) injval.simps(2)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	131	@{thm (lhs) injval.simps(3)} & $\dn$ & @{thm (rhs) injval.simps(3)}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	132	@{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ &
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	133	@{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	134	@{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ &
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	135	@{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	136	@{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	137	& @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "c" "v\<^sub>1" "v\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	138	@{thm (lhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	139	& @{thm (rhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	140	@{thm (lhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	141	& @{thm (rhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	142	@{thm (lhs) injval.simps(9)[of "r" "c" "v" "vs"]} & $\dn$
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	143	& @{thm (rhs) injval.simps(9)[of "r" "c" "v" "vs"]}\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	144	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	145	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	146
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	147	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	148	The inhabitation relation:
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	149
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	150	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	151	\begin{tabular}{c}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	152	@{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	153	@{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	154	@{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	155	@{thm[mode=Axiom] Prf.intros(4)} \qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	156	@{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	157	@{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	158	@{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	159	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	160	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	161
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	162	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	163	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	164	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	165	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	166	\bigskip
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	167
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	168
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	169	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	170	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	171
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	172	\begin{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	173	\begin{tabular}{c}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	174	@{thm[mode=Axiom] PMatch.intros(1)} \qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	175	@{thm[mode=Axiom] PMatch.intros(2)}\medskip\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	176	@{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	177	@{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	178	\multicolumn{1}{p{5cm}}{@{thm[mode=Rule] PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}\medskip\\
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	179	@{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	180	@{thm[mode=Axiom] PMatch.intros(7)}\medskip\\
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	Our version of Sulzmann's ordering relation
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}{c}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	189	@{thm[mode=Rule] ValOrd.intros(2)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'"]} \qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	190	@{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	191	@{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	192	@{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	193	@{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	194	@{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	195	@{thm[mode=Axiom] ValOrd.intros(7)}\qquad
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	196	@{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	197	@{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	198	@{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	199	@{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	200	@{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	201	@{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	202	\end{tabular}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	203	\end{center}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	204	*}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	205
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	206	text {*
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	207	\noindent
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	208	Some lemmas
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	209
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	210
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	211	@{thm[mode=IfThen] mkeps_nullable}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	212
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	213	@{thm[mode=IfThen] mkeps_flat}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	214
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	215	\ldots
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	216	*}
38696f516c6b updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 95 diff changeset	217
95 a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	218
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	219	text {*
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	220	%\noindent
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	221	%{\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	222	%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	223	%referees.
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	224
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	225	\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	226	\bibliography{root}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	227	*}
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	228
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	229
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	230	(<)
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	231	end
a33d3040bf7e started a paper and moved cruft to Attic Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	232	(>)

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Sun, 07 Feb 2016 23:44:34 +0000
changeset 97	38696f516c6b
parent 95	a33d3040bf7e
child 98	8b4c8cdd0b51
permissions	-rw-r--r--