theory Solution07
imports "HOL-IMP.Small_Step" "HOL-IMP.Compiler"
begin
section "Deskip"
(* similar strategy as for asimp *)
definition de_seq :: "com \ com \ com" where
"de_seq c1 c2 = (if c1=SKIP then c2 else if c2=SKIP then c1 else c1;;c2)"
lemma de_seq_sim: "de_seq c1 c2 \ c1;;c2"
unfolding de_seq_def by auto
definition de_if :: "bexp \ com \ com \ com" where
"de_if b c1 c2 = (if c1=SKIP & c2=SKIP then SKIP else IF b THEN c1 ELSE c2)"
lemma de_if_sim: "de_if b c1 c2 \ IF b THEN c1 ELSE c2"
unfolding de_if_def by auto
fun deskip :: "com \ com" where
"deskip (c1;;c2) = de_seq (deskip c1) (deskip c2)" |
"deskip (IF b THEN c1 ELSE c2) = de_if b (deskip c1) (deskip c2)" |
"deskip (WHILE b DO c) = WHILE b DO deskip c" |
"deskip c = c"
lemma "deskip c \ c"
proof (induction c)
case (Seq c1 c2)
moreover have "deskip (c1;; c2) \ deskip c1 ;; deskip c2"
by simp (rule de_seq_sim)
ultimately show ?case
by auto
next
case (If b c1 c2)
moreover have "deskip (IF b THEN c1 ELSE c2) \ IF b THEN deskip c1 ELSE deskip c2"
by simp (rule de_if_sim)
ultimately show ?case
by auto
next
case (While x1 c)
then have "WHILE x1 DO deskip c \ WHILE x1 DO c"
by (meson sim_while_cong)
then show ?case
by simp
qed auto
section "Compiler optimization"
fun ccomp2 :: "com \ instr list" where
"ccomp2 SKIP = []" |
"ccomp2 (x ::= a) = acomp a @ [STORE x]" |
"ccomp2 (c\<^sub>1;;c\<^sub>2) = ccomp2 c\<^sub>1 @ ccomp2 c\<^sub>2" |
"ccomp2 (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
(if c\<^sub>2 = SKIP
then (let cc1 = ccomp2 c\<^sub>1; cb = bcomp b False (size cc1) in cb @ cc1)
else (let cc\<^sub>1 = ccomp2 c\<^sub>1; cc\<^sub>2 = ccomp2 c\<^sub>2; cb = bcomp b False (size cc\<^sub>1 + 1)
in cb @ cc\<^sub>1 @ JMP (size cc\<^sub>2) # cc\<^sub>2))" |
"ccomp2 (WHILE b DO c) =
(let cc = ccomp2 c; cb = bcomp b False (size cc + 1)
in cb @ cc @ [JMP (-(size cb + size cc + 1))])"
lemma ccomp_bigstep:
"(c,s) \ t \ ccomp2 c \ (0,s,stk) \* (size(ccomp2 c),t,stk)"
proof(induction arbitrary: stk rule: big_step_induct)
case (Assign x a s)
show ?case by (fastforce simp:fun_upd_def cong: if_cong)
next
case (Seq c1 s1 s2 c2 s3)
let ?cc1 = "ccomp2 c1" let ?cc2 = "ccomp2 c2"
have "?cc1 @ ?cc2 \ (0,s1,stk) \* (size ?cc1,s2,stk)"
using Seq.IH(1) by fastforce
moreover
have "?cc1 @ ?cc2 \ (size ?cc1,s2,stk) \* (size(?cc1 @ ?cc2),s3,stk)"
using Seq.IH(2) by fastforce
ultimately show ?case by simp (blast intro: star_trans)
next
case (WhileTrue b s1 c s2 s3)
let ?cc = "ccomp2 c"
let ?cb = "bcomp b False (size ?cc + 1)"
let ?cw = "ccomp2 (WHILE b DO c)"
have "?cw \ (0,s1,stk) \* (size ?cb,s1,stk)"
using \bval b s1\ by fastforce
moreover
have "?cw \ (size ?cb,s1,stk) \* (size ?cb + size ?cc,s2,stk)"
using WhileTrue.IH(1) by fastforce
moreover
have "?cw \ (size ?cb + size ?cc,s2,stk) \* (0,s2,stk)"
by fastforce
moreover
have "?cw \ (0,s2,stk) \* (size ?cw,s3,stk)" by(rule WhileTrue.IH(2))
ultimately show ?case by(blast intro: star_trans)
qed fastforce+
end