header {* R12: Representación de fórmulas proposicionales mediante
polinomios *}
theory R12
imports Main
begin
text {*
El objetivo de esta relación es definir un procedimiento para
transformar fórmulas proposicionales (construidas con ⊤, ∧ y ⊕) en
polinomios de la forma
(p₁ ∧ … ∧ pₙ) ⊕ … ⊕ (q₁ ∧ … ∧ qₘ)
y demostrar que, para cualquier interpretación I, el valor de las
fórmulas coincide con la de su correspondiente polinomio. *}
text {*
---------------------------------------------------------------------
Ejercicio 1. Las fórmulas proposicionales pueden definirse mediante
las siguientes reglas:
· ⊤ es una fórmula proposicional
· Las variables proposicionales p_1, p_2, … son fórmulas
proposicionales,
· Si F y G son fórmulas proposicionales, entonces (F ∧ G) y (F ⊕ G)
también lo son.
donde ⊤ es una fórmula que siempre es verdadera, ∧ es la conjunción y
⊕ es la disyunción exclusiva.
Definir el tipo de datos form para representar las fórmulas
proposicionales usando
· T en lugar de ⊤,
· (Var i) en lugar de p_i,
· (And F G) en lugar de (F ∧ G) y
· (Xor F G) en lugar de (F ⊕ G).
------------------------------------------------------------------ *}
datatype form = T | Var nat | And form form | Xor form form
text {*
---------------------------------------------------------------------
Ejercicio 2. Los siguientes ejemplos de fórmulas
form1 = p0 ⊕ ⊤
form2 = (p0 ⊕ p1) ⊕ (p0 ∧ p1)
es usará en lo que sigue.
------------------------------------------------------------------ *}
abbreviation form1 :: "form" where
"form1 ≡ Xor (Var 0) T"
abbreviation form2 :: "form" where
"form2 ≡ Xor (Xor (Var 0) (Var 1)) (And (Var 0) (Var 1))"
text {*
---------------------------------------------------------------------
Ejercicio 3. Definir la función
xor :: bool ⇒ bool ⇒ bool
tal que (xor p q) es el valor de la disyunción exclusiva de p y q. Por
ejemplo,
xor False True = True
------------------------------------------------------------------ *}
definition xor :: "bool ⇒ bool ⇒ bool" where
"xor x y ≡ undefined"
text {*
---------------------------------------------------------------------
Ejercicio 4. Una interpretación es una aplicación de los naturales en
los booleanos. Definir las siguientes interpretaciones
| p0 | p1 | p2 | p3 | ...
int1 | F | F | F | F | ...
int2 | F | V | F | F | ...
int3 | V | F | F | F | ...
int3 | V | V | F | F | ...
------------------------------------------------------------------ *}
abbreviation int1 :: "nat ⇒ bool" where
"int1 x ≡ False"
abbreviation int2 :: "nat ⇒ bool" where
"int2 ≡ int1 (1 := True)"
abbreviation int3 :: "nat ⇒ bool" where
"int3 ≡ int1 (0 := True)"
abbreviation int4 :: "nat ⇒ bool" where
"int4 ≡ int1 (0 := True, 1 := True)"
text {*
---------------------------------------------------------------------
Ejercicio 5. Dada una interpretación I, el valor de de una fórmula F
repecto de I, I(F), se define por
· T, si F es ⊤;
· I(n), si F es p_n;
· I(G) ∧ I(H), si F es (G ∧ H);
· I(G) ⊕ I(H), si F es (G ⊕ H).
Definir la función
valorF :: (nat ⇒ bool) ⇒ form ⇒ bool
tal que (valorF i f) es el valor de la fórmula f respecto de la
interpretación i. Por ejemplo,
valorF int1 form1 = True
valorF int3 form1 = False
valorF int1 form2 = False
valorF int2 form2 = True
valorF int3 form2 = True
valorF int4 form2 = True
--------------------------------------------------------------------- *}
fun valorF :: "(nat ⇒ bool) ⇒ form ⇒ bool" where
"valorF i f = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 6. Un monomio es una lista de números naturales y se puede
interpretar como la conjunción de variables proposionales cuyos
índices son los números de la lista. Por ejemplo, el monomio [0,2,1]
se interpreta como la fórmula (p0 ∧ p2 ∧ p1).
Definir la función
formM :: nat list ⇒ form
tal que (formM m) es la fórmula correspondiente al monomio. Por
ejemplo,
formM [0,2,1] = And (Var 0) (And (Var 2) (And (Var 1) T))
--------------------------------------------------------------------- *}
fun formM :: "nat list ⇒ form" where
"formM ns = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 7. Definir, por recursión, la función
valorM :: (nat ⇒ bool) ⇒ nat list ⇒ bool
tal que (valorM i m) es el valor de la fórmula representada por el
monomio m en la interpretación i. Por ejemplo,
valorM int1 [0,2,1] = False
valorM (int1(0:=True,1:=True,2:=True)) [0,2,1] = True
Demostrar que, para toda interpretación i y todo monomio m, se tiene
que
valorM i m = valorF i (formM m)
--------------------------------------------------------------------- *}
fun valorM :: "(nat ⇒ bool) ⇒ nat list ⇒ bool" where
"valorM i ns = undefined"
lemma correccion_valorM:
"valorM i m = valorF i (formM m)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 8. Un polinomio es una lista de monomios y se puede
interpretar como la disyunción exclusiva de los monomios. Por ejemplo,
el polinomio [[0,2,1],[1,3]] se interpreta como la fórmula
(p0 ∧ p2 ∧ p1) ⊕ (p1 ∧ p3).
Definir la función
formP :: nat list list ⇒ form
tal que (formP p) es la fórmula correspondiente al polinomio p. Por
ejemplo,
formP [[1,2],[3]]
= Xor (And (Var 1) (And (Var 2) T)) (Xor (And (Var 3) T) (Xor T T))
--------------------------------------------------------------------- *}
fun formP :: "nat list list ⇒ form" where
"formP ms = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 9. Definir la función
valorP :: (nat ⇒ bool) ⇒ nat list list ⇒ bool
tal que (valorP i p) es el valor de la fórmula representada por el
polinomio p en la interpretación i. Por ejemplo,
valorP (int1(1:=True,3:=True)) [[0,2,1],[1,3]] = True
Demostrar que, para toda interpretación i y todo polinomio p, se tiene
que
valorM i p = valorF i (formP p)
--------------------------------------------------------------------- *}
fun valorP :: "(nat ⇒ bool) ⇒ nat list list ⇒ bool" where
"valorP i ms = undefined"
lemma correccion_valorP:
"valorP i p = valorF i (formP p)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 10. Definir la función
productoM :: nat list ⇒ nat list list ⇒ nat list list
tal que (productoM m p) es el producto del monomio p por el polinomio
p. Por ejemplo,
productoM [1,3] [[1,2,4],[7],[4,1]]
= [[1,3,1,2,4],[1,3,7],[1,3,4,1]]
--------------------------------------------------------------------- *}
fun productoM :: "nat list ⇒ nat list list ⇒ nat list list" where
"productoM m ns = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 11. Demostrar que, en cualquier interpretación i, el valor
de la concatenación de dos monomios es la conjunción de sus valores.
--------------------------------------------------------------------- *}
lemma valorM_conc:
"valorM i (xs @ ys) = (valorM i xs ∧ valorM i ys)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 12. Demostrar que, en cualquier interpretación i, el valor
del producto de un monomio por un polinomio es la conjunción de sus
valores.
--------------------------------------------------------------------- *}
lemma correccion_productoM:
"valorP i (productoM m p) = (valorM i m ∧ valorP i p)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 13. Definir la función
producto :: nat list list ⇒ nat list list ⇒ nat list list
tal que (producto p q) es el producto de los polinomios p y q. Por
ejemplo,
producto [[1,3],[2]] [[1,2,4],[7],[4,1]]
= [[1,3,1,2,4],[1,3,7],[1,3,4,1],[2,1,2,4],[2,7],[2,4,1]]
--------------------------------------------------------------------- *}
fun producto :: "nat list list ⇒ nat list list ⇒ nat list list" where
"producto p q = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 14. Demostrar que, en cualquier interpretación i, el valor
de la concatenación de dos polinomios es la disyunción exclusiva de
sus valores.
--------------------------------------------------------------------- *}
lemma valorP_conc:
"valorP i (xs @ ys) = (xor (valorP i xs) (valorP i ys))"
oops
text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar que, en cualquier interpretación i, el valor
del producto de dos polinomios es la conjunción de sus valores.
--------------------------------------------------------------------- *}
lemma correccion_producto:
"valorP i (producto p q) = (valorP i p ∧ valorP i q)"
oops
text {*
---------------------------------------------------------------------
Ejercicio 16. Definir la función
polinomio :: form ⇒ nat list list
tal que (polinomio f) es el polinomio que representa la fórmula f. Por
ejemplo,
polinomio (Xor (Var 1) (Var 2)) = [[1],[2]]
polinomio (And (Var 1) (Var 2)) = [[1,2]]
polinomio (Xor (Var 1) T) = [[1],[]]
polinomio (And (Var 1) T) = [[1]]]
polinomio (And (Xor (Var 1) (Var 2)) (Var 3)) = [[1,3],[2,3]]
polinomio (Xor (And (Var 1) (Var 2)) (Var 3)) = [[1,2],[3]]
--------------------------------------------------------------------- *}
fun polinomio :: "form ⇒ nat list list" where
"polinomio f = undefined"
text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar que, en cualquier interpretación i, el valor
de f es igual que el de su polinomio.
--------------------------------------------------------------------- *}
theorem correccion_polinomio:
"valorF i f = valorP i (polinomio f)"
oops
end
