fun aval :: "aexp \ state \ val option" where "aval (N i) s = Some i" | "aval (V x) s = s x" | "aval (Plus a\<^sub>1 a\<^sub>2) s =
(case (aval a\<^sub>1 s, aval a\<^sub>2 s) of
(Some i\<^sub>1,Some i\<^sub>2) \<Rightarrow> Some(i\<^sub>1+i\<^sub>2) | _ \<Rightarrow> None)"
fun bval :: "bexp \ state \ bool option" where "bval (Bc v) s = Some v" | "bval (Not b) s = (case bval b s of None \ None | Some bv \ Some(\ bv))" | "bval (And b\<^sub>1 b\<^sub>2) s = (case (bval b\<^sub>1 s, bval b\<^sub>2 s) of
(Some bv\<^sub>1, Some bv\<^sub>2) \<Rightarrow> Some(bv\<^sub>1 & bv\<^sub>2) | _ \<Rightarrow> None)" | "bval (Less a\<^sub>1 a\<^sub>2) s = (case (aval a\<^sub>1 s, aval a\<^sub>2 s) of
(Some i\<^sub>1, Some i\<^sub>2) \<Rightarrow> Some(i\<^sub>1 < i\<^sub>2) | _ \<Rightarrow> None)"
lemma aval_Some: "vars a \ dom s \ \ i. aval a s = Some i" by (induct a) auto
lemma bval_Some: "vars b \ dom s \ \ bv. bval b s = Some bv" by (induct b) (auto dest!: aval_Some)
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
