Diferencia entre revisiones de «Relación 12»
De Razonamiento automático (2013-14)
Línea 59: | Línea 59: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | --"diecabmen1 irealetei pabflomar jaisalmen zoiruicha maresccas4" | + | --"diecabmen1 irealetei pabflomar jaisalmen zoiruicha maresccas4 marescpla" |
-- "jaisalmen: http://es.wikipedia.org/wiki/Disyunci%C3%B3n_exclusiva" | -- "jaisalmen: http://es.wikipedia.org/wiki/Disyunci%C3%B3n_exclusiva" | ||
-- "jaisalmen: de la definicion de xor: p xor q = ( p∧¬ q) or (¬ p ∧ q)" | -- "jaisalmen: de la definicion de xor: p xor q = ( p∧¬ q) or (¬ p ∧ q)" | ||
Línea 106: | Línea 106: | ||
--------------------------------------------------------------------- *} | --------------------------------------------------------------------- *} | ||
− | --"diecabmen1 irealetei maresccas4" | + | --"diecabmen1 irealetei maresccas4 marescpla" |
fun valorF :: "(nat ⇒ bool) ⇒ form ⇒ bool" where | fun valorF :: "(nat ⇒ bool) ⇒ form ⇒ bool" where | ||
"valorF i T = True" | "valorF i T = True" | ||
Línea 127: | Línea 127: | ||
--------------------------------------------------------------------- *} | --------------------------------------------------------------------- *} | ||
− | --"diecabmen1 irealetei maresccas4" | + | --"diecabmen1 irealetei maresccas4 marescpla" |
fun formM :: "nat list ⇒ form" where | fun formM :: "nat list ⇒ form" where | ||
"formM [] = T" | "formM [] = T" | ||
Línea 147: | Línea 147: | ||
--------------------------------------------------------------------- *} | --------------------------------------------------------------------- *} | ||
− | --"diecabmen1 irealetei maresccas4" | + | --"diecabmen1 irealetei maresccas4 marescpla" |
fun valorM :: "(nat ⇒ bool) ⇒ nat list ⇒ bool" where | fun valorM :: "(nat ⇒ bool) ⇒ nat list ⇒ bool" where | ||
"valorM i [] = True" | "valorM i [] = True" | ||
Línea 171: | Línea 171: | ||
qed | qed | ||
− | --"irealetei maresccas4" | + | --"irealetei maresccas4 marescpla" |
lemma correccion_valorM_detalle: | lemma correccion_valorM_detalle: | ||
"valorM i m = valorF i (formM m)" | "valorM i m = valorF i (formM m)" | ||
Línea 200: | Línea 200: | ||
--------------------------------------------------------------------- *} | --------------------------------------------------------------------- *} | ||
− | --"diecabmen1 irealetei maresccas4" | + | --"diecabmen1 irealetei maresccas4 marescpla" |
fun formP :: "nat list list ⇒ form" where | fun formP :: "nat list list ⇒ form" where | ||
"formP [] = Xor T T" | "formP [] = Xor T T" |
Revisión del 00:26 10 mar 2014
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
------------------------------------------------------------------ *}
--"diecabmen1 irealetei pabflomar jaisalmen zoiruicha maresccas4 marescpla"
-- "jaisalmen: http://es.wikipedia.org/wiki/Disyunci%C3%B3n_exclusiva"
-- "jaisalmen: de la definicion de xor: p xor q = ( p∧¬ q) or (¬ p ∧ q)"
definition xor :: "bool ⇒ bool ⇒ bool" where
"xor x y ≡ (x∧¬y)∨(¬x∧y)"
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
--------------------------------------------------------------------- *}
--"diecabmen1 irealetei maresccas4 marescpla"
fun valorF :: "(nat ⇒ bool) ⇒ form ⇒ bool" where
"valorF i T = True"
| "valorF i (Var n) = i n"
| "valorF i (And G H) = ((valorF i G) ∧ (valorF i H))"
| "valorF i (Xor G H) = xor (valorF i G) (valorF i H)"
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))
--------------------------------------------------------------------- *}
--"diecabmen1 irealetei maresccas4 marescpla"
fun formM :: "nat list ⇒ form" where
"formM [] = T"
| "formM (x#xs) = And (Var x) (formM xs)"
value "formM [0,2,1]"
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)
--------------------------------------------------------------------- *}
--"diecabmen1 irealetei maresccas4 marescpla"
fun valorM :: "(nat ⇒ bool) ⇒ nat list ⇒ bool" where
"valorM i [] = True"
| "valorM i (x#xs) = ((valorF i (Var x)) ∧ (valorM i xs))" --"Aquí he quitado algún paréntesis, pero la solución es, en esencia, la misma."
value "valorM int1 [0,2,1]"
value "valorM (int1(0:=True,1:=True,2:=True)) [0,2,1]"
--"diecabmen1 irealetei"
lemma correccion_valorM:
"valorM i m = valorF i (formM m)"
by (induct m) auto
--"diecabmen1"
lemma correccion_valorM2:
"valorM i m = valorF i (formM m)" (is "?P i m")
proof (induct m)
show "?P i []" by simp
next
fix a m
assume HI: "?P i m"
then show "?P i (a#m)" by simp
qed
--"irealetei maresccas4 marescpla"
lemma correccion_valorM_detalle:
"valorM i m = valorF i (formM m)"
proof (induct m)
show "valorM i [] = valorF i (formM [])" by simp
next
fix a m
assume HI:"valorM i m = valorF i (formM m)"
have "valorM i (a # m) = (valorF i (Var a) ∧ valorM i m)" by simp
also have "... = (valorF i (Var a) ∧ valorF i (formM m))" using HI by simp
also have "... = valorF i (formM (a # m))" by simp
finally show "valorM i (a # m) = valorF i (formM (a # m))" by simp
qed
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))
--------------------------------------------------------------------- *}
--"diecabmen1 irealetei maresccas4 marescpla"
fun formP :: "nat list list ⇒ form" where
"formP [] = Xor T T"
| "formP (x#xs) = Xor (formM x) (formP xs)"
value "formP [[1,2],[3]]"
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)
--------------------------------------------------------------------- *}
--"diecabmen1 irealetei"
fun valorP :: "(nat ⇒ bool) ⇒ nat list list ⇒ bool" where
"valorP i [] = xor True True"
| "valorP i (x#xs) = xor (valorM i x) (valorP i xs)"
value "valorP (int1(1:=True,3:=True)) [[0,2,1],[1,3]]"
lemma correccion_valorP:
"valorP i p = valorF i (formP p)"
by (induct p) (auto simp add:correccion_valorM)
-- "irealetei"
lemma correccion_valorP_detalle:
"valorP i p = valorF i (formP p)"
proof (induct p)
show "valorP i [] = valorF i (formP [])" by simp
next
fix a p
assume HI:"valorP i p = valorF i (formP p)"
have "valorP i (a # p) = xor (valorM i a) (valorP i p)" by simp
also have "... = xor (valorF i (formM a)) (valorP i p) " by (simp add:correccion_valorM)
also have "... = xor (valorF i (formM a)) (valorF i (formP p))" using HI by simp
also have "... = valorF i (formP (a # p))" by simp
finally show " valorP i (a # p) = valorF i (formP (a # p))" by simp
qed
-- "maresccas4"
fun valorP4 :: "(nat ⇒ bool) ⇒ nat list list ⇒ bool" where
"valorP4 i [] = False"
| "valorP4 i (x#xs) = xor (valorM i x) (valorP4 i xs)"
value "valorP4 (int1(1:=True,3:=True)) [[0,2,1],[1,3]]"
lemma correccion_valorP4:
"valorP4 i p = valorF i (formP p)"
proof (induct p)
show "valorP4 i [] = valorF i (formP [])" by (simp add:xor_def)
next
fix x xs
assume HI: "valorP4 i xs = valorF i (formP xs)"
have "valorP4 i (x#xs) = xor (valorM i x) (valorP4 i xs)" by simp
also have "... = xor (valorM i x) (valorF i (formP xs))" using HI by simp
also have "... = valorF i (Xor (formM x) (formP xs))" by (simp add: correccion_valorM)
also have "... = valorF i (formP (x#xs))" by simp
finally show "valorP4 i (x#xs) = valorF i (formP (x#xs))" by simp
qed
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]]
--------------------------------------------------------------------- *}
--"diecabmen1"
fun productoM :: "nat list ⇒ nat list list ⇒ nat list list" where
"productoM m [] = []"
| "productoM m (x#xs) = [m@x] @ (productoM m xs)"
--"irealetei maresccas4"
fun productoM2 :: "nat list ⇒ nat list list ⇒ nat list list" where
"productoM2 m [] = []"
| "productoM2 m (a#ns) = (m@a)#(productoM2 m ns)"
value "productoM [1,3] [[1,2,4],[7],[4,1]]"
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.
--------------------------------------------------------------------- *}
--"diecabmen1"
lemma valorM_conc:
"valorM i (xs @ ys) = (valorM i xs ∧ valorM i ys)" (is "?P i xs ys")
proof (induct xs)
show "?P i [] ys" by simp
next
fix a xs
assume HI: "?P i xs ys"
then show "?P i (a#xs) ys" by simp
qed
--"irealetei maresccas4"
lemma valorM_conc_auto:
"valorM i (xs @ ys) = (valorM i xs ∧ valorM i ys)"
by (induct xs) auto
lemma valorM_conc_detalle:
"valorM i (xs @ ys) = (valorM i xs ∧ valorM i ys)"
proof (induct xs)
show "valorM i ([] @ ys) = (valorM i [] ∧ valorM i ys)" by simp
next
fix a xs
assume HI:"valorM i (xs @ ys) = (valorM i xs ∧ valorM i ys)"
have "valorM i ((a # xs) @ ys) = (valorF i (Var a) ∧ valorM i (xs @ ys))" by simp
also have "... = (valorF i (Var a) ∧ (valorM i xs ∧ valorM i ys))" using HI by simp
also have "... = (valorM i (a # xs) ∧ valorM i ys)" by simp
finally show "valorM i ((a # xs) @ ys) = (valorM i (a # xs) ∧ valorM i ys)" by simp
qed
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.
--------------------------------------------------------------------- *}
--"irealetei"
lemma xor_compl: "xor (a ∧ p) (a ∧ q) = (a ∧ (xor p q))"
proof -
have "xor (a ∧ p) (a ∧ q) = (((a ∧ p) ∧ ¬(a ∧ q)) ∨ (¬(a ∧ p) ∧ (a ∧ q)))" by (simp add:xor_def)
also have "... = (a ∧ ((p ∧ ¬q) ∨ (¬p ∧ q)))" by auto
also have "... = (a ∧ (xor p q))" by (simp add:xor_def)
finally show "xor (a ∧ p) (a ∧ q) = (a ∧ (xor p q))" by simp
qed
-- "No me hacía falta definir el xor_neg, anterior, que es como matar moscas a cañonazos"
lemma correccion_productoM:
"valorP i (productoM m p) = (valorM i m ∧ valorP i p)"
proof (induct p)
have "valorP i (productoM m []) = valorP i []" by simp
also have "... = (valorM i m ∧ valorP i [])" by (simp add:xor_def)
then show "valorP i (productoM m []) = (valorM i m ∧ valorP i [])" by simp
next
fix a p
assume HI:"valorP i (productoM m p) = (valorM i m ∧ valorP i p)"
have "valorP i (productoM m (a # p)) = valorP i ((m@a)#(productoM m p))" by simp
also have "... = xor (valorM i (m@a)) (valorP i (productoM m p))" by simp
also have "... = xor (valorM i (m@a)) (valorM i m ∧ valorP i p)" using HI by simp
also have "... = xor (valorM i m ∧ valorM i a) (valorM i m ∧ valorP i p)" by (simp add:valorM_conc)
also have "... = (valorM i m ∧ xor (valorM i a) (valorP i p))" by (simp add:xor_compl)
also have "... = (valorM i m ∧ valorP i (a # p))" by simp
finally show "valorP i (productoM m (a # p)) = (valorM i m ∧ valorP i (a # p))" by simp
qed
lemma correccion_productoM_auto:
"valorP i (productoM m p) = (valorM i m ∧ valorP i p)"
by (induct p) (auto simp add:xor_def valorM_conc xor_compl)
-- "maresccas4"
lemma lema1: "xor (a ∧ b) (a ∧ c) = (a ∧ (xor b c))"
proof (cases a)
assume H: "a"
then show "xor (a ∧ b) (a ∧ c) = (a ∧ (xor b c))" by simp
next
assume H: "¬a"
then show "xor (a ∧ b) (a ∧ c) = (a ∧ (xor b c))" by (simp add: xor_def)
qed
lemma correccion_productoM:
"valorP4 i (productoM m p) = (valorM i m ∧ valorP4 i p)"
proof (induct p)
show "valorP4 i (productoM m []) = (valorM i m ∧ valorP4 i [])" by simp
next
fix p px
assume HI: "valorP4 i (productoM m px) = (valorM i m ∧ valorP4 i px)"
have "valorP4 i (productoM m (p#px)) = valorP4 i ((m@p) # productoM m px)" by simp
also have "... = xor (valorF i (formM (m@p))) (valorP4 i (productoM m px))" by (simp add: correccion_valorM)
also have "... = xor (valorF i (formM (m@p))) (valorM i m ∧ valorP4 i px)" using HI by simp
also have "... = xor (valorM i (m @ p)) (valorM i m ∧ valorP4 i px)" by (simp add: correccion_valorM)
also have "... = xor (valorM i m ∧ valorM i p) (valorM i m ∧ valorP4 i px)" by (simp add: valorM_conc)
also have "... = (valorM i m ∧ (xor (valorM i p) (valorP4 i px)))" by (simp add: lema1)
also have "... = (valorM i m ∧ valorP4 i (p#px))" by simp
finally show "valorP4 i (productoM m (p#px)) = (valorM i m ∧ valorP4 i (p#px))" by simp
qed
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]]
--------------------------------------------------------------------- *}
--"irealetei: tenía una de más que no valía para nada, se me queda igual que maresccas4"
fun producto :: "nat list list ⇒ nat list list ⇒ nat list list" where
"producto [] q = []"
| "producto (a1 # p) (q) = (productoM a1 q)@(producto p q)"
value "producto [[1,3],[2]] [[1,2,4],[7],[4,1]]"
-- "maresccas4"
fun producto4 :: "nat list list ⇒ nat list list ⇒ nat list list" where
"producto [] q = []"
| "producto (m#p) q = (productoM m q) @ (producto p q)"
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.
--------------------------------------------------------------------- *}
-- "maresccas4 irealetei"
-- "Si me da tiempo, intentaré probar este lema. Irealetei: lo estoy intentando pero me he quedado en: '((a ∧ (¬b ∨ c) ∧ (b∨¬c)) ∨ (¬a ∧ ((b∧¬c) ∨ (¬b∧c ))))' y me va a petar el cerebro..."
lemma lema2: "xor a (xor b c) = xor (xor a b) c"
by (auto simp add: xor_def)
-- "Me ha dado tiempo. De forma análoga al lema1"
lemma lema2_simp: "xor a (xor b c) = xor (xor a b) c"
proof (cases a)
assume "a"
show "xor a (xor b c) = xor (xor a b) c"
proof (cases b)
assume "b"
then show "xor a (xor b c) = xor (xor a b) c" using `a` by (simp add: xor_def)
next
assume "¬b"
then show "xor a (xor b c) = xor (xor a b) c" by (simp add: xor_def)
qed
next
assume "¬a"
show "xor a (xor b c) = xor (xor a b) c"
proof (cases b)
assume "b"
then show "xor a (xor b c) = xor (xor a b) c" using `¬a`by (simp add: xor_def)
next
assume "¬b"
then show "xor a (xor b c) = xor (xor a b) c" by (simp add: xor_def)
qed
qed
lemma valorP_conc:
"valorP4 i (xs @ ys) = (xor (valorP4 i xs) (valorP4 i ys))"
proof (induct xs)
show "valorP4 i ([] @ ys) = (xor (valorP4 i []) (valorP4 i ys))" by (simp add: xor_def)
next
fix x xs
assume HI: "valorP4 i (xs @ ys) = (xor (valorP4 i xs) (valorP4 i ys))"
have "valorP4 i ((x#xs) @ ys) = valorP4 i (x # (xs@ys))" by simp
also have "... = xor (valorM i x) (valorP4 i (xs@ys))" by simp
also have "... = xor (valorM i x) (xor (valorP4 i xs) (valorP4 i ys))" using HI by simp
also have "... = xor (xor (valorM i x) (valorP4 i xs)) (valorP4 i ys)" by (simp add: lema2)
also have "... = xor (valorP4 i (x#xs)) (valorP4 i ys)" by simp
finally show "valorP4 i ((x#xs) @ ys) = (xor (valorP4 i (x#xs)) (valorP4 i ys))" by simp
qed
text {*
---------------------------------------------------------------------
Ejercicio 15. Demostrar que, en cualquier interpretación i, el valor
del producto de dos polinomios es la conjunción de sus valores.
--------------------------------------------------------------------- *}
-- "maresccas4 irealetei"
-- "Es fácil ver que este lema es análogo al demostrado lema1"
lemma lema3: "xor (a ∧ c) (b ∧ c) = ((xor a b) ∧ c)"
by (auto simp add: xor_def)
lemma correccion_producto:
"valorP4 i (producto4 p q) = (valorP4 i p ∧ valorP4 i q)"
proof (induct p)
show "valorP4 i (producto4 [] q) = (valorP4 i [] ∧ valorP4 i q)" by simp
next
fix m p
assume HI: "valorP4 i (producto4 p q) = (valorP4 i p ∧ valorP4 i q)"
have "valorP4 i (producto4 (m#p) q) = valorP4 i ((productoM m q) @ (producto4 p q))" by simp
also have "... = (xor (valorP4 i (productoM m q)) (valorP4 i (producto4 p q)))" by (simp add: valorP_conc)
also have "... = (xor (valorP4 i (productoM m q)) (valorP4 i p ∧ valorP4 i q))" using HI by simp
also have "... = (xor (valorM i m ∧ valorP4 i q) (valorP4 i p ∧ valorP4 i q))" by (simp add: correccion_productoM)
also have "... = ((xor (valorM i m) (valorP4 i p)) ∧ valorP4 i q)" by (simp add: lema3)
also have "... = (valorP4 i (m#p) ∧ valorP4 i q)" by simp
finally show "valorP4 i (producto4 (m#p) q) = (valorP4 i (m#p) ∧ valorP4 i q)" by simp
qed
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]]
--------------------------------------------------------------------- *}
-- "maresccas4 irealetei"
fun polinomio :: "form ⇒ nat list list" where
"polinomio T = [[]]"
| "polinomio (Var a) = [[a]]"
| "polinomio (And G H) = producto4 (polinomio G) (polinomio H)"
| "polinomio (Xor G H) = (polinomio G) @ (polinomio H)"
value "polinomio (Xor (Var 1) (Var 2))"
value "polinomio (And (Var 1) (Var 2))"
value "polinomio (Xor (Var 1) T)"
value "polinomio (And (Var 1) T)"
value "polinomio (And (Xor (Var 1) (Var 2)) (Var 3))"
value "polinomio (Xor (And (Var 1) (Var 2)) (Var 3))"
text {*
---------------------------------------------------------------------
Ejercicio 17. Demostrar que, en cualquier interpretación i, el valor
de f es igual que el de su polinomio.
--------------------------------------------------------------------- *}
-- "maresccas4 irealetei"
theorem correccion_polinomio:
"valorF i f = valorP4 i (polinomio f)"
proof (induct f)
show "valorF i T = valorP4 i (polinomio T)" by (simp add: xor_def)
next
fix a
show "valorF i (Var a) = valorP4 i (polinomio (Var a))" by (simp add: xor_def)
next
fix G H
assume H1: "valorF i G = valorP4 i (polinomio G)"
assume H2: "valorF i H = valorP4 i (polinomio H)"
have "valorF i (And G H) = (valorF i G ∧ valorF i H)" by simp
also have "... = ((valorP4 i (polinomio G)) ∧ (valorP4 i (polinomio H)))" using H1 H2 by simp
also have "... = valorP4 i (producto4 (polinomio G) (polinomio H))" by (simp add: correccion_producto)
also have "... = valorP4 i (polinomio (And G H))" by simp
finally show "valorF i (And G H) = valorP4 i (polinomio (And G H))" by simp
next
fix G H
assume H1: "valorF i G = valorP4 i (polinomio G)"
assume H2: "valorF i H = valorP4 i (polinomio H)"
have "valorF i (Xor G H) = xor (valorF i G) (valorF i H)" by simp
also have "... = xor (valorP4 i (polinomio G)) (valorP4 i (polinomio H))" using H1 H2 by simp
also have "... = valorP4 i ((polinomio G) @ (polinomio H))" by (simp add: valorP_conc)
also have "... = valorP4 i (polinomio (Xor G H))" by simp
finally show "valorF i (Xor G H) = valorP4 i (polinomio (Xor G H))" by simp
qed
end