2 theory Nested2 = Nested0:
5 text{*The termination condition is easily proved by induction:*}
7 lemma [simp]: "t \<in> set ts \<longrightarrow> size t < Suc(term_list_size ts)"
8 by(induct_tac ts, auto)
10 recdef trev "measure size"
11 "trev (Var x) = Var x"
12 "trev (App f ts) = App f (rev(map trev ts))"
15 By making this theorem a simplification rule, \isacommand{recdef}
16 applies it automatically and the definition of @{term"trev"}
17 succeeds now. As a reward for our effort, we can now prove the desired
18 lemma directly. We no longer need the verbose
19 induction schema for type @{text"term"} and can use the simpler one arising from
23 lemma "trev(trev t) = t"
24 apply(induct_tac t rule:trev.induct)
26 @{subgoals[display,indent=0]}
27 Both the base case and the induction step fall to simplification:
30 by(simp_all add:rev_map sym[OF map_compose] cong:map_cong)
33 If the proof of the induction step mystifies you, we recommend that you go through
34 the chain of simplification steps in detail; you will probably need the help of
35 @{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
37 %{term[display]"trev(trev(App f ts))"}\\
38 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
39 %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\
40 %{term[display]"App f (map trev (map trev ts))"}\\
41 %{term[display]"App f (map (trev o trev) ts)"}\\
42 %{term[display]"App f (map (%x. x) ts)"}\\
43 %{term[display]"App f ts"}
46 The definition of @{term"trev"} above is superior to the one in
47 \S\ref{sec:nested-datatype} because it uses @{term"rev"}
48 and lets us use existing facts such as \hbox{@{prop"rev(rev xs) = xs"}}.
49 Thus this proof is a good example of an important principle:
51 \emph{Chose your definitions carefully\\
52 because they determine the complexity of your proofs.}
55 Let us now return to the question of how \isacommand{recdef} can come up with
56 sensible termination conditions in the presence of higher-order functions
57 like @{term"map"}. For a start, if nothing were known about @{term"map"},
58 @{term"map trev ts"} might apply @{term"trev"} to arbitrary terms, and thus
59 \isacommand{recdef} would try to prove the unprovable @{term"size t < Suc
60 (term_list_size ts)"}, without any assumption about @{term"t"}. Therefore
61 \isacommand{recdef} has been supplied with the congruence theorem
62 @{thm[source]map_cong}:
63 @{thm[display,margin=50]"map_cong"[no_vars]}
64 Its second premise expresses (indirectly) that the first argument of
65 @{term"map"} is only applied to elements of its second argument. Congruence
66 rules for other higher-order functions on lists look very similar. If you get
67 into a situation where you need to supply \isacommand{recdef} with new
68 congruence rules, you can either append a hint after the end of
69 the recursion equations
72 consts dummy :: "nat => nat"
76 (hints recdef_cong: map_cong)
79 or declare them globally
80 by giving them the \isaindexbold{recdef_cong} attribute as in
83 declare map_cong[recdef_cong]
86 Note that the @{text cong} and @{text recdef_cong} attributes are
87 intentionally kept apart because they control different activities, namely
88 simplification and making recursive definitions.
89 % The local @{text cong} in
90 % the hints section of \isacommand{recdef} is merely short for @{text recdef_cong}.
91 %The simplifier's congruence rules cannot be used by recdef.
92 %For example the weak congruence rules for if and case would prevent
93 %recdef from generating sensible termination conditions.