equal
deleted
inserted
replaced
32 however will reject. Applying @{term"map_bt"} to only one of its arguments |
32 however will reject. Applying @{term"map_bt"} to only one of its arguments |
33 makes the termination proof less obvious. |
33 makes the termination proof less obvious. |
34 |
34 |
35 The following lemma has a simple proof by induction: *} |
35 The following lemma has a simple proof by induction: *} |
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 Because of the function type, the proof state after induction looks unusual. |
43 Because of the function type, the proof state after induction looks unusual. |
44 Notice the quantified induction hypothesis: |
44 Notice the quantified induction hypothesis: |
45 @{subgoals[display,indent=0]} |
45 @{subgoals[display,indent=0]} |