# HG changeset patch # User Christian Urban # Date 1458264374 0 # Node ID 2de3cf684ba0287cbb9e7a03c2163cd3a1c6ec45 # Parent 69ec99b14ac9e7c82385526345870750e6182ae2 updated diff -r 69ec99b14ac9 -r 2de3cf684ba0 thys/Paper/Paper.thy --- 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\" "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] 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} diff -r 69ec99b14ac9 -r 2de3cf684ba0 thys/Paper/document/root.tex --- 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} diff -r 69ec99b14ac9 -r 2de3cf684ba0 thys/Simplifying.thy --- 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 \ rexp * (val \ 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 "\ ((snd (simp r)) v) : r \ \ 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 \ r \ ((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 diff -r 69ec99b14ac9 -r 2de3cf684ba0 thys/Sulzmann.thy --- 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 \ rexp \ 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 \ val \ val" +where + "Stars_add v (Stars vs) = Stars (v # vs)" + +function + decode' :: "bool list \ rexp \ (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)) \ 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 \ rexp \ val option" +where + "decode ds r = (let (v, ds') = decode' ds r + in (if ds' = [] then Some v else None))" + +lemma decode'_code: + assumes "\ v : r" + shows "decode' ((code v r) @ ds) r = (v, ds)" +using assms +by (induct v r arbitrary: ds) (auto) + + +lemma decode_code: + assumes "\ v : r" + shows "decode (code v r) r = Some v" +using assms decode'_code[of _ _ "[]"] +by auto + end \ No newline at end of file diff -r 69ec99b14ac9 -r 2de3cf684ba0 thys/paper.pdf Binary file thys/paper.pdf has changed