equal
deleted
inserted
replaced
137 G\<turnstile>Norm s0 -While(e) c-> s1" |
137 G\<turnstile>Norm s0 -While(e) c-> s1" |
138 LoopT:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; the_Bool v; |
138 LoopT:"[| G\<turnstile>Norm s0 -e\<succ>v-> s1; the_Bool v; |
139 G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==> |
139 G\<turnstile>s1 -c-> s2; G\<turnstile>s2 -While(e) c-> s3 |] ==> |
140 G\<turnstile>Norm s0 -While(e) c-> s3" |
140 G\<turnstile>Norm s0 -While(e) c-> s3" |
141 |
141 |
142 lemmas eval_evals_exec_induct = eval_evals_exec.induct [complete_split] |
142 lemmas eval_evals_exec_induct = eval_evals_exec.induct [split_format (complete)] |
143 |
143 |
144 lemma NewCI: "[|new_Addr (heap s) = (a,x); |
144 lemma NewCI: "[|new_Addr (heap s) = (a,x); |
145 s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> |
145 s' = c_hupd (heap s(a\<mapsto>(C,init_vars (fields (G,C))))) (x,s)|] ==> |
146 G\<turnstile>Norm s -NewC C\<succ>Addr a-> s'" |
146 G\<turnstile>Norm s -NewC C\<succ>Addr a-> s'" |
147 apply (simp (no_asm_simp)) |
147 apply (simp (no_asm_simp)) |