Examen 3

text ‹Examen de Lógica Matemática y Fundamentos (5 julio 2019)›

theory examen_3_05_jul_sol
imports Main 
begin

text ‹Nota: En las demostraciones se pueden las reglas básicas de 
  deducción natural de la lógica proposicional, de los cuantificadores 
  y de la igualdad:  
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · impI:       (P ⟹ Q) ⟹ P ⟶ Q
  · disjI1:     P ⟹ P ∨ Q
  · disjI2:     Q ⟹ P ∨ Q
  · disjE:      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
  · FalseE:     False ⟹ P
  · notE:       ⟦¬P; P⟧ ⟹ R
  · notI:       (P ⟹ False) ⟹ ¬P
  · iffI:       ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:      ⟦Q = P; Q⟧ ⟹ P 
  · iffD2:      ⟦P = Q; Q⟧ ⟹ P
  · ccontr:     (¬P ⟹ False) ⟹ P
  · excluded_middle: (¬P ∨ P) 

  · allE:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  · allI:       (⋀x. P x) ⟹ ∀x. P x
  · exI:        P x ⟹ ∃x. P x
  · exE:        ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

  · refl:       t = t
  · subst:      ⟦s = t; P s⟧ ⟹ P t
  · trans:      ⟦r = s; s = t⟧ ⟹ r = t
  · sym:        s = t ⟹ t = s
  · not_sym:    t ≠ s ⟹ s ≠ t
  · ssubst:     ⟦t = s; P s⟧ ⟹ P t
  · box_equals: ⟦a = b; a = c; b = d⟧ ⟹ c = d
  · arg_cong:   x = y ⟹ f x = f y
  · fun_cong:   f = g ⟹ f x = g x
  · cong:       ⟦f = g; x = y⟧ ⟹ f x = g y

  También se pueden usar las reglas notnotI y mt que demostramos a
  continuación. ›

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

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

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

(* Demostración declarativa. *)
lemma "p ∨ (q ⟶ ¬(p ⟷ q))"
proof - 
  have "¬p ∨ p" by (rule excluded_middle)
  then show "p ∨ (q ⟶ ¬(p ⟷ q))"
  proof
    assume "¬p"
    have "q ⟶ ¬(p ⟷ q)"
    proof
      assume "q"
      show "¬(p ⟷ q)"
      proof
        assume "p ⟷ q"
        then have "p" using `q` by (rule iffD2)
        with `¬p` show False by (rule notE)
      qed
    qed
    then show "p ∨ (q ⟶ ¬(p ⟷ q))" by (rule disjI2)
  next
    assume "p"
    then show "p ∨ (q ⟶ ¬(p ⟷ q))" by (rule disjI1)
  qed
qed

(* Demostración aplicativa. *)
lemma "p ∨ (q ⟶ ¬(p ⟷ q))"
  apply (case_tac "p")
   apply (erule disjI1)
  apply (rule disjI2) 
  apply (rule impI)
  apply (rule notI)
  apply (drule iffD2)
   apply assumption
  apply (erule notE)
  apply assumption
  done

text ‹-----------------------------------------------------------------
  Ejercicio 2. (2.5 puntos) Se puede formalizar la teoría de las tallas
  usando los siguientes símbolos
     P x       representa que x es de la talla pequeña
     M x       representa que x es de la talla mediana
     G x       representa que x es de la talla grande
     Mayor x y representa que la talla de x es mayor que la de y.

  Los axiomas de las tallas son
     ∃x. P x
     ∃x. M x
     ∃x. G x
     ∀x y. G x ∧ M y ⟶ Mayor x y
     ∀x y. M x ∧ P y ⟶ Mayor x y
     ∀x y z . Mayor x y ∧ Mayor y z ⟶ Mayor x z
     ∀x. ¬(Mayor x x)
 
  Demostrar detalladamente que la fórmula
      ∀x. ¬(P x) ∨ ¬(M x)
  es consecuencia de los axiomas de las tallas.

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

(* Demostración declarativa *)
lemma
  assumes "∃x. P x"
          "∃x. M x"
          "∃x. G x"
          "∀x y. G x ∧ M y ⟶ Mayor x y"
          "∀x y. M x ∧ P y ⟶ Mayor x y"
          "∀x y z . Mayor x y ∧ Mayor y z ⟶ Mayor x z"
          "∀x. ¬(Mayor x x)"
  shows "∀x. ¬(P x) ∨ ¬(M x)"
proof
  fix a
  have "¬(P a) ∨ P a" by (rule excluded_middle)
  then show "¬(P a) ∨ ¬(M a)"
  proof
    assume "¬(P a)"
    then show "¬(P a) ∨ ¬(M a)" by (rule disjI1)
  next
    assume "P a"
    have "~(M a)"
    proof
      assume "M a"
      have "~(Mayor a a)" using assms(7) by (rule allE)
      moreover
      have "Mayor a a"
      proof -
        have "∀y. M a ∧ P y ⟶ Mayor a y" using assms(5) by (rule allE)
        then have "M a ∧ P a ⟶ Mayor a a"  by (rule allE)
        moreover
        have "M a ∧ P a" using `M a` `P a` by (rule conjI)
        ultimately show "Mayor a a"  by (rule mp)
      qed  
      ultimately show False by (rule notE) 
    qed
    then show "¬ P a ∨ ¬ M a" by (rule disjI2)
  qed
qed

