author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46430  ead59736792b 
permissions  rwrr 
45111  1 
(* Author: Tobias Nipkow *) 
2 

3 
theory Abs_Int2 

4 
imports Abs_Int1_ivl 

5 
begin 

6 

7 
subsection "Widening and Narrowing" 

8 

9 
class WN = SL_top + 

10 
fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65) 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

11 
assumes widen1: "x \<sqsubseteq> x \<nabla> y" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

12 
assumes widen2: "y \<sqsubseteq> x \<nabla> y" 
45111  13 
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65) 
14 
assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y" 

15 
assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x" 

16 

17 

46249  18 
subsubsection "Intervals" 
19 

45111  20 
instantiation ivl :: WN 
21 
begin 

22 

23 
definition "widen_ivl ivl1 ivl2 = 

24 
((*if is_empty ivl1 then ivl2 else 

25 
if is_empty ivl2 then ivl1 else*) 

26 
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow> 

27 
I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1) 

28 
(if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))" 

29 

30 
definition "narrow_ivl ivl1 ivl2 = 

31 
((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*) 

32 
case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow> 

33 
I (if l1 = None then l2 else l1) 

34 
(if h1 = None then h2 else h1))" 

35 

36 
instance 

37 
proof qed 

38 
(auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits) 

39 

40 
end 

41 

46249  42 

43 
subsubsection "Abstract State" 

44 

45111  45 
instantiation st :: (WN)WN 
46 
begin 

47 

48 
definition "widen_st F1 F2 = 

49 
FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))" 

50 

51 
definition "narrow_st F1 F2 = 

52 
FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))" 

53 

54 
instance 

55 
proof 

56 
case goal1 thus ?case 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

57 
by(simp add: widen_st_def le_st_def lookup_def widen1) 
45111  58 
next 
59 
case goal2 thus ?case 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

60 
by(simp add: widen_st_def le_st_def lookup_def widen2) 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

61 
next 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

62 
case goal3 thus ?case 
45111  63 
by(auto simp: narrow_st_def le_st_def lookup_def narrow1) 
64 
next 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

65 
case goal4 thus ?case 
45111  66 
by(auto simp: narrow_st_def le_st_def lookup_def narrow2) 
67 
qed 

68 

69 
end 

70 

46249  71 

72 
subsubsection "Option" 

73 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

74 
instantiation option :: (WN)WN 
45111  75 
begin 
76 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

77 
fun widen_option where 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

78 
"None \<nabla> x = x"  
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

79 
"x \<nabla> None = x"  
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

80 
"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)" 
45111  81 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

82 
fun narrow_option where 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

83 
"None \<triangle> x = None"  
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

84 
"x \<triangle> None = None"  
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

85 
"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)" 
45111  86 

87 
instance 

88 
proof 

89 
case goal1 show ?case 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

90 
by(induct x y rule: widen_option.induct) (simp_all add: widen1) 
45111  91 
next 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

92 
case goal2 show ?case 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

93 
by(induct x y rule: widen_option.induct) (simp_all add: widen2) 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

94 
next 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

95 
case goal3 thus ?case 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

96 
by(induct x y rule: narrow_option.induct) (simp_all add: narrow1) 
45111  97 
next 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

98 
case goal4 thus ?case 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

99 
by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) 
45111  100 
qed 
101 

102 
end 

103 

46249  104 

105 
subsubsection "Annotated commands" 

106 

45111  107 
fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where 
108 
"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})"  

109 
"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})"  

110 
"map2_acom f (c1;c2) (c1';c2') = (map2_acom f c1 c1'; map2_acom f c2 c2')"  

111 
"map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) = 

112 
(IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})"  

113 
"map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) = 

114 
({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})" 

115 

116 
abbreviation widen_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<nabla>\<^sub>c" 65) 

117 
where "widen_acom == map2_acom (op \<nabla>)" 

118 

119 
abbreviation narrow_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<triangle>\<^sub>c" 65) 

120 
where "narrow_acom == map2_acom (op \<triangle>)" 

121 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

122 
lemma widen1_acom: "strip c = strip c' \<Longrightarrow> c \<sqsubseteq> c \<nabla>\<^sub>c c'" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

