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 "~~/src/HOL/Library/LaTeXsugar" |
8 "HOL-Library.LaTeXsugar" |
9 begin |
9 begin |
10 |
10 |
11 lemma Suc_0_fold: |
11 lemma Suc_0_fold: |
12 "Suc 0 = 1" |
12 "Suc 0 = 1" |
13 by simp |
13 by simp |
48 If ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and |
48 If ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10) and |
49 Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) and |
49 Cons ("_\<^latex>\<open>\\mbox{$\\,$}\<close>::\<^latex>\<open>\\mbox{$\\,$}\<close>_" [75,73] 73) and |
50 |
50 |
51 ZERO ("\<^bold>0" 81) and |
51 ZERO ("\<^bold>0" 81) and |
52 ONE ("\<^bold>1" 81) and |
52 ONE ("\<^bold>1" 81) and |
53 CHAR ("_" [1000] 80) and |
53 CH ("_" [1000] 80) and |
54 ALT ("_ + _" [77,77] 78) and |
54 ALT ("_ + _" [77,77] 78) and |
55 SEQ ("_ \<cdot> _" [77,77] 78) and |
55 SEQ ("_ \<cdot> _" [77,77] 78) and |
56 STAR ("_\<^sup>\<star>" [79] 78) and |
56 STAR ("_\<^sup>\<star>" [79] 78) and |
57 |
57 |
58 val.Void ("Empty" 78) and |
58 val.Void ("Empty" 78) and |
331 |
331 |
332 \begin{center} |
332 \begin{center} |
333 \<open>r :=\<close> |
333 \<open>r :=\<close> |
334 @{const "ZERO"} $\mid$ |
334 @{const "ZERO"} $\mid$ |
335 @{const "ONE"} $\mid$ |
335 @{const "ONE"} $\mid$ |
336 @{term "CHAR c"} $\mid$ |
336 @{term "CH c"} $\mid$ |
337 @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$ |
337 @{term "ALT r\<^sub>1 r\<^sub>2"} $\mid$ |
338 @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$ |
338 @{term "SEQ r\<^sub>1 r\<^sub>2"} $\mid$ |
339 @{term "STAR r"} |
339 @{term "STAR r"} |
340 \end{center} |
340 \end{center} |
341 |
341 |
1409 |
1409 |
1410 \begin{center} |
1410 \begin{center} |
1411 \begin{tabular}{lcl} |
1411 \begin{tabular}{lcl} |
1412 @{term areg} & $::=$ & @{term "AZERO"}\\ |
1412 @{term areg} & $::=$ & @{term "AZERO"}\\ |
1413 & $\mid$ & @{term "AONE bs"}\\ |
1413 & $\mid$ & @{term "AONE bs"}\\ |
1414 & $\mid$ & @{term "ACHAR bs c"}\\ |
1414 & $\mid$ & @{term "ACH bs c"}\\ |
1415 & $\mid$ & @{term "AALT bs r\<^sub>1 r\<^sub>2"}\\ |
1415 & $\mid$ & @{term "AALT bs r\<^sub>1 r\<^sub>2"}\\ |
1416 & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ |
1416 & $\mid$ & @{term "ASEQ bs r\<^sub>1 r\<^sub>2"}\\ |
1417 & $\mid$ & @{term "ASTAR bs r"} |
1417 & $\mid$ & @{term "ASTAR bs r"} |
1418 \end{tabular} |
1418 \end{tabular} |
1419 \end{center} |
1419 \end{center} |
1691 |
1691 |
1692 \begin{proof} |
1692 \begin{proof} |
1693 By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are |
1693 By induction on the definition of @{term "erase r"}. The cases for rule 1) and 2) are |
1694 straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to |
1694 straightforward as @{term "der c ZERO"} and @{term "der c ONE"} are both equal to |
1695 @{term ZERO}. This means @{term "\<Turnstile> v : ZERO"} cannot hold. Similarly in case of rule 3) |
1695 @{term ZERO}. This means @{term "\<Turnstile> v : ZERO"} cannot hold. Similarly in case of rule 3) |
1696 where @{term r} is of the form @{term "ACHAR d"} with @{term "c = d"}. Then by assumption |
1696 where @{term r} is of the form @{term "ACH d"} with @{term "c = d"}. Then by assumption |
1697 we know @{term "\<Turnstile> v : ONE"}, which implies @{term "v = Void"}. The equation follows by |
1697 we know @{term "\<Turnstile> v : ONE"}, which implies @{term "v = Void"}. The equation follows by |
1698 simplification of left- and right-hand side. In case @{term "c \<noteq> d"} we have again |
1698 simplification of left- and right-hand side. In case @{term "c \<noteq> d"} we have again |
1699 @{term "\<Turnstile> v : ZERO"}, which cannot hold. |
1699 @{term "\<Turnstile> v : ZERO"}, which cannot hold. |
1700 |
1700 |
1701 For rule 4a) we have again @{term "\<Turnstile> v : ZERO"}. The property holds by IH for rule 4b). |
1701 For rule 4a) we have again @{term "\<Turnstile> v : ZERO"}. The property holds by IH for rule 4b). |