fun aval :: "aexp ==> state ==> val option"where "aval (N i) s = Some i" | "aval (V x) s = s x" | "aval (Plus a1 a2) s = (case (aval a1 s, aval a2 s) of (Some i1,Some i2) ==> Some(i1+i2) | _ ==> 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 b1 b2) s = (case (bval b1 s, bval b2 s) of (Some bv1, Some bv2) ==> Some(bv1 & bv2) | _ ==> None)" | "bval (Less a1 a2) s = (case (aval a1 s, aval a2 s) of (Some i1, Some i2) ==> Some(i1 < i2) | _ ==> 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
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet am 2026-06-09)
¤
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 und die Messung sind noch experimentell.
