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

3 
theory Abs_Int1 

46246  4 
imports Abs_Int0 Vars 
45111  5 
begin 
6 

7 
instantiation prod :: (preord,preord) preord 

8 
begin 

9 

10 
definition "le_prod p1 p2 = (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)" 

11 

12 
instance 

13 
proof 

14 
case goal1 show ?case by(simp add: le_prod_def) 

15 
next 

16 
case goal2 thus ?case unfolding le_prod_def by(metis le_trans) 

17 
qed 

18 

19 
end 

20 

46246  21 
instantiation com :: vars 
22 
begin 

23 

24 
fun vars_com :: "com \<Rightarrow> vname set" where 

25 
"vars com.SKIP = {}"  

26 
"vars (x::=e) = {x} \<union> vars e"  

27 
"vars (c1;c2) = vars c1 \<union> vars c2"  

28 
"vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2"  

29 
"vars (WHILE b DO c) = vars b \<union> vars c" 

30 

31 
instance .. 

32 

33 
end 

34 

35 
lemma finite_avars: "finite(vars(a::aexp))" 

36 
by(induction a) simp_all 

37 

38 
lemma finite_bvars: "finite(vars(b::bexp))" 

39 
by(induction b) (simp_all add: finite_avars) 

40 

41 
lemma finite_cvars: "finite(vars(c::com))" 

42 
by(induction c) (simp_all add: finite_avars finite_bvars) 

43 

45111  44 

45 
subsection "Backward Analysis of Expressions" 

46 

47 
hide_const bot 

48 

49 
class L_top_bot = SL_top + 

50 
fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65) 

51 
and bot :: "'a" ("\<bottom>") 

52 
assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x" 

53 
and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y" 

54 
and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z" 

55 
assumes bot[simp]: "\<bottom> \<sqsubseteq> x" 

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

56 
begin 
45111  57 

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

58 
lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

59 
by (metis meet_greatest meet_le1 meet_le2 le_trans) 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

60 

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

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

62 

46039  63 
locale Val_abs1_gamma = 
46346
10c18630612a
removed duplicate definitions that made locale inconsistent
nipkow
parents:
46251
diff
changeset

64 
Gamma where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" + 
46039  65 
assumes inter_gamma_subset_gamma_meet: 
66 
"\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)" 

67 
and gamma_Bot[simp]: "\<gamma> \<bottom> = {}" 

45111  68 
begin 
69 

46039  70 
lemma in_gamma_meet: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)" 
71 
by (metis IntI inter_gamma_subset_gamma_meet set_mp) 

45111  72 

46039  73 
lemma gamma_meet[simp]: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2" 
74 
by (metis equalityI inter_gamma_subset_gamma_meet le_inf_iff mono_gamma meet_le1 meet_le2) 

45111  75 

76 
end 

77 

78 

46063  79 
locale Val_abs1 = 
46355
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

80 
Val_abs1_gamma where \<gamma> = \<gamma> 
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

81 
for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" + 
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

82 
fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool" 
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

83 
and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av" 
46063  84 
and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av" 
46355
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

85 
assumes test_num': "test_num' n a = (n : \<gamma> a)" 
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

86 
and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow> 
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

87 
n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2" 
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

88 
and filter_less': "filter_less' (n1<n2) a1 a2 = (b1,b2) \<Longrightarrow> 
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

89 
n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2" 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

90 

45111  91 

46063  92 
locale Abs_Int1 = 
93 
Val_abs1 where \<gamma> = \<gamma> for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" 

45111  94 
begin 
95 

46039  96 
lemma in_gamma_join_UpI: "s : \<gamma>\<^isub>o S1 \<or> s : \<gamma>\<^isub>o S2 \<Longrightarrow> s : \<gamma>\<^isub>o(S1 \<squnion> S2)" 
97 
by (metis (no_types) join_ge1 join_ge2 mono_gamma_o set_rev_mp) 

45111  98 

46063  99 
fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

100 
"aval'' e None = \<bottom>"  
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

101 
"aval'' e (Some sa) = aval' e sa" 
45111  102 

46039  103 
lemma aval''_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)" 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

