author  nipkow 
Fri, 07 Feb 2014 14:18:31 +0100  
changeset 55357  1dd39517e1ce 
parent 53015  a1119cf551e8 
child 55599  6535c537b243 
permissions  rwrr 
47613  1 
(* Author: Tobias Nipkow *) 
2 

3 
theory Abs_Int3 

4 
imports Abs_Int2_ivl 

5 
begin 

6 

7 

8 
subsection "Widening and Narrowing" 

9 

10 
class widen = 

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

12 

13 
class narrow = 

14 
fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65) 

15 

52504  16 
class wn = widen + narrow + order + 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

17 
assumes widen1: "x \<le> x \<nabla> y" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

18 
assumes widen2: "y \<le> x \<nabla> y" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

19 
assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

20 
assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x" 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

21 
begin 
47613  22 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

23 
lemma narrowid[simp]: "x \<triangle> x = x" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

24 
by (metis eq_iff narrow1 narrow2) 
47613  25 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

26 
end 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

27 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52504
diff
changeset

28 
lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{wn,order_top})" 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

29 
by (metis eq_iff top_greatest widen2) 
47613  30 

52504  31 
instantiation ivl :: wn 
47613  32 
begin 
33 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

34 
definition "widen_rep p1 p2 = 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

35 
(if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 else 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

36 
let (l1,h1) = p1; (l2,h2) = p2 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

37 
in (if l2 < l1 then Minf else l1, if h1 < h2 then Pinf else h1))" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

38 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

39 
lift_definition widen_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is widen_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

40 
by(auto simp: widen_rep_def eq_ivl_iff) 
47613  41 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

42 
definition "narrow_rep p1 p2 = 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

43 
(if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

44 
let (l1,h1) = p1; (l2,h2) = p2 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

45 
in (if l1 = Minf then l2 else l1, if h1 = Pinf then h2 else h1))" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

46 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

47 
lift_definition narrow_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is narrow_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

48 
by(auto simp: narrow_rep_def eq_ivl_iff) 
47613  49 

50 
instance 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

51 
proof 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

52 
qed (transfer, auto simp: widen_rep_def narrow_rep_def le_iff_subset \<gamma>_rep_def subset_eq is_empty_rep_def empty_rep_def eq_ivl_def split: if_splits extended.splits)+ 
47613  53 

54 
end 

55 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52504
diff
changeset

56 
instantiation st :: ("{order_top,wn}")wn 
47613  57 
begin 
58 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

59 
lift_definition widen_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<nabla>)" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

60 
by(auto simp: eq_st_def) 
47613  61 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

62 
lift_definition narrow_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<triangle>)" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

63 
by(auto simp: eq_st_def) 
47613  64 

65 
instance 

66 
proof 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

67 
case goal1 thus ?case 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

68 
by transfer (simp add: less_eq_st_rep_iff widen1) 
47613  69 
next 
70 
case goal2 thus ?case 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

71 
by transfer (simp add: less_eq_st_rep_iff widen2) 
47613  72 
next 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

73 
case goal3 thus ?case 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

74 
by transfer (simp add: less_eq_st_rep_iff narrow1) 
47613  75 
next 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

76 
case goal4 thus ?case 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

77 
by transfer (simp add: less_eq_st_rep_iff narrow2) 
47613  78 
qed 
79 

80 
end 

81 

82 

52504  83 
instantiation option :: (wn)wn 
47613  84 
begin 
85 

86 
fun widen_option where 

87 
"None \<nabla> x = x"  

88 
"x \<nabla> None = x"  

89 
"(Some x) \<nabla> (Some y) = Some(x \<nabla> y)" 

90 

91 
fun narrow_option where 

92 
"None \<triangle> x = None"  

93 
"x \<triangle> None = None"  

94 
"(Some x) \<triangle> (Some y) = Some(x \<triangle> y)" 

95 

96 
instance 

97 
proof 

98 
case goal1 thus ?case 

99 
by(induct x y rule: widen_option.induct)(simp_all add: widen1) 

100 
next 

101 
case goal2 thus ?case 

102 
by(induct x y rule: widen_option.induct)(simp_all add: widen2) 

103 
next 

104 
case goal3 thus ?case 

105 
by(induct x y rule: narrow_option.induct) (simp_all add: narrow1) 

106 
next 

107 
case goal4 thus ?case 

108 
by(induct x y rule: narrow_option.induct) (simp_all add: narrow2) 

109 
qed 

110 

111 
end 

112 

52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

113 
definition map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" 
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

