44932
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
theory AbsInt2
|
|
4 |
imports AbsInt1_ivl
|
|
5 |
begin
|
|
6 |
|
|
7 |
subsection "Widening and Narrowing"
|
|
8 |
|
|
9 |
text{* The assumptions about winden and narrow are merely sanity checks. They
|
|
10 |
are only needed in case we want to prove termination of the fixedpoint
|
|
11 |
iteration, which we do not --- we limit the number of iterations as before. *}
|
|
12 |
|
|
13 |
class WN = SL_top +
|
|
14 |
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
|
|
15 |
assumes widen: "y \<sqsubseteq> x \<nabla> y"
|
|
16 |
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
|
|
17 |
assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
|
|
18 |
assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
|
|
19 |
begin
|
|
20 |
|
|
21 |
fun iter_up :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
|
|
22 |
"iter_up f 0 x = Top" |
|
|
23 |
"iter_up f (Suc n) x =
|
|
24 |
(let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
|
|
25 |
|
|
26 |
lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
|
|
27 |
apply (induct n arbitrary: x)
|
|
28 |
apply (simp)
|
|
29 |
apply (simp add: Let_def)
|
|
30 |
done
|
|
31 |
|
|
32 |
fun iter_down :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
|
|
33 |
"iter_down f 0 x = x" |
|
|
34 |
"iter_down f (Suc n) x =
|
|
35 |
(let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
|
|
36 |
|
|
37 |
lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
|
|
38 |
apply (induct n arbitrary: x)
|
|
39 |
apply (simp)
|
|
40 |
apply (simp add: Let_def)
|
|
41 |
done
|
|
42 |
|
|
43 |
definition iter_above :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
|
|
44 |
"iter_above m n f x =
|
|
45 |
(let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
|
|
46 |
|
|
47 |
lemma iter_above_pfp:
|
|
48 |
shows "f(iter_above m n f x0) \<sqsubseteq> iter_above m n f x0"
|
|
49 |
and "x0 \<sqsubseteq> iter_above m n f x0"
|
|
50 |
using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
|
|
51 |
by(auto simp add: iter_above_def Let_def)
|
|
52 |
|
|
53 |
end
|
|
54 |
|
|
55 |
|
|
56 |
instantiation ivl :: WN
|
|
57 |
begin
|
|
58 |
|
|
59 |
definition "widen_ivl ivl1 ivl2 =
|
|
60 |
((*if is_empty ivl1 then ivl2 else
|
|
61 |
if is_empty ivl2 then ivl1 else*)
|
|
62 |
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
|
|
63 |
I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
|
|
64 |
(if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
|
|
65 |
|
|
66 |
definition "narrow_ivl ivl1 ivl2 =
|
|
67 |
((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
|
|
68 |
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
|
|
69 |
I (if l1 = None then l2 else l1)
|
|
70 |
(if h1 = None then h2 else h1))"
|
|
71 |
|
|
72 |
instance
|
|
73 |
proof qed
|
|
74 |
(auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
|
|
75 |
|
|
76 |
end
|
|
77 |
|
|
78 |
instantiation astate :: (WN)WN
|
|
79 |
begin
|
|
80 |
|
|
81 |
definition "widen_astate F1 F2 =
|
|
82 |
FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
|
|
83 |
|
|
84 |
definition "narrow_astate F1 F2 =
|
|
85 |
FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
|
|
86 |
|
|
87 |
instance
|
|
88 |
proof
|
|
89 |
case goal1 thus ?case
|
|
90 |
by(simp add: widen_astate_def le_astate_def lookup_def widen)
|
|
91 |
next
|
|
92 |
case goal2 thus ?case
|
|
93 |
by(auto simp: narrow_astate_def le_astate_def lookup_def narrow1)
|
|
94 |
next
|
|
95 |
case goal3 thus ?case
|
|
96 |
by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
|
|
97 |
qed
|
|
98 |
|
|
99 |
end
|
|
100 |
|
|
101 |
instantiation up :: (WN)WN
|
|
102 |
begin
|
|
103 |
|
|
104 |
fun widen_up where
|
|
105 |
"widen_up bot x = x" |
|
|
106 |
"widen_up x bot = x" |
|
|
107 |
"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
|
|
108 |
|
|
109 |
fun narrow_up where
|
|
110 |
"narrow_up bot x = bot" |
|
|
111 |
"narrow_up x bot = bot" |
|
|
112 |
"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
|
|
113 |
|
|
114 |
instance
|
|
115 |
proof
|
|
116 |
case goal1 show ?case
|
|
117 |
by(induct x y rule: widen_up.induct) (simp_all add: widen)
|
|
118 |
next
|
|
119 |
case goal2 thus ?case
|
|
120 |
by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
|
|
121 |
next
|
|
122 |
case goal3 thus ?case
|
|
123 |
by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
|
|
124 |
qed
|
|
125 |
|
|
126 |
end
|
|
127 |
|
|
128 |
interpretation
|
|
129 |
Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter_above 3 2)"
|
|
130 |
defines afilter_ivl' is afilter
|
|
131 |
and bfilter_ivl' is bfilter
|
|
132 |
and AI_ivl' is AI
|
|
133 |
and aval_ivl' is aval'
|
|
134 |
proof qed (auto simp: iter_above_pfp)
|
|
135 |
|
|
136 |
value [code] "list_up(AI_ivl' test3_ivl Top)"
|
|
137 |
value [code] "list_up(AI_ivl' test4_ivl Top)"
|
|
138 |
|
|
139 |
end
|