9690
|
1 |
(*<*)
|
|
2 |
theory Nested2 = Nested0:;
|
|
3 |
consts trev :: "('a,'b)term => ('a,'b)term";
|
|
4 |
(*>*)
|
|
5 |
|
|
6 |
text{*\noindent
|
|
7 |
The termintion condition is easily proved by induction:
|
|
8 |
*};
|
|
9 |
|
9754
|
10 |
lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)";
|
9690
|
11 |
by(induct_tac ts, auto);
|
|
12 |
(*<*)
|
|
13 |
recdef trev "measure size"
|
|
14 |
"trev (Var x) = Var x"
|
|
15 |
"trev (App f ts) = App f (rev(map trev ts))";
|
|
16 |
(*>*)
|
|
17 |
text{*\noindent
|
|
18 |
By making this theorem a simplification rule, \isacommand{recdef}
|
|
19 |
applies it automatically and the above definition of @{term"trev"}
|
|
20 |
succeeds now. As a reward for our effort, we can now prove the desired
|
|
21 |
lemma directly. The key is the fact that we no longer need the verbose
|
9792
|
22 |
induction schema for type @{text"term"} but the simpler one arising from
|
9690
|
23 |
@{term"trev"}:
|
|
24 |
*};
|
|
25 |
|
|
26 |
lemma "trev(trev t) = t";
|
|
27 |
apply(induct_tac t rule:trev.induct);
|
|
28 |
txt{*\noindent
|
|
29 |
This leaves us with a trivial base case @{term"trev (trev (Var x)) = Var x"} and the step case
|
|
30 |
@{term[display,margin=60]"ALL t. t : set ts --> trev (trev t) = t ==> trev (trev (App f ts)) = App f ts"}
|
|
31 |
both of which are solved by simplification:
|
|
32 |
*};
|
|
33 |
|
9933
|
34 |
by(simp_all add:rev_map sym[OF map_compose] cong:map_cong);
|
9690
|
35 |
|
|
36 |
text{*\noindent
|
9721
|
37 |
If the proof of the induction step mystifies you, we recommend to go through
|
9754
|
38 |
the chain of simplification steps in detail; you will probably need the help of
|
9933
|
39 |
@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
|
9721
|
40 |
%\begin{quote}
|
|
41 |
%{term[display]"trev(trev(App f ts))"}\\
|
|
42 |
%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
|
|
43 |
%{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\
|
|
44 |
%{term[display]"App f (map trev (map trev ts))"}\\
|
|
45 |
%{term[display]"App f (map (trev o trev) ts)"}\\
|
|
46 |
%{term[display]"App f (map (%x. x) ts)"}\\
|
|
47 |
%{term[display]"App f ts"}
|
|
48 |
%\end{quote}
|
9690
|
49 |
|
9754
|
50 |
The above definition of @{term"trev"} is superior to the one in
|
|
51 |
\S\ref{sec:nested-datatype} because it brings @{term"rev"} into play, about
|
|
52 |
which already know a lot, in particular @{prop"rev(rev xs) = xs"}.
|
9690
|
53 |
Thus this proof is a good example of an important principle:
|
|
54 |
\begin{quote}
|
|
55 |
\emph{Chose your definitions carefully\\
|
|
56 |
because they determine the complexity of your proofs.}
|
|
57 |
\end{quote}
|
|
58 |
|
9721
|
59 |
Let us now return to the question of how \isacommand{recdef} can come up with
|
|
60 |
sensible termination conditions in the presence of higher-order functions
|
|
61 |
like @{term"map"}. For a start, if nothing were known about @{term"map"},
|
|
62 |
@{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus
|
|
63 |
\isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
|
9754
|
64 |
(term_list_size ts)"}, without any assumption about @{term"t"}. Therefore
|
9721
|
65 |
\isacommand{recdef} has been supplied with the congruence theorem
|
9792
|
66 |
@{thm[source]map_cong}:
|
9690
|
67 |
@{thm[display,margin=50]"map_cong"[no_vars]}
|
9721
|
68 |
Its second premise expresses (indirectly) that the second argument of
|
|
69 |
@{term"map"} is only applied to elements of its third argument. Congruence
|
|
70 |
rules for other higher-order functions on lists would look very similar but
|
|
71 |
have not been proved yet because they were never needed. If you get into a
|
|
72 |
situation where you need to supply \isacommand{recdef} with new congruence
|
9940
|
73 |
rules, you can either append a hint locally
|
|
74 |
to the specific occurrence of \isacommand{recdef}
|
|
75 |
*}
|
|
76 |
(*<*)
|
|
77 |
consts dummy :: "nat => nat"
|
|
78 |
recdef dummy "{}"
|
|
79 |
"dummy n = n"
|
|
80 |
(*>*)
|
|
81 |
(hints cong: map_cong)
|
9690
|
82 |
|
9940
|
83 |
text{*\noindent
|
|
84 |
or declare them globally
|
|
85 |
by giving them the @{text recdef_cong} attribute as in
|
|
86 |
*}
|
|
87 |
|
|
88 |
declare map_cong[recdef_cong];
|
|
89 |
|
|
90 |
text{*
|
|
91 |
Note that the global @{text cong} and @{text recdef_cong} attributes are
|
|
92 |
intentionally kept apart because they control different activities, namely
|
|
93 |
simplification and making recursive definitions. The local @{text cong} in
|
|
94 |
the hints section of \isacommand{recdef} is merely short for @{text
|
|
95 |
recdef_cong}.
|
9933
|
96 |
%The simplifier's congruence rules cannot be used by recdef.
|
|
97 |
%For example the weak congruence rules for if and case would prevent
|
|
98 |
%recdef from generating sensible termination conditions.
|
9690
|
99 |
*};
|
|
100 |
(*<*)end;(*>*)
|