equal
deleted
inserted
replaced
98 At last, we have something we can verify: that \isa{bool{\isadigit{2}}if} preserves the |
98 At last, we have something we can verify: that \isa{bool{\isadigit{2}}if} preserves the |
99 value of its argument:% |
99 value of its argument:% |
100 \end{isamarkuptext}% |
100 \end{isamarkuptext}% |
101 \isamarkuptrue% |
101 \isamarkuptrue% |
102 \isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}\isamarkupfalse% |
102 \isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}\isamarkupfalse% |
103 % |
103 \isamarkuptrue% |
104 \begin{isamarkuptxt}% |
104 \isamarkupfalse% |
105 \noindent |
105 \isamarkupfalse% |
106 The proof is canonical:% |
106 \isamarkupfalse% |
107 \end{isamarkuptxt}% |
|
108 \isamarkuptrue% |
|
109 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline |
|
110 \isamarkupfalse% |
|
111 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline |
|
112 \isamarkupfalse% |
|
113 \isacommand{done}\isamarkupfalse% |
|
114 % |
107 % |
115 \begin{isamarkuptext}% |
108 \begin{isamarkuptext}% |
116 \noindent |
109 \noindent |
117 In fact, all proofs in this case study look exactly like this. Hence we do |
110 In fact, all proofs in this case study look exactly like this. Hence we do |
118 not show them below. |
111 not show them below. |