34 |
34 |
35 types instrs = "instr list" |
35 types instrs = "instr list" |
36 |
36 |
37 subsection "M0 with PC" |
37 subsection "M0 with PC" |
38 |
38 |
39 consts exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set" |
39 inductive_set |
40 syntax |
40 exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set" |
41 "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool" |
41 and exec01' :: "[instrs, nat,state, nat,state] \<Rightarrow> bool" |
42 ("(_/ |- (1<_,/_>)/ -1-> (1<_,/_>))" [50,0,0,0,0] 50) |
42 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) |
43 "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool" |
43 for P :: "instr list" |
44 ("(_/ |- (1<_,/_>)/ -*-> (1<_,/_>))" [50,0,0,0,0] 50) |
44 where |
45 "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool" |
45 "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)" |
46 ("(_/ |- (1<_,/_>)/ -_-> (1<_,/_>))" [50,0,0,0,0] 50) |
46 | SET: "\<lbrakk> n<size P; P!n = SET x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s[x\<mapsto> a s]\<rangle>" |
47 |
47 | JMPFT: "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s\<rangle>" |
48 syntax (xsymbols) |
48 | JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk> |
49 "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool" |
|
50 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) |
|
51 "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool" |
|
52 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) |
|
53 "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool" |
|
54 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) |
|
55 |
|
56 syntax (HTML output) |
|
57 "_exec01" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool" |
|
58 ("(_/ |- (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) |
|
59 "_exec0s" :: "[instrs, nat,state, nat,state] \<Rightarrow> bool" |
|
60 ("(_/ |- (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) |
|
61 "_exec0n" :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool" |
|
62 ("(_/ |- (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) |
|
63 |
|
64 translations |
|
65 "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)" |
|
66 "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^*" |
|
67 "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle>" == "((i,s),j,t) : (exec01 p)^n" |
|
68 |
|
69 inductive "exec01 P" |
|
70 intros |
|
71 SET: "\<lbrakk> n<size P; P!n = SET x a \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s[x\<mapsto> a s]\<rangle>" |
|
72 JMPFT: "\<lbrakk> n<size P; P!n = JMPF b i; b s \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>Suc n,s\<rangle>" |
|
73 JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk> |
|
74 \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>" |
49 \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>" |
75 JMPB: "\<lbrakk> n<size P; P!n = JMPB i; i \<le> n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>j,s\<rangle>" |
50 | JMPB: "\<lbrakk> n<size P; P!n = JMPB i; i \<le> n; j = n-i \<rbrakk> \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>j,s\<rangle>" |
|
51 |
|
52 abbreviation |
|
53 exec0s :: "[instrs, nat,state, nat,state] \<Rightarrow> bool" |
|
54 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) where |
|
55 "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^*" |
|
56 |
|
57 abbreviation |
|
58 exec0n :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool" |
|
59 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) where |
|
60 "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^n" |
76 |
61 |
77 subsection "M0 with lists" |
62 subsection "M0 with lists" |
78 |
63 |
79 text {* We describe execution of programs in the machine by |
64 text {* We describe execution of programs in the machine by |
80 an operational (small step) semantics: |
65 an operational (small step) semantics: |
81 *} |
66 *} |
82 |
67 |
83 types config = "instrs \<times> instrs \<times> state" |
68 types config = "instrs \<times> instrs \<times> state" |
84 |
69 |
85 consts stepa1 :: "(config \<times> config)set" |
70 |
86 |
71 inductive_set |
87 syntax |
72 stepa1 :: "(config \<times> config)set" |
88 "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool" |
73 and stepa1' :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool" |
89 ("((1<_,/_,/_>)/ -1-> (1<_,/_,/_>))" 50) |
74 ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) |
90 "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool" |
75 where |
91 ("((1<_,/_,/_>)/ -*-> (1<_,/_,/_>))" 50) |
76 "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : stepa1" |
92 "_stepan" :: "[state,instrs,instrs, nat, instrs,instrs,state] \<Rightarrow> bool" |
77 | "\<langle>SET x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,SET x a#q,s[x\<mapsto> a s]\<rangle>" |
93 ("((1<_,/_,/_>)/ -_-> (1<_,/_,/_>))" 50) |
78 | "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>" |
94 |
79 | "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk> |
95 syntax (xsymbols) |
|
96 "_stepa1" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool" |
|
97 ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) |
|
98 "_stepa" :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool" |
|
99 ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) |
|
100 "_stepan" :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool" |
|
101 ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) |
|
102 |
|
103 translations |
|
104 "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : stepa1" |
|
105 "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^*)" |
|
106 "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle>" == "((p,q,s),p',q',t) : (stepa1^i)" |
|
107 |
|
108 |
|
109 inductive "stepa1" |
|
110 intros |
|
111 "\<langle>SET x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,SET x a#q,s[x\<mapsto> a s]\<rangle>" |
|
112 "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>" |
|
113 "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk> |
|
114 \<Longrightarrow> \<langle>JMPF b i # p, q, s\<rangle> -1\<rightarrow> \<langle>drop i p, rev(take i p) @ JMPF b i # q, s\<rangle>" |
80 \<Longrightarrow> \<langle>JMPF b i # p, q, s\<rangle> -1\<rightarrow> \<langle>drop i p, rev(take i p) @ JMPF b i # q, s\<rangle>" |
115 "i \<le> size q |
81 | "i \<le> size q |
116 \<Longrightarrow> \<langle>JMPB i # p, q, s\<rangle> -1\<rightarrow> \<langle>rev(take i q) @ JMPB i # p, drop i q, s\<rangle>" |
82 \<Longrightarrow> \<langle>JMPB i # p, q, s\<rangle> -1\<rightarrow> \<langle>rev(take i q) @ JMPB i # p, drop i q, s\<rangle>" |
117 |
83 |
118 inductive_cases execE: "((i#is,p,s),next) : stepa1" |
84 abbreviation |
|
85 stepa :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool" |
|
86 ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where |
|
87 "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^*)" |
|
88 |
|
89 abbreviation |
|
90 stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool" |
|
91 ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where |
|
92 "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^i)" |
|
93 |
|
94 inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1" |
119 |
95 |
120 lemma exec_simp[simp]: |
96 lemma exec_simp[simp]: |
121 "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of |
97 "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of |
122 SET x a \<Rightarrow> t = s[x\<mapsto> a s] \<and> p' = p \<and> q' = i#q | |
98 SET x a \<Rightarrow> t = s[x\<mapsto> a s] \<and> p' = p \<and> q' = i#q | |
123 JMPF b n \<Rightarrow> t=s \<and> (if b s then p' = p \<and> q' = i#q |
99 JMPF b n \<Rightarrow> t=s \<and> (if b s then p' = p \<and> q' = i#q |