Relación 12

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 domlloriv"
-- "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 jaisalmen zoiruicha domlloriv"
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 jaisalmen zoiruicha domlloriv"
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 domlloriv"
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 domlloriv"
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