# HG changeset patch # User Christian Urban # Date 1534553684 -3600 # Node ID 807acaf7f5998328898ecea0cda010775cd14d34 # Parent 9ab8609c66c59c18864fec81731e811e8f72b69e updated diff -r 9ab8609c66c5 -r 807acaf7f599 thys/Journal/Paper.thy --- a/thys/Journal/Paper.thy Fri Aug 17 12:00:25 2018 +0100 +++ b/thys/Journal/Paper.thy Sat Aug 18 01:54:44 2018 +0100 @@ -31,6 +31,12 @@ abbreviation "ders_syn r s \ ders s r" + abbreviation + "bder_syn r c \ bder c r" + +abbreviation + "bders_syn r s \ bders r s" + abbreviation "nprec v1 v2 \ \(v1 :\val v2)" @@ -91,6 +97,15 @@ pflat_len ("\_\\<^bsub>_\<^esub>") and nprec ("_ \<^latex>\\\mbox{$\\not\\prec$}\ _" [77,77] 77) and + bder_syn ("_\<^latex>\\\mbox{$\\bbslash$}\_" [79, 1000] 76) and + bders_syn ("_\<^latex>\\\mbox{$\\bbslash$}\_" [79, 1000] 76) and + intern ("_\<^latex>\\\mbox{$^\\uparrow$}\" [900] 80) and + erase ("_\<^latex>\\\mbox{$^\\downarrow$}\" [1000] 74) and + bnullable ("nullable\<^latex>\\\mbox{$_b$}\ _" [1000] 80) and + bmkeps ("mkeps\<^latex>\\\mbox{$_b$}\ _" [1000] 80) and + blexer ("lexer\<^latex>\\\mbox{$_b$}\ _ _" [77, 77] 80) and + code ("code _" [79] 74) and + DUMMY ("\<^latex>\\\underline{\\hspace{2mm}}\") @@ -710,10 +725,10 @@ The idea of the @{term inj}-function to ``inject'' a character, say @{term c}, into a value can be made precise by the first part of the following lemma, which shows that the underlying string of an injected - value has a prepended character @{term c}; the second part shows that the - underlying string of an @{const mkeps}-value is always the empty string - (given the regular expression is nullable since otherwise @{text mkeps} - might not be defined). + value has a prepended character @{term c}; the second part shows that + the underlying string of an @{const mkeps}-value is always the empty + string (given the regular expression is nullable since otherwise + @{text mkeps} might not be defined). \begin{lemma}\mbox{}\smallskip\\\label{Prf_injval_flat} \begin{tabular}{ll} @@ -1385,6 +1400,126 @@ *} +section {* Bitcoded Lexing *} + + +text {* + +Incremental calculation of the value. To simplify the proof we first define the function +@{const flex} which calculates the ``iterated'' injection function. With this we can +rewrite the lexer as + +\begin{center} +@{thm lexer_flex} +\end{center} + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) code.simps(1)} & $\dn$ & @{thm (rhs) code.simps(1)}\\ + @{thm (lhs) code.simps(2)} & $\dn$ & @{thm (rhs) code.simps(2)}\\ + @{thm (lhs) code.simps(3)} & $\dn$ & @{thm (rhs) code.simps(3)}\\ + @{thm (lhs) code.simps(4)} & $\dn$ & @{thm (rhs) code.simps(4)}\\ + @{thm (lhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]} & $\dn$ & @{thm (rhs) code.simps(5)[of "v\<^sub>1" "v\<^sub>2"]}\\ + @{thm (lhs) code.simps(6)} & $\dn$ & @{thm (rhs) code.simps(6)}\\ + @{thm (lhs) code.simps(7)} & $\dn$ & @{thm (rhs) code.simps(7)} +\end{tabular} +\end{center} + +\begin{center} +\begin{tabular}{lcl} + @{term areg} & $::=$ & @{term "AZERO"}\\ + & $\mid$ & @{term "AONE bs"}\\ + & $\mid$ & @{term "ACHAR bs c"}\\ + & $\mid$ & @{term "AALT bs r\<^sub>1 r\<^sub>2"}\\ + & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ + & $\mid$ & @{term "ASTAR bs r"} +\end{tabular} +\end{center} + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\ + @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\ + @{thm (lhs) intern.simps(3)} & $\dn$ & @{thm (rhs) intern.simps(3)}\\ + @{thm (lhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(4)[of "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) intern.simps(5)[of "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) intern.simps(6)} & $\dn$ & @{thm (rhs) intern.simps(6)}\\ +\end{tabular} +\end{center} + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) erase.simps(1)} & $\dn$ & @{thm (rhs) erase.simps(1)}\\ + @{thm (lhs) erase.simps(2)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(2)[of bs]}\\ + @{thm (lhs) erase.simps(3)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(3)[of bs]}\\ + @{thm (lhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) erase.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) erase.simps(6)[of bs]} & $\dn$ & @{thm (rhs) erase.simps(6)[of bs]}\\ +\end{tabular} +\end{center} + +Some simple facts about erase + +\begin{lemma}\mbox{}\\ +@{thm erase_bder}\\ +@{thm erase_intern} +\end{lemma} + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) bnullable.simps(1)} & $\dn$ & @{thm (rhs) bnullable.simps(1)}\\ + @{thm (lhs) bnullable.simps(2)} & $\dn$ & @{thm (rhs) bnullable.simps(2)}\\ + @{thm (lhs) bnullable.simps(3)} & $\dn$ & @{thm (rhs) bnullable.simps(3)}\\ + @{thm (lhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bnullable.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bnullable.simps(6)} & $\dn$ & @{thm (rhs) bnullable.simps(6)}\medskip\\ + +% \end{tabular} +% \end{center} + +% \begin{center} +% \begin{tabular}{lcl} + + @{thm (lhs) bder.simps(1)} & $\dn$ & @{thm (rhs) bder.simps(1)}\\ + @{thm (lhs) bder.simps(2)} & $\dn$ & @{thm (rhs) bder.simps(2)}\\ + @{thm (lhs) bder.simps(3)} & $\dn$ & @{thm (rhs) bder.simps(3)}\\ + @{thm (lhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(4)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bder.simps(5)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bder.simps(6)} & $\dn$ & @{thm (rhs) bder.simps(6)} + \end{tabular} + \end{center} + + +\begin{center} + \begin{tabular}{lcl} + @{thm (lhs) bmkeps.simps(1)} & $\dn$ & @{thm (rhs) bmkeps.simps(1)}\\ + @{thm (lhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(2)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]} & $\dn$ & @{thm (rhs) bmkeps.simps(3)[of bs "r\<^sub>1" "r\<^sub>2"]}\\ + @{thm (lhs) bmkeps.simps(4)} & $\dn$ & @{thm (rhs) bmkeps.simps(4)}\medskip\\ +\end{tabular} +\end{center} + + +@{thm [mode=IfThen] bder_retrieve} + +By induction on @{text r} + +\begin{theorem}[Main Lemma]\mbox{}\\ +@{thm [mode=IfThen] MAIN_decode} +\end{theorem} + +\noindent +Definition of the bitcoded lexer + +@{thm blexer_def} + + +\begin{theorem} +@{thm blexer_correctness} +\end{theorem} + +*} + section {* Optimisations *} text {* diff -r 9ab8609c66c5 -r 807acaf7f599 thys/Journal/document/root.tex --- a/thys/Journal/document/root.tex Fri Aug 17 12:00:25 2018 +0100 +++ b/thys/Journal/document/root.tex Sat Aug 18 01:54:44 2018 +0100 @@ -9,7 +9,7 @@ \usepackage{pgf} \usetikzlibrary{positioning} \usepackage{pdfsetup} -%%\usepackage{stmaryrd} +\usepackage{stmaryrd} \usepackage{url} \usepackage{color} \usepackage[safe]{tipa} diff -r 9ab8609c66c5 -r 807acaf7f599 thys/Spec.thy --- a/thys/Spec.thy Fri Aug 17 12:00:25 2018 +0100 +++ b/thys/Spec.thy Sat Aug 18 01:54:44 2018 +0100 @@ -395,7 +395,7 @@ moreover have "LV (STAR r) s \ {Stars []} \ f ` (S1 \ S2)" unfolding S1_def S2_def f_def - unfolding LV_def image_def prefix_def strict_suffix_def + unfolding LV_def image_def prefix_def strict_suffix_def apply(auto) apply(case_tac x) apply(auto elim: Prf_elims) @@ -559,16 +559,21 @@ text {* - Our POSIX value is a lexical value. + Our POSIX values are lexical values. *} lemma Posix_LV: assumes "s \ r \ v" shows "v \ LV r s" -using assms unfolding LV_def -apply(induct rule: Posix.induct) -apply(auto simp add: intro!: Prf.intros elim!: Prf_elims) -done + using assms unfolding LV_def + apply(induct rule: Posix.induct) + apply(auto simp add: intro!: Prf.intros elim!: Prf_elims) + done +lemma Posix_Prf: + assumes "s \ r \ v" + shows "\ v : r" + using assms Posix_LV LV_def + by simp end \ No newline at end of file diff -r 9ab8609c66c5 -r 807acaf7f599 thys/Sulzmann.thy --- a/thys/Sulzmann.thy Fri Aug 17 12:00:25 2018 +0100 +++ b/thys/Sulzmann.thy Sat Aug 18 01:54:44 2018 +0100 @@ -5,16 +5,18 @@ section {* Bit-Encodings *} +datatype bit = Z | S + fun - code :: "val \ bool list" + code :: "val \ bit list" where "code Void = []" | "code (Char c) = []" -| "code (Left v) = False # (code v)" -| "code (Right v) = True # (code v)" +| "code (Left v) = Z # (code v)" +| "code (Right v) = S # (code v)" | "code (Seq v1 v2) = (code v1) @ (code v2)" -| "code (Stars []) = [True]" -| "code (Stars (v # vs)) = False # (code v) @ code (Stars vs)" +| "code (Stars []) = [S]" +| "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)" fun @@ -23,19 +25,19 @@ "Stars_add v (Stars vs) = Stars (v # vs)" function - decode' :: "bool list \ rexp \ (val * bool list)" + decode' :: "bit list \ rexp \ (val * bit 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' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" +| "decode' (S # 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 +| "decode' (S # ds) (STAR r) = (Stars [], ds)" +| "decode' (Z # 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 @@ -55,7 +57,7 @@ by (metis less_Suc_eq_le snd_conv) definition - decode :: "bool list \ rexp \ val option" + decode :: "bit list \ rexp \ val option" where "decode ds r \ (let (v, ds') = decode' ds r in (if ds' = [] then Some v else None))" @@ -76,7 +78,6 @@ apply(auto) using decode'_code_Stars by blast - lemma decode_code: assumes "\ v : r" shows "decode (code v) r = Some v" @@ -86,13 +87,13 @@ datatype arexp = AZERO -| AONE "bool list" -| ACHAR "bool list" char -| ASEQ "bool list" arexp arexp -| AALT "bool list" arexp arexp -| ASTAR "bool list" arexp +| AONE "bit list" +| ACHAR "bit list" char +| ASEQ "bit list" arexp arexp +| AALT "bit list" arexp arexp +| ASTAR "bit list" arexp -fun fuse :: "bool list \ arexp \ arexp" where +fun fuse :: "bit list \ arexp \ arexp" where "fuse bs AZERO = AZERO" | "fuse bs (AONE cs) = AONE (bs @ cs)" | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c" @@ -100,236 +101,219 @@ | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2" | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" -fun internalise :: "rexp \ arexp" where - "internalise ZERO = AZERO" -| "internalise ONE = AONE []" -| "internalise (CHAR c) = ACHAR [] c" -| "internalise (ALT r1 r2) = AALT [] (fuse [False] (internalise r1)) - (fuse [True] (internalise r2))" -| "internalise (SEQ r1 r2) = ASEQ [] (internalise r1) (internalise r2)" -| "internalise (STAR r) = ASTAR [] (internalise r)" +fun intern :: "rexp \ arexp" where + "intern ZERO = AZERO" +| "intern ONE = AONE []" +| "intern (CHAR c) = ACHAR [] c" +| "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) + (fuse [S] (intern r2))" +| "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" +| "intern (STAR r) = ASTAR [] (intern r)" -fun retrieve :: "arexp \ val \ bool list" where +fun retrieve :: "arexp \ val \ bit list" where "retrieve (AONE bs) Void = bs" | "retrieve (ACHAR bs c) (Char d) = bs" | "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v" | "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v" | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" -| "retrieve (ASTAR bs r) (Stars []) = bs @ [True]" +| "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" | "retrieve (ASTAR bs r) (Stars (v#vs)) = - bs @ [False] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)" - + bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)" fun - aerase :: "arexp \ rexp" + erase :: "arexp \ rexp" +where + "erase AZERO = ZERO" +| "erase (AONE _) = ONE" +| "erase (ACHAR _ c) = CHAR c" +| "erase (AALT _ r1 r2) = ALT (erase r1) (erase r2)" +| "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" +| "erase (ASTAR _ r) = STAR (erase r)" + +fun + bnullable :: "arexp \ bool" where - "aerase AZERO = ZERO" -| "aerase (AONE _) = ONE" -| "aerase (ACHAR _ c) = CHAR c" -| "aerase (AALT _ r1 r2) = ALT (aerase r1) (aerase r2)" -| "aerase (ASEQ _ r1 r2) = SEQ (aerase r1) (aerase r2)" -| "aerase (ASTAR _ r) = STAR (aerase r)" + "bnullable (AZERO) = False" +| "bnullable (AONE bs) = True" +| "bnullable (ACHAR bs c) = False" +| "bnullable (AALT bs r1 r2) = (bnullable r1 \ bnullable r2)" +| "bnullable (ASEQ bs r1 r2) = (bnullable r1 \ bnullable r2)" +| "bnullable (ASTAR bs r) = True" +fun + bmkeps :: "arexp \ bit list" +where + "bmkeps(AONE bs) = bs" +| "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" +| "bmkeps(AALT bs r1 r2) = (if bnullable(r1) then bs @ (bmkeps r1) else bs @ (bmkeps r2))" +| "bmkeps(ASTAR bs r) = bs @ [S]" fun - anullable :: "arexp \ bool" -where - "anullable (AZERO) = False" -| "anullable (AONE bs) = True" -| "anullable (ACHAR bs c) = False" -| "anullable (AALT bs r1 r2) = (anullable r1 \ anullable r2)" -| "anullable (ASEQ bs r1 r2) = (anullable r1 \ anullable r2)" -| "anullable (ASTAR bs r) = True" - -fun - amkeps :: "arexp \ bool list" + bder :: "char \ arexp \ arexp" where - "amkeps(AONE bs) = bs" -| "amkeps(ASEQ bs r1 r2) = bs @ (amkeps r1) @ (amkeps r2)" -| "amkeps(AALT bs r1 r2) = (if anullable(r1) then bs @ (amkeps r1) else bs @ (amkeps r2))" -| "amkeps(ASTAR bs r) = bs @ [True]" - - -fun - ader :: "char \ arexp \ arexp" -where - "ader c (AZERO) = AZERO" -| "ader c (AONE bs) = AZERO" -| "ader c (ACHAR bs d) = (if c = d then AONE bs else AZERO)" -| "ader c (AALT bs r1 r2) = AALT bs (ader c r1) (ader c r2)" -| "ader c (ASEQ bs r1 r2) = - (if anullable r1 - then AALT bs (ASEQ [] (ader c r1) r2) (fuse (amkeps r1) (ader c r2)) - else ASEQ bs (ader c r1) r2)" -| "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)" + "bder c (AZERO) = AZERO" +| "bder c (AONE bs) = AZERO" +| "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)" +| "bder c (AALT bs r1 r2) = AALT bs (bder c r1) (bder c r2)" +| "bder c (ASEQ bs r1 r2) = + (if bnullable r1 + then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) + else ASEQ bs (bder c r1) r2)" +| "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)" fun - aders :: "arexp \ string \ arexp" + bders :: "arexp \ string \ arexp" where - "aders r [] = r" -| "aders r (c#s) = aders (ader c r) s" + "bders r [] = r" +| "bders r (c#s) = bders (bder c r) s" -lemma aders_append: - "aders r (s1 @ s2) = aders (aders r s1) s2" +lemma bders_append: + "bders r (s1 @ s2) = bders (bders r s1) s2" apply(induct s1 arbitrary: r s2) apply(simp_all) done -lemma anullable_correctness: - shows "nullable (aerase r) = anullable r" +lemma bnullable_correctness: + shows "nullable (erase r) = bnullable r" apply(induct r) apply(simp_all) done -lemma aerase_fuse: - shows "aerase (fuse bs r) = aerase r" +lemma erase_fuse: + shows "erase (fuse bs r) = erase r" apply(induct r) apply(simp_all) done -lemma aerase_internalise: - shows "aerase (internalise r) = r" +lemma erase_intern[simp]: + shows "erase (intern r) = r" apply(induct r) - apply(simp_all add: aerase_fuse) + apply(simp_all add: erase_fuse) done -lemma aerase_ader: - shows "aerase (ader a r) = der a (aerase r)" +lemma erase_bder[simp]: + shows "erase (bder a r) = der a (erase r)" apply(induct r) - apply(simp_all add: aerase_fuse anullable_correctness) + apply(simp_all add: erase_fuse bnullable_correctness) done -lemma aerase_aders: - shows "aerase (aders r s) = ders s (aerase r)" +lemma erase_bders[simp]: + shows "erase (bders r s) = ders s (erase r)" apply(induct s arbitrary: r ) - apply(simp_all add: aerase_ader) + apply(simp_all) done lemma retrieve_encode_STARS: - assumes "\v\set vs. \ v : r \ code v = retrieve (internalise r) v" - shows "code (Stars vs) = retrieve (ASTAR [] (internalise r)) (Stars vs)" + assumes "\v\set vs. \ v : r \ code v = retrieve (intern r) v" + shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)" using assms apply(induct vs) + apply(simp_all) + done + +lemma retrieve_fuse2: + assumes "\ v : (erase r)" + shows "retrieve (fuse bs r) v = bs @ retrieve r v" + using assms + apply(induct r arbitrary: v bs) + using retrieve_encode_STARS + apply(auto elim!: Prf_elims) + apply(case_tac vs) apply(simp) apply(simp) done -lemma retrieve_afuse2: - assumes "\ v : (aerase r)" - shows "retrieve (fuse bs r) v = bs @ retrieve r v" +lemma retrieve_fuse: + assumes "\ v : r" + shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v" + using assms + by (simp_all add: retrieve_fuse2) + + +lemma retrieve_code: + assumes "\ v : r" + shows "code v = retrieve (intern r) v" using assms - apply(induct r arbitrary: v bs) - apply(auto) - using Prf_elims(1) apply blast - using Prf_elims(4) apply fastforce - using Prf_elims(5) apply fastforce - apply (smt Prf_elims(2) append_assoc retrieve.simps(5)) - apply(erule Prf_elims) - apply(simp) - apply(simp) - apply(erule Prf_elims) - apply(simp) - apply(case_tac vs) - apply(simp) - apply(simp) + apply(induct v r) + apply(simp_all add: retrieve_fuse retrieve_encode_STARS) done -lemma retrieve_afuse: - assumes "\ v : r" - shows "retrieve (fuse bs (internalise r)) v = bs @ retrieve (internalise r) v" - using assms - by (simp_all add: retrieve_afuse2 aerase_internalise) - -lemma retrieve_encode: - assumes "\ v : r" - shows "code v = retrieve (internalise r) v" - using assms - apply(induct v r) - apply(simp_all add: retrieve_afuse retrieve_encode_STARS) - done - -lemma Q00: - assumes "s \ r \ v" - shows "\ v : r" - using assms - apply(induct) - apply(auto intro: Prf.intros) - by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5)) - -lemma Qa: - assumes "anullable r" - shows "retrieve r (mkeps (aerase r)) = amkeps r" +lemma bmkeps_retrieve: + assumes "nullable (erase r)" + shows "bmkeps r = retrieve r (mkeps (erase r))" using assms apply(induct r) - apply(auto) - using anullable_correctness apply auto[1] - apply (simp add: anullable_correctness) - by (simp add: anullable_correctness) - + apply(auto simp add: bnullable_correctness) + done -lemma Qb: - assumes "\ v : der c (aerase r)" - shows "retrieve (ader c r) v = retrieve r (injval (aerase r) c v)" +lemma bder_retrieve: + assumes "\ v : der c (erase r)" + shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" using assms - apply(induct r arbitrary: v c) - apply(simp_all) - using Prf_elims(1) apply blast - using Prf_elims(1) apply blast - apply(auto)[1] - using Prf_elims(4) apply fastforce - using Prf_elims(1) apply blast - apply(auto split: if_splits)[1] - apply(auto elim!: Prf_elims)[1] - apply(rotate_tac 1) - apply(drule_tac x="v2" in meta_spec) - apply(drule_tac x="c" in meta_spec) - apply(drule meta_mp) - apply(simp) - apply(drule sym) - apply(simp) - apply(subst retrieve_afuse2) - apply (simp add: aerase_ader) - apply (simp add: Qa) - using anullable_correctness apply auto[1] - apply(auto elim!: Prf_elims)[1] - using anullable_correctness apply auto[1] - apply(auto elim!: Prf_elims)[1] - apply(auto elim!: Prf_elims)[1] - apply(auto elim!: Prf_elims)[1] - by (simp add: retrieve_afuse2 aerase_ader) - -lemma MAIN: - assumes "\ v : ders s r" - shows "code (flex r id s v) = retrieve (aders (internalise r) s) v" - using assms - apply(induct s arbitrary: v rule: rev_induct) - apply(simp) - apply(simp add: retrieve_encode) - apply(simp add: flex_append aders_append) - apply(subst Qb) - apply(simp add: aerase_internalise ders_append aerase_aders) - apply(simp add: aerase_aders aerase_internalise) - apply(drule_tac x="injval (ders xs r) x v" in meta_spec) - apply(drule meta_mp) - apply(simp add: Prf_injval ders_append) - apply(simp) + apply(induct r arbitrary: v) + apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve) done -fun alexer where - "alexer r s = (if anullable (aders (internalise r) s) then - decode (amkeps (aders (internalise r) s)) r else None)" +lemma MAIN_decode: + assumes "\ v : ders s r" + shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" + using assms +proof (induct s arbitrary: v rule: rev_induct) + case Nil + have "\ v : ders [] r" by fact + then have "\ v : r" by simp + then have "Some v = decode (retrieve (intern r) v) r" + using decode_code retrieve_code by auto + then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r" + by simp +next + case (snoc c s v) + have IH: "\v. \ v : ders s r \ + Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact + have asm: "\ v : ders (s @ [c]) r" by fact + then have asm2: "\ injval (ders s r) c v : ders s r" + by(simp add: Prf_injval ders_append) + have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))" + by (simp add: flex_append) + also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r" + using asm2 IH by simp + also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" + using asm by(simp_all add: bder_retrieve ders_append) + finally show "Some (flex r id (s @ [c]) v) = + decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) +qed -lemma FIN: - "alexer r s = lexer r s" - apply(auto simp add: lexer_flex) - apply (smt MAIN Q00 Qa aerase_aders aerase_internalise decode_code lexer_correctness(1) lexer_flex mkeps_nullable) - apply (metis aerase_aders aerase_internalise anullable_correctness) - using aerase_aders aerase_internalise anullable_correctness by force +definition blexer where + "blexer r s \ if bnullable (bders (intern r) s) then + decode (bmkeps (bders (intern r) s)) r else None" + +lemma blexer_correctness: + shows "blexer r s = lexer r s" +proof - + { define bds where "bds \ bders (intern r) s" + define ds where "ds \ ders s r" + assume asm: "nullable ds" + have era: "erase bds = ds" + unfolding ds_def bds_def by simp + have mke: "\ mkeps ds : ds" + using asm by (simp add: mkeps_nullable) + have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r" + using bmkeps_retrieve + using asm era by (simp add: bmkeps_retrieve) + also have "... = Some (flex r id s (mkeps ds))" + using mke by (simp_all add: MAIN_decode ds_def bds_def) + finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" + unfolding bds_def ds_def . + } + then show "blexer r s = lexer r s" + unfolding blexer_def lexer_flex + by(auto simp add: bnullable_correctness[symmetric]) +qed unused_thms diff -r 9ab8609c66c5 -r 807acaf7f599 thys/journal.pdf Binary file thys/journal.pdf has changed