TF

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