equal
deleted
inserted
replaced
12 text\<open>\noindent |
12 text\<open>\noindent |
13 By making this theorem a simplification rule, \isacommand{recdef} |
13 By making this theorem a simplification rule, \isacommand{recdef} |
14 applies it automatically and the definition of @{term"trev"} |
14 applies it automatically and the definition of @{term"trev"} |
15 succeeds now. As a reward for our effort, we can now prove the desired |
15 succeeds now. As a reward for our effort, we can now prove the desired |
16 lemma directly. We no longer need the verbose |
16 lemma directly. We no longer need the verbose |
17 induction schema for type @{text"term"} and can use the simpler one arising from |
17 induction schema for type \<open>term\<close> and can use the simpler one arising from |
18 @{term"trev"}: |
18 @{term"trev"}: |
19 \<close> |
19 \<close> |
20 |
20 |
21 lemma "trev(trev t) = t" |
21 lemma "trev(trev t) = t" |
22 apply(induct_tac t rule: trev.induct) |
22 apply(induct_tac t rule: trev.induct) |
28 by(simp_all add: rev_map sym[OF map_compose] cong: map_cong) |
28 by(simp_all add: rev_map sym[OF map_compose] cong: map_cong) |
29 |
29 |
30 text\<open>\noindent |
30 text\<open>\noindent |
31 If the proof of the induction step mystifies you, we recommend that you go through |
31 If the proof of the induction step mystifies you, we recommend that you go through |
32 the chain of simplification steps in detail; you will probably need the help of |
32 the chain of simplification steps in detail; you will probably need the help of |
33 @{text"simp_trace"}. Theorem @{thm[source]map_cong} is discussed below. |
33 \<open>simp_trace\<close>. Theorem @{thm[source]map_cong} is discussed below. |
34 %\begin{quote} |
34 %\begin{quote} |
35 %{term[display]"trev(trev(App f ts))"}\\ |
35 %{term[display]"trev(trev(App f ts))"}\\ |
36 %{term[display]"App f (rev(map trev (rev(map trev 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))))"}\\ |
37 %{term[display]"App f (map trev (rev(rev(map trev ts))))"}\\ |
38 %{term[display]"App f (map trev (map trev ts))"}\\ |
38 %{term[display]"App f (map trev (map trev ts))"}\\ |
79 \<close> |
79 \<close> |
80 |
80 |
81 declare map_cong[recdef_cong] |
81 declare map_cong[recdef_cong] |
82 |
82 |
83 text\<open> |
83 text\<open> |
84 The @{text cong} and @{text recdef_cong} attributes are |
84 The \<open>cong\<close> and \<open>recdef_cong\<close> attributes are |
85 intentionally kept apart because they control different activities, namely |
85 intentionally kept apart because they control different activities, namely |
86 simplification and making recursive definitions. |
86 simplification and making recursive definitions. |
87 %The simplifier's congruence rules cannot be used by recdef. |
87 %The simplifier's congruence rules cannot be used by recdef. |
88 %For example the weak congruence rules for if and case would prevent |
88 %For example the weak congruence rules for if and case would prevent |
89 %recdef from generating sensible termination conditions. |
89 %recdef from generating sensible termination conditions. |