1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Ifexpr}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isamarkupsubsection{Case Study: Boolean Expressions% |
|
19 } |
|
20 \isamarkuptrue% |
|
21 % |
|
22 \begin{isamarkuptext}% |
|
23 \label{sec:boolex}\index{boolean expressions example|(} |
|
24 The aim of this case study is twofold: it shows how to model boolean |
|
25 expressions and some algorithms for manipulating them, and it demonstrates |
|
26 the constructs introduced above.% |
|
27 \end{isamarkuptext}% |
|
28 \isamarkuptrue% |
|
29 % |
|
30 \isamarkupsubsubsection{Modelling Boolean Expressions% |
|
31 } |
|
32 \isamarkuptrue% |
|
33 % |
|
34 \begin{isamarkuptext}% |
|
35 We want to represent boolean expressions built up from variables and |
|
36 constants by negation and conjunction. The following datatype serves exactly |
|
37 that purpose:% |
|
38 \end{isamarkuptext}% |
|
39 \isamarkuptrue% |
|
40 \isacommand{datatype}\isamarkupfalse% |
|
41 \ boolex\ {\isaliteral{3D}{\isacharequal}}\ Const\ bool\ {\isaliteral{7C}{\isacharbar}}\ Var\ nat\ {\isaliteral{7C}{\isacharbar}}\ Neg\ boolex\isanewline |
|
42 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ And\ boolex\ boolex% |
|
43 \begin{isamarkuptext}% |
|
44 \noindent |
|
45 The two constants are represented by \isa{Const\ True} and |
|
46 \isa{Const\ False}. Variables are represented by terms of the form |
|
47 \isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}). |
|
48 For example, the formula $P@0 \land \neg P@1$ is represented by the term |
|
49 \isa{And\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Neg\ {\isaliteral{28}{\isacharparenleft}}Var\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}. |
|
50 |
|
51 \subsubsection{The Value of a Boolean Expression} |
|
52 |
|
53 The value of a boolean expression depends on the value of its variables. |
|
54 Hence the function \isa{value} takes an additional parameter, an |
|
55 \emph{environment} of type \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}, which maps variables to their |
|
56 values:% |
|
57 \end{isamarkuptext}% |
|
58 \isamarkuptrue% |
|
59 \isacommand{primrec}\isamarkupfalse% |
|
60 \ {\isaliteral{22}{\isachardoublequoteopen}}value{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}boolex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
61 {\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}Const\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
62 {\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}Var\ x{\isaliteral{29}{\isacharparenright}}\ \ \ env\ {\isaliteral{3D}{\isacharequal}}\ env\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
63 {\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ \ \ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ value\ b\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
64 {\isaliteral{22}{\isachardoublequoteopen}}value\ {\isaliteral{28}{\isacharparenleft}}And\ b\ c{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}value\ b\ env\ {\isaliteral{5C3C616E643E}{\isasymand}}\ value\ c\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
65 \begin{isamarkuptext}% |
|
66 \noindent |
|
67 \subsubsection{If-Expressions} |
|
68 |
|
69 An alternative and often more efficient (because in a certain sense |
|
70 canonical) representation are so-called \emph{If-expressions} built up |
|
71 from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals |
|
72 (\isa{IF}):% |
|
73 \end{isamarkuptext}% |
|
74 \isamarkuptrue% |
|
75 \isacommand{datatype}\isamarkupfalse% |
|
76 \ ifex\ {\isaliteral{3D}{\isacharequal}}\ CIF\ bool\ {\isaliteral{7C}{\isacharbar}}\ VIF\ nat\ {\isaliteral{7C}{\isacharbar}}\ IF\ ifex\ ifex\ ifex% |
|
77 \begin{isamarkuptext}% |
|
78 \noindent |
|
79 The evaluation of If-expressions proceeds as for \isa{boolex}:% |
|
80 \end{isamarkuptext}% |
|
81 \isamarkuptrue% |
|
82 \isacommand{primrec}\isamarkupfalse% |
|
83 \ valif\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
84 {\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}CIF\ b{\isaliteral{29}{\isacharparenright}}\ \ \ \ env\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
85 {\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}VIF\ x{\isaliteral{29}{\isacharparenright}}\ \ \ \ env\ {\isaliteral{3D}{\isacharequal}}\ env\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
86 {\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline |
|
87 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
88 \begin{isamarkuptext}% |
|
89 \subsubsection{Converting Boolean and If-Expressions} |
|
90 |
|
91 The type \isa{boolex} is close to the customary representation of logical |
|
92 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to |
|
93 translate from \isa{boolex} into \isa{ifex}:% |
|
94 \end{isamarkuptext}% |
|
95 \isamarkuptrue% |
|
96 \isacommand{primrec}\isamarkupfalse% |
|
97 \ bool{\isadigit{2}}if\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}boolex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ ifex{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
98 {\isaliteral{22}{\isachardoublequoteopen}}bool{\isadigit{2}}if\ {\isaliteral{28}{\isacharparenleft}}Const\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ CIF\ b{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
99 {\isaliteral{22}{\isachardoublequoteopen}}bool{\isadigit{2}}if\ {\isaliteral{28}{\isacharparenleft}}Var\ x{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{3D}{\isacharequal}}\ VIF\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
100 {\isaliteral{22}{\isachardoublequoteopen}}bool{\isadigit{2}}if\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ \ \ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}bool{\isadigit{2}}if\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}CIF\ False{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}CIF\ True{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
101 {\isaliteral{22}{\isachardoublequoteopen}}bool{\isadigit{2}}if\ {\isaliteral{28}{\isacharparenleft}}And\ b\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}bool{\isadigit{2}}if\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}bool{\isadigit{2}}if\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}CIF\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
102 \begin{isamarkuptext}% |
|
103 \noindent |
|
104 At last, we have something we can verify: that \isa{bool{\isadigit{2}}if} preserves the |
|
105 value of its argument:% |
|
106 \end{isamarkuptext}% |
|
107 \isamarkuptrue% |
|
108 \isacommand{lemma}\isamarkupfalse% |
|
109 \ {\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}bool{\isadigit{2}}if\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ value\ b\ env{\isaliteral{22}{\isachardoublequoteclose}}% |
|
110 \isadelimproof |
|
111 % |
|
112 \endisadelimproof |
|
113 % |
|
114 \isatagproof |
|
115 % |
|
116 \begin{isamarkuptxt}% |
|
117 \noindent |
|
118 The proof is canonical:% |
|
119 \end{isamarkuptxt}% |
|
120 \isamarkuptrue% |
|
121 \isacommand{apply}\isamarkupfalse% |
|
122 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ b{\isaliteral{29}{\isacharparenright}}\isanewline |
|
123 \isacommand{apply}\isamarkupfalse% |
|
124 {\isaliteral{28}{\isacharparenleft}}auto{\isaliteral{29}{\isacharparenright}}\isanewline |
|
125 \isacommand{done}\isamarkupfalse% |
|
126 % |
|
127 \endisatagproof |
|
128 {\isafoldproof}% |
|
129 % |
|
130 \isadelimproof |
|
131 % |
|
132 \endisadelimproof |
|
133 % |
|
134 \begin{isamarkuptext}% |
|
135 \noindent |
|
136 In fact, all proofs in this case study look exactly like this. Hence we do |
|
137 not show them below. |
|
138 |
|
139 More interesting is the transformation of If-expressions into a normal form |
|
140 where the first argument of \isa{IF} cannot be another \isa{IF} but |
|
141 must be a constant or variable. Such a normal form can be computed by |
|
142 repeatedly replacing a subterm of the form \isa{IF\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ x\ y{\isaliteral{29}{\isacharparenright}}\ z\ u} by |
|
143 \isa{IF\ b\ {\isaliteral{28}{\isacharparenleft}}IF\ x\ z\ u{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}IF\ y\ z\ u{\isaliteral{29}{\isacharparenright}}}, which has the same value. The following |
|
144 primitive recursive functions perform this task:% |
|
145 \end{isamarkuptext}% |
|
146 \isamarkuptrue% |
|
147 \isacommand{primrec}\isamarkupfalse% |
|
148 \ normif\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ ifex{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
149 {\isaliteral{22}{\isachardoublequoteopen}}normif\ {\isaliteral{28}{\isacharparenleft}}CIF\ b{\isaliteral{29}{\isacharparenright}}\ \ \ \ t\ e\ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}CIF\ b{\isaliteral{29}{\isacharparenright}}\ t\ e{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
150 {\isaliteral{22}{\isachardoublequoteopen}}normif\ {\isaliteral{28}{\isacharparenleft}}VIF\ x{\isaliteral{29}{\isacharparenright}}\ \ \ \ t\ e\ {\isaliteral{3D}{\isacharequal}}\ IF\ {\isaliteral{28}{\isacharparenleft}}VIF\ x{\isaliteral{29}{\isacharparenright}}\ t\ e{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
151 {\isaliteral{22}{\isachardoublequoteopen}}normif\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ u\ f\ {\isaliteral{3D}{\isacharequal}}\ normif\ b\ {\isaliteral{28}{\isacharparenleft}}normif\ t\ u\ f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}normif\ e\ u\ f{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
152 \isanewline |
|
153 \isacommand{primrec}\isamarkupfalse% |
|
154 \ norm\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ ifex{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
155 {\isaliteral{22}{\isachardoublequoteopen}}norm\ {\isaliteral{28}{\isacharparenleft}}CIF\ b{\isaliteral{29}{\isacharparenright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ CIF\ b{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
156 {\isaliteral{22}{\isachardoublequoteopen}}norm\ {\isaliteral{28}{\isacharparenleft}}VIF\ x{\isaliteral{29}{\isacharparenright}}\ \ \ \ {\isaliteral{3D}{\isacharequal}}\ VIF\ x{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
157 {\isaliteral{22}{\isachardoublequoteopen}}norm\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ normif\ b\ {\isaliteral{28}{\isacharparenleft}}norm\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}norm\ e{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
158 \begin{isamarkuptext}% |
|
159 \noindent |
|
160 Their interplay is tricky; we leave it to you to develop an |
|
161 intuitive understanding. Fortunately, Isabelle can help us to verify that the |
|
162 transformation preserves the value of the expression:% |
|
163 \end{isamarkuptext}% |
|
164 \isamarkuptrue% |
|
165 \isacommand{theorem}\isamarkupfalse% |
|
166 \ {\isaliteral{22}{\isachardoublequoteopen}}valif\ {\isaliteral{28}{\isacharparenleft}}norm\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ valif\ b\ env{\isaliteral{22}{\isachardoublequoteclose}}% |
|
167 \isadelimproof |
|
168 % |
|
169 \endisadelimproof |
|
170 % |
|
171 \isatagproof |
|
172 % |
|
173 \endisatagproof |
|
174 {\isafoldproof}% |
|
175 % |
|
176 \isadelimproof |
|
177 % |
|
178 \endisadelimproof |
|
179 % |
|
180 \begin{isamarkuptext}% |
|
181 \noindent |
|
182 The proof is canonical, provided we first show the following simplification |
|
183 lemma, which also helps to understand what \isa{normif} does:% |
|
184 \end{isamarkuptext}% |
|
185 \isamarkuptrue% |
|
186 \isacommand{lemma}\isamarkupfalse% |
|
187 \ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
|
188 \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ e{\isaliteral{2E}{\isachardot}}\ valif\ {\isaliteral{28}{\isacharparenleft}}normif\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ valif\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ env{\isaliteral{22}{\isachardoublequoteclose}}% |
|
189 \isadelimproof |
|
190 % |
|
191 \endisadelimproof |
|
192 % |
|
193 \isatagproof |
|
194 % |
|
195 \endisatagproof |
|
196 {\isafoldproof}% |
|
197 % |
|
198 \isadelimproof |
|
199 % |
|
200 \endisadelimproof |
|
201 % |
|
202 \isadelimproof |
|
203 % |
|
204 \endisadelimproof |
|
205 % |
|
206 \isatagproof |
|
207 % |
|
208 \endisatagproof |
|
209 {\isafoldproof}% |
|
210 % |
|
211 \isadelimproof |
|
212 % |
|
213 \endisadelimproof |
|
214 % |
|
215 \begin{isamarkuptext}% |
|
216 \noindent |
|
217 Note that the lemma does not have a name, but is implicitly used in the proof |
|
218 of the theorem shown above because of the \isa{{\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}} attribute. |
|
219 |
|
220 But how can we be sure that \isa{norm} really produces a normal form in |
|
221 the above sense? We define a function that tests If-expressions for normality:% |
|
222 \end{isamarkuptext}% |
|
223 \isamarkuptrue% |
|
224 \isacommand{primrec}\isamarkupfalse% |
|
225 \ normal\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}ifex\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
226 {\isaliteral{22}{\isachardoublequoteopen}}normal{\isaliteral{28}{\isacharparenleft}}CIF\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
227 {\isaliteral{22}{\isachardoublequoteopen}}normal{\isaliteral{28}{\isacharparenleft}}VIF\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
228 {\isaliteral{22}{\isachardoublequoteopen}}normal{\isaliteral{28}{\isacharparenleft}}IF\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}normal\ t\ {\isaliteral{5C3C616E643E}{\isasymand}}\ normal\ e\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline |
|
229 \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}case\ b\ of\ CIF\ b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ True\ {\isaliteral{7C}{\isacharbar}}\ VIF\ x\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ True\ {\isaliteral{7C}{\isacharbar}}\ IF\ x\ y\ z\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ False{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
230 \begin{isamarkuptext}% |
|
231 \noindent |
|
232 Now we prove \isa{normal\ {\isaliteral{28}{\isacharparenleft}}norm\ b{\isaliteral{29}{\isacharparenright}}}. Of course, this requires a lemma about |
|
233 normality of \isa{normif}:% |
|
234 \end{isamarkuptext}% |
|
235 \isamarkuptrue% |
|
236 \isacommand{lemma}\isamarkupfalse% |
|
237 \ {\isaliteral{5B}{\isacharbrackleft}}simp{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ e{\isaliteral{2E}{\isachardot}}\ normal{\isaliteral{28}{\isacharparenleft}}normif\ b\ t\ e{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}normal\ t\ {\isaliteral{5C3C616E643E}{\isasymand}}\ normal\ e{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
238 \isadelimproof |
|
239 % |
|
240 \endisadelimproof |
|
241 % |
|
242 \isatagproof |
|
243 % |
|
244 \endisatagproof |
|
245 {\isafoldproof}% |
|
246 % |
|
247 \isadelimproof |
|
248 % |
|
249 \endisadelimproof |
|
250 % |
|
251 \isadelimproof |
|
252 % |
|
253 \endisadelimproof |
|
254 % |
|
255 \isatagproof |
|
256 % |
|
257 \endisatagproof |
|
258 {\isafoldproof}% |
|
259 % |
|
260 \isadelimproof |
|
261 % |
|
262 \endisadelimproof |
|
263 % |
|
264 \begin{isamarkuptext}% |
|
265 \medskip |
|
266 How do we come up with the required lemmas? Try to prove the main theorems |
|
267 without them and study carefully what \isa{auto} leaves unproved. This |
|
268 can provide the clue. The necessity of universal quantification |
|
269 (\isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}t\ e}) in the two lemmas is explained in |
|
270 \S\ref{sec:InductionHeuristics} |
|
271 |
|
272 \begin{exercise} |
|
273 We strengthen the definition of a \isa{normal} If-expression as follows: |
|
274 the first argument of all \isa{IF}s must be a variable. Adapt the above |
|
275 development to this changed requirement. (Hint: you may need to formulate |
|
276 some of the goals as implications (\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}) rather than |
|
277 equalities (\isa{{\isaliteral{3D}{\isacharequal}}}).) |
|
278 \end{exercise} |
|
279 \index{boolean expressions example|)}% |
|
280 \end{isamarkuptext}% |
|
281 \isamarkuptrue% |
|
282 % |
|
283 \isadelimproof |
|
284 % |
|
285 \endisadelimproof |
|
286 % |
|
287 \isatagproof |
|
288 % |
|
289 \endisatagproof |
|
290 {\isafoldproof}% |
|
291 % |
|
292 \isadelimproof |
|
293 % |
|
294 \endisadelimproof |
|
295 % |
|
296 \isadelimproof |
|
297 % |
|
298 \endisadelimproof |
|
299 % |
|
300 \isatagproof |
|
301 % |
|
302 \endisatagproof |
|
303 {\isafoldproof}% |
|
304 % |
|
305 \isadelimproof |
|
306 % |
|
307 \endisadelimproof |
|
308 % |
|
309 \isadelimproof |
|
310 % |
|
311 \endisadelimproof |
|
312 % |
|
313 \isatagproof |
|
314 % |
|
315 \endisatagproof |
|
316 {\isafoldproof}% |
|
317 % |
|
318 \isadelimproof |
|
319 % |
|
320 \endisadelimproof |
|
321 % |
|
322 \isadelimproof |
|
323 % |
|
324 \endisadelimproof |
|
325 % |
|
326 \isatagproof |
|
327 % |
|
328 \endisatagproof |
|
329 {\isafoldproof}% |
|
330 % |
|
331 \isadelimproof |
|
332 % |
|
333 \endisadelimproof |
|
334 % |
|
335 \isadelimtheory |
|
336 % |
|
337 \endisadelimtheory |
|
338 % |
|
339 \isatagtheory |
|
340 % |
|
341 \endisatagtheory |
|
342 {\isafoldtheory}% |
|
343 % |
|
344 \isadelimtheory |
|
345 % |
|
346 \endisadelimtheory |
|
347 \end{isabellebody}% |
|
348 %%% Local Variables: |
|
349 %%% mode: latex |
|
350 %%% TeX-master: "root" |
|
351 %%% End: |
|