author | nipkow |

Wed Sep 21 07:04:04 2011 +0200 (2011-09-21) | |

changeset 45022 | 3c888c58e10b |

parent 45021 | d16343c47fb8 |

child 45023 | 76abd26e2e2d |

Added proofs about narowing

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