author | wenzelm |
Tue, 13 Aug 2013 16:25:47 +0200 | |
changeset 53015 | a1119cf551e8 |
parent 52046 | bc01725d7918 |
child 55601 | b7f4da504b75 |
permissions | -rw-r--r-- |
45111 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
47602 | 3 |
theory Abs_Int0_ITP |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
4 |
imports "~~/src/HOL/ex/Interpretation_with_Defs" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
5 |
"~~/src/HOL/Library/While_Combinator" |
48759
ff570720ba1c
Improved complete lattice formalisation - no more index set.
nipkow
parents:
48480
diff
changeset
|
6 |
"Collecting_ITP" |
45111 | 7 |
begin |
8 |
||
9 |
subsection "Orderings" |
|
10 |
||
11 |
class preord = |
|
12 |
fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50) |
|
13 |
assumes le_refl[simp]: "x \<sqsubseteq> x" |
|
14 |
and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z" |
|
15 |
begin |
|
16 |
||
17 |
definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)" |
|
18 |
||
19 |
lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def) |
|
20 |
||
21 |
lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)" |
|
22 |
by(simp add: mono_def) |
|
23 |
||
24 |
declare le_trans[trans] |
|
25 |
||
26 |
end |
|
27 |
||
28 |
text{* Note: no antisymmetry. Allows implementations where some abstract |
|
29 |
element is implemented by two different values @{prop "x \<noteq> y"} |
|
30 |
such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not |
|
31 |
needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}. |
|
32 |
*} |
|
33 |
||
34 |
class SL_top = preord + |
|
35 |
fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65) |
|
36 |
fixes Top :: "'a" ("\<top>") |
|
37 |
assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y" |
|
38 |
and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y" |
|
39 |
and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z" |
|
40 |
and top[simp]: "x \<sqsubseteq> \<top>" |
|
41 |
begin |
|
42 |
||
43 |
lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z" |
|
44 |
by (metis join_ge1 join_ge2 join_least le_trans) |
|
45 |
||
46 |
lemma le_join_disj: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z" |
|
47 |
by (metis join_ge1 join_ge2 le_trans) |
|
48 |
||
49 |
end |
|
50 |
||
51 |
instantiation "fun" :: (type, SL_top) SL_top |
|
52 |
begin |
|
53 |
||
54 |
definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)" |
|
55 |
definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)" |
|
56 |
definition "\<top> = (\<lambda>x. \<top>)" |
|
57 |
||
58 |
lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x" |
|
59 |
by (simp add: join_fun_def) |
|
60 |
||
61 |
instance |
|
62 |
proof |
|
63 |
case goal2 thus ?case by (metis le_fun_def preord_class.le_trans) |
|
64 |
qed (simp_all add: le_fun_def Top_fun_def) |
|
65 |
||
66 |
end |
|
67 |
||
68 |
||
69 |
instantiation acom :: (preord) preord |
|
70 |
begin |
|
71 |
||
72 |
fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where |
|
73 |
"le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" | |
|
74 |
"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" | |
|
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51625
diff
changeset
|
75 |
"le_acom (c1;;c2) (c1';;c2') = (le_acom c1 c1' \<and> le_acom c2 c2')" | |
45111 | 76 |
"le_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) = |
77 |
(b=b' \<and> le_acom c1 c1' \<and> le_acom c2 c2' \<and> S \<sqsubseteq> S')" | |
|
78 |
"le_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) = |
|
79 |
(b=b' \<and> le_acom c c' \<and> Inv \<sqsubseteq> Inv' \<and> P \<sqsubseteq> P')" | |
|
80 |
"le_acom _ _ = False" |
|
81 |
||
82 |
lemma [simp]: "SKIP {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<sqsubseteq> S')" |
|
83 |
by (cases c) auto |
|
84 |
||
85 |
lemma [simp]: "x ::= e {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<sqsubseteq> S')" |
|
86 |
by (cases c) auto |
|
87 |
||
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51625
diff
changeset
|
88 |
lemma [simp]: "c1;;c2 \<sqsubseteq> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';;c2' \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2')" |
45111 | 89 |
by (cases c) auto |
90 |
||
91 |
lemma [simp]: "IF b THEN c1 ELSE c2 {S} \<sqsubseteq> c \<longleftrightarrow> |
|
92 |
(\<exists>c1' c2' S'. c = IF b THEN c1' ELSE c2' {S'} \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2' \<and> S \<sqsubseteq> S')" |
|
93 |
by (cases c) auto |
|
94 |
||
95 |
lemma [simp]: "{Inv} WHILE b DO c {P} \<sqsubseteq> w \<longleftrightarrow> |
|
96 |
(\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<sqsubseteq> c' \<and> Inv \<sqsubseteq> Inv' \<and> P \<sqsubseteq> P')" |
|
97 |
by (cases w) auto |
|
98 |
||
99 |
instance |
|
100 |
proof |
|
101 |
case goal1 thus ?case by (induct x) auto |
|
102 |
next |
|
103 |
case goal2 thus ?case |
|
104 |
apply(induct x y arbitrary: z rule: le_acom.induct) |
|
105 |
apply (auto intro: le_trans) |
|
106 |
done |
|
107 |
qed |
|
108 |
||
109 |
end |
|
110 |
||
111 |
||
112 |
subsubsection "Lifting" |
|
113 |
||
46078 | 114 |
instantiation option :: (preord)preord |
45111 | 115 |
begin |
116 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
117 |
fun le_option where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
118 |
"Some x \<sqsubseteq> Some y = (x \<sqsubseteq> y)" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
119 |
"None \<sqsubseteq> y = True" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
120 |
"Some _ \<sqsubseteq> None = False" |
45111 | 121 |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
122 |
lemma [simp]: "(x \<sqsubseteq> None) = (x = None)" |
45111 | 123 |
by (cases x) simp_all |
124 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
125 |
lemma [simp]: "(Some x \<sqsubseteq> u) = (\<exists>y. u = Some y & x \<sqsubseteq> y)" |
45111 | 126 |
by (cases u) auto |
127 |
||
46078 | 128 |
instance proof |
129 |
case goal1 show ?case by(cases x, simp_all) |
|
130 |
next |
|
131 |
case goal2 thus ?case |
|
132 |
by(cases z, simp, cases y, simp, cases x, auto intro: le_trans) |
|
133 |
qed |
|
134 |
||
135 |
end |
|
136 |
||
137 |
instantiation option :: (SL_top)SL_top |
|
138 |
begin |
|
139 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
140 |
fun join_option where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
141 |
"Some x \<squnion> Some y = Some(x \<squnion> y)" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
142 |
"None \<squnion> y = y" | |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
143 |
"x \<squnion> None = x" |
45111 | 144 |
|
46039 | 145 |
lemma join_None2[simp]: "x \<squnion> None = x" |
45111 | 146 |
by (cases x) simp_all |
147 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
148 |
definition "\<top> = Some \<top>" |
45111 | 149 |
|
150 |
instance proof |
|
46078 | 151 |
case goal1 thus ?case by(cases x, simp, cases y, simp_all) |
45111 | 152 |
next |
46078 | 153 |
case goal2 thus ?case by(cases y, simp, cases x, simp_all) |
45111 | 154 |
next |
46078 | 155 |
case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all) |
45111 | 156 |
next |
46078 | 157 |
case goal4 thus ?case by(cases x, simp_all add: Top_option_def) |
45111 | 158 |
qed |
159 |
||
160 |
end |
|
161 |
||
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
162 |
definition bot_acom :: "com \<Rightarrow> ('a::SL_top)option acom" ("\<bottom>\<^sub>c") where |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
163 |
"\<bottom>\<^sub>c = anno None" |
45111 | 164 |
|
165 |
lemma strip_bot_acom[simp]: "strip(\<bottom>\<^sub>c c) = c" |
|
166 |
by(simp add: bot_acom_def) |
|
167 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
168 |
lemma bot_acom[rule_format]: "strip c' = c \<longrightarrow> \<bottom>\<^sub>c c \<sqsubseteq> c'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
169 |
apply(induct c arbitrary: c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
170 |
apply (simp_all add: bot_acom_def) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
171 |
apply(induct_tac c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
172 |
apply simp_all |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
173 |
apply(induct_tac c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
174 |
apply simp_all |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
175 |
apply(induct_tac c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
176 |
apply simp_all |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
177 |
apply(induct_tac c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
178 |
apply simp_all |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
179 |
apply(induct_tac c') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
180 |
apply simp_all |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
181 |
done |
45111 | 182 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
183 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
184 |
subsubsection "Post-fixed point iteration" |
45111 | 185 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
186 |
definition |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
187 |
pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
188 |
"pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
189 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
190 |
lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
191 |
using while_option_stop[OF assms[simplified pfp_def]] by simp |
45111 | 192 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
193 |
lemma pfp_least: |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
194 |
assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
195 |
and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" and "pfp f x0 = Some x" shows "x \<sqsubseteq> p" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
196 |
proof- |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
197 |
{ fix x assume "x \<sqsubseteq> p" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
198 |
hence "f x \<sqsubseteq> f p" by(rule mono) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
199 |
from this `f p \<sqsubseteq> p` have "f x \<sqsubseteq> p" by(rule le_trans) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
200 |
} |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
201 |
thus "x \<sqsubseteq> p" using assms(2-) while_option_rule[where P = "%x. x \<sqsubseteq> p"] |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
202 |
unfolding pfp_def by blast |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
203 |
qed |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
204 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
205 |
definition |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
206 |
lpfp\<^sub>c :: "(('a::SL_top)option acom \<Rightarrow> 'a option acom) \<Rightarrow> com \<Rightarrow> 'a option acom option" where |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
207 |
"lpfp\<^sub>c f c = pfp f (\<bottom>\<^sub>c c)" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
208 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
209 |
lemma lpfpc_pfp: "lpfp\<^sub>c f c0 = Some c \<Longrightarrow> f c \<sqsubseteq> c" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
210 |
by(simp add: pfp_pfp lpfp\<^sub>c_def) |
45111 | 211 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
212 |
lemma strip_pfp: |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
213 |
assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
214 |
using assms while_option_rule[where P = "%x. g x = g x0" and c = f] |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
215 |
unfolding pfp_def by metis |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
216 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
217 |
lemma strip_lpfpc: assumes "\<And>c. strip(f c) = strip c" and "lpfp\<^sub>c f c = Some c'" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
218 |
shows "strip c' = c" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
219 |
using assms(1) strip_pfp[OF _ assms(2)[simplified lpfp\<^sub>c_def]] |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
220 |
by(metis strip_bot_acom) |
45111 | 221 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
222 |
lemma lpfpc_least: |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
223 |
assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
224 |
and "strip p = c0" and "f p \<sqsubseteq> p" and lp: "lpfp\<^sub>c f c0 = Some c" shows "c \<sqsubseteq> p" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
225 |
using pfp_least[OF _ _ bot_acom[OF `strip p = c0`] lp[simplified lpfp\<^sub>c_def]] |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
226 |
mono `f p \<sqsubseteq> p` |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
227 |
by blast |
45111 | 228 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
229 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
230 |
subsection "Abstract Interpretation" |
45111 | 231 |
|
46039 | 232 |
definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where |
233 |
"\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}" |
|
45111 | 234 |
|
46039 | 235 |
fun \<gamma>_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where |
236 |
"\<gamma>_option \<gamma> None = {}" | |
|
237 |
"\<gamma>_option \<gamma> (Some a) = \<gamma> a" |
|
45111 | 238 |
|
239 |
text{* The interface for abstract values: *} |
|
240 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
241 |
locale Val_abs = |
46063 | 242 |
fixes \<gamma> :: "'av::SL_top \<Rightarrow> val set" |
46039 | 243 |
assumes mono_gamma: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b" |
244 |
and gamma_Top[simp]: "\<gamma> \<top> = UNIV" |
|
46063 | 245 |
fixes num' :: "val \<Rightarrow> 'av" |
246 |
and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av" |
|
46039 | 247 |
assumes gamma_num': "n : \<gamma>(num' n)" |
248 |
and gamma_plus': |
|
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
249 |
"n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma>(plus' a1 a2)" |
45111 | 250 |
|
46063 | 251 |
type_synonym 'av st = "(vname \<Rightarrow> 'av)" |
45111 | 252 |
|
46063 | 253 |
locale Abs_Int_Fun = Val_abs \<gamma> for \<gamma> :: "'av::SL_top \<Rightarrow> val set" |
45111 | 254 |
begin |
255 |
||
46063 | 256 |
fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where |
46039 | 257 |
"aval' (N n) S = num' n" | |
45111 | 258 |
"aval' (V x) S = S x" | |
259 |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" |
|
260 |
||
46063 | 261 |
fun step' :: "'av st option \<Rightarrow> 'av st option acom \<Rightarrow> 'av st option acom" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
262 |
where |
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
263 |
"step' S (SKIP {P}) = (SKIP {S})" | |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
264 |
"step' S (x ::= e {P}) = |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
265 |
x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}" | |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
51625
diff
changeset
|
266 |
"step' S (c1;; c2) = step' S c1;; step' (post c1) c2" | |
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
267 |
"step' S (IF b THEN c1 ELSE c2 {P}) = |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
268 |
IF b THEN step' S c1 ELSE step' S c2 {post c1 \<squnion> post c2}" | |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
269 |
"step' S ({Inv} WHILE b DO c {P}) = |
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
270 |
{S \<squnion> post c} WHILE b DO (step' Inv c) {Inv}" |
45111 | 271 |
|
46063 | 272 |
definition AI :: "com \<Rightarrow> 'av st option acom option" where |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
273 |
"AI = lpfp\<^sub>c (step' \<top>)" |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
274 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
275 |
|
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
276 |
lemma strip_step'[simp]: "strip(step' S c) = strip c" |
45111 | 277 |
by(induct c arbitrary: S) (simp_all add: Let_def) |
278 |
||
279 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
280 |
abbreviation \<gamma>\<^sub>f :: "'av st \<Rightarrow> state set" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
281 |
where "\<gamma>\<^sub>f == \<gamma>_fun \<gamma>" |
45111 | 282 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
283 |
abbreviation \<gamma>\<^sub>o :: "'av st option \<Rightarrow> state set" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
284 |
where "\<gamma>\<^sub>o == \<gamma>_option \<gamma>\<^sub>f" |
45111 | 285 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
286 |
abbreviation \<gamma>\<^sub>c :: "'av st option acom \<Rightarrow> state set acom" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
287 |
where "\<gamma>\<^sub>c == map_acom \<gamma>\<^sub>o" |
45111 | 288 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
289 |
lemma gamma_f_Top[simp]: "\<gamma>\<^sub>f Top = UNIV" |
46039 | 290 |
by(simp add: Top_fun_def \<gamma>_fun_def) |
45111 | 291 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
292 |
lemma gamma_o_Top[simp]: "\<gamma>\<^sub>o Top = UNIV" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
293 |
by (simp add: Top_option_def) |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
294 |
|
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
295 |
(* FIXME (maybe also le \<rightarrow> sqle?) *) |
45111 | 296 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
297 |
lemma mono_gamma_f: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^sub>f f \<subseteq> \<gamma>\<^sub>f g" |
46039 | 298 |
by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
299 |
|
46039 | 300 |
lemma mono_gamma_o: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
301 |
"sa \<sqsubseteq> sa' \<Longrightarrow> \<gamma>\<^sub>o sa \<subseteq> \<gamma>\<^sub>o sa'" |
46039 | 302 |
by(induction sa sa' rule: le_option.induct)(simp_all add: mono_gamma_f) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
303 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
304 |
lemma mono_gamma_c: "ca \<sqsubseteq> ca' \<Longrightarrow> \<gamma>\<^sub>c ca \<le> \<gamma>\<^sub>c ca'" |
46039 | 305 |
by (induction ca ca' rule: le_acom.induct) (simp_all add:mono_gamma_o) |
45111 | 306 |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
307 |
text{* Soundness: *} |
45111 | 308 |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
309 |
lemma aval'_sound: "s : \<gamma>\<^sub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)" |
46039 | 310 |
by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_fun_def) |
45111 | 311 |
|
46039 | 312 |
lemma in_gamma_update: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
313 |
"\<lbrakk> s : \<gamma>\<^sub>f S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^sub>f(S(x := a))" |
46039 | 314 |
by(simp add: \<gamma>_fun_def) |
45111 | 315 |
|
46068 | 316 |
lemma step_preserves_le: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
317 |
"\<lbrakk> S \<subseteq> \<gamma>\<^sub>o S'; c \<le> \<gamma>\<^sub>c c' \<rbrakk> \<Longrightarrow> step S c \<le> \<gamma>\<^sub>c (step' S' c')" |
46334 | 318 |
proof(induction c arbitrary: c' S S') |
46068 | 319 |
case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP) |
45111 | 320 |
next |
321 |
case Assign thus ?case |
|
46068 | 322 |
by (fastforce simp: Assign_le map_acom_Assign intro: aval'_sound in_gamma_update |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
323 |
split: option.splits del:subsetD) |
45111 | 324 |
next |
47818 | 325 |
case Seq thus ?case apply (auto simp: Seq_le map_acom_Seq) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
326 |
by (metis le_post post_map_acom) |
45111 | 327 |
next |
46334 | 328 |
case (If b c1 c2 P) |
329 |
then obtain c1' c2' P' where |
|
330 |
"c' = IF b THEN c1' ELSE c2' {P'}" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
331 |
"P \<subseteq> \<gamma>\<^sub>o P'" "c1 \<le> \<gamma>\<^sub>c c1'" "c2 \<le> \<gamma>\<^sub>c c2'" |
46068 | 332 |
by (fastforce simp: If_le map_acom_If) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
333 |
moreover have "post c1 \<subseteq> \<gamma>\<^sub>o(post c1' \<squnion> post c2')" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
334 |
by (metis (no_types) `c1 \<le> \<gamma>\<^sub>c c1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
335 |
moreover have "post c2 \<subseteq> \<gamma>\<^sub>o(post c1' \<squnion> post c2')" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
336 |
by (metis (no_types) `c2 \<le> \<gamma>\<^sub>c c2'` join_ge2 le_post mono_gamma_o order_trans post_map_acom) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
337 |
ultimately show ?case using `S \<subseteq> \<gamma>\<^sub>o S'` by (simp add: If.IH subset_iff) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
338 |
next |
46334 | 339 |
case (While I b c1 P) |
340 |
then obtain c1' I' P' where |
|
341 |
"c' = {I'} WHILE b DO c1' {P'}" |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
342 |
"I \<subseteq> \<gamma>\<^sub>o I'" "P \<subseteq> \<gamma>\<^sub>o P'" "c1 \<le> \<gamma>\<^sub>c c1'" |
46068 | 343 |
by (fastforce simp: map_acom_While While_le) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
344 |
moreover have "S \<union> post c1 \<subseteq> \<gamma>\<^sub>o (S' \<squnion> post c1')" |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
345 |
using `S \<subseteq> \<gamma>\<^sub>o S'` le_post[OF `c1 \<le> \<gamma>\<^sub>c c1'`, simplified] |
46039 | 346 |
by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
347 |
ultimately show ?case by (simp add: While.IH subset_iff) |
45111 | 348 |
qed |
349 |
||
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
350 |
lemma AI_sound: "AI c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c c'" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
351 |
proof(simp add: CS_def AI_def) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
352 |
assume 1: "lpfp\<^sub>c (step' \<top>) c = Some c'" |
45655
a49f9428aba4
simplified Collecting1 and renamed: step -> step', step_cs -> step
nipkow
parents:
45623
diff
changeset
|
353 |
have 2: "step' \<top> c' \<sqsubseteq> c'" by(rule lpfpc_pfp[OF 1]) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
354 |
have 3: "strip (\<gamma>\<^sub>c (step' \<top> c')) = c" |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
355 |
by(simp add: strip_lpfpc[OF _ 1]) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
356 |
have "lfp (step UNIV) c \<le> \<gamma>\<^sub>c (step' \<top> c')" |
45903 | 357 |
proof(rule lfp_lowerbound[simplified,OF 3]) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
358 |
show "step UNIV (\<gamma>\<^sub>c (step' \<top> c')) \<le> \<gamma>\<^sub>c (step' \<top> c')" |
46068 | 359 |
proof(rule step_preserves_le[OF _ _]) |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
360 |
show "UNIV \<subseteq> \<gamma>\<^sub>o \<top>" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
361 |
show "\<gamma>\<^sub>c (step' \<top> c') \<le> \<gamma>\<^sub>c c'" by(rule mono_gamma_c[OF 2]) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
362 |
qed |
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
363 |
qed |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52046
diff
changeset
|
364 |
with 2 show "lfp (step UNIV) c \<le> \<gamma>\<^sub>c c'" |
46039 | 365 |
by (blast intro: mono_gamma_c order_trans) |
45623
f682f3f7b726
Abstract interpretation is now based uniformly on annotated programs,
nipkow
parents:
45212
diff
changeset
|
366 |
qed |
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
367 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
368 |
end |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
369 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
370 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
371 |
subsubsection "Monotonicity" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
372 |
|
46153 | 373 |
lemma mono_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'" |
374 |
by(induction c c' rule: le_acom.induct) (auto) |
|
375 |
||
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
376 |
locale Abs_Int_Fun_mono = Abs_Int_Fun + |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
377 |
assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
378 |
begin |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
379 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
380 |
lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
381 |
by(induction e)(auto simp: le_fun_def mono_plus') |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
382 |
|
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
383 |
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')" |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
384 |
by(simp add: le_fun_def) |
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
385 |
|
46153 | 386 |
lemma mono_step': "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step' S c \<sqsubseteq> step' S' c'" |
387 |
apply(induction c c' arbitrary: S S' rule: le_acom.induct) |
|
388 |
apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj |
|
389 |
split: option.split) |
|
45127
d2eb07a1e01b
separated monotonicity reasoning and defined narrowing with while_option
nipkow
parents:
45113
diff
changeset
|
390 |
done |
45111 | 391 |
|
392 |
end |
|
393 |
||
394 |
text{* Problem: not executable because of the comparison of abstract states, |
|
395 |
i.e. functions, in the post-fixedpoint computation. *} |
|
396 |
||
397 |
end |