123 
by(induct c c' rule: le_acom.induct)(simp_all add: widen1) 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

124 

d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

125 
lemma widen2_acom: "strip c = strip c' \<Longrightarrow> c' \<sqsubseteq> c \<nabla>\<^sub>c c'" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

126 
by(induct c c' rule: le_acom.induct)(simp_all add: widen2) 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

127 

45111  128 
lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y" 
129 
by(induct y x rule: le_acom.induct) (simp_all add: narrow1) 

130 

131 
lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x" 

132 
by(induct y x rule: le_acom.induct) (simp_all add: narrow2) 

133 

134 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

135 
subsubsection "Postfixed point computation" 
45111  136 

46249  137 
definition iter_widen :: "('a acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> ('a::WN)acom option" 
138 
where "iter_widen f = while_option (\<lambda>c. \<not> f c \<sqsubseteq> c) (\<lambda>c. c \<nabla>\<^sub>c f c)" 

139 

46251  140 
definition iter_narrow :: "('a acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a::WN acom option" 
141 
where "iter_narrow f = while_option (\<lambda>c. \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) (\<lambda>c. c \<triangle>\<^sub>c f c)" 

46249  142 

46251  143 
definition pfp_wn :: 
144 
"(('a::WN)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option" 

145 
where "pfp_wn f c = (case iter_widen f (\<bottom>\<^sub>c c) of None \<Rightarrow> None 

146 
 Some c' \<Rightarrow> iter_narrow f c')" 

45111  147 

148 
lemma strip_map2_acom: 

149 
"strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1" 

150 
by(induct f c1 c2 rule: map2_acom.induct) simp_all 

151 

46249  152 
lemma iter_widen_pfp: "iter_widen f c = Some c' \<Longrightarrow> f c' \<sqsubseteq> c'" 
153 
by(auto simp add: iter_widen_def dest: while_option_stop) 

154 

155 
lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom" 

156 
assumes "\<forall>c. strip (f c) = strip c" and "while_option P f c = Some c'" 

157 
shows "strip c' = strip c" 

158 
using while_option_rule[where P = "\<lambda>c'. strip c' = strip c", OF _ assms(2)] 

159 
by (metis assms(1)) 

160 

161 
lemma strip_iter_widen: fixes f :: "'a::WN acom \<Rightarrow> 'a acom" 

162 
assumes "\<forall>c. strip (f c) = strip c" and "iter_widen f c = Some c'" 

163 
shows "strip c' = strip c" 

164 
proof 

165 
have "\<forall>c. strip(c \<nabla>\<^sub>c f c) = strip c" by (metis assms(1) strip_map2_acom) 

166 
from strip_while[OF this] assms(2) show ?thesis by(simp add: iter_widen_def) 

167 
qed 

45111  168 

46251  169 
lemma iter_narrow_pfp: assumes "mono f" and "f c0 \<sqsubseteq> c0" 
170 
and "iter_narrow f c0 = Some c" 

171 
shows "f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0" (is "?P c") 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

172 
proof 
46251  173 
{ fix c assume "?P c" 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

174 
note 1 = conjunct1[OF this] and 2 = conjunct2[OF this] 
46251  175 
let ?c' = "c \<triangle>\<^sub>c f c" 
176 
have "?P ?c'" 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

177 
proof 
46251  178 
have "f ?c' \<sqsubseteq> f c" by(rule monoD[OF `mono f` narrow2_acom[OF 1]]) 
179 
also have "\<dots> \<sqsubseteq> ?c'" by(rule narrow1_acom[OF 1]) 

180 
finally show "f ?c' \<sqsubseteq> ?c'" . 

181 
have "?c' \<sqsubseteq> c" by (rule narrow2_acom[OF 1]) 

182 
also have "c \<sqsubseteq> c0" by(rule 2) 

183 
finally show "?c' \<sqsubseteq> c0" . 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

184 
qed 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

185 
} 
46251  186 
with while_option_rule[where P = ?P, OF _ assms(3)[simplified iter_narrow_def]] 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

187 
assms(2) le_refl 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

188 
show ?thesis by blast 
45111  189 
qed 
190 

46251  191 
lemma pfp_wn_pfp: 
192 
"\<lbrakk> mono f; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'" 

193 
unfolding pfp_wn_def 

194 
by (auto dest: iter_widen_pfp iter_narrow_pfp split: option.splits) 

45111  195 

46251  196 
lemma strip_pfp_wn: 
197 
"\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c" 

198 
apply(auto simp add: pfp_wn_def iter_narrow_def split: option.splits) 

46249  199 
by (metis (no_types) strip_map2_acom strip_while strip_bot_acom strip_iter_widen) 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

200 

46063  201 
locale Abs_Int2 = Abs_Int1_mono 
202 
where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set" 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

203 
begin 
45111  204 

46251  205 
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where 
206 
"AI_wn = pfp_wn (step' \<top>)" 

45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

207 

46251  208 
lemma AI_wn_sound: "AI_wn c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'" 
209 
proof(simp add: CS_def AI_wn_def) 

210 
assume 1: "pfp_wn (step' \<top>) c = Some c'" 

211 
from pfp_wn_pfp[OF mono_step'2 1] 

45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

212 
have 2: "step' \<top> c' \<sqsubseteq> c'" . 
46251  213 
have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" by(simp add: strip_pfp_wn[OF _ 1]) 
46066  214 
have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')" 
45903  215 
proof(rule lfp_lowerbound[simplified,OF 3]) 
45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

216 
show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')" 
46068  217 
proof(rule step_preserves_le[OF _ _]) 
46039  218 
show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp 
219 
show "\<gamma>\<^isub>c (step' \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_gamma_c[OF 2]) 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

220 
qed 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

221 
qed 
46066  222 
from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c c'" 
46039  223 
by (blast intro: mono_gamma_c order_trans) 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

224 
qed 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

225 

d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

226 
end 
45111  227 

46063  228 
interpretation Abs_Int2 
229 
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl 

46430  230 
and test_num' = in_ivl 
46063  231 
and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl 
46251  232 
defines AI_ivl' is AI_wn 
46355
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46303
diff
changeset

233 
.. 
45111  234 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

235 

f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

236 
subsubsection "Tests" 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

237 

d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

238 
definition "step_up_ivl n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

239 
definition "step_down_ivl n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)" 
45111  240 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

241 
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as 
46303  242 
the loop took to execute. In contrast, @{const AI_ivl'} converges in a 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

243 
constant number of steps: *} 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

244 

46303  245 
value "show_acom (step_up_ivl 1 (\<bottom>\<^sub>c test3_ivl))" 
246 
value "show_acom (step_up_ivl 2 (\<bottom>\<^sub>c test3_ivl))" 

247 
value "show_acom (step_up_ivl 3 (\<bottom>\<^sub>c test3_ivl))" 

248 
value "show_acom (step_up_ivl 4 (\<bottom>\<^sub>c test3_ivl))" 

249 
value "show_acom (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl))" 

250 
value "show_acom (step_down_ivl 1 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" 

251 
value "show_acom (step_down_ivl 2 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" 

252 
value "show_acom (step_down_ivl 3 (step_up_ivl 5 (\<bottom>\<^sub>c test3_ivl)))" 

45111  253 

45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

254 
text{* Now all the analyses terminate: *} 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset

255 

46303  256 
value "show_acom_opt (AI_ivl' test4_ivl)" 
257 
value "show_acom_opt (AI_ivl' test5_ivl)" 

258 
value "show_acom_opt (AI_ivl' test6_ivl)" 

45111  259 

46249  260 

261 
subsubsection "Termination: Intervals" 

262 

263 
definition m_ivl :: "ivl \<Rightarrow> nat" where 

264 
"m_ivl ivl = (case ivl of I l h \<Rightarrow> 

265 
(case l of None \<Rightarrow> 0  Some _ \<Rightarrow> 1) + (case h of None \<Rightarrow> 0  Some _ \<Rightarrow> 1))" 

266 

267 
lemma m_ivl_height: "m_ivl ivl \<le> 2" 

268 
by(simp add: m_ivl_def split: ivl.split option.split) 

269 

270 
lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y" 

271 
by(auto simp: m_ivl_def le_option_def le_ivl_def 

272 
split: ivl.split option.split if_splits) 

273 

46251  274 
lemma m_ivl_widen: 
46249  275 
"~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x" 
276 
by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def 

277 
split: ivl.splits option.splits if_splits) 

