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"
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"
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"
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"
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"
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"
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

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"
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"
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_neg: "xor True True = False"
proof -
  have "xor True True = (True ∧ ¬True) ∨ (¬True ∧ True)" by (simp add:xor_def)
  also have "... = False" by simp
  finally show "xor True True = False" by simp
qed

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

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_neg)
  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_neg valorM_conc xor_compl)

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