1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{Nested{\isadigit{2}}}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 \isanewline |
|
16 % |
|
17 \endisadelimtheory |
|
18 \isacommand{lemma}\isamarkupfalse% |
|
19 \ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc{\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}{\isachardoublequoteclose}\isanewline |
|
20 % |
|
21 \isadelimproof |
|
22 % |
|
23 \endisadelimproof |
|
24 % |
|
25 \isatagproof |
|
26 \isacommand{by}\isamarkupfalse% |
|
27 {\isacharparenleft}induct{\isacharunderscore}tac\ ts{\isacharcomma}\ auto{\isacharparenright}% |
|
28 \endisatagproof |
|
29 {\isafoldproof}% |
|
30 % |
|
31 \isadelimproof |
|
32 % |
|
33 \endisadelimproof |
|
34 % |
|
35 \begin{isamarkuptext}% |
|
36 \noindent |
|
37 By making this theorem a simplification rule, \isacommand{recdef} |
|
38 applies it automatically and the definition of \isa{trev} |
|
39 succeeds now. As a reward for our effort, we can now prove the desired |
|
40 lemma directly. We no longer need the verbose |
|
41 induction schema for type \isa{term} and can use the simpler one arising from |
|
42 \isa{trev}:% |
|
43 \end{isamarkuptext}% |
|
44 \isamarkuptrue% |
|
45 \isacommand{lemma}\isamarkupfalse% |
|
46 \ {\isachardoublequoteopen}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequoteclose}\isanewline |
|
47 % |
|
48 \isadelimproof |
|
49 % |
|
50 \endisadelimproof |
|
51 % |
|
52 \isatagproof |
|
53 \isacommand{apply}\isamarkupfalse% |
|
54 {\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}\ trev{\isachardot}induct{\isacharparenright}% |
|
55 \begin{isamarkuptxt}% |
|
56 \begin{isabelle}% |
|
57 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x{\isachardot}\ trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x\isanewline |
|
58 \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}f\ ts{\isachardot}\isanewline |
|
59 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }{\isasymforall}x{\isachardot}\ x\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ x{\isacharparenright}\ {\isacharequal}\ x\ {\isasymLongrightarrow}\isanewline |
|
60 \isaindent{\ {\isadigit{2}}{\isachardot}\ \ \ \ }trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts% |
|
61 \end{isabelle} |
|
62 Both the base case and the induction step fall to simplification:% |
|
63 \end{isamarkuptxt}% |
|
64 \isamarkuptrue% |
|
65 \isacommand{by}\isamarkupfalse% |
|
66 {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}% |
|
67 \endisatagproof |
|
68 {\isafoldproof}% |
|
69 % |
|
70 \isadelimproof |
|
71 % |
|
72 \endisadelimproof |
|
73 % |
|
74 \begin{isamarkuptext}% |
|
75 \noindent |
|
76 If the proof of the induction step mystifies you, we recommend that you go through |
|
77 the chain of simplification steps in detail; you will probably need the help of |
|
78 \isa{trace{\isacharunderscore}simp}. Theorem \isa{map{\isacharunderscore}cong} is discussed below. |
|
79 %\begin{quote} |
|
80 %{term[display]"trev(trev(App f ts))"}\\ |
|
81 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\ |
|
82 %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\ |
|
83 %{term[display]"App f (map trev (map trev ts))"}\\ |
|
84 %{term[display]"App f (map (trev o trev) ts)"}\\ |
|
85 %{term[display]"App f (map (%x. x) ts)"}\\ |
|
86 %{term[display]"App f ts"} |
|
87 %\end{quote} |
|
88 |
|
89 The definition of \isa{trev} above is superior to the one in |
|
90 \S\ref{sec:nested-datatype} because it uses \isa{rev} |
|
91 and lets us use existing facts such as \hbox{\isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}}. |
|
92 Thus this proof is a good example of an important principle: |
|
93 \begin{quote} |
|
94 \emph{Chose your definitions carefully\\ |
|
95 because they determine the complexity of your proofs.} |
|
96 \end{quote} |
|
97 |
|
98 Let us now return to the question of how \isacommand{recdef} can come up with |
|
99 sensible termination conditions in the presence of higher-order functions |
|
100 like \isa{map}. For a start, if nothing were known about \isa{map}, then |
|
101 \isa{map\ trev\ ts} might apply \isa{trev} to arbitrary terms, and thus |
|
102 \isacommand{recdef} would try to prove the unprovable \isa{size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}, without any assumption about \isa{t}. Therefore |
|
103 \isacommand{recdef} has been supplied with the congruence theorem |
|
104 \isa{map{\isacharunderscore}cong}: |
|
105 \begin{isabelle}% |
|
106 \ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline |
|
107 \isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys% |
|
108 \end{isabelle} |
|
109 Its second premise expresses that in \isa{map\ f\ xs}, |
|
110 function \isa{f} is only applied to elements of list \isa{xs}. Congruence |
|
111 rules for other higher-order functions on lists are similar. If you get |
|
112 into a situation where you need to supply \isacommand{recdef} with new |
|
113 congruence rules, you can append a hint after the end of |
|
114 the recursion equations:\cmmdx{hints}% |
|
115 \end{isamarkuptext}% |
|
116 \isamarkuptrue% |
|
117 {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}% |
|
118 \begin{isamarkuptext}% |
|
119 \noindent |
|
120 Or you can declare them globally |
|
121 by giving them the \attrdx{recdef_cong} attribute:% |
|
122 \end{isamarkuptext}% |
|
123 \isamarkuptrue% |
|
124 \isacommand{declare}\isamarkupfalse% |
|
125 \ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}% |
|
126 \begin{isamarkuptext}% |
|
127 The \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are |
|
128 intentionally kept apart because they control different activities, namely |
|
129 simplification and making recursive definitions. |
|
130 %The simplifier's congruence rules cannot be used by recdef. |
|
131 %For example the weak congruence rules for if and case would prevent |
|
132 %recdef from generating sensible termination conditions.% |
|
133 \end{isamarkuptext}% |
|
134 \isamarkuptrue% |
|
135 % |
|
136 \isadelimtheory |
|
137 % |
|
138 \endisadelimtheory |
|
139 % |
|
140 \isatagtheory |
|
141 % |
|
142 \endisatagtheory |
|
143 {\isafoldtheory}% |
|
144 % |
|
145 \isadelimtheory |
|
146 % |
|
147 \endisadelimtheory |
|
148 \end{isabellebody}% |
|
149 %%% Local Variables: |
|
150 %%% mode: latex |
|
151 %%% TeX-master: "root" |
|
152 %%% End: |
|