278 

279 
lemma Top_less_ivl: "\<top> \<sqsubseteq> x \<Longrightarrow> m_ivl x = 0" 

280 
by(auto simp: m_ivl_def le_option_def le_ivl_def empty_def Top_ivl_def 

281 
split: ivl.split option.split if_splits) 

282 

283 

46251  284 
definition n_ivl :: "ivl \<Rightarrow> nat" where 
285 
"n_ivl ivl = 2  m_ivl ivl" 

286 

287 
lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y" 

288 
unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono) 

289 

290 
lemma n_ivl_narrow: 

291 
"~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x" 

292 
by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def 

293 
split: ivl.splits option.splits if_splits) 

294 

295 

46249  296 
subsubsection "Termination: Abstract State" 
297 

298 
definition "m_st m st = (\<Sum>x\<in>set(dom st). m(fun st x))" 

299 

300 
lemma m_st_height: assumes "finite X" and "set (dom S) \<subseteq> X" 

301 
shows "m_st m_ivl S \<le> 2 * card X" 

302 
proof(auto simp: m_st_def) 

303 
have "(\<Sum>x\<in>set(dom S). m_ivl (fun S x)) \<le> (\<Sum>x\<in>set(dom S). 2)" (is "?L \<le> _") 

304 
by(rule setsum_mono)(simp add:m_ivl_height) 

