1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
3 \def\isabellecontext{Ifexpr}% |
3 \def\isabellecontext{Ifexpr}% |
|
4 \isamarkupfalse% |
4 % |
5 % |
5 \isamarkupsubsection{Case Study: Boolean Expressions% |
6 \isamarkupsubsection{Case Study: Boolean Expressions% |
6 } |
7 } |
|
8 \isamarkuptrue% |
7 % |
9 % |
8 \begin{isamarkuptext}% |
10 \begin{isamarkuptext}% |
9 \label{sec:boolex}\index{boolean expressions example|(} |
11 \label{sec:boolex}\index{boolean expressions example|(} |
10 The aim of this case study is twofold: it shows how to model boolean |
12 The aim of this case study is twofold: it shows how to model boolean |
11 expressions and some algorithms for manipulating them, and it demonstrates |
13 expressions and some algorithms for manipulating them, and it demonstrates |
12 the constructs introduced above.% |
14 the constructs introduced above.% |
13 \end{isamarkuptext}% |
15 \end{isamarkuptext}% |
|
16 \isamarkuptrue% |
14 % |
17 % |
15 \isamarkupsubsubsection{Modelling Boolean Expressions% |
18 \isamarkupsubsubsection{Modelling Boolean Expressions% |
16 } |
19 } |
|
20 \isamarkuptrue% |
17 % |
21 % |
18 \begin{isamarkuptext}% |
22 \begin{isamarkuptext}% |
19 We want to represent boolean expressions built up from variables and |
23 We want to represent boolean expressions built up from variables and |
20 constants by negation and conjunction. The following datatype serves exactly |
24 constants by negation and conjunction. The following datatype serves exactly |
21 that purpose:% |
25 that purpose:% |
22 \end{isamarkuptext}% |
26 \end{isamarkuptext}% |
|
27 \isamarkuptrue% |
23 \isacommand{datatype}\ boolex\ {\isacharequal}\ Const\ bool\ {\isacharbar}\ Var\ nat\ {\isacharbar}\ Neg\ boolex\isanewline |
28 \isacommand{datatype}\ boolex\ {\isacharequal}\ Const\ bool\ {\isacharbar}\ Var\ nat\ {\isacharbar}\ Neg\ boolex\isanewline |
24 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ boolex\ boolex% |
29 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ boolex\ boolex\isamarkupfalse% |
|
30 % |
25 \begin{isamarkuptext}% |
31 \begin{isamarkuptext}% |
26 \noindent |
32 \noindent |
27 The two constants are represented by \isa{Const\ True} and |
33 The two constants are represented by \isa{Const\ True} and |
28 \isa{Const\ False}. Variables are represented by terms of the form |
34 \isa{Const\ False}. Variables are represented by terms of the form |
29 \isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}). |
35 \isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}). |
35 The value of a boolean expression depends on the value of its variables. |
41 The value of a boolean expression depends on the value of its variables. |
36 Hence the function \isa{value} takes an additional parameter, an |
42 Hence the function \isa{value} takes an additional parameter, an |
37 \emph{environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to their |
43 \emph{environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to their |
38 values:% |
44 values:% |
39 \end{isamarkuptext}% |
45 \end{isamarkuptext}% |
|
46 \isamarkuptrue% |
40 \isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
47 \isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
|
48 \isamarkupfalse% |
41 \isacommand{primrec}\isanewline |
49 \isacommand{primrec}\isanewline |
42 {\isachardoublequote}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline |
50 {\isachardoublequote}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline |
43 {\isachardoublequote}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline |
51 {\isachardoublequote}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline |
44 {\isachardoublequote}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequote}\isanewline |
52 {\isachardoublequote}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequote}\isanewline |
45 {\isachardoublequote}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequote}% |
53 {\isachardoublequote}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
54 % |
46 \begin{isamarkuptext}% |
55 \begin{isamarkuptext}% |
47 \noindent |
56 \noindent |
48 \subsubsection{If-Expressions} |
57 \subsubsection{If-Expressions} |
49 |
58 |
50 An alternative and often more efficient (because in a certain sense |
59 An alternative and often more efficient (because in a certain sense |
51 canonical) representation are so-called \emph{If-expressions} built up |
60 canonical) representation are so-called \emph{If-expressions} built up |
52 from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals |
61 from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals |
53 (\isa{IF}):% |
62 (\isa{IF}):% |
54 \end{isamarkuptext}% |
63 \end{isamarkuptext}% |
55 \isacommand{datatype}\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex% |
64 \isamarkuptrue% |
|
65 \isacommand{datatype}\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex\isamarkupfalse% |
|
66 % |
56 \begin{isamarkuptext}% |
67 \begin{isamarkuptext}% |
57 \noindent |
68 \noindent |
58 The evaluation of If-expressions proceeds as for \isa{boolex}:% |
69 The evaluation of If-expressions proceeds as for \isa{boolex}:% |
59 \end{isamarkuptext}% |
70 \end{isamarkuptext}% |
|
71 \isamarkuptrue% |
60 \isacommand{consts}\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
72 \isacommand{consts}\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
|
73 \isamarkupfalse% |
61 \isacommand{primrec}\isanewline |
74 \isacommand{primrec}\isanewline |
62 {\isachardoublequote}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline |
75 {\isachardoublequote}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline |
63 {\isachardoublequote}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline |
76 {\isachardoublequote}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline |
64 {\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline |
77 {\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline |
65 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}% |
78 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
79 % |
66 \begin{isamarkuptext}% |
80 \begin{isamarkuptext}% |
67 \subsubsection{Converting Boolean and If-Expressions} |
81 \subsubsection{Converting Boolean and If-Expressions} |
68 |
82 |
69 The type \isa{boolex} is close to the customary representation of logical |
83 The type \isa{boolex} is close to the customary representation of logical |
70 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to |
84 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to |
71 translate from \isa{boolex} into \isa{ifex}:% |
85 translate from \isa{boolex} into \isa{ifex}:% |
72 \end{isamarkuptext}% |
86 \end{isamarkuptext}% |
|
87 \isamarkuptrue% |
73 \isacommand{consts}\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |
88 \isacommand{consts}\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |
|
89 \isamarkupfalse% |
74 \isacommand{primrec}\isanewline |
90 \isacommand{primrec}\isanewline |
75 {\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline |
91 {\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline |
76 {\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline |
92 {\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline |
77 {\isachardoublequote}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}{\isachardoublequote}\isanewline |
93 {\isachardoublequote}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}{\isachardoublequote}\isanewline |
78 {\isachardoublequote}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}{\isachardoublequote}% |
94 {\isachardoublequote}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}{\isachardoublequote}\isamarkupfalse% |
|
95 % |
79 \begin{isamarkuptext}% |
96 \begin{isamarkuptext}% |
80 \noindent |
97 \noindent |
81 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 |
82 value of its argument:% |
99 value of its argument:% |
83 \end{isamarkuptext}% |
100 \end{isamarkuptext}% |
84 \isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}% |
101 \isamarkuptrue% |
|
102 \isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}\isamarkupfalse% |
|
103 % |
85 \begin{isamarkuptxt}% |
104 \begin{isamarkuptxt}% |
86 \noindent |
105 \noindent |
87 The proof is canonical:% |
106 The proof is canonical:% |
88 \end{isamarkuptxt}% |
107 \end{isamarkuptxt}% |
|
108 \isamarkuptrue% |
89 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline |
109 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline |
|
110 \isamarkupfalse% |
90 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline |
111 \isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline |
91 \isacommand{done}% |
112 \isamarkupfalse% |
|
113 \isacommand{done}\isamarkupfalse% |
|
114 % |
92 \begin{isamarkuptext}% |
115 \begin{isamarkuptext}% |
93 \noindent |
116 \noindent |
94 In fact, all proofs in this case study look exactly like this. Hence we do |
117 In fact, all proofs in this case study look exactly like this. Hence we do |
95 not show them below. |
118 not show them below. |
96 |
119 |
99 must be a constant or variable. Such a normal form can be computed by |
122 must be a constant or variable. Such a normal form can be computed by |
100 repeatedly replacing a subterm of the form \isa{IF\ {\isacharparenleft}IF\ b\ x\ y{\isacharparenright}\ z\ u} by |
123 repeatedly replacing a subterm of the form \isa{IF\ {\isacharparenleft}IF\ b\ x\ y{\isacharparenright}\ z\ u} by |
101 \isa{IF\ b\ {\isacharparenleft}IF\ x\ z\ u{\isacharparenright}\ {\isacharparenleft}IF\ y\ z\ u{\isacharparenright}}, which has the same value. The following |
124 \isa{IF\ b\ {\isacharparenleft}IF\ x\ z\ u{\isacharparenright}\ {\isacharparenleft}IF\ y\ z\ u{\isacharparenright}}, which has the same value. The following |
102 primitive recursive functions perform this task:% |
125 primitive recursive functions perform this task:% |
103 \end{isamarkuptext}% |
126 \end{isamarkuptext}% |
|
127 \isamarkuptrue% |
104 \isacommand{consts}\ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |
128 \isacommand{consts}\ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |
|
129 \isamarkupfalse% |
105 \isacommand{primrec}\isanewline |
130 \isacommand{primrec}\isanewline |
106 {\isachardoublequote}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline |
131 {\isachardoublequote}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline |
107 {\isachardoublequote}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline |
132 {\isachardoublequote}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline |
108 {\isachardoublequote}normif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ u\ f\ {\isacharequal}\ normif\ b\ {\isacharparenleft}normif\ t\ u\ f{\isacharparenright}\ {\isacharparenleft}normif\ e\ u\ f{\isacharparenright}{\isachardoublequote}\isanewline |
133 {\isachardoublequote}normif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ u\ f\ {\isacharequal}\ normif\ b\ {\isacharparenleft}normif\ t\ u\ f{\isacharparenright}\ {\isacharparenleft}normif\ e\ u\ f{\isacharparenright}{\isachardoublequote}\isanewline |
109 \isanewline |
134 \isanewline |
|
135 \isamarkupfalse% |
110 \isacommand{consts}\ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |
136 \isacommand{consts}\ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |
|
137 \isamarkupfalse% |
111 \isacommand{primrec}\isanewline |
138 \isacommand{primrec}\isanewline |
112 {\isachardoublequote}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline |
139 {\isachardoublequote}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline |
113 {\isachardoublequote}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline |
140 {\isachardoublequote}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline |
114 {\isachardoublequote}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequote}% |
141 {\isachardoublequote}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
142 % |
115 \begin{isamarkuptext}% |
143 \begin{isamarkuptext}% |
116 \noindent |
144 \noindent |
117 Their interplay is tricky; we leave it to you to develop an |
145 Their interplay is tricky; we leave it to you to develop an |
118 intuitive understanding. Fortunately, Isabelle can help us to verify that the |
146 intuitive understanding. Fortunately, Isabelle can help us to verify that the |
119 transformation preserves the value of the expression:% |
147 transformation preserves the value of the expression:% |
120 \end{isamarkuptext}% |
148 \end{isamarkuptext}% |
121 \isacommand{theorem}\ {\isachardoublequote}valif\ {\isacharparenleft}norm\ b{\isacharparenright}\ env\ {\isacharequal}\ valif\ b\ env{\isachardoublequote}% |
149 \isamarkuptrue% |
|
150 \isacommand{theorem}\ {\isachardoublequote}valif\ {\isacharparenleft}norm\ b{\isacharparenright}\ env\ {\isacharequal}\ valif\ b\ env{\isachardoublequote}\isamarkupfalse% |
|
151 \isamarkupfalse% |
|
152 % |
122 \begin{isamarkuptext}% |
153 \begin{isamarkuptext}% |
123 \noindent |
154 \noindent |
124 The proof is canonical, provided we first show the following simplification |
155 The proof is canonical, provided we first show the following simplification |
125 lemma, which also helps to understand what \isa{normif} does:% |
156 lemma, which also helps to understand what \isa{normif} does:% |
126 \end{isamarkuptext}% |
157 \end{isamarkuptext}% |
|
158 \isamarkuptrue% |
127 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
159 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
128 \ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}% |
160 \ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}\isamarkupfalse% |
|
161 \isamarkupfalse% |
|
162 \isamarkupfalse% |
|
163 \isamarkupfalse% |
|
164 \isamarkupfalse% |
|
165 \isamarkupfalse% |
|
166 % |
129 \begin{isamarkuptext}% |
167 \begin{isamarkuptext}% |
130 \noindent |
168 \noindent |
131 Note that the lemma does not have a name, but is implicitly used in the proof |
169 Note that the lemma does not have a name, but is implicitly used in the proof |
132 of the theorem shown above because of the \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute. |
170 of the theorem shown above because of the \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute. |
133 |
171 |
134 But how can we be sure that \isa{norm} really produces a normal form in |
172 But how can we be sure that \isa{norm} really produces a normal form in |
135 the above sense? We define a function that tests If-expressions for normality:% |
173 the above sense? We define a function that tests If-expressions for normality:% |
136 \end{isamarkuptext}% |
174 \end{isamarkuptext}% |
|
175 \isamarkuptrue% |
137 \isacommand{consts}\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
176 \isacommand{consts}\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
|
177 \isamarkupfalse% |
138 \isacommand{primrec}\isanewline |
178 \isacommand{primrec}\isanewline |
139 {\isachardoublequote}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline |
179 {\isachardoublequote}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline |
140 {\isachardoublequote}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline |
180 {\isachardoublequote}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline |
141 {\isachardoublequote}normal{\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline |
181 {\isachardoublequote}normal{\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline |
142 \ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
182 \ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
183 % |
143 \begin{isamarkuptext}% |
184 \begin{isamarkuptext}% |
144 \noindent |
185 \noindent |
145 Now we prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about |
186 Now we prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about |
146 normality of \isa{normif}:% |
187 normality of \isa{normif}:% |
147 \end{isamarkuptext}% |
188 \end{isamarkuptext}% |
148 \isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}% |
189 \isamarkuptrue% |
|
190 \isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}\isamarkupfalse% |
|
191 \isamarkupfalse% |
|
192 \isamarkupfalse% |
|
193 \isamarkupfalse% |
|
194 \isamarkupfalse% |
|
195 \isamarkupfalse% |
|
196 % |
149 \begin{isamarkuptext}% |
197 \begin{isamarkuptext}% |
150 \medskip |
198 \medskip |
151 How do we come up with the required lemmas? Try to prove the main theorems |
199 How do we come up with the required lemmas? Try to prove the main theorems |
152 without them and study carefully what \isa{auto} leaves unproved. This |
200 without them and study carefully what \isa{auto} leaves unproved. This |
153 can provide the clue. The necessity of universal quantification |
201 can provide the clue. The necessity of universal quantification |