diff -r 504d72a39638 -r 11fce8564415 src/HOL/IMP/Compiler.thy --- a/src/HOL/IMP/Compiler.thy Wed Jun 01 15:53:47 2011 +0200 +++ b/src/HOL/IMP/Compiler.thy Wed Jun 01 21:35:34 2011 +0200 @@ -1,298 +1,237 @@ -(* Title: HOL/IMP/Compiler.thy - Author: Tobias Nipkow, TUM - Copyright 1996 TUM -*) +(* Author: Tobias Nipkow *) + +header "A Compiler for IMP" -theory Compiler imports Machines begin +theory Compiler imports Big_Step +begin -subsection "The compiler" +subsection "Instructions and Stack Machine" -primrec compile :: "com \ instr list" -where - "compile \ = []" -| "compile (x:==a) = [SET x a]" -| "compile (c1;c2) = compile c1 @ compile c2" -| "compile (\ b \ c1 \ c2) = - [JMPF b (length(compile c1) + 1)] @ compile c1 @ - [JMPF (\x. False) (length(compile c2))] @ compile c2" -| "compile (\ b \ c) = [JMPF b (length(compile c) + 1)] @ compile c @ - [JMPB (length(compile c)+1)]" +datatype instr = + LOADI int | LOAD string | ADD | + STORE string | + JMPF nat | + JMPB nat | + JMPFLESS nat | + JMPFGE nat -subsection "Compiler correctness" +type_synonym stack = "int list" +type_synonym config = "nat\state\stack" + +abbreviation "hd2 xs == hd(tl xs)" +abbreviation "tl2 xs == tl(tl xs)" -theorem assumes A: "\c,s\ \\<^sub>c t" -shows "\p q. \compile c @ p,q,s\ -*\ \p,rev(compile c)@q,t\" - (is "\p q. ?P c s t p q") -proof - - from A show "\p q. ?thesis p q" - proof induct - case Skip thus ?case by simp - next - case Assign thus ?case by force - next - case Semi thus ?case by simp (blast intro:rtrancl_trans) - next - fix b c0 c1 s0 s1 p q - assume IH: "\p q. ?P c0 s0 s1 p q" - assume "b s0" - thus "?P (\ b \ c0 \ c1) s0 s1 p q" - by(simp add: IH[THEN rtrancl_trans]) - next - case IfFalse thus ?case by(simp) - next - case WhileFalse thus ?case by simp - next - fix b c and s0::state and s1 s2 p q - assume b: "b s0" and - IHc: "\p q. ?P c s0 s1 p q" and - IHw: "\p q. ?P (\ b \ c) s1 s2 p q" - show "?P (\ b \ c) s0 s2 p q" - using b IHc[THEN rtrancl_trans] IHw by(simp) - qed +inductive exec1 :: "instr list \ config \ config \ bool" + ("(_/ \ (_ \/ _))" [50,0,0] 50) + for P :: "instr list" +where +"\ i < size P; P!i = LOADI n \ \ + P \ (i,s,stk) \ (i+1,s, n#stk)" | +"\ i < size P; P!i = LOAD x \ \ + P \ (i,s,stk) \ (i+1,s, s x # stk)" | +"\ i < size P; P!i = ADD \ \ + P \ (i,s,stk) \ (i+1,s, (hd2 stk + hd stk) # tl2 stk)" | +"\ i < size P; P!i = STORE n \ \ + P \ (i,s,stk) \ (i+1,s(n := hd stk),tl stk)" | +"\ i < size P; P!i = JMPF n \ \ + P \ (i,s,stk) \ (i+1+n,s,stk)" | +"\ i < size P; P!i = JMPB n; n \ i+1 \ \ + P \ (i,s,stk) \ (i+1-n,s,stk)" | +"\ i < size P; P!i = JMPFLESS n \ \ + P \ (i,s,stk) \ (if hd2 stk < hd stk then i+1+n else i+1,s,tl2 stk)" | +"\ i < size P; P!i = JMPFGE n \ \ + P \ (i,s,stk) \ (if hd2 stk >= hd stk then i+1+n else i+1,s,tl2 stk)" + +code_pred exec1 . + +declare exec1.intros[intro] + +inductive exec :: "instr list \ config \ config \ bool" ("_/ \ (_ \*/ _)" 50) +where +refl: "P \ c \* c" | +step: "P \ c \ c' \ P \ c' \* c'' \ P \ c \* c''" + +declare exec.intros[intro] + +lemmas exec_induct = exec.induct[split_format(complete)] + +code_pred exec . + +values + "{(i,map t [''x'',''y''],stk) | i t stk. + [LOAD ''y'', STORE ''x''] \ + (0,lookup[(''x'',3),(''y'',4)],[]) \* (i,t,stk)}" + + +subsection{* Verification infrastructure *} + +lemma exec_trans: "P \ c \* c' \ P \ c' \* c'' \ P \ c \* c''" +apply(induct rule: exec.induct) + apply blast +by (metis exec.step) + +lemma exec1_subst: "P \ c \ c' \ c' = c'' \ P \ c \ c''" +by auto + +lemmas exec1_simps = exec1.intros[THEN exec1_subst] + +text{* Below we need to argue about the execution of code that is embedded in +larger programs. For this purpose we show that execution is preserved by +appending code to the left or right of a program. *} + +lemma exec1_appendR: assumes "P \ c \ c'" shows "P@P' \ c \ c'" +proof- + from assms show ?thesis + by cases (simp_all add: exec1_simps nth_append) + -- "All cases proved with the final simp-all" qed -text {* The other direction! *} - -inductive_cases [elim!]: "(([],p,s),(is',p',s')) : stepa1" - -lemma [simp]: "(\[],q,s\ -n\ \p',q',t\) = (n=0 \ p' = [] \ q' = q \ t = s)" -apply(rule iffI) - apply(erule rel_pow_E2, simp, fast) -apply simp -done +lemma exec_appendR: "P \ c \* c' \ P@P' \ c \* c'" +apply(induct rule: exec.induct) + apply blast +by (metis exec1_appendR exec.step) -lemma [simp]: "(\[],q,s\ -*\ \p',q',t\) = (p' = [] \ q' = q \ t = s)" -by(simp add: rtrancl_is_UN_rel_pow) - -definition - forws :: "instr \ nat set" where - "forws instr = (case instr of - SET x a \ {0} | - JMPF b n \ {0,n} | - JMPB n \ {})" +lemma exec1_appendL: +assumes "P \ (i,s,stk) \ (i',s',stk')" +shows "P' @ P \ (size(P')+i,s,stk) \ (size(P')+i',s',stk')" +proof- + from assms show ?thesis + by cases (simp_all add: exec1_simps) +qed -definition - backws :: "instr \ nat set" where - "backws instr = (case instr of - SET x a \ {} | - JMPF b n \ {} | - JMPB n \ {n})" - -primrec closed :: "nat \ nat \ instr list \ bool" -where - "closed m n [] = True" -| "closed m n (instr#is) = ((\j \ forws instr. j \ size is+n) \ - (\j \ backws instr. j \ m) \ closed (Suc m) n is)" +lemma exec_appendL: + "P \ (i,s,stk) \* (i',s',stk') \ + P' @ P \ (size(P')+i,s,stk) \* (size(P')+i',s',stk')" +apply(induct rule: exec_induct) + apply blast +by (blast intro: exec1_appendL exec.step) -lemma [simp]: - "\m n. closed m n (C1@C2) = - (closed m (n+size C2) C1 \ closed (m+size C1) n C2)" -by(induct C1) (simp, simp add:add_ac) - -theorem [simp]: "\m n. closed m n (compile c)" -by(induct c) (simp_all add:backws_def forws_def) +text{* Now we specialise the above lemmas to enable automatic proofs of +@{prop "P \ c \* c'"} where @{text P} is a mixture of concrete instructions and +pieces of code that we already know how they execute (by induction), combined +by @{text "@"} and @{text "#"}. Backward jumps are not supported. +The details should be skipped on a first reading. -lemma drop_lem: "n \ size(p1@p2) - \ (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) = - (n \ size p1 & p1' = drop n p1)" -apply(rule iffI) - defer apply simp -apply(subgoal_tac "n \ size p1") - apply simp -apply(rule ccontr) -apply(drule_tac f = length in arg_cong) +If the pc points beyond the first instruction or part of the program, drop it: *} + +lemma exec_Cons_Suc[intro]: + "P \ (i,s,stk) \* (j,t,stk') \ + instr#P \ (Suc i,s,stk) \* (Suc j,t,stk')" +apply(drule exec_appendL[where P'="[instr]"]) apply simp done -lemma reduce_exec1: - "\i # p1 @ p2,q1 @ q2,s\ -1\ \p1' @ p2,q1' @ q2,s'\ \ - \i # p1,q1,s\ -1\ \p1',q1',s'\" -by(clarsimp simp add: drop_lem split:instr.split_asm split_if_asm) - - -lemma closed_exec1: - "\ closed 0 0 (rev q1 @ instr # p1); - \instr # p1 @ p2, q1 @ q2,r\ -1\ \p',q',r'\ \ \ - \p1' q1'. p' = p1'@p2 \ q' = q1'@q2 \ rev q1' @ p1' = rev q1 @ instr # p1" -apply(clarsimp simp add:forws_def backws_def - split:instr.split_asm split_if_asm) +lemma exec_appendL_if[intro]: + "size P' <= i + \ P \ (i - size P',s,stk) \* (i',s',stk') + \ P' @ P \ (i,s,stk) \* (size P' + i',s',stk')" +apply(drule exec_appendL[where P'=P']) +apply simp done -theorem closed_execn_decomp: "\C1 C2 r. - \ closed 0 0 (rev C1 @ C2); - \C2 @ p1 @ p2, C1 @ q,r\ -n\ \p2,rev p1 @ rev C2 @ C1 @ q,t\ \ - \ \s n1 n2. \C2,C1,r\ -n1\ \[],rev C2 @ C1,s\ \ - \p1@p2,rev C2 @ C1 @ q,s\ -n2\ \p2, rev p1 @ rev C2 @ C1 @ q,t\ \ - n = n1+n2" -(is "\C1 C2 r. \?CL C1 C2; ?H C1 C2 r n\ \ ?P C1 C2 r n") -proof(induct n) - fix C1 C2 r - assume "?H C1 C2 r 0" - thus "?P C1 C2 r 0" by simp -next - fix C1 C2 r n - assume IH: "\C1 C2 r. ?CL C1 C2 \ ?H C1 C2 r n \ ?P C1 C2 r n" - assume CL: "?CL C1 C2" and H: "?H C1 C2 r (Suc n)" - show "?P C1 C2 r (Suc n)" - proof (cases C2) - assume "C2 = []" with H show ?thesis by simp - next - fix instr tlC2 - assume C2: "C2 = instr # tlC2" - from H C2 obtain p' q' r' - where 1: "\instr # tlC2 @ p1 @ p2, C1 @ q,r\ -1\ \p',q',r'\" - and n: "\p',q',r'\ -n\ \p2,rev p1 @ rev C2 @ C1 @ q,t\" - by(fastsimp simp add:rel_pow_commute) - from CL closed_exec1[OF _ 1] C2 - obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \ q' = C1' @ q" - and same: "rev C1' @ C2' = rev C1 @ C2" - by fastsimp - have rev_same: "rev C2' @ C1' = rev C2 @ C1" - proof - - have "rev C2' @ C1' = rev(rev C1' @ C2')" by simp - also have "\ = rev(rev C1 @ C2)" by(simp only:same) - also have "\ = rev C2 @ C1" by simp - finally show ?thesis . - qed - hence rev_same': "\p. rev C2' @ C1' @ p = rev C2 @ C1 @ p" by simp - from n have n': "\C2' @ p1 @ p2,C1' @ q,r'\ -n\ - \p2,rev p1 @ rev C2' @ C1' @ q,t\" - by(simp add:pq' rev_same') - from IH[OF _ n'] CL - obtain s n1 n2 where n1: "\C2',C1',r'\ -n1\ \[],rev C2 @ C1,s\" and - "\p1 @ p2,rev C2 @ C1 @ q,s\ -n2\ \p2,rev p1 @ rev C2 @ C1 @ q,t\ \ - n = n1 + n2" - by(fastsimp simp add: same rev_same rev_same') - moreover - from 1 n1 pq' C2 have "\C2,C1,r\ -Suc n1\ \[],rev C2 @ C1,s\" - by (simp del:relpow.simps exec_simp) (fast dest:reduce_exec1) - ultimately show ?thesis by (fastsimp simp del:relpow.simps) - qed -qed +text{* Split the execution of a compound program up into the excution of its +parts: *} -lemma execn_decomp: -"\compile c @ p1 @ p2,q,r\ -n\ \p2,rev p1 @ rev(compile c) @ q,t\ - \ \s n1 n2. \compile c,[],r\ -n1\ \[],rev(compile c),s\ \ - \p1@p2,rev(compile c) @ q,s\ -n2\ \p2, rev p1 @ rev(compile c) @ q,t\ \ - n = n1+n2" -using closed_execn_decomp[of "[]",simplified] by simp +lemma exec_append_trans[intro]: +"P \ (0,s,stk) \* (i',s',stk') \ + size P \ i' \ + P' \ (i' - size P,s',stk') \* (i'',s'',stk'') \ + j'' = size P + i'' + \ + P @ P' \ (0,s,stk) \* (j'',s'',stk'')" +by(metis exec_trans[OF exec_appendR exec_appendL_if]) -lemma exec_star_decomp: -"\compile c @ p1 @ p2,q,r\ -*\ \p2,rev p1 @ rev(compile c) @ q,t\ - \ \s. \compile c,[],r\ -*\ \[],rev(compile c),s\ \ - \p1@p2,rev(compile c) @ q,s\ -*\ \p2, rev p1 @ rev(compile c) @ q,t\" -by(simp add:rtrancl_is_UN_rel_pow)(fast dest: execn_decomp) + +declare Let_def[simp] eval_nat_numeral[simp] -(* Alternative: -lemma exec_comp_n: -"\p1 p2 q r t n. - \compile c @ p1 @ p2,q,r\ -n\ \p2,rev p1 @ rev(compile c) @ q,t\ - \ \s n1 n2. \compile c,[],r\ -n1\ \[],rev(compile c),s\ \ - \p1@p2,rev(compile c) @ q,s\ -n2\ \p2, rev p1 @ rev(compile c) @ q,t\ \ - n = n1+n2" - (is "\p1 p2 q r t n. ?H c p1 p2 q r t n \ ?P c p1 p2 q r t n") -proof (induct c) -*) +subsection "Compilation" -text{*Warning: -@{prop"\compile c @ p,q,s\ -*\ \p,rev(compile c)@q,t\ \ \c,s\ \\<^sub>c t"} -is not true! *} +fun acomp :: "aexp \ instr list" where +"acomp (N n) = [LOADI n]" | +"acomp (V x) = [LOAD x]" | +"acomp (Plus a1 a2) = acomp a1 @ acomp a2 @ [ADD]" + +lemma acomp_correct[intro]: + "acomp a \ (0,s,stk) \* (size(acomp a),s,aval a s#stk)" +apply(induct a arbitrary: stk) +apply(fastsimp)+ +done -theorem "\s t. - \compile c,[],s\ -*\ \[],rev(compile c),t\ \ \c,s\ \\<^sub>c t" -proof (induct c) - fix s t - assume "\compile SKIP,[],s\ -*\ \[],rev(compile SKIP),t\" - thus "\SKIP,s\ \\<^sub>c t" by simp -next - fix s t v f - assume "\compile(v :== f),[],s\ -*\ \[],rev(compile(v :== f)),t\" - thus "\v :== f,s\ \\<^sub>c t" by simp -next - fix s1 s3 c1 c2 - let ?C1 = "compile c1" let ?C2 = "compile c2" - assume IH1: "\s t. \?C1,[],s\ -*\ \[],rev ?C1,t\ \ \c1,s\ \\<^sub>c t" - and IH2: "\s t. \?C2,[],s\ -*\ \[],rev ?C2,t\ \ \c2,s\ \\<^sub>c t" - assume "\compile(c1;c2),[],s1\ -*\ \[],rev(compile(c1;c2)),s3\" - then obtain s2 where exec1: "\?C1,[],s1\