--- a/thys/Paper/Paper.thy Wed Feb 24 21:08:35 2016 +0000
+++ b/thys/Paper/Paper.thy Thu Feb 25 12:17:31 2016 +0000
@@ -16,8 +16,8 @@
Sequ ("_ @ _" [78,77] 63) and
injval ("inj _ _ _" [1000,77,1000] 77) and
projval ("proj _ _ _" [1000,77,1000] 77) and
- length ("len _" [78] 73) and
- ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73)
+ length ("len _" [78] 73)
+ (* and ValOrd ("_ \<succeq>\<^bsub>_\<^esub> _" [78,77,77] 73) *)
(*>*)
section {* Introduction *}
@@ -328,24 +328,6 @@
to the cases above.
*}
-text {*
- \noindent
- Things we have proved about our version of the Sulzmann ordering
-
- \begin{center}
- \begin{tabular}{c}
- @{thm[mode=IfThen] ValOrd_refl[of "v" "r"]}\medskip\\
- %@ {thm[mode=IfThen] ValOrd_total[of "v\<^sub>1" "r" "v\<^sub>2"]}
- \end{tabular}
- \end{center}\bigskip
-
- \noindent
- Things we like to prove, but cannot:\bigskip
-
- If @{term "s \<in> r \<rightarrow> v\<^sub>1"}, @{term "\<turnstile> v\<^sub>2 : r"}, then @{term "v\<^sub>1 \<succ>r v\<^sub>2"}
-
-*}
-
text {*
%\noindent
--- a/thys/Paper/document/root.tex Wed Feb 24 21:08:35 2016 +0000
+++ b/thys/Paper/document/root.tex Thu Feb 25 12:17:31 2016 +0000
@@ -15,7 +15,6 @@
\titlerunning{BLA BLA}
-
\urlstyle{rm}
\isabellestyle{it}
\renewcommand{\isastyleminor}{\it}%
@@ -28,16 +27,21 @@
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
\definecolor{mygrey}{rgb}{.80,.80,.80}
+\def\Brz{Brzozowski}
+
\begin{document}
-\title{RegEx}
+\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)}
\author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{1}}
\institute{King's College London, United Kingdom \and
St Andrews}
\maketitle
\begin{abstract}
+\Brz{} introduced the notion of derivatives of regular expressions
+that can be used for very simple regular expression matching algorithms.
+
BLA BLA Sulzmann and Lu \cite{Sulzmann2014}
{\bf Keywords:}
--- a/thys/ReStar.thy Wed Feb 24 21:08:35 2016 +0000
+++ b/thys/ReStar.thy Thu Feb 25 12:17:31 2016 +0000
@@ -1224,10 +1224,13 @@
using assms
apply(induct c r arbitrary: s v rule: der.induct)
apply(auto)
+(* NULL case *)
apply(erule PMatch.cases)
apply(simp_all)[7]
+(* EMPTY case *)
apply(erule PMatch.cases)
apply(simp_all)[7]
+(* CHAR case *)
apply(case_tac "c = c'")
apply(simp)
apply(erule PMatch.cases)
@@ -1236,6 +1239,7 @@
apply(simp)
apply(erule PMatch.cases)
apply(simp_all)[7]
+(* ALT case *)
apply(erule PMatch.cases)
apply(simp_all)[7]
apply (metis PMatch.intros(3))
@@ -1247,6 +1251,7 @@
apply(case_tac "nullable r1")
apply(simp)
prefer 2
+(* not-nullbale case *)
apply(simp)
apply(erule PMatch.cases)
apply(simp_all)[7]
@@ -1261,9 +1266,14 @@
(* nullable case *)
apply(erule PMatch.cases)
apply(simp_all)[7]
+(* left case *)
apply(clarify)
apply(erule PMatch.cases)
apply(simp_all)[4]
+prefer 2
+apply(clarify)
+prefer 2
+apply(clarify)
apply(clarify)
apply(simp (no_asm))
apply(subst append.simps(2)[symmetric])
@@ -1275,9 +1285,7 @@
apply(auto)[1]
apply(simp add: der_correctness Der_def)
apply metis
-apply(simp)
-(* interesting case *)
-apply(clarify)
+(* right interesting case *)
apply(clarify)
apply(simp)
apply(subst (asm) L.simps(4)[symmetric])
--- a/thys/ReTest.thy Wed Feb 24 21:08:35 2016 +0000
+++ b/thys/ReTest.thy Thu Feb 25 12:17:31 2016 +0000
@@ -1152,6 +1152,19 @@
L7: "s' \<in> L(r') \<longrightarrow> s' \<in> L(r) \<longrightarrow> \<not>PC32 s' r r'" and
L8: "s \<in> L(r) \<longrightarrow> s' \<in> L(r') \<longrightarrow> s @ x \<in> L(r) \<longrightarrow> s' \<in> {x} ;; (L(r') ;; {y}) \<longrightarrow> x \<noteq> [] \<longrightarrow> \<not>PC42 s s' r r'"
apply(auto simp add: PC32_def PC42_def)[1]
+apply(simp add: Sequ_def)
+apply (metis nullable_correctness)
+apply(auto simp add: PC32_def PC42_def Sequ_def)[1]
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+apply(simp add: Cons_eq_append_conv)
+apply(auto)[1]
+defer
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def nullable_correctness)[1]
+apply (metis append_Cons append_assoc hd_Cons_tl list.discI list.inject)
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
+apply(auto simp add: PC32_def PC42_def Sequ_def der_correctness Der_def)[1]
oops
definition
@@ -1663,6 +1676,7 @@
apply(drule_tac x="Seq (projval r1 c v) vb" in spec)
apply(drule mp)
apply(simp)
+
apply (metis append_Cons butlast_snoc list.sel(1) neq_Nil_conv rotate1.simps(2) v4_proj2)
apply(subgoal_tac "\<turnstile> projval r1 c v : der c r1")
apply (metis NPrf_imp_Prf Prf.intros(1))
Binary file thys/paper.pdf has changed