TF sol

chapter ‹Expresiones booleanas y expresiones condicionales›

theory Trabajo_final_sol
imports Main 
begin

section ‹Expresiones booleanas›

text ‹------------------------------------------------------------------ 
  Ejercicio 1. 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

section ‹El valor de las expresiones boolenas›

text ‹------------------------------------------------------------------ 
  Ejercicio 2. Una interpretación es una función i que asigna a cada
  número natural un booleano de forma que el valor 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)"

section ‹Expresiones If›

text ‹------------------------------------------------------------------ 
  Ejercicio 3. 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 ‹------------------------------------------------------------------ 
  Ejercicio 4. 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))"

section ‹Transformación de expresiones booleanas en expresiones if›

subsection ‹Definición de bool2if›

text ‹------------------------------------------------------------------ 
  Ejercicio 5. 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 6. Demostrar que para cualquier expresión boolena e, son
  equivalentes (bool2if e) y e.
  ---------------------------------------------------------------------›

subsection ‹Demostraciones de valor_if_bool2if›

subsubsection ‹Demostración estructurada de valor_if_bool2if›
lemma valor_if_bool2if_E:
  "valor_if (bool2if e) ent = valor e ent"
proof (induct e)
  case (Const x)
  then show ?case by simp
next
  case (Var x)
  then show ?case by simp
next
  case (Neg e)
  then show ?case by simp
next
  case (And e1 e2)
  then show ?case by simp
qed

subsubsection ‹Demostración automática de valor_if_bool2if›

lemma valor_if_bool2if_A:
  "valor_if (bool2if e) ent = valor e ent"
  by (induct e) simp_all

subsubsection ‹Demostración declarativa detallada de valor_if_bool2if›

lemma valor_if_bool2if:
  "valor_if (bool2if e) ent = valor e ent"
proof (induct e)
  fix b
  have "valor_if (bool2if (Const b)) ent = valor_if (CIF b) ent"
    by (simp only: bool2if.simps(1))
  also have "… = b"
    by (simp only: valor_if.simps(1))
  also have "… = valor (Const b) ent"
    by (simp only: valor.simps(1))
  finally show "valor_if (bool2if (Const b)) ent = valor (Const b) ent" 
    by this
next
  fix n
  have "valor_if (bool2if (Var n)) ent = valor_if (VIF n) ent"
    by (simp only: bool2if.simps(2))
  also have "… = ent n"
    by (simp only: valor_if.simps(2))
  also have "… = valor (Var n) ent"
    by (simp only: valor.simps(2))
  finally show "valor_if (bool2if (Var n)) ent = valor (Var n) ent" 
    by this
next
  fix e
  assume HI: "valor_if (bool2if e) ent = valor e ent"
  have "valor_if (bool2if (Neg e)) ent = 
        valor_if (IF (bool2if e) (CIF False) (CIF True)) ent"
    by (simp only: bool2if.simps(3))
  also have "… = (if valor_if (bool2if e) ent 
                   then valor_if (CIF False) ent
                   else valor_if (CIF True) ent)"
    by (simp only: valor_if.simps(3))
  also have "… = (if valor e ent 
                   then False
                   else True)"
    by (simp only: HI valor_if.simps(1))
    also have "… = (¬ valor e ent)" 
    by (rule SMT.z3_rule(52))
  also have "… = valor (Neg e) ent"
    by (simp only: valor.simps(3))
  finally show "valor_if (bool2if (Neg e)) ent = valor (Neg e) ent"
    by this
next
  fix e1 e2
  assume HI1: "valor_if (bool2if e1) ent = valor e1 ent" and
         HI2: "valor_if (bool2if e2) ent = valor e2 ent"
  have "valor_if (bool2if (And e1 e2)) ent = 
        valor_if (IF (bool2if e1) (bool2if e2) (CIF False)) ent"
    by (simp only: bool2if.simps(4))
  also have "… = (if valor_if (bool2if e1) ent 
                   then valor_if (bool2if e2) ent
                   else valor_if (CIF False) ent)"
    by (simp only: valor_if.simps(3))
  also have "… = (if valor e1 ent 
                   then valor e2 ent
                   else False)"
    by (simp only: HI1 HI2 valor_if.simps(1))
  also have "… = ((valor e1 ent ∧ valor e2 ent) ∨
                   (¬(valor e1 ent) ∧ False))"
    by (rule if_bool_eq_disj)
    also have "… = ((valor e1 ent ∧ valor e2 ent) ∨ False)"
    by (simp only: simp_thms(23))
  also have "… = (valor e1 ent ∧ valor e2 ent)"
    by (simp only: simp_thms(31))
  also have "… = valor (And e1 e2) ent"
    by (simp only: valor.simps(4))
  finally show "valor_if (bool2if (And e1 e2)) ent = 
                valor (And e1 e2) ent"
    by this
