author | wenzelm |
Tue, 13 Aug 2013 16:25:47 +0200 | |
changeset 53015 | a1119cf551e8 |
parent 52046 | bc01725d7918 |
child 54941 | 6d99745afe34 |
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 |
|
46225 | 7 |
subsection "Annotated Commands" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
8 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
9 |
datatype 'a acom = |
47818 | 10 |
SKIP 'a ("SKIP {_}" 61) | |
11 |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) | |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
52019
diff
changeset
|
12 |
Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) | |
49095 | 13 |
If bexp 'a "('a acom)" 'a "('a acom)" 'a |
14 |
("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})" [0, 0, 0, 61, 0, 0] 61) | |
|
15 |
While 'a bexp 'a "('a acom)" 'a |
|
49138 | 16 |
("({_}//WHILE _//DO ({_}//_)//{_})" [0, 0, 0, 61, 0] 61) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
17 |
|
49603 | 18 |
text_raw{*\snip{stripdef}{1}{1}{% *} |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
19 |
fun strip :: "'a acom \<Rightarrow> com" where |
45746 | 20 |
"strip (SKIP {P}) = com.SKIP" | |
49603 | 21 |
"strip (x ::= e {P}) = x ::= e" | |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
22 |
"strip (C\<^sub>1;;C\<^sub>2) = strip C\<^sub>1;; strip C\<^sub>2" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
23 |
"strip (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {P}) = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
24 |
IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2" | |
49603 | 25 |
"strip ({I} WHILE b DO {P} C {Q}) = WHILE b DO strip C" |
26 |
text_raw{*}%endsnip*} |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
27 |
|
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
28 |
text_raw{*\snip{asizedef}{1}{1}{% *} |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
29 |
fun asize :: "com \<Rightarrow> nat" where |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
30 |
"asize com.SKIP = 1" | |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
31 |
"asize (x ::= e) = 1" | |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
32 |
"asize (C\<^sub>1;;C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
33 |
"asize (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2 + 3" | |
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
34 |
"asize (WHILE b DO C) = asize C + 3" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
35 |
text_raw{*}%endsnip*} |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
36 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
37 |
text_raw{*\snip{annotatedef}{1}{1}{% *} |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
38 |
definition shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
39 |
"shift f n = (\<lambda>p. f(p+n))" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
40 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
41 |
fun annotate :: "(nat \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom" where |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
42 |
"annotate f com.SKIP = SKIP {f 0}" | |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
43 |
"annotate f (x ::= e) = x ::= e {f 0}" | |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
44 |
"annotate f (c\<^sub>1;;c\<^sub>2) = annotate f c\<^sub>1;; annotate (shift f (asize c\<^sub>1)) c\<^sub>2" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
45 |
"annotate f (IF b THEN c\<^sub>1 ELSE c\<^sub>2) = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
46 |
IF b THEN {f 0} annotate (shift f 1) c\<^sub>1 |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
47 |
ELSE {f(asize c\<^sub>1 + 1)} annotate (shift f (asize c\<^sub>1 + 2)) c\<^sub>2 |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
48 |
{f(asize c\<^sub>1 + asize c\<^sub>2 + 2)}" | |
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
49 |
"annotate f (WHILE b DO c) = |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
50 |
{f 0} WHILE b DO {f 1} annotate (shift f 2) c {f(asize c + 2)}" |
49603 | 51 |
text_raw{*}%endsnip*} |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
52 |
|
49603 | 53 |
text_raw{*\snip{annosdef}{1}{1}{% *} |
47613 | 54 |
fun annos :: "'a acom \<Rightarrow> 'a list" where |
49603 | 55 |
"annos (SKIP {P}) = [P]" | |
56 |
"annos (x ::= e {P}) = [P]" | |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
57 |
"annos (C\<^sub>1;;C\<^sub>2) = annos C\<^sub>1 @ annos C\<^sub>2" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
58 |
"annos (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {Q}) = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
59 |
P\<^sub>1 # annos C\<^sub>1 @ P\<^sub>2 # annos C\<^sub>2 @ [Q]" | |
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
60 |
"annos ({I} WHILE b DO {P} C {Q}) = I # P # annos C @ [Q]" |
49603 | 61 |
text_raw{*}%endsnip*} |
47613 | 62 |
|
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
63 |
definition anno :: "'a acom \<Rightarrow> nat \<Rightarrow> 'a" where |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
64 |
"anno C p = annos C ! p" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
65 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
66 |
definition post :: "'a acom \<Rightarrow>'a" where |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
67 |
"post C = last(annos C)" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
68 |
|
49603 | 69 |
text_raw{*\snip{mapacomdef}{1}{2}{% *} |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
70 |
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where |
45746 | 71 |
"map_acom f (SKIP {P}) = SKIP {f P}" | |
49603 | 72 |
"map_acom f (x ::= e {P}) = x ::= e {f P}" | |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
73 |
"map_acom f (C\<^sub>1;;C\<^sub>2) = map_acom f C\<^sub>1;; map_acom f C\<^sub>2" | |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
74 |
"map_acom f (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {Q}) = |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
75 |
IF b THEN {f P\<^sub>1} map_acom f C\<^sub>1 ELSE {f P\<^sub>2} map_acom f C\<^sub>2 |
49603 | 76 |
{f Q}" | |
77 |
"map_acom f ({I} WHILE b DO {P} C {Q}) = |
|
78 |
{f I} WHILE b DO {f P} map_acom f C {f Q}" |
|
79 |
text_raw{*}%endsnip*} |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
80 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
81 |
|
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
82 |
lemma annos_ne: "annos C \<noteq> []" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
83 |
by(induction C) auto |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
84 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
85 |
lemma strip_annotate[simp]: "strip(annotate f c) = c" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
86 |
by(induction c arbitrary: f) auto |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
87 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
88 |
lemma length_annos_annotate[simp]: "length (annos (annotate f c)) = asize c" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
89 |
by(induction c arbitrary: f) auto |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
90 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
91 |
lemma size_annos: "size(annos C) = asize(strip C)" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
92 |
by(induction C)(auto) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
93 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
94 |
lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
95 |
apply(induct C2 arbitrary: C1) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
96 |
apply(case_tac C1, simp_all)+ |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
97 |
done |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
98 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
99 |
lemmas size_annos_same2 = eqTrueI[OF size_annos_same] |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
100 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
101 |
lemma anno_annotate[simp]: "p < asize c \<Longrightarrow> anno (annotate f c) p = f p" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
102 |
apply(induction c arbitrary: f p) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
103 |
apply (auto simp: anno_def nth_append nth_Cons numeral_eq_Suc shift_def |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
104 |
split: nat.split) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
105 |
apply (metis add_Suc_right add_diff_inverse nat_add_commute) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
106 |
apply(rule_tac f=f in arg_cong) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
107 |
apply arith |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
108 |
apply (metis less_Suc_eq) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
109 |
done |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
110 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
111 |
lemma eq_acom_iff_strip_annos: |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
112 |
"C1 = C2 \<longleftrightarrow> strip C1 = strip C2 \<and> annos C1 = annos C2" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
113 |
apply(induction C1 arbitrary: C2) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
114 |
apply(case_tac C2, auto simp: size_annos_same2)+ |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
115 |
done |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
116 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
117 |
lemma eq_acom_iff_strip_anno: |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
118 |
"C1=C2 \<longleftrightarrow> strip C1 = strip C2 \<and> (\<forall>p<size(annos C1). anno C1 p = anno C2 p)" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
119 |
by(auto simp add: eq_acom_iff_strip_annos anno_def |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
120 |
list_eq_iff_nth_eq size_annos_same2) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
121 |
|
49477 | 122 |
lemma post_map_acom[simp]: "post(map_acom f C) = f(post C)" |
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
123 |
by (induction C) (auto simp: post_def last_append annos_ne) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
124 |
|
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
125 |
lemma strip_map_acom[simp]: "strip (map_acom f C) = strip C" |
49477 | 126 |
by (induction C) auto |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
127 |
|
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
128 |
lemma anno_map_acom: "p < size(annos C) \<Longrightarrow> anno (map_acom f C) p = f(anno C p)" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
129 |
apply(induction C arbitrary: p) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
130 |
apply(auto simp: anno_def nth_append nth_Cons' size_annos) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
131 |
done |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
132 |
|
46157 | 133 |
lemma strip_eq_SKIP: |
49095 | 134 |
"strip C = com.SKIP \<longleftrightarrow> (EX P. C = SKIP {P})" |
135 |
by (cases C) simp_all |
|
46157 | 136 |
|
137 |
lemma strip_eq_Assign: |
|
49095 | 138 |
"strip C = x::=e \<longleftrightarrow> (EX P. C = x::=e {P})" |
139 |
by (cases C) simp_all |
|
46157 | 140 |
|
47818 | 141 |
lemma strip_eq_Seq: |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
52019
diff
changeset
|
142 |
"strip C = c1;;c2 \<longleftrightarrow> (EX C1 C2. C = C1;;C2 & strip C1 = c1 & strip C2 = c2)" |
49095 | 143 |
by (cases C) simp_all |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
144 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
145 |
lemma strip_eq_If: |
49095 | 146 |
"strip C = IF b THEN c1 ELSE c2 \<longleftrightarrow> |
49477 | 147 |
(EX P1 P2 C1 C2 Q. C = IF b THEN {P1} C1 ELSE {P2} C2 {Q} & strip C1 = c1 & strip C2 = c2)" |
49095 | 148 |
by (cases C) simp_all |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
149 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
150 |
lemma strip_eq_While: |
49095 | 151 |
"strip C = WHILE b DO c1 \<longleftrightarrow> |
49477 | 152 |
(EX I P C1 Q. C = {I} WHILE b DO {P} C1 {Q} & strip C1 = c1)" |
49095 | 153 |
by (cases C) simp_all |
47613 | 154 |
|
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
155 |
lemma [simp]: "shift (\<lambda>p. a) n = (\<lambda>p. a)" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
156 |
by(simp add:shift_def) |
47613 | 157 |
|
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
158 |
lemma set_annos_anno[simp]: "set (annos (annotate (\<lambda>p. a) c)) = {a}" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
159 |
by(induction c) simp_all |
47613 | 160 |
|
51712 | 161 |
lemma post_in_annos: "post C \<in> set(annos C)" |
52019
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
162 |
by(auto simp: post_def annos_ne) |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
163 |
|
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
164 |
lemma post_anno_asize: "post C = anno C (size(annos C) - 1)" |
a4cbca8f7342
finally: acom with pointwise access and update of annotations
nipkow
parents:
51712
diff
changeset
|
165 |
by(simp add: post_def last_conv_nth[OF annos_ne] anno_def) |
51712 | 166 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
167 |
end |