114 
where 
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

115 
"map2_acom f C1 C2 = annotate (\<lambda>p. f (anno C1 p) (anno C2 p)) (strip C1)" 
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

116 

52504  117 

49548  118 
instantiation acom :: (widen)widen 
119 
begin 

120 
definition "widen_acom = map2_acom (op \<nabla>)" 

121 
instance .. 

122 
end 

123 

124 
instantiation acom :: (narrow)narrow 

125 
begin 

126 
definition "narrow_acom = map2_acom (op \<triangle>)" 

127 
instance .. 

128 
end 

129 

47613  130 
lemma strip_map2_acom[simp]: 
131 
"strip C1 = strip C2 \<Longrightarrow> strip(map2_acom f C1 C2) = strip C1" 

52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

132 
by(simp add: map2_acom_def) 
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

133 
(*by(induct f C1 C2 rule: map2_acom.induct) simp_all*) 
47613  134 

135 
lemma strip_widen_acom[simp]: 

136 
"strip C1 = strip C2 \<Longrightarrow> strip(C1 \<nabla> C2) = strip C1" 

49548  137 
by(simp add: widen_acom_def) 
47613  138 

139 
lemma strip_narrow_acom[simp]: 

140 
"strip C1 = strip C2 \<Longrightarrow> strip(C1 \<triangle> C2) = strip C1" 

49548  141 
by(simp add: narrow_acom_def) 
47613  142 

52504  143 
lemma narrow1_acom: "C2 \<le> C1 \<Longrightarrow> C2 \<le> C1 \<triangle> (C2::'a::wn acom)" 
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

144 
by(simp add: narrow_acom_def narrow1 map2_acom_def less_eq_acom_def size_annos) 
47613  145 

52504  146 
lemma narrow2_acom: "C2 \<le> C1 \<Longrightarrow> C1 \<triangle> (C2::'a::wn acom) \<le> C1" 
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

147 
by(simp add: narrow_acom_def narrow2 map2_acom_def less_eq_acom_def size_annos) 
47613  148 

149 

52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

150 
subsubsection "Prefixpoint computation" 
47613  151 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

152 
definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,widen})option" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

153 
where "iter_widen f = while_option (\<lambda>x. \<not> f x \<le> x) (\<lambda>x. x \<nabla> f x)" 
47613  154 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

155 
definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,narrow})option" 
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

156 
where "iter_narrow f = while_option (\<lambda>x. x \<triangle> f x < x) (\<lambda>x. x \<triangle> f x)" 
47613  157 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

158 
definition pfp_wn :: "('a::{order,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" 
49548  159 
where "pfp_wn f x = 
49576  160 
(case iter_widen f x of None \<Rightarrow> None  Some p \<Rightarrow> iter_narrow f p)" 
47613  161 

162 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

163 
lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<le> p" 
47613  164 
by(auto simp add: iter_widen_def dest: while_option_stop) 
165 

166 
lemma iter_widen_inv: 

167 
assumes "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" and "P x" 

168 
and "iter_widen f x = Some y" shows "P y" 

169 
using while_option_rule[where P = "P", OF _ assms(4)[unfolded iter_widen_def]] 

170 
by (blast intro: assms(13)) 

171 

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

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

174 
shows "strip C' = strip C" 

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

176 
by (metis assms(1)) 

177 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

178 
lemma strip_iter_widen: fixes f :: "'a::{order,widen} acom \<Rightarrow> 'a acom" 
47613  179 
assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'" 
180 
shows "strip C' = strip C" 

181 
proof 

182 
have "\<forall>C. strip(C \<nabla> f C) = strip C" 

183 
by (metis assms(1) strip_map2_acom widen_acom_def) 

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

185 
qed 

186 

187 
lemma iter_narrow_pfp: 

52504  188 
assumes mono: "!!x1 x2::_::wn acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2" 
49576  189 
and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)" 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

190 
and "P p0" and "f p0 \<le> p0" and "iter_narrow f p0 = Some p" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

191 
shows "P p \<and> f p \<le> p" 
47613  192 
proof 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

193 
let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0" 
49576  194 
{ fix p assume "?Q p" 
47613  195 
note P = conjunct1[OF this] and 12 = conjunct2[OF this] 
196 
note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12] 

49576  197 
let ?p' = "p \<triangle> f p" 
198 
have "?Q ?p'" 

47613  199 
proof auto 
49576  200 
show "P ?p'" by (blast intro: P Pinv) 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

