Acciones

Examen 2

De Lógica matemática y fundamentos (2018-19)

Revisión del 17:20 12 jun 2019 de Jalonso (discusión | contribuciones)
(dif) ← Revisión anterior | Revisión actual (dif) | Revisión siguiente → (dif)
chapter {* Examen de Lógica Matemática y Fundamentos (6-junio-2919) *}

theory examen_2_06_jun_sol
imports Main 
begin

text {* --------------------------------------------------------------- 
  Ejercicio 1. (2.5 puntos) Demostrar detalladamente que la siguiente
  fórmula es una tautología: 
     (p ⟶ q) ⟶((¬p ⟶ q) ⟶ q)

  Nota: No usar ninguno de los métodos automáticos: simp, simp_all, 
  auto, blast, force, fast, arith o metis
  ------------------------------------------------------------------ *}

lemma ej1: 
  shows "(p ⟶ q) ⟶ ((¬p ⟶ q) ⟶ q)"  
proof
  assume "p ⟶ q"
  show "(¬p ⟶ q) ⟶ q"
  proof 
    assume "¬p ⟶ q"
    have "¬p ∨ p" by (rule excluded_middle)
    then show "q"
    proof (rule disjE)
      assume "¬p"
      with `¬p ⟶ q` show q by (rule mp)
    next
      assume "p"
      with `p ⟶ q` show q by (rule mp)
    qed
  qed 
qed

text {* --------------------------------------------------------------- 
  Ejercicio 2. (2.5 puntos) Demostrar detalladamente que si R es una
  relación irreflexiva y transitiva, entonces R es antisimétrica. 
  { ∀x. ¬R(x,x), 
    ∀x. ∀y. ∀z. (R(x,y) ∧ R(y,z) ⟶ R(x,z)) } 
  ⊢  ∀x. ∀y. (R(x,y) ⟶ ¬R(y,x))

  Nota: No usar ninguno de los métodos automáticos: simp, simp_all, 
  auto, blast, force, fast, arith o metis
  ------------------------------------------------------------------ *}

(* La demostración declarativa es *)
lemma
  assumes "∀x. ¬R(x,x)"
          "∀x. ∀y. ∀z. (R(x,y) ∧ R(y,z) ⟶ R(x,z))" 
  shows   "∀x. ∀y. (R(x,y) ⟶ ¬ R(y,x))"
proof 
  fix a
  show "∀y. (R(a,y) ⟶ ¬R(y,a))"
  proof
   fix b
   show "R(a,b) ⟶ ¬R(b,a)"
   proof
     assume "R(a,b)"
     show "¬ R(b,a)"
     proof
       assume "R(b,a)"
       then have "R(b,a) ∧ R(a,b)" using `R(a,b)` by (rule conjI)
       have "∀y. ∀z.(R(b,y) ∧ R(y,z) ⟶ R(b,z))" 
         using assms(2) by (rule allE)
       then have "∀z.(R(b,a) ∧ R(a,z) ⟶ R(b,z))" by (rule allE)
       then have "R(b,a) ∧ R(a,b) ⟶ R(b,b)" by (rule allE)
       then have "R(b,b)" using `R(b,a) ∧ R(a,b)` by (rule mp)
       have "¬R(b,b)" using assms(1) by (rule allE)
       then show False using `R(b,b)` by (rule notE)
     qed
   qed
 qed
qed