qed

subsubsection ‹Demostración aplicativa detallada de valor_if_bool2if›

lemma valor_if_bool2if_aplicativa:
  "valor_if (bool2if e) ent = valor e ent"
  apply (induct e)
     apply (simp only: bool2if.simps valor_if.simps valor.simps)
    apply (simp only: bool2if.simps valor_if.simps valor.simps)
   apply (simp only: bool2if.simps)
   apply (simp only: valor_if.simps)
   apply (simp only: valor.simps)
   apply (split if_split)
   apply (rule conjI)
    apply (rule impI)
    apply (rule iffI)
     apply (rule ccontr, assumption)
    apply (erule notE, assumption)
   apply (rule impI)
   apply (rule iffI, assumption)
   apply (simp only: TrueI)
  apply (simp only: bool2if.simps)
  apply (simp only: valor_if.simps)
  apply (simp only: valor.simps)
  apply (split if_split)
  apply (rule conjI)
   apply (rule impI)
   apply (rule iffI)
    apply (erule conjI, assumption)
   apply (erule conjunct2)
  apply (rule impI)
  apply (rule iffI)
   apply (rule FalseE, assumption)
  apply (erule notE)
  apply (erule conjunct1)
  done

section ‹Formas normales›

subsection ‹Definición de es_normal›

text ‹------------------------------------------------------------------ 
  Ejercicio 6. 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"

subsection ‹Definición de normal›

text ‹------------------------------------------------------------------ 
  Ejercicio 7. 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)" 

section ‹Corrección de la normalización›

text ‹------------------------------------------------------------------
  Ejercicio 8. 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
  ---------------------------------------------------------------------›

subsection ‹Lema auxiliar valor_if_normalAux›

subsubsection ‹Demostración estructurada de valor_if_normalAux›

lemma valor_if_normalAux_E:
  "valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
proof (induct e arbitrary: e1 e2)
  case (CIF x)
  then show ?case by simp
next
  case (VIF x)
  then show ?case by simp
next
  case (IF e1 e2 e3)
  then show ?case by simp
qed

subsubsection ‹Demostración automática de valor_if_normalAux›

lemma valor_if_normalAux_A:
  "valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
  by (induct e arbitrary: e1 e2) simp_all

subsubsection ‹Demostración declarativa detallada de valor_if_normalAux›

lemma if_if:
  fixes A and A1 and A2 and C1 and C2 :: bool
  shows
  "(if A
    then (if A1 then C1 else C2)
    else (if A2 then C1 else C2)) =
   (if (if A then A1 else A2)
    then C1
    else C2)"  
  by (cases A; cases A1; cases A2) 
     (simp_all only: if_True if_False)

lemma valor_if_IF:
  "valor_if (IF a (IF a1 c1 c2) (IF a2 c1 c2)) ent =
   valor_if (IF (IF a a1 a2) c1 c2) ent"
  by (simp only: valor_if.simps(3) if_if)

lemma valor_if_normalAux: 
  "valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
proof (induct e arbitrary: e1 e2)
  fix b e1 e2
  show "valor_if (normalAux (CIF b) e1 e2) ent = 
        valor_if (IF (CIF b) e1 e2) ent"  
    by (simp only: normalAux.simps(1)) 
next
  fix n e1 e2
  show "valor_if (normalAux (VIF n) e1 e2) ent = 
        valor_if (IF (VIF n) e1 e2) ent" 
    by (simp only: normalAux.simps(2)) 