(* Demostración aplicativa *)
lemma "⟦∃x. P x;
        ∃x. M x;
        ∃x. G x;
        ∀x y. M x ∧ P y ⟶ Mayor x y;
        ∀x y. G x ∧ M y ⟶ Mayor x y;
        ∀x y z . Mayor x y ∧ Mayor y z ⟶ Mayor x z;
        ∀x. ¬(Mayor x x)⟧⟹
                             ∀x. ¬(P x) ∨ ¬(M x)"
  apply (rule allI)
  apply (case_tac "P x")
   prefer 2
   apply (rule disjI1, assumption)
  apply (rule disjI2)
  apply (rule notI)
  apply (erule_tac x = x in allE)
  apply (erule_tac x = x in allE)
  apply (erule_tac x = x in allE)
  apply (erule_tac x = x in allE)
  apply (erule_tac x = x in allE)
  apply (erule notE)
  apply (drule mp)
   apply (rule conjI, 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)".

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

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

    definition nHojasA :: "'a arbol ⇒ nat" where
      "nHojasA a ≡ nHojasAaux a 0"
  tales que
  + (nHojas a) es el número de hojas del árbol a. Por ejemplo, 
       nHojas (N e (N c H H) (N g H H)) = 4
  + (nHojasAA a) es el número de hojas del árbol a, calculado 
    con la función auxiliar nHojasAaux que usa un acumulador. Por 
    ejemplo, 
       nHojasA (N e (N c H H) (N g H H)) = 4
 
  Demostrar estructuradamente (es decir, mediante una demostración 
  declarativa) que las funciones nHojas y nHojasA son equivalentes; 
  es decir,
     nHojasA a = nHojas a

  Notas: 
  1. Los únicos métodos que se pueden usar son induct, (simp only: ...)
     y this.
  2. En las demostraciones por introducción del cuantificador universal
     hay que explicitar el tipo de las variables introducidas con fix.
     Por ejemplo, en lugar de   
          fix x t n
     hay que escribir
          fix x :: 'a and t :: "'a arbol" and and n :: nat
  -------------------------------------------------------------------›

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

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

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

definition nHojasA :: "'a arbol ⇒ nat" where
  "nHojasA a ≡ nHojasAaux a 0"

value "nHojas (N e (N c H H) (N g H H)) = 4"
value "nHojasA (N e (N c H H) (N g H H)) = 4"

lemma nHojasA:
  "nHojasAaux a n = (nHojas a) + n"
proof (induct a arbitrary: n)
  fix n
  have "nHojasAaux H n = n + 1" by (simp only: nHojasAaux.simps(1))
  also have "… = nHojas H + n" by (simp only: nHojas.simps(1))
  finally show "nHojasAaux H n = nHojas H + n" by this
next
  fix x :: 'a and 
      i :: "'a arbol" and
      d :: "'a arbol" and
      n :: nat
  assume HI1: "⋀n. nHojasAaux i n = nHojas i + n"
     and HI2: "⋀n. nHojasAaux d n = nHojas d + n"
  have "nHojasAaux (N x i d) n = nHojasAaux i (nHojasAaux d n)" 
    by (simp only: nHojasAaux.simps(2))
  also have "… = nHojasAaux i (nHojas d + n)" 
    by (simp only: HI2)
  also have "… = nHojas i + (nHojas d + n)" 
    by (simp only: HI1)
  also have "… = nHojas (N x i d) + n" 
    by (simp only: nHojas.simps(2))
  finally show "nHojasAaux (N x i d) n = nHojas (N x i d) + n"  
    by this
qed

(* Demostración aplicativa del lema anterior *)
lemma "nHojasAaux a n = (nHojas a) + n"
  apply (induct a arbitrary: n)
   apply (simp only: nHojasAaux.simps(1))
   apply (simp only: nHojas.simps(1))
  apply (simp only: nHojasAaux.simps(2))
  apply (simp only: nHojas.simps(2))
  done

lemma "nHojasA a = nHojas a"
proof -
  have "nHojasA a = nHojasAaux a 0" by (simp only: nHojasA_def)
  also have "… = (nHojas a)" by (simp only: nHojasA)
  finally show "nHojasA a = nHojas a" by this
qed

text ‹--------------------------------------------------------------- 
  Ejercicio 4. (2.5 puntos) Demostrar detalladamente que los grupos 
  booleanos son conmutativos; es decir, si G un grupo tal que  
     x ⋅ x = 1 
  para todo x de G, entonces
     x ⋅ y = y ⋅ x 
  para todo x, y de G.

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

  Nota: Los únicos métodos que se pueden usar son (simp only: ...) o 
  rule.
  ------------------------------------------------------------------›

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

(* Una demostración declarativa es *)
lemma
  assumes "∀x. x ⋅ x = 𝟭"
  shows   "∀x. ∀y. x ⋅ y = y ⋅ x"
proof (rule allI)+
  fix a b
  show "a ⋅ b = b ⋅ a"
  proof -
    have "(b ⋅ a) ⋅ (b ⋅ a) = 𝟭" by (simp only: assms)
    then have "b ⋅ ((b ⋅ a) ⋅ (b ⋅ a)) = b ⋅ 𝟭" by (rule arg_cong)
    then have "b ⋅ ((b ⋅ a) ⋅ (b ⋅ a)) = b" by (simp only: neutro_d)
    then have "(b ⋅ b) ⋅ (a ⋅ (b ⋅ a)) = b" by (simp only: asociativa)
    then have "𝟭 ⋅ (a ⋅ (b ⋅ a)) = b" by (simp only: assms)
    then have "a ⋅ (b ⋅ a) = b" by (simp only: neutro_i)
    then have "(a ⋅ (b ⋅ a)) ⋅ a = b ⋅ a" by (rule arg_cong)
    then have "(a ⋅ b) ⋅ (a ⋅ a) = b ⋅ a" by (simp only: asociativa)
    then have "(a ⋅ b) ⋅ 𝟭 = b ⋅ a" by (simp only: assms)
    then show "a ⋅ b = b ⋅ a" by (simp only: neutro_d)
  qed 
qed

end

end