equal
deleted
inserted
replaced
50 theorem exec_all_trans: "\<lbrakk>(exec_all G s0 s1); (exec_all G s1 s2)\<rbrakk> \<Longrightarrow> (exec_all G s0 s2)" |
50 theorem exec_all_trans: "\<lbrakk>(exec_all G s0 s1); (exec_all G s1 s2)\<rbrakk> \<Longrightarrow> (exec_all G s0 s2)" |
51 apply (auto simp: exec_all_def elim: Transitive_Closure.rtrancl_trans) |
51 apply (auto simp: exec_all_def elim: Transitive_Closure.rtrancl_trans) |
52 done |
52 done |
53 |
53 |
54 theorem exec_all_refl: "exec_all G s s" |
54 theorem exec_all_refl: "exec_all G s s" |
55 by (simp only: exec_all_def (* CBtrancl, rule rtrancl_refl*) ) |
55 by (simp only: exec_all_def) |
56 |
56 |
57 |
57 |
58 theorem exec_instr_in_exec_all: |
58 theorem exec_instr_in_exec_all: |
59 "\<lbrakk> exec_instr i G hp stk lvars C S pc frs = (None, hp', frs'); |
59 "\<lbrakk> exec_instr i G hp stk lvars C S pc frs = (None, hp', frs'); |
60 gis (gmb G C S) ! pc = i\<rbrakk> \<Longrightarrow> |
60 gis (gmb G C S) ! pc = i\<rbrakk> \<Longrightarrow> |