104 
by(cases S)(simp add: aval'_sound)+ 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

105 

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

106 
subsubsection "Backward analysis" 
45111  107 

46063  108 
fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where 
46355
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

109 
"afilter (N n) a S = (if test_num' n a then S else None)"  
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

110 
"afilter (V x) a S = (case S of None \<Rightarrow> None  Some S \<Rightarrow> 
45111  111 
let a' = lookup S x \<sqinter> a in 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

112 
if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))"  
45111  113 
"afilter (Plus e1 e2) a S = 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

114 
(let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S) 
45111  115 
in afilter e1 a1 (afilter e2 a2 S))" 
116 

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

117 
text{* The test for @{const bot} in the @{const V}case is important: @{const 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

118 
bot} indicates that a variable has no possible values, i.e.\ that the current 
45111  119 
program point is unreachable. But then the abstract state should collapse to 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

120 
@{const None}. Put differently, we maintain the invariant that in an abstract 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

121 
state of the form @{term"Some s"}, all variables are mapped to non@{const 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

122 
bot} values. Otherwise the (pointwise) join of two abstract states, one of 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

123 
which contains @{const bot} values, may produce too large a result, thus 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

124 
making the analysis less precise. *} 
45111  125 

126 

46063  127 
fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

128 
"bfilter (Bc v) res S = (if v=res then S else None)"  
45111  129 
"bfilter (Not b) res S = bfilter b (\<not> res) S"  
130 
"bfilter (And b1 b2) res S = 

131 
(if res then bfilter b1 True (bfilter b2 True S) 

132 
else bfilter b1 False S \<squnion> bfilter b2 False S)"  

133 
"bfilter (Less e1 e2) res S = 

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

134 
(let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S) 
45111  135 
in afilter e1 res1 (afilter e2 res2 S))" 
136 

46039  137 
lemma afilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)" 
45111  138 
proof(induction e arbitrary: a S) 
46355
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

139 
case N thus ?case by simp (metis test_num') 
45111  140 
next 
141 
case (V x) 

46039  142 
obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>f S'" using `s : \<gamma>\<^isub>o S` 
143 
by(auto simp: in_gamma_option_iff) 

144 
moreover hence "s x : \<gamma> (lookup S' x)" by(simp add: \<gamma>_st_def) 

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

145 
moreover have "s x : \<gamma> a" using V by simp 
45111  146 
ultimately show ?case using V(1) 
46039  147 
by(simp add: lookup_update Let_def \<gamma>_st_def) 
148 
(metis mono_gamma emptyE in_gamma_meet gamma_Bot subset_empty) 

45111  149 
next 
150 
case (Plus e1 e2) thus ?case 

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

151 
using filter_plus'[OF _ aval''_sound[OF Plus(3)] aval''_sound[OF Plus(3)]] 
45111  152 
by (auto split: prod.split) 
153 
qed 

154 

46039  155 
lemma bfilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^isub>o(bfilter b bv S)" 
45111  156 
proof(induction b arbitrary: S bv) 
45200  157 
case Bc thus ?case by simp 
45111  158 
next 
159 
case (Not b) thus ?case by simp 

160 
next 

46039  161 
case (And b1 b2) thus ?case by(fastforce simp: in_gamma_join_UpI) 
45111  162 
next 
163 
case (Less e1 e2) thus ?case 

164 
by (auto split: prod.split) 

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

165 
(metis afilter_sound filter_less' aval''_sound Less) 
45111  166 
qed 
167 

168 

46063  169 
fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom" 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

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

171 
"step' S (SKIP {P}) = (SKIP {S})"  
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

172 
"step' S (x ::= e {P}) = 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

173 
x ::= e {case S of None \<Rightarrow> None  Some S \<Rightarrow> Some(update S x (aval' e S))}"  
45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

174 
"step' S (c1; c2) = step' S c1; step' (post c1) c2"  
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

175 
"step' S (IF b THEN c1 ELSE c2 {P}) = 
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

176 
(let c1' = step' (bfilter b True S) c1; c2' = step' (bfilter b False S) c2 
45111  177 
in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})"  
45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

178 
"step' S ({Inv} WHILE b DO c {P}) = 
45111  179 
{S \<squnion> post c} 
45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

180 
WHILE b DO step' (bfilter b True Inv) c 
45111  181 
{bfilter b False Inv}" 
182 

46063  183 
definition AI :: "com \<Rightarrow> 'av st option acom option" where 
45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

184 
"AI = lpfp\<^isub>c (step' \<top>)" 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

185 

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

186 
lemma strip_step'[simp]: "strip(step' S c) = strip c" 
45111  187 
by(induct c arbitrary: S) (simp_all add: Let_def) 
188 

189 

190 
subsubsection "Soundness" 

191 

46039  192 
lemma in_gamma_update: 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

193 
"\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(update S x a)" 
46039  194 
by(simp add: \<gamma>_st_def lookup_update) 
45111  195 

46068  196 
lemma step_preserves_le: 
197 
"\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; cs \<le> \<gamma>\<^isub>c ca \<rbrakk> \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' S' ca)" 

198 
proof(induction cs arbitrary: ca S S') 

199 
case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP) 

45111  200 
next 
201 
case Assign thus ?case 

46068  202 
by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

203 
split: option.splits del:subsetD) 
45111  204 
next 
46068  205 
case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi) 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

206 
by (metis le_post post_map_acom) 
45111  207 
next 
46068  208 
case (If b cs1 cs2 P) 
209 
then obtain ca1 ca2 Pa where 

210 
"ca= IF b THEN ca1 ELSE ca2 {Pa}" 

46039  211 
"P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2" 
46068  212 
by (fastforce simp: If_le map_acom_If) 
46039  213 
moreover have "post cs1 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)" 
214 
by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom) 

