54 |
54 |
55 Let us define a substitution function on terms. Because terms involve term |
55 Let us define a substitution function on terms. Because terms involve term |
56 lists, we need to define two substitution functions simultaneously:% |
56 lists, we need to define two substitution functions simultaneously:% |
57 \end{isamarkuptext}% |
57 \end{isamarkuptext}% |
58 \isamarkuptrue% |
58 \isamarkuptrue% |
59 \isacommand{consts}\isamarkupfalse% |
|
60 \isanewline |
|
61 subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequoteclose}\isanewline |
|
62 substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequoteclose}\isanewline |
|
63 \isanewline |
|
64 \isacommand{primrec}\isamarkupfalse% |
59 \isacommand{primrec}\isamarkupfalse% |
65 \isanewline |
60 \isanewline |
66 \ \ {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequoteclose}\isanewline |
61 subst\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ \ \ \ \ \ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isachardoublequoteclose}\ \isakeyword{and}\isanewline |
|
62 substs{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}v{\isasymRightarrow}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequoteclose}\isanewline |
|
63 \isakeyword{where}\isanewline |
|
64 {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ s\ x{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
67 \ \ subst{\isacharunderscore}App{\isacharcolon}\isanewline |
65 \ \ subst{\isacharunderscore}App{\isacharcolon}\isanewline |
68 \ \ {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}substs\ s\ ts{\isacharparenright}{\isachardoublequoteclose}\isanewline |
66 {\isachardoublequoteopen}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}substs\ s\ ts{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
69 \isanewline |
67 \isanewline |
70 \ \ {\isachardoublequoteopen}substs\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline |
68 {\isachardoublequoteopen}substs\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline |
71 \ \ {\isachardoublequoteopen}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequoteclose}% |
69 {\isachardoublequoteopen}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequoteclose}% |
72 \begin{isamarkuptext}% |
70 \begin{isamarkuptext}% |
73 \noindent |
71 \noindent |
74 Individual equations in a \commdx{primrec} definition may be |
72 Individual equations in a \commdx{primrec} definition may be |
75 named as shown for \isa{subst{\isacharunderscore}App}. |
73 named as shown for \isa{subst{\isacharunderscore}App}. |
76 The significance of this device will become apparent below. |
74 The significance of this device will become apparent below. |