author | wenzelm |
Tue, 28 Aug 2012 18:57:32 +0200 | |
changeset 48985 | 5386df44a037 |
parent 40878 | doc-src/TutorialI/Recdef/Nested2.thy@7695e4de4d86 |
child 56846 | 9df717fef2bb |
permissions | -rw-r--r-- |
9690 | 1 |
(*<*) |
16417 | 2 |
theory Nested2 imports Nested0 begin |
9690 | 3 |
(*>*) |
4 |
||
11196 | 5 |
lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)" |
6 |
by(induct_tac ts, auto) |
|
9690 | 7 |
(*<*) |
8 |
recdef trev "measure size" |
|
9 |
"trev (Var x) = Var x" |
|
11196 | 10 |
"trev (App f ts) = App f (rev(map trev ts))" |
9690 | 11 |
(*>*) |
12 |
text{*\noindent |
|
13 |
By making this theorem a simplification rule, \isacommand{recdef} |
|
10885 | 14 |
applies it automatically and the definition of @{term"trev"} |
9690 | 15 |
succeeds now. As a reward for our effort, we can now prove the desired |
10885 | 16 |
lemma directly. We no longer need the verbose |
17 |
induction schema for type @{text"term"} and can use the simpler one arising from |
|
9690 | 18 |
@{term"trev"}: |
11196 | 19 |
*} |
9690 | 20 |
|
11196 | 21 |
lemma "trev(trev t) = t" |
12815 | 22 |
apply(induct_tac t rule: trev.induct) |
11196 | 23 |
txt{* |
24 |
@{subgoals[display,indent=0]} |
|
25 |
Both the base case and the induction step fall to simplification: |
|
26 |
*} |
|
9690 | 27 |
|
12815 | 28 |
by(simp_all add: rev_map sym[OF map_compose] cong: map_cong) |
9690 | 29 |
|
30 |
text{*\noindent |
|
10885 | 31 |
If the proof of the induction step mystifies you, we recommend that you go through |
9754 | 32 |
the chain of simplification steps in detail; you will probably need the help of |
40878
7695e4de4d86
renamed trace_simp to simp_trace, and debug_simp to simp_debug;
wenzelm
parents:
16417
diff
changeset
|
33 |
@{text"simp_trace"}. Theorem @{thm[source]map_cong} is discussed below. |
9721 | 34 |
%\begin{quote} |
35 |
%{term[display]"trev(trev(App f ts))"}\\ |
|
36 |
%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\ |
|
37 |
%{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\ |
|
38 |
%{term[display]"App f (map trev (map trev ts))"}\\ |
|
39 |
%{term[display]"App f (map (trev o trev) ts)"}\\ |
|
40 |
%{term[display]"App f (map (%x. x) ts)"}\\ |
|
41 |
%{term[display]"App f ts"} |
|
42 |
%\end{quote} |
|
9690 | 43 |
|
10885 | 44 |
The definition of @{term"trev"} above is superior to the one in |
45 |
\S\ref{sec:nested-datatype} because it uses @{term"rev"} |
|
46 |
and lets us use existing facts such as \hbox{@{prop"rev(rev xs) = xs"}}. |
|
9690 | 47 |
Thus this proof is a good example of an important principle: |
48 |
\begin{quote} |
|
49 |
\emph{Chose your definitions carefully\\ |
|
50 |
because they determine the complexity of your proofs.} |
|
51 |
\end{quote} |
|
52 |
||
9721 | 53 |
Let us now return to the question of how \isacommand{recdef} can come up with |
54 |
sensible termination conditions in the presence of higher-order functions |
|
11494 | 55 |
like @{term"map"}. For a start, if nothing were known about @{term"map"}, then |
9721 | 56 |
@{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus |
57 |
\isacommand{recdef} would try to prove the unprovable @{term"size t < Suc |
|
9754 | 58 |
(term_list_size ts)"}, without any assumption about @{term"t"}. Therefore |
9721 | 59 |
\isacommand{recdef} has been supplied with the congruence theorem |
9792 | 60 |
@{thm[source]map_cong}: |
9690 | 61 |
@{thm[display,margin=50]"map_cong"[no_vars]} |
11494 | 62 |
Its second premise expresses that in @{term"map f xs"}, |
63 |
function @{term"f"} is only applied to elements of list @{term"xs"}. Congruence |
|
64 |
rules for other higher-order functions on lists are similar. If you get |
|
10212 | 65 |
into a situation where you need to supply \isacommand{recdef} with new |
11494 | 66 |
congruence rules, you can append a hint after the end of |
13111 | 67 |
the recursion equations:\cmmdx{hints} |
9940 | 68 |
*} |
69 |
(*<*) |
|
70 |
consts dummy :: "nat => nat" |
|
71 |
recdef dummy "{}" |
|
72 |
"dummy n = n" |
|
73 |
(*>*) |
|
10171 | 74 |
(hints recdef_cong: map_cong) |
9690 | 75 |
|
9940 | 76 |
text{*\noindent |
11494 | 77 |
Or you can declare them globally |
78 |
by giving them the \attrdx{recdef_cong} attribute: |
|
9940 | 79 |
*} |
80 |
||
11196 | 81 |
declare map_cong[recdef_cong] |
9940 | 82 |
|
83 |
text{* |
|
11494 | 84 |
The @{text cong} and @{text recdef_cong} attributes are |
9940 | 85 |
intentionally kept apart because they control different activities, namely |
10171 | 86 |
simplification and making recursive definitions. |
9933 | 87 |
%The simplifier's congruence rules cannot be used by recdef. |
88 |
%For example the weak congruence rules for if and case would prevent |
|
89 |
%recdef from generating sensible termination conditions. |
|
11196 | 90 |
*} |
91 |
(*<*)end(*>*) |