author kleing Mon Aug 08 16:47:55 2011 +0200 (2011-08-08) changeset 44070 cebb7abb54b1 parent 44069 d7c7ec248ef0 child 44071 9ee98b584494 child 44084 caac24afcadb
import constant folding theory into IMP
 src/HOL/IMP/Big_Step.thy file | annotate | diff | revisions src/HOL/IMP/Comp_Rev.thy file | annotate | diff | revisions src/HOL/IMP/Fold.thy file | annotate | diff | revisions src/HOL/IMP/ROOT.ML file | annotate | diff | revisions src/HOL/IMP/Sem_Equiv.thy file | annotate | diff | revisions
```     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.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
```