next
  fix a a1 a2 c1 c2
  assume HI:  "⋀e1 e2. valor_if (normalAux a e1 e2) ent = 
                        valor_if (IF a e1 e2) ent" and
         HI1: "⋀e1 e2. valor_if (normalAux a1 e1 e2) ent = 
                        valor_if (IF a1 e1 e2) ent" and
         HI2: "⋀e1 e2. valor_if (normalAux a2 e1 e2) ent = 
                        valor_if (IF a2 e1 e2) ent"
  show "valor_if (normalAux (IF a a1 a2) c1 c2) ent =
        valor_if (IF (IF a a1 a2) c1 c2) ent"
  proof -
    have "valor_if (normalAux (IF a a1 a2) c1 c2) ent =
          valor_if (normalAux a 
                              (normalAux a1 c1 c2) 
                              (normalAux a2 c1 c2)) ent" 
      by (simp only: normalAux.simps(3))
    also have "… = valor_if (IF a 
                                 (normalAux a1 c1 c2) 
                                 (normalAux a2 c1 c2)) ent" 
      by (simp only: HI)
    also have "… = (if valor_if a ent 
                     then valor_if (normalAux a1 c1 c2) ent
                     else valor_if (normalAux a2 c1 c2) ent)" 
      by (simp only: valor_if.simps(3))
    also have "… = (if valor_if a ent
                     then valor_if (IF a1 c1 c2) ent
                     else valor_if (IF a2 c1 c2) ent)" 
      by (simp only: HI1 HI2)
    also have "… = valor_if (IF a (IF a1 c1 c2) (IF a2 c1 c2)) ent"
      by (simp only: valor_if.simps(3))
    also have "… = valor_if (IF (IF a a1 a2) c1 c2) ent" 
      by (simp only: valor_if_IF)    
    finally show ?thesis 
      by this
  qed
qed


subsubsection ‹Demostración aplicativa detallada de valor_if_normalAux›  

lemma valor_if_normalAux_aplicativo:
  "∀e1 e2. valor_if (normalAux e e1 e2) ent = valor_if (IF e e1 e2) ent"
  apply (induct e)
    apply (rule allI)+
    apply (simp only: normalAux.simps(1))
   apply (rule allI)+
   apply (simp only: normalAux.simps(2))
  apply (rule allI)+
  apply (simp only: normalAux.simps(3))
  apply (simp only: valor_if.simps(3))
  apply (case_tac "valor_if e1 ent")
   apply (simp only: if_True)
  apply (simp only: if_False)
  done

subsection ‹Demostraciones del teorema valor_if_normal›

subsubsection ‹Demostración estructurada del teorema valor_if_normal›

theorem valor_if_normal_E:
  "valor_if (normal b) ent = valor_if b ent"
proof (induct b)
  case (CIF x)
  then show ?case by simp
next
  case (VIF x)
  then show ?case by simp
next
  case (IF b1 b2 b3)
  then show ?case by (simp add: valor_if_normalAux)
qed

subsubsection ‹Demostración automática del teorema valor_if_normal›

theorem valor_if_normal_A:
  "valor_if (normal b) ent = valor_if b ent"
  by (induct b) (simp_all add: valor_if_normalAux)

subsubsection ‹Demostración declarativa detallada del teorema valor_if_normal›

theorem valor_if_normal:
  "valor_if (normal b) ent = valor_if b ent"
proof (induct b)
  fix b
  show "valor_if (normal (CIF b)) ent = valor_if (CIF b) ent"
    by (simp only: normal.simps(1) valor_if.simps(1))
next
  fix n
  show "valor_if (normal (VIF n)) ent = valor_if (VIF n) ent" 
    by (simp only: normal.simps(2) valor_if.simps(2))
next
  fix e e1 e2
  assume HI:  "valor_if (normal e) ent = valor_if e ent" and
         HI1: "valor_if (normal e1) ent = valor_if e1 ent" and
         HI2: "valor_if (normal e2) ent = valor_if e2 ent"
  show "valor_if (normal (IF e e1 e2)) ent = 
        valor_if (IF e e1 e2) ent"
  proof -
    have "valor_if (normal (IF e e1 e2)) ent = 
          valor_if (normalAux e (normal e1) (normal e2)) ent" 
      by (simp only: normal.simps(3))
    also have "… = valor_if (IF e (normal e1) (normal e2)) ent" 
      by (simp only: valor_if_normalAux)
    also have "… = (if (valor_if e ent) 
                     then (valor_if (normal e1) ent) 
                     else (valor_if (normal e2) ent))" 
      by (simp only: valor_if.simps(3))
    also have "… = (if (valor_if e ent) 
                     then (valor_if e1 ent) 
                     else (valor_if e2 ent))" 
      by (simp only: HI1 HI2)
    also have "… = valor_if (IF e e1 e2) ent" 
      by (simp only: valor_if.simps(3))
    finally show ?thesis 
      by this
  qed
