summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 29 Sep 2014 22:09:05 +0200 | |

changeset 58486 | f62a887c3ae7 |

parent 58483 | d5f24630c104 |

child 58487 | 1ae4ab94ea63 |

tuned

src/Doc/Prog_Prove/Isar.thy | file | annotate | diff | comparison | revisions | |

src/Doc/Prog_Prove/Types_and_funs.thy | file | annotate | diff | comparison | revisions |

--- a/src/Doc/Prog_Prove/Isar.thy Mon Sep 29 21:34:48 2014 +0200 +++ b/src/Doc/Prog_Prove/Isar.thy Mon Sep 29 22:09:05 2014 +0200 @@ -546,7 +546,7 @@ Sometimes one would like to prove some lemma locally within a proof, a lemma that shares the current context of assumptions but that -has its own assumptions and is generalized over its locally fixed +has its own assumptions and is generalised over its locally fixed variables at the end. This is what a \concept{raw proof block} does: \begin{quote}\index{$IMP053@@{text"{ ... }"} (proof block)} @{text"{"} \isacom{fix} @{text"x\<^sub>1 \<dots> x\<^sub>n"}\\ @@ -1031,7 +1031,7 @@ \isacom{lemma} @{text[source]"I x y z \<Longrightarrow> x = r \<Longrightarrow> y = s \<Longrightarrow> z = t \<Longrightarrow> \<dots>"} \end{isabelle} Standard rule induction will work fine now, provided the free variables in -@{text r}, @{text s}, @{text t} are generalized via @{text"arbitrary"}. +@{text r}, @{text s}, @{text t} are generalised via @{text"arbitrary"}. However, induction can do the above transformation for us, behind the curtains, so we never need to see the expanded version of the lemma. This is what we need to write:

--- a/src/Doc/Prog_Prove/Types_and_funs.thy Mon Sep 29 21:34:48 2014 +0200 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy Mon Sep 29 22:09:05 2014 +0200 @@ -249,7 +249,7 @@ if the function is defined by recursion on argument number $i$.} \end{quote} The key heuristic, and the main point of this section, is to -\emph{generalize the goal before induction}. +\emph{generalise the goal before induction}. The reason is simple: if the goal is too specific, the induction hypothesis is too weak to allow the induction step to go through. Let us illustrate the idea with an example. @@ -294,10 +294,10 @@ argument,~@{term"[]"}, prevents it from rewriting the conclusion. This example suggests a heuristic: \begin{quote} -\emph{Generalize goals for induction by replacing constants by variables.} +\emph{Generalise goals for induction by replacing constants by variables.} \end{quote} Of course one cannot do this na\"{\i}vely: @{prop"itrev xs ys = rev xs"} is -just not true. The correct generalization is +just not true. The correct generalisation is *}; (*<*)oops;(*>*) lemma "itrev xs ys = rev xs @ ys" @@ -305,7 +305,7 @@ txt{* If @{text ys} is replaced by @{term"[]"}, the right-hand side simplifies to @{term"rev xs"}, as required. -In this instance it was easy to guess the right generalization. +In this instance it was easy to guess the right generalisation. Other situations can require a good deal of creativity. Although we now have two variables, only @{text xs} is suitable for @@ -313,12 +313,12 @@ not there: @{subgoals[display,margin=65]} The induction hypothesis is still too weak, but this time it takes no -intuition to generalize: the problem is that the @{text ys} +intuition to generalise: the problem is that the @{text ys} in the induction hypothesis is fixed, but the induction hypothesis needs to be applied with @{term"a # ys"} instead of @{text ys}. Hence we prove the theorem for all @{text ys} instead of a fixed one. We can instruct induction -to perform this generalization for us by adding @{text "arbitrary: ys"}\index{arbitrary@@{text"arbitrary:"}}. +to perform this generalisation for us by adding @{text "arbitrary: ys"}\index{arbitrary@@{text"arbitrary:"}}. *} (*<*)oops lemma "itrev xs ys = rev xs @ ys" @@ -334,12 +334,12 @@ done text{* -This leads to another heuristic for generalization: +This leads to another heuristic for generalisation: \begin{quote} -\emph{Generalize induction by generalizing all free +\emph{Generalise induction by generalising all free variables\\ {\em(except the induction variable itself)}.} \end{quote} -Generalization is best performed with @{text"arbitrary: y\<^sub>1 \<dots> y\<^sub>k"}. +Generalisation is best performed with @{text"arbitrary: y\<^sub>1 \<dots> y\<^sub>k"}. This heuristic prevents trivial failures like the one above. However, it should not be applied blindly. It is not always required, and the additional quantifiers can complicate