author | nipkow |
Thu, 24 Nov 2011 19:58:37 +0100 | |
changeset 45623 | f682f3f7b726 |
parent 45127 | d2eb07a1e01b |
child 45655 | a49f9428aba4 |
permissions | -rw-r--r-- |
45111 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory Abs_Int0 |
|
4 |
imports Abs_State |
|
5 |
begin |
|
6 |
||
7 |
subsection "Computable Abstract Interpretation" |
|
8 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
9 |
text{* Abstract interpretation over type @{text st} instead of |
45111 | 10 |
functions. *} |
11 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
12 |
context Val_abs |
45111 | 13 |
begin |
14 |
||
15 |
fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where |
|
16 |
"aval' (N n) _ = num' n" | |
|
17 |
"aval' (V x) S = lookup S x" | |
|
18 |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" |
|
19 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
20 |
lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
21 |
by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
22 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
23 |
end |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
24 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
25 |
locale Abs_Int = Val_abs |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
26 |
begin |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
27 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
28 |
fun step :: "'a st option \<Rightarrow> 'a st option acom \<Rightarrow> 'a st option acom" where |
45111 | 29 |
"step S (SKIP {P}) = (SKIP {S})" | |
30 |
"step S (x ::= e {P}) = |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
31 |
x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))}" | |
45111 | 32 |
"step S (c1; c2) = step S c1; step (post c1) c2" | |
33 |
"step S (IF b THEN c1 ELSE c2 {P}) = |
|
34 |
(let c1' = step S c1; c2' = step S c2 |
|
35 |
in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" | |
|
36 |
"step S ({Inv} WHILE b DO c {P}) = |
|
37 |
{S \<squnion> post c} WHILE b DO step Inv c {Inv}" |
|
38 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
39 |
definition AI :: "com \<Rightarrow> 'a st option acom option" where |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
40 |
"AI = lpfp\<^isub>c (step \<top>)" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
41 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
42 |
|
45111 | 43 |
lemma strip_step[simp]: "strip(step S c) = strip c" |
44 |
by(induct c arbitrary: S) (simp_all add: Let_def) |
|
45 |
||
46 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
47 |
text{* Soundness: *} |
45111 | 48 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
49 |
lemma in_rep_update: |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
50 |
"\<lbrakk> s : \<gamma>\<^isub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>f(update S x a)" |
45111 | 51 |
by(simp add: rep_st_def lookup_update) |
52 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
53 |
text{* The soundness proofs are textually identical to the ones for the step |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
54 |
function operating on states as functions. *} |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
55 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
56 |
lemma step_preserves_le2: |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
57 |
"\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c; strip ca = c \<rbrakk> |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
58 |
\<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c (step sa ca)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
59 |
proof(induction c arbitrary: cs ca S sa) |
45111 | 60 |
case SKIP thus ?case |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
61 |
by(auto simp:strip_eq_SKIP) |
45111 | 62 |
next |
63 |
case Assign thus ?case |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
64 |
by (fastforce simp: strip_eq_Assign intro: aval'_sound in_rep_update |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
65 |
split: option.splits del:subsetD) |
45111 | 66 |
next |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
67 |
case Semi thus ?case apply (auto simp: strip_eq_Semi) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
68 |
by (metis le_post post_map_acom) |
45111 | 69 |
next |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
70 |
case (If b c1 c2) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
71 |
then obtain cs1 cs2 ca1 ca2 P Pa where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
72 |
"cs = IF b THEN cs1 ELSE cs2 {P}" "ca = IF b THEN ca1 ELSE ca2 {Pa}" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
73 |
"P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
74 |
"strip cs1 = c1" "strip ca1 = c1" "strip cs2 = c2" "strip ca2 = c2" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
75 |
by (fastforce simp: strip_eq_If) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
76 |
moreover have "post cs1 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
77 |
by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_rep_u order_trans post_map_acom) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
78 |
moreover have "post cs2 \<subseteq> \<gamma>\<^isub>u(post ca1 \<squnion> post ca2)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
79 |
by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_rep_u order_trans post_map_acom) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
80 |
ultimately show ?case using If.prems(1) by (simp add: If.IH subset_iff) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
81 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
82 |
case (While b c1) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
83 |
then obtain cs1 ca1 I P Ia Pa where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
84 |
"cs = {I} WHILE b DO cs1 {P}" "ca = {Ia} WHILE b DO ca1 {Pa}" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
85 |
"I \<subseteq> \<gamma>\<^isub>u Ia" "P \<subseteq> \<gamma>\<^isub>u Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
86 |
"strip cs1 = c1" "strip ca1 = c1" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
87 |
by (fastforce simp: strip_eq_While) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
88 |
moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>u (sa \<squnion> post ca1)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
89 |
using `S \<subseteq> \<gamma>\<^isub>u sa` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified] |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
90 |
by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_rep_u order_trans) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
91 |
ultimately show ?case by (simp add: While.IH subset_iff) |
45111 | 92 |
qed |
93 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
94 |
lemma step_preserves_le: |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
95 |
"\<lbrakk> S \<subseteq> \<gamma>\<^isub>u sa; cs \<le> \<gamma>\<^isub>c ca; strip cs = c \<rbrakk> |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
96 |
\<Longrightarrow> step_cs S cs \<le> \<gamma>\<^isub>c(step sa ca)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
97 |
by (metis le_strip step_preserves_le2 strip_acom) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
98 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
99 |
lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS UNIV c \<le> \<gamma>\<^isub>c c'" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
100 |
proof(simp add: CS_def AI_def) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
101 |
assume 1: "lpfp\<^isub>c (step \<top>) c = Some c'" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
102 |
have 2: "step \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1]) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
103 |
have 3: "strip (\<gamma>\<^isub>c (step \<top> c')) = c" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
104 |
by(simp add: strip_lpfpc[OF _ 1]) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
105 |
have "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c (step \<top> c')" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
106 |
proof(rule lfp_lowerbound[OF 3]) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
107 |
show "step_cs UNIV (\<gamma>\<^isub>c (step \<top> c')) \<le> \<gamma>\<^isub>c (step \<top> c')" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
108 |
proof(rule step_preserves_le[OF _ _ 3]) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
109 |
show "UNIV \<subseteq> \<gamma>\<^isub>u \<top>" by simp |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
110 |
show "\<gamma>\<^isub>c (step \<top> c') \<le> \<gamma>\<^isub>c c'" by(rule mono_rep_c[OF 2]) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
111 |
qed |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
112 |
qed |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
113 |
from this 2 show "lfp c (step_cs UNIV) \<le> \<gamma>\<^isub>c c'" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
114 |
by (blast intro: mono_rep_c order_trans) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
115 |
qed |
45111 | 116 |
|
117 |
end |
|
118 |
||
119 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
120 |
subsubsection "Monotonicity" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
121 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
122 |
locale Abs_Int_mono = Abs_Int + |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
123 |
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
|
124 |
begin |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
125 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
126 |
lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
127 |
by(induction e) (auto simp: le_st_def lookup_def mono_plus') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
128 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
129 |
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
130 |
by(auto simp add: le_st_def lookup_def update_def) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
131 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
132 |
lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
133 |
apply(induction c arbitrary: S S') |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45127
diff
changeset
|
134 |
apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: option.split) |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
135 |
done |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
136 |
|
45111 | 137 |
end |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
138 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45111
diff
changeset
|
139 |
end |