1 theory Machines |
|
2 imports Natural |
|
3 begin |
|
4 |
|
5 lemma converse_in_rel_pow_eq: |
|
6 "((x,z) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R ^^ m))" |
|
7 apply(rule iffI) |
|
8 apply(blast elim:rel_pow_E2) |
|
9 apply (auto simp: rel_pow_commute[symmetric]) |
|
10 done |
|
11 |
|
12 subsection "Instructions" |
|
13 |
|
14 text {* There are only three instructions: *} |
|
15 datatype instr = SET loc aexp | JMPF bexp nat | JMPB nat |
|
16 |
|
17 type_synonym instrs = "instr list" |
|
18 |
|
19 subsection "M0 with PC" |
|
20 |
|
21 inductive_set |
|
22 exec01 :: "instr list \<Rightarrow> ((nat\<times>state) \<times> (nat\<times>state))set" |
|
23 and exec01' :: "[instrs, nat,state, nat,state] \<Rightarrow> bool" |
|
24 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) |
|
25 for P :: "instr list" |
|
26 where |
|
27 "p \<turnstile> \<langle>i,s\<rangle> -1\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)" |
|
28 | 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>" |
|
29 | 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>" |
|
30 | JMPFF: "\<lbrakk> n<size P; P!n = JMPF b i; \<not>b s; m=n+i+1; m \<le> size P \<rbrakk> |
|
31 \<Longrightarrow> P \<turnstile> \<langle>n,s\<rangle> -1\<rightarrow> \<langle>m,s\<rangle>" |
|
32 | 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>" |
|
33 |
|
34 abbreviation |
|
35 exec0s :: "[instrs, nat,state, nat,state] \<Rightarrow> bool" |
|
36 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) where |
|
37 "p \<turnstile> \<langle>i,s\<rangle> -*\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^*" |
|
38 |
|
39 abbreviation |
|
40 exec0n :: "[instrs, nat,state, nat, nat,state] \<Rightarrow> bool" |
|
41 ("(_/ \<turnstile> (1\<langle>_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_\<rangle>))" [50,0,0,0,0] 50) where |
|
42 "p \<turnstile> \<langle>i,s\<rangle> -n\<rightarrow> \<langle>j,t\<rangle> == ((i,s),j,t) : (exec01 p)^^n" |
|
43 |
|
44 subsection "M0 with lists" |
|
45 |
|
46 text {* We describe execution of programs in the machine by |
|
47 an operational (small step) semantics: |
|
48 *} |
|
49 |
|
50 type_synonym config = "instrs \<times> instrs \<times> state" |
|
51 |
|
52 |
|
53 inductive_set |
|
54 stepa1 :: "(config \<times> config)set" |
|
55 and stepa1' :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool" |
|
56 ("((1\<langle>_,/_,/_\<rangle>)/ -1\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) |
|
57 where |
|
58 "\<langle>p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : stepa1" |
|
59 | "\<langle>SET x a#p,q,s\<rangle> -1\<rightarrow> \<langle>p,SET x a#q,s[x\<mapsto> a s]\<rangle>" |
|
60 | "b s \<Longrightarrow> \<langle>JMPF b i#p,q,s\<rangle> -1\<rightarrow> \<langle>p,JMPF b i#q,s\<rangle>" |
|
61 | "\<lbrakk> \<not> b s; i \<le> size p \<rbrakk> |
|
62 \<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>" |
|
63 | "i \<le> size q |
|
64 \<Longrightarrow> \<langle>JMPB i # p, q, s\<rangle> -1\<rightarrow> \<langle>rev(take i q) @ JMPB i # p, drop i q, s\<rangle>" |
|
65 |
|
66 abbreviation |
|
67 stepa :: "[instrs,instrs,state, instrs,instrs,state] \<Rightarrow> bool" |
|
68 ("((1\<langle>_,/_,/_\<rangle>)/ -*\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where |
|
69 "\<langle>p,q,s\<rangle> -*\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^*)" |
|
70 |
|
71 abbreviation |
|
72 stepan :: "[instrs,instrs,state, nat, instrs,instrs,state] \<Rightarrow> bool" |
|
73 ("((1\<langle>_,/_,/_\<rangle>)/ -_\<rightarrow> (1\<langle>_,/_,/_\<rangle>))" 50) where |
|
74 "\<langle>p,q,s\<rangle> -i\<rightarrow> \<langle>p',q',t\<rangle> == ((p,q,s),p',q',t) : (stepa1^^i)" |
|
75 |
|
76 inductive_cases execE: "((i#is,p,s), (is',p',s')) : stepa1" |
|
77 |
|
78 lemma exec_simp[simp]: |
|
79 "(\<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle>) = (case i of |
|
80 SET x a \<Rightarrow> t = s[x\<mapsto> a s] \<and> p' = p \<and> q' = i#q | |
|
81 JMPF b n \<Rightarrow> t=s \<and> (if b s then p' = p \<and> q' = i#q |
|
82 else n \<le> size p \<and> p' = drop n p \<and> q' = rev(take n p) @ i # q) | |
|
83 JMPB n \<Rightarrow> n \<le> size q \<and> t=s \<and> p' = rev(take n q) @ i # p \<and> q' = drop n q)" |
|
84 apply(rule iffI) |
|
85 defer |
|
86 apply(clarsimp simp add: stepa1.intros split: instr.split_asm split_if_asm) |
|
87 apply(erule execE) |
|
88 apply(simp_all) |
|
89 done |
|
90 |
|
91 lemma execn_simp[simp]: |
|
92 "(\<langle>i#p,q,s\<rangle> -n\<rightarrow> \<langle>p'',q'',u\<rangle>) = |
|
93 (n=0 \<and> p'' = i#p \<and> q'' = q \<and> u = s \<or> |
|
94 ((\<exists>m p' q' t. n = Suc m \<and> |
|
95 \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -m\<rightarrow> \<langle>p'',q'',u\<rangle>)))" |
|
96 by(subst converse_in_rel_pow_eq, simp) |
|
97 |
|
98 |
|
99 lemma exec_star_simp[simp]: "(\<langle>i#p,q,s\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>) = |
|
100 (p'' = i#p & q''=q & u=s | |
|
101 (\<exists>p' q' t. \<langle>i#p,q,s\<rangle> -1\<rightarrow> \<langle>p',q',t\<rangle> \<and> \<langle>p',q',t\<rangle> -*\<rightarrow> \<langle>p'',q'',u\<rangle>))" |
|
102 apply(simp add: rtrancl_is_UN_rel_pow del:exec_simp) |
|
103 apply(blast) |
|
104 done |
|
105 |
|
106 declare nth_append[simp] |
|
107 |
|
108 lemma rev_revD: "rev xs = rev ys \<Longrightarrow> xs = ys" |
|
109 by simp |
|
110 |
|
111 lemma [simp]: "(rev xs @ rev ys = rev zs) = (ys @ xs = zs)" |
|
112 apply(rule iffI) |
|
113 apply(rule rev_revD, simp) |
|
114 apply fastsimp |
|
115 done |
|
116 |
|
117 lemma direction1: |
|
118 "\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle> \<Longrightarrow> |
|
119 rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>" |
|
120 apply(induct set: stepa1) |
|
121 apply(simp add:exec01.SET) |
|
122 apply(fastsimp intro:exec01.JMPFT) |
|
123 apply simp |
|
124 apply(rule exec01.JMPFF) |
|
125 apply simp |
|
126 apply fastsimp |
|
127 apply simp |
|
128 apply simp |
|
129 apply simp |
|
130 apply(fastsimp simp add:exec01.JMPB) |
|
131 done |
|
132 |
|
133 (* |
|
134 lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)" |
|
135 apply(induct xs) |
|
136 apply simp_all |
|
137 apply(case_tac i) |
|
138 apply simp_all |
|
139 done |
|
140 |
|
141 lemma rev_drop: "\<And>i. rev (drop i xs) = take (length xs - i) (rev xs)" |
|
142 apply(induct xs) |
|
143 apply simp_all |
|
144 apply(case_tac i) |
|
145 apply simp_all |
|
146 done |
|
147 *) |
|
148 |
|
149 lemma direction2: |
|
150 "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow> |
|
151 rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow> |
|
152 rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>" |
|
153 apply(induct arbitrary: p q p' q' set: exec01) |
|
154 apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj) |
|
155 apply(drule sym) |
|
156 apply simp |
|
157 apply(rule rev_revD) |
|
158 apply simp |
|
159 apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj) |
|
160 apply(drule sym) |
|
161 apply simp |
|
162 apply(rule rev_revD) |
|
163 apply simp |
|
164 apply(simp (no_asm_use) add: neq_Nil_conv append_eq_conv_conj, clarify)+ |
|
165 apply(drule sym) |
|
166 apply simp |
|
167 apply(rule rev_revD) |
|
168 apply simp |
|
169 apply(clarsimp simp add: neq_Nil_conv append_eq_conv_conj) |
|
170 apply(drule sym) |
|
171 apply(simp add:rev_take) |
|
172 apply(rule rev_revD) |
|
173 apply(simp add:rev_drop) |
|
174 done |
|
175 |
|
176 |
|
177 theorem M_eqiv: |
|
178 "(\<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>) = |
|
179 (rev p' @ q' = rev p @ q \<and> rev p @ q \<turnstile> \<langle>size p,s\<rangle> -1\<rightarrow> \<langle>size p',t\<rangle>)" |
|
180 by (blast dest: direction1 direction2) |
|
181 |
|
182 end |
|