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)^*)"
27 ASIN: "P!n = ASIN x a ==> P |- <s,n> -1-> <s[x::= a s],Suc n>"
28 JMPFT: "[| P!n = JMPF b i; b s |] ==> P |- <s,n> -1-> <s,Suc n>"
29 JMPFF: "[| P!n = JMPF b i; ~b s; m=n+i |] ==> P |- <s,n> -1-> <s,m>"
30 JMPB: "[| P!n = JMB i |] ==> P |- <s,n> -1-> <s,n-i>"
32 consts compile :: "com => instr list"
35 "compile (x:==a) = [ASIN x a]"
36 "compile (c1;c2) = compile c1 @ compile c2"
37 "compile (IF b THEN c1 ELSE c2) =
38 [JMPF b (length(compile c1)+2)] @ compile c1 @
39 [JMPF (%x. False) (length(compile c2)+1)] @ compile c2"
40 "compile (WHILE b DO c) = [JMPF b (length(compile c)+2)] @ compile c @
41 [JMPB (length(compile c)+1)]"
43 declare nth_append[simp];
45 lemma nth_tl[simp]: "tl(xs @ y # ys) ! (length xs + z) = ys!z";
49 theorem "<c,s> -c-> t ==>
50 !a z. a@compile c@z |- <s,length a> -*-> <t,length a + length(compile c)>";
51 apply(erule evalc.induct);
53 apply(force intro!: ASIN);
55 apply(erule_tac x = a in allE);
56 apply(erule_tac x = "a@compile c0" in allE);
57 apply(erule_tac x = "compile c1@z" in allE);
58 apply(erule_tac x = z in allE);
59 apply(simp add:add_assoc[THEN sym]);
60 apply(blast intro:rtrancl_trans);
61 (* IF b THEN c0 ELSE c1; case b is true *)
63 (* instantiate assumption sufficiently for later: *)
64 apply(erule_tac x = "a@[?I]" in allE);
67 apply(rule rtrancl_into_rtrancl2);
72 (* execute compile c0: *)
73 apply(rule rtrancl_trans);
77 apply(rule r_into_rtrancl);
83 (* end of case b is true *)
85 apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE);
86 apply(simp add:add_assoc);
87 apply(rule rtrancl_into_rtrancl2);
94 apply(force intro: JMPFF);
96 apply(erule_tac x = "a@[?I]" in allE);
97 apply(erule_tac x = a in allE);
99 apply(rule rtrancl_into_rtrancl2);
104 apply(rule rtrancl_trans);
107 apply(rule rtrancl_into_rtrancl2);
113 (* Missing: the other direction! *)