equal
deleted
inserted
replaced
68 by auto |
68 by auto |
69 |
69 |
70 lemma update_at_index: " |
70 lemma update_at_index: " |
71 \<lbrakk> distinct (gjmb_plns (gmb G C S)); |
71 \<lbrakk> distinct (gjmb_plns (gmb G C S)); |
72 x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow> |
72 x \<in> set (gjmb_plns (gmb G C S)); x \<noteq> This \<rbrakk> \<Longrightarrow> |
73 locvars_xstate G C S (Norm (h, l))[index (gmb G C S) x := val] = |
73 (locvars_xstate G C S (Norm (h, l)))[index (gmb G C S) x := val] = |
74 locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))" |
74 locvars_xstate G C S (Norm (h, l(x\<mapsto>val)))" |
75 apply (simp only: locvars_xstate_def locvars_locals_def index_def) |
75 apply (simp only: locvars_xstate_def locvars_locals_def index_def) |
76 apply (case_tac "gmb G C S" rule: prod.exhaust, simp) |
76 apply (case_tac "gmb G C S" rule: prod.exhaust, simp) |
77 apply (rename_tac a b) |
77 apply (rename_tac a b) |
78 apply (case_tac b, simp) |
78 apply (case_tac b, simp) |