215 
moreover have "post cs2 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)" 

216 
by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom) 

46067  217 
ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

218 
by (simp add: If.IH subset_iff bfilter_sound) 
45111  219 
next 
46068  220 
case (While I b cs1 P) 
221 
then obtain ca1 Ia Pa where 

222 
"ca = {Ia} WHILE b DO ca1 {Pa}" 

46039  223 
"I \<subseteq> \<gamma>\<^isub>o Ia" "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" 
46068  224 
by (fastforce simp: map_acom_While While_le) 
46067  225 
moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post ca1)" 
226 
using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified] 

46039  227 
by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans) 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

228 
ultimately show ?case by (simp add: While.IH subset_iff bfilter_sound) 
45111  229 
qed 
230 

46070  231 
lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c c'" 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

232 
proof(simp add: CS_def AI_def) 
45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

233 
assume 1: "lpfp\<^isub>c (step' \<top>) c = Some c'" 
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

234 
have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1]) 
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

235 
have 3: "strip (\<gamma>\<^isub>c (step' \<top> c')) = c" 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

236 
by(simp add: strip_lpfpc[OF _ 1]) 
46066  237 
have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' \<top> c')" 
45903  238 
proof(rule lfp_lowerbound[simplified,OF 3]) 
45655
a49f9428aba4
simplified Collecting1 and renamed: step > step', step_cs > step
nipkow
parents:
45623
diff
changeset

239 
show "step UNIV (\<gamma>\<^isub>c (step' \<top> c')) \<le> \<gamma>\<^isub>c (step' \<top> c')" 
46068  240 
proof(rule step_preserves_le[OF _ _]) 
46039  241 
show "UNIV \<subseteq> \<gamma>\<^isub>o \<top>" by simp 
242 
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:
45200
diff
changeset

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

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

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

248 

46246  249 

250 
subsubsection "Commands over a set of variables" 

251 

252 
text{* Key invariant: the domains of all abstract states are subsets of the 

253 
set of variables of the program. *} 

254 

255 
definition "domo S = (case S of None \<Rightarrow> {}  Some S' \<Rightarrow> set(dom S'))" 

256 

257 
definition Com :: "vname set \<Rightarrow> 'a st option acom set" where 

258 
"Com X = {c. \<forall>S \<in> set(annos c). domo S \<subseteq> X}" 

259 

260 
lemma domo_Top[simp]: "domo \<top> = {}" 

261 
by(simp add: domo_def Top_st_def Top_option_def) 

262 

46251  263 
lemma bot_acom_Com[simp]: "\<bottom>\<^sub>c c \<in> Com X" 
46246  264 
by(simp add: bot_acom_def Com_def domo_def set_annos_anno) 
265 

266 
lemma post_in_annos: "post c : set(annos c)" 

267 
by(induction c) simp_all 

268 

269 
lemma domo_join: "domo (S \<squnion> T) \<subseteq> domo S \<union> domo T" 

270 
by(auto simp: domo_def join_st_def split: option.split) 

271 