305 
also have "\<dots> \<le> (\<Sum>x\<in>X. 2)" 

306 
by(rule setsum_mono3[OF assms]) simp 

307 
also have "\<dots> = 2 * card X" by(simp add: setsum_constant) 

308 
finally show "?L \<le> \<dots>" . 

309 
qed 

310 

311 
lemma m_st_anti_mono: 

312 
"S1 \<sqsubseteq> S2 \<Longrightarrow> m_st m_ivl S2 \<le> m_st m_ivl S1" 

313 
proof(auto simp: m_st_def le_st_def lookup_def split: if_splits) 

314 
let ?X = "set(dom S1)" let ?Y = "set(dom S2)" 

315 
let ?f = "fun S1" let ?g = "fun S2" 

316 
assume asm: "\<forall>x\<in>?Y. (x \<in> ?X \<longrightarrow> ?f x \<sqsubseteq> ?g x) \<and> (x \<in> ?X \<or> \<top> \<sqsubseteq> ?g x)" 

317 
hence 1: "\<forall>y\<in>?Y\<inter>?X. m_ivl(?g y) \<le> m_ivl(?f y)" by(simp add: m_ivl_anti_mono) 

318 
have 0: "\<forall>x\<in>?Y?X. m_ivl(?g x) = 0" using asm by (auto simp: Top_less_ivl) 

319 
have "(\<Sum>y\<in>?Y. m_ivl(?g y)) = (\<Sum>y\<in>(?Y?X) \<union> (?Y\<inter>?X). m_ivl(?g y))" 

320 
by (metis Un_Diff_Int) 

321 
also have "\<dots> = (\<Sum>y\<in>?Y?X. m_ivl(?g y)) + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))" 

322 
by(subst setsum_Un_disjoint) auto 

323 
also have "(\<Sum>y\<in>?Y?X. m_ivl(?g y)) = 0" using 0 by simp 

324 
also have "0 + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y)) = (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))" by simp 

325 
also have "\<dots> \<le> (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?f y))" 

326 
by(rule setsum_mono)(simp add: 1) 

327 
also have "\<dots> \<le> (\<Sum>y\<in>?X. m_ivl(?f y))" 

328 
by(simp add: setsum_mono3[of "?X" "?Y Int ?X", OF _ Int_lower2]) 

329 
finally show "(\<Sum>y\<in>?Y. m_ivl(?g y)) \<le> (\<Sum>x\<in>?X. m_ivl(?f x))" 

330 
by (metis add_less_cancel_left) 

331 
qed 

332 

46251  333 
lemma m_st_widen: 
46249  334 
assumes "\<not> S2 \<sqsubseteq> S1" shows "m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1" 
335 
proof 

336 
{ let ?X = "set(dom S1)" let ?Y = "set(dom S2)" 

337 
let ?f = "fun S1" let ?g = "fun S2" 

338 
fix x assume "x \<in> ?X" "\<not> lookup S2 x \<sqsubseteq> ?f x" 

339 
have "(\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x)) < (\<Sum>x\<in>?X. m_ivl(?f x))" (is "?L < ?R") 

340 
proof cases 

341 
assume "x : ?Y" 

342 
have "?L < (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))" 

343 
proof(rule setsum_strict_mono1, simp) 

344 
show "\<forall>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)" 

345 
by (metis m_ivl_anti_mono widen1) 

346 
next 

347 
show "\<exists>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) < m_ivl(?f x)" 

348 
using `x:?X` `x:?Y` `\<not> lookup S2 x \<sqsubseteq> ?f x` 

46251  349 
by (metis IntI m_ivl_widen lookup_def) 
46249  350 
qed 
351 
also have "\<dots> \<le> ?R" by(simp add: setsum_mono3[OF _ Int_lower1]) 

352 
finally show ?thesis . 

353 
next 

354 
assume "x ~: ?Y" 

355 
have "?L \<le> (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))" 

356 
proof(rule setsum_mono, simp) 

357 
fix x assume "x:?X \<and> x:?Y" show "m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)" 

358 
by (metis m_ivl_anti_mono widen1) 

359 
qed 

360 
also have "\<dots> < m_ivl(?f x) + \<dots>" 

46251  361 
using m_ivl_widen[OF `\<not> lookup S2 x \<sqsubseteq> ?f x`] 
46249  362 
by (metis Nat.le_refl add_strict_increasing gr0I not_less0) 
363 
also have "\<dots> = (\<Sum>y\<in>insert x (?X\<inter>?Y). m_ivl(?f y))" 

364 
using `x ~: ?Y` by simp 

365 
also have "\<dots> \<le> (\<Sum>x\<in>?X. m_ivl(?f x))" 

366 
by(rule setsum_mono3)(insert `x:?X`, auto) 

367 
finally show ?thesis . 

368 
qed 

369 
} with assms show ?thesis 

