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\ =\ Const\ bool\ |\ Var\ nat\ |\ Neg\ boolex\isanewline |
11 ~~~~~~~~~~~~~~~~|~And~boolex~boolex% |
11 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ 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~$n$}, where $n$ is a natural number (type \isa{nat}). |
16 \isa{Var\ n}, where \isa{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\ (Var\ 0)\ (Neg\ (Var\ 1))}. |
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 \isasymFun\ 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\ ::\ {"}boolex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline |
28 \isacommand{primrec}\isanewline |
28 \isacommand{primrec}\isanewline |
29 {"}value~(Const~b)~env~=~b{"}\isanewline |
29 {"}value\ (Const\ b)\ env\ =\ b{"}\isanewline |
30 {"}value~(Var~x)~~~env~=~env~x{"}\isanewline |
30 {"}value\ (Var\ x)\ \ \ env\ =\ env\ x{"}\isanewline |
31 {"}value~(Neg~b)~~~env~=~({\isasymnot}~value~b~env){"}\isanewline |
31 {"}value\ (Neg\ b)\ \ \ env\ =\ ({\isasymnot}\ value\ b\ env){"}\isanewline |
32 {"}value~(And~b~c)~env~=~(value~b~env~{\isasymand}~value~c~env){"}% |
32 {"}value\ (And\ b\ c)\ env\ =\ (value\ b\ env\ {\isasymand}\ value\ c\ env){"}% |
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\ =\ CIF\ bool\ |\ VIF\ nat\ |\ 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\ ::\ {"}ifex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline |
48 \isacommand{primrec}\isanewline |
48 \isacommand{primrec}\isanewline |
49 {"}valif~(CIF~b)~~~~env~=~b{"}\isanewline |
49 {"}valif\ (CIF\ b)\ \ \ \ env\ =\ b{"}\isanewline |
50 {"}valif~(VIF~x)~~~~env~=~env~x{"}\isanewline |
50 {"}valif\ (VIF\ x)\ \ \ \ env\ =\ env\ x{"}\isanewline |
51 {"}valif~(IF~b~t~e)~env~=~(if~valif~b~env~then~valif~t~env\isanewline |
51 {"}valif\ (IF\ b\ t\ e)\ env\ =\ (if\ valif\ b\ env\ then\ valif\ t\ env\isanewline |
52 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~else~valif~e~env){"}% |
52 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env){"}% |
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}\ bool2if\ ::\ {"}boolex\ {\isasymRightarrow}\ ifex{"}\isanewline |
61 \isacommand{primrec}\isanewline |
61 \isacommand{primrec}\isanewline |
62 {"}bool2if~(Const~b)~=~CIF~b{"}\isanewline |
62 {"}bool2if\ (Const\ b)\ =\ CIF\ b{"}\isanewline |
63 {"}bool2if~(Var~x)~~~=~VIF~x{"}\isanewline |
63 {"}bool2if\ (Var\ x)\ \ \ =\ VIF\ x{"}\isanewline |
64 {"}bool2if~(Neg~b)~~~=~IF~(bool2if~b)~(CIF~False)~(CIF~True){"}\isanewline |
64 {"}bool2if\ (Neg\ b)\ \ \ =\ IF\ (bool2if\ b)\ (CIF\ False)\ (CIF\ True){"}\isanewline |
65 {"}bool2if~(And~b~c)~=~IF~(bool2if~b)~(bool2if~c)~(CIF~False){"}% |
65 {"}bool2if\ (And\ b\ c)\ =\ IF\ (bool2if\ b)\ (bool2if\ c)\ (CIF\ False){"}% |
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}\ {"}valif\ (bool2if\ b)\ env\ =\ value\ b\ env{"}% |
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}(induct\_tac\ b)\isanewline |
77 \isacommand{by}(auto)% |
77 \isacommand{by}(auto)% |
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~b~x~y)~z~u} by |
86 repeatedly replacing a subterm of the form \isa{IF\ (IF\ b\ x\ y)\ z\ u} by |
87 \isa{IF b (IF x z u) (IF y z u)}, which has the same value. The following |
87 \isa{IF\ b\ (IF\ x\ z\ u)\ (IF\ y\ z\ u)}, 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\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{"}\isanewline |
91 \isacommand{primrec}\isanewline |
91 \isacommand{primrec}\isanewline |
92 {"}normif~(CIF~b)~~~~t~e~=~IF~(CIF~b)~t~e{"}\isanewline |
92 {"}normif\ (CIF\ b)\ \ \ \ t\ e\ =\ IF\ (CIF\ b)\ t\ e{"}\isanewline |
93 {"}normif~(VIF~x)~~~~t~e~=~IF~(VIF~x)~t~e{"}\isanewline |
93 {"}normif\ (VIF\ x)\ \ \ \ t\ e\ =\ IF\ (VIF\ x)\ t\ e{"}\isanewline |
94 {"}normif~(IF~b~t~e)~u~f~=~normif~b~(normif~t~u~f)~(normif~e~u~f){"}\isanewline |
94 {"}normif\ (IF\ b\ t\ e)\ u\ f\ =\ normif\ b\ (normif\ t\ u\ f)\ (normif\ e\ u\ f){"}\isanewline |
95 \isanewline |
95 \isanewline |
96 \isacommand{consts}~norm~::~{"}ifex~{\isasymRightarrow}~ifex{"}\isanewline |
96 \isacommand{consts}\ norm\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex{"}\isanewline |
97 \isacommand{primrec}\isanewline |
97 \isacommand{primrec}\isanewline |
98 {"}norm~(CIF~b)~~~~=~CIF~b{"}\isanewline |
98 {"}norm\ (CIF\ b)\ \ \ \ =\ CIF\ b{"}\isanewline |
99 {"}norm~(VIF~x)~~~~=~VIF~x{"}\isanewline |
99 {"}norm\ (VIF\ x)\ \ \ \ =\ VIF\ x{"}\isanewline |
100 {"}norm~(IF~b~t~e)~=~normif~b~(norm~t)~(norm~e){"}% |
100 {"}norm\ (IF\ b\ t\ e)\ =\ normif\ b\ (norm\ t)\ (norm\ e){"}% |
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}\ {"}valif\ (norm\ b)\ env\ =\ valif\ b\ env{"}% |
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}\ [simp]:\isanewline |
114 ~~{"}{\isasymforall}t~e.~valif~(normif~b~t~e)~env~=~valif~(IF~b~t~e)~env{"}% |
114 \ \ {"}{\isasymforall}t\ e.\ valif\ (normif\ b\ t\ e)\ env\ =\ valif\ (IF\ b\ t\ e)\ env{"}% |
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\ ::\ {"}ifex\ {\isasymRightarrow}\ bool{"}\isanewline |
124 \isacommand{primrec}\isanewline |
124 \isacommand{primrec}\isanewline |
125 {"}normal(CIF~b)~=~True{"}\isanewline |
125 {"}normal(CIF\ b)\ =\ True{"}\isanewline |
126 {"}normal(VIF~x)~=~True{"}\isanewline |
126 {"}normal(VIF\ x)\ =\ True{"}\isanewline |
127 {"}normal(IF~b~t~e)~=~(normal~t~{\isasymand}~normal~e~{\isasymand}\isanewline |
127 {"}normal(IF\ b\ t\ e)\ =\ (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 \ \ \ \ \ (case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ |\ VIF\ x\ {\isasymRightarrow}\ True\ |\ IF\ x\ y\ z\ {\isasymRightarrow}\ False)){"}% |
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}[simp]:\ {"}{\isasymforall}t\ e.\ normal(normif\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e){"}\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: |