Added proofs about narowing
authornipkow
Wed Sep 21 07:04:04 2011 +0200 (2011-09-21)
changeset 450223c888c58e10b
parent 45021 d16343c47fb8
child 45023 76abd26e2e2d
Added proofs about narowing
src/HOL/IMP/AbsInt2.thy
     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