201 
have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)` P narrow2_acom[OF 1]]) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

202 
also have "\<dots> \<le> ?p'" by(rule narrow1_acom[OF 1]) 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

203 
finally show "f ?p' \<le> ?p'" . 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

204 
have "?p' \<le> p" by (rule narrow2_acom[OF 1]) 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

205 
also have "p \<le> p0" by(rule 2) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

206 
finally show "?p' \<le> p0" . 
47613  207 
qed 
208 
} 

209 
thus ?thesis 

210 
using while_option_rule[where P = ?Q, OF _ assms(6)[simplified iter_narrow_def]] 

211 
by (blast intro: assms(4,5) le_refl) 

212 
qed 

213 

214 
lemma pfp_wn_pfp: 

52504  215 
assumes mono: "!!x1 x2::_::wn acom. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2" 
49548  216 
and Pinv: "P x" "!!x. P x \<Longrightarrow> P(f x)" 
217 
"!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)" 

218 
"!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)" 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

219 
and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<le> p" 
47613  220 
proof 
49576  221 
from pfp_wn obtain p0 
222 
where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p" 

47613  223 
by(auto simp: pfp_wn_def split: option.splits) 
49576  224 
have "P p0" by (blast intro: iter_widen_inv[where P="P"] its(1) Pinv(13)) 
47613  225 
thus ?thesis 
226 
by  (assumption  

227 
rule iter_narrow_pfp[where P=P] mono Pinv(2,4) iter_widen_pfp its)+ 

228 
qed 

229 

230 
lemma strip_pfp_wn: 

49548  231 
"\<lbrakk> \<forall>C. strip(f C) = strip C; pfp_wn f C = Some C' \<rbrakk> \<Longrightarrow> strip C' = strip C" 
47613  232 
by(auto simp add: pfp_wn_def iter_narrow_def split: option.splits) 
51390  233 
(metis (mono_tags) strip_iter_widen strip_narrow_acom strip_while) 
47613  234 

235 

52504  236 
locale Abs_Int_wn = Abs_Int_inv_mono where \<gamma>=\<gamma> 
237 
for \<gamma> :: "'av::{wn,bounded_lattice} \<Rightarrow> val set" 

47613  238 
begin 
239 

240 
definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

241 
"AI_wn c = pfp_wn (step' \<top>) (bot c)" 
47613  242 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

243 
lemma AI_wn_correct: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c C" 
47613  244 
proof(simp add: CS_def AI_wn_def) 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

245 
assume 1: "pfp_wn (step' \<top>) (bot c) = Some C" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

246 
have 2: "strip C = c \<and> step' \<top> C \<le> C" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

247 
by(rule pfp_wn_pfp[where x="bot c"]) (simp_all add: 1 mono_step'_top) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

248 
have pfp: "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c C" 
50986  249 
proof(rule order_trans) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

250 
show "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' \<top> C)" 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

251 
by(rule step_step') 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

252 
show "... \<le> \<gamma>\<^sub>c C" 
50986  253 
by(rule mono_gamma_c[OF conjunct2[OF 2]]) 
47613  254 
qed 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

255 
have 3: "strip (\<gamma>\<^sub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1]) 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

256 
have "lfp c (step (\<gamma>\<^sub>o \<top>)) \<le> \<gamma>\<^sub>c C" 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

257 
by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^sub>o \<top>)", OF 3 pfp]) 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

258 
thus "lfp c (step UNIV) \<le> \<gamma>\<^sub>c C" by simp 
47613  259 
qed 
260 

261 
end 

262 

52504  263 
interpretation Abs_Int_wn 
51245  264 
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" 
47613  265 
and test_num' = in_ivl 
51974  266 
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl 
51953  267 
defines AI_wn_ivl is AI_wn 
47613  268 
.. 
269 

270 

271 
subsubsection "Tests" 

272 

51791  273 
definition "step_up_ivl n = ((\<lambda>C. C \<nabla> step_ivl \<top> C)^^n)" 
274 
definition "step_down_ivl n = ((\<lambda>C. C \<triangle> step_ivl \<top> C)^^n)" 

47613  275 

276 
text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as 

51953  277 
the loop took to execute. In contrast, @{const AI_wn_ivl} converges in a 
47613  278 
constant number of steps: *} 
279 

280 
value "show_acom (step_up_ivl 1 (bot test3_ivl))" 

281 
value "show_acom (step_up_ivl 2 (bot test3_ivl))" 

282 
value "show_acom (step_up_ivl 3 (bot test3_ivl))" 

283 
value "show_acom (step_up_ivl 4 (bot test3_ivl))" 

284 
value "show_acom (step_up_ivl 5 (bot test3_ivl))" 

49188  285 
value "show_acom (step_up_ivl 6 (bot test3_ivl))" 
286 
value "show_acom (step_up_ivl 7 (bot test3_ivl))" 

287 
value "show_acom (step_up_ivl 8 (bot test3_ivl))" 

288 
value "show_acom (step_down_ivl 1 (step_up_ivl 8 (bot test3_ivl)))" 

289 
value "show_acom (step_down_ivl 2 (step_up_ivl 8 (bot test3_ivl)))" 

290 
value "show_acom (step_down_ivl 3 (step_up_ivl 8 (bot test3_ivl)))" 

291 
value "show_acom (step_down_ivl 4 (step_up_ivl 8 (bot test3_ivl)))" 

51953  292 
value "show_acom_opt (AI_wn_ivl test3_ivl)" 
47613  293 

294 

295 
text{* Now all the analyses terminate: *} 

296 

51953  297 
value "show_acom_opt (AI_wn_ivl test4_ivl)" 
298 
value "show_acom_opt (AI_wn_ivl test5_ivl)" 

299 
value "show_acom_opt (AI_wn_ivl test6_ivl)" 

47613  300 

301 

302 
subsubsection "Generic Termination Proof" 

303 

51722  304 
lemma top_on_opt_widen: 
51785  305 
"top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<nabla> o2 :: _ st option) X" 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

306 
apply(induct o1 o2 rule: widen_option.induct) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

307 
apply (auto) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

308 
by transfer simp 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

309 

51722  310 
lemma top_on_opt_narrow: 
51785  311 
"top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<triangle> o2 :: _ st option) X" 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

312 
apply(induct o1 o2 rule: narrow_option.induct) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

313 
apply (auto) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

314 
by transfer simp 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

315 

52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

316 
(* FIXME mk anno abbrv *) 
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

317 
lemma annos_map2_acom[simp]: "strip C2 = strip C1 \<Longrightarrow> 
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

318 
annos(map2_acom f C1 C2) = map (%(x,y).f x y) (zip (annos C1) (annos C2))" 
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

319 
by(simp add: map2_acom_def list_eq_iff_nth_eq size_annos anno_def[symmetric] size_annos_same[of C1 C2]) 
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

320 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

321 
lemma top_on_acom_widen: 
51785  322 
"\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk> 
323 
\<Longrightarrow> top_on_acom (C1 \<nabla> C2 :: _ st option acom) X" 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

324 
by(auto simp add: widen_acom_def top_on_acom_def)(metis top_on_opt_widen in_set_zipE) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

325 

df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

326 
lemma top_on_acom_narrow: 
51785  327 
"\<lbrakk>top_on_acom C1 X; strip C1 = strip C2; top_on_acom C2 X\<rbrakk> 
328 
\<Longrightarrow> top_on_acom (C1 \<triangle> C2 :: _ st option acom) X" 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

329 
by(auto simp add: narrow_acom_def top_on_acom_def)(metis top_on_opt_narrow in_set_zipE) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

330 

51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

331 
text{* The assumptions for widening and narrowing differ because during 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

332 
narrowing we have the invariant @{prop"y \<le> x"} (where @{text y} is the next 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

333 
iterate), but during widening there is no such invariant, there we only have 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

334 
that not yet @{prop"y \<le> x"}. This complicates the termination proof for 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

335 
widening. *} 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

336 

52504  337 
locale Measure_wn = Measure1 where m=m 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52504
diff
changeset

338 
for m :: "'av::{order_top,wn} \<Rightarrow> nat" + 
47613  339 
fixes n :: "'av \<Rightarrow> nat" 
51372  340 
assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y" 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

341 
assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x" 
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

342 
assumes n_narrow: "y \<le> x \<Longrightarrow> x \<triangle> y < x \<Longrightarrow> n(x \<triangle> y) < n x" 
47613  343 

344 
begin 

345 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

346 
lemma m_s_anti_mono_rep: assumes "\<forall>x. S1 x \<le> S2 x" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

347 
shows "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

348 
proof 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

349 
from assms have "\<forall>x. m(S1 x) \<ge> m(S2 x)" by (metis m_anti_mono) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

350 
thus "(\<Sum>x\<in>X. m (S2 x)) \<le> (\<Sum>x\<in>X. m (S1 x))" by (metis setsum_mono) 
51372  351 
qed 
352 

51791  353 
lemma m_s_anti_mono: "S1 \<le> S2 \<Longrightarrow> m_s S1 X \<ge> m_s S2 X" 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

354 
unfolding m_s_def 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

355 
apply (transfer fixing: m) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

356 
apply(simp add: less_eq_st_rep_iff eq_st_def m_s_anti_mono_rep) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

357 
done 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

358 

df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

359 
lemma m_s_widen_rep: assumes "finite X" "S1 = S2 on X" "\<not> S2 x \<le> S1 x" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

360 
shows "(\<Sum>x\<in>X. m (S1 x \<nabla> S2 x)) < (\<Sum>x\<in>X. m (S1 x))" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

361 
proof 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

362 
have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S1 x \<nabla> S2 x)" 
52504  363 
by (metis m_anti_mono wn_class.widen1) 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

364 
have "x \<in> X" using assms(2,3) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

365 
by(auto simp add: Ball_def) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

366 
hence 2: "\<exists>x\<in>X. m(S1 x) > m(S1 x \<nabla> S2 x)" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

367 
using assms(3) m_widen by blast 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

368 
from setsum_strict_mono_ex1[OF `finite X` 1 2] 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

369 
show ?thesis . 
47613  370 
qed 
371 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

372 
lemma m_s_widen: "finite X \<Longrightarrow> fun S1 = fun S2 on X ==> 
51791  373 
~ S2 \<le> S1 \<Longrightarrow> m_s (S1 \<nabla> S2) X < m_s S1 X" 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

374 
apply(auto simp add: less_st_def m_s_def) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

375 
apply (transfer fixing: m) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

376 
apply(auto simp add: less_eq_st_rep_iff m_s_widen_rep) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

377 
done 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

378 

51785  379 
lemma m_o_anti_mono: "finite X \<Longrightarrow> top_on_opt o1 (X) \<Longrightarrow> top_on_opt o2 (X) \<Longrightarrow> 
51791  380 
o1 \<le> o2 \<Longrightarrow> m_o o1 X \<ge> m_o o2 X" 
51372  381 
proof(induction o1 o2 rule: less_eq_option.induct) 
382 
case 1 thus ?case by (simp add: m_o_def)(metis m_s_anti_mono) 

383 
next 

384 
case 2 thus ?case 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

385 
by(simp add: m_o_def le_SucI m_s_h split: option.splits) 
51372  386 
next 
387 
case 3 thus ?case by simp 

388 
qed 

389 

51785  390 
lemma m_o_widen: "\<lbrakk> finite X; top_on_opt S1 (X); top_on_opt S2 (X); \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow> 
51791  391 
m_o (S1 \<nabla> S2) X < m_o S1 X" 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

392 
by(auto simp: m_o_def m_s_h less_Suc_eq_le m_s_widen split: option.split) 
47613  393 

49547  394 
lemma m_c_widen: 
51785  395 
"strip C1 = strip C2 \<Longrightarrow> top_on_acom C1 (vars C1) \<Longrightarrow> top_on_acom C2 (vars C2) 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

396 
\<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1" 
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

397 
apply(auto simp: m_c_def widen_acom_def map2_acom_def size_annos[symmetric] anno_def[symmetric]listsum_setsum_nth) 
49547  398 
apply(subgoal_tac "length(annos C2) = length(annos C1)") 
51390  399 
prefer 2 apply (simp add: size_annos_same2) 
49547  400 
apply (auto) 
401 
apply(rule setsum_strict_mono_ex1) 

52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

402 
apply(auto simp add: m_o_anti_mono vars_acom_def anno_def top_on_acom_def top_on_opt_widen widen1 less_eq_acom_def listrel_iff_nth) 
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51974
diff
changeset

403 
apply(rule_tac x=p in bexI) 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

404 
apply (auto simp: vars_acom_def m_o_widen top_on_acom_def) 
49547  405 
done 
406 

407 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

408 
definition n_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^sub>s") where 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

409 
"n\<^sub>s S X = (\<Sum>x\<in>X. n(fun S x))" 
49547  410 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

411 
lemma n_s_narrow_rep: 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

412 
assumes "finite X" "S1 = S2 on X" "\<forall>x. S2 x \<le> S1 x" "\<forall>x. S1 x \<triangle> S2 x \<le> S1 x" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

413 
"S1 x \<noteq> S1 x \<triangle> S2 x" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

414 
shows "(\<Sum>x\<in>X. n (S1 x \<triangle> S2 x)) < (\<Sum>x\<in>X. n (S1 x))" 
47613  415 
proof 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

416 
have 1: "\<forall>x. n(S1 x \<triangle> S2 x) \<le> n(S1 x)" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

417 
by (metis assms(3) assms(4) eq_iff less_le_not_le n_narrow) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

418 
have "x \<in> X" by (metis Compl_iff assms(2) assms(5) narrowid) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

419 
hence 2: "\<exists>x\<in>X. n(S1 x \<triangle> S2 x) < n(S1 x)" 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

420 
by (metis assms(35) eq_iff less_le_not_le n_narrow) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

421 
show ?thesis 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

422 
apply(rule setsum_strict_mono_ex1[OF `finite X`]) using 1 2 by blast+ 
47613  423 
qed 
424 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

425 
lemma n_s_narrow: "finite X \<Longrightarrow> fun S1 = fun S2 on X \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

426 
\<Longrightarrow> n\<^sub>s (S1 \<triangle> S2) X < n\<^sub>s S1 X" 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

427 
apply(auto simp add: less_st_def n_s_def) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

428 
apply (transfer fixing: n) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

429 
apply(auto simp add: less_eq_st_rep_iff eq_st_def fun_eq_iff n_s_narrow_rep) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

430 
done 
47613  431 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

432 
definition n_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("n\<^sub>o") where 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

433 
"n\<^sub>o opt X = (case opt of None \<Rightarrow> 0  Some S \<Rightarrow> n\<^sub>s S X + 1)" 
47613  434 

435 
lemma n_o_narrow: 

51785  436 
"top_on_opt S1 (X) \<Longrightarrow> top_on_opt S2 (X) \<Longrightarrow> finite X 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

437 
\<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^sub>o (S1 \<triangle> S2) X < n\<^sub>o S1 X" 
47613  438 
apply(induction S1 S2 rule: narrow_option.induct) 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

439 
apply(auto simp: n_o_def n_s_narrow) 
47613  440 
done 
441 

49576  442 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

443 
definition n_c :: "'av st option acom \<Rightarrow> nat" ("n\<^sub>c") where 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

444 
"n\<^sub>c C = listsum (map (\<lambda>a. n\<^sub>o a (vars C)) (annos C))" 
47613  445 

51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

446 
lemma less_annos_iff: "(C1 < C2) = (C1 \<le> C2 \<and> 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

447 
(\<exists>i<length (annos C1). annos C1 ! i < annos C2 ! i))" 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

448 
by(metis (hide_lams, no_types) less_le_not_le le_iff_le_annos size_annos_same2) 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

449 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

450 
lemma n_c_narrow: "strip C1 = strip C2 
51785  451 
\<Longrightarrow> top_on_acom C1 ( vars C1) \<Longrightarrow> top_on_acom C2 ( vars C2) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52729
diff
changeset

452 
\<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^sub>c (C1 \<triangle> C2) < n\<^sub>c C1" 
51792  453 
apply(auto simp: n_c_def narrow_acom_def listsum_setsum_nth) 
47613  454 
apply(subgoal_tac "length(annos C2) = length(annos C1)") 
455 
prefer 2 apply (simp add: size_annos_same2) 

456 
apply (auto) 

51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

457 
apply(simp add: less_annos_iff le_iff_le_annos) 
47613  458 
apply(rule setsum_strict_mono_ex1) 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

459 
apply (auto simp: vars_acom_def top_on_acom_def) 
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

460 
apply (metis n_o_narrow nth_mem finite_cvars less_imp_le le_less order_refl) 
47613  461 
apply(rule_tac x=i in bexI) 
462 
prefer 2 apply simp 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

463 
apply(rule n_o_narrow[where X = "vars(strip C2)"]) 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

464 
apply (simp_all) 
47613  465 
done 
466 

467 
end 

468 

469 

470 
lemma iter_widen_termination: 

52504  471 
fixes m :: "'a::wn acom \<Rightarrow> nat" 
47613  472 
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)" 
473 
and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)" 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

474 
and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<le> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1" 
47613  475 
and "P C" shows "EX C'. iter_widen f C = Some C'" 
49547  476 
proof(simp add: iter_widen_def, 
477 
rule measure_while_option_Some[where P = P and f=m]) 

47613  478 
show "P C" by(rule `P C`) 
479 
next 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

480 
fix C assume "P C" "\<not> f C \<le> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C" 
49547  481 
by(simp add: P_f P_widen m_widen) 
47613  482 
qed 
49496  483 

47613  484 
lemma iter_narrow_termination: 
52504  485 
fixes n :: "'a::wn acom \<Rightarrow> nat" 
47613  486 
assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)" 
487 
and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)" 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

488 
and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> f C1 \<le> f C2" 
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

489 
and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n(C1 \<triangle> C2) < n C1" 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

490 
and init: "P C" "f C \<le> C" shows "EX C'. iter_narrow f C = Some C'" 
49547  491 
proof(simp add: iter_narrow_def, 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

492 
rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<le> C"]) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

493 
show "P C \<and> f C \<le> C" using init by blast 
47613  494 
next 
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

495 
fix C assume 1: "P C \<and> f C \<le> C" and 2: "C \<triangle> f C < C" 
47613  496 
hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow) 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

497 
moreover then have "f (C \<triangle> f C) \<le> C \<triangle> f C" 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

498 
by (metis narrow1_acom narrow2_acom 1 mono order_trans) 
49547  499 
moreover have "n (C \<triangle> f C) < n C" using 1 2 by(simp add: n_narrow P_f) 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

500 
ultimately show "(P (C \<triangle> f C) \<and> f (C \<triangle> f C) \<le> C \<triangle> f C) \<and> n(C \<triangle> f C) < n C" 
49547  501 
by blast 
47613  502 
qed 
503 

52504  504 
locale Abs_Int_wn_measure = Abs_Int_wn where \<gamma>=\<gamma> + Measure_wn where m=m 
505 
for \<gamma> :: "'av::{wn,bounded_lattice} \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat" 

49547  506 

47613  507 

508 
subsubsection "Termination: Intervals" 

509 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

510 
definition m_rep :: "eint2 \<Rightarrow> nat" where 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

511 
"m_rep p = (if is_empty_rep p then 3 else 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

512 
let (l,h) = p in (case l of Minf \<Rightarrow> 0  _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0  _ \<Rightarrow> 1))" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

513 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

514 
lift_definition m_ivl :: "ivl \<Rightarrow> nat" is m_rep 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

515 
by(auto simp: m_rep_def eq_ivl_iff) 
47613  516 

51924  517 
lemma m_ivl_nice: "m_ivl[l,h] = (if [l,h] = \<bottom> then 3 else 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

518 
(if l = Minf then 0 else 1) + (if h = Pinf then 0 else 1))" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

519 
unfolding bot_ivl_def 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

520 
by transfer (auto simp: m_rep_def eq_ivl_empty split: extended.split) 
47613  521 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

522 
lemma m_ivl_height: "m_ivl iv \<le> 3" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

523 
by transfer (simp add: m_rep_def split: prod.split extended.split) 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

524 

00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

525 
lemma m_ivl_anti_mono: "y \<le> x \<Longrightarrow> m_ivl x \<le> m_ivl y" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

526 
by transfer 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

527 
(auto simp: m_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

528 
split: prod.split extended.splits if_splits) 
47613  529 

530 
lemma m_ivl_widen: 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

531 
"~ y \<le> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

532 
by transfer 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

533 
(auto simp: m_rep_def widen_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

534 
split: prod.split extended.splits if_splits) 
47613  535 

536 
definition n_ivl :: "ivl \<Rightarrow> nat" where 

51953  537 
"n_ivl iv = 3  m_ivl iv" 
47613  538 

539 
lemma n_ivl_narrow: 

51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

540 
"x \<triangle> y < x \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x" 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

541 
unfolding n_ivl_def 
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

542 
apply(subst (asm) less_le_not_le) 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

543 
apply transfer 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

544 
by(auto simp add: m_rep_def narrow_rep_def is_empty_rep_def empty_rep_def \<gamma>_rep_cases le_iff_subset 
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

545 
split: prod.splits if_splits extended.split) 
47613  546 

547 

52504  548 
interpretation Abs_Int_wn_measure 
51245  549 
where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +" 
47613  550 
and test_num' = in_ivl 
51974  551 
and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

552 
and m = m_ivl and n = n_ivl and h = 3 
47613  553 
proof 
51372  554 
case goal2 thus ?case by(rule m_ivl_anti_mono) 
47613  555 
next 
51372  556 
case goal1 thus ?case by(rule m_ivl_height) 
47613  557 
next 
49547  558 
case goal3 thus ?case by(rule m_ivl_widen) 
47613  559 
next 
51385
f193d44d4918
termination proof for narrowing: fewer assumptions
nipkow
parents:
51372
diff
changeset

560 
case goal4 from goal4(2) show ?case by(rule n_ivl_narrow) 
49576  561 
 "note that the first assms is unnecessary for intervals" 
47613  562 
qed 
563 

564 
lemma iter_winden_step_ivl_termination: 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

565 
"\<exists>C. iter_widen (step_ivl \<top>) (bot c) = Some C" 
51785  566 
apply(rule iter_widen_termination[where m = "m_c" and P = "%C. strip C = c \<and> top_on_acom C ( vars C)"]) 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

567 
apply (auto simp add: m_c_widen top_on_bot top_on_step'[simplified comp_def vars_acom_def] 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

568 
vars_acom_def top_on_acom_widen) 
47613  569 
done 
570 

571 
lemma iter_narrow_step_ivl_termination: 

51953  572 
"top_on_acom C ( vars C) \<Longrightarrow> step_ivl \<top> C \<le> C \<Longrightarrow> 
573 
\<exists>C'. iter_narrow (step_ivl \<top>) C = Some C'" 

574 
apply(rule iter_narrow_termination[where n = "n_c" and P = "%C'. strip C = strip C' \<and> top_on_acom C' (vars C')"]) 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

575 
apply(auto simp: top_on_step'[simplified comp_def vars_acom_def] 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

576 
mono_step'_top n_c_narrow vars_acom_def top_on_acom_narrow) 
47613  577 
done 
578 

51953  579 
theorem AI_wn_ivl_termination: 
580 
"\<exists>C. AI_wn_ivl c = Some C" 

47613  581 
apply(auto simp: AI_wn_def pfp_wn_def iter_winden_step_ivl_termination 
582 
split: option.split) 

583 
apply(rule iter_narrow_step_ivl_termination) 

51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

584 
apply(rule conjunct2) 
51785  585 
apply(rule iter_widen_inv[where f = "step' \<top>" and P = "%C. c = strip C & top_on_acom C ( vars C)"]) 
51711
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

586 
apply(auto simp: top_on_acom_widen top_on_step'[simplified comp_def vars_acom_def] 
df3426139651
complete revision: finally got rid of annoying Lpredicate
nipkow
parents:
51390
diff
changeset

587 
iter_widen_pfp top_on_bot vars_acom_def) 
47613  588 
done 
589 

51390  590 
(*unused_thms Abs_Int_init  *) 
47613  591 

49578  592 
subsubsection "Counterexamples" 
593 

51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

594 
text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening. 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

595 
It can already be lost after the first step: *} 
49578  596 

52504  597 
lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y" 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

598 
and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)" 
55357  599 
nitpick[card = 3, expect = genuine, show_consts, timeout = 120] 
49578  600 
(* 
601 
1 < 2 < 3, 

602 
f x = 2, 

603 
x widen y = 3  guarantees termination with top=3 

604 
x = 1 

605 
Now f is mono, x <= f x, not f x <= x 

606 
but x widen f x = 3, f 3 = 2, but not 3 <= 2 

607 
*) 

608 
oops 

609 

610 
text{* Widening terminates but may converge more slowly than Kleene iteration. 

611 
In the following model, Kleene iteration goes from 0 to the least pfp 

612 
in one step but widening takes 2 steps to reach a strictly larger pfp: *} 

52504  613 
lemma assumes "!!x y::'a::wn. x \<le> y \<Longrightarrow> f x \<le> f y" 
51359
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

614 
and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x" 
00b45c7e831f
major redesign: order instead of preorder, new definition of intervals as quotients
nipkow
parents:
51245
diff
changeset

615 
shows "f(x \<nabla> f x) \<le> x \<nabla> f x" 
55357  616 
nitpick[card = 4, expect = genuine, show_consts, timeout = 120] 
49578  617 
(* 
618 

619 
0 < 1 < 2 < 3 

620 
f: 1 1 3 3 

621 

622 
0 widen 1 = 2 

623 
2 widen 3 = 3 

624 
and x widen y arbitrary, eg 3, which guarantees termination 

625 

626 
Kleene: f(f 0) = f 1 = 1 <= 1 = f 1 

627 

628 
but 

629 

630 
because not f 0 <= 0, we obtain 0 widen f 0 = 0 wide 1 = 2, 

631 
which is again not a pfp: not f 2 = 3 <= 2 

632 
Another widening step yields 2 widen f 2 = 2 widen 3 = 3 

633 
*) 

49892
09956f7a00af
proper 'oops' to force sequential checking here, and avoid spurious *** Interrupt stemming from crash of forked outer syntax element;
wenzelm
parents:
49579
diff
changeset

634 
oops 
49578  635 

47613  636 
end 