|
1 theory Compiler = Natural: |
|
2 |
|
3 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat |
|
4 |
|
5 consts stepa1 :: "instr list => ((state*nat) * (state*nat))set" |
|
6 |
|
7 syntax |
|
8 "@stepa1" :: "[instr list,state,nat,state,nat] => bool" |
|
9 ("_ |- <_,_>/ -1-> <_,_>" [50,0,0,0,0] 50) |
|
10 "@stepa" :: "[instr list,state,nat,state,nat] => bool" |
|
11 ("_ |-/ <_,_>/ -*-> <_,_>" [50,0,0,0,0] 50) |
|
12 |
|
13 translations "P |- <s,m> -1-> <t,n>" == "((s,m),t,n) : stepa1 P" |
|
14 "P |- <s,m> -*-> <t,n>" == "((s,m),t,n) : ((stepa1 P)^*)" |
|
15 |
|
16 |
|
17 inductive "stepa1 P" |
|
18 intros |
|
19 ASIN: "P!n = ASIN x a ==> P |- <s,n> -1-> <s[x::= a s],Suc n>" |
|
20 JMPFT: "[| P!n = JMPF b i; b s |] ==> P |- <s,n> -1-> <s,Suc n>" |
|
21 JMPFF: "[| P!n = JMPF b i; ~b s; m=n+i |] ==> P |- <s,n> -1-> <s,m>" |
|
22 JMPB: "[| P!n = JMB i |] ==> P |- <s,n> -1-> <s,n-i>" |
|
23 |
|
24 consts compile :: "com => instr list" |
|
25 primrec |
|
26 "compile SKIP = []" |
|
27 "compile (x:==a) = [ASIN x a]" |
|
28 "compile (c1;c2) = compile c1 @ compile c2" |
|
29 "compile (IF b THEN c1 ELSE c2) = |
|
30 [JMPF b (length(compile c1)+2)] @ compile c1 @ |
|
31 [JMPF (%x. False) (length(compile c2)+1)] @ compile c2" |
|
32 "compile (WHILE b DO c) = [JMPF b (length(compile c)+2)] @ compile c @ |
|
33 [JMPB (length(compile c)+1)]" |
|
34 |
|
35 declare nth_append[simp]; |
|
36 |
|
37 lemma nth_tl[simp]: "tl(xs @ y # ys) ! (length xs + z) = ys!z"; |
|
38 apply(induct_tac xs); |
|
39 by(auto); |
|
40 |
|
41 theorem "<c,s> -c-> t ==> |
|
42 !a z. a@compile c@z |- <s,length a> -*-> <t,length a + length(compile c)>"; |
|
43 apply(erule evalc.induct); |
|
44 apply simp; |
|
45 apply(force intro!: ASIN); |
|
46 apply(intro strip); |
|
47 apply(erule_tac x = a in allE); |
|
48 apply(erule_tac x = "a@compile c0" in allE); |
|
49 apply(erule_tac x = "compile c1@z" in allE); |
|
50 apply(erule_tac x = z in allE); |
|
51 apply(simp add:add_assoc[THEN sym]); |
|
52 apply(blast intro:rtrancl_trans); |
|
53 (* IF b THEN c0 ELSE c1; case b is true *) |
|
54 apply(intro strip); |
|
55 (* instantiate assumption sufficiently for later: *) |
|
56 apply(erule_tac x = "a@[?I]" in allE); |
|
57 apply(simp); |
|
58 (* execute JMPF: *) |
|
59 apply(rule rtrancl_into_rtrancl2); |
|
60 apply(rule JMPFT); |
|
61 apply(simp); |
|
62 apply(blast); |
|
63 apply assumption; |
|
64 (* execute compile c0: *) |
|
65 apply(rule rtrancl_trans); |
|
66 apply(erule allE); |
|
67 apply assumption; |
|
68 (* execute JMPF: *) |
|
69 apply(rule r_into_rtrancl); |
|
70 apply(rule JMPFF); |
|
71 apply(simp); |
|
72 apply(blast); |
|
73 apply(blast); |
|
74 apply(simp); |
|
75 (* end of case b is true *) |
|
76 apply(intro strip); |
|
77 apply(erule_tac x = "a@[?I]@compile c0@[?J]" in allE); |
|
78 apply(simp add:add_assoc); |
|
79 apply(rule rtrancl_into_rtrancl2); |
|
80 apply(rule JMPFF); |
|
81 apply(simp); |
|
82 apply(blast); |
|
83 apply assumption; |
|
84 apply(simp); |
|
85 apply(blast); |
|
86 apply(force intro: JMPFF); |
|
87 apply(intro strip); |
|
88 apply(erule_tac x = "a@[?I]" in allE); |
|
89 apply(erule_tac x = a in allE); |
|
90 apply(simp); |
|
91 apply(rule rtrancl_into_rtrancl2); |
|
92 apply(rule JMPFT); |
|
93 apply(simp); |
|
94 apply(blast); |
|
95 apply assumption; |
|
96 apply(rule rtrancl_trans); |
|
97 apply(erule allE); |
|
98 apply assumption; |
|
99 apply(rule rtrancl_into_rtrancl2); |
|
100 apply(rule JMPB); |
|
101 apply(simp); |
|
102 apply(simp); |
|
103 done |
|
104 |
|
105 (* Missing: the other direction! *) |
|
106 |
|
107 end |