qed

subsubsection ‹Demostración aplicativa detallada del teorema valor_if_normal›

lemma valor_if_normal_aplicativo:
  "valor_if (normal b) ent = valor_if b ent"
  apply (induct b)
    apply (simp only: normal.simps(1))
   apply (simp only: normal.simps(2))
  apply (simp only: normal.simps(3))
  apply (simp only: valor_if_normalAux_aplicativo)
  apply (simp only: valor_if.simps(3))
  done 

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

subsection ‹Lema auxiliar es_normal_normalAux›

subsubsection ‹Demostración estructurada de es_normal_normalAux›

lemma es_normal_normalAux_E:
  "es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
proof (induct e arbitrary: e1 e2)
  case (CIF x)
  then show ?case by simp
next
  case (VIF x)
  then show ?case by simp
next
  case (IF e1 e2 e3)
  then show ?case by simp
qed 

subsubsection ‹Demostración automática de es_normal_normalAux›

lemma es_normal_normalAux_A:
  "es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
  by (induct e arbitrary: e1 e2) simp_all

subsubsection ‹Demostración declarativa detallada de es_normal_normalAux›

lemma es_normal_normalAux:
  "es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"
proof (induct e arbitrary: e1 e2)
  fix b e1 e2
  have "es_normal (normalAux (CIF b) e1 e2) = 
        es_normal (IF (CIF b) e1 e2)"
    by (simp only: normalAux.simps(1))
  also have "… =  (es_normal e1 ∧ es_normal e2)"
    by (simp only: es_normal.simps(3))
  finally show "es_normal (normalAux (CIF b) e1 e2) =
                (es_normal e1 ∧ es_normal e2)"
    by this 
next
  fix n e1 e2
  have "es_normal (normalAux (VIF n) e1 e2) = 
        es_normal (IF (VIF n) e1 e2)"
    by (simp only: normalAux.simps(2))
  also have "… =  (es_normal e1 ∧ es_normal e2)"
    by (simp only: es_normal.simps(4))
  finally show "es_normal (normalAux (VIF n) e1 e2) =
                (es_normal e1 ∧ es_normal e2)"
    by this 
next
  fix a a1 a2 e1 e2
  assume 
    HI:  "⋀e1 e2. es_normal (normalAux a e1 e2) = 
                  (es_normal e1 ∧ es_normal e2)" and
    HI1: "⋀e1 e2. es_normal (normalAux a1 e1 e2) = 
                  (es_normal e1 ∧ es_normal e2)" and
    HI2: "⋀e1 e2. es_normal (normalAux a2 e1 e2) = 
                  (es_normal e1 ∧ es_normal e2)"
  have "es_normal (normalAux (IF a a1 a2) e1 e2) = 
        es_normal (normalAux a 
                             (normalAux a1 e1 e2)
                             (normalAux a2 e1 e2))" 
    by (simp only: normalAux.simps(3))
  also have "… = (es_normal (normalAux a1 e1 e2) ∧
                   es_normal (normalAux a2 e1 e2))"
    by (simp only: HI)
  also have "… = ((es_normal e1 ∧ es_normal e2) ∧
                   (es_normal e1 ∧ es_normal e2))"
    by (simp only: HI1 HI2)
  also have "… = (es_normal e1 ∧ es_normal e2)"
    by (simp only: conj_absorb)
  finally show "es_normal (normalAux (IF a a1 a2) e1 e2) = 
               (es_normal e1 ∧ es_normal e2)" 
    by this
    qed

subsubsection ‹Demostración aplicativa detallada de es_normal_normalAux›

lemma es_normal_normalAux_aplicativa:
  "es_normal (normalAux e e1 e2) = (es_normal e1 ∧ es_normal e2)"    
  apply (induct e arbitrary: e1 e2)
    apply (simp only: normalAux.simps es_normal.simps)+
  apply (rule iffI)
   apply (erule conjunct2)
  apply (rule conjI)
   apply assumption+
  done

