summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Doc/Tutorial/Misc/Itrev.thy

changeset 58860 | fee7cfa69c50 |

parent 48985 | 5386df44a037 |

child 67406 | 23307fd33906 |

1.1 --- a/src/Doc/Tutorial/Misc/Itrev.thy Sat Nov 01 11:40:55 2014 +0100 1.2 +++ b/src/Doc/Tutorial/Misc/Itrev.thy Sat Nov 01 14:20:38 2014 +0100 1.3 @@ -58,15 +58,15 @@ 1.4 1.5 Naturally, we would like to show that @{term"itrev"} does indeed reverse 1.6 its first argument provided the second one is empty: 1.7 -*}; 1.8 +*} 1.9 1.10 -lemma "itrev xs [] = rev xs"; 1.11 +lemma "itrev xs [] = rev xs" 1.12 1.13 txt{*\noindent 1.14 There is no choice as to the induction variable, and we immediately simplify: 1.15 -*}; 1.16 +*} 1.17 1.18 -apply(induct_tac xs, simp_all); 1.19 +apply(induct_tac xs, simp_all) 1.20 1.21 txt{*\noindent 1.22 Unfortunately, this attempt does not prove 1.23 @@ -80,9 +80,9 @@ 1.24 \end{quote} 1.25 Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is 1.26 just not true. The correct generalization is 1.27 -*}; 1.28 -(*<*)oops;(*>*) 1.29 -lemma "itrev xs ys = rev xs @ ys"; 1.30 +*} 1.31 +(*<*)oops(*>*) 1.32 +lemma "itrev xs ys = rev xs @ ys" 1.33 (*<*)apply(induct_tac xs, simp_all)(*>*) 1.34 txt{*\noindent 1.35 If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to 1.36 @@ -100,11 +100,11 @@ 1.37 the subgoal, but the induction hypothesis needs to be applied with 1.38 @{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem 1.39 for all @{term"ys"} instead of a fixed one: 1.40 -*}; 1.41 -(*<*)oops;(*>*) 1.42 -lemma "\<forall>ys. itrev xs ys = rev xs @ ys"; 1.43 +*} 1.44 +(*<*)oops(*>*) 1.45 +lemma "\<forall>ys. itrev xs ys = rev xs @ ys" 1.46 (*<*) 1.47 -by(induct_tac xs, simp_all); 1.48 +by(induct_tac xs, simp_all) 1.49 (*>*) 1.50 1.51 text{*\noindent