272 
lemma domo_afilter: "vars a \<subseteq> X \<Longrightarrow> domo S \<subseteq> X \<Longrightarrow> domo(afilter a i S) \<subseteq> X" 

273 
apply(induction a arbitrary: i S) 

274 
apply(simp add: domo_def) 

275 
apply(simp add: domo_def Let_def update_def lookup_def split: option.splits) 

276 
apply blast 

277 
apply(simp split: prod.split) 

278 
done 

279 

280 
lemma domo_bfilter: "vars b \<subseteq> X \<Longrightarrow> domo S \<subseteq> X \<Longrightarrow> domo(bfilter b bv S) \<subseteq> X" 

281 
apply(induction b arbitrary: bv S) 

282 
apply(simp add: domo_def) 

283 
apply(simp) 

284 
apply(simp) 

285 
apply rule 

286 
apply (metis le_sup_iff subset_trans[OF domo_join]) 

287 
apply(simp split: prod.split) 

288 
by (metis domo_afilter) 

289 

290 
lemma step'_Com: 

291 
"domo S \<subseteq> X \<Longrightarrow> vars(strip c) \<subseteq> X \<Longrightarrow> c : Com X \<Longrightarrow> step' S c : Com X" 

292 
apply(induction c arbitrary: S) 

293 
apply(simp add: Com_def) 

294 
apply(simp add: Com_def domo_def update_def split: option.splits) 

295 
apply(simp (no_asm_use) add: Com_def ball_Un) 

296 
apply (metis post_in_annos) 

297 
apply(simp (no_asm_use) add: Com_def ball_Un) 

298 
apply rule 

299 
apply (metis Un_assoc domo_join order_trans post_in_annos subset_Un_eq) 

300 
apply (metis domo_bfilter) 

301 
apply(simp (no_asm_use) add: Com_def) 

302 
apply rule 

303 
apply (metis domo_join le_sup_iff post_in_annos subset_trans) 

304 
apply rule 

305 
apply (metis domo_bfilter) 

306 
by (metis domo_bfilter) 

307 

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

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

309 

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

310 

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

311 
subsubsection "Monotonicity" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

312 

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

313 
locale Abs_Int1_mono = Abs_Int1 + 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

314 
assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

315 
and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow> 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

316 
filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

317 
and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

318 
filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

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

320 

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

321 
lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'" 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

322 
by(induction e) (auto simp: le_st_def lookup_def mono_plus') 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

323 

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

324 
lemma mono_aval'': "S \<sqsubseteq> S' \<Longrightarrow> aval'' e S \<sqsubseteq> aval'' e S'" 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

325 
apply(cases S) 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

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

327 
apply(cases S') 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

328 
apply simp 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

329 
by (simp add: mono_aval') 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

330 

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

331 
lemma mono_afilter: "r \<sqsubseteq> r' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> afilter e r S \<sqsubseteq> afilter e r' S'" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

332 
apply(induction e arbitrary: r r' S S') 
46355
42a01315d998
removed accidental dependance of abstract interpreter on gamma
nipkow
parents:
46346
diff
changeset

333 
apply(auto simp: test_num' Let_def split: option.splits prod.splits) 
46039  334 
apply (metis mono_gamma subsetD) 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

335 
apply(drule_tac x = "list" in mono_lookup) 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

336 
apply (metis mono_meet le_trans) 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

337 
apply (metis mono_meet mono_lookup mono_update) 
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

338 
apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv) 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

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

340 

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

341 
lemma mono_bfilter: "S \<sqsubseteq> S' \<Longrightarrow> bfilter b r S \<sqsubseteq> bfilter b r S'" 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

342 
apply(induction b arbitrary: r S S') 
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

343 
apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] split: prod.splits) 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

344 
apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv) 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

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

346 

46153  347 
lemma mono_step': "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'" 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

348 
apply(induction c c' arbitrary: S S' rule: le_acom.induct) 
46153  349 
apply (auto simp: mono_post mono_bfilter mono_update mono_aval' Let_def le_join_disj 
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45200
diff
changeset

350 
split: option.split) 
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset

351 
done 
45111  352 

46153  353 
lemma mono_step'2: "mono (step' S)" 
354 
by(simp add: mono_def mono_step'[OF le_refl]) 

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

355 

45111  356 
end 
357 

358 
end 