equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Nested}% |
3 % |
4 % |
4 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
5 So far, all datatypes had the property that on the right-hand side of their |
6 So far, all datatypes had the property that on the right-hand side of their |
6 definition they occurred only at the top-level, i.e.\ directly below a |
7 definition they occurred only at the top-level, i.e.\ directly below a |
7 constructor. This is not the case any longer for the following model of terms |
8 constructor. This is not the case any longer for the following model of terms |
69 because the two halves of the goal would be unrelated. |
70 because the two halves of the goal would be unrelated. |
70 |
71 |
71 \begin{exercise} |
72 \begin{exercise} |
72 The fact that substitution distributes over composition can be expressed |
73 The fact that substitution distributes over composition can be expressed |
73 roughly as follows: |
74 roughly as follows: |
74 % |
|
75 \begin{isabelle}% |
75 \begin{isabelle}% |
76 \ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}% |
76 \ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}% |
77 \end{isabelle}% |
77 \end{isabelle} |
78 |
|
79 Correct this statement (you will find that it does not type-check), |
78 Correct this statement (you will find that it does not type-check), |
80 strengthen it, and prove it. (Note: \isaindexbold{o} is function composition; |
79 strengthen it, and prove it. (Note: \isaindexbold{o} is function composition; |
81 its definition is found in theorem \isa{o{\isacharunderscore}def}). |
80 its definition is found in theorem \isa{o{\isacharunderscore}def}). |
82 \end{exercise} |
81 \end{exercise} |
83 \begin{exercise}\label{ex:trev-trev} |
82 \begin{exercise}\label{ex:trev-trev} |
87 \end{exercise} |
86 \end{exercise} |
88 |
87 |
89 The experienced functional programmer may feel that our above definition of |
88 The experienced functional programmer may feel that our above definition of |
90 \isa{subst} is unnecessarily complicated in that \isa{substs} is |
89 \isa{subst} is unnecessarily complicated in that \isa{substs} is |
91 completely unnecessary. The \isa{App}-case can be defined directly as |
90 completely unnecessary. The \isa{App}-case can be defined directly as |
92 % |
|
93 \begin{isabelle}% |
91 \begin{isabelle}% |
94 \ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}% |
92 \ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}% |
95 \end{isabelle}% |
93 \end{isabelle} |
96 |
|
97 where \isa{map} is the standard list function such that |
94 where \isa{map} is the standard list function such that |
98 \isa{map\ f\ {\isacharbrackleft}x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle |
95 \isa{map\ f\ {\isacharbrackleft}x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle |
99 insists on the above fixed format. Fortunately, we can easily \emph{prove} |
96 insists on the above fixed format. Fortunately, we can easily \emph{prove} |
100 that the suggested equation holds:% |
97 that the suggested equation holds:% |
101 \end{isamarkuptext}% |
98 \end{isamarkuptext}% |