370 
by(auto simp: le_st_def widen_st_def m_st_def Int_def) 

371 
qed 

372 

46251  373 
definition "n_st m X st = (\<Sum>x\<in>X. m(lookup st x))" 
374 

375 
lemma n_st_mono: assumes "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X" "S1 \<sqsubseteq> S2" 

376 
shows "n_st n_ivl X S1 \<le> n_st n_ivl X S2" 

377 
proof 

378 
have "(\<Sum>x\<in>X. n_ivl(lookup S1 x)) \<le> (\<Sum>x\<in>X. n_ivl(lookup S2 x))" 

379 
apply(rule setsum_mono) using assms 

380 
by(auto simp: le_st_def lookup_def n_ivl_mono split: if_splits) 

381 
thus ?thesis by(simp add: n_st_def) 

382 
qed 

383 

384 
lemma n_st_narrow: 

385 
assumes "finite X" and "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X" 

386 
and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2" 

387 
shows "n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1" 

388 
proof 

389 
have 1: "\<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)" 

390 
using assms(24) 

391 
by(auto simp: le_st_def narrow_st_def lookup_def n_ivl_mono narrow2 

392 
split: if_splits) 

393 
have 2: "\<exists>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) < n_ivl (lookup S1 x)" 

394 
using assms(25) 

395 
by(auto simp: le_st_def narrow_st_def lookup_def intro: n_ivl_narrow 

396 
split: if_splits) 

397 
have "(\<Sum>x\<in>X. n_ivl(lookup (S1 \<triangle> S2) x)) < (\<Sum>x\<in>X. n_ivl(lookup S1 x))" 

398 
apply(rule setsum_strict_mono1[OF `finite X`]) using 1 2 by blast+ 

399 
thus ?thesis by(simp add: n_st_def) 

400 
qed 

401 

46249  402 

403 
subsubsection "Termination: Option" 

404 

405 
definition "m_o m n opt = (case opt of None \<Rightarrow> n+1  Some x \<Rightarrow> m x)" 

406 

407 
lemma m_o_anti_mono: "finite X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> 

408 
m_o (m_st m_ivl) (2 * card X) S2 \<le> m_o (m_st m_ivl) (2 * card X) S1" 

409 
apply(induction S1 S2 rule: le_option.induct) 

410 
apply(auto simp: domo_def m_o_def m_st_anti_mono le_SucI m_st_height 

411 
split: option.splits) 

412 
done 

413 

46251  414 
lemma m_o_widen: "\<lbrakk> finite X; domo S2 \<subseteq> X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow> 
46249  415 
m_o (m_st m_ivl) (2 * card X) (S1 \<nabla> S2) < m_o (m_st m_ivl) (2 * card X) S1" 
46251  416 
by(auto simp: m_o_def domo_def m_st_height less_Suc_eq_le m_st_widen 
46249  417 
split: option.split) 
418 

46251  419 
definition "n_o n opt = (case opt of None \<Rightarrow> 0  Some x \<Rightarrow> n x + 1)" 
420 

421 
lemma n_o_mono: "domo S1 \<subseteq> X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> 

422 
n_o (n_st n_ivl X) S1 \<le> n_o (n_st n_ivl X) S2" 

423 
apply(induction S1 S2 rule: le_option.induct) 

424 
apply(auto simp: domo_def n_o_def n_st_mono 

425 
split: option.splits) 

426 
done 

427 

428 
lemma n_o_narrow: 

429 
"\<lbrakk> finite X; domo S1 \<subseteq> X; domo S2 \<subseteq> X; S2 \<sqsubseteq> S1; \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<rbrakk> 

430 
\<Longrightarrow> n_o (n_st n_ivl X) (S1 \<triangle> S2) < n_o (n_st n_ivl X) S1" 

431 
apply(induction S1 S2 rule: narrow_option.induct) 

432 
apply(auto simp: n_o_def domo_def n_st_narrow) 

433 
done 

46249  434 

435 
lemma domo_widen_subset: "domo (S1 \<nabla> S2) \<subseteq> domo S1 \<union> domo S2" 

436 
apply(induction S1 S2 rule: widen_option.induct) 

