54 Hence the function \isa{value} takes an additional parameter, an |
54 Hence the function \isa{value} takes an additional parameter, an |
55 \emph{environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to their |
55 \emph{environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to their |
56 values:% |
56 values:% |
57 \end{isamarkuptext}% |
57 \end{isamarkuptext}% |
58 \isamarkuptrue% |
58 \isamarkuptrue% |
59 \isacommand{consts}\isamarkupfalse% |
59 \isacommand{primrec}\isamarkupfalse% |
60 \ {\isachardoublequoteopen}value{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
60 \ {\isachardoublequoteopen}value{\isachardoublequoteclose}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
61 \isacommand{primrec}\isamarkupfalse% |
61 {\isachardoublequoteopen}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
62 \isanewline |
62 {\isachardoublequoteopen}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
63 {\isachardoublequoteopen}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequoteclose}\isanewline |
63 {\isachardoublequoteopen}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
64 {\isachardoublequoteopen}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\isanewline |
|
65 {\isachardoublequoteopen}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
66 {\isachardoublequoteopen}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequoteclose}% |
64 {\isachardoublequoteopen}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequoteclose}% |
67 \begin{isamarkuptext}% |
65 \begin{isamarkuptext}% |
68 \noindent |
66 \noindent |
69 \subsubsection{If-Expressions} |
67 \subsubsection{If-Expressions} |
70 |
68 |
79 \begin{isamarkuptext}% |
77 \begin{isamarkuptext}% |
80 \noindent |
78 \noindent |
81 The evaluation of If-expressions proceeds as for \isa{boolex}:% |
79 The evaluation of If-expressions proceeds as for \isa{boolex}:% |
82 \end{isamarkuptext}% |
80 \end{isamarkuptext}% |
83 \isamarkuptrue% |
81 \isamarkuptrue% |
84 \isacommand{consts}\isamarkupfalse% |
82 \isacommand{primrec}\isamarkupfalse% |
85 \ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
83 \ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
86 \isacommand{primrec}\isamarkupfalse% |
84 {\isachardoublequoteopen}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
87 \isanewline |
85 {\isachardoublequoteopen}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
88 {\isachardoublequoteopen}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequoteclose}\isanewline |
|
89 {\isachardoublequoteopen}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequoteclose}\isanewline |
|
90 {\isachardoublequoteopen}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline |
86 {\isachardoublequoteopen}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline |
91 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequoteclose}% |
87 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequoteclose}% |
92 \begin{isamarkuptext}% |
88 \begin{isamarkuptext}% |
93 \subsubsection{Converting Boolean and If-Expressions} |
89 \subsubsection{Converting Boolean and If-Expressions} |
94 |
90 |
95 The type \isa{boolex} is close to the customary representation of logical |
91 The type \isa{boolex} is close to the customary representation of logical |
96 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to |
92 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to |
97 translate from \isa{boolex} into \isa{ifex}:% |
93 translate from \isa{boolex} into \isa{ifex}:% |
98 \end{isamarkuptext}% |
94 \end{isamarkuptext}% |
99 \isamarkuptrue% |
95 \isamarkuptrue% |
100 \isacommand{consts}\isamarkupfalse% |
96 \isacommand{primrec}\isamarkupfalse% |
101 \ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\isanewline |
97 \ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
102 \isacommand{primrec}\isamarkupfalse% |
98 {\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
103 \isanewline |
99 {\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
104 {\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\isanewline |
100 {\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}\ {\isacharparenleft}CIF\ True{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
105 {\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\isanewline |
|
106 {\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}\ {\isacharparenleft}CIF\ True{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
107 {\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}bool{\isadigit{2}}if\ c{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}{\isachardoublequoteclose}% |
101 {\isachardoublequoteopen}bool{\isadigit{2}}if\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}bool{\isadigit{2}}if\ c{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}{\isachardoublequoteclose}% |
108 \begin{isamarkuptext}% |
102 \begin{isamarkuptext}% |
109 \noindent |
103 \noindent |
110 At last, we have something we can verify: that \isa{bool{\isadigit{2}}if} preserves the |
104 At last, we have something we can verify: that \isa{bool{\isadigit{2}}if} preserves the |
111 value of its argument:% |
105 value of its argument:% |
148 repeatedly replacing a subterm of the form \isa{IF\ {\isacharparenleft}IF\ b\ x\ y{\isacharparenright}\ z\ u} by |
142 repeatedly replacing a subterm of the form \isa{IF\ {\isacharparenleft}IF\ b\ x\ y{\isacharparenright}\ z\ u} by |
149 \isa{IF\ b\ {\isacharparenleft}IF\ x\ z\ u{\isacharparenright}\ {\isacharparenleft}IF\ y\ z\ u{\isacharparenright}}, which has the same value. The following |
143 \isa{IF\ b\ {\isacharparenleft}IF\ x\ z\ u{\isacharparenright}\ {\isacharparenleft}IF\ y\ z\ u{\isacharparenright}}, which has the same value. The following |
150 primitive recursive functions perform this task:% |
144 primitive recursive functions perform this task:% |
151 \end{isamarkuptext}% |
145 \end{isamarkuptext}% |
152 \isamarkuptrue% |
146 \isamarkuptrue% |
153 \isacommand{consts}\isamarkupfalse% |
147 \isacommand{primrec}\isamarkupfalse% |
154 \ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\isanewline |
148 \ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
155 \isacommand{primrec}\isamarkupfalse% |
149 {\isachardoublequoteopen}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
156 \isanewline |
150 {\isachardoublequoteopen}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
157 {\isachardoublequoteopen}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequoteclose}\isanewline |
|
158 {\isachardoublequoteopen}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequoteclose}\isanewline |
|
159 {\isachardoublequoteopen}normif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ u\ f\ {\isacharequal}\ normif\ b\ {\isacharparenleft}normif\ t\ u\ f{\isacharparenright}\ {\isacharparenleft}normif\ e\ u\ f{\isacharparenright}{\isachardoublequoteclose}\isanewline |
151 {\isachardoublequoteopen}normif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ u\ f\ {\isacharequal}\ normif\ b\ {\isacharparenleft}normif\ t\ u\ f{\isacharparenright}\ {\isacharparenleft}normif\ e\ u\ f{\isacharparenright}{\isachardoublequoteclose}\isanewline |
160 \isanewline |
152 \isanewline |
161 \isacommand{consts}\isamarkupfalse% |
153 \isacommand{primrec}\isamarkupfalse% |
162 \ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\isanewline |
154 \ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
163 \isacommand{primrec}\isamarkupfalse% |
155 {\isachardoublequoteopen}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
164 \isanewline |
156 {\isachardoublequoteopen}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
165 {\isachardoublequoteopen}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequoteclose}\isanewline |
|
166 {\isachardoublequoteopen}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequoteclose}\isanewline |
|
167 {\isachardoublequoteopen}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequoteclose}% |
157 {\isachardoublequoteopen}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequoteclose}% |
168 \begin{isamarkuptext}% |
158 \begin{isamarkuptext}% |
169 \noindent |
159 \noindent |
170 Their interplay is tricky; we leave it to you to develop an |
160 Their interplay is tricky; we leave it to you to develop an |
171 intuitive understanding. Fortunately, Isabelle can help us to verify that the |
161 intuitive understanding. Fortunately, Isabelle can help us to verify that the |
229 |
219 |
230 But how can we be sure that \isa{norm} really produces a normal form in |
220 But how can we be sure that \isa{norm} really produces a normal form in |
231 the above sense? We define a function that tests If-expressions for normality:% |
221 the above sense? We define a function that tests If-expressions for normality:% |
232 \end{isamarkuptext}% |
222 \end{isamarkuptext}% |
233 \isamarkuptrue% |
223 \isamarkuptrue% |
234 \isacommand{consts}\isamarkupfalse% |
224 \isacommand{primrec}\isamarkupfalse% |
235 \ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
225 \ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}ifex\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
236 \isacommand{primrec}\isamarkupfalse% |
226 {\isachardoublequoteopen}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
237 \isanewline |
227 {\isachardoublequoteopen}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
238 {\isachardoublequoteopen}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline |
|
239 {\isachardoublequoteopen}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequoteclose}\isanewline |
|
240 {\isachardoublequoteopen}normal{\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline |
228 {\isachardoublequoteopen}normal{\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline |
241 \ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
229 \ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
242 \begin{isamarkuptext}% |
230 \begin{isamarkuptext}% |
243 \noindent |
231 \noindent |
244 Now we prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about |
232 Now we prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about |