30 seasoned functional programmer might have written @{term"map_bt f o F"} |
30 seasoned functional programmer might have written @{term"map_bt f o F"} |
31 instead of @{term"%i. map_bt f (F i)"}, but the former is not accepted by |
31 instead of @{term"%i. map_bt f (F i)"}, but the former is not accepted by |
32 Isabelle because the termination proof is not as obvious since |
32 Isabelle because the termination proof is not as obvious since |
33 @{term"map_bt"} is only partially applied. |
33 @{term"map_bt"} is only partially applied. |
34 |
34 |
35 The following lemma has a canonical proof *} |
35 The following lemma has a canonical proof: *} |
36 |
36 |
37 lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; |
37 lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; |
38 apply(induct_tac T, simp_all) |
38 apply(induct_tac T, simp_all) |
39 done |
39 done |
40 (*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; |
40 (*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; |
41 apply(induct_tac T, rename_tac[2] F)(*>*) |
41 apply(induct_tac T, rename_tac[2] F)(*>*) |
42 txt{*\noindent |
42 txt{*\noindent |
43 but it is worth taking a look at the proof state after the induction step |
43 It is worth taking a look at the proof state after the induction step |
44 to understand what the presence of the function type entails: |
44 to understand what the presence of the function type entails. |
|
45 Notice the quantified induction hypothesis: |
45 @{subgoals[display,indent=0]} |
46 @{subgoals[display,indent=0]} |
46 *} |
47 *} |
47 (*<*) |
48 (*<*) |
48 oops |
49 oops |
49 end |
50 end |