inductive D :: "vname set \ com \ vname set \ bool" where
Skip: "D A SKIP A" |
Assign: "vars a \ A \ D A (x ::= a) (insert x A)" |
Seq: "\ D A\<^sub>1 c\<^sub>1 A\<^sub>2; D A\<^sub>2 c\<^sub>2 A\<^sub>3 \ \ D A\<^sub>1 (c\<^sub>1;; c\<^sub>2) A\<^sub>3" | If: "\ vars b \ A; D A c\<^sub>1 A\<^sub>1; D A c\<^sub>2 A\<^sub>2 \ \
D A (IF b THEN c\<^sub>1 ELSE c\<^sub>2) (A\<^sub>1 Int A\<^sub>2)" |
While: "\ vars b \ A; D A c A' \ \ D A (WHILE b DO c) A"
inductive_cases [elim!]: "D A SKIP A'" "D A (x ::= a) A'" "D A (c1;;c2) A'" "D A (IF b THEN c1 ELSE c2) A'" "D A (WHILE b DO c) A'"
lemma D_incr: "D A c A' \ A \ A'" by (induct rule: D.induct) auto
end
¤ 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.0.12Bemerkung:
(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.
