# HG changeset patch
# User nipkow
# Date 1316565533 -7200
# Node ID 020e460b6644959a8eacfcf6ea30d8ad7a4ea9b6
# Parent  07a0638c351ad28482d82263011a9c22a7f21eaf
refined comment

diff -r 07a0638c351a -r 020e460b6644 src/HOL/IMP/AbsInt2.thy
--- a/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 09:17:01 2011 +1000
+++ b/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 02:38:53 2011 +0200
@@ -6,9 +6,18 @@
 
 subsection "Widening and Narrowing"
 
-text{* The assumptions about widen and narrow are merely sanity checks. They
-are only needed in case we want to prove termination of the fixedpoint
-iteration, which we do not --- we limit the number of iterations as before. *}
+text{* The assumptions about widen and narrow are merely sanity checks for
+us. Normaly, they serve two purposes. Together with a further assumption that
+certain chains become stationary, they permit to prove termination of the
+fixed point iteration, which we do not --- we limit the number of iterations
+as before. The second purpose of the narrowing assumptions is to prove that
+the narrowing iteration keeps on producing post-fixed points and that it goes
+down. However, this requires the function being iterated to be
+monotone. Unfortunately, abstract interpretation with widening is not
+monotone. Hence the (recursive) abstract interpretation of a loop body that
+again contains a loop may result in a non-monotone function. Therefore our
+narrowing interation needs to check at every step that a post-fixed point is
+maintained, and we cannot prove that the precision increases. *}
 
 class WN = SL_top +
 fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)