equal
deleted
inserted
replaced
7 subsection {* Definitions *} |
7 subsection {* Definitions *} |
8 |
8 |
9 text {* Execution in @{term n} steps for simpler induction *} |
9 text {* Execution in @{term n} steps for simpler induction *} |
10 primrec |
10 primrec |
11 exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" |
11 exec_n :: "instr list \<Rightarrow> config \<Rightarrow> nat \<Rightarrow> config \<Rightarrow> bool" |
12 ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,55,55] 55) |
12 ("_/ \<turnstile> (_ \<rightarrow>^_/ _)" [65,0,1000,55] 55) |
13 where |
13 where |
14 "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" | |
14 "P \<turnstile> c \<rightarrow>^0 c' = (c'=c)" | |
15 "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')" |
15 "P \<turnstile> c \<rightarrow>^(Suc n) c'' = (\<exists>c'. (P \<turnstile> c \<rightarrow> c') \<and> P \<turnstile> c' \<rightarrow>^n c'')" |
16 |
16 |
17 text {* The possible successor pc's of an instruction at position @{term n} *} |
17 text {* The possible successor pc's of an instruction at position @{term n} *} |
39 by (induct n arbitrary: c) (auto intro: exec.step) |
39 by (induct n arbitrary: c) (auto intro: exec.step) |
40 |
40 |
41 lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp |
41 lemma exec_0 [intro!]: "P \<turnstile> c \<rightarrow>^0 c" by simp |
42 |
42 |
43 lemma exec_Suc [trans]: |
43 lemma exec_Suc [trans]: |
44 "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^Suc n c''" |
44 "\<lbrakk> P \<turnstile> c \<rightarrow> c'; P \<turnstile> c' \<rightarrow>^n c'' \<rbrakk> \<Longrightarrow> P \<turnstile> c \<rightarrow>^(Suc n) c''" |
45 by (fastsimp simp del: split_paired_Ex) |
45 by (fastsimp simp del: split_paired_Ex) |
46 |
46 |
47 lemma exec_exec_n: |
47 lemma exec_exec_n: |
48 "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'" |
48 "P \<turnstile> c \<rightarrow>* c' \<Longrightarrow> \<exists>n. P \<turnstile> c \<rightarrow>^n c'" |
49 by (induct rule: exec.induct) (auto intro: exec_Suc) |
49 by (induct rule: exec.induct) (auto intro: exec_Suc) |