18 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat |
18 datatype instr = ASIN loc aexp | JMPF bexp nat | JMPB nat |
19 |
19 |
20 text {* We describe execution of programs in the machine by |
20 text {* We describe execution of programs in the machine by |
21 an operational (small step) semantics: |
21 an operational (small step) semantics: |
22 *} |
22 *} |
23 consts stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set" |
23 |
24 |
24 inductive_set |
25 syntax |
25 stepa1 :: "instr list \<Rightarrow> ((state\<times>nat) \<times> (state\<times>nat))set" |
26 "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
26 and stepa1' :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
27 ("_ |- (3<_,_>/ -1-> <_,_>)" [50,0,0,0,0] 50) |
27 ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50) |
28 "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
28 for P :: "instr list" |
29 ("_ |-/ (3<_,_>/ -*-> <_,_>)" [50,0,0,0,0] 50) |
29 where |
30 |
30 "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : stepa1 P" |
31 "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool" |
31 | ASIN[simp]: |
32 ("_ |-/ (3<_,_>/ -(_)-> <_,_>)" [50,0,0,0,0,0] 50) |
|
33 |
|
34 syntax (xsymbols) |
|
35 "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
|
36 ("_ \<turnstile> (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50) |
|
37 "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
|
38 ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50) |
|
39 "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool" |
|
40 ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50) |
|
41 |
|
42 syntax (HTML output) |
|
43 "_stepa1" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
|
44 ("_ |- (3\<langle>_,_\<rangle>/ -1\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50) |
|
45 "_stepa" :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
|
46 ("_ |-/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50) |
|
47 "_stepan" :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool" |
|
48 ("_ |-/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50) |
|
49 |
|
50 translations |
|
51 "P \<turnstile> \<langle>s,m\<rangle> -1\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : stepa1 P" |
|
52 "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^*)" |
|
53 "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle>" == "((s,m),t,n) : ((stepa1 P)^i)" |
|
54 |
|
55 inductive "stepa1 P" |
|
56 intros |
|
57 ASIN[simp]: |
|
58 "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s[x\<mapsto> a s],Suc n\<rangle>" |
32 "\<lbrakk> n<size P; P!n = ASIN x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s[x\<mapsto> a s],Suc n\<rangle>" |
59 JMPFT[simp,intro]: |
33 | JMPFT[simp,intro]: |
60 "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,Suc n\<rangle>" |
34 "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,Suc n\<rangle>" |
61 JMPFF[simp,intro]: |
35 | JMPFF[simp,intro]: |
62 "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,m\<rangle>" |
36 "\<lbrakk> n<size P; P!n = JMPF b i; ~b s; m=n+i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,m\<rangle>" |
63 JMPB[simp]: |
37 | JMPB[simp]: |
64 "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,j\<rangle>" |
38 "\<lbrakk> n<size P; P!n = JMPB i; i <= n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>s,n\<rangle> -1\<rightarrow> \<langle>s,j\<rangle>" |
|
39 |
|
40 abbreviation |
|
41 stepa :: "[instr list,state,nat,state,nat] \<Rightarrow> bool" |
|
42 ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -*\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0] 50) where |
|
43 "P \<turnstile> \<langle>s,m\<rangle> -*\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^*)" |
|
44 |
|
45 abbreviation |
|
46 stepan :: "[instr list,state,nat,nat,state,nat] \<Rightarrow> bool" |
|
47 ("_ \<turnstile>/ (3\<langle>_,_\<rangle>/ -(_)\<rightarrow> \<langle>_,_\<rangle>)" [50,0,0,0,0,0] 50) where |
|
48 "P \<turnstile> \<langle>s,m\<rangle> -(i)\<rightarrow> \<langle>t,n\<rangle> == ((s,m),t,n) : ((stepa1 P)^i)" |
65 |
49 |
66 subsection "The compiler" |
50 subsection "The compiler" |
67 |
51 |
68 consts compile :: "com \<Rightarrow> instr list" |
52 consts compile :: "com \<Rightarrow> instr list" |
69 primrec |
53 primrec |