Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: BExp.thy Sprache: Isabelle

Original von: Isabelle^©

subsection "Boolean Expressions"

theory BExp imports AExp begin

datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp

text_raw\<open>\snip{BExpbvaldef}{1}{2}{%\<close>
fun bval :: "bexp \ state \ bool" where
"bval (Bc v) s = v" |
"bval (Not b) s = (\ bval b s)" |
"bval (And b\<^sub>1 b\<^sub>2) s = (bval b\<^sub>1 s \ bval b\<^sub>2 s)" |
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
text_raw\<open>}%endsnip\<close>

value "bval (Less (V ''x'') (Plus (N 3) (V ''y'')))
<''x'' := 3, ''y'' := 1>"

subsection "Constant Folding"

text\<open>Optimizing constructors:\<close>

text_raw\<open>\snip{BExplessdef}{0}{2}{%\<close>
fun less :: "aexp \ aexp \ bexp" where
"less (N n\<^sub>1) (N n\<^sub>2) = Bc(n\<^sub>1 < n\<^sub>2)" |
"less a\<^sub>1 a\<^sub>2 = Less a\<^sub>1 a\<^sub>2"
text_raw\<open>}%endsnip\<close>

lemma [simp]: "bval (less a1 a2) s = (aval a1 s < aval a2 s)"
apply(induction a1 a2 rule: less.induct)
apply simp_all
done

text_raw\<open>\snip{BExpanddef}{2}{2}{%\<close>
fun "and" :: "bexp \ bexp \ bexp" where
"and (Bc True) b = b" |
"and b (Bc True) = b" |
"and (Bc False) b = Bc False" |
"and b (Bc False) = Bc False" |
"and b\<^sub>1 b\<^sub>2 = And b\<^sub>1 b\<^sub>2"
text_raw\<open>}%endsnip\<close>

lemma bval_and[simp]: "bval (and b1 b2) s = (bval b1 s \ bval b2 s)"
apply(induction b1 b2 rule: and.induct)
apply simp_all
done

text_raw\<open>\snip{BExpnotdef}{2}{2}{%\<close>
fun not :: "bexp \ bexp" where
"not (Bc True) = Bc False" |
"not (Bc False) = Bc True" |
"not b = Not b"
text_raw\<open>}%endsnip\<close>

lemma bval_not[simp]: "bval (not b) s = (\ bval b s)"
apply(induction b rule: not.induct)
apply simp_all
done

text\<open>Now the overall optimizer:\<close>

text_raw\<open>\snip{BExpbsimpdef}{0}{2}{%\<close>
fun bsimp :: "bexp \ bexp" where
"bsimp (Bc v) = Bc v" |
"bsimp (Not b) = not(bsimp b)" |
"bsimp (And b\<^sub>1 b\<^sub>2) = and (bsimp b\<^sub>1) (bsimp b\<^sub>2)" |
"bsimp (Less a\<^sub>1 a\<^sub>2) = less (asimp a\<^sub>1) (asimp a\<^sub>2)"
text_raw\<open>}%endsnip\<close>

value "bsimp (And (Less (N 0) (N 1)) b)"

value "bsimp (And (Less (N 1) (N 0)) (Bc True))"

theorem "bval (bsimp b) s = bval b s"
apply(induction b)
apply simp_all
done

end

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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.