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

2020-06-18T06:53:16Z

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

Mjoseh: Página creada con « chapter ‹Expresiones booleanas y expresiones condicionales› theory Trabajo_final_sol imports Main begin section ‹Expresiones booleanas…»

2020-06-18T06:53:06Z

Página creada con «<source lang = "isabelle"> chapter ‹Expresiones booleanas y expresiones condicionales› theory Trabajo_final_sol imports Main begin section ‹Expresiones booleanas…»

Página nueva

<source lang = "isabelle">
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

</source>

TF sol - Historial de revisiones

Mjoseh en 07:13 18 jun 2020

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

Mjoseh: Página creada con « chapter ‹Expresiones booleanas y expresiones condicionales› theory Trabajo_final_sol imports Main begin section ‹Expresiones booleanas…»

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