author | nipkow |
Thu, 27 Sep 2012 10:20:38 +0200 | |
changeset 49603 | a115dda10251 |
parent 49477 | f1f2a03e8669 |
child 50986 | c54ea7f5418f |
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 |
|
49138 | 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 |
|
49603 | 21 |
text_raw{*\snip{postdef}{2}{1}{% *} |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
22 |
fun post :: "'a acom \<Rightarrow>'a" where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
23 |
"post (SKIP {P}) = P" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
24 |
"post (x ::= e {P}) = P" | |
49603 | 25 |
"post (C\<^isub>1; C\<^isub>2) = post C\<^isub>2" | |
26 |
"post (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = Q" | |
|
27 |
"post ({I} WHILE b DO {P} C {Q}) = Q" |
|
28 |
text_raw{*}%endsnip*} |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
29 |
|
49603 | 30 |
text_raw{*\snip{stripdef}{1}{1}{% *} |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
31 |
fun strip :: "'a acom \<Rightarrow> com" where |
45746 | 32 |
"strip (SKIP {P}) = com.SKIP" | |
49603 | 33 |
"strip (x ::= e {P}) = x ::= e" | |
34 |
"strip (C\<^isub>1;C\<^isub>2) = strip C\<^isub>1; strip C\<^isub>2" | |
|
35 |
"strip (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {P}) = |
|
36 |
IF b THEN strip C\<^isub>1 ELSE strip C\<^isub>2" | |
|
37 |
"strip ({I} WHILE b DO {P} C {Q}) = WHILE b DO strip C" |
|
38 |
text_raw{*}%endsnip*} |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
39 |
|
49603 | 40 |
text_raw{*\snip{annodef}{1}{1}{% *} |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
41 |
fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where |
49603 | 42 |
"anno A com.SKIP = SKIP {A}" | |
43 |
"anno A (x ::= e) = x ::= e {A}" | |
|
44 |
"anno A (c\<^isub>1;c\<^isub>2) = anno A c\<^isub>1; anno A c\<^isub>2" | |
|
45 |
"anno A (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = |
|
46 |
IF b THEN {A} anno A c\<^isub>1 ELSE {A} anno A c\<^isub>2 {A}" | |
|
47 |
"anno A (WHILE b DO c) = |
|
48 |
{A} WHILE b DO {A} anno A c {A}" |
|
49 |
text_raw{*}%endsnip*} |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
50 |
|
49603 | 51 |
text_raw{*\snip{annosdef}{1}{1}{% *} |
47613 | 52 |
fun annos :: "'a acom \<Rightarrow> 'a list" where |
49603 | 53 |
"annos (SKIP {P}) = [P]" | |
54 |
"annos (x ::= e {P}) = [P]" | |
|
55 |
"annos (C\<^isub>1;C\<^isub>2) = annos C\<^isub>1 @ annos C\<^isub>2" | |
|
56 |
"annos (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = |
|
57 |
P\<^isub>1 # P\<^isub>2 # Q # annos C\<^isub>1 @ annos C\<^isub>2" | |
|
58 |
"annos ({I} WHILE b DO {P} C {Q}) = I # P # Q # annos C" |
|
59 |
text_raw{*}%endsnip*} |
|
47613 | 60 |
|
49603 | 61 |
text_raw{*\snip{mapacomdef}{1}{2}{% *} |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
62 |
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where |
45746 | 63 |
"map_acom f (SKIP {P}) = SKIP {f P}" | |
49603 | 64 |
"map_acom f (x ::= e {P}) = x ::= e {f P}" | |
65 |
"map_acom f (C\<^isub>1;C\<^isub>2) = map_acom f C\<^isub>1; map_acom f C\<^isub>2" | |
|
66 |
"map_acom f (IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = |
|
67 |
IF b THEN {f P\<^isub>1} map_acom f C\<^isub>1 ELSE {f P\<^isub>2} map_acom f C\<^isub>2 |
|
68 |
{f Q}" | |
|
69 |
"map_acom f ({I} WHILE b DO {P} C {Q}) = |
|
70 |
{f I} WHILE b DO {f P} map_acom f C {f Q}" |
|
71 |
text_raw{*}%endsnip*} |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
72 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
73 |
|
49477 | 74 |
lemma post_map_acom[simp]: "post(map_acom f C) = f(post C)" |
75 |
by (induction C) simp_all |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
76 |
|
49477 | 77 |
lemma strip_acom[simp]: "strip (map_acom f C) = strip C" |
78 |
by (induction C) auto |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
79 |
|
46068 | 80 |
lemma map_acom_SKIP: |
49477 | 81 |
"map_acom f C = SKIP {S'} \<longleftrightarrow> (\<exists>S. C = SKIP {S} \<and> S' = f S)" |
82 |
by (cases C) auto |
|
46068 | 83 |
|
84 |
lemma map_acom_Assign: |
|
49477 | 85 |
"map_acom f C = x ::= e {S'} \<longleftrightarrow> (\<exists>S. C = x::=e {S} \<and> S' = f S)" |
86 |
by (cases C) auto |
|
46068 | 87 |
|
47818 | 88 |
lemma map_acom_Seq: |
49477 | 89 |
"map_acom f C = C1';C2' \<longleftrightarrow> |
90 |
(\<exists>C1 C2. C = C1;C2 \<and> map_acom f C1 = C1' \<and> map_acom f C2 = C2')" |
|
91 |
by (cases C) auto |
|
46068 | 92 |
|
93 |
lemma map_acom_If: |
|
49477 | 94 |
"map_acom f C = IF b THEN {P1'} C1' ELSE {P2'} C2' {Q'} \<longleftrightarrow> |
95 |
(\<exists>P1 P2 C1 C2 Q. C = IF b THEN {P1} C1 ELSE {P2} C2 {Q} \<and> |
|
96 |
map_acom f C1 = C1' \<and> map_acom f C2 = C2' \<and> P1' = f P1 \<and> P2' = f P2 \<and> Q' = f Q)" |
|
97 |
by (cases C) auto |
|
46068 | 98 |
|
99 |
lemma map_acom_While: |
|
49477 | 100 |
"map_acom f w = {I'} WHILE b DO {p'} C' {P'} \<longleftrightarrow> |
101 |
(\<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 | 102 |
by (cases w) auto |
103 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
104 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
105 |
lemma strip_anno[simp]: "strip (anno a c) = c" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
106 |
by(induct c) simp_all |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
107 |
|
46157 | 108 |
lemma strip_eq_SKIP: |
49095 | 109 |
"strip C = com.SKIP \<longleftrightarrow> (EX P. C = SKIP {P})" |
110 |
by (cases C) simp_all |
|
46157 | 111 |
|
112 |
lemma strip_eq_Assign: |
|
49095 | 113 |
"strip C = x::=e \<longleftrightarrow> (EX P. C = x::=e {P})" |
114 |
by (cases C) simp_all |
|
46157 | 115 |
|
47818 | 116 |
lemma strip_eq_Seq: |
49095 | 117 |
"strip C = c1;c2 \<longleftrightarrow> (EX C1 C2. C = C1;C2 & strip C1 = c1 & strip C2 = c2)" |
118 |
by (cases C) simp_all |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
119 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
120 |
lemma strip_eq_If: |
49095 | 121 |
"strip C = IF b THEN c1 ELSE c2 \<longleftrightarrow> |
49477 | 122 |
(EX P1 P2 C1 C2 Q. C = IF b THEN {P1} C1 ELSE {P2} C2 {Q} & strip C1 = c1 & strip C2 = c2)" |
49095 | 123 |
by (cases C) simp_all |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
124 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
125 |
lemma strip_eq_While: |
49095 | 126 |
"strip C = WHILE b DO c1 \<longleftrightarrow> |
49477 | 127 |
(EX I P C1 Q. C = {I} WHILE b DO {P} C1 {Q} & strip C1 = c1)" |
49095 | 128 |
by (cases C) simp_all |
47613 | 129 |
|
49477 | 130 |
lemma set_annos_anno[simp]: "set (annos (anno a c)) = {a}" |
131 |
by(induction c)(auto) |
|
47613 | 132 |
|
133 |
lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)" |
|
134 |
apply(induct C2 arbitrary: C1) |
|
47818 | 135 |
apply (auto simp: strip_eq_SKIP strip_eq_Assign strip_eq_Seq strip_eq_If strip_eq_While) |
47613 | 136 |
done |
137 |
||
138 |
lemmas size_annos_same2 = eqTrueI[OF size_annos_same] |
|
139 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
140 |
end |