diff -r c3d7125f9950 -r 38696f516c6b thys/Paper/Paper.thy --- a/thys/Paper/Paper.thy Fri Feb 05 10:16:41 2016 +0000 +++ b/thys/Paper/Paper.thy Sun Feb 07 23:44:34 2016 +0000 @@ -2,11 +2,219 @@ theory Paper imports "../ReStar" "~~/src/HOL/Library/LaTeXsugar" begin + +declare [[show_question_marks = false]] + +notation (latex output) + If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and + Cons ("_::_" [78,77] 73) and + val.Char ("Char _" [1000] 78) and + val.Left ("Left _" [1000] 78) and + val.Right ("Right _" [1000] 78) and + L ("L _" [1000] 0) and + flat ("|_|" [70] 73) and + Sequ ("_ @ _" [78,77] 63) and + injval ("inj _ _ _" [1000,77,1000] 77) and + length ("len _" [78] 73) and + ValOrd ("_ \\<^bsub>_\<^esub> _" [78,77,77] 73) (*>*) section {* Introduction *} - +text {* + + \noindent + Regular exprtessions + + \begin{center} + @{text "r :="} + @{const "NULL"} $\mid$ + @{const "EMPTY"} $\mid$ + @{term "CHAR c"} $\mid$ + @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$ + @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$ + @{term "STAR r"} + \end{center} + + \noindent + Values + + \begin{center} + @{text "v :="} + @{const "Void"} $\mid$ + @{term "val.Char c"} $\mid$ + @{term "Left v"} $\mid$ + @{term "Right v"} $\mid$ + @{term "Seq v\<^sub>1 v\<^sub>2"} $\mid$ + @{term "Stars vs"} + \end{center} + + \noindent + The language of a regular expression + + \begin{center} + \begin{tabular}{lcl} + @{thm (lhs) L.simps(1)} & $\dn$ & @{thm (rhs) L.simps(1)}\\ + @{thm (lhs) L.simps(2)} & $\dn$ & @{thm (rhs) L.simps(2)}\\ + @{thm (lhs) L.simps(3)} & $\dn$ & @{thm (rhs) L.simps(3)}\\ + @{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"]}\\ + @{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"]}\\ + @{thm (lhs) L.simps(6)} & $\dn$ & @{thm (rhs) L.simps(6)}\\ + \end{tabular} + \end{center} + + \noindent + The nullable function + + \begin{center} + \begin{tabular}{lcl} + @{thm (lhs) nullable.simps(1)} & $\dn$ & @{thm (rhs) nullable.simps(1)}\\ + @{thm (lhs) nullable.simps(2)} & $\dn$ & @{thm (rhs) nullable.simps(2)}\\ + @{thm (lhs) nullable.simps(3)} & $\dn$ & @{thm (rhs) nullable.simps(3)}\\ + @{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"]}\\ + @{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"]}\\ + @{thm (lhs) nullable.simps(6)} & $\dn$ & @{thm (rhs) nullable.simps(6)}\\ + \end{tabular} + \end{center} + + \noindent + The derivative function for characters and strings + + \begin{center} + \begin{tabular}{lcp{7.5cm}} + @{thm (lhs) der.simps(1)} & $\dn$ & @{thm (rhs) der.simps(1)}\\ + @{thm (lhs) der.simps(2)} & $\dn$ & @{thm (rhs) der.simps(2)}\\ + @{thm (lhs) der.simps(3)} & $\dn$ & @{thm (rhs) der.simps(3)}\\ + @{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"]}\\ + @{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"]}\\ + @{thm (lhs) der.simps(6)} & $\dn$ & @{thm (rhs) der.simps(6)}\medskip\\ + + @{thm (lhs) ders.simps(1)} & $\dn$ & @{thm (rhs) ders.simps(1)}\\ + @{thm (lhs) ders.simps(2)} & $\dn$ & @{thm (rhs) ders.simps(2)}\\ + \end{tabular} + \end{center} + + \noindent + The @{const flat} function for values + + \begin{center} + \begin{tabular}{lcl} + @{thm (lhs) flat.simps(1)} & $\dn$ & @{thm (rhs) flat.simps(1)}\\ + @{thm (lhs) flat.simps(2)} & $\dn$ & @{thm (rhs) flat.simps(2)}\\ + @{thm (lhs) flat.simps(3)} & $\dn$ & @{thm (rhs) flat.simps(3)}\\ + @{thm (lhs) flat.simps(4)} & $\dn$ & @{thm (rhs) flat.simps(4)}\\ + @{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"]}\\ + @{thm (lhs) flat.simps(6)} & $\dn$ & @{thm (rhs) flat.simps(6)}\\ + @{thm (lhs) flat.simps(7)} & $\dn$ & @{thm (rhs) flat.simps(7)}\\ + \end{tabular} + \end{center} + + \noindent + The @{const mkeps} function + + \begin{center} + \begin{tabular}{lcl} + @{thm (lhs) mkeps.simps(1)} & $\dn$ & @{thm (rhs) mkeps.simps(1)}\\ + @{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"]}\\ + @{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"]}\\ + @{thm (lhs) mkeps.simps(4)} & $\dn$ & @{thm (rhs) mkeps.simps(4)}\\ + \end{tabular} + \end{center} + + \noindent + The @{text inj} function + + \begin{center} + \begin{tabular}{lcl} + @{thm (lhs) injval.simps(1)} & $\dn$ & @{thm (rhs) injval.simps(1)}\\ + @{thm (lhs) injval.simps(2)} & $\dn$ & @{thm (rhs) injval.simps(2)}\\ + @{thm (lhs) injval.simps(3)} & $\dn$ & @{thm (rhs) injval.simps(3)}\\ + @{thm (lhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]} & $\dn$ & + @{thm (rhs) injval.simps(4)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1"]}\\ + @{thm (lhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ & + @{thm (rhs) injval.simps(5)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ + @{thm (lhs) injval.simps(6)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ + & @{thm (rhs) injval.simps(6)[of "r\<^sub>1" "c" "v\<^sub>1" "v\<^sub>2"]}\\ + @{thm (lhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]} & $\dn$ + & @{thm (rhs) injval.simps(7)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>1" "v\<^sub>2"]}\\ + @{thm (lhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]} & $\dn$ + & @{thm (rhs) injval.simps(8)[of "r\<^sub>1" "r\<^sub>2" "c" "v\<^sub>2"]}\\ + @{thm (lhs) injval.simps(9)[of "r" "c" "v" "vs"]} & $\dn$ + & @{thm (rhs) injval.simps(9)[of "r" "c" "v" "vs"]}\\ + \end{tabular} + \end{center} + + \noindent + The inhabitation relation: + + \begin{center} + \begin{tabular}{c} + @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\medskip\\ + @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad + @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\medskip\\ + @{thm[mode=Axiom] Prf.intros(4)} \qquad + @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\medskip\\ + @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad + @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}\medskip\\ + \end{tabular} + \end{center} + + \noindent + We have also introduced a slightly restricted version of this relation + where the last rule is restricted so that @{term "flat v \ []"}. + This relation for \emph{non-problematic} is written @{term "\ v : r"}. + \bigskip + + + \noindent + Our Posix relation @{term "s \ r \ v"} + + \begin{center} + \begin{tabular}{c} + @{thm[mode=Axiom] PMatch.intros(1)} \qquad + @{thm[mode=Axiom] PMatch.intros(2)}\medskip\\ + @{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}\qquad + @{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}\medskip\\ + \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\\ + @{thm[mode=Rule] PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad + @{thm[mode=Axiom] PMatch.intros(7)}\medskip\\ + \end{tabular} + \end{center} + + \noindent + Our version of Sulzmann's ordering relation + + \begin{center} + \begin{tabular}{c} + @{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 + @{thm[mode=Rule] ValOrd.intros(1)[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "v\<^sub>1" "r\<^sub>1"]}\medskip\\ + @{thm[mode=Rule] ValOrd.intros(3)[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]} \qquad + @{thm[mode=Rule] ValOrd.intros(4)[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\medskip\\ + @{thm[mode=Rule] ValOrd.intros(5)[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "r\<^sub>1"]} \qquad + @{thm[mode=Rule] ValOrd.intros(6)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "r\<^sub>2"]} \medskip\\ + @{thm[mode=Axiom] ValOrd.intros(7)}\qquad + @{thm[mode=Axiom] ValOrd.intros(8)[of "c"]}\medskip\\ + @{thm[mode=Rule] ValOrd.intros(9)[of "v" "vs" "r"]}\qquad + @{thm[mode=Rule] ValOrd.intros(10)[of "v" "vs" "r"]}\medskip\\ + @{thm[mode=Rule] ValOrd.intros(11)[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\medskip\\ + @{thm[mode=Rule] ValOrd.intros(12)[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\qquad + @{thm[mode=Axiom] ValOrd.intros(13)[of "r"]}\medskip\\ + \end{tabular} + \end{center} +*} + +text {* + \noindent + Some lemmas + + + @{thm[mode=IfThen] mkeps_nullable} + + @{thm[mode=IfThen] mkeps_flat} + + \ldots +*} + text {* %\noindent