--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Tue Feb 23 16:20:12 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,207 +0,0 @@
-(* Author: Tobias Nipkow *)
-
-theory Abs_Int_den2
-imports Abs_Int_den1_ivl
-begin
-
-context preord
-begin
-
-definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
-
-lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
-
-lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
-by(simp add: mono_def)
-
-declare le_trans[trans]
-
-end
-
-
-subsection "Widening and Narrowing"
-
-text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
-rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
-a trivial widening step. We generalise this idea and complement it with
-narrowing, a process to regain precision.
-
-Class @{text WN} makes some assumptions about the widening and narrowing
-operators. The assumptions 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 iteration 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)
-assumes widen: "y \<sqsubseteq> x \<nabla> y"
-fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
-assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
-assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
-begin
-
-fun iter_up :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_up f 0 x = Top" |
-"iter_up f (Suc n) x =
- (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
-
-lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
-apply (induction n arbitrary: x)
- apply (simp)
-apply (simp add: Let_def)
-done
-
-fun iter_down :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_down f 0 x = x" |
-"iter_down f (Suc n) x =
- (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
-
-lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
-apply (induction n arbitrary: x)
- apply (simp)
-apply (simp add: Let_def)
-done
-
-definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter' m n f x =
- (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
-
-lemma iter'_pfp_above:
-shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
-and "x0 \<sqsubseteq> iter' m n f x0"
-using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
-by(auto simp add: iter'_def Let_def)
-
-text{* This is how narrowing works on monotone functions: you just iterate. *}
-
-abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
-"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
-
-text{* Narrowing always yields a post-fixed point: *}
-
-lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
-defines "x n == iter_down_mono f n x0"
-shows "f(x n) \<sqsubseteq> x n"
-proof (induction n)
- case 0 show ?case by (simp add: x_def assms(2))
-next
- case (Suc n)
- have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
- also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
- also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
- also have "\<dots> = x(Suc n)" by(simp add: x_def)
- finally show ?case .
-qed
-
-text{* Narrowing can only increase precision: *}
-
-lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
-defines "x n == iter_down_mono f n x0"
-shows "x n \<sqsubseteq> x0"
-proof (induction n)
- case 0 show ?case by(simp add: x_def)
-next
- case (Suc n)
- have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
- also have "\<dots> \<sqsubseteq> x n" unfolding x_def
- by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
- also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
- finally show ?case .
-qed
-
-
-end
-
-
-instantiation ivl :: WN
-begin
-
-definition "widen_ivl ivl1 ivl2 =
- ((*if is_empty ivl1 then ivl2 else if is_empty ivl2 then ivl1 else*)
- case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
- I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
- (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
-
-definition "narrow_ivl ivl1 ivl2 =
- ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
- case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
- I (if l1 = None then l2 else l1)
- (if h1 = None then h2 else h1))"
-
-instance
-proof qed
- (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
-
-end
-
-instantiation astate :: (WN) WN
-begin
-
-definition "widen_astate F1 F2 =
- FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
-
-definition "narrow_astate F1 F2 =
- FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
-
-instance
-proof
- case goal1 thus ?case
- by(simp add: widen_astate_def le_astate_def lookup_def widen)
-next
- case goal2 thus ?case
- by(auto simp: narrow_astate_def le_astate_def lookup_def narrow1)
-next
- case goal3 thus ?case
- by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
-qed
-
-end
-
-instantiation up :: (WN) WN
-begin
-
-fun widen_up where
-"widen_up bot x = x" |
-"widen_up x bot = x" |
-"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
-
-fun narrow_up where
-"narrow_up bot x = bot" |
-"narrow_up x bot = bot" |
-"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
-
-instance
-proof
- case goal1 show ?case
- by(induct x y rule: widen_up.induct) (simp_all add: widen)
-next
- case goal2 thus ?case
- by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
-next
- case goal3 thus ?case
- by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
-qed
-
-end
-
-global_interpretation
- Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
-defines afilter_ivl' = afilter
-and bfilter_ivl' = bfilter
-and AI_ivl' = AI
-and aval_ivl' = aval'
-proof qed (auto simp: iter'_pfp_above)
-
-value "list_up(AI_ivl' test3_ivl Top)"
-value "list_up(AI_ivl' test4_ivl Top)"
-value "list_up(AI_ivl' test5_ivl Top)"
-
-end