16 \S\ref{sec:boolex}. This time we do not commit ourselves to a particular |
29 \S\ref{sec:boolex}. This time we do not commit ourselves to a particular |
17 type of variables or values but make them type parameters. Neither is there |
30 type of variables or values but make them type parameters. Neither is there |
18 a fixed set of binary operations: instead the expression contains the |
31 a fixed set of binary operations: instead the expression contains the |
19 appropriate function itself.% |
32 appropriate function itself.% |
20 \end{isamarkuptext}% |
33 \end{isamarkuptext}% |
21 \isamarkuptrue% |
34 \isamarkupfalse% |
22 \isacommand{types}\ {\isacharprime}v\ binop\ {\isacharequal}\ {\isachardoublequote}{\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline |
35 \isacommand{types}\ {\isacharprime}v\ binop\ {\isacharequal}\ {\isachardoublequote}{\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline |
23 \isamarkupfalse% |
36 \isamarkupfalse% |
24 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isacharequal}\ Cex\ {\isacharprime}v\isanewline |
37 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isacharequal}\ Cex\ {\isacharprime}v\isanewline |
25 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Vex\ {\isacharprime}a\isanewline |
38 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Vex\ {\isacharprime}a\isanewline |
26 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Bex\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr{\isachardoublequote}\isamarkupfalse% |
39 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Bex\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr{\isachardoublequote}\ \ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr{\isachardoublequote}\isamarkuptrue% |
27 % |
40 % |
28 \begin{isamarkuptext}% |
41 \begin{isamarkuptext}% |
29 \noindent |
42 \noindent |
30 The three constructors represent constants, variables and the application of |
43 The three constructors represent constants, variables and the application of |
31 a binary operation to two subexpressions. |
44 a binary operation to two subexpressions. |
32 |
45 |
33 The value of an expression with respect to an environment that maps variables to |
46 The value of an expression with respect to an environment that maps variables to |
34 values is easily defined:% |
47 values is easily defined:% |
35 \end{isamarkuptext}% |
48 \end{isamarkuptext}% |
36 \isamarkuptrue% |
49 \isamarkupfalse% |
37 \isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline |
50 \isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline |
38 \isamarkupfalse% |
51 \isamarkupfalse% |
39 \isacommand{primrec}\isanewline |
52 \isacommand{primrec}\isanewline |
40 {\isachardoublequote}value\ {\isacharparenleft}Cex\ v{\isacharparenright}\ env\ {\isacharequal}\ v{\isachardoublequote}\isanewline |
53 {\isachardoublequote}value\ {\isacharparenleft}Cex\ v{\isacharparenright}\ env\ {\isacharequal}\ v{\isachardoublequote}\isanewline |
41 {\isachardoublequote}value\ {\isacharparenleft}Vex\ a{\isacharparenright}\ env\ {\isacharequal}\ env\ a{\isachardoublequote}\isanewline |
54 {\isachardoublequote}value\ {\isacharparenleft}Vex\ a{\isacharparenright}\ env\ {\isacharequal}\ env\ a{\isachardoublequote}\isanewline |
42 {\isachardoublequote}value\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ f\ {\isacharparenleft}value\ e{\isadigit{1}}\ env{\isacharparenright}\ {\isacharparenleft}value\ e{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
55 {\isachardoublequote}value\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ f\ {\isacharparenleft}value\ e{\isadigit{1}}\ env{\isacharparenright}\ {\isacharparenleft}value\ e{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
43 % |
56 % |
44 \begin{isamarkuptext}% |
57 \begin{isamarkuptext}% |
45 The stack machine has three instructions: load a constant value onto the |
58 The stack machine has three instructions: load a constant value onto the |
46 stack, load the contents of an address onto the stack, and apply a |
59 stack, load the contents of an address onto the stack, and apply a |
47 binary operation to the two topmost elements of the stack, replacing them by |
60 binary operation to the two topmost elements of the stack, replacing them by |
48 the result. As for \isa{expr}, addresses and values are type parameters:% |
61 the result. As for \isa{expr}, addresses and values are type parameters:% |
49 \end{isamarkuptext}% |
62 \end{isamarkuptext}% |
50 \isamarkuptrue% |
63 \isamarkupfalse% |
51 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ instr\ {\isacharequal}\ Const\ {\isacharprime}v\isanewline |
64 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}\ instr\ {\isacharequal}\ Const\ {\isacharprime}v\isanewline |
52 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Load\ {\isacharprime}a\isanewline |
65 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Load\ {\isacharprime}a\isanewline |
53 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Apply\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}\isamarkupfalse% |
66 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ Apply\ {\isachardoublequote}{\isacharprime}v\ binop{\isachardoublequote}\isamarkuptrue% |
54 % |
67 % |
55 \begin{isamarkuptext}% |
68 \begin{isamarkuptext}% |
56 The execution of the stack machine is modelled by a function |
69 The execution of the stack machine is modelled by a function |
57 \isa{exec} that takes a list of instructions, a store (modelled as a |
70 \isa{exec} that takes a list of instructions, a store (modelled as a |
58 function from addresses to values, just like the environment for |
71 function from addresses to values, just like the environment for |
59 evaluating expressions), and a stack (modelled as a list) of values, |
72 evaluating expressions), and a stack (modelled as a list) of values, |
60 and returns the stack at the end of the execution --- the store remains |
73 and returns the stack at the end of the execution --- the store remains |
61 unchanged:% |
74 unchanged:% |
62 \end{isamarkuptext}% |
75 \end{isamarkuptext}% |
63 \isamarkuptrue% |
76 \isamarkupfalse% |
64 \isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v\ list\ {\isasymRightarrow}\ {\isacharprime}v\ list{\isachardoublequote}\isanewline |
77 \isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isasymRightarrow}{\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v\ list\ {\isasymRightarrow}\ {\isacharprime}v\ list{\isachardoublequote}\isanewline |
65 \isamarkupfalse% |
78 \isamarkupfalse% |
66 \isacommand{primrec}\isanewline |
79 \isacommand{primrec}\isanewline |
67 {\isachardoublequote}exec\ {\isacharbrackleft}{\isacharbrackright}\ s\ vs\ {\isacharequal}\ vs{\isachardoublequote}\isanewline |
80 {\isachardoublequote}exec\ {\isacharbrackleft}{\isacharbrackright}\ s\ vs\ {\isacharequal}\ vs{\isachardoublequote}\isanewline |
68 {\isachardoublequote}exec\ {\isacharparenleft}i{\isacharhash}is{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}case\ i\ of\isanewline |
81 {\isachardoublequote}exec\ {\isacharparenleft}i{\isacharhash}is{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}case\ i\ of\isanewline |
69 \ \ \ \ Const\ v\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}v{\isacharhash}vs{\isacharparenright}\isanewline |
82 \ \ \ \ Const\ v\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}v{\isacharhash}vs{\isacharparenright}\isanewline |
70 \ \ {\isacharbar}\ Load\ a\ \ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}s\ a{\isacharparenright}{\isacharhash}vs{\isacharparenright}\isanewline |
83 \ \ {\isacharbar}\ Load\ a\ \ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}s\ a{\isacharparenright}{\isacharhash}vs{\isacharparenright}\isanewline |
71 \ \ {\isacharbar}\ Apply\ f\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}f\ {\isacharparenleft}hd\ vs{\isacharparenright}\ {\isacharparenleft}hd{\isacharparenleft}tl\ vs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharhash}{\isacharparenleft}tl{\isacharparenleft}tl\ vs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
84 \ \ {\isacharbar}\ Apply\ f\ \ {\isasymRightarrow}\ exec\ is\ s\ {\isacharparenleft}{\isacharparenleft}f\ {\isacharparenleft}hd\ vs{\isacharparenright}\ {\isacharparenleft}hd{\isacharparenleft}tl\ vs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharhash}{\isacharparenleft}tl{\isacharparenleft}tl\ vs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkuptrue% |
72 % |
85 % |
73 \begin{isamarkuptext}% |
86 \begin{isamarkuptext}% |
74 \noindent |
87 \noindent |
75 Recall that \isa{hd} and \isa{tl} |
88 Recall that \isa{hd} and \isa{tl} |
76 return the first element and the remainder of a list. |
89 return the first element and the remainder of a list. |
81 with fewer than two elements on the stack. |
94 with fewer than two elements on the stack. |
82 |
95 |
83 The compiler is a function from expressions to a list of instructions. Its |
96 The compiler is a function from expressions to a list of instructions. Its |
84 definition is obvious:% |
97 definition is obvious:% |
85 \end{isamarkuptext}% |
98 \end{isamarkuptext}% |
86 \isamarkuptrue% |
99 \isamarkupfalse% |
87 \isacommand{consts}\ comp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequote}\isanewline |
100 \isacommand{consts}\ comp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequote}\isanewline |
88 \isamarkupfalse% |
101 \isamarkupfalse% |
89 \isacommand{primrec}\isanewline |
102 \isacommand{primrec}\isanewline |
90 {\isachardoublequote}comp\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequote}\isanewline |
103 {\isachardoublequote}comp\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequote}\isanewline |
91 {\isachardoublequote}comp\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequote}\isanewline |
104 {\isachardoublequote}comp\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequote}\isanewline |
92 {\isachardoublequote}comp\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}comp\ e{\isadigit{2}}{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}comp\ e{\isadigit{1}}{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}Apply\ f{\isacharbrackright}{\isachardoublequote}\isamarkupfalse% |
105 {\isachardoublequote}comp\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}comp\ e{\isadigit{2}}{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}comp\ e{\isadigit{1}}{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}Apply\ f{\isacharbrackright}{\isachardoublequote}\isamarkuptrue% |
93 % |
106 % |
94 \begin{isamarkuptext}% |
107 \begin{isamarkuptext}% |
95 Now we have to prove the correctness of the compiler, i.e.\ that the |
108 Now we have to prove the correctness of the compiler, i.e.\ that the |
96 execution of a compiled expression results in the value of the expression:% |
109 execution of a compiled expression results in the value of the expression:% |
97 \end{isamarkuptext}% |
110 \end{isamarkuptext}% |
98 \isamarkuptrue% |
111 \isamarkupfalse% |
99 \isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}\isamarkupfalse% |
112 \isacommand{theorem}\ {\isachardoublequote}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequote}% |
100 \isamarkupfalse% |
113 \isadelimproof |
|
114 % |
|
115 \endisadelimproof |
|
116 % |
|
117 \isatagproof |
|
118 % |
|
119 \endisatagproof |
|
120 {\isafoldproof}% |
|
121 % |
|
122 \isadelimproof |
|
123 % |
|
124 \endisadelimproof |
|
125 \isamarkuptrue% |
101 % |
126 % |
102 \begin{isamarkuptext}% |
127 \begin{isamarkuptext}% |
103 \noindent |
128 \noindent |
104 This theorem needs to be generalized:% |
129 This theorem needs to be generalized:% |
105 \end{isamarkuptext}% |
130 \end{isamarkuptext}% |
106 \isamarkuptrue% |
131 \isamarkupfalse% |
107 \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}\isamarkupfalse% |
132 \isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}% |
|
133 \isadelimproof |
|
134 % |
|
135 \endisadelimproof |
|
136 % |
|
137 \isatagproof |
|
138 \isamarkuptrue% |
108 % |
139 % |
109 \begin{isamarkuptxt}% |
140 \begin{isamarkuptxt}% |
110 \noindent |
141 \noindent |
111 It will be proved by induction on \isa{e} followed by simplification. |
142 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 |
143 First, we must prove a lemma about executing the concatenation of two |
113 instruction sequences:% |
144 instruction sequences:% |
114 \end{isamarkuptxt}% |
145 \end{isamarkuptxt}% |
115 \isamarkuptrue% |
146 % |
|
147 \endisatagproof |
|
148 {\isafoldproof}% |
|
149 % |
|
150 \isadelimproof |
|
151 % |
|
152 \endisadelimproof |
116 \isamarkupfalse% |
153 \isamarkupfalse% |
117 \isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
154 \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% |
155 \ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}% |
|
156 \isadelimproof |
|
157 % |
|
158 \endisadelimproof |
|
159 % |
|
160 \isatagproof |
|
161 \isamarkuptrue% |
119 % |
162 % |
120 \begin{isamarkuptxt}% |
163 \begin{isamarkuptxt}% |
121 \noindent |
164 \noindent |
122 This requires induction on \isa{xs} and ordinary simplification for the |
165 This requires induction on \isa{xs} and ordinary simplification for the |
123 base cases. In the induction step, simplification leaves us with a formula |
166 base cases. In the induction step, simplification leaves us with a formula |
124 that contains two \isa{case}-expressions over instructions. Thus we add |
167 that contains two \isa{case}-expressions over instructions. Thus we add |
125 automatic case splitting, which finishes the proof:% |
168 automatic case splitting, which finishes the proof:% |
126 \end{isamarkuptxt}% |
169 \end{isamarkuptxt}% |
127 \isamarkuptrue% |
170 \isamarkupfalse% |
128 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse% |
171 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
129 \isamarkupfalse% |
172 \endisatagproof |
|
173 {\isafoldproof}% |
|
174 % |
|
175 \isadelimproof |
|
176 % |
|
177 \endisadelimproof |
|
178 \isamarkuptrue% |
130 % |
179 % |
131 \begin{isamarkuptext}% |
180 \begin{isamarkuptext}% |
132 \noindent |
181 \noindent |
133 Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can |
182 Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can |
134 be modified in the same way as \isa{simp}. Thus the proof can be |
183 be modified in the same way as \isa{simp}. Thus the proof can be |
135 rewritten as% |
184 rewritten as% |
136 \end{isamarkuptext}% |
185 \end{isamarkuptext}% |
137 \isamarkuptrue% |
186 % |
138 \isamarkupfalse% |
187 \isadelimproof |
139 \isamarkupfalse% |
188 % |
140 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse% |
189 \endisadelimproof |
141 \isamarkupfalse% |
190 % |
|
191 \isatagproof |
|
192 \isamarkupfalse% |
|
193 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}% |
|
194 \endisatagproof |
|
195 {\isafoldproof}% |
|
196 % |
|
197 \isadelimproof |
|
198 % |
|
199 \endisadelimproof |
|
200 \isamarkuptrue% |
142 % |
201 % |
143 \begin{isamarkuptext}% |
202 \begin{isamarkuptext}% |
144 \noindent |
203 \noindent |
145 Although this is more compact, it is less clear for the reader of the proof. |
204 Although this is more compact, it is less clear for the reader of the proof. |
146 |
205 |