16 "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" | |
16 "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" | |
17 "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')" |
17 "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')" |
18 |
18 |
19 text {* The possible successor PCs of an instruction at position @{term n} *} |
19 text {* The possible successor PCs of an instruction at position @{term n} *} |
20 text_raw{*\snip{isuccsdef}{0}{1}{% *} |
20 text_raw{*\snip{isuccsdef}{0}{1}{% *} |
21 definition |
21 definition isuccs :: "instr \<Rightarrow> int \<Rightarrow> int set" where |
22 "isuccs i n \<equiv> case i of |
22 "isuccs i n = (case i of |
23 JMP j \<Rightarrow> {n + 1 + j} |
23 JMP j \<Rightarrow> {n + 1 + j} | |
24 | JMPLESS j \<Rightarrow> {n + 1 + j, n + 1} |
24 JMPLESS j \<Rightarrow> {n + 1 + j, n + 1} | |
25 | JMPGE j \<Rightarrow> {n + 1 + j, n + 1} |
25 JMPGE j \<Rightarrow> {n + 1 + j, n + 1} | |
26 | _ \<Rightarrow> {n +1}" |
26 _ \<Rightarrow> {n +1})" |
27 text_raw{*}%endsnip*} |
27 text_raw{*}%endsnip*} |
28 |
28 |
29 text {* The possible successors PCs of an instruction list *} |
29 text {* The possible successors PCs of an instruction list *} |
30 definition |
30 definition succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where |
31 succs :: "instr list \<Rightarrow> int \<Rightarrow> int set" where |
31 "succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}" |
32 "succs P n = {s. \<exists>i::int. 0 \<le> i \<and> i < size P \<and> s \<in> isuccs (P!!i) (n+i)}" |
|
33 |
32 |
34 text {* Possible exit PCs of a program *} |
33 text {* Possible exit PCs of a program *} |
35 definition |
34 definition exits :: "instr list \<Rightarrow> int set" where |
36 "exits P = succs P 0 - {0..< size P}" |
35 "exits P = succs P 0 - {0..< size P}" |
37 |
36 |
38 |
37 |
39 subsection {* Basic properties of @{term exec_n} *} |
38 subsection {* Basic properties of @{term exec_n} *} |
40 |
39 |
41 lemma exec_n_exec: |
40 lemma exec_n_exec: |