135 lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)] |
135 lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)] |
136 |
136 |
137 lemma NewCI: "[|new_Addr (heap s) = (a,x); |
137 lemma NewCI: "[|new_Addr (heap s) = (a,x); |
138 s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> |
138 s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> |
139 G\<turnstile>Norm s -NewC C\<succ>Addr a-> s'" |
139 G\<turnstile>Norm s -NewC C\<succ>Addr a-> s'" |
140 apply (simp (no_asm_simp)) |
140 apply simp |
141 apply (rule eval_evals_exec.NewC) |
141 apply (rule eval_evals_exec.NewC) |
142 apply auto |
142 apply auto |
143 done |
143 done |
144 |
144 |
145 lemma eval_evals_exec_no_xcpt: |
145 lemma eval_evals_exec_no_xcpt: |
146 "!!s s'. (G\<turnstile>(x,s) -e \<succ> v -> (x',s') --> x'=None --> x=None) \<and> |
146 "!!s s'. (G\<turnstile>(x,s) -e \<succ> v -> (x',s') --> x'=None --> x=None) \<and> |
147 (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x'=None --> x=None) \<and> |
147 (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x'=None --> x=None) \<and> |
148 (G\<turnstile>(x,s) -c -> (x',s') --> x'=None --> x=None)" |
148 (G\<turnstile>(x,s) -c -> (x',s') --> x'=None --> x=None)" |
149 apply(simp (no_asm_simp) only: split_tupled_all) |
149 apply(simp only: split_tupled_all) |
150 apply(rule eval_evals_exec_induct) |
150 apply(rule eval_evals_exec_induct) |
151 apply(unfold c_hupd_def) |
151 apply(unfold c_hupd_def) |
152 apply(simp_all) |
152 apply(simp_all) |
153 done |
153 done |
154 |
154 |
171 |
171 |
172 lemma eval_evals_exec_xcpt: |
172 lemma eval_evals_exec_xcpt: |
173 "!!s s'. (G\<turnstile>(x,s) -e \<succ> v -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and> |
173 "!!s s'. (G\<turnstile>(x,s) -e \<succ> v -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and> |
174 (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and> |
174 (G\<turnstile>(x,s) -es[\<succ>]vs-> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s) \<and> |
175 (G\<turnstile>(x,s) -c -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s)" |
175 (G\<turnstile>(x,s) -c -> (x',s') --> x=Some xc --> x'=Some xc \<and> s'=s)" |
176 apply (simp (no_asm_simp) only: split_tupled_all) |
176 apply (simp only: split_tupled_all) |
177 apply (rule eval_evals_exec_induct) |
177 apply (rule eval_evals_exec_induct) |
178 apply (unfold c_hupd_def) |
178 apply (unfold c_hupd_def) |
179 apply (simp_all) |
179 apply (simp_all) |
180 done |
180 done |
181 |
181 |