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