Mercurial Mercurial > hg > lexing / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Fri, 18 Mar 2016 01:26:14 +0000
changeset 154 2de3cf684ba0
parent 153 69ec99b14ac9
child 155 c9027db225cc
updated
thys/Paper/Paper.thy file | annotate | diff | comparison | revisions
thys/Paper/document/root.tex file | annotate | diff | comparison | revisions
thys/Simplifying.thy file | annotate | diff | comparison | revisions
thys/Sulzmann.thy file | annotate | diff | comparison | revisions
thys/paper.pdf file | annotate | diff | comparison | revisions 
--- a/thys/Paper/Paper.thy	Wed Mar 16 10:02:19 2016 +0000
+++ b/thys/Paper/Paper.thy	Fri Mar 18 01:26:14 2016 +0000
@@ -918,20 +918,20 @@
 
 \begin{center}  
 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}}	
-@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1'" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'"]}(C2) &
-@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2'" "v\<^sub>1" "r\<^sub>1"]}(C1)\smallskip\\
+@{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) &
+@{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\
 
-@{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}(A1) &
-@{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}(A2)\smallskip\\
+@{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\,(A1) &
+@{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\,(A2)\smallskip\\
 
-@{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}(A3) &
-@{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}(A4)\smallskip\\
+@{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}\,(A3) &
+@{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\,(A4)\smallskip\\
 
-@{thm[mode=Rule] K1[of "v" "vs" "r"]}(K1) &
-@{thm[mode=Rule] K2[of "v" "vs" "r"]}(K2)\smallskip\\
+@{thm[mode=Rule] K1[of "v" "vs" "r"]}\,(K1) &
+@{thm[mode=Rule] K2[of "v" "vs" "r"]}\,(K2)\smallskip\\
 
-@{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}(K3) &
-@{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}(K4)
+@{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\,(K3) &
+@{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\,(K4)
 \end{tabular}
 \end{center}
 
--- a/thys/Paper/document/root.tex	Wed Mar 16 10:02:19 2016 +0000
+++ b/thys/Paper/document/root.tex	Fri Mar 18 01:26:14 2016 +0000
@@ -14,6 +14,8 @@
 \usepackage{url}
 \usepackage{color}
 
+\usepackage{mathtools}
+
 \titlerunning{POSIX Lexing with Derivatives of Regular Expressions}
 
 \urlstyle{rm}
@@ -26,7 +28,8 @@
 \renewcommand{\isasymequiv}{$\dn$}
 \renewcommand{\isasymemptyset}{$\varnothing$}
 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
-%%\renewcommand{\isacharprime}{\makebox[0mm]{$\mbox{}\mbox{$\,^\prime$}$}}
+\renewcommand{\isasymiota}{\makebox[0mm]{${}^{\prime}$}}
+%%\makebox[0mm]{$\mbox{}\mbox{$\,^\prime$}$}}
 
 \definecolor{mygrey}{rgb}{.80,.80,.80}
 \def\Brz{Brzozowski}
--- a/thys/Simplifying.thy	Wed Mar 16 10:02:19 2016 +0000
+++ b/thys/Simplifying.thy	Fri Mar 18 01:26:14 2016 +0000
@@ -37,74 +37,17 @@
 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (ONE, f\<^sub>2) = (r\<^sub>1, F_SEQ2 f\<^sub>1 f\<^sub>2)"
 | "simp_SEQ (r\<^sub>1, f\<^sub>1) (r\<^sub>2, f\<^sub>2) = (SEQ r\<^sub>1 r\<^sub>2, F_SEQ f\<^sub>1 f\<^sub>2)"  
  
-lemma simp_SEQ_simps:
+lemma simp_SEQ_simps[simp]:
   "simp_SEQ p1 p2 = (if (fst p1 = ONE) then (fst p2, F_SEQ1 (snd p1) (snd p2))
                     else (if (fst p2 = ONE) then (fst p1, F_SEQ2 (snd p1) (snd p2))
                     else (SEQ (fst p1) (fst p2), F_SEQ (snd p1) (snd p2))))"
-apply(auto)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(auto)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-done
+by (induct p1 p2 rule: simp_SEQ.induct) (auto)
 
-lemma simp_ALT_simps:
+lemma simp_ALT_simps[simp]:
   "simp_ALT p1 p2 = (if (fst p1 = ZERO) then (fst p2, F_RIGHT (snd p2))
                     else (if (fst p2 = ZERO) then (fst p1, F_LEFT (snd p1))
                     else (ALT (fst p1) (fst p2), F_ALT (snd p1) (snd p2))))"
-apply(auto)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac p1)
-apply(case_tac p2)
-apply(simp)
-apply(case_tac a)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(auto)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-apply(case_tac aa)
-apply(simp_all)
-done
-
+by (induct p1 p2 rule: simp_ALT.induct) (auto)
 
 fun 
   simp :: "rexp \<Rightarrow> rexp * (val \<Rightarrow> val)"
@@ -126,15 +69,14 @@
 lemma L_fst_simp:
   shows "L(r) = L(fst (simp r))"
 using assms
-apply(induct r rule: rexp.induct)
-apply(auto simp add: simp_SEQ_simps simp_ALT_simps)
-done
+by (induct r) (auto)
+
 
 lemma 
   shows "\<turnstile> ((snd (simp r)) v) : r \<longleftrightarrow> \<turnstile> v : (fst (simp r))"
 using assms
 apply(induct r arbitrary: v rule: simp.induct)
-apply(auto simp add: simp_SEQ_simps simp_ALT_simps intro: Prf.intros)
+apply(auto intro: Prf.intros)
 using Prf_elims(3) apply blast
 apply(erule Prf_elims)
 apply(simp)
@@ -210,7 +152,7 @@
   shows "((snd (simp r)) v) = mkeps r"
 using assms 
 apply(induct r arbitrary: v)
-apply(auto simp add: simp_SEQ_simps simp_ALT_simps)
+apply(auto)
 apply(erule Posix_elims)
 apply(simp)
 apply(erule Posix_elims)
@@ -254,7 +196,7 @@
   shows "s \<in> r \<rightarrow> ((snd (simp r)) v)"
 using assms
 apply(induct r arbitrary: s v rule: rexp.induct) 
-apply(auto split: if_splits simp add: simp_SEQ_simps simp_ALT_simps)
+apply(auto split: if_splits)
 prefer 3
 apply(erule Posix_elims)
 apply(clarify)
@@ -311,7 +253,6 @@
   shows "slexer r s = lexer r s"
 apply(induct s arbitrary: r)
 apply(simp)
-apply(simp)
 apply(auto split: option.split prod.split)
 apply (metis L_fst_simp fst_conv lexer_correct_None)
 using L_fst_simp lexer_correct_None apply fastforce
--- a/thys/Sulzmann.thy	Wed Mar 16 10:02:19 2016 +0000
+++ b/thys/Sulzmann.thy	Fri Mar 18 01:26:14 2016 +0000
@@ -45,6 +45,78 @@
 *)
 
 
+section {* Bit-Encodings *}
+
+
+fun 
+  code :: "val \<Rightarrow> rexp \<Rightarrow> bool list"
+where
+  "code Void ONE = []"
+| "code (Char c) (CHAR d) = []"
+| "code (Left v) (ALT r1 r2) = False # (code v r1)"
+| "code (Right v) (ALT r1 r2) = True # (code v r2)"
+| "code (Seq v1 v2) (SEQ r1 r2) = (code v1 r1) @ (code v2 r2)"
+| "code (Stars []) (STAR r) = [True]"
+| "code (Stars (v # vs)) (STAR r) =  False # (code v r) @ code (Stars vs) (STAR r)"
+
+fun 
+  Stars_add :: "val \<Rightarrow> val \<Rightarrow> val"
+where
+  "Stars_add v (Stars vs) = Stars (v # vs)"
+
+function
+  decode' :: "bool list \<Rightarrow> rexp \<Rightarrow> (val * bool list)"
+where
+  "decode' ds ZERO = (Void, [])"
+| "decode' ds ONE = (Void, ds)"
+| "decode' ds (CHAR d) = (Char d, ds)"
+| "decode' [] (ALT r1 r2) = (Void, [])"
+| "decode' (False # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
+| "decode' (True # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
+| "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in
+                             let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))"
+| "decode' [] (STAR r) = (Void, [])"
+| "decode' (True # ds) (STAR r) = (Stars [], ds)"
+| "decode' (False # ds) (STAR r) = (let (v, ds') = decode' ds r in
+                                    let (vs, ds'') = decode' ds' (STAR r) 
+                                    in (Stars_add v vs, ds''))"
+by pat_completeness auto
+
+term "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))"
+
+lemma decode'_smaller:
+  assumes "decode'_dom (ds, r)"
+  shows "length (snd (decode' ds r)) \<le> length ds"
+using assms
+apply(induct ds r)
+apply(auto simp add: decode'.psimps split: prod.split)
+using dual_order.trans apply blast
+by (meson dual_order.trans le_SucI)
+
+termination "decode'"  
+apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") 
+apply(auto dest!: decode'_smaller)
+by (metis less_Suc_eq_le snd_conv)
+
+fun 
+  decode :: "bool list \<Rightarrow> rexp \<Rightarrow> val option"
+where
+  "decode ds r = (let (v, ds') = decode' ds r 
+                  in (if ds' = [] then Some v else None))"
+
+lemma decode'_code:
+  assumes "\<turnstile> v : r"
+  shows "decode' ((code v r) @ ds) r = (v, ds)"
+using assms
+by (induct v r arbitrary: ds) (auto)
+
+
+lemma decode_code:
+  assumes "\<turnstile> v : r"
+  shows "decode (code v r) r = Some v"
+using assms decode'_code[of _ _ "[]"]
+by auto
+
 
 
 end
\ No newline at end of file
Binary file thys/paper.pdf has changed
lexing