equal
deleted
inserted
replaced
661 with while eval_e continue eval_c s3 show ?thesis |
661 with while eval_e continue eval_c s3 show ?thesis |
662 by (auto intro!: eval.Loop) |
662 by (auto intro!: eval.Loop) |
663 qed |
663 qed |
664 qed |
664 qed |
665 |
665 |
666 |
|
667 ML"Addsimprocs [eval_expr_proc, eval_var_proc, eval_exprs_proc, eval_stmt_proc]" |
|
668 |
|
669 lemma MGFn_Loop: |
666 lemma MGFn_Loop: |
670 assumes mfg_e: "G,(A::state triple set)\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" |
667 assumes mfg_e: "G,(A::state triple set)\<turnstile>{=:n} \<langle>e\<rangle>\<^sub>e\<succ> {G\<rightarrow>}" |
671 and mfg_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" |
668 and mfg_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" |
672 and wf: "wf_prog G" |
669 and wf: "wf_prog G" |
673 shows "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" |
670 shows "G,A\<turnstile>{=:n} \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" |