author | huffman |
Mon, 12 Sep 2011 09:21:01 -0700 | |
changeset 44902 | 9ba11d41cd1f |
parent 44890 | 22f665a2e91c |
child 44923 | b80108b346a9 |
permissions | -rw-r--r-- |
44656 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory AbsInt0 |
|
4 |
imports Astate |
|
5 |
begin |
|
6 |
||
7 |
subsection "Computable Abstract Interpretation" |
|
8 |
||
9 |
text{* Abstract interpretation over type @{text astate} instead of |
|
10 |
functions. *} |
|
11 |
||
12 |
locale Abs_Int = Val_abs |
|
13 |
begin |
|
14 |
||
15 |
fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" ("aval\<^isup>#") where |
|
16 |
"aval' (N n) _ = num' n" | |
|
17 |
"aval' (V x) S = lookup S x" | |
|
18 |
"aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)" |
|
19 |
||
20 |
abbreviation astate_in_rep (infix "<:" 50) where |
|
21 |
"s <: S == ALL x. s x <: lookup S x" |
|
22 |
||
23 |
lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T" |
|
24 |
by (metis in_mono le_astate_def le_rep lookup_def top) |
|
25 |
||
26 |
lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S" |
|
27 |
by (induct a) (auto simp: rep_num' rep_plus') |
|
28 |
||
29 |
||
30 |
fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where |
|
31 |
"AI SKIP S = S" | |
|
32 |
"AI (x ::= a) S = update S x (aval' a S)" | |
|
33 |
"AI (c1;c2) S = AI c2 (AI c1 S)" | |
|
34 |
"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" | |
|
35 |
"AI (WHILE b DO c) S = pfp_above (AI c) S" |
|
36 |
||
37 |
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0" |
|
38 |
proof(induct c arbitrary: s t S0) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44656
diff
changeset
|
39 |
case SKIP thus ?case by fastforce |
44656 | 40 |
next |
41 |
case Assign thus ?case |
|
42 |
by (auto simp: lookup_update aval'_sound) |
|
43 |
next |
|
44 |
case Semi thus ?case by auto |
|
45 |
next |
|
46 |
case If thus ?case |
|
47 |
by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2) |
|
48 |
next |
|
49 |
case (While b c) |
|
50 |
let ?P = "pfp_above (AI c) S0" |
|
51 |
have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P" |
|
52 |
by(simp_all add: SL_top_class.pfp_above_pfp) |
|
53 |
{ fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P" |
|
54 |
proof(induct "WHILE b DO c" s t rule: big_step_induct) |
|
55 |
case WhileFalse thus ?case by simp |
|
56 |
next |
|
57 |
case WhileTrue thus ?case using While.hyps pfp astate_in_rep_le by metis |
|
58 |
qed |
|
59 |
} |
|
60 |
with astate_in_rep_le[OF `s <: S0` `S0 \<sqsubseteq> ?P`] |
|
61 |
show ?case by (metis While(2) AI.simps(5)) |
|
62 |
qed |
|
63 |
||
64 |
end |
|
65 |
||
66 |
end |