equal
deleted
inserted
replaced
30 fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where |
30 fun exec :: "instr list \<Rightarrow> state \<Rightarrow> stack \<Rightarrow> stack" where |
31 "exec [] _ stk = stk" | |
31 "exec [] _ stk = stk" | |
32 "exec (i#is) s stk = exec is s (exec1 i s stk)" |
32 "exec (i#is) s stk = exec is s (exec1 i s stk)" |
33 text_raw{*}%endsnip*} |
33 text_raw{*}%endsnip*} |
34 |
34 |
35 value "exec [LOADI 5, LOAD ''y'', ADD] |
35 value "exec [LOADI 5, LOAD ''y'', ADD] <''x'' := 42, ''y'' := 43> [50]" |
36 <''x'' := 42, ''y'' := 43> [50]" |
|
37 |
36 |
38 lemma exec_append[simp]: |
37 lemma exec_append[simp]: |
39 "exec (is1@is2) s stk = exec is2 s (exec is1 s stk)" |
38 "exec (is1@is2) s stk = exec is2 s (exec is1 s stk)" |
40 apply(induction is1 arbitrary: stk) |
39 apply(induction is1 arbitrary: stk) |
41 apply (auto) |
40 apply (auto) |