equal
deleted
inserted
replaced
17 induction schema for type @{text"term"} and can use the simpler one arising from |
17 induction schema for type @{text"term"} and can use the simpler one arising from |
18 @{term"trev"}: |
18 @{term"trev"}: |
19 *} |
19 *} |
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) |
23 txt{* |
23 txt{* |
24 @{subgoals[display,indent=0]} |
24 @{subgoals[display,indent=0]} |
25 Both the base case and the induction step fall to simplification: |
25 Both the base case and the induction step fall to simplification: |
26 *} |
26 *} |
27 |
27 |
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{*\noindent |
30 text{*\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"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below. |
33 @{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below. |