# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1456402651 0
# Node ID 80218dddbb15dba71e9cda77bd1a4d21195a3aa4
# Parent  59bad592a0095ddc0080ab6cd802c79a8c1754df
updated

diff -r 59bad592a009 -r 80218dddbb15 thys/Paper/Paper.thy
--- 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
diff -r 59bad592a009 -r 80218dddbb15 thys/Paper/document/root.tex
--- 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:} 
diff -r 59bad592a009 -r 80218dddbb15 thys/ReStar.thy
--- 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])
diff -r 59bad592a009 -r 80218dddbb15 thys/ReTest.thy
--- 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))
diff -r 59bad592a009 -r 80218dddbb15 thys/paper.pdf
Binary file thys/paper.pdf has changed