author | nipkow |
Sun, 07 Apr 2013 10:06:37 +0200 | |
changeset 51629 | f0b375b69292 |
parent 51610 | d1e192124cd6 |
child 51630 | 603436283686 |
permissions | -rw-r--r-- |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
1 |
theory Collecting |
49487 | 2 |
imports Complete_Lattice Big_Step ACom |
51389 | 3 |
"~~/src/HOL/ex/Interpretation_with_Defs" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
4 |
begin |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
5 |
|
51389 | 6 |
subsection "The generic Step function" |
7 |
||
8 |
notation |
|
9 |
sup (infixl "\<squnion>" 65) and |
|
10 |
inf (infixl "\<sqinter>" 70) and |
|
11 |
bot ("\<bottom>") and |
|
12 |
top ("\<top>") |
|
13 |
||
51390 | 14 |
fun Step :: "(vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup) \<Rightarrow> (bexp \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where |
15 |
"Step f g S (SKIP {Q}) = (SKIP {S})" | |
|
16 |
"Step f g S (x ::= e {Q}) = |
|
17 |
x ::= e {f x e S}" | |
|
18 |
"Step f g S (C1; C2) = Step f g S C1; Step f g (post C1) C2" | |
|
19 |
"Step f g S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) = |
|
20 |
IF b THEN {g b S} Step f g P1 C1 ELSE {g (Not b) S} Step f g P2 C2 |
|
21 |
{post C1 \<squnion> post C2}" | |
|
22 |
"Step f g S ({I} WHILE b DO {P} C {Q}) = |
|
23 |
{S \<squnion> post C} WHILE b DO {g b I} Step f g P C {g (Not b) I}" |
|
51389 | 24 |
|
51390 | 25 |
(* Could hide f and g like this: |
26 |
consts fa :: "vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup" |
|
27 |
fb :: "bexp \<Rightarrow> 'a \<Rightarrow> 'a::sup" |
|
28 |
abbreviation "STEP == Step fa fb" |
|
29 |
thm Step.simps[where f = fa and g = fb] |
|
30 |
*) |
|
51389 | 31 |
|
51390 | 32 |
lemma strip_Step[simp]: "strip(Step f g S C) = strip C" |
33 |
by(induct C arbitrary: S) auto |
|
51389 | 34 |
|
35 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
36 |
subsection "Collecting Semantics of Commands" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
37 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
38 |
subsubsection "Annotated commands as a complete lattice" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
39 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
40 |
instantiation acom :: (order) order |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
41 |
begin |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
42 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
43 |
fun less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where |
49344 | 44 |
"(SKIP {P}) \<le> (SKIP {P'}) = (P \<le> P')" | |
45 |
"(x ::= e {P}) \<le> (x' ::= e' {P'}) = (x=x' \<and> e=e' \<and> P \<le> P')" | |
|
46 |
"(C1;C2) \<le> (C1';C2') = (C1 \<le> C1' \<and> C2 \<le> C2')" | |
|
47 |
"(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) \<le> (IF b' THEN {P1'} C1' ELSE {P2'} C2' {Q'}) = |
|
48 |
(b=b' \<and> P1 \<le> P1' \<and> C1 \<le> C1' \<and> P2 \<le> P2' \<and> C2 \<le> C2' \<and> Q \<le> Q')" | |
|
49 |
"({I} WHILE b DO {P} C {Q}) \<le> ({I'} WHILE b' DO {P'} C' {Q'}) = |
|
50 |
(b=b' \<and> C \<le> C' \<and> I \<le> I' \<and> P \<le> P' \<and> Q \<le> Q')" | |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
51 |
"less_eq_acom _ _ = False" |
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 |
lemma SKIP_le: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
54 |
by (cases c) auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
55 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
56 |
lemma Assign_le: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
57 |
by (cases c) auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
58 |
|
49095 | 59 |
lemma Seq_le: "C1;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')" |
60 |
by (cases C) auto |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
61 |
|
49095 | 62 |
lemma If_le: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<le> C \<longleftrightarrow> |
63 |
(\<exists>p1' p2' C1' C2' S'. C = IF b THEN {p1'} C1' ELSE {p2'} C2' {S'} \<and> |
|
64 |
p1 \<le> p1' \<and> p2 \<le> p2' \<and> C1 \<le> C1' \<and> C2 \<le> C2' \<and> S \<le> S')" |
|
65 |
by (cases C) auto |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
66 |
|
49095 | 67 |
lemma While_le: "{I} WHILE b DO {p} C {P} \<le> W \<longleftrightarrow> |
68 |
(\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> C \<le> C' \<and> p \<le> p' \<and> I \<le> I' \<and> P \<le> P')" |
|
69 |
by (cases W) auto |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
70 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
71 |
definition less_acom :: "'a acom \<Rightarrow> 'a acom \<Rightarrow> bool" where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
72 |
"less_acom x y = (x \<le> y \<and> \<not> y \<le> x)" |
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 |
instance |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
75 |
proof |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
76 |
case goal1 show ?case by(simp add: less_acom_def) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
77 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
78 |
case goal2 thus ?case by (induct x) auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
79 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
80 |
case goal3 thus ?case |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
81 |
apply(induct x y arbitrary: z rule: less_eq_acom.induct) |
47818 | 82 |
apply (auto intro: le_trans simp: SKIP_le Assign_le Seq_le If_le While_le) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
83 |
done |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
84 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
85 |
case goal4 thus ?case |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
86 |
apply(induct x y rule: less_eq_acom.induct) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
87 |
apply (auto intro: le_antisym) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
88 |
done |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
89 |
qed |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
90 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
91 |
end |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
92 |
|
51610 | 93 |
text_raw{*\snip{subadef}{2}{1}{% *} |
45919 | 94 |
fun sub\<^isub>1 :: "'a acom \<Rightarrow> 'a acom" where |
51610 | 95 |
"sub\<^isub>1(C\<^isub>1;C\<^isub>2) = C\<^isub>1" | |
96 |
"sub\<^isub>1(IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = C\<^isub>1" | |
|
49344 | 97 |
"sub\<^isub>1({I} WHILE b DO {P} C {Q}) = C" |
51610 | 98 |
text_raw{*}%endsnip*} |
45903 | 99 |
|
51610 | 100 |
text_raw{*\snip{subbdef}{1}{1}{% *} |
45919 | 101 |
fun sub\<^isub>2 :: "'a acom \<Rightarrow> 'a acom" where |
51610 | 102 |
"sub\<^isub>2(C\<^isub>1;C\<^isub>2) = C\<^isub>2" | |
103 |
"sub\<^isub>2(IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = C\<^isub>2" |
|
104 |
text_raw{*}%endsnip*} |
|
45903 | 105 |
|
51610 | 106 |
text_raw{*\snip{annoadef}{1}{1}{% *} |
49095 | 107 |
fun anno\<^isub>1 :: "'a acom \<Rightarrow> 'a" where |
51610 | 108 |
"anno\<^isub>1(IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = P\<^isub>1" | |
49344 | 109 |
"anno\<^isub>1({I} WHILE b DO {P} C {Q}) = I" |
51610 | 110 |
text_raw{*}%endsnip*} |
49095 | 111 |
|
51610 | 112 |
text_raw{*\snip{annobdef}{1}{2}{% *} |
49095 | 113 |
fun anno\<^isub>2 :: "'a acom \<Rightarrow> 'a" where |
51610 | 114 |
"anno\<^isub>2(IF b THEN {P\<^isub>1} C\<^isub>1 ELSE {P\<^isub>2} C\<^isub>2 {Q}) = P\<^isub>2" | |
49344 | 115 |
"anno\<^isub>2({I} WHILE b DO {P} C {Q}) = P" |
51610 | 116 |
text_raw{*}%endsnip*} |
45903 | 117 |
|
51610 | 118 |
fun merge :: "com \<Rightarrow> 'a acom set \<Rightarrow> 'a set acom" where |
119 |
"merge com.SKIP M = (SKIP {post ` M})" | |
|
120 |
"merge (x ::= a) M = (x ::= a {post ` M})" | |
|
121 |
"merge (c1;c2) M = |
|
122 |
merge c1 (sub\<^isub>1 ` M); merge c2 (sub\<^isub>2 ` M)" | |
|
123 |
"merge (IF b THEN c1 ELSE c2) M = |
|
124 |
IF b THEN {anno\<^isub>1 ` M} merge c1 (sub\<^isub>1 ` M) ELSE {anno\<^isub>2 ` M} merge c2 (sub\<^isub>2 ` M) |
|
49397 | 125 |
{post ` M}" | |
51610 | 126 |
"merge (WHILE b DO c) M = |
49397 | 127 |
{anno\<^isub>1 ` M} |
51610 | 128 |
WHILE b DO {anno\<^isub>2 ` M} merge c (sub\<^isub>1 ` M) |
49397 | 129 |
{post ` M}" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
130 |
|
49397 | 131 |
interpretation |
51610 | 132 |
Complete_Lattice "{C. strip C = c}" "map_acom Inter o (merge c)" for c |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
133 |
proof |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
134 |
case goal1 |
51610 | 135 |
have "a:A \<Longrightarrow> map_acom Inter (merge (strip a) A) \<le> a" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
136 |
proof(induction a arbitrary: A) |
47818 | 137 |
case Seq from Seq.prems show ?case by(force intro!: Seq.IH) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
138 |
next |
45903 | 139 |
case If from If.prems show ?case by(force intro!: If.IH) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
140 |
next |
45903 | 141 |
case While from While.prems show ?case by(force intro!: While.IH) |
142 |
qed force+ |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
143 |
with goal1 show ?case by auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
144 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
145 |
case goal2 |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
146 |
thus ?case |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
147 |
proof(simp, induction b arbitrary: c A) |
45903 | 148 |
case SKIP thus ?case by (force simp:SKIP_le) |
149 |
next |
|
150 |
case Assign thus ?case by (force simp:Assign_le) |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
151 |
next |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
152 |
case Seq from Seq.prems show ?case by(force intro!: Seq.IH simp:Seq_le) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
153 |
next |
45903 | 154 |
case If from If.prems show ?case by (force simp: If_le intro!: If.IH) |
155 |
next |
|
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
156 |
case While from While.prems show ?case by(fastforce simp: While_le intro: While.IH) |
45903 | 157 |
qed |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
158 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
159 |
case goal3 |
51610 | 160 |
have "strip(merge c A) = c" |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
161 |
proof(induction c arbitrary: A) |
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
162 |
case Seq from Seq.prems show ?case by (fastforce simp: strip_eq_Seq subset_iff intro!: Seq.IH) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
163 |
next |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
164 |
case If from If.prems show ?case by (fastforce intro!: If.IH simp: strip_eq_If) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
165 |
next |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
166 |
case While from While.prems show ?case by(fastforce intro: While.IH simp: strip_eq_While) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
167 |
qed auto |
45903 | 168 |
thus ?case by auto |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
169 |
qed |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
170 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
171 |
lemma le_post: "c \<le> d \<Longrightarrow> post c \<le> post d" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
172 |
by(induction c d rule: less_eq_acom.induct) auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
173 |
|
49487 | 174 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
175 |
subsubsection "Collecting semantics" |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
176 |
|
51390 | 177 |
definition "step = Step (\<lambda>x e S. {s(x := aval e s) |s. s : S}) (\<lambda>b S. {s:S. bval b s})" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
178 |
|
46070 | 179 |
definition CS :: "com \<Rightarrow> state set acom" where |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
180 |
"CS c = lfp c (step UNIV)" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
181 |
|
51390 | 182 |
lemma mono2_Step: fixes C1 C2 :: "'a::semilattice_sup acom" |
183 |
assumes "!!x e S1 S2. S1 \<le> S2 \<Longrightarrow> f x e S1 \<le> f x e S2" |
|
184 |
"!!b S1 S2. S1 \<le> S2 \<Longrightarrow> g b S1 \<le> g b S2" |
|
185 |
shows "C1 \<le> C2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> Step f g S1 C1 \<le> Step f g S2 C2" |
|
186 |
proof(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct) |
|
187 |
case 2 thus ?case by (fastforce simp: assms(1)) |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
188 |
next |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
189 |
case 3 thus ?case by(simp add: le_post) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
190 |
next |
51390 | 191 |
case 4 thus ?case |
192 |
by(simp add: subset_iff assms(2)) (metis le_post le_supI1 le_supI2) |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
193 |
next |
51390 | 194 |
case 5 thus ?case |
195 |
by(simp add: subset_iff assms(2)) (metis le_post le_supI1 le_supI2) |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
196 |
qed auto |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
197 |
|
51390 | 198 |
lemma mono2_step: "C1 \<le> C2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 C1 \<le> step S2 C2" |
199 |
unfolding step_def by(rule mono2_Step) auto |
|
200 |
||
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
201 |
lemma mono_step: "mono (step S)" |
46334 | 202 |
by(blast intro: monoI mono2_step) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
203 |
|
49095 | 204 |
lemma strip_step: "strip(step S C) = strip C" |
51390 | 205 |
by (induction C arbitrary: S) (auto simp: step_def) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
206 |
|
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
47818
diff
changeset
|
207 |
lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))" |
45903 | 208 |
apply(rule lfp_unfold[OF _ mono_step]) |
209 |
apply(simp add: strip_step) |
|
210 |
done |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
211 |
|
46070 | 212 |
lemma CS_unfold: "CS c = step UNIV (CS c)" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
213 |
by (metis CS_def lfp_cs_unfold) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
214 |
|
46070 | 215 |
lemma strip_CS[simp]: "strip(CS c) = c" |
45903 | 216 |
by(simp add: CS_def index_lfp[simplified]) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
217 |
|
49487 | 218 |
|
219 |
subsubsection "Relation to big-step semantics" |
|
220 |
||
51610 | 221 |
lemma post_merge: "\<forall> c' \<in> M. strip c' = c \<Longrightarrow> post (merge c M) = post ` M" |
49487 | 222 |
proof(induction c arbitrary: M) |
223 |
case (Seq c1 c2) |
|
224 |
have "post ` M = post ` sub\<^isub>2 ` M" using Seq.prems by (force simp: strip_eq_Seq) |
|
225 |
moreover have "\<forall> c' \<in> sub\<^isub>2 ` M. strip c' = c2" using Seq.prems by (auto simp: strip_eq_Seq) |
|
226 |
ultimately show ?case using Seq.IH(2)[of "sub\<^isub>2 ` M"] by simp |
|
227 |
qed simp_all |
|
228 |
||
229 |
||
230 |
lemma post_lfp: "post(lfp c f) = (\<Inter>{post C|C. strip C = c \<and> f C \<le> C})" |
|
51610 | 231 |
by(auto simp add: lfp_def post_merge) |
49487 | 232 |
|
233 |
lemma big_step_post_step: |
|
234 |
"\<lbrakk> (c, s) \<Rightarrow> t; strip C = c; s \<in> S; step S C \<le> C \<rbrakk> \<Longrightarrow> t \<in> post C" |
|
235 |
proof(induction arbitrary: C S rule: big_step_induct) |
|
51390 | 236 |
case Skip thus ?case by(auto simp: strip_eq_SKIP step_def) |
49487 | 237 |
next |
51390 | 238 |
case Assign thus ?case by(fastforce simp: strip_eq_Assign step_def) |
49487 | 239 |
next |
51390 | 240 |
case Seq thus ?case by(fastforce simp: strip_eq_Seq step_def) |
49487 | 241 |
next |
51390 | 242 |
case IfTrue thus ?case apply(auto simp: strip_eq_If step_def) |
243 |
by (metis (lifting,full_types) mem_Collect_eq set_mp) |
|
49487 | 244 |
next |
51390 | 245 |
case IfFalse thus ?case apply(auto simp: strip_eq_If step_def) |
246 |
by (metis (lifting,full_types) mem_Collect_eq set_mp) |
|
49487 | 247 |
next |
248 |
case (WhileTrue b s1 c' s2 s3) |
|
249 |
from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'" |
|
250 |
by(auto simp: strip_eq_While) |
|
251 |
from WhileTrue.prems(3) `C = _` |
|
51390 | 252 |
have "step P C' \<le> C'" "{s \<in> I. bval b s} \<le> P" "S \<le> I" "step (post C') C \<le> C" |
253 |
by (auto simp: step_def) |
|
49487 | 254 |
have "step {s \<in> I. bval b s} C' \<le> C'" |
255 |
by (rule order_trans[OF mono2_step[OF order_refl `{s \<in> I. bval b s} \<le> P`] `step P C' \<le> C'`]) |
|
256 |
have "s1: {s:I. bval b s}" using `s1 \<in> S` `S \<subseteq> I` `bval b s1` by auto |
|
257 |
note s2_in_post_C' = WhileTrue.IH(1)[OF `strip C' = c'` this `step {s \<in> I. bval b s} C' \<le> C'`] |
|
258 |
from WhileTrue.IH(2)[OF WhileTrue.prems(1) s2_in_post_C' `step (post C') C \<le> C`] |
|
259 |
show ?case . |
|
260 |
next |
|
51390 | 261 |
case (WhileFalse b s1 c') thus ?case by (force simp: strip_eq_While step_def) |
49487 | 262 |
qed |
263 |
||
264 |
lemma big_step_lfp: "\<lbrakk> (c,s) \<Rightarrow> t; s \<in> S \<rbrakk> \<Longrightarrow> t \<in> post(lfp c (step S))" |
|
265 |
by(auto simp add: post_lfp intro: big_step_post_step) |
|
266 |
||
267 |
lemma big_step_CS: "(c,s) \<Rightarrow> t \<Longrightarrow> t : post(CS c)" |
|
268 |
by(simp add: CS_def big_step_lfp) |
|
269 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
diff
changeset
|
270 |
end |