44070

1 
header "Constant Folding"


2 


3 
theory Fold imports Sem_Equiv begin


4 

44850

5 
subsection "Simple folding of arithmetic expressions"

44070

6 


7 
types


8 
tab = "name \<Rightarrow> val option"


9 


10 
(* maybe better as the composition of substitution and the existing simp_const(0) *)


11 
fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where


12 
"simp_const (N n) _ = N n" 


13 
"simp_const (V x) t = (case t x of None \<Rightarrow> V x  Some k \<Rightarrow> N k)" 


14 
"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of


15 
(N n1, N n2) \<Rightarrow> N(n1+n2)  (e1',e2') \<Rightarrow> Plus e1' e2')"


16 


17 
definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)"


18 


19 
theorem aval_simp_const[simp]:


20 
assumes "approx t s"


21 
shows "aval (simp_const a t) s = aval a s"


22 
using assms


23 
by (induct a) (auto simp: approx_def split: aexp.split option.split)


24 


25 
theorem aval_simp_const_N:


26 
assumes "approx t s"


27 
shows "simp_const a t = N n \<Longrightarrow> aval a s = n"


28 
using assms


29 
by (induct a arbitrary: n)


30 
(auto simp: approx_def split: aexp.splits option.splits)


31 


32 
definition


33 
"merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"


34 


35 
primrec lnames :: "com \<Rightarrow> name set" where


36 
"lnames SKIP = {}" 


37 
"lnames (x ::= a) = {x}" 


38 
"lnames (c1; c2) = lnames c1 \<union> lnames c2" 


39 
"lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2" 


40 
"lnames (WHILE b DO c) = lnames c"


41 


42 
primrec "defs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where


43 
"defs SKIP t = t" 


44 
"defs (x ::= a) t =


45 
(case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k)  _ \<Rightarrow> t(x:=None))" 


46 
"defs (c1;c2) t = (defs c2 o defs c1) t" 


47 
"defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" 


48 
"defs (WHILE b DO c) t = t ` (lnames c)"


49 


50 
primrec fold where


51 
"fold SKIP _ = SKIP" 


52 
"fold (x ::= a) t = (x ::= (simp_const a t))" 


53 
"fold (c1;c2) t = (fold c1 t; fold c2 (defs c1 t))" 


54 
"fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" 


55 
"fold (WHILE b DO c) t = WHILE b DO fold c (t ` (lnames c))"


56 


57 
lemma approx_merge:


58 
"approx t1 s \<or> approx t2 s \<Longrightarrow> approx (merge t1 t2) s"


59 
by (fastsimp simp: merge_def approx_def)


60 


61 
lemma approx_map_le:


62 
"approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s"


63 
by (clarsimp simp: approx_def map_le_def dom_def)


64 


65 
lemma restrict_map_le [intro!, simp]: "t ` S \<subseteq>\<^sub>m t"


66 
by (clarsimp simp: restrict_map_def map_le_def)


67 


68 
lemma merge_restrict:


69 
assumes "t1 ` S = t ` S"


70 
assumes "t2 ` S = t ` S"


71 
shows "merge t1 t2 ` S = t ` S"


72 
proof 


73 
from assms


74 
have "\<forall>x. (t1 ` S) x = (t ` S) x"


75 
and "\<forall>x. (t2 ` S) x = (t ` S) x" by auto


76 
thus ?thesis


77 
by (auto simp: merge_def restrict_map_def


78 
split: if_splits intro: ext)


79 
qed


80 


81 


82 
lemma defs_restrict:


83 
"defs c t ` ( lnames c) = t ` ( lnames c)"


84 
proof (induct c arbitrary: t)


85 
case (Semi c1 c2)


86 
hence "defs c1 t ` ( lnames c1) = t ` ( lnames c1)"


87 
by simp


88 
hence "defs c1 t ` ( lnames c1) ` (lnames c2) =


89 
t ` ( lnames c1) ` (lnames c2)" by simp


90 
moreover


91 
from Semi


92 
have "defs c2 (defs c1 t) ` ( lnames c2) =


