317 % |
317 % |
318 \begin{isamarkuptext}% |
318 \begin{isamarkuptext}% |
319 Let us close this section with a few words about the executability of our model checkers. |
319 Let us close this section with a few words about the executability of our model checkers. |
320 It is clear that if all sets are finite, they can be represented as lists and the usual |
320 It is clear that if all sets are finite, they can be represented as lists and the usual |
321 set operations are easily implemented. Only \isa{lfp} requires a little thought. |
321 set operations are easily implemented. Only \isa{lfp} requires a little thought. |
322 \REMARK{you had `in the library' but I assume you meant it was a |
322 Fortunately, the HOL Library% |
323 built in lemma. Do we give its name?} |
323 \footnote{See theory \isa{While_Combinator_Example}.} |
324 Fortunately, Isabelle/HOL provides a theorem stating that |
324 provides a theorem stating that |
325 in the case of finite sets and a monotone \isa{F}, |
325 in the case of finite sets and a monotone function~\isa{F}, |
326 the value of \isa{lfp\ F} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until |
326 the value of \isa{lfp\ F} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until |
327 a fixed point is reached. It is actually possible to generate executable functional programs |
327 a fixed point is reached. It is actually possible to generate executable functional programs |
328 from HOL definitions, but that is beyond the scope of the tutorial.% |
328 from HOL definitions, but that is beyond the scope of the tutorial.% |
329 \end{isamarkuptext}% |
329 \end{isamarkuptext}% |
330 \end{isabellebody}% |
330 \end{isabellebody}% |