equal
deleted
inserted
replaced
166 apply(rule exec01.JMPFF) |
166 apply(rule exec01.JMPFF) |
167 apply simp |
167 apply simp |
168 apply fastsimp |
168 apply fastsimp |
169 apply simp |
169 apply simp |
170 apply simp |
170 apply simp |
171 apply arith |
171 apply simp |
172 apply simp |
|
173 apply arith |
|
174 apply(fastsimp simp add:exec01.JMPB) |
172 apply(fastsimp simp add:exec01.JMPB) |
175 done |
173 done |
|
174 |
176 (* |
175 (* |
177 lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)" |
176 lemma rev_take: "\<And>i. rev (take i xs) = drop (length xs - i) (rev xs)" |
178 apply(induct xs) |
177 apply(induct xs) |
179 apply simp_all |
178 apply simp_all |
180 apply(case_tac i) |
179 apply(case_tac i) |
186 apply simp_all |
185 apply simp_all |
187 apply(case_tac i) |
186 apply(case_tac i) |
188 apply simp_all |
187 apply simp_all |
189 done |
188 done |
190 *) |
189 *) |
|
190 |
191 lemma direction2: |
191 lemma direction2: |
192 "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow> |
192 "rpq \<turnstile> \<langle>sp,s\<rangle> -1\<rightarrow> \<langle>sp',t\<rangle> \<Longrightarrow> |
193 rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow> |
193 rpq = rev p @ q & sp = size p & sp' = size p' \<longrightarrow> |
194 rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>" |
194 rev p' @ q' = rev p @ q \<longrightarrow> \<langle>q,p,s\<rangle> -1\<rightarrow> \<langle>q',p',t\<rangle>" |
195 apply(induct fixing: p q p' q' set: exec01) |
195 apply(induct fixing: p q p' q' set: exec01) |