93 
defs c1 t ` ( lnames c2)"


94 
by simp


95 
hence "defs c2 (defs c1 t) ` ( lnames c2) ` ( lnames c1) =


96 
defs c1 t ` ( lnames c2) ` ( lnames c1)"


97 
by simp


98 
ultimately


99 
show ?case by (clarsimp simp: Int_commute)


100 
next


101 
case (If b c1 c2)


102 
hence "defs c1 t ` ( lnames c1) = t ` ( lnames c1)" by simp


103 
hence "defs c1 t ` ( lnames c1) ` (lnames c2) =


104 
t ` ( lnames c1) ` (lnames c2)" by simp


105 
moreover


106 
from If


107 
have "defs c2 t ` ( lnames c2) = t ` ( lnames c2)" by simp


108 
hence "defs c2 t ` ( lnames c2) ` (lnames c1) =


109 
t ` ( lnames c2) ` (lnames c1)" by simp


110 
ultimately


111 
show ?case by (auto simp: Int_commute intro: merge_restrict)


112 
qed (auto split: aexp.split)


113 


114 


115 
lemma big_step_pres_approx:


116 
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"


117 
proof (induct arbitrary: t rule: big_step_induct)


118 
case Skip thus ?case by simp


119 
next


120 
case Assign


121 
thus ?case


122 
by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)


123 
next


124 
case (Semi c1 s1 s2 c2 s3)


125 
have "approx (defs c1 t) s2" by (rule Semi(2) [OF Semi.prems])


126 
hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi(4))


127 
thus ?case by simp


128 
next


129 
case (IfTrue b s c1 s')


130 
hence "approx (defs c1 t) s'" by simp


131 
thus ?case by (simp add: approx_merge)


132 
next


133 
case (IfFalse b s c2 s')


134 
hence "approx (defs c2 t) s'" by simp


135 
thus ?case by (simp add: approx_merge)


136 
next


137 
case WhileFalse


138 
thus ?case by (simp add: approx_def restrict_map_def)


139 
next


140 
case (WhileTrue b s1 c s2 s3)


141 
hence "approx (defs c t) s2" by simp


142 
with WhileTrue


143 
have "approx (defs c t ` (lnames c)) s3" by simp


144 
thus ?case by (simp add: defs_restrict)


145 
qed


146 


147 
corollary approx_defs_inv [simp]:


148 
"\<Turnstile> {approx t} c {approx (defs c t)}"


149 
by (simp add: hoare_valid_def big_step_pres_approx)


150 


151 


152 
lemma big_step_pres_approx_restrict:


153 
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t ` (lnames c)) s \<Longrightarrow> approx (t ` (lnames c)) s'"


154 
proof (induct arbitrary: t rule: big_step_induct)


155 
case Assign


156 
thus ?case by (clarsimp simp: approx_def)


157 
next


158 
case (Semi c1 s1 s2 c2 s3)


159 
hence "approx (t ` (lnames c2) ` (lnames c1)) s1"


160 
by (simp add: Int_commute)


161 
hence "approx (t ` (lnames c2) ` (lnames c1)) s2"


162 
by (rule Semi)


163 
hence "approx (t ` (lnames c1) ` (lnames c2)) s2"


164 
by (simp add: Int_commute)


165 
hence "approx (t ` (lnames c1) ` (lnames c2)) s3"


166 
by (rule Semi)


167 
thus ?case by simp


168 
next


