1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/IMP/Abs_Int0_fun.thy Wed Sep 28 09:55:11 2011 +0200
1.3 @@ -0,0 +1,423 @@
1.4 +(* Author: Tobias Nipkow *)
1.5 +
1.6 +header "Abstract Interpretation"
1.7 +
1.8 +theory Abs_Int0_fun
1.9 +imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
1.10 +begin
1.11 +
1.12 +subsection "Annotated Commands"
1.13 +
1.14 +datatype 'a acom =
1.15 + SKIP 'a ("SKIP {_}") |
1.16 + Assign name aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
1.17 + Semi "'a acom" "'a acom" ("_;// _" [60, 61] 60) |
1.18 + If bexp "'a acom" "'a acom" 'a
1.19 + ("((IF _/ THEN _/ ELSE _)/ {_})" [0, 0, 61, 0] 61) |
1.20 + While 'a bexp "'a acom" 'a
1.21 + ("({_}// WHILE _/ DO (_)// {_})" [0, 0, 61, 0] 61)
1.22 +
1.23 +fun post :: "'a acom \<Rightarrow>'a" where
1.24 +"post (SKIP {P}) = P" |
1.25 +"post (x ::= e {P}) = P" |
1.26 +"post (c1; c2) = post c2" |
1.27 +"post (IF b THEN c1 ELSE c2 {P}) = P" |
1.28 +"post ({Inv} WHILE b DO c {P}) = P"
1.29 +
1.30 +fun strip :: "'a acom \<Rightarrow> com" where
1.31 +"strip (SKIP {a}) = com.SKIP" |
1.32 +"strip (x ::= e {a}) = (x ::= e)" |
1.33 +"strip (c1;c2) = (strip c1; strip c2)" |
1.34 +"strip (IF b THEN c1 ELSE c2 {a}) = (IF b THEN strip c1 ELSE strip c2)" |
1.35 +"strip ({a1} WHILE b DO c {a2}) = (WHILE b DO strip c)"
1.36 +
1.37 +fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
1.38 +"anno a com.SKIP = SKIP {a}" |
1.39 +"anno a (x ::= e) = (x ::= e {a})" |
1.40 +"anno a (c1;c2) = (anno a c1; anno a c2)" |
1.41 +"anno a (IF b THEN c1 ELSE c2) =
1.42 + (IF b THEN anno a c1 ELSE anno a c2 {a})" |
1.43 +"anno a (WHILE b DO c) =
1.44 + ({a} WHILE b DO anno a c {a})"
1.45 +
1.46 +lemma strip_anno[simp]: "strip (anno a c) = c"
1.47 +by(induct c) simp_all
1.48 +
1.49 +fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
1.50 +"map_acom f (SKIP {a}) = SKIP {f a}" |
1.51 +"map_acom f (x ::= e {a}) = (x ::= e {f a})" |
1.52 +"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
1.53 +"map_acom f (IF b THEN c1 ELSE c2 {a}) =
1.54 + (IF b THEN map_acom f c1 ELSE map_acom f c2 {f a})" |
1.55 +"map_acom f ({a1} WHILE b DO c {a2}) =
1.56 + ({f a1} WHILE b DO map_acom f c {f a2})"
1.57 +
1.58 +
1.59 +subsection "Orderings"
1.60 +
1.61 +class preord =
1.62 +fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
1.63 +assumes le_refl[simp]: "x \<sqsubseteq> x"
1.64 +and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
1.65 +begin
1.66 +
1.67 +definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
1.68 +
1.69 +lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
1.70 +
1.71 +lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
1.72 +by(simp add: mono_def)
1.73 +
1.74 +declare le_trans[trans]
1.75 +
1.76 +end
1.77 +
1.78 +text{* Note: no antisymmetry. Allows implementations where some abstract
1.79 +element is implemented by two different values @{prop "x \<noteq> y"}
1.80 +such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
1.81 +needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
1.82 +*}
1.83 +
1.84 +class SL_top = preord +
1.85 +fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
1.86 +fixes Top :: "'a" ("\<top>")
1.87 +assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
1.88 +and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
1.89 +and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
1.90 +and top[simp]: "x \<sqsubseteq> \<top>"
1.91 +begin
1.92 +
1.93 +lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
1.94 +by (metis join_ge1 join_ge2 join_least le_trans)
1.95 +
1.96 +lemma le_join_disj: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z"
1.97 +by (metis join_ge1 join_ge2 le_trans)
1.98 +
1.99 +end
1.100 +
1.101 +instantiation "fun" :: (type, SL_top) SL_top
1.102 +begin
1.103 +
1.104 +definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
1.105 +definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
1.106 +definition "\<top> = (\<lambda>x. \<top>)"
1.107 +
1.108 +lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x"
1.109 +by (simp add: join_fun_def)
1.110 +
1.111 +instance
1.112 +proof
1.113 + case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
1.114 +qed (simp_all add: le_fun_def Top_fun_def)
1.115 +
1.116 +end
1.117 +
1.118 +
1.119 +instantiation acom :: (preord) preord
1.120 +begin
1.121 +
1.122 +fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
1.123 +"le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" |
1.124 +"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" |
1.125 +"le_acom (c1;c2) (c1';c2') = (le_acom c1 c1' \<and> le_acom c2 c2')" |
1.126 +"le_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) =
1.127 + (b=b' \<and> le_acom c1 c1' \<and> le_acom c2 c2' \<and> S \<sqsubseteq> S')" |
1.128 +"le_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) =
1.129 + (b=b' \<and> le_acom c c' \<and> Inv \<sqsubseteq> Inv' \<and> P \<sqsubseteq> P')" |
1.130 +"le_acom _ _ = False"
1.131 +
1.132 +lemma [simp]: "SKIP {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<sqsubseteq> S')"
1.133 +by (cases c) auto
1.134 +
1.135 +lemma [simp]: "x ::= e {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<sqsubseteq> S')"
1.136 +by (cases c) auto
1.137 +
1.138 +lemma [simp]: "c1;c2 \<sqsubseteq> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2')"
1.139 +by (cases c) auto
1.140 +
1.141 +lemma [simp]: "IF b THEN c1 ELSE c2 {S} \<sqsubseteq> c \<longleftrightarrow>
1.142 + (\<exists>c1' c2' S'. c = IF b THEN c1' ELSE c2' {S'} \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2' \<and> S \<sqsubseteq> S')"
1.143 +by (cases c) auto
1.144 +
1.145 +lemma [simp]: "{Inv} WHILE b DO c {P} \<sqsubseteq> w \<longleftrightarrow>
1.146 + (\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<sqsubseteq> c' \<and> Inv \<sqsubseteq> Inv' \<and> P \<sqsubseteq> P')"
1.147 +by (cases w) auto
1.148 +
1.149 +instance
1.150 +proof
1.151 + case goal1 thus ?case by (induct x) auto
1.152 +next
1.153 + case goal2 thus ?case
1.154 + apply(induct x y arbitrary: z rule: le_acom.induct)
1.155 + apply (auto intro: le_trans)
1.156 + done
1.157 +qed
1.158 +
1.159 +end
1.160 +
1.161 +definition Top_acom :: "com \<Rightarrow> ('a::SL_top) acom" ("\<top>\<^sub>c") where
1.162 +"\<top>\<^sub>c = anno \<top>"
1.163 +
1.164 +lemma strip_Top_acom[simp]: "strip (\<top>\<^sub>c c) = c"
1.165 +by(simp add: Top_acom_def)
1.166 +
1.167 +lemma le_Top_acomp[simp]: "strip c' = c \<Longrightarrow> c' \<sqsubseteq> \<top>\<^sub>c c"
1.168 +by(induct c' arbitrary: c) (auto simp: Top_acom_def)
1.169 +
1.170 +
1.171 +subsubsection "Lifting"
1.172 +
1.173 +datatype 'a up = Bot | Up 'a
1.174 +
1.175 +instantiation up :: (SL_top)SL_top
1.176 +begin
1.177 +
1.178 +fun le_up where
1.179 +"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
1.180 +"Bot \<sqsubseteq> y = True" |
1.181 +"Up _ \<sqsubseteq> Bot = False"
1.182 +
1.183 +lemma [simp]: "(x \<sqsubseteq> Bot) = (x = Bot)"
1.184 +by (cases x) simp_all
1.185 +
1.186 +lemma [simp]: "(Up x \<sqsubseteq> u) = (\<exists>y. u = Up y & x \<sqsubseteq> y)"
1.187 +by (cases u) auto
1.188 +
1.189 +fun join_up where
1.190 +"Up x \<squnion> Up y = Up(x \<squnion> y)" |
1.191 +"Bot \<squnion> y = y" |
1.192 +"x \<squnion> Bot = x"
1.193 +
1.194 +lemma [simp]: "x \<squnion> Bot = x"
1.195 +by (cases x) simp_all
1.196 +
1.197 +definition "\<top> = Up \<top>"
1.198 +
1.199 +instance proof
1.200 + case goal1 show ?case by(cases x, simp_all)
1.201 +next
1.202 + case goal2 thus ?case
1.203 + by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
1.204 +next
1.205 + case goal3 thus ?case by(cases x, simp, cases y, simp_all)
1.206 +next
1.207 + case goal4 thus ?case by(cases y, simp, cases x, simp_all)
1.208 +next
1.209 + case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
1.210 +next
1.211 + case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
1.212 +qed
1.213 +
1.214 +end
1.215 +
1.216 +definition bot_acom :: "com \<Rightarrow> ('a::SL_top)up acom" ("\<bottom>\<^sub>c") where
1.217 +"\<bottom>\<^sub>c = anno Bot"
1.218 +
1.219 +lemma strip_bot_acom[simp]: "strip(\<bottom>\<^sub>c c) = c"
1.220 +by(simp add: bot_acom_def)
1.221 +
1.222 +
1.223 +subsection "Absract Interpretation"
1.224 +
1.225 +text{* The representation of abstract by a set of concrete values: *}
1.226 +
1.227 +locale Rep =
1.228 +fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
1.229 +assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
1.230 +and rep_Top: "rep \<top> = UNIV"
1.231 +begin
1.232 +
1.233 +abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
1.234 +
1.235 +lemma in_rep_Top[simp]: "x <: \<top>"
1.236 +by(simp add: rep_Top)
1.237 +
1.238 +end
1.239 +
1.240 +definition rep_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
1.241 +"rep_fun rep F = {f. \<forall>x. f x \<in> rep(F x)}"
1.242 +
1.243 +fun rep_up :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a up \<Rightarrow> 'b set" where
1.244 +"rep_up rep Bot = {}" |
1.245 +"rep_up rep (Up a) = rep a"
1.246 +
1.247 +text{* The interface for abstract values: *}
1.248 +
1.249 +(* FIXME: separate Rep interface needed? *)
1.250 +locale Val_abs = Rep rep for rep :: "'a::SL_top \<Rightarrow> val set" +
1.251 +fixes num' :: "val \<Rightarrow> 'a"
1.252 +and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.253 +assumes rep_num': "n <: num' n"
1.254 +and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
1.255 +and mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
1.256 +
1.257 +
1.258 +subsubsection "Post-fixed point iteration"
1.259 +
1.260 +fun iter :: "nat \<Rightarrow> (('a::SL_top) acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
1.261 +"iter 0 f c = \<top>\<^sub>c (strip c)" |
1.262 +"iter (Suc n) f c = (let fc = f c in if fc \<sqsubseteq> c then c else iter n f fc)"
1.263 +(* code lemma?? *)
1.264 +
1.265 +lemma strip_iter: assumes "\<forall>c. strip(f c) = strip c"
1.266 +shows "strip(iter n f c) = strip c"
1.267 +apply (induction n arbitrary: c)
1.268 + apply (metis iter.simps(1) strip_Top_acom)
1.269 +apply (simp add:Let_def)
1.270 +by (metis assms)
1.271 +
1.272 +lemma iter_pfp: assumes "\<forall>c. strip(f c) = strip c"
1.273 +shows "f(iter n f c) \<sqsubseteq> iter n f c"
1.274 +apply (induction n arbitrary: c)
1.275 + apply(simp add: assms)
1.276 +apply (simp add:Let_def)
1.277 +done
1.278 +
1.279 +lemma iter_funpow: assumes "\<forall>c. strip(f c) = strip c"
1.280 +shows "iter n f x \<noteq> \<top>\<^sub>c (strip x) \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
1.281 +apply(induction n arbitrary: x)
1.282 + apply simp
1.283 +apply (auto simp: Let_def assms)
1.284 + apply(metis funpow.simps(1) id_def)
1.285 +by (metis assms funpow.simps(2) funpow_swap1 o_apply)
1.286 +
1.287 +text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
1.288 +post-fixed point above @{text x0}, unless it yields @{text Top}. *}
1.289 +
1.290 +lemma iter_least_pfp:
1.291 +assumes strip: "\<forall>c. strip(f c) = strip c"
1.292 +and mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
1.293 +and not_top: "iter n f x0 \<noteq> \<top>\<^sub>c (strip x0)"
1.294 +and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
1.295 +proof-
1.296 + obtain k where "iter n f x0 = (f^^k) x0"
1.297 + using iter_funpow[OF strip not_top] by blast
1.298 + moreover
1.299 + { fix n have "(f^^n) x0 \<sqsubseteq> p"
1.300 + proof(induction n)
1.301 + case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
1.302 + next
1.303 + case (Suc n) thus ?case
1.304 + by (simp add: `x0 \<sqsubseteq> p`)(metis Suc `f p \<sqsubseteq> p` le_trans mono)
1.305 + qed
1.306 + } ultimately show ?thesis by simp
1.307 +qed
1.308 +
1.309 +type_synonym 'a st = "(name \<Rightarrow> 'a)"
1.310 +
1.311 +locale Abs_Int_Fun = Val_abs +
1.312 +fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
1.313 +assumes pfp: "f(pfp f c) \<sqsubseteq> pfp f c"
1.314 +and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
1.315 +begin
1.316 +
1.317 +fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
1.318 +"aval' (N n) _ = num' n" |
1.319 +"aval' (V x) S = S x" |
1.320 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
1.321 +
1.322 +fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
1.323 +"step S (SKIP {P}) = (SKIP {S})" |
1.324 +"step S (x ::= e {P}) =
1.325 + x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(S(x := aval' e S))}" |
1.326 +"step S (c1; c2) = step S c1; step (post c1) c2" |
1.327 +"step S (IF b THEN c1 ELSE c2 {P}) =
1.328 + (let c1' = step S c1; c2' = step S c2
1.329 + in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
1.330 +"step S ({Inv} WHILE b DO c {P}) =
1.331 + {S \<squnion> post c} WHILE b DO (step Inv c) {Inv}"
1.332 +
1.333 +lemma strip_step[simp]: "strip(step S c) = strip c"
1.334 +by(induct c arbitrary: S) (simp_all add: Let_def)
1.335 +
1.336 +
1.337 +definition AI :: "com \<Rightarrow> 'a st up acom" where
1.338 +"AI c = pfp (step \<top>) (\<bottom>\<^sub>c c)"
1.339 +
1.340 +
1.341 +abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
1.342 +"s <:f S == s \<in> rep_fun rep S"
1.343 +
1.344 +notation fun_in_rep (infix "<:\<^sub>f" 50)
1.345 +
1.346 +lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
1.347 +by(auto simp add: rep_fun_def le_fun_def dest: le_rep)
1.348 +
1.349 +abbreviation up_in_rep :: "state \<Rightarrow> 'a st up \<Rightarrow> bool" (infix "<:up" 50) where
1.350 +"s <:up S == s : rep_up (rep_fun rep) S"
1.351 +
1.352 +notation (output) up_in_rep (infix "<:\<^sub>u\<^sub>p" 50)
1.353 +
1.354 +lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
1.355 +by (cases S) (auto intro:fun_in_rep_le)
1.356 +
1.357 +lemma in_rep_Top_fun: "s <:f Top"
1.358 +by(simp add: Top_fun_def rep_fun_def)
1.359 +
1.360 +lemma in_rep_Top_up: "s <:up Top"
1.361 +by(simp add: Top_up_def in_rep_Top_fun)
1.362 +
1.363 +
1.364 +subsubsection "Monotonicity"
1.365 +
1.366 +lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
1.367 +by(induction e)(auto simp: le_fun_def mono_plus')
1.368 +
1.369 +lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
1.370 +by(simp add: le_fun_def)
1.371 +
1.372 +lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
1.373 +apply(induction c arbitrary: S S')
1.374 +apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
1.375 +done
1.376 +
1.377 +subsubsection "Soundness"
1.378 +
1.379 +lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
1.380 +by (induct a) (auto simp: rep_num' rep_plus' rep_fun_def)
1.381 +
1.382 +lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f S(x := a)"
1.383 +by(simp add: rep_fun_def)
1.384 +
1.385 +lemma step_sound:
1.386 + "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
1.387 +proof(induction c arbitrary: S s t)
1.388 + case SKIP thus ?case
1.389 + by simp (metis skipE up_fun_in_rep_le)
1.390 +next
1.391 + case Assign thus ?case
1.392 + apply (auto simp del: fun_upd_apply split: up.splits)
1.393 + by (metis aval'_sound fun_in_rep_le in_rep_update)
1.394 +next
1.395 + case Semi thus ?case by simp blast
1.396 +next
1.397 + case (If b c1 c2 S0) thus ?case
1.398 + apply(auto simp: Let_def)
1.399 + apply (metis up_fun_in_rep_le)+
1.400 + done
1.401 +next
1.402 + case (While Inv b c P)
1.403 + from While.prems have inv: "step Inv c \<sqsubseteq> c"
1.404 + and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def)
1.405 + { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
1.406 + proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
1.407 + case WhileFalse thus ?case by simp
1.408 + next
1.409 + case (WhileTrue s1 s2 s3)
1.410 + from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` `s1 <:up Inv`] `post c \<sqsubseteq> Inv`]]
1.411 + show ?case .
1.412 + qed
1.413 + }
1.414 + thus ?case using While.prems(2)
1.415 + by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
1.416 +qed
1.417 +
1.418 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
1.419 +by(auto simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp)
1.420 +
1.421 +end
1.422 +
1.423 +text{* Problem: not executable because of the comparison of abstract states,
1.424 +i.e. functions, in the post-fixedpoint computation. *}
1.425 +
1.426 +end