Mjoseh: Protegió «TF» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-06-18T06:52:23Z

Protegió «TF» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹Expresiones booleanas y expresiones condicionales› theory Trabajo_final imports Main begin text ‹El objetivo del trabajo es dem…»

2020-06-18T06:52:13Z

Página creada con «<source lang = "isabelle"> chapter ‹Expresiones booleanas y expresiones condicionales› theory Trabajo_final imports Main begin text ‹El objetivo del trabajo es dem…»

Página nueva

<source lang = "isabelle">
chapter ‹Expresiones booleanas y expresiones condicionales›

theory Trabajo_final
imports Main
begin

text ‹El objetivo del trabajo es demostrar las propiedades de los 5
ejercicios de la forma más detallada posible.›

text ‹------------------------------------------------------------------
Definición. La expresiones booleanas se definen por
* las constantes booleanas son expresiones,
* las variables son expresiones,
* Si e es una expresión, entonces ¬e también lo es.
* Si e1 y e2 son expresiones, entonces e1 ∧ e2 también lo es.

Definir exp_booleana como el tipo de las expresiones booleanas.
---------------------------------------------------------------------›

datatype exp_booleana = Const bool
| Var nat
| Neg exp_booleana
| And exp_booleana exp_booleana

text ‹------------------------------------------------------------------
Definición. Una interpretación es una función i que asigna a cada
número natural un booleano de forma que el vlor de la variable
'Var n' en la interpretación 'i' es 'i(n)'.

Definir la función
valor :: exp_booleana ⇒ (nat ⇒ bool) ⇒ bool
tal que (valor e i) es el valor de la expresión booleana e en la
interpretación i. Por ejemplo,
value "(valor (Var 3) (λx. False))
es False
---------------------------------------------------------------------›

fun valor :: "exp_booleana ⇒ (nat ⇒ bool) ⇒ bool" where
"valor (Const b) _ = b"
| "valor (Var n) i = i n "
| "valor (Neg e) i = (¬ (valor e i))"
| "valor (And e1 e2) i = (valor e1 i ∧ valor e2 i)"

text ‹------------------------------------------------------------------
Definición. La expresiones if se definen por
* las constantes booleanas son expresiones,
* las variables son expresiones,
* Si e, e1 y e2 son expresiones, entonces (if e e1 e2) también lo es.

Definir exp_if como el tipo de las expresiones if.
---------------------------------------------------------------------›

datatype exp_if = CIF bool
| VIF nat
| IF exp_if exp_if exp_if

text ‹------------------------------------------------------------------
Definición. Definir la función
valor_if :: exp_if ⇒ (nat ⇒ bool) ⇒ bool
tal que (valor_if e i) es el valor de la expresión if e en la
interpretación i.
---------------------------------------------------------------------›

fun valor_if :: "exp_if ⇒ (nat ⇒ bool) ⇒ bool" where
"valor_if (CIF b) _ = b"
| "valor_if (VIF n) i = i n"
| "valor_if (IF e e1 e2) i = (if (valor_if e i)
then (valor_if e1 i)
else (valor_if e2 i))"

text ‹------------------------------------------------------------------
Definición. Definir la función
bool2if :: exp_booleana ⇒ exp_if
tal que (bool2if e) es una expresión if equivalente a la expresión
booleana e.
---------------------------------------------------------------------›

fun bool2if :: "exp_booleana ⇒ exp_if" where
"bool2if (Const b) = CIF b"
| "bool2if (Var n) = VIF n"
| "bool2if (Neg e) = IF (bool2if e) (CIF False) (CIF True)"
| "bool2if (And e1 e2) = IF (bool2if e1) (bool2if e2) (CIF False)"

text ‹------------------------------------------------------------------
Ejercicio 1. Demostrar que para cualquier expresión boolena e, son
equivalentes (bool2if e) y e.
---------------------------------------------------------------------›

lemma valor_if_bool2if:
"valor_if (bool2if e) ent = valor e ent"
oops

text ‹------------------------------------------------------------------
Definición. Un expresión if, e, está en forma normal si para cada
subexpresión de e de la forma (if c e1 e2) se tiene que c es una
constante o una variable.

Definir la función
es_normal :: exp_if ⇒ bool
tal que (es_normal e) se verifica si e está en forma normal.
---------------------------------------------------------------------›

fun es_normal :: "exp_if ⇒ bool" where
"es_normal (CIF _) = True"
| "es_normal (VIF _) = True"
| "es_normal (IF (CIF _) e1 e2) = (es_normal e1 ∧ es_normal e2)"
| "es_normal (IF (VIF _) e1 e2) = (es_normal e1 ∧ es_normal e2)"
| "es_normal _ = False"

text ‹------------------------------------------------------------------
Definición. Definir la función
normal :: exp_if ⇒ exp_if
tal que (normal e) es una expresión if en forma normal equivalente a
la expresión e.
--------------------------------------------------------------------- ›

fun normalAux :: "exp_if ⇒ exp_if ⇒ exp_if ⇒ exp_if" where
"normalAux (CIF b) e1 e2 = IF (CIF b) e1 e2"
| "normalAux (VIF n) e1 e2 = IF (VIF n) e1 e2"
| "normalAux (IF a a1 a2) e1 e2 =
normalAux a (normalAux a1 e1 e2) (normalAux a2 e1 e2)"

fun normal :: "exp_if ⇒ exp_if" where
"normal (CIF b) = CIF b"
| "normal (VIF n) = VIF n"
| "normal (IF e e1 e2) = normalAux e (normal e1) (normal e2)"

text ‹------------------------------------------------------------------
Ejercicio 2. Demostrar que la forma normal de una expresión if es
equivalente a la expresión; es decir,
valor_if (normal e) i = valor_if e i
---------------------------------------------------------------------›

lemma valor_if_normal:
"valor_if (normal b) ent = valor_if b ent"
oops

text ‹------------------------------------------------------------------
Ejercicio 3. Demostrar que para toda expresión if e, (normal e) está
en forma normal.
---------------------------------------------------------------------›

lemma es_normal_normal:
"es_normal (normal b)"
oops

text ‹------------------------------------------------------------------
Definición. Definir la función
bool2ifN :: exp_booleana ⇒ exp_if
tal que (bool2ifN e) es una expresión if en forma normal equivalente a
la expresión Booleana e.
---------------------------------------------------------------------›

definition bool2ifN :: "exp_booleana ⇒ exp_if" where
"bool2ifN e ≡ normal (bool2if e)"

text ‹------------------------------------------------------------------
Ejercicio 4. Demostrar que para toda expresión booleana e,
(bool2ifN e) está en forma normal.
---------------------------------------------------------------------›

lemma es_normal_bool2ifN:
"es_normal (bool2ifN e)"
oops

text ‹------------------------------------------------------------------
Ejercicio 5. Demostrar que para toda expresión booleana e,
(bool2ifN e) es equivalente a e.
---------------------------------------------------------------------›

lemma valor_if_bool2ifN:
"valor_if (bool2ifN e) ent = valor e ent"
oops

end

</source>

← Revisión anterior	Revisión del 06:52 18 jun 2020
(Sin diferencias)

TF - Historial de revisiones

Mjoseh: Protegió «TF» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « chapter ‹Expresiones booleanas y expresiones condicionales› theory Trabajo_final imports Main begin text ‹El objetivo del trabajo es dem…»