equal
deleted
inserted
replaced
73 |
73 |
74 \begin{exercise} |
74 \begin{exercise} |
75 The fact that substitution distributes over composition can be expressed |
75 The fact that substitution distributes over composition can be expressed |
76 roughly as follows: |
76 roughly as follows: |
77 \begin{isabelle}% |
77 \begin{isabelle}% |
78 \ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}% |
78 \ \ \ \ \ subst\ {\isacharparenleft}f\ {\isasymcirc}\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}% |
79 \end{isabelle} |
79 \end{isabelle} |
80 Correct this statement (you will find that it does not type-check), |
80 Correct this statement (you will find that it does not type-check), |
81 strengthen it, and prove it. (Note: \isaindexbold{o} is function composition; |
81 strengthen it, and prove it. (Note: \isa{{\isasymcirc}} is function composition; |
82 its definition is found in theorem \isa{o{\isacharunderscore}def}). |
82 its definition is found in theorem \isa{o{\isacharunderscore}def}). |
83 \end{exercise} |
83 \end{exercise} |
84 \begin{exercise}\label{ex:trev-trev} |
84 \begin{exercise}\label{ex:trev-trev} |
85 Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ term} |
85 Define a function \isa{trev} of type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}b{\isacharparenright}\ term} |
86 that recursively reverses the order of arguments of all function symbols in a |
86 that recursively reverses the order of arguments of all function symbols in a |