437 
apply (auto simp: domo_def widen_st_def) 

438 
done 

439 

46251  440 
lemma domo_narrow_subset: "domo (S1 \<triangle> S2) \<subseteq> domo S1 \<union> domo S2" 
441 
apply(induction S1 S2 rule: narrow_option.induct) 

442 
apply (auto simp: domo_def narrow_st_def) 

443 
done 

444 

46249  445 
subsubsection "Termination: Commands" 
446 

46251  447 
lemma strip_widen_acom[simp]: 
46249  448 
"strip c' = strip (c::'a::WN acom) \<Longrightarrow> strip (c \<nabla>\<^sub>c c') = strip c" 
449 
by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all 

450 

46251  451 
lemma strip_narrow_acom[simp]: 
452 
"strip c' = strip (c::'a::WN acom) \<Longrightarrow> strip (c \<triangle>\<^sub>c c') = strip c" 

453 
by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all 

454 

46249  455 
lemma annos_widen_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow> 
456 
annos(c1 \<nabla>\<^sub>c c2) = map (%(x,y).x\<nabla>y) (zip (annos c1) (annos(c2::'a::WN acom)))" 

457 
by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct) 

458 
(simp_all add: size_annos_same2) 

459 

46251  460 
lemma annos_narrow_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow> 
461 
annos(c1 \<triangle>\<^sub>c c2) = map (%(x,y).x\<triangle>y) (zip (annos c1) (annos(c2::'a::WN acom)))" 

462 
by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct) 

463 
(simp_all add: size_annos_same2) 

464 

465 
lemma widen_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow> 

46249  466 
c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<nabla>\<^sub>c c2) : Com X" 
46251  467 
apply(auto simp add: Com_def) 
46249  468 
apply(rename_tac S S' x) 
469 
apply(erule in_set_zipE) 

46251  470 
apply(auto simp: domo_def split: option.splits) 
46249  471 
apply(case_tac S) 
472 
apply(case_tac S') 

473 
apply simp 

474 
apply fastforce 

475 
apply(case_tac S') 

476 
apply fastforce 

477 
apply (fastforce simp: widen_st_def) 

478 
done 

479 

46251  480 
lemma narrow_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow> 
481 
c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<triangle>\<^sub>c c2) : Com X" 

482 
apply(auto simp add: Com_def) 

483 
apply(rename_tac S S' x) 

484 
apply(erule in_set_zipE) 

485 
apply(auto simp: domo_def split: option.splits) 

486 
apply(case_tac S) 

487 
apply(case_tac S') 

488 
apply simp 

489 
apply fastforce 

490 
apply(case_tac S') 

491 
apply fastforce 

492 
apply (fastforce simp: narrow_st_def) 

493 
done 

494 

46249  495 
definition "m_c m c = (let as = annos c in \<Sum>i=0..<size as. m(as!i))" 
496 

497 
lemma measure_m_c: "finite X \<Longrightarrow> {(c, c \<nabla>\<^sub>c c') c c'\<Colon>ivl st option acom. 

498 
strip c' = strip c \<and> c : Com X \<and> c' : Com X \<and> \<not> c' \<sqsubseteq> c}\<inverse> 

499 
\<subseteq> measure(m_c(m_o (m_st m_ivl) (2*card(X))))" 

500 
apply(auto simp: m_c_def Let_def Com_def) 

501 
apply(subgoal_tac "length(annos c') = length(annos c)") 

502 
prefer 2 apply (simp add: size_annos_same2) 

503 
apply (auto) 

504 
apply(rule setsum_strict_mono1) 

505 
apply simp 

506 
apply (clarsimp) 

507 
apply(erule m_o_anti_mono) 

508 
apply(rule subset_trans[OF domo_widen_subset]) 

46251  509 
apply fastforce 
46249  510 
apply(rule widen1) 
511 
apply(auto simp: le_iff_le_annos listrel_iff_nth) 

512 
apply(rule_tac x=n in bexI) 

513 
prefer 2 apply simp 

46251  514 
apply(erule m_o_widen) 
515 
apply (simp)+ 

516 
done 

517 

518 
lemma measure_n_c: "finite X \<Longrightarrow> {(c, c \<triangle>\<^sub>c c') c c'. 

519 
strip c = strip c' \<and> c \<in> Com X \<and> c' \<in> Com X \<and> c' \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'}\<inverse> 

520 
\<subseteq> measure(m_c(n_o (n_st n_ivl X)))" 

521 
apply(auto simp: m_c_def Let_def Com_def) 

522 
apply(subgoal_tac "length(annos c') = length(annos c)") 

523 
prefer 2 apply (simp add: size_annos_same2) 

524 
apply (auto) 

525 
apply(rule setsum_strict_mono1) 

526 
apply simp 

527 
apply (clarsimp) 

528 
apply(rule n_o_mono) 

529 
using domo_narrow_subset apply fastforce 

530 
apply fastforce 

531 
apply(rule narrow2) 

532 
apply(fastforce simp: le_iff_le_annos listrel_iff_nth) 

533 
apply(auto simp: le_iff_le_annos listrel_iff_nth strip_narrow_acom) 

534 
apply(rule_tac x=n in bexI) 

535 
prefer 2 apply simp 

536 
apply(erule n_o_narrow) 

46249  537 
apply (simp)+ 
538 
done 

539 

540 

541 
subsubsection "Termination: PostFixed Point Iterations" 

542 

543 
lemma iter_widen_termination: 

544 
fixes c0 :: "'a::WN acom" 

545 
assumes P_f: "\<And>c. P c \<Longrightarrow> P(f c)" 

546 
assumes P_widen: "\<And>c c'. P c \<Longrightarrow> P c' \<Longrightarrow> P(c \<nabla>\<^sub>c c')" 

547 
and "wf({(c::'a acom,c \<nabla>\<^sub>c c')c c'. P c \<and> P c' \<and> ~ c' \<sqsubseteq> c}^1)" 

548 
and "P c0" and "c0 \<sqsubseteq> f c0" shows "EX c. iter_widen f c0 = Some c" 

549 
proof(simp add: iter_widen_def, rule wf_while_option_Some[where P = "P"]) 

550 
show "wf {(cc', c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc' = c \<nabla>\<^sub>c f c}" 

551 
apply(rule wf_subset[OF assms(3)]) by(blast intro: P_f) 

552 
next 

553 
show "P c0" by(rule `P c0`) 

554 
next 

555 
fix c assume "P c" thus "P (c \<nabla>\<^sub>c f c)" by(simp add: P_f P_widen) 

556 
qed 

557 

46251  558 
lemma iter_narrow_termination: 
559 
assumes P_f: "\<And>c. P c \<Longrightarrow> P(c \<triangle>\<^sub>c f c)" 

560 
and wf: "wf({(c, c \<triangle>\<^sub>c f c)c c'. P c \<and> ~ c \<sqsubseteq> c \<triangle>\<^sub>c f c}^1)" 

561 
and "P c0" shows "EX c. iter_narrow f c0 = Some c" 

562 
proof(simp add: iter_narrow_def, rule wf_while_option_Some[where P = "P"]) 

563 
show "wf {(c', c). (P c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) \<and> c' = c \<triangle>\<^sub>c f c}" 

564 
apply(rule wf_subset[OF wf]) by(blast intro: P_f) 

565 
next 

566 
show "P c0" by(rule `P c0`) 

567 
next 

568 
fix c assume "P c" thus "P (c \<triangle>\<^sub>c f c)" by(simp add: P_f) 

569 
qed 

570 

571 
lemma iter_winden_step_ivl_termination: 

572 
"EX c. iter_widen (step_ivl \<top>) (\<bottom>\<^sub>c c0) = Some c" 

46249  573 
apply(rule iter_widen_termination[where 
574 
P = "%c. strip c = c0 \<and> c : Com(vars c0)"]) 

46251  575 
apply (simp_all add: step'_Com bot_acom) 
46249  576 
apply(rule wf_subset) 
577 
apply(rule wf_measure) 

578 
apply(rule subset_trans) 

579 
prefer 2 

580 
apply(rule measure_m_c[where X = "vars c0", OF finite_cvars]) 

581 
apply blast 

582 
done 

583 

46251  584 
lemma iter_narrow_step_ivl_termination: 
585 
"c0 \<in> Com (vars(strip c0)) \<Longrightarrow> step_ivl \<top> c0 \<sqsubseteq> c0 \<Longrightarrow> 

586 
EX c. iter_narrow (step_ivl \<top>) c0 = Some c" 

587 
apply(rule iter_narrow_termination[where 

588 
P = "%c. strip c = strip c0 \<and> c : Com(vars(strip c0)) \<and> step_ivl \<top> c \<sqsubseteq> c"]) 

589 
apply (simp_all add: step'_Com) 

590 
apply(clarify) 

591 
apply(frule narrow2_acom, drule mono_step'[OF le_refl], erule le_trans[OF _ narrow1_acom]) 

592 
apply assumption 

593 
apply(rule wf_subset) 

594 
apply(rule wf_measure) 

595 
apply(rule subset_trans) 

596 
prefer 2 

597 
apply(rule measure_n_c[where X = "vars(strip c0)", OF finite_cvars]) 

598 
apply auto 

599 
by (metis bot_least domo_Top order_refl step'_Com strip_step') 

600 

601 
(* FIXME: simplify type system: Combine Com(X) and vars <= X?? *) 

602 
lemma while_Com: 

603 
fixes c :: "'a st option acom" 

604 
assumes "while_option P f c = Some c'" 

605 
and "!!c. strip(f c) = strip c" 

606 
and "\<forall>c::'a st option acom. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)" 

607 
and "c : Com(X)" and "vars(strip c) \<subseteq> X" shows "c' : Com(X)" 

608 
using while_option_rule[where P = "\<lambda>c'. c' : Com(X) \<and> vars(strip c') \<subseteq> X", OF _ assms(1)] 

609 
by(simp add: assms(2)) 

610 

611 
lemma iter_widen_Com: fixes f :: "'a::WN st option acom \<Rightarrow> 'a st option acom" 

612 
assumes "iter_widen f c = Some c'" 

613 
and "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> f c : Com(X)" 

614 
and "!!c. strip(f c) = strip c" 

615 
and "c : Com(X)" and "vars (strip c) \<subseteq> X" shows "c' : Com(X)" 

616 
proof 

617 
have "\<forall>c. c : Com(X) \<longrightarrow> vars(strip c) \<subseteq> X \<longrightarrow> c \<nabla>\<^sub>c f c : Com(X)" 

618 
by (metis (full_types) widen_acom_Com assms(2,3)) 

619 
from while_Com[OF assms(1)[simplified iter_widen_def] _ this assms(4,5)] 

620 
show ?thesis using assms(3) by(simp) 

621 
qed 

622 

46387  623 

624 
context Abs_Int2 

625 
begin 

626 

46251  627 
lemma iter_widen_step'_Com: 
628 
"iter_widen (step' \<top>) c = Some c' \<Longrightarrow> vars(strip c) \<subseteq> X \<Longrightarrow> c : Com(X) 

629 
\<Longrightarrow> c' : Com(X)" 

630 
apply(subgoal_tac "strip c'= strip c") 

631 
prefer 2 apply (metis strip_iter_widen strip_step') 

632 
apply(drule iter_widen_Com) 

633 
prefer 3 apply assumption 

634 
prefer 3 apply assumption 

635 
apply (auto simp: step'_Com) 

636 
done 

637 

46387  638 
end 
639 

640 
theorem AI_ivl'_termination: 

641 
"EX c'. AI_ivl' c = Some c'" 

46251  642 
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination split: option.split) 
643 
apply(rule iter_narrow_step_ivl_termination) 

644 
apply (metis bot_acom_Com iter_widen_step'_Com[OF _ subset_refl] strip_iter_widen strip_step') 

645 
apply(erule iter_widen_pfp) 

646 
done 

647 

45111  648 
end 
46251  649 

650 

651 
(* interesting(?) relic 

652 
lemma widen_assoc: 

653 
"~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> ((x::ivl) \<nabla> y) \<nabla> z = x \<nabla> (y \<nabla> z)" 

654 
apply(cases x) 

655 
apply(cases y) 

656 
apply(cases z) 

657 
apply(rename_tac x1 x2 y1 y2 z1 z2) 

658 
apply(simp add: le_ivl_def) 

659 
apply(case_tac x1) 

660 
apply(case_tac x2) 

661 
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) 

662 
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) 

663 
apply(case_tac x2) 

664 
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) 

665 
apply(case_tac y1) 

666 
apply(case_tac y2) 

667 
apply(simp add:le_option_def widen_ivl_def split: if_splits option.splits) 

668 
apply(case_tac z1) 

669 
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1] 

670 
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1] 

671 
apply(case_tac y2) 

672 
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits ivl.splits)[1] 

673 
apply(case_tac z1) 

674 
apply(auto simp add:le_option_def widen_ivl_def split: if_splits ivl.splits option.splits)[1] 

675 
apply(case_tac z2) 

676 
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1] 

677 
apply(auto simp add:le_option_def widen_ivl_def split: if_splits option.splits)[1] 

678 
done 

679 

680 
lemma widen_step_trans: 

681 
"~ (y::ivl) \<sqsubseteq> x \<Longrightarrow> ~ z \<sqsubseteq> x \<nabla> y \<Longrightarrow> EX u. (x \<nabla> y) \<nabla> z = x \<nabla> u \<and> ~ u \<sqsubseteq> x" 

682 
by (metis widen_assoc preord_class.le_trans widen1) 

683 
*) 