169 
case (IfTrue b s c1 s' c2)


170 
hence "approx (t ` (lnames c2) ` (lnames c1)) s"


171 
by (simp add: Int_commute)


172 
hence "approx (t ` (lnames c2) ` (lnames c1)) s'"


173 
by (rule IfTrue)


174 
thus ?case by (simp add: Int_commute)


175 
next


176 
case (IfFalse b s c2 s' c1)


177 
hence "approx (t ` (lnames c1) ` (lnames c2)) s"


178 
by simp


179 
hence "approx (t ` (lnames c1) ` (lnames c2)) s'"


180 
by (rule IfFalse)


181 
thus ?case by simp


182 
qed auto


183 


184 


185 
lemma approx_restrict_inv:


186 
"\<Turnstile> {approx (t ` (lnames c))} c {approx (t ` (lnames c))}"


187 
by (simp add: hoare_valid_def big_step_pres_approx_restrict)


188 


189 
declare assign_simp [simp]


190 


191 
lemma approx_eq:


192 
"approx t \<Turnstile> c \<sim> fold c t"


193 
proof (induct c arbitrary: t)


194 
case SKIP show ?case by simp


195 
next


196 
case Assign


197 
show ?case by (simp add: equiv_up_to_def)


198 
next


199 
case Semi


200 
thus ?case by (auto intro!: equiv_up_to_semi)


201 
next


202 
case If


203 
thus ?case by (auto intro!: equiv_up_to_if_weak)


204 
next


205 
case (While b c)


206 
hence "approx (t ` ( lnames c)) \<Turnstile>


207 
WHILE b DO c \<sim> WHILE b DO fold c (t ` ( lnames c))"


208 
by (auto intro: equiv_up_to_while_weak approx_restrict_inv)


209 
thus ?case


210 
by (auto intro: equiv_up_to_weaken approx_map_le)


211 
qed


212 


213 


214 
lemma approx_empty [simp]:


215 
"approx empty = (\<lambda>_. True)"


216 
by (auto intro!: ext simp: approx_def)


217 


218 
lemma equiv_sym:


219 
"c \<sim> c' \<longleftrightarrow> c' \<sim> c"


220 
by (auto simp add: equiv_def)


221 


222 
theorem constant_folding_equiv:


223 
"fold c empty \<sim> c"


224 
using approx_eq [of empty c]


225 
by (simp add: equiv_up_to_True equiv_sym)


226 


227 


228 

44850

229 
subsection {* More ambitious folding including boolean expressions *}

44070

230 


231 


232 
fun bsimp_const :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where


233 
"bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" 


234 
"bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" 


235 
"bsimp_const (Not b) t = not(bsimp_const b t)" 


236 
"bsimp_const (B bv) _ = B bv"


237 


238 
theorem bvalsimp_const [simp]:


239 
assumes "approx t s"


240 
shows "bval (bsimp_const b t) s = bval b s"


241 
using assms by (induct b) auto


242 


243 
lemma not_B [simp]: "not (B v) = B (\<not>v)"


244 
by (cases v) auto


245 


246 
lemma not_B_eq [simp]: "(not b = B v) = (b = B (\<not>v))"


247 
by (cases b) auto


248 


249 
lemma and_B_eq:


250 
"(and a b = B v) = (a = B False \<and> \<not>v \<or>


251 
b = B False \<and> \<not>v \<or>


252 
(\<exists>v1 v2. a = B v1 \<and> b = B v2 \<and> v = v1 \<and> v2))"


253 
by (rule and.induct) auto


254 


255 
lemma less_B_eq [simp]:


256 
"(less a b = B v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"


257 
by (rule less.induct) auto


258 


259 
theorem bvalsimp_const_B:


260 
assumes "approx t s"


261 
shows "bsimp_const b t = B v \<Longrightarrow> bval b s = v"


262 
using assms


263 
by (induct b arbitrary: v)


264 
(auto simp: approx_def and_B_eq aval_simp_const_N


265 
split: bexp.splits bool.splits)


266 


267 


268 
primrec "bdefs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where


269 
"bdefs SKIP t = t" 


270 
"bdefs (x ::= a) t =


271 
(case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k)  _ \<Rightarrow> t(x:=None))" 


272 
"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" 


273 
"bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of


274 
B True \<Rightarrow> bdefs c1 t


275 
 B False \<Rightarrow> bdefs c2 t


276 
 _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" 


277 
"bdefs (WHILE b DO c) t = t ` (lnames c)"


278 


279 


280 
primrec bfold where


281 
"bfold SKIP _ = SKIP" 


282 
"bfold (x ::= a) t = (x ::= (simp_const a t))" 


283 
"bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))" 


284 
"bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of


285 
B True \<Rightarrow> bfold c1 t


286 
 B False \<Rightarrow> bfold c2 t


287 
 _ \<Rightarrow> IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)" 


288 
"bfold (WHILE b DO c) t = (case bsimp_const b t of


289 
B False \<Rightarrow> SKIP


290 
 _ \<Rightarrow> WHILE bsimp_const b (t ` (lnames c)) DO bfold c (t ` (lnames c)))"


291 


292 


293 
lemma bdefs_restrict:


294 
"bdefs c t ` ( lnames c) = t ` ( lnames c)"


295 
proof (induct c arbitrary: t)


296 
case (Semi c1 c2)


297 
hence "bdefs c1 t ` ( lnames c1) = t ` ( lnames c1)"


298 
by simp


299 
hence "bdefs c1 t ` ( lnames c1) ` (lnames c2) =


300 
t ` ( lnames c1) ` (lnames c2)" by simp


301 
moreover


302 
from Semi


303 
have "bdefs c2 (bdefs c1 t) ` ( lnames c2) =


304 
bdefs c1 t ` ( lnames c2)"


305 
by simp


306 
hence "bdefs c2 (bdefs c1 t) ` ( lnames c2) ` ( lnames c1) =


307 
bdefs c1 t ` ( lnames c2) ` ( lnames c1)"


308 
by simp


309 
ultimately


310 
show ?case by (clarsimp simp: Int_commute)


311 
next


312 
case (If b c1 c2)


313 
hence "bdefs c1 t ` ( lnames c1) = t ` ( lnames c1)" by simp


314 
hence "bdefs c1 t ` ( lnames c1) ` (lnames c2) =


315 
t ` ( lnames c1) ` (lnames c2)" by simp


316 
moreover


317 
from If


318 
have "bdefs c2 t ` ( lnames c2) = t ` ( lnames c2)" by simp


319 
hence "bdefs c2 t ` ( lnames c2) ` (lnames c1) =


320 
t ` ( lnames c2) ` (lnames c1)" by simp


321 
ultimately


322 
show ?case


323 
by (auto simp: Int_commute intro: merge_restrict


324 
split: bexp.splits bool.splits)


325 
qed (auto split: aexp.split bexp.split bool.split)


326 


327 


328 
lemma big_step_pres_approx_b:


329 
"(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'"


330 
proof (induct arbitrary: t rule: big_step_induct)


331 
case Skip thus ?case by simp


332 
next


333 
case Assign


334 
thus ?case


335 
by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)


336 
next


337 
case (Semi c1 s1 s2 c2 s3)


338 
have "approx (bdefs c1 t) s2" by (rule Semi(2) [OF Semi.prems])


339 
hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi(4))


340 
thus ?case by simp


341 
next


342 
case (IfTrue b s c1 s')


343 
hence "approx (bdefs c1 t) s'" by simp


344 
thus ?case using `bval b s` `approx t s`


345 
by (clarsimp simp: approx_merge bvalsimp_const_B


346 
split: bexp.splits bool.splits)


347 
next


348 
case (IfFalse b s c2 s')


349 
hence "approx (bdefs c2 t) s'" by simp


350 
thus ?case using `\<not>bval b s` `approx t s`


351 
by (clarsimp simp: approx_merge bvalsimp_const_B


352 
split: bexp.splits bool.splits)


353 
next


354 
case WhileFalse


355 
thus ?case


356 
by (clarsimp simp: bvalsimp_const_B approx_def restrict_map_def


357 
split: bexp.splits bool.splits)


358 
next


359 
case (WhileTrue b s1 c s2 s3)


360 
hence "approx (bdefs c t) s2" by simp


361 
with WhileTrue


362 
have "approx (bdefs c t ` ( lnames c)) s3"


