1 (* Title: HOL/IMP/Compiler.thy
3 Author: Tobias Nipkow, TUM
6 A simple compiler for a simplistic machine.
9 theory Compiler = Natural:
11 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat
13 consts stepa1 :: "instr list => ((state*nat) * (state*nat))set"
16 "@stepa1" :: "[instr list,state,nat,state,nat] => bool"
17 ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50)
18 "@stepa" :: "[instr list,state,nat,state,nat] => bool"
19 ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50)
21 translations "P |- <s,m> -1-> <t,n>" == "((s,m),t,n) : stepa1 P"
22 "P |- <s,m> -*-> <t,n>" == "((s,m),t,n) : ((stepa1 P)^*)"
28 "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s[x::= a s],Suc n>"
30 "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,Suc n>"
32 "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,m>"
34 "\<lbrakk> n<size P; P!n = JMPB i; i <= n \<rbrakk> \<Longrightarrow> P |- <s,n> -1-> <s,n-i>"
36 consts compile :: "com => instr list"
39 "compile (x:==a) = [ASIN x a]"
40 "compile (c1;c2) = compile c1 @ compile c2"
41 "compile (IF b THEN c1 ELSE c2) =
42 [JMPF b (length(compile c1) + 2)] @ compile c1 @
43 [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
44 "compile (WHILE b DO c) = [JMPF b (length(compile c) + 2)] @ compile c @
45 [JMPB (length(compile c)+1)]"
47 declare nth_append[simp];
49 (* Lemmas for lifting an execution into a prefix and suffix
50 of instructions; only needed for the first proof *)
53 "is1 |- <s1,i1> -1-> <s2,i2> \<Longrightarrow> is1 @ is2 |- <s1,i1> -1-> <s2,i2>"
54 apply(erule stepa1.induct);
56 apply (force intro!:JMPFT)
57 apply (force intro!:JMPFF)
58 apply (simp add: JMPB)
62 "is2 |- <s1,i1> -1-> <s2,i2> \<Longrightarrow>
63 is1 @ is2 |- <s1,size is1+i1> -1-> <s2,size is1+i2>"
64 apply(erule stepa1.induct);
66 apply (fastsimp intro!:JMPFT)
67 apply (fastsimp intro!:JMPFF)
68 apply (simp add: JMPB)
72 "is1 |- <s1,i1> -*-> <s2,i2> \<Longrightarrow> is1 @ is2 |- <s1,i1> -*-> <s2,i2>"
73 apply(erule rtrancl_induct2);
75 apply(blast intro:app_right_1 rtrancl_trans)
79 "is2 |- <s1,i1> -*-> <s2,i2> \<Longrightarrow>
80 is1 @ is2 |- <s1,size is1+i1> -*-> <s2,size is1+i2>"
81 apply(erule rtrancl_induct2);
83 apply(blast intro:app_left_1 rtrancl_trans)
87 "\<lbrakk> is2 |- <s1,i1> -*-> <s2,i2>; j1 = size is1+i1; j2 = size is1+i2 \<rbrakk> \<Longrightarrow>
88 is1 @ is2 |- <s1,j1> -*-> <s2,j2>"
89 by (simp add:app_left)
92 "is |- <s1,i1> -*-> <s2,i2> \<Longrightarrow>
93 instr # is |- <s1,Suc i1> -*-> <s2,Suc i2>"
94 by(erule app_left[of _ _ _ _ _ "[instr]",simplified])
97 (* The first proof; statement very intuitive,
98 but application of induction hypothesis requires the above lifting lemmas
100 theorem "<c,s> -c-> t ==> compile c |- <s,0> -*-> <t,length(compile c)>"
101 apply(erule evalc.induct);
103 apply(force intro!: ASIN);
105 apply(rule rtrancl_trans)
106 apply(erule app_right)
107 apply(erule app_left[of _ 0,simplified])
108 (* IF b THEN c0 ELSE c1; case b is true *)
111 apply (rule rtrancl_into_rtrancl2)
112 apply(force intro!: JMPFT);
113 (* execute compile c0: *)
114 apply(rule app1_left)
115 apply(rule rtrancl_into_rtrancl);
116 apply(erule app_right)
118 apply(force intro!: JMPFF);
119 (* end of case b is true *)
121 apply (rule rtrancl_into_rtrancl2)
122 apply(force intro!: JMPFF)
123 apply(force intro!: app_left2 app1_left)
125 apply(force intro: JMPFF);
128 apply(rule rtrancl_into_rtrancl2);
129 apply(force intro!: JMPFT);
130 apply(rule rtrancl_trans);
131 apply(rule app1_left)
132 apply(erule app_right)
133 apply(rule rtrancl_into_rtrancl2);
134 apply(force intro!: JMPB)
138 (* Second proof; statement is generalized to cater for prefixes and suffixes;
139 needs none of the lifting lemmas, but instantiations of pre/suffix.
141 theorem "<c,s> -c-> t ==>
142 !a z. a@compile c@z |- <s,length a> -*-> <t,length a + length(compile c)>";
143 apply(erule evalc.induct);
145 apply(force intro!: ASIN);
147 apply(erule_tac x = a in allE);
148 apply(erule_tac x = "a@compile c0" in allE);
149 apply(erule_tac x = "compile c1@z" in allE);
150 apply(erule_tac x = z in allE);
151 apply(simp add:add_assoc[THEN sym]);
152 apply(blast intro:rtrancl_trans);
153 (* IF b THEN c0 ELSE c1; case b is true *)
155 (* instantiate assumption sufficiently for later: *)
156 apply(erule_tac x = "a@[?I]" in allE);
159 apply(rule rtrancl_into_rtrancl2);
160 apply(force intro!: JMPFT);
161 (* execute compile c0: *)
162 apply(rule rtrancl_trans);
166 apply(rule r_into_rtrancl);
167 apply(force intro!: JMPFF);
168 (* end of case b is true *)
170 apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE);
171 apply(simp add:add_assoc);
172 apply(rule rtrancl_into_rtrancl2);
173 apply(force intro!: JMPFF);
175 apply(force intro: JMPFF);
177 apply(erule_tac x = "a@[?I]" in allE);
178 apply(erule_tac x = a in allE);
180 apply(rule rtrancl_into_rtrancl2);
181 apply(force intro!: JMPFT);
182 apply(rule rtrancl_trans);
185 apply(rule rtrancl_into_rtrancl2);
186 apply(force intro!: JMPB);
190 (* Missing: the other direction! *)