subsection ‹Demostraciones del teorema es_normal_normal›

subsubsection ‹Demostración estructurada del teorema es_normal_normal›

theorem es_normal_normal_E:
  "es_normal (normal b)"
proof (induct b)
  case (CIF x)
  then show ?case by simp
next
  case (VIF x)
  then show ?case by simp
next
  case (IF b1 b2 b3)
  then show ?case by (simp add: es_normal_normalAux)
qed

subsubsection ‹Demostración automática del teorema es_normal_normal›

theorem es_normal_normal_A:
  "es_normal (normal b)"
  by (induct b) (simp_all add: es_normal_normalAux)

subsubsection ‹Demostración declarativa detallada del teorema 
  es_normal_normal›

theorem es_normal_normal:
  "es_normal (normal b)"
proof (induct b)
  fix b
  show "es_normal (normal (CIF b))"
    by (simp only: normal.simps(1) es_normal.simps(1))
next
  fix n
  show "es_normal (normal (VIF n))" 
    by (simp only: normal.simps(2) es_normal.simps(2))
next
  fix e e1 e2
  assume "es_normal (normal e)"
    "es_normal (normal e1)"
    "es_normal (normal e2)"
  then show "es_normal (normal (IF e e1 e2))" 
    by (simp only: normal.simps(3) es_normal_normalAux)
qed

subsubsection ‹Demostración aplicativa detallada del teorema 
  es_normal_normal›

lemma es_normal_normal_aplicativa:
  "es_normal (normal b)"
  apply (induct b)
    apply (simp only: normal.simps(1))
    apply (simp only: es_normal.simps(1))
   apply (simp only: normal.simps(2))
   apply (simp only: es_normal.simps(2))
  apply (simp only: normal.simps)
  apply (simp only: es_normal_normalAux_aplicativa)
  done

section ‹Definición de bool2ifN›

text ‹------------------------------------------------------------------ 
  Ejercicio 10. 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)"

section ‹Lema es_normal_bool2ifN›

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

subsection ‹Demostración automática de es_normal_bool2ifN›

theorem es_normal_bool2ifN_A:
  "es_normal (bool2ifN e)"
   by (simp only: bool2ifN_def es_normal_normal) 

subsection ‹Demostración declarativa detallada de es_normal_bool2ifN›

lemma es_normal_bool2ifN: 
  "es_normal (bool2ifN e)"
proof-
  have "bool2ifN e = normal (bool2if e)" 
    by (simp only: bool2ifN_def)
  then show "es_normal (bool2ifN e)" 
    by (simp only: es_normal_normal) 
qed  

subsection ‹Demostración aplicativa detallada de es_normal_bool2ifN›

lemma es_normal_bool2ifN_aplicativa: 
  "es_normal (bool2ifN e)"  
  apply (simp only: bool2ifN_def)
  apply (simp only: es_normal_normal) 
  done
  
section ‹Lema valor_if_bool2ifN›

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

subsection ‹Demostración automática de valor_if_bool2ifN›

theorem valor_if_bool2ifN_A:
  "valor_if (bool2ifN e) ent = valor e ent"
  by (simp only: bool2ifN_def valor_if_bool2if valor_if_normal)

subsection ‹Demostración declarativa detallada de valor_if_bool2ifN›

lemma valor_if_bool2ifN:
  "valor_if (bool2ifN e) ent = valor e ent"
proof -
  have "bool2ifN e ≡ normal (bool2if e)" 
    by (simp only: bool2ifN_def)
  then have "valor_if (bool2ifN e) ent = 
             valor_if (normal (bool2if e)) ent" 
    by (simp only: )
  also have "… = valor_if (bool2if e) ent" 
    by (simp only: valor_if_normal)
  also have "… = valor e ent" 
    by (simp only: valor_if_bool2if)
  finally show  "valor_if (bool2ifN e) ent = valor e ent" 
    by this
qed

subsection ‹Demostración aplicativa detallada de valor_if_bool2ifN›

lemma valor_if_bool2ifN_aplicativa:
  "valor_if (bool2ifN e) ent = valor e ent"
  apply (simp only: bool2ifN_def)
  apply (simp only: valor_if_normal)
  apply (simp only: valor_if_bool2if)
  done
 
end