(* La demostración aplicativa es *)
lemma 
  "⟦ ∀x. ¬R(x,x);
     ∀x. ∀y. ∀z. (R(x,y) ∧ R(y,z) ⟶ R(x,z))⟧
   ⟹ ∀x. ∀y. (R(x,y) ⟶ ¬ R(y,x))"   
  apply (rule allI)+
      (* ⋀x y. ⟦ ∀x. ¬ R (x, x);
                 ∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z)⟧
               ⟹ R (x, y) ⟶ ¬ R (y, x)*)
  apply (rule impI)
      (* ⋀x y. ⟦ ∀x. ¬ R (x, x);
                 ∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z);
                 R (x, y)⟧
               ⟹ ¬ R (y, x) *)
    apply (rule notI)
      (* ⋀x y. ⟦ ∀x. ¬ R (x, x);
                 ∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z);
                 R (x, y); 
                 R (y, x)⟧
               ⟹ False *)
  apply (erule_tac x=x in allE)
      (* ⋀x y. ⟦ ∀x y z. R (x, y) ∧ R (y, z) ⟶ R (x, z);
                 R (x, y); 
                 R (y, x); 
                 ¬ R (x, x)⟧
           ⟹ False *)
  apply (erule_tac x=x in allE)
      (* ⋀x y. ⟦ R (x, y); 
                 R (y, x); 
                 ¬ R (x, x);
                 ∀y z. R (x, y) ∧ R (y, z) ⟶ R (x, z)⟧
               ⟹ False *)
  apply (erule_tac x=y in allE)
      (* ⋀x y. ⟦ R (x, y); 
                 R (y, x); 
                 ¬ R (x, x);
                 ∀z. R (x, y) ∧ R (y, z) ⟶ R (x, z)⟧
               ⟹ False *)
  apply (erule_tac x=x in allE)
      (* ⋀x y. ⟦ R (x, y); 
                 R (y, x); 
                 ¬ R (x, x);
                 R (x, y) ∧ R (y, x) ⟶ R (x, x)⟧
               ⟹ False *)
  apply (erule notE)
      (* ⋀x y. ⟦ R (x, y); 
                 R (y, x);
                 R (x, y) ∧ R (y, x) ⟶ R (x, x)⟧
               ⟹ R (x, x) *)
  apply (drule mp)
      (* 1. ⋀x y. ⟦R (x, y); R (y, x)⟧ ⟹ R (x, y) ∧ R (y, x)
         2. ⋀x y. ⟦R (x, y); R (y, x); R (x, x)⟧ ⟹ R (x, x) *)
    apply (rule conjI)
      (* 1. ⋀x y. ⟦R (x, y); R (y, x)⟧ ⟹ R (x, y)
         2. ⋀x y. ⟦R (x, y); R (y, x)⟧ ⟹ R (y, x)
         3. ⋀x y. ⟦R (x, y); R (y, x); R (x, x)⟧ ⟹ R (x, x)*)
    apply assumption+
      (* *)
  done  

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 3 (2.5 puntos) Consideremos el árbol binario definido por
     datatype 'a arbol = H  | N "'a" "'a arbol" "'a arbol"
  
  Por ejemplo, el árbol
          e
         / \
        /   \
       c     g
      / \   / \
             
  se representa por "N e (N c H H) (N g H H)".

  Definir las funciones 
     nNodos :: "'a arbol ⇒ nat"
     nHojas :: "'a arbol ⇒ nat" 
  tales que 
  + (nNodos a) es el número de nodos de a. Por ejemplo,
       nNodos (N e (N c H H) (N g H H)) = 3
  + (nHojas a) es el número de hojas de a. Por ejemplo,
       nHojas (N e (N c H H) (N g H H)) = 4

  Demostrar detalladamente que el número de hojas de un árbol es igual 
  al número de nodos más 1.

  Nota: Los únicos métodos que se pueden usar son induct, 
  (simp only: ...) o this.
  ------------------------------------------------------------------- *}

datatype 'a arbol = H  | N "'a" "'a arbol" "'a arbol"

fun nNodos :: "'a arbol ⇒ nat" where
  "nNodos H         = 0"
| "nNodos (N x i d) = 1 + (nNodos i) + (nNodos d)"

fun nHojas :: "'a arbol ⇒ nat" where
  "nHojas H         = 1"
| "nHojas (N x i d) = (nHojas i) + (nHojas d)"

(* Demostración declarativa *)
lemma ej3: 
  "nHojas a = (nNodos a) + 1" (is "?P a")
