Ver el código de «Tema 14: Expresiones booleanas.» - Demostración automática de teoremas (2014-15)

<source lang = "isar">
theory BExp_b 

imports AExp_b 

begin

subsection "Expresiones booleanas"

text{* Una expresión booleana es:
- una constante booleana, o
- la negación de una expresión booleana, o
- la conjunción de dos expresiones booleanas, o
- la comparación de dos expresiones aritméticas.
*}

text{* Sintaxis:
*}

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

text{* Semántica: valor de una expresión booleana en un estado.
*}

fun bval :: "bexp ⇒ state ⇒ bool" where
"bval (Bc v) s = v" |
"bval (Not b) s = (¬ bval b s)" |
"bval (And b⇩1 b⇩2) s = (bval b⇩1 s ∧ bval b⇩2 s)" |
"bval (Less a⇩1 a⇩2) s = (aval a⇩1 s < aval a⇩2 s)"


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

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

text{* Las reglas de simplificación introducidas por la 
definición son:
*}

thm bval.simps

text{* Establecemos el siguiente lema como regla de simplificación,
con objeto de mejorar los procesos automáticos de demostración: 
*}

lemma bval_And_if[simp]:
  "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)"
by(simp)

text{*
Eliminamos la tercera regla de simplicacción del proceso automático.
*}

declare bval.simps(3)[simp del]


subsection "Simplificación de constantes"

text{* El objetivo de las siguientes funciones es realizar 
una simplificación de las expresiones booleanas. *}

text{* La función less simplificará las expresiones de la forma
"Less (N n1) (N n2)" a "Bc (n1 < n2)".
*}

fun less :: "aexp ⇒ aexp ⇒ bexp" where
"less (N n⇩1) (N n⇩2) = Bc(n⇩1 < n⇩2)" |
"less a⇩1 a⇩2 = Less a⇩1 a⇩2"

text{* Lema: la función less es correcta. 
El valor de la expresión "less a1 a2" en un estado s coincide 
con el valor de "aval a1 s < aval a2 s."
*}

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{* Definimos una función "and" que simplificará las expresiones
booleanas conjuntivas, una de cuyas componentes sea una constante 
booleana.
*}

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⇩1 b⇩2 = And b⇩1 b⇩2"

text{* La función "and" es correcta.
*}

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{* Definimos una función "not" que simplificará las expresiones
booleanas negativas de constantes booleanas.
*}

fun not :: "bexp ⇒ bexp" where
"not (Bc True) = Bc False" |
"not (Bc False) = Bc True" |
"not b = Not b"

text{* Lema: la función not es correcta.
*}

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

text{* La función "bsimp" simplifica las expresiones booleanas, 
mediante las funciones previas.
 *}

fun bsimp :: "bexp ⇒ bexp" where
"bsimp (Bc v) = Bc v" |
"bsimp (Not b) = not (bsimp b)" |
"bsimp (And b⇩1 b⇩2) = and (bsimp b⇩1) (bsimp b⇩2)" |
"bsimp (Less a⇩1 a⇩2) = less (asimp a⇩1) (asimp a⇩2)"


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

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

text{* Teorema: La función bsimp es correcta: el valor de la 
expresión booleana simplificada coincide con el valor de la 
expresión inicial, en cualquier estado.
*}

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

end
</source>