363 
by simp


364 
thus ?case


365 
by (simp add: bdefs_restrict)


366 
qed


367 


368 
corollary approx_bdefs_inv [simp]:


369 
"\<Turnstile> {approx t} c {approx (bdefs c t)}"


370 
by (simp add: hoare_valid_def big_step_pres_approx_b)


371 


372 
lemma bfold_equiv:


373 
"approx t \<Turnstile> c \<sim> bfold c t"


374 
proof (induct c arbitrary: t)


375 
case SKIP show ?case by simp


376 
next


377 
case Assign


378 
thus ?case by (simp add: equiv_up_to_def)


379 
next


380 
case Semi


381 
thus ?case by (auto intro!: equiv_up_to_semi)


382 
next


383 
case (If b c1 c2)


384 
hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim>


385 
IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"


386 
by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def)


387 
thus ?case using If


388 
by (fastsimp simp: bvalsimp_const_B split: bexp.splits bool.splits


389 
intro: equiv_up_to_trans)


390 
next


391 
case (While b c)


392 
hence "approx (t ` ( lnames c)) \<Turnstile>


393 
WHILE b DO c \<sim>


394 
WHILE bsimp_const b (t ` ( lnames c))


395 
DO bfold c (t ` ( lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'")


396 
by (auto intro: equiv_up_to_while_weak approx_restrict_inv


397 
simp: bequiv_up_to_def)


398 
hence "approx t \<Turnstile> ?W \<sim> ?W'"


399 
by (auto intro: equiv_up_to_weaken approx_map_le)


400 
thus ?case


401 
by (auto split: bexp.splits bool.splits


402 
intro: equiv_up_to_while_False


403 
simp: bvalsimp_const_B)


404 
qed


405 


406 


407 
theorem constant_bfolding_equiv:


408 
"bfold c empty \<sim> c"


409 
using bfold_equiv [of empty c]


410 
by (simp add: equiv_up_to_True equiv_sym)


411 


412 


413 
end