proof (induct a)
  show "?P H" by (simp only: nHojas.simps(1) nNodos.simps(1)) 
next
  fix x i d
  assume HI1: "?P i"
  assume HI2: "?P d"
  show "?P (N x i d)" 
  proof -
    have "nHojas (N x i d) = (nHojas i) + (nHojas d)" 
      by (simp only: nHojas.simps(2))
    also have "... = (nNodos i + 1) + (nNodos d + 1)" 
      by (simp only: HI1 HI2)
    also have "... = (nNodos (N x i d)) + 1" 
      by (simp only: nNodos.simps(2))
    finally show "?P (N x i d)" by this
  qed
qed

(* Demostración aplicativa *)
lemma ej3_b: 
  "nHojas a = (nNodos a) + 1"  
  apply (induct a)
     (* 1. nHojas H = nNodos H + 1
        2. ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1; 
                        nHojas a2 = nNodos a2 + 1⟧
                      ⟹ nHojas (N x1 a1 a2) = 
                          nNodos (N x1 a1 a2) + 1 *)
   apply (simp only: nHojas.simps(1)) 
     (* 1. 1 = nNodos H + 1
        2. ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1; 
                        nHojas a2 = nNodos a2 + 1⟧
                      ⟹ nHojas (N x1 a1 a2) = nNodos (N x1 a1 a2) + 1 *)
  apply (simp only: nNodos.simps(1))
     (* ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1; 
                     nHojas a2 = nNodos a2 + 1⟧
                   ⟹ nHojas (N x1 a1 a2) = 
                       nNodos (N x1 a1 a2) + 1 *)
  apply (simp only: nHojas.simps(2))
     (* ⋀x1 a1 a2. ⟦ nHojas a1 = nNodos a1 + 1;
                     nHojas a2 = nNodos a2 + 1⟧
                   ⟹ nNodos a1 + 1 + (nNodos a2 + 1) = 
                       nNodos (N x1 a1 a2) + 1 *)
  apply (simp only: nNodos.simps(2))
     (* *)
  done

text {* --------------------------------------------------------------- 
  Ejercicio 4. (2.5 puntos) Sea G un grupo. Domostrar detalladamente que 
  para todo par de elementos x e y de G, si x es el inverso de y, 
  entonces y es el inverso de x.

  Nota: No usar ninguno de los métodos automáticos: auto, blast, force,
  fast, arith o metis 
  ------------------------------------------------------------------ *}

locale grupo =
  fixes prod :: "['a, 'a] ⇒ 'a" (infixl "⋅" 70)
    and neutro ("𝟭") 
    and inverso ("_^" [100] 100)
  assumes asociativa: "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"
      and neutro_i:   "𝟭 ⋅ x = x"
      and neutro_d:   "x ⋅ 𝟭 = x"
      and inverso_i:  "x^ ⋅ x = 𝟭"

(* Notas sobre notación:
   * El producto es ⋅ y se escribe con \ cdot (sin espacio entre ellos). 
   * El neutro es 𝟭 y se escribe con \ y one (sin espacio entre ellos).
   * El inverso de x es x^ y se escribe pulsando 2 veces en ^. *)

context grupo
begin

lemma ej5:
  shows "∀x. ∀y. x = y^ ⟶ y = x^" 
proof (rule allI)+
  fix a b
  show "a = b^ ⟶ b = a^"
  proof 
    assume "a = b^"
    then have "a^ ⋅ a = a^ ⋅ b^" by simp
    then have "𝟭 = a^ ⋅ b^" by (simp only: inverso_i)
    then have "𝟭 ⋅ b = (a^ ⋅ b^) ⋅ b" by simp
    then have "b = (a^ ⋅ b^) ⋅ b" by (simp only: neutro_i)
    then have "b = a^ ⋅ (b^ ⋅ b)" by (simp only: asociativa)
    then have "b = a^ ⋅ 𝟭" by (simp only: inverso_i)
    then show "b = a^ " by (simp only: neutro_d)
  qed
qed

end

end