author | nipkow |
Sun, 04 Dec 2011 18:29:16 +0100 | |
changeset 45746 | 579fb74aa409 |
parent 45623 | f682f3f7b726 |
child 45751 | f8723843c29e |
permissions | -rw-r--r-- |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
1 |
(* Author: Tobias Nipkow *) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
2 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
3 |
theory ACom |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
4 |
imports Com |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
5 |
begin |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
6 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
7 |
(* is there a better place? *) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
8 |
definition "show_state xs s = [(x,s x). x \<leftarrow> xs]" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
9 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
10 |
section "Annotated Commands" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
11 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
12 |
datatype 'a acom = |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
13 |
SKIP 'a ("SKIP {_}") | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
14 |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
15 |
Semi "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
16 |
If bexp "('a acom)" "('a acom)" 'a |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
17 |
("(IF _/ THEN _/ ELSE _//{_})" [0, 0, 61, 0] 61) | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
18 |
While 'a bexp "('a acom)" 'a |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
19 |
("({_}//WHILE _/ DO (_)//{_})" [0, 0, 61, 0] 61) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
20 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
21 |
fun post :: "'a acom \<Rightarrow>'a" where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
22 |
"post (SKIP {P}) = P" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
23 |
"post (x ::= e {P}) = P" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
24 |
"post (c1; c2) = post c2" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
25 |
"post (IF b THEN c1 ELSE c2 {P}) = P" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
26 |
"post ({Inv} WHILE b DO c {P}) = P" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
27 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
28 |
fun strip :: "'a acom \<Rightarrow> com" where |
45746 | 29 |
"strip (SKIP {P}) = com.SKIP" | |
30 |
"strip (x ::= e {P}) = (x ::= e)" | |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
31 |
"strip (c1;c2) = (strip c1; strip c2)" | |
45746 | 32 |
"strip (IF b THEN c1 ELSE c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" | |
33 |
"strip ({Inv} WHILE b DO c {P}) = (WHILE b DO strip c)" |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
34 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
35 |
fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
36 |
"anno a com.SKIP = SKIP {a}" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
37 |
"anno a (x ::= e) = (x ::= e {a})" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
38 |
"anno a (c1;c2) = (anno a c1; anno a c2)" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
39 |
"anno a (IF b THEN c1 ELSE c2) = |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
40 |
(IF b THEN anno a c1 ELSE anno a c2 {a})" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
41 |
"anno a (WHILE b DO c) = |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
42 |
({a} WHILE b DO anno a c {a})" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
43 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
44 |
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where |
45746 | 45 |
"map_acom f (SKIP {P}) = SKIP {f P}" | |
46 |
"map_acom f (x ::= e {P}) = (x ::= e {f P})" | |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
47 |
"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" | |
45746 | 48 |
"map_acom f (IF b THEN c1 ELSE c2 {P}) = |
49 |
(IF b THEN map_acom f c1 ELSE map_acom f c2 {f P})" | |
|
50 |
"map_acom f ({Inv} WHILE b DO c {P}) = |
|
51 |
({f Inv} WHILE b DO map_acom f c {f P})" |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
52 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
53 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
54 |
lemma post_map_acom[simp]: "post(map_acom f c) = f(post c)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
55 |
by (induction c) simp_all |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
56 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
57 |
lemma strip_acom[simp]: "strip (map_acom f c) = strip c" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
58 |
by (induction c) auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
59 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
60 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
61 |
lemma strip_anno[simp]: "strip (anno a c) = c" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
62 |
by(induct c) simp_all |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
63 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
64 |
lemma strip_eq_SKIP: "strip c = com.SKIP \<longleftrightarrow> (EX P. c = SKIP {P})" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
65 |
by (cases c) simp_all |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
66 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
67 |
lemma strip_eq_Assign: "strip c = x::=e \<longleftrightarrow> (EX P. c = x::=e {P})" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
68 |
by (cases c) simp_all |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
69 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
70 |
lemma strip_eq_Semi: |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
71 |
"strip c = c1;c2 \<longleftrightarrow> (EX d1 d2. c = d1;d2 & strip d1 = c1 & strip d2 = c2)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
72 |
by (cases c) simp_all |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
73 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
74 |
lemma strip_eq_If: |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
75 |
"strip c = IF b THEN c1 ELSE c2 \<longleftrightarrow> |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
76 |
(EX d1 d2 P. c = IF b THEN d1 ELSE d2 {P} & strip d1 = c1 & strip d2 = c2)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
77 |
by (cases c) simp_all |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
78 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
79 |
lemma strip_eq_While: |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
80 |
"strip c = WHILE b DO c1 \<longleftrightarrow> |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
81 |
(EX I d1 P. c = {I} WHILE b DO d1 {P} & strip d1 = c1)" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
82 |
by (cases c) simp_all |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
83 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
84 |
end |