5 |
5 |
6 We want to represent boolean expressions built up from variables and |
6 We want to represent boolean expressions built up from variables and |
7 constants by negation and conjunction. The following datatype serves exactly |
7 constants by negation and conjunction. The following datatype serves exactly |
8 that purpose:% |
8 that purpose:% |
9 \end{isamarkuptext}% |
9 \end{isamarkuptext}% |
10 \isacommand{datatype}\ boolex\ =\ Const\ bool\ |\ Var\ nat\ |\ Neg\ boolex\isanewline |
10 \isacommand{datatype}\ boolex\ {\isacharequal}\ Const\ bool\ {\isacharbar}\ Var\ nat\ {\isacharbar}\ Neg\ boolex\isanewline |
11 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ And\ boolex\ boolex% |
11 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ boolex\ boolex% |
12 \begin{isamarkuptext}% |
12 \begin{isamarkuptext}% |
13 \noindent |
13 \noindent |
14 The two constants are represented by \isa{Const\ True} and |
14 The two constants are represented by \isa{Const\ True} and |
15 \isa{Const\ False}. Variables are represented by terms of the form |
15 \isa{Const\ False}. Variables are represented by terms of the form |
16 \isa{Var\ \mbox{n}}, where \isa{\mbox{n}} is a natural number (type \isa{nat}). |
16 \isa{Var\ \mbox{n}}, where \isa{\mbox{n}} is a natural number (type \isa{nat}). |
17 For example, the formula $P@0 \land \neg P@1$ is represented by the term |
17 For example, the formula $P@0 \land \neg P@1$ is represented by the term |
18 \isa{And\ (Var\ 0)\ (Neg\ (Var\ 1))}. |
18 \isa{And\ {\isacharparenleft}Var\ \isadigit{0}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ \isadigit{1}{\isacharparenright}{\isacharparenright}}. |
19 |
19 |
20 \subsubsection{What is the value of a boolean expression?} |
20 \subsubsection{What is the value of a boolean expression?} |
21 |
21 |
22 The value of a boolean expression depends on the value of its variables. |
22 The value of a boolean expression depends on the value of its variables. |
23 Hence the function \isa{value} takes an additional parameter, an {\em |
23 Hence the function \isa{value} takes an additional parameter, an {\em |
24 environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to |
24 environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to |
25 their values:% |
25 their values:% |
26 \end{isamarkuptext}% |
26 \end{isamarkuptext}% |
27 \isacommand{consts}\ value\ ::\ {"}boolex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline |
27 \isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
28 \isacommand{primrec}\isanewline |
28 \isacommand{primrec}\isanewline |
29 {"}value\ (Const\ b)\ env\ =\ b{"}\isanewline |
29 {\isachardoublequote}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline |
30 {"}value\ (Var\ x)\ \ \ env\ =\ env\ x{"}\isanewline |
30 {\isachardoublequote}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline |
31 {"}value\ (Neg\ b)\ \ \ env\ =\ ({\isasymnot}\ value\ b\ env){"}\isanewline |
31 {\isachardoublequote}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequote}\isanewline |
32 {"}value\ (And\ b\ c)\ env\ =\ (value\ b\ env\ {\isasymand}\ value\ c\ env){"}% |
32 {\isachardoublequote}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequote}% |
33 \begin{isamarkuptext}% |
33 \begin{isamarkuptext}% |
34 \noindent |
34 \noindent |
35 \subsubsection{If-expressions} |
35 \subsubsection{If-expressions} |
36 |
36 |
37 An alternative and often more efficient (because in a certain sense |
37 An alternative and often more efficient (because in a certain sense |
38 canonical) representation are so-called \emph{If-expressions} built up |
38 canonical) representation are so-called \emph{If-expressions} built up |
39 from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals |
39 from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals |
40 (\isa{IF}):% |
40 (\isa{IF}):% |
41 \end{isamarkuptext}% |
41 \end{isamarkuptext}% |
42 \isacommand{datatype}\ ifex\ =\ CIF\ bool\ |\ VIF\ nat\ |\ IF\ ifex\ ifex\ ifex% |
42 \isacommand{datatype}\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex% |
43 \begin{isamarkuptext}% |
43 \begin{isamarkuptext}% |
44 \noindent |
44 \noindent |
45 The evaluation if If-expressions proceeds as for \isa{boolex}:% |
45 The evaluation if If-expressions proceeds as for \isa{boolex}:% |
46 \end{isamarkuptext}% |
46 \end{isamarkuptext}% |
47 \isacommand{consts}\ valif\ ::\ {"}ifex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline |
47 \isacommand{consts}\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
48 \isacommand{primrec}\isanewline |
48 \isacommand{primrec}\isanewline |
49 {"}valif\ (CIF\ b)\ \ \ \ env\ =\ b{"}\isanewline |
49 {\isachardoublequote}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline |
50 {"}valif\ (VIF\ x)\ \ \ \ env\ =\ env\ x{"}\isanewline |
50 {\isachardoublequote}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline |
51 {"}valif\ (IF\ b\ t\ e)\ env\ =\ (if\ valif\ b\ env\ then\ valif\ t\ env\isanewline |
51 {\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline |
52 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env){"}% |
52 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}% |
53 \begin{isamarkuptext}% |
53 \begin{isamarkuptext}% |
54 \subsubsection{Transformation into and of If-expressions} |
54 \subsubsection{Transformation into and of If-expressions} |
55 |
55 |
56 The type \isa{boolex} is close to the customary representation of logical |
56 The type \isa{boolex} is close to the customary representation of logical |
57 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to |
57 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to |
58 translate from \isa{boolex} into \isa{ifex}:% |
58 translate from \isa{boolex} into \isa{ifex}:% |
59 \end{isamarkuptext}% |
59 \end{isamarkuptext}% |
60 \isacommand{consts}\ bool2if\ ::\ {"}boolex\ {\isasymRightarrow}\ ifex{"}\isanewline |
60 \isacommand{consts}\ bool\isadigit{2}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |
61 \isacommand{primrec}\isanewline |
61 \isacommand{primrec}\isanewline |
62 {"}bool2if\ (Const\ b)\ =\ CIF\ b{"}\isanewline |
62 {\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline |
63 {"}bool2if\ (Var\ x)\ \ \ =\ VIF\ x{"}\isanewline |
63 {\isachardoublequote}bool\isadigit{2}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline |
64 {"}bool2if\ (Neg\ b)\ \ \ =\ IF\ (bool2if\ b)\ (CIF\ False)\ (CIF\ True){"}\isanewline |
64 {\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 |
65 {"}bool2if\ (And\ b\ c)\ =\ IF\ (bool2if\ b)\ (bool2if\ c)\ (CIF\ False){"}% |
65 {\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}% |
66 \begin{isamarkuptext}% |
66 \begin{isamarkuptext}% |
67 \noindent |
67 \noindent |
68 At last, we have something we can verify: that \isa{bool2if} preserves the |
68 At last, we have something we can verify: that \isa{bool2if} preserves the |
69 value of its argument:% |
69 value of its argument:% |
70 \end{isamarkuptext}% |
70 \end{isamarkuptext}% |
71 \isacommand{lemma}\ {"}valif\ (bool2if\ b)\ env\ =\ value\ b\ env{"}% |
71 \isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool\isadigit{2}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}% |
72 \begin{isamarkuptxt}% |
72 \begin{isamarkuptxt}% |
73 \noindent |
73 \noindent |
74 The proof is canonical:% |
74 The proof is canonical:% |
75 \end{isamarkuptxt}% |
75 \end{isamarkuptxt}% |
76 \isacommand{apply}(induct\_tac\ b)\isanewline |
76 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline |
77 \isacommand{by}(auto)% |
77 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}% |
78 \begin{isamarkuptext}% |
78 \begin{isamarkuptext}% |
79 \noindent |
79 \noindent |
80 In fact, all proofs in this case study look exactly like this. Hence we do |
80 In fact, all proofs in this case study look exactly like this. Hence we do |
81 not show them below. |
81 not show them below. |
82 |
82 |
83 More interesting is the transformation of If-expressions into a normal form |
83 More interesting is the transformation of If-expressions into a normal form |
84 where the first argument of \isa{IF} cannot be another \isa{IF} but |
84 where the first argument of \isa{IF} cannot be another \isa{IF} but |
85 must be a constant or variable. Such a normal form can be computed by |
85 must be a constant or variable. Such a normal form can be computed by |
86 repeatedly replacing a subterm of the form \isa{IF\ (IF\ \mbox{b}\ \mbox{x}\ \mbox{y})\ \mbox{z}\ \mbox{u}} by |
86 repeatedly replacing a subterm of the form \isa{IF\ {\isacharparenleft}IF\ \mbox{b}\ \mbox{x}\ \mbox{y}{\isacharparenright}\ \mbox{z}\ \mbox{u}} by |
87 \isa{IF\ \mbox{b}\ (IF\ \mbox{x}\ \mbox{z}\ \mbox{u})\ (IF\ \mbox{y}\ \mbox{z}\ \mbox{u})}, which has the same value. The following |
87 \isa{IF\ \mbox{b}\ {\isacharparenleft}IF\ \mbox{x}\ \mbox{z}\ \mbox{u}{\isacharparenright}\ {\isacharparenleft}IF\ \mbox{y}\ \mbox{z}\ \mbox{u}{\isacharparenright}}, which has the same value. The following |
88 primitive recursive functions perform this task:% |
88 primitive recursive functions perform this task:% |
89 \end{isamarkuptext}% |
89 \end{isamarkuptext}% |
90 \isacommand{consts}\ normif\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{"}\isanewline |
90 \isacommand{consts}\ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |
91 \isacommand{primrec}\isanewline |
91 \isacommand{primrec}\isanewline |
92 {"}normif\ (CIF\ b)\ \ \ \ t\ e\ =\ IF\ (CIF\ b)\ t\ e{"}\isanewline |
92 {\isachardoublequote}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline |
93 {"}normif\ (VIF\ x)\ \ \ \ t\ e\ =\ IF\ (VIF\ x)\ t\ e{"}\isanewline |
93 {\isachardoublequote}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline |
94 {"}normif\ (IF\ b\ t\ e)\ u\ f\ =\ normif\ b\ (normif\ t\ u\ f)\ (normif\ e\ u\ f){"}\isanewline |
94 {\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 |
95 \isanewline |
95 \isanewline |
96 \isacommand{consts}\ norm\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex{"}\isanewline |
96 \isacommand{consts}\ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline |
97 \isacommand{primrec}\isanewline |
97 \isacommand{primrec}\isanewline |
98 {"}norm\ (CIF\ b)\ \ \ \ =\ CIF\ b{"}\isanewline |
98 {\isachardoublequote}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline |
99 {"}norm\ (VIF\ x)\ \ \ \ =\ VIF\ x{"}\isanewline |
99 {\isachardoublequote}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline |
100 {"}norm\ (IF\ b\ t\ e)\ =\ normif\ b\ (norm\ t)\ (norm\ e){"}% |
100 {\isachardoublequote}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequote}% |
101 \begin{isamarkuptext}% |
101 \begin{isamarkuptext}% |
102 \noindent |
102 \noindent |
103 Their interplay is a bit tricky, and we leave it to the reader to develop an |
103 Their interplay is a bit tricky, and we leave it to the reader to develop an |
104 intuitive understanding. Fortunately, Isabelle can help us to verify that the |
104 intuitive understanding. Fortunately, Isabelle can help us to verify that the |
105 transformation preserves the value of the expression:% |
105 transformation preserves the value of the expression:% |
106 \end{isamarkuptext}% |
106 \end{isamarkuptext}% |
107 \isacommand{theorem}\ {"}valif\ (norm\ b)\ env\ =\ valif\ b\ env{"}% |
107 \isacommand{theorem}\ {\isachardoublequote}valif\ {\isacharparenleft}norm\ b{\isacharparenright}\ env\ {\isacharequal}\ valif\ b\ env{\isachardoublequote}% |
108 \begin{isamarkuptext}% |
108 \begin{isamarkuptext}% |
109 \noindent |
109 \noindent |
110 The proof is canonical, provided we first show the following simplification |
110 The proof is canonical, provided we first show the following simplification |
111 lemma (which also helps to understand what \isa{normif} does):% |
111 lemma (which also helps to understand what \isa{normif} does):% |
112 \end{isamarkuptext}% |
112 \end{isamarkuptext}% |
113 \isacommand{lemma}\ [simp]:\isanewline |
113 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline |
114 \ \ {"}{\isasymforall}t\ e.\ valif\ (normif\ b\ t\ e)\ env\ =\ valif\ (IF\ b\ t\ e)\ env{"}% |
114 \ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}% |
115 \begin{isamarkuptext}% |
115 \begin{isamarkuptext}% |
116 \noindent |
116 \noindent |
117 Note that the lemma does not have a name, but is implicitly used in the proof |
117 Note that the lemma does not have a name, but is implicitly used in the proof |
118 of the theorem shown above because of the \isa{[simp]} attribute. |
118 of the theorem shown above because of the \isa{[simp]} attribute. |
119 |
119 |
120 But how can we be sure that \isa{norm} really produces a normal form in |
120 But how can we be sure that \isa{norm} really produces a normal form in |
121 the above sense? We define a function that tests If-expressions for normality% |
121 the above sense? We define a function that tests If-expressions for normality% |
122 \end{isamarkuptext}% |
122 \end{isamarkuptext}% |
123 \isacommand{consts}\ normal\ ::\ {"}ifex\ {\isasymRightarrow}\ bool{"}\isanewline |
123 \isacommand{consts}\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline |
124 \isacommand{primrec}\isanewline |
124 \isacommand{primrec}\isanewline |
125 {"}normal(CIF\ b)\ =\ True{"}\isanewline |
125 {\isachardoublequote}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline |
126 {"}normal(VIF\ x)\ =\ True{"}\isanewline |
126 {\isachardoublequote}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline |
127 {"}normal(IF\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline |
127 {\isachardoublequote}normal{\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline |
128 \ \ \ \ \ (case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ |\ VIF\ x\ {\isasymRightarrow}\ True\ |\ IF\ x\ y\ z\ {\isasymRightarrow}\ False)){"}% |
128 \ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequote}% |
129 \begin{isamarkuptext}% |
129 \begin{isamarkuptext}% |
130 \noindent |
130 \noindent |
131 and prove \isa{normal(norm b)}. Of course, this requires a lemma about |
131 and prove \isa{normal(norm b)}. Of course, this requires a lemma about |
132 normality of \isa{normif}:% |
132 normality of \isa{normif}:% |
133 \end{isamarkuptext}% |
133 \end{isamarkuptext}% |
134 \isacommand{lemma}[simp]:\ {"}{\isasymforall}t\ e.\ normal(normif\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e){"}\end{isabelle}% |
134 \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}\end{isabelle}% |
135 %%% Local Variables: |
135 %%% Local Variables: |
136 %%% mode: latex |
136 %%% mode: latex |
137 %%% TeX-master: "root" |
137 %%% TeX-master: "root" |
138 %%% End: |
138 %%% End: |