equal
deleted
inserted
replaced
3 imports |
3 imports |
4 "../Lexer" |
4 "../Lexer" |
5 "../Simplifying" |
5 "../Simplifying" |
6 "../Positions" |
6 "../Positions" |
7 "../Sulzmann" |
7 "../Sulzmann" |
|
8 (* "../SizeBound" *) |
8 "HOL-Library.LaTeXsugar" |
9 "HOL-Library.LaTeXsugar" |
9 begin |
10 begin |
10 |
11 |
11 lemma Suc_0_fold: |
12 lemma Suc_0_fold: |
12 "Suc 0 = 1" |
13 "Suc 0 = 1" |
1383 \<close> |
1384 \<close> |
1384 |
1385 |
1385 section \<open>Bitcoded Lexing\<close> |
1386 section \<open>Bitcoded Lexing\<close> |
1386 |
1387 |
1387 |
1388 |
|
1389 |
|
1390 |
1388 text \<open> |
1391 text \<open> |
1389 |
1392 |
1390 Incremental calculation of the value. To simplify the proof we first define the function |
1393 Incremental calculation of the value. To simplify the proof we first define the function |
1391 @{const flex} which calculates the ``iterated'' injection function. With this we can |
1394 @{const flex} which calculates the ``iterated'' injection function. With this we can |
1392 rewrite the lexer as |
1395 rewrite the lexer as |
1410 \begin{center} |
1413 \begin{center} |
1411 \begin{tabular}{lcl} |
1414 \begin{tabular}{lcl} |
1412 @{term areg} & $::=$ & @{term "AZERO"}\\ |
1415 @{term areg} & $::=$ & @{term "AZERO"}\\ |
1413 & $\mid$ & @{term "AONE bs"}\\ |
1416 & $\mid$ & @{term "AONE bs"}\\ |
1414 & $\mid$ & @{term "ACH bs c"}\\ |
1417 & $\mid$ & @{term "ACH bs c"}\\ |
1415 & $\mid$ & @{term "AALT bs r\<^sub>1 r\<^sub>2"}\\ |
1418 & $\mid$ & @{term "AALT bs r1 r2"}\\ |
1416 & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ |
1419 & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ |
1417 & $\mid$ & @{term "ASTAR bs r"} |
1420 & $\mid$ & @{term "ASTAR bs r"} |
1418 \end{tabular} |
1421 \end{tabular} |
1419 \end{center} |
1422 \end{center} |
|
1423 |
1420 |
1424 |
1421 \begin{center} |
1425 \begin{center} |
1422 \begin{tabular}{lcl} |
1426 \begin{tabular}{lcl} |
1423 @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\ |
1427 @{thm (lhs) intern.simps(1)} & $\dn$ & @{thm (rhs) intern.simps(1)}\\ |
1424 @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\ |
1428 @{thm (lhs) intern.simps(2)} & $\dn$ & @{thm (rhs) intern.simps(2)}\\ |