2 % |
2 % |
3 \begin{isamarkuptext}% |
3 \begin{isamarkuptext}% |
4 \noindent |
4 \noindent |
5 The termintion condition is easily proved by induction:% |
5 The termintion condition is easily proved by induction:% |
6 \end{isamarkuptext}% |
6 \end{isamarkuptext}% |
7 \isacommand{lemma}\ [simp]:\ {"}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ <\ Suc(term\_size\ ts){"}\isanewline |
7 \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequote}\isanewline |
8 \isacommand{by}(induct\_tac\ ts,\ auto)% |
8 \isacommand{by}{\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}% |
9 \begin{isamarkuptext}% |
9 \begin{isamarkuptext}% |
10 \noindent |
10 \noindent |
11 By making this theorem a simplification rule, \isacommand{recdef} |
11 By making this theorem a simplification rule, \isacommand{recdef} |
12 applies it automatically and the above definition of \isa{trev} |
12 applies it automatically and the above definition of \isa{trev} |
13 succeeds now. As a reward for our effort, we can now prove the desired |
13 succeeds now. As a reward for our effort, we can now prove the desired |
14 lemma directly. The key is the fact that we no longer need the verbose |
14 lemma directly. The key is the fact that we no longer need the verbose |
15 induction schema for type \isa{term} but the simpler one arising from |
15 induction schema for type \isa{term} but the simpler one arising from |
16 \isa{trev}:% |
16 \isa{trev}:% |
17 \end{isamarkuptext}% |
17 \end{isamarkuptext}% |
18 \isacommand{lemmas}\ [cong]\ =\ map\_cong\isanewline |
18 \isacommand{lemmas}\ {\isacharbrackleft}cong{\isacharbrackright}\ {\isacharequal}\ map{\isacharunderscore}cong\isanewline |
19 \isacommand{lemma}\ {"}trev(trev\ t)\ =\ t{"}\isanewline |
19 \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline |
20 \isacommand{apply}(induct\_tac\ t\ rule:trev.induct)% |
20 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}% |
21 \begin{isamarkuptxt}% |
21 \begin{isamarkuptxt}% |
22 \noindent |
22 \noindent |
23 This leaves us with a trivial base case \isa{trev\ (trev\ (Var\ \mbox{x}))\ =\ Var\ \mbox{x}} and the step case |
23 This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ \mbox{x}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ \mbox{x}} and the step case |
24 \begin{quote} |
24 \begin{quote} |
25 |
25 |
26 \begin{isabelle}% |
26 \begin{isabelle}% |
27 {\isasymforall}\mbox{t}.\ \mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ trev\ (trev\ \mbox{t})\ =\ \mbox{t}\ {\isasymLongrightarrow}\isanewline |
27 {\isasymforall}\mbox{t}{\isachardot}\ \mbox{t}\ {\isasymin}\ set\ \mbox{ts}\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ \mbox{t}{\isacharparenright}\ {\isacharequal}\ \mbox{t}\ {\isasymLongrightarrow}\isanewline |
28 trev\ (trev\ (App\ \mbox{f}\ \mbox{ts}))\ =\ App\ \mbox{f}\ \mbox{ts} |
28 trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ \mbox{f}\ \mbox{ts}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ \mbox{f}\ \mbox{ts} |
29 \end{isabelle}% |
29 \end{isabelle}% |
30 |
30 |
31 \end{quote} |
31 \end{quote} |
32 both of which are solved by simplification:% |
32 both of which are solved by simplification:% |
33 \end{isamarkuptxt}% |
33 \end{isamarkuptxt}% |
34 \isacommand{by}(simp\_all\ del:map\_compose\ add:sym[OF\ map\_compose]\ rev\_map)% |
34 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ del{\isacharcolon}map{\isacharunderscore}compose\ add{\isacharcolon}sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ rev{\isacharunderscore}map{\isacharparenright}% |
35 \begin{isamarkuptext}% |
35 \begin{isamarkuptext}% |
36 \noindent |
36 \noindent |
37 If this surprises you, see Datatype/Nested2...... |
37 If this surprises you, see Datatype/Nested2...... |
38 |
38 |
39 The above definition of \isa{trev} is superior to the one in \S\ref{sec:nested-datatype} |
39 The above definition of \isa{trev} is superior to the one in \S\ref{sec:nested-datatype} |
40 because it brings \isa{rev} into play, about which already know a lot, in particular |
40 because it brings \isa{rev} into play, about which already know a lot, in particular |
41 \isa{rev\ (rev\ \mbox{xs})\ =\ \mbox{xs}}. |
41 \isa{rev\ {\isacharparenleft}rev\ \mbox{xs}{\isacharparenright}\ {\isacharequal}\ \mbox{xs}}. |
42 Thus this proof is a good example of an important principle: |
42 Thus this proof is a good example of an important principle: |
43 \begin{quote} |
43 \begin{quote} |
44 \emph{Chose your definitions carefully\\ |
44 \emph{Chose your definitions carefully\\ |
45 because they determine the complexity of your proofs.} |
45 because they determine the complexity of your proofs.} |
46 \end{quote} |
46 \end{quote} |
47 |
47 |
48 Let us now return to the question of how \isacommand{recdef} can come up with sensible termination |
48 Let us now return to the question of how \isacommand{recdef} can come up with sensible termination |
49 conditions in the presence of higher-order functions like \isa{map}. For a start, if nothing |
49 conditions in the presence of higher-order functions like \isa{map}. For a start, if nothing |
50 were known about \isa{map}, \isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms, |
50 were known about \isa{map}, \isa{map\ trev\ \mbox{ts}} might apply \isa{trev} to arbitrary terms, |
51 and thus \isacommand{recdef} would try to prove the unprovable |
51 and thus \isacommand{recdef} would try to prove the unprovable |
52 \isa{size\ \mbox{t}\ <\ Suc\ (term\_size\ \mbox{ts})}, without any assumption about \isa{t}. |
52 \isa{size\ \mbox{t}\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}size\ \mbox{ts}{\isacharparenright}}, without any assumption about \isa{t}. |
53 Therefore \isacommand{recdef} has been supplied with the congruence theorem \isa{map\_cong}: |
53 Therefore \isacommand{recdef} has been supplied with the congruence theorem \isa{map\_cong}: |
54 \begin{quote} |
54 \begin{quote} |
55 |
55 |
56 \begin{isabelle}% |
56 \begin{isabelle}% |
57 {\isasymlbrakk}\mbox{xs}\ =\ \mbox{ys};\ {\isasymAnd}\mbox{x}.\ \mbox{x}\ {\isasymin}\ set\ \mbox{ys}\ {\isasymLongrightarrow}\ \mbox{f}\ \mbox{x}\ =\ \mbox{g}\ \mbox{x}{\isasymrbrakk}\isanewline |
57 {\isasymlbrakk}\mbox{xs}\ {\isacharequal}\ \mbox{ys}{\isacharsemicolon}\ {\isasymAnd}\mbox{x}{\isachardot}\ \mbox{x}\ {\isasymin}\ set\ \mbox{ys}\ {\isasymLongrightarrow}\ \mbox{f}\ \mbox{x}\ {\isacharequal}\ \mbox{g}\ \mbox{x}{\isasymrbrakk}\isanewline |
58 {\isasymLongrightarrow}\ map\ \mbox{f}\ \mbox{xs}\ =\ map\ \mbox{g}\ \mbox{ys} |
58 {\isasymLongrightarrow}\ map\ \mbox{f}\ \mbox{xs}\ {\isacharequal}\ map\ \mbox{g}\ \mbox{ys} |
59 \end{isabelle}% |
59 \end{isabelle}% |
60 |
60 |
61 \end{quote} |
61 \end{quote} |
62 Its second premise expresses (indirectly) that the second argument of \isa{map} is only applied |
62 Its second premise expresses (indirectly) that the second argument of \isa{map} is only applied |
63 to elements of its third argument. Congruence rules for other higher-order functions on lists would |
63 to elements of its third argument. Congruence rules for other higher-order functions on lists would |