author | nipkow |
Mon, 03 Sep 2012 15:41:06 +0200 | |
changeset 49095 | 7df19036392e |
parent 47818 | 151d137f1095 |
child 49138 | 53f954510a8c |
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 |
|
46225 | 10 |
subsection "Annotated Commands" |
45623
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 = |
47818 | 13 |
SKIP 'a ("SKIP {_}" 61) | |
14 |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | |
|
15 |
Seq "('a acom)" "('a acom)" ("_;//_" [60, 61] 60) | |
|
49095 | 16 |
If bexp 'a "('a acom)" 'a "('a acom)" 'a |
17 |
("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})" [0, 0, 0, 61, 0, 0] 61) | |
|
18 |
While 'a bexp 'a "('a acom)" 'a |
|
19 |
("({_}//WHILE _/ DO ({_}/ _)//{_})" [0, 0, 0, 61, 0] 61) |
|
45623
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" | |
49095 | 25 |
"post (IF b THEN {P1} c1 ELSE {P2} c2 {P}) = P" | |
26 |
"post ({Inv} WHILE b DO {Pc} c {P}) = P" |
|
45623
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)" | |
49095 | 32 |
"strip (IF b THEN {P1} c1 ELSE {P2} c2 {P}) = (IF b THEN strip c1 ELSE strip c2)" | |
33 |
"strip ({Inv} WHILE b DO {Pc} 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) = |
49095 | 40 |
(IF b THEN {a} anno a c1 ELSE {a} anno a c2 {a})" | |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
41 |
"anno a (WHILE b DO c) = |
49095 | 42 |
({a} WHILE b DO {a} anno a c {a})" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
43 |
|
47613 | 44 |
fun annos :: "'a acom \<Rightarrow> 'a list" where |
45 |
"annos (SKIP {a}) = [a]" | |
|
46 |
"annos (x::=e {a}) = [a]" | |
|
47 |
"annos (C1;C2) = annos C1 @ annos C2" | |
|
49095 | 48 |
"annos (IF b THEN {a1} C1 ELSE {a2} C2 {a}) = a1 # a2 #a # annos C1 @ annos C2" | |
49 |
"annos ({i} WHILE b DO {ac} C {a}) = i # ac # a # annos C" |
|
47613 | 50 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
51 |
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where |
45746 | 52 |
"map_acom f (SKIP {P}) = SKIP {f P}" | |
53 |
"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
|
54 |
"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" | |
49095 | 55 |
"map_acom f (IF b THEN {p1} c1 ELSE {p2} c2 {P}) = |
56 |
(IF b THEN {f p1} map_acom f c1 ELSE {f p2} map_acom f c2 {f P})" | |
|
57 |
"map_acom f ({Inv} WHILE b DO {p} c {P}) = |
|
58 |
({f Inv} WHILE b DO {f p} map_acom f c {f P})" |
|
45623
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 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
|
62 |
by (induction 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_acom[simp]: "strip (map_acom f c) = strip c" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
65 |
by (induction c) auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
66 |
|
46068 | 67 |
lemma map_acom_SKIP: |
68 |
"map_acom f c = SKIP {S'} \<longleftrightarrow> (\<exists>S. c = SKIP {S} \<and> S' = f S)" |
|
69 |
by (cases c) auto |
|
70 |
||
71 |
lemma map_acom_Assign: |
|
72 |
"map_acom f c = x ::= e {S'} \<longleftrightarrow> (\<exists>S. c = x::=e {S} \<and> S' = f S)" |
|
73 |
by (cases c) auto |
|
74 |
||
47818 | 75 |
lemma map_acom_Seq: |
46068 | 76 |
"map_acom f c = c1';c2' \<longleftrightarrow> |
77 |
(\<exists>c1 c2. c = c1;c2 \<and> map_acom f c1 = c1' \<and> map_acom f c2 = c2')" |
|
78 |
by (cases c) auto |
|
79 |
||
80 |
lemma map_acom_If: |
|
49095 | 81 |
"map_acom f c = IF b THEN {p1'} c1' ELSE {p2'} c2' {S'} \<longleftrightarrow> |
82 |
(\<exists>S p1 p2 c1 c2. c = IF b THEN {p1} c1 ELSE {p2} c2 {S} \<and> |
|
83 |
map_acom f c1 = c1' \<and> map_acom f c2 = c2' \<and> p1' = f p1 \<and> p2' = f p2 \<and> S' = f S)" |
|
46068 | 84 |
by (cases c) auto |
85 |
||
86 |
lemma map_acom_While: |
|
49095 | 87 |
"map_acom f w = {I'} WHILE b DO {p'} c' {P'} \<longleftrightarrow> |
88 |
(\<exists>I p P c. w = {I} WHILE b DO {p} c {P} \<and> map_acom f c = c' \<and> I' = f I \<and> p' = f p \<and> P' = f P)" |
|
46068 | 89 |
by (cases w) auto |
90 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
91 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
92 |
lemma strip_anno[simp]: "strip (anno a c) = c" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
93 |
by(induct c) simp_all |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
94 |
|
46157 | 95 |
lemma strip_eq_SKIP: |
49095 | 96 |
"strip C = com.SKIP \<longleftrightarrow> (EX P. C = SKIP {P})" |
97 |
by (cases C) simp_all |
|
46157 | 98 |
|
99 |
lemma strip_eq_Assign: |
|
49095 | 100 |
"strip C = x::=e \<longleftrightarrow> (EX P. C = x::=e {P})" |
101 |
by (cases C) simp_all |
|
46157 | 102 |
|
47818 | 103 |
lemma strip_eq_Seq: |
49095 | 104 |
"strip C = c1;c2 \<longleftrightarrow> (EX C1 C2. C = C1;C2 & strip C1 = c1 & strip C2 = c2)" |
105 |
by (cases C) simp_all |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
106 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
107 |
lemma strip_eq_If: |
49095 | 108 |
"strip C = IF b THEN c1 ELSE c2 \<longleftrightarrow> |
109 |
(EX p1 p2 C1 C2 P. C = IF b THEN {p1} C1 ELSE {p2} C2 {P} & strip C1 = c1 & strip C2 = c2)" |
|
110 |
by (cases C) simp_all |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
111 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
112 |
lemma strip_eq_While: |
49095 | 113 |
"strip C = WHILE b DO c1 \<longleftrightarrow> |
114 |
(EX I p C1 P. C = {I} WHILE b DO {p} C1 {P} & strip C1 = c1)" |
|
115 |
by (cases C) simp_all |
|
47613 | 116 |
|
117 |
lemma set_annos_anno[simp]: "set (annos (anno a C)) = {a}" |
|
118 |
by(induction C)(auto) |
|
119 |
||
120 |
lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)" |
|
121 |
apply(induct C2 arbitrary: C1) |
|
47818 | 122 |
apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Seq strip_eq_If strip_eq_While) |
47613 | 123 |
done |
124 |
||
125 |
lemmas size_annos_same2 = eqTrueI[OF size_annos_same] |
|
126 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
127 |
end |