362 steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81) |
362 steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81) |
363 where "G\<turnstile>p \<mapsto>* p' \<equiv> (p,p') \<in> {(x, y). step G x y}\<^sup>*" |
363 where "G\<turnstile>p \<mapsto>* p' \<equiv> (p,p') \<in> {(x, y). step G x y}\<^sup>*" |
364 |
364 |
365 (* Equivalenzen: |
365 (* Equivalenzen: |
366 Bigstep zu Smallstep komplett. |
366 Bigstep zu Smallstep komplett. |
367 Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots> |
367 Smallstep zu Bigstep, nur wenn nicht die Ausdrücke Callee, FinA ,\<dots> |
368 *) |
368 *) |
369 |
369 |
370 (* |
370 (* |
371 lemma imp_eval_trans: |
371 lemma imp_eval_trans: |
372 assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" |
372 assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" |
373 shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)" |
373 shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)" |
374 *) |
374 *) |
375 (* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var! |
375 (* Jetzt muss man bei trans natürlich wieder unterscheiden: Stmt, Expr, Var! |
376 Sowas blödes: |
376 Sowas blödes: |
377 Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann |
377 Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann |
378 the_vals definieren\<dots> |
378 the_vals definieren\<dots> |
379 G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v |
379 G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v |
380 *) |
380 *) |
381 |
381 |