63 |
63 |
64 code_pred iexec1 . |
64 code_pred iexec1 . |
65 |
65 |
66 declare iexec1.intros |
66 declare iexec1.intros |
67 |
67 |
68 (* FIXME: why does code gen not work with fun? *) |
68 definition |
69 inductive |
69 exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) |
70 exec1 :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" |
70 where |
71 ("(_/ \<turnstile> (_ \<rightarrow>/ _))" [50,0,0] 50) where |
|
72 "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'" |
|
73 |
|
74 code_pred exec1 . |
|
75 |
|
76 declare exec1.intros [intro!] |
|
77 |
|
78 inductive_cases exec1_elim [elim!]: "P \<turnstile> c \<rightarrow> c'" |
|
79 |
|
80 lemma exec1_simp [simp]: |
|
81 "P \<turnstile> c \<rightarrow> c' = |
71 "P \<turnstile> c \<rightarrow> c' = |
82 (\<exists>i s stk. c = (i,s,stk) \<and> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c' \<and> 0 \<le> i \<and> i < isize P)" |
72 (\<exists>i s stk. c = (i,s,stk) \<and> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c' \<and> 0 \<le> i \<and> i < isize P)" |
83 by auto |
73 |
|
74 declare exec1_def [simp] |
|
75 |
|
76 lemma exec1I [intro, code_pred_intro]: |
|
77 "\<lbrakk> P!!i \<turnstile>i (i,s,stk) \<rightarrow> c'; 0 \<le> i; i < isize P \<rbrakk> \<Longrightarrow> P \<turnstile> (i,s,stk) \<rightarrow> c'" |
|
78 by simp |
84 |
79 |
85 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50) |
80 inductive exec :: "instr list \<Rightarrow> config \<Rightarrow> config \<Rightarrow> bool" ("_/ \<turnstile> (_ \<rightarrow>*/ _)" 50) |
86 where |
81 where |
87 refl: "P \<turnstile> c \<rightarrow>* c" | |
82 refl: "P \<turnstile> c \<rightarrow>* c" | |
88 step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" |
83 step: "P \<turnstile> c \<rightarrow> c' \<Longrightarrow> P \<turnstile> c' \<rightarrow>* c'' \<Longrightarrow> P \<turnstile> c \<rightarrow>* c''" |
89 |
84 |
90 declare refl[intro] step[intro] |
85 declare refl[intro] step[intro] |
91 |
86 |
92 lemmas exec_induct = exec.induct[split_format(complete)] |
87 lemmas exec_induct = exec.induct[split_format(complete)] |
93 |
88 |
94 code_pred exec . |
89 code_pred exec by force |
95 |
90 |
96 values |
91 values |
97 "{(i,map t [''x'',''y''],stk) | i t stk. |
92 "{(i,map t [''x'',''y''],stk) | i t stk. |
98 [LOAD ''y'', STORE ''x''] \<turnstile> |
93 [LOAD ''y'', STORE ''x''] \<turnstile> |
99 (0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}" |
94 (0, [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 4], []) \<rightarrow>* (i,t,stk)}" |