author nipkow Wed Sep 21 07:04:04 2011 +0200 (2011-09-21) changeset 45022 3c888c58e10b parent 45021 d16343c47fb8 child 45023 76abd26e2e2d
 src/HOL/IMP/AbsInt2.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 07:03:16 2011 +0200
1.2 +++ b/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 07:04:04 2011 +0200
1.3 @@ -4,20 +4,41 @@
1.4  imports AbsInt1_ivl
1.5  begin
1.6
1.7 +context preord
1.8 +begin
1.9 +
1.10 +definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
1.11 +
1.12 +lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
1.13 +
1.14 +lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
1.15 +by(simp add: mono_def)
1.16 +
1.17 +declare le_trans[trans]
1.18 +
1.19 +end
1.20 +
1.21 +
1.22  subsection "Widening and Narrowing"
1.23
1.24 -text{* The assumptions about widen and narrow are merely sanity checks for
1.25 -us. Normaly, they serve two purposes. Together with a further assumption that
1.26 -certain chains become stationary, they permit to prove termination of the
1.27 -fixed point iteration, which we do not --- we limit the number of iterations
1.28 -as before. The second purpose of the narrowing assumptions is to prove that
1.29 -the narrowing iteration keeps on producing post-fixed points and that it goes
1.30 -down. However, this requires the function being iterated to be
1.31 -monotone. Unfortunately, abstract interpretation with widening is not
1.32 -monotone. Hence the (recursive) abstract interpretation of a loop body that
1.33 -again contains a loop may result in a non-monotone function. Therefore our
1.34 -narrowing interation needs to check at every step that a post-fixed point is
1.35 -maintained, and we cannot prove that the precision increases. *}
1.36 +text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
1.37 +rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
1.38 +a trivial widening step. We generalise this idea and complement it with
1.39 +narrowing, a process to regain precision.
1.40 +
1.41 +Class @{text WN} makes some assumptions about the widening and narrowing
1.42 +operators. The assumptions serve two purposes. Together with a further
1.43 +assumption that certain chains become stationary, they permit to prove
1.44 +termination of the fixed point iteration, which we do not --- we limit the
1.45 +number of iterations as before. The second purpose of the narrowing
1.46 +assumptions is to prove that the narrowing iteration keeps on producing
1.47 +post-fixed points and that it goes down. However, this requires the function
1.48 +being iterated to be monotone. Unfortunately, abstract interpretation with
1.49 +widening is not monotone. Hence the (recursive) abstract interpretation of a
1.50 +loop body that again contains a loop may result in a non-monotone
1.51 +function. Therefore our narrowing interation needs to check at every step
1.52 +that a post-fixed point is maintained, and we cannot prove that the precision
1.53 +increases. *}
1.54
1.55  class WN = SL_top +
1.56  fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
1.57 @@ -59,6 +80,44 @@
1.58  using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
1.59  by(auto simp add: iter'_def Let_def)
1.60
1.61 +text{* This is how narrowing works on monotone functions: you just iterate. *}
1.62 +
1.63 +abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
1.64 +"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
1.65 +
1.66 +text{* Narrowing always yields a post-fixed point: *}
1.67 +
1.68 +lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
1.69 +defines "x n == iter_down_mono f n x0"
1.70 +shows "f(x n) \<sqsubseteq> x n"
1.71 +proof (induction n)
1.72 +  case 0 show ?case by (simp add: x_def assms(2))
1.73 +next
1.74 +  case (Suc n)
1.75 +  have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
1.76 +  also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
1.77 +  also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
1.78 +  also have "\<dots> = x(Suc n)" by(simp add: x_def)
1.79 +  finally show ?case .
1.80 +qed
1.81 +
1.82 +text{* Narrowing can only increase precision: *}
1.83 +
1.84 +lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
1.85 +defines "x n == iter_down_mono f n x0"
1.86 +shows "x n \<sqsubseteq> x0"
1.87 +proof (induction n)
1.88 +  case 0 show ?case by(simp add: x_def)
1.89 +next
1.90 +  case (Suc n)
1.91 +  have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
1.92 +  also have "\<dots> \<sqsubseteq> x n" unfolding x_def
1.93 +    by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
1.94 +  also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
1.95 +  finally show ?case .
1.96 +qed
1.97 +
1.98 +
1.99  end
1.100
1.101
```