13 \noindent |
13 \noindent |
14 Note that we need to quote \isa{term} on the left to avoid confusion with |
14 Note that we need to quote \isa{term} on the left to avoid confusion with |
15 the command \isacommand{term}. |
15 the command \isacommand{term}. |
16 Parameter \isa{{\isacharprime}a} is the type of variables and \isa{{\isacharprime}b} the type of |
16 Parameter \isa{{\isacharprime}a} is the type of variables and \isa{{\isacharprime}b} the type of |
17 function symbols. |
17 function symbols. |
18 A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isacharbrackleft}term{\isachardot}Var\ x{\isacharcomma}\ App\ g\ {\isacharbrackleft}term{\isachardot}Var\ y{\isacharbrackright}{\isacharbrackright}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are |
18 A mathematical term like $f(x,g(y))$ becomes \isa{App\ f\ {\isacharbrackleft}Var\ x{\isacharcomma}\ App\ g\ {\isacharbrackleft}Var\ y{\isacharbrackright}{\isacharbrackright}}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are |
19 suitable values, e.g.\ numbers or strings. |
19 suitable values, e.g.\ numbers or strings. |
20 |
20 |
21 What complicates the definition of \isa{term} is the nested occurrence of |
21 What complicates the definition of \isa{term} is the nested occurrence of |
22 \isa{term} inside \isa{list} on the right-hand side. In principle, |
22 \isa{term} inside \isa{list} on the right-hand side. In principle, |
23 nested recursion can be eliminated in favour of mutual recursion by unfolding |
23 nested recursion can be eliminated in favour of mutual recursion by unfolding |
48 \isanewline |
48 \isanewline |
49 \ \ {\isachardoublequote}substs\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
49 \ \ {\isachardoublequote}substs\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequote}\isanewline |
50 \ \ {\isachardoublequote}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequote}% |
50 \ \ {\isachardoublequote}substs\ s\ {\isacharparenleft}t\ {\isacharhash}\ ts{\isacharparenright}\ {\isacharequal}\ subst\ s\ t\ {\isacharhash}\ substs\ s\ ts{\isachardoublequote}% |
51 \begin{isamarkuptext}% |
51 \begin{isamarkuptext}% |
52 \noindent |
52 \noindent |
53 You should ignore the label \isa{subst{\isacharunderscore}App} for the moment. |
53 (Please ignore the label \isa{subst{\isacharunderscore}App} for the moment.) |
54 |
54 |
55 Similarly, when proving a statement about terms inductively, we need |
55 Similarly, when proving a statement about terms inductively, we need |
56 to prove a related statement about term lists simultaneously. For example, |
56 to prove a related statement about term lists simultaneously. For example, |
57 the fact that the identity substitution does not change a term needs to be |
57 the fact that the identity substitution does not change a term needs to be |
58 strengthened and proved as follows:% |
58 strengthened and proved as follows:% |
60 \isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline |
60 \isacommand{lemma}\ {\isachardoublequote}subst\ \ Var\ t\ \ {\isacharequal}\ {\isacharparenleft}t\ {\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isacharparenright}\ \ {\isasymand}\isanewline |
61 \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline |
61 \ \ \ \ \ \ \ \ substs\ Var\ ts\ {\isacharequal}\ {\isacharparenleft}ts{\isacharcolon}{\isacharcolon}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ list{\isacharparenright}{\isachardoublequote}\isanewline |
62 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% |
62 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ \isakeyword{and}\ ts{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}% |
63 \begin{isamarkuptext}% |
63 \begin{isamarkuptext}% |
64 \noindent |
64 \noindent |
65 Note that \isa{term{\isachardot}Var} is the identity substitution because by definition it |
65 Note that \isa{Var} is the identity substitution because by definition it |
66 leaves variables unchanged: \isa{subst\ term{\isachardot}Var\ {\isacharparenleft}term{\isachardot}Var\ x{\isacharparenright}\ {\isacharequal}\ term{\isachardot}Var\ x}. Note also |
66 leaves variables unchanged: \isa{subst\ Var\ {\isacharparenleft}Var\ x{\isacharparenright}\ {\isacharequal}\ Var\ x}. Note also |
67 that the type annotations are necessary because otherwise there is nothing in |
67 that the type annotations are necessary because otherwise there is nothing in |
68 the goal to enforce that both halves of the goal talk about the same type |
68 the goal to enforce that both halves of the goal talk about the same type |
69 parameters \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}}. As a result, induction would fail |
69 parameters \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}}. As a result, induction would fail |
70 because the two halves of the goal would be unrelated. |
70 because the two halves of the goal would be unrelated. |
71 |
71 |
101 \begin{isamarkuptext}% |
101 \begin{isamarkuptext}% |
102 \noindent |
102 \noindent |
103 What is more, we can now disable the old defining equation as a |
103 What is more, we can now disable the old defining equation as a |
104 simplification rule:% |
104 simplification rule:% |
105 \end{isamarkuptext}% |
105 \end{isamarkuptext}% |
106 \isacommand{lemmas}\ {\isacharbrackleft}simp\ del{\isacharbrackright}\ {\isacharequal}\ subst{\isacharunderscore}App% |
106 \isacommand{declare}\ subst{\isacharunderscore}App\ {\isacharbrackleft}simp\ del{\isacharbrackright}% |
107 \begin{isamarkuptext}% |
107 \begin{isamarkuptext}% |
108 \noindent |
108 \noindent |
109 The advantage is that now we have replaced \isa{substs} by |
109 The advantage is that now we have replaced \isa{substs} by |
110 \isa{map}, we can profit from the large number of pre-proved lemmas |
110 \isa{map}, we can profit from the large number of pre-proved lemmas |
111 about \isa{map}. Unfortunately inductive proofs about type |
111 about \isa{map}. Unfortunately inductive proofs about type |