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