1.1 --- a/src/HOL/IMP/Big_Step.thy Sat Aug 06 15:48:08 2011 +0200
1.2 +++ b/src/HOL/IMP/Big_Step.thy Mon Aug 08 16:47:55 2011 +0200
1.3 @@ -113,6 +113,10 @@
1.4 qed
1.5 qed
1.6
1.7 +(* Using rule inversion to prove simplification rules: *)
1.8 +lemma assign_simp:
1.9 + "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
1.10 + by auto
1.11
1.12 subsection "Command Equivalence"
1.13
2.1 --- a/src/HOL/IMP/Comp_Rev.thy Sat Aug 06 15:48:08 2011 +0200
2.2 +++ b/src/HOL/IMP/Comp_Rev.thy Mon Aug 08 16:47:55 2011 +0200
2.3 @@ -479,9 +479,7 @@
2.4 "ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s"
2.5 by (induct c) auto
2.6
2.7 -lemma assign [simp]:
2.8 - "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
2.9 - by auto
2.10 +declare assign_simp [simp]
2.11
2.12 lemma ccomp_exec_n:
2.13 "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/IMP/Fold.thy Mon Aug 08 16:47:55 2011 +0200
3.3 @@ -0,0 +1,413 @@
3.4 +header "Constant Folding"
3.5 +
3.6 +theory Fold imports Sem_Equiv begin
3.7 +
3.8 +section "Simple folding of arithmetic expressions"
3.9 +
3.10 +types
3.11 + tab = "name \<Rightarrow> val option"
3.12 +
3.13 +(* maybe better as the composition of substitution and the existing simp_const(0) *)
3.14 +fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
3.15 +"simp_const (N n) _ = N n" |
3.16 +"simp_const (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |
3.17 +"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of
3.18 + (N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')"
3.19 +
3.20 +definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)"
3.21 +
3.22 +theorem aval_simp_const[simp]:
3.23 +assumes "approx t s"
3.24 +shows "aval (simp_const a t) s = aval a s"
3.25 + using assms
3.26 + by (induct a) (auto simp: approx_def split: aexp.split option.split)
3.27 +
3.28 +theorem aval_simp_const_N:
3.29 +assumes "approx t s"
3.30 +shows "simp_const a t = N n \<Longrightarrow> aval a s = n"
3.31 + using assms
3.32 + by (induct a arbitrary: n)
3.33 + (auto simp: approx_def split: aexp.splits option.splits)
3.34 +
3.35 +definition
3.36 + "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"
3.37 +
3.38 +primrec lnames :: "com \<Rightarrow> name set" where
3.39 +"lnames SKIP = {}" |
3.40 +"lnames (x ::= a) = {x}" |
3.41 +"lnames (c1; c2) = lnames c1 \<union> lnames c2" |
3.42 +"lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2" |
3.43 +"lnames (WHILE b DO c) = lnames c"
3.44 +
3.45 +primrec "defs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
3.46 +"defs SKIP t = t" |
3.47 +"defs (x ::= a) t =
3.48 + (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
3.49 +"defs (c1;c2) t = (defs c2 o defs c1) t" |
3.50 +"defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
3.51 +"defs (WHILE b DO c) t = t |` (-lnames c)"
3.52 +
3.53 +primrec fold where
3.54 +"fold SKIP _ = SKIP" |
3.55 +"fold (x ::= a) t = (x ::= (simp_const a t))" |
3.56 +"fold (c1;c2) t = (fold c1 t; fold c2 (defs c1 t))" |
3.57 +"fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" |
3.58 +"fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lnames c))"
3.59 +
3.60 +lemma approx_merge:
3.61 + "approx t1 s \<or> approx t2 s \<Longrightarrow> approx (merge t1 t2) s"
3.62 + by (fastsimp simp: merge_def approx_def)
3.63 +
3.64 +lemma approx_map_le:
3.65 + "approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s"
3.66 + by (clarsimp simp: approx_def map_le_def dom_def)
3.67 +
3.68 +lemma restrict_map_le [intro!, simp]: "t |` S \<subseteq>\<^sub>m t"
3.69 + by (clarsimp simp: restrict_map_def map_le_def)
3.70 +
3.71 +lemma merge_restrict:
3.72 + assumes "t1 |` S = t |` S"
3.73 + assumes "t2 |` S = t |` S"
3.74 + shows "merge t1 t2 |` S = t |` S"
3.75 +proof -
3.76 + from assms
3.77 + have "\<forall>x. (t1 |` S) x = (t |` S) x"
3.78 + and "\<forall>x. (t2 |` S) x = (t |` S) x" by auto
3.79 + thus ?thesis
3.80 + by (auto simp: merge_def restrict_map_def
3.81 + split: if_splits intro: ext)
3.82 +qed
3.83 +
3.84 +
3.85 +lemma defs_restrict:
3.86 + "defs c t |` (- lnames c) = t |` (- lnames c)"
3.87 +proof (induct c arbitrary: t)
3.88 + case (Semi c1 c2)
3.89 + hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)"
3.90 + by simp
3.91 + hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
3.92 + t |` (- lnames c1) |` (-lnames c2)" by simp
3.93 + moreover
3.94 + from Semi
3.95 + have "defs c2 (defs c1 t) |` (- lnames c2) =
3.96 + defs c1 t |` (- lnames c2)"
3.97 + by simp
3.98 + hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) =
3.99 + defs c1 t |` (- lnames c2) |` (- lnames c1)"
3.100 + by simp
3.101 + ultimately
3.102 + show ?case by (clarsimp simp: Int_commute)
3.103 +next
3.104 + case (If b c1 c2)
3.105 + hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
3.106 + hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
3.107 + t |` (- lnames c1) |` (-lnames c2)" by simp
3.108 + moreover
3.109 + from If
3.110 + have "defs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
3.111 + hence "defs c2 t |` (- lnames c2) |` (-lnames c1) =
3.112 + t |` (- lnames c2) |` (-lnames c1)" by simp
3.113 + ultimately
3.114 + show ?case by (auto simp: Int_commute intro: merge_restrict)
3.115 +qed (auto split: aexp.split)
3.116 +
3.117 +
3.118 +lemma big_step_pres_approx:
3.119 + "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"
3.120 +proof (induct arbitrary: t rule: big_step_induct)
3.121 + case Skip thus ?case by simp
3.122 +next
3.123 + case Assign
3.124 + thus ?case
3.125 + by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
3.126 +next
3.127 + case (Semi c1 s1 s2 c2 s3)
3.128 + have "approx (defs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
3.129 + hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi(4))
3.130 + thus ?case by simp
3.131 +next
3.132 + case (IfTrue b s c1 s')
3.133 + hence "approx (defs c1 t) s'" by simp
3.134 + thus ?case by (simp add: approx_merge)
3.135 +next
3.136 + case (IfFalse b s c2 s')
3.137 + hence "approx (defs c2 t) s'" by simp
3.138 + thus ?case by (simp add: approx_merge)
3.139 +next
3.140 + case WhileFalse
3.141 + thus ?case by (simp add: approx_def restrict_map_def)
3.142 +next
3.143 + case (WhileTrue b s1 c s2 s3)
3.144 + hence "approx (defs c t) s2" by simp
3.145 + with WhileTrue
3.146 + have "approx (defs c t |` (-lnames c)) s3" by simp
3.147 + thus ?case by (simp add: defs_restrict)
3.148 +qed
3.149 +
3.150 +corollary approx_defs_inv [simp]:
3.151 + "\<Turnstile> {approx t} c {approx (defs c t)}"
3.152 + by (simp add: hoare_valid_def big_step_pres_approx)
3.153 +
3.154 +
3.155 +lemma big_step_pres_approx_restrict:
3.156 + "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
3.157 +proof (induct arbitrary: t rule: big_step_induct)
3.158 + case Assign
3.159 + thus ?case by (clarsimp simp: approx_def)
3.160 +next
3.161 + case (Semi c1 s1 s2 c2 s3)
3.162 + hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1"
3.163 + by (simp add: Int_commute)
3.164 + hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
3.165 + by (rule Semi)
3.166 + hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2"
3.167 + by (simp add: Int_commute)
3.168 + hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3"
3.169 + by (rule Semi)
3.170 + thus ?case by simp
3.171 +next
3.172 + case (IfTrue b s c1 s' c2)
3.173 + hence "approx (t |` (-lnames c2) |` (-lnames c1)) s"
3.174 + by (simp add: Int_commute)
3.175 + hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'"
3.176 + by (rule IfTrue)
3.177 + thus ?case by (simp add: Int_commute)
3.178 +next
3.179 + case (IfFalse b s c2 s' c1)
3.180 + hence "approx (t |` (-lnames c1) |` (-lnames c2)) s"
3.181 + by simp
3.182 + hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'"
3.183 + by (rule IfFalse)
3.184 + thus ?case by simp
3.185 +qed auto
3.186 +
3.187 +
3.188 +lemma approx_restrict_inv:
3.189 + "\<Turnstile> {approx (t |` (-lnames c))} c {approx (t |` (-lnames c))}"
3.190 + by (simp add: hoare_valid_def big_step_pres_approx_restrict)
3.191 +
3.192 +declare assign_simp [simp]
3.193 +
3.194 +lemma approx_eq:
3.195 + "approx t \<Turnstile> c \<sim> fold c t"
3.196 +proof (induct c arbitrary: t)
3.197 + case SKIP show ?case by simp
3.198 +next
3.199 + case Assign
3.200 + show ?case by (simp add: equiv_up_to_def)
3.201 +next
3.202 + case Semi
3.203 + thus ?case by (auto intro!: equiv_up_to_semi)
3.204 +next
3.205 + case If
3.206 + thus ?case by (auto intro!: equiv_up_to_if_weak)
3.207 +next
3.208 + case (While b c)
3.209 + hence "approx (t |` (- lnames c)) \<Turnstile>
3.210 + WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lnames c))"
3.211 + by (auto intro: equiv_up_to_while_weak approx_restrict_inv)
3.212 + thus ?case
3.213 + by (auto intro: equiv_up_to_weaken approx_map_le)
3.214 +qed
3.215 +
3.216 +
3.217 +lemma approx_empty [simp]:
3.218 + "approx empty = (\<lambda>_. True)"
3.219 + by (auto intro!: ext simp: approx_def)
3.220 +
3.221 +lemma equiv_sym:
3.222 + "c \<sim> c' \<longleftrightarrow> c' \<sim> c"
3.223 + by (auto simp add: equiv_def)
3.224 +
3.225 +theorem constant_folding_equiv:
3.226 + "fold c empty \<sim> c"
3.227 + using approx_eq [of empty c]
3.228 + by (simp add: equiv_up_to_True equiv_sym)
3.229 +
3.230 +
3.231 +
3.232 +section {* More ambitious folding including boolean expressions *}
3.233 +
3.234 +
3.235 +fun bsimp_const :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where
3.236 +"bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" |
3.237 +"bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" |
3.238 +"bsimp_const (Not b) t = not(bsimp_const b t)" |
3.239 +"bsimp_const (B bv) _ = B bv"
3.240 +
3.241 +theorem bvalsimp_const [simp]:
3.242 + assumes "approx t s"
3.243 + shows "bval (bsimp_const b t) s = bval b s"
3.244 + using assms by (induct b) auto
3.245 +
3.246 +lemma not_B [simp]: "not (B v) = B (\<not>v)"
3.247 + by (cases v) auto
3.248 +
3.249 +lemma not_B_eq [simp]: "(not b = B v) = (b = B (\<not>v))"
3.250 + by (cases b) auto
3.251 +
3.252 +lemma and_B_eq:
3.253 + "(and a b = B v) = (a = B False \<and> \<not>v \<or>
3.254 + b = B False \<and> \<not>v \<or>
3.255 + (\<exists>v1 v2. a = B v1 \<and> b = B v2 \<and> v = v1 \<and> v2))"
3.256 + by (rule and.induct) auto
3.257 +
3.258 +lemma less_B_eq [simp]:
3.259 + "(less a b = B v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
3.260 + by (rule less.induct) auto
3.261 +
3.262 +theorem bvalsimp_const_B:
3.263 +assumes "approx t s"
3.264 +shows "bsimp_const b t = B v \<Longrightarrow> bval b s = v"
3.265 + using assms
3.266 + by (induct b arbitrary: v)
3.267 + (auto simp: approx_def and_B_eq aval_simp_const_N
3.268 + split: bexp.splits bool.splits)
3.269 +
3.270 +
3.271 +primrec "bdefs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
3.272 +"bdefs SKIP t = t" |
3.273 +"bdefs (x ::= a) t =
3.274 + (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
3.275 +"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" |
3.276 +"bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
3.277 + B True \<Rightarrow> bdefs c1 t
3.278 + | B False \<Rightarrow> bdefs c2 t
3.279 + | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
3.280 +"bdefs (WHILE b DO c) t = t |` (-lnames c)"
3.281 +
3.282 +
3.283 +primrec bfold where
3.284 +"bfold SKIP _ = SKIP" |
3.285 +"bfold (x ::= a) t = (x ::= (simp_const a t))" |
3.286 +"bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))" |
3.287 +"bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
3.288 + B True \<Rightarrow> bfold c1 t
3.289 + | B False \<Rightarrow> bfold c2 t
3.290 + | _ \<Rightarrow> IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)" |
3.291 +"bfold (WHILE b DO c) t = (case bsimp_const b t of
3.292 + B False \<Rightarrow> SKIP
3.293 + | _ \<Rightarrow> WHILE bsimp_const b (t |` (-lnames c)) DO bfold c (t |` (-lnames c)))"
3.294 +
3.295 +
3.296 +lemma bdefs_restrict:
3.297 + "bdefs c t |` (- lnames c) = t |` (- lnames c)"
3.298 +proof (induct c arbitrary: t)
3.299 + case (Semi c1 c2)
3.300 + hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)"
3.301 + by simp
3.302 + hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
3.303 + t |` (- lnames c1) |` (-lnames c2)" by simp
3.304 + moreover
3.305 + from Semi
3.306 + have "bdefs c2 (bdefs c1 t) |` (- lnames c2) =
3.307 + bdefs c1 t |` (- lnames c2)"
3.308 + by simp
3.309 + hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) =
3.310 + bdefs c1 t |` (- lnames c2) |` (- lnames c1)"
3.311 + by simp
3.312 + ultimately
3.313 + show ?case by (clarsimp simp: Int_commute)
3.314 +next
3.315 + case (If b c1 c2)
3.316 + hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
3.317 + hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
3.318 + t |` (- lnames c1) |` (-lnames c2)" by simp
3.319 + moreover
3.320 + from If
3.321 + have "bdefs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
3.322 + hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) =
3.323 + t |` (- lnames c2) |` (-lnames c1)" by simp
3.324 + ultimately
3.325 + show ?case
3.326 + by (auto simp: Int_commute intro: merge_restrict
3.327 + split: bexp.splits bool.splits)
3.328 +qed (auto split: aexp.split bexp.split bool.split)
3.329 +
3.330 +
3.331 +lemma big_step_pres_approx_b:
3.332 + "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'"
3.333 +proof (induct arbitrary: t rule: big_step_induct)
3.334 + case Skip thus ?case by simp
3.335 +next
3.336 + case Assign
3.337 + thus ?case
3.338 + by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
3.339 +next
3.340 + case (Semi c1 s1 s2 c2 s3)
3.341 + have "approx (bdefs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
3.342 + hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi(4))
3.343 + thus ?case by simp
3.344 +next
3.345 + case (IfTrue b s c1 s')
3.346 + hence "approx (bdefs c1 t) s'" by simp
3.347 + thus ?case using `bval b s` `approx t s`
3.348 + by (clarsimp simp: approx_merge bvalsimp_const_B
3.349 + split: bexp.splits bool.splits)
3.350 +next
3.351 + case (IfFalse b s c2 s')
3.352 + hence "approx (bdefs c2 t) s'" by simp
3.353 + thus ?case using `\<not>bval b s` `approx t s`
3.354 + by (clarsimp simp: approx_merge bvalsimp_const_B
3.355 + split: bexp.splits bool.splits)
3.356 +next
3.357 + case WhileFalse
3.358 + thus ?case
3.359 + by (clarsimp simp: bvalsimp_const_B approx_def restrict_map_def
3.360 + split: bexp.splits bool.splits)
3.361 +next
3.362 + case (WhileTrue b s1 c s2 s3)
3.363 + hence "approx (bdefs c t) s2" by simp
3.364 + with WhileTrue
3.365 + have "approx (bdefs c t |` (- lnames c)) s3"
3.366 + by simp
3.367 + thus ?case
3.368 + by (simp add: bdefs_restrict)
3.369 +qed
3.370 +
3.371 +corollary approx_bdefs_inv [simp]:
3.372 + "\<Turnstile> {approx t} c {approx (bdefs c t)}"
3.373 + by (simp add: hoare_valid_def big_step_pres_approx_b)
3.374 +
3.375 +lemma bfold_equiv:
3.376 + "approx t \<Turnstile> c \<sim> bfold c t"
3.377 +proof (induct c arbitrary: t)
3.378 + case SKIP show ?case by simp
3.379 +next
3.380 + case Assign
3.381 + thus ?case by (simp add: equiv_up_to_def)
3.382 +next
3.383 + case Semi
3.384 + thus ?case by (auto intro!: equiv_up_to_semi)
3.385 +next
3.386 + case (If b c1 c2)
3.387 + hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim>
3.388 + IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
3.389 + by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def)
3.390 + thus ?case using If
3.391 + by (fastsimp simp: bvalsimp_const_B split: bexp.splits bool.splits
3.392 + intro: equiv_up_to_trans)
3.393 + next
3.394 + case (While b c)
3.395 + hence "approx (t |` (- lnames c)) \<Turnstile>
3.396 + WHILE b DO c \<sim>
3.397 + WHILE bsimp_const b (t |` (- lnames c))
3.398 + DO bfold c (t |` (- lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'")
3.399 + by (auto intro: equiv_up_to_while_weak approx_restrict_inv
3.400 + simp: bequiv_up_to_def)
3.401 + hence "approx t \<Turnstile> ?W \<sim> ?W'"
3.402 + by (auto intro: equiv_up_to_weaken approx_map_le)
3.403 + thus ?case
3.404 + by (auto split: bexp.splits bool.splits
3.405 + intro: equiv_up_to_while_False
3.406 + simp: bvalsimp_const_B)
3.407 +qed
3.408 +
3.409 +
3.410 +theorem constant_bfolding_equiv:
3.411 + "bfold c empty \<sim> c"
3.412 + using bfold_equiv [of empty c]
3.413 + by (simp add: equiv_up_to_True equiv_sym)
3.414 +
3.415 +
3.416 +end
4.1 --- a/src/HOL/IMP/ROOT.ML Sat Aug 06 15:48:08 2011 +0200
4.2 +++ b/src/HOL/IMP/ROOT.ML Mon Aug 08 16:47:55 2011 +0200
4.3 @@ -17,5 +17,6 @@
4.4 "Procs_Stat_Vars_Dyn",
4.5 "Procs_Stat_Vars_Stat",
4.6 "C_like",
4.7 - "OO"
4.8 + "OO",
4.9 + "Fold"
4.10 ];
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/IMP/Sem_Equiv.thy Mon Aug 08 16:47:55 2011 +0200
5.3 @@ -0,0 +1,165 @@
5.4 +header "Semantic Equivalence up to a Condition"
5.5 +
5.6 +theory Sem_Equiv
5.7 +imports Hoare_Sound_Complete
5.8 +begin
5.9 +
5.10 +definition
5.11 + equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60)
5.12 +where
5.13 + "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'"
5.14 +
5.15 +definition
5.16 + bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60)
5.17 +where
5.18 + "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s"
5.19 +
5.20 +lemma equiv_up_to_True:
5.21 + "((\<lambda>_. True) \<Turnstile> c \<sim> c') = (c \<sim> c')"
5.22 + by (simp add: equiv_def equiv_up_to_def)
5.23 +
5.24 +lemma equiv_up_to_weaken:
5.25 + "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P' s \<Longrightarrow> P s) \<Longrightarrow> P' \<Turnstile> c \<sim> c'"
5.26 + by (simp add: equiv_up_to_def)
5.27 +
5.28 +lemma equiv_up_toI:
5.29 + "(\<And>s s'. P s \<Longrightarrow> (c, s) \<Rightarrow> s' = (c', s) \<Rightarrow> s') \<Longrightarrow> P \<Turnstile> c \<sim> c'"
5.30 + by (unfold equiv_up_to_def) blast
5.31 +
5.32 +lemma equiv_up_toD1:
5.33 + "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> (c', s) \<Rightarrow> s'"
5.34 + by (unfold equiv_up_to_def) blast
5.35 +
5.36 +lemma equiv_up_toD2:
5.37 + "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
5.38 + by (unfold equiv_up_to_def) blast
5.39 +
5.40 +
5.41 +lemma equiv_up_to_refl [simp, intro!]:
5.42 + "P \<Turnstile> c \<sim> c"
5.43 + by (auto simp: equiv_up_to_def)
5.44 +
5.45 +lemma equiv_up_to_sym:
5.46 + "(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)"
5.47 + by (auto simp: equiv_up_to_def)
5.48 +
5.49 +lemma equiv_up_to_trans [trans]:
5.50 + "P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''"
5.51 + by (auto simp: equiv_up_to_def)
5.52 +
5.53 +
5.54 +lemma bequiv_up_to_refl [simp, intro!]:
5.55 + "P \<Turnstile> b <\<sim>> b"
5.56 + by (auto simp: bequiv_up_to_def)
5.57 +
5.58 +lemma bequiv_up_to_sym:
5.59 + "(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)"
5.60 + by (auto simp: bequiv_up_to_def)
5.61 +
5.62 +lemma bequiv_up_to_trans [trans]:
5.63 + "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
5.64 + by (auto simp: bequiv_up_to_def)
5.65 +
5.66 +
5.67 +lemma equiv_up_to_hoare:
5.68 + "P' \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
5.69 + unfolding hoare_valid_def equiv_up_to_def by blast
5.70 +
5.71 +lemma equiv_up_to_hoare_eq:
5.72 + "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
5.73 + by (rule equiv_up_to_hoare)
5.74 +
5.75 +
5.76 +lemma equiv_up_to_semi:
5.77 + "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
5.78 + P \<Turnstile> (c; d) \<sim> (c'; d')"
5.79 + by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast
5.80 +
5.81 +lemma equiv_up_to_while_lemma:
5.82 + shows "(d,s) \<Rightarrow> s' \<Longrightarrow>
5.83 + P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
5.84 + (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
5.85 + \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
5.86 + P s \<Longrightarrow>
5.87 + d = WHILE b DO c \<Longrightarrow>
5.88 + (WHILE b' DO c', s) \<Rightarrow> s'"
5.89 +proof (induct rule: big_step_induct)
5.90 + case (WhileTrue b s1 c s2 s3)
5.91 + note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
5.92 +
5.93 + from WhileTrue.prems
5.94 + have "P \<Turnstile> b <\<sim>> b'" by simp
5.95 + with `bval b s1` `P s1`
5.96 + have "bval b' s1" by (simp add: bequiv_up_to_def)
5.97 + moreover
5.98 + from WhileTrue.prems
5.99 + have "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'" by simp
5.100 + with `bval b s1` `P s1` `(c, s1) \<Rightarrow> s2`
5.101 + have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
5.102 + moreover
5.103 + from WhileTrue.prems
5.104 + have "\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" by simp
5.105 + with `P s1` `bval b s1` `(c, s1) \<Rightarrow> s2`
5.106 + have "P s2" by (simp add: hoare_valid_def)
5.107 + hence "(WHILE b' DO c', s2) \<Rightarrow> s3" by (rule IH)
5.108 + ultimately
5.109 + show ?case by blast
5.110 +next
5.111 + case WhileFalse
5.112 + thus ?case by (auto simp: bequiv_up_to_def)
5.113 +qed (fastsimp simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
5.114 +
5.115 +lemma bequiv_context_subst:
5.116 + "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
5.117 + by (auto simp: bequiv_up_to_def)
5.118 +
5.119 +lemma equiv_up_to_while:
5.120 + "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
5.121 + \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow>
5.122 + P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
5.123 + apply (safe intro!: equiv_up_toI)
5.124 + apply (auto intro: equiv_up_to_while_lemma)[1]
5.125 + apply (simp add: equiv_up_to_hoare_eq bequiv_context_subst)
5.126 + apply (drule equiv_up_to_sym [THEN iffD1])
5.127 + apply (drule bequiv_up_to_sym [THEN iffD1])
5.128 + apply (auto intro: equiv_up_to_while_lemma)[1]
5.129 + done
5.130 +
5.131 +lemma equiv_up_to_while_weak:
5.132 + "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow>
5.133 + P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
5.134 + by (fastsimp elim!: equiv_up_to_while equiv_up_to_weaken
5.135 + simp: hoare_valid_def)
5.136 +
5.137 +lemma equiv_up_to_if:
5.138 + "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<inter> bval b \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
5.139 + P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
5.140 + by (auto simp: bequiv_up_to_def equiv_up_to_def)
5.141 +
5.142 +lemma equiv_up_to_if_weak:
5.143 + "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
5.144 + P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
5.145 + by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken)
5.146 +
5.147 +lemma equiv_up_to_if_True [intro!]:
5.148 + "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
5.149 + by (auto simp: equiv_up_to_def)
5.150 +
5.151 +lemma equiv_up_to_if_False [intro!]:
5.152 + "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c2"
5.153 + by (auto simp: equiv_up_to_def)
5.154 +
5.155 +lemma equiv_up_to_while_False [intro!]:
5.156 + "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
5.157 + by (auto simp: equiv_up_to_def)
5.158 +
5.159 +lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (B True) DO c'"
5.160 + by (induct rule: big_step_induct) auto
5.161 +
5.162 +lemma equiv_up_to_while_True [intro!,simp]:
5.163 + "P \<Turnstile> WHILE B True DO c \<sim> WHILE B True DO SKIP"
5.164 + unfolding equiv_up_to_def
5.165 + by (blast dest: while_never)
5.166 +
5.167 +
5.168 +end
5.169 \ No newline at end of file