equal
deleted
inserted
replaced
111 It will be proved by induction on \isa{e} followed by simplification. |
111 It will be proved by induction on \isa{e} followed by simplification. |
112 First, we must prove a lemma about executing the concatenation of two |
112 First, we must prove a lemma about executing the concatenation of two |
113 instruction sequences:% |
113 instruction sequences:% |
114 \end{isamarkuptxt}% |
114 \end{isamarkuptxt}% |
115 \isamarkuptrue% |
115 \isamarkuptrue% |
|
116 \isanewline |
116 \isamarkupfalse% |
117 \isamarkupfalse% |
117 \isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
118 \isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
118 \ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
119 \ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
119 % |
120 % |
120 \begin{isamarkuptxt}% |
121 \begin{isamarkuptxt}% |
134 be modified in the same way as \isa{simp}. Thus the proof can be |
135 be modified in the same way as \isa{simp}. Thus the proof can be |
135 rewritten as% |
136 rewritten as% |
136 \end{isamarkuptext}% |
137 \end{isamarkuptext}% |
137 \isamarkuptrue% |
138 \isamarkuptrue% |
138 \isamarkupfalse% |
139 \isamarkupfalse% |
|
140 \isanewline |
139 \isamarkupfalse% |
141 \isamarkupfalse% |
140 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse% |
142 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse% |
141 \isamarkupfalse% |
143 \isamarkupfalse% |
142 % |
144 % |
143 \begin{isamarkuptext}% |
145 \begin{isamarkuptext}% |
151 \index{compiling expressions example|)}% |
153 \index{compiling expressions example|)}% |
152 \end{isamarkuptext}% |
154 \end{isamarkuptext}% |
153 \isamarkuptrue% |
155 \isamarkuptrue% |
154 \isamarkupfalse% |
156 \isamarkupfalse% |
155 \isamarkupfalse% |
157 \isamarkupfalse% |
|
158 \isanewline |
156 \isamarkupfalse% |
159 \isamarkupfalse% |
157 \end{isabellebody}% |
160 \end{isabellebody}% |
158 %%% Local Variables: |
161 %%% Local Variables: |
159 %%% mode: latex |
162 %%% mode: latex |
160 %%% TeX-master: "root" |
163 %%% TeX-master: "root" |