Acciones

Diferencia entre revisiones de «RA12 Relación 1»

De DAO (Demostración asistida por ordenador)

(Página creada con '<source lang="isar"> header {* Relación 1: Programación funcional en Isabelle *} theory Programacion_funcional_en_Isabelle imports Main begin text {* ----------------------...')
 
 
(No se muestran 2 ediciones intermedias del mismo usuario)
Línea 1: Línea 1:
−
<source lang="isar">
+
<source lang="isabelle">
−
header {* Relación 1: Programación funcional en Isabelle *}
+
header {* R1: Deducción natural proposicional *}
  
−
theory Programacion_funcional_en_Isabelle
+
theory R1
 
imports Main  
 
imports Main  
 
begin
 
begin
  
−
text {* ----------------------------------------------------------------
+
text {*
−
   Ejercicio 1. Definir, por recursión, la función
+
  ---------------------------------------------------------------------  
−
    longitud :: 'a list ⇒ nat
+
   El objetivo de esta relación es demostrar cada uno de los ejercicios
−
   tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
+
  usando sólo las reglas básicas de deducción natural de la lógica
−
    longitud [4,2,5] = 3
+
   proposicional (sin usar el método auto).
−
  ------------------------------------------------------------------- *}
 
  
−
fun longitud :: "'a list ⇒ nat" where
+
  Las reglas básicas de la deducción natural son las siguientes:
−
   "longitud xs = undefined"
+
  · TrueI:          True
−
 
+
  · conjI:          ⟦P; Q⟧ ⟹ P ∧ Q
−
value "longitud [4,2,5]" -- "= 3"
+
  · conjunct1:      P ∧ Q ⟹ P
 +
  · conjunct2:      P ∧ Q ⟹ Q
 +
  · conjE:          ⟦P ∧ Q; ⟦P; Q⟧ ⟹ R⟧ ⟹ R
 +
  · disjI1:        P ⟹ P ∨ Q
 +
  · disjI2:        Q ⟹ P ∨ Q
 +
  · disjE:          ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
 +
  · notI:          (P ⟹ False) ⟹ ¬P
 +
  · notE:          ⟦¬P; P⟧ ⟹ R
 +
  · FalseE:        False ⟹ P
 +
  · notnotD:        ¬¬ P ⟹ P
 +
  · impI:          (P ⟹ Q) ⟹ P ⟶ Q
 +
  · impE:          ⟦P ⟶ Q; P; Q ⟹ R⟧ ⟹ R
 +
  · mp:            ⟦P ⟶ Q; P⟧ ⟹ Q
 +
  · iff:            (P ⟶ Q) ⟶ (Q ⟶ P) ⟶ P = Q
 +
  · iffI:          ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
 +
  · iffD1:          ⟦Q = P; Q⟧ ⟹ P
 +
  · iffD2:          ⟦P = Q; Q⟧ ⟹ P
 +
  · iffE:          ⟦P = Q; ⟦P ⟶ Q; Q ⟶ P⟧ ⟹ R⟧ ⟹ R
 +
  · ccontr:        (¬P ⟹ False) ⟹ P
 +
  · classical:      (¬P ⟹ P) ⟹ P     
 +
  · exluded_middle: ¬P ∨ P
 +
  · disjCI:        (¬Q ⟹ P) ⟹ P ∨ Q
 +
  · impCE:          ⟦P ⟶ Q; ¬P ⟹ R; Q ⟹ R⟧ ⟹ R
 +
  · iffCE:          ⟦P = Q; ⟦P; Q⟧ ⟹ R; ⟦¬P; ¬Q⟧ ⟹ R⟧ ⟹ R
 +
  · swap:          ⟦¬P; ¬R ⟹ P⟧ ⟹ R
 +
  ---------------------------------------------------------------------
 +
*}
 +
 
 +
text {*
 +
  Se usarán las reglas notnotI y mt que demostramos a continuación. *}
 +
 
 +
lemma notnotI: "P ⟹ ¬¬ P"
 +
by auto
 +
 
 +
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
 +
by auto
 +
 
 +
section {* Implicaciones *}
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 1. Demostrar
 +
      p ⟶ q, p ⊢ q
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_1:
 +
  assumes "p ⟶ q"
 +
          "p"
 +
  shows "q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 2. Demostrar
 +
    p ⟶ q, q ⟶ r, p ⊢ r
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_2:
 +
  assumes "p ⟶ q"
 +
          "q ⟶ r"
 +
          "p"
 +
  shows "r"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
   Ejercicio 3. Demostrar
 +
    p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_3:
 +
  assumes "p ⟶ (q ⟶ r)"
 +
          "p ⟶ q"
 +
          "p"
 +
  shows "r"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 4. Demostrar
 +
    p ⟶ q, q ⟶ r ⊢ p ⟶ r
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_4:
 +
  assumes "p ⟶ q"
 +
          "q ⟶ r"
 +
  shows "p ⟶ r"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 5. Demostrar
 +
    p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_5:
 +
  assumes "p ⟶ (q ⟶ r)"
 +
  shows  "q ⟶ (p ⟶ r)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 6. Demostrar
 +
    p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_6:
 +
  assumes "p ⟶ (q ⟶ r)"
 +
  shows  "(p ⟶ q) ⟶ (p ⟶ r)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 7. Demostrar
 +
    p ⊢ q ⟶ p
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_7:
 +
  assumes "p" 
 +
  shows  "q ⟶ p"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 8. Demostrar
 +
    ⊢ p ⟶ (q ⟶ p)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_8:
 +
  "p ⟶ (q ⟶ p)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 9. Demostrar
 +
    p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_9:
 +
  assumes "p ⟶ q"
 +
  shows  "(q ⟶ r) ⟶ (p ⟶ r)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 10. Demostrar
 +
    p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_10:
 +
  assumes "p ⟶ (q ⟶ (r ⟶ s))"
 +
  shows  "r ⟶ (q ⟶ (p ⟶ s))"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 11. Demostrar
 +
    ⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_11:
 +
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 12. Demostrar
 +
    (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_12:
 +
  assumes "(p ⟶ q) ⟶ r"
 +
  shows  "p ⟶ (q ⟶ r)"
 +
oops
 +
 
 +
section {* Conjunciones *}
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 13. Demostrar
 +
    p, q ⊢  p ∧ q
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_13:
 +
  assumes "p"
 +
          "q"
 +
  shows "p ∧ q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 14. Demostrar
 +
    p ∧ q ⊢ p
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_14:
 +
  assumes "p ∧ q" 
 +
  shows  "p"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 15. Demostrar
 +
    p ∧ q ⊢ q
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_15:
 +
  assumes "p ∧ q"
 +
  shows  "q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 16. Demostrar
 +
    p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_16:
 +
  assumes "p ∧ (q ∧ r)"
 +
  shows  "(p ∧ q) ∧ r"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 17. Demostrar
 +
    (p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_17:
 +
  assumes "(p ∧ q) ∧ r"
 +
  shows  "p ∧ (q ∧ r)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 18. Demostrar
 +
    p ∧ q ⊢ p ⟶ q
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_18:
 +
  assumes "p ∧ q"
 +
  shows  "p ⟶ q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 19. Demostrar
 +
    (p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r 
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_19:
 +
  assumes "(p ⟶ q) ∧ (p ⟶ r)"
 +
  shows  "p ⟶ q ∧ r"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 20. Demostrar
 +
    p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_20:
 +
  assumes "p ⟶ q ∧ r"
 +
  shows  "(p ⟶ q) ∧ (p ⟶ r)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 21. Demostrar
 +
    p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_21:
 +
  assumes "p ⟶ (q ⟶ r)"
 +
  shows  "p ∧ q ⟶ r"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 22. Demostrar
 +
    p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_22:
 +
  assumes "p ∧ q ⟶ r"
 +
  shows  "p ⟶ (q ⟶ r)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 23. Demostrar
 +
    (p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_23:
 +
  assumes "(p ⟶ q) ⟶ r"
 +
  shows  "p ∧ q ⟶ r"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 24. Demostrar
 +
    p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_24:
 +
  assumes "p ∧ (q ⟶ r)"
 +
  shows  "(p ⟶ q) ⟶ r"
 +
oops
 +
 
 +
section {* Disyunciones *}
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 25. Demostrar
 +
    p ⊢ p ∨ q
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_25:
 +
  assumes "p"
 +
  shows  "p ∨ q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 26. Demostrar
 +
    q ⊢ p ∨ q
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_26:
 +
  assumes "q"
 +
  shows  "p ∨ q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 27. Demostrar
 +
    p ∨ q ⊢ q ∨ p
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_27:
 +
  assumes "p ∨ q"
 +
  shows  "q ∨ p"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 28. Demostrar
 +
    q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_28:
 +
  assumes "q ⟶ r"
 +
  shows  "p ∨ q ⟶ p ∨ r"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 29. Demostrar
 +
    p ∨ p ⊢ p
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_29:
 +
  assumes "p ∨ p"
 +
  shows  "p"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 30. Demostrar
 +
    p ⊢ p ∨ p
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_30:
 +
  assumes "p"
 +
  shows  "p ∨ p"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 31. Demostrar
 +
    p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_31:
 +
  assumes "p ∨ (q ∨ r)"
 +
  shows  "(p ∨ q) ∨ r"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 32. Demostrar
 +
    (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_32:
 +
  assumes "(p ∨ q) ∨ r"
 +
  shows  "p ∨ (q ∨ r)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 33. Demostrar
 +
    p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_33:
 +
  assumes "p ∧ (q ∨ r)"
 +
  shows  "(p ∧ q) ∨ (p ∧ r)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 34. Demostrar
 +
    (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_34:
 +
  assumes "(p ∧ q) ∨ (p ∧ r)"
 +
  shows  "p ∧ (q ∨ r)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 35. Demostrar
 +
    p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_35:
 +
  assumes "p ∨ (q ∧ r)"
 +
  shows  "(p ∨ q) ∧ (p ∨ r)"
 +
oops
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
−
   Ejercicio 2. Definir la función
+
   Ejercicio 36. Demostrar
−
     fun intercambia :: 'a × 'b ⇒ 'b × 'a
+
     (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
−
  tal que (intercambia p) es el par obtenido intercambiando las
 
−
  componentes del par p. Por ejemplo,
 
−
    intercambia (u,v) = (v,u)
 
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
+
lemma ejercicio_36:
−
   "intercambia (x,y) = undefined"
+
  assumes "(p ∨ q) ∧ (p ∨ r)"
 +
  shows   "p ∨ (q ∧ r)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 37. Demostrar
 +
    (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
 +
  ------------------------------------------------------------------ *}
  
−
value "intercambia (u,v)" -- "= (v,u)"
+
lemma ejercicio_37:
 +
  assumes "(p ⟶ r) ∧ (q ⟶ r)"  
 +
  shows  "p ∨ q ⟶ r"
 +
oops
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
−
   Ejercicio 3. Definir, por recursión, la función
+
   Ejercicio 38. Demostrar
−
     inversa :: 'a list ⇒ 'a list
+
     p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
−
  tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
 
−
  elementos de xs. Por ejemplo,
 
−
    inversa [a,d,c] = [c,d,a]
 
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
fun inversa :: "'a list ⇒ 'a list" where
+
lemma ejercicio_38:
−
   "inversa xs = undefined"
+
  assumes "p ∨ q ⟶ r"  
 +
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
 +
oops
  
−
value "inversa [a,d,c]" -- "= [c,d,a]"
+
section {* Negaciones *}
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
−
   Ejercicio 4. Definir la función
+
   Ejercicio 39. Demostrar
−
     repite :: nat ⇒ 'a ⇒ 'a list
+
     p ⊢ ¬¬p
−
  tal que (repite n x) es la lista formada por n copias del elemento
 
−
  x. Por ejemplo,
 
−
    repite 3 a = [a,a,a]
 
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
fun repite :: "nat ⇒ 'a ⇒ 'a list" where
+
lemma ejercicio_39:
−
   "repite n x = undefined"
+
  assumes "p"
 +
  shows   "¬¬p"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 40. Demostrar
 +
    ¬p ⊢ p ⟶ q
 +
  ------------------------------------------------------------------ *}
  
−
value "repite 3 a" -- "= [a,a,a]"
+
lemma ejercicio_40:
 +
  assumes "¬p"  
 +
  shows  "p ⟶ q"
 +
oops
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
−
   Ejercicio 5. Definir la función
+
   Ejercicio 41. Demostrar
−
     conc :: 'a list ⇒ 'a list ⇒ 'a list
+
     p ⟶ q ⊢ ¬q ⟶ ¬p
−
  tal que (conc xs ys) es la concatención de las listas xs e ys. Por
 
−
  ejemplo,
 
−
    conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
 
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
+
lemma ejercicio_41:
−
   "conc xs ys = undefined"
+
  assumes "p ⟶ q"
 +
  shows   "¬q ⟶ ¬p"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 42. Demostrar
 +
    p∨q, ¬q ⊢ p
 +
  ------------------------------------------------------------------ *}
  
−
value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"
+
lemma ejercicio_42:
 +
  assumes "p∨q"
 +
          "¬q"  
 +
  shows  "p"
 +
oops
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
−
   Ejercicio 6. Definir la función
+
   Ejercicio 42. Demostrar
−
     coge :: nat ⇒ 'a list ⇒ 'a list
+
     p ∨ q, ¬p ⊢ q
−
  tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
 
−
  ejemplo,
 
−
    coge 2 [a,c,d,b,e] = [a,c]
 
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
+
lemma ejercicio_43:
−
   "coge n xs = undefined"
+
  assumes "p ∨ q"
 +
          "¬p"  
 +
  shows   "q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 40. Demostrar
 +
    p ∨ q ⊢ ¬(¬p ∧ ¬q)
 +
  ------------------------------------------------------------------ *}
  
−
value "coge 2 [a,c,d,b,e]" -- "= [a,c]"
+
lemma ejercicio_44:
 +
  assumes "p ∨ q"  
 +
  shows  "¬(¬p ∧ ¬q)"
 +
oops
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
−
   Ejercicio 7. Definir la función
+
   Ejercicio 45. Demostrar
−
     elimina :: nat ⇒ 'a list ⇒ 'a list
+
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
−
  tal que (elimina n xs) es la lista obtenida eliminando los n primeros
 
−
  elementos de xs. Por ejemplo,
 
−
    elimina 2 [a,c,d,b,e] = [d,b,e]
 
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
+
lemma ejercicio_45:
−
   "elimina n xs = undefined"
+
  assumes "p ∧ q"  
 +
  shows   "¬(¬p ∨ ¬q)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 46. Demostrar
 +
    ¬(p ∨ q) ⊢ ¬p ∧ ¬q
 +
  ------------------------------------------------------------------ *}
  
−
value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"
+
lemma ejercicio_46:
 +
  assumes "¬(p ∨ q)"  
 +
  shows  "¬p ∧ ¬q"
 +
oops
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
−
   Ejercicio 8. Definir la función
+
   Ejercicio 47. Demostrar
−
     esVacia :: 'a list ⇒ bool
+
     ¬p ∧ ¬q ⊢ ¬(p ∨ q)
−
  tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
 
−
    esVacia []  = True
 
−
    esVacia [1] = False
 
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
fun esVacia :: "'a list ⇒ bool" where
+
lemma ejercicio_47:
−
   "esVacia xs = undefined"
+
  assumes "¬p ∧ ¬q"  
 +
  shows   "¬(p ∨ q)"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 48. Demostrar
 +
    ¬p ∨ ¬q ⊢ ¬(p ∧ q)
 +
  ------------------------------------------------------------------ *}
  
−
value "esVacia []" -- "= True"
+
lemma ejercicio_48:
−
value "esVacia [1]" -- "= False"
+
  assumes "¬p ∨ ¬q"
 +
  shows  "¬(p ∧ q)"
 +
oops
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
−
   Ejercicio 9. Definir la función
+
   Ejercicio 49. Demostrar
−
     inversaAc :: 'a list ⇒ 'a list
+
     ⊢ ¬(p ∧ ¬p)
−
  tal que (inversaAc xs) es a inversa de xs calculada usando
 
−
  acumuladores. Por ejemplo,
 
−
    inversaAc [a,c,b,e] = [e,b,c,a]
 
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
+
lemma ejercicio_49:
−
   "inversaAcAux xs ys = undefined"
+
   "¬(p ∧ ¬p)"
 +
oops
  
−
fun inversaAc :: "'a list ⇒ 'a list" where
+
text {* ---------------------------------------------------------------
−
   "inversaAc xs = undefined"
+
  Ejercicio 50. Demostrar
 +
    p ∧ ¬p ⊢ q
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_50:
 +
  assumes "p ∧ ¬p"
 +
  shows  "q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 51. Demostrar
 +
    ¬¬p ⊢ p
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_51:
 +
  assumes "¬¬p"
 +
  shows   "p"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 52. Demostrar
 +
    ⊢ p ∨ ¬p
 +
  ------------------------------------------------------------------ *}
  
−
value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"
+
lemma ejercicio_52:
 +
  "p ∨ ¬p"
 +
oops
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
−
   Ejercicio 10. Definir la función
+
   Ejercicio 53. Demostrar
−
     sum :: nat list ⇒ nat
+
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
−
  tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
 
−
    sum [3,2,5] = 10
 
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
fun sum :: "nat list ⇒ nat" where
+
lemma ejercicio_53:
−
   "sum xs = undefined"
+
   "((p ⟶ q) ⟶ p) ⟶ p"
 +
oops
  
−
value "sum [3,2,5]" -- "= 10"
+
text {* ---------------------------------------------------------------
 +
  Ejercicio 54. Demostrar
 +
    ¬q ⟶ ¬p ⊢ p ⟶ q
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_54:
 +
  assumes "¬q ⟶ ¬p"
 +
  shows  "p ⟶ q"
 +
oops
  
 
text {* ---------------------------------------------------------------  
 
text {* ---------------------------------------------------------------  
−
   Ejercicio 11. Definir la función
+
   Ejercicio 55. Demostrar
−
     map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
+
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
−
  tal que (map f xs) es la lista obtenida aplicando la función f a los
 
−
  elementos de xs. Por ejemplo,
 
−
    map (λx. 2*x) [3,2,5] = [6,4,10]
 
 
   ------------------------------------------------------------------ *}
 
   ------------------------------------------------------------------ *}
  
−
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
+
lemma ejercicio_55:
−
   "map f xs = undefined"
+
  assumes "¬(¬p ∧ ¬q)"
 +
  shows  "p ∨ q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 56. Demostrar
 +
    ¬(¬p ∨ ¬q) ⊢ p ∧ q
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_56:
 +
  assumes "¬(¬p ∨ ¬q)"
 +
  shows  "p ∧ q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 57. Demostrar
 +
    ¬(p ∧ q) ⊢ ¬p ∨ ¬q
 +
  ------------------------------------------------------------------ *}
 +
 
 +
lemma ejercicio_57:
 +
  assumes "¬(p ∧ q)"
 +
  shows   "¬p ∨ ¬q"
 +
oops
 +
 
 +
text {* ---------------------------------------------------------------
 +
  Ejercicio 58. Demostrar
 +
    ⊢ (p ⟶ q) ∨ (q ⟶ p)
 +
  ------------------------------------------------------------------ *}
  
−
value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"
+
lemma ejercicio_58:
 +
  "(p ⟶ q) ∨ (q ⟶ p)"
 +
oops
  
 
end
 
end
 
</source>
 
</source>

Revisión actual del 13:47 15 jul 2018

header {* R1: Deducción natural proposicional *}

theory R1
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta relación es demostrar cada uno de los ejercicios
  usando sólo las reglas básicas de deducción natural de la lógica
  proposicional (sin usar el método auto).

  Las reglas básicas de la deducción natural son las siguientes:
  · TrueI:          True
  · conjI:          ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:      P ∧ Q ⟹ P
  · conjunct2:      P ∧ Q ⟹ Q
  · conjE:          ⟦P ∧ Q; ⟦P; Q⟧ ⟹ R⟧ ⟹ R
  · disjI1:         P ⟹ P ∨ Q
  · disjI2:         Q ⟹ P ∨ Q
  · disjE:          ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
  · notI:           (P ⟹ False) ⟹ ¬P
  · notE:           ⟦¬P; P⟧ ⟹ R
  · FalseE:         False ⟹ P
  · notnotD:        ¬¬ P ⟹ P
  · impI:           (P ⟹ Q) ⟹ P ⟶ Q
  · impE:           ⟦P ⟶ Q; P; Q ⟹ R⟧ ⟹ R
  · mp:             ⟦P ⟶ Q; P⟧ ⟹ Q
  · iff:            (P ⟶ Q) ⟶ (Q ⟶ P) ⟶ P = Q
  · iffI:           ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:          ⟦Q = P; Q⟧ ⟹ P
  · iffD2:          ⟦P = Q; Q⟧ ⟹ P
  · iffE:           ⟦P = Q; ⟦P ⟶ Q; Q ⟶ P⟧ ⟹ R⟧ ⟹ R
  · ccontr:         (¬P ⟹ False) ⟹ P
  · classical:      (¬P ⟹ P) ⟹ P      
  · exluded_middle: ¬P ∨ P
  · disjCI:         (¬Q ⟹ P) ⟹ P ∨ Q
  · impCE:          ⟦P ⟶ Q; ¬P ⟹ R; Q ⟹ R⟧ ⟹ R
  · iffCE:          ⟦P = Q; ⟦P; Q⟧ ⟹ R; ⟦¬P; ¬Q⟧ ⟹ R⟧ ⟹ R
  · swap:           ⟦¬P; ¬R ⟹ P⟧ ⟹ R
  --------------------------------------------------------------------- 
*}

text {*
  Se usarán las reglas notnotI y mt que demostramos a continuación. *}

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

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

section {* Implicaciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       p ⟶ q, p ⊢ q
  ------------------------------------------------------------------ *}

lemma ejercicio_1:
  assumes "p ⟶ q"
          "p"
  shows "q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
     p ⟶ q, q ⟶ r, p ⊢ r
  ------------------------------------------------------------------ *}

lemma ejercicio_2:
  assumes "p ⟶ q"
          "q ⟶ r"
          "p" 
  shows "r"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar
     p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
  ------------------------------------------------------------------ *}

lemma ejercicio_3:
  assumes "p ⟶ (q ⟶ r)"
          "p ⟶ q"
          "p"
  shows "r"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar
     p ⟶ q, q ⟶ r ⊢ p ⟶ r
  ------------------------------------------------------------------ *}

lemma ejercicio_4:
  assumes "p ⟶ q"
          "q ⟶ r" 
  shows "p ⟶ r"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
     p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_5:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
     p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_6:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar
     p ⊢ q ⟶ p
  ------------------------------------------------------------------ *}

lemma ejercicio_7:
  assumes "p"  
  shows   "q ⟶ p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
     ⊢ p ⟶ (q ⟶ p)
  ------------------------------------------------------------------ *}

lemma ejercicio_8:
  "p ⟶ (q ⟶ p)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
     p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_9:
  assumes "p ⟶ q" 
  shows   "(q ⟶ r) ⟶ (p ⟶ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
     p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
  ------------------------------------------------------------------ *}

lemma ejercicio_10:
  assumes "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 11. Demostrar
     ⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
  ------------------------------------------------------------------ *}

lemma ejercicio_11:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_12:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
oops

section {* Conjunciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar
     p, q ⊢  p ∧ q
  ------------------------------------------------------------------ *}

lemma ejercicio_13:
  assumes "p"
          "q" 
  shows "p ∧ q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar
     p ∧ q ⊢ p
  ------------------------------------------------------------------ *}

lemma ejercicio_14:
  assumes "p ∧ q"  
  shows   "p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 15. Demostrar
     p ∧ q ⊢ q
  ------------------------------------------------------------------ *}

lemma ejercicio_15:
  assumes "p ∧ q" 
  shows   "q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 16. Demostrar
     p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
  ------------------------------------------------------------------ *}

lemma ejercicio_16:
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 17. Demostrar
     (p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_17:
  assumes "(p ∧ q) ∧ r" 
  shows   "p ∧ (q ∧ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 18. Demostrar
     p ∧ q ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

lemma ejercicio_18:
  assumes "p ∧ q" 
  shows   "p ⟶ q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 19. Demostrar
     (p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r   
  ------------------------------------------------------------------ *}

lemma ejercicio_19:
  assumes "(p ⟶ q) ∧ (p ⟶ r)" 
  shows   "p ⟶ q ∧ r"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 20. Demostrar
     p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_20:
  assumes "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 21. Demostrar
     p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}

lemma ejercicio_21:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 22. Demostrar
     p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_22:
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}

lemma ejercicio_23:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 24. Demostrar
     p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
  ------------------------------------------------------------------ *}

lemma ejercicio_24:
  assumes "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
oops

section {* Disyunciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 25. Demostrar
     p ⊢ p ∨ q
  ------------------------------------------------------------------ *}

lemma ejercicio_25:
  assumes "p"
  shows   "p ∨ q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
     q ⊢ p ∨ q
  ------------------------------------------------------------------ *}

lemma ejercicio_26:
  assumes "q"
  shows   "p ∨ q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 27. Demostrar
     p ∨ q ⊢ q ∨ p
  ------------------------------------------------------------------ *}

lemma ejercicio_27:
  assumes "p ∨ q"
  shows   "q ∨ p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 28. Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
  ------------------------------------------------------------------ *}

lemma ejercicio_28:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 29. Demostrar
     p ∨ p ⊢ p
  ------------------------------------------------------------------ *}

lemma ejercicio_29:
  assumes "p ∨ p"
  shows   "p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 30. Demostrar
     p ⊢ p ∨ p
  ------------------------------------------------------------------ *}

lemma ejercicio_30:
  assumes "p" 
  shows   "p ∨ p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 31. Demostrar
     p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
  ------------------------------------------------------------------ *}

lemma ejercicio_31:
  assumes "p ∨ (q ∨ r)" 
  shows   "(p ∨ q) ∨ r"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 32. Demostrar
     (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_32:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 33. Demostrar
     p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_33:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 34. Demostrar
     (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_34:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 35. Demostrar
     p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_35:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 36. Demostrar
     (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_36:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 37. Demostrar
     (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
  ------------------------------------------------------------------ *}

lemma ejercicio_37:
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 38. Demostrar
     p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
  ------------------------------------------------------------------ *}

lemma ejercicio_38:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
oops

section {* Negaciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 39. Demostrar
     p ⊢ ¬¬p
  ------------------------------------------------------------------ *}

lemma ejercicio_39:
  assumes "p"
  shows   "¬¬p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

lemma ejercicio_40:
  assumes "¬p" 
  shows   "p ⟶ q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 41. Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p
  ------------------------------------------------------------------ *}

lemma ejercicio_41:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p∨q, ¬q ⊢ p
  ------------------------------------------------------------------ *}

lemma ejercicio_42:
  assumes "p∨q"
          "¬q" 
  shows   "p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p ∨ q, ¬p ⊢ q
  ------------------------------------------------------------------ *}

lemma ejercicio_43:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     p ∨ q ⊢ ¬(¬p ∧ ¬q)
  ------------------------------------------------------------------ *}

lemma ejercicio_44:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 45. Demostrar
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
  ------------------------------------------------------------------ *}

lemma ejercicio_45:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 46. Demostrar
     ¬(p ∨ q) ⊢ ¬p ∧ ¬q
  ------------------------------------------------------------------ *}

lemma ejercicio_46:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 47. Demostrar
     ¬p ∧ ¬q ⊢ ¬(p ∨ q)
  ------------------------------------------------------------------ *}

lemma ejercicio_47:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 48. Demostrar
     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
  ------------------------------------------------------------------ *}

lemma ejercicio_48:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 49. Demostrar
     ⊢ ¬(p ∧ ¬p)
  ------------------------------------------------------------------ *}

lemma ejercicio_49:
  "¬(p ∧ ¬p)"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 50. Demostrar
     p ∧ ¬p ⊢ q
  ------------------------------------------------------------------ *}

lemma ejercicio_50:
  assumes "p ∧ ¬p" 
  shows   "q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 51. Demostrar
     ¬¬p ⊢ p
  ------------------------------------------------------------------ *}

lemma ejercicio_51:
  assumes "¬¬p"
  shows   "p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 52. Demostrar
     ⊢ p ∨ ¬p
  ------------------------------------------------------------------ *}

lemma ejercicio_52:
  "p ∨ ¬p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 53. Demostrar
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
  ------------------------------------------------------------------ *}

lemma ejercicio_53:
  "((p ⟶ q) ⟶ p) ⟶ p"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 54. Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

lemma ejercicio_54:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 55. Demostrar
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
  ------------------------------------------------------------------ *}

lemma ejercicio_55:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 56. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------ *}

lemma ejercicio_56:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 57. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------ *}

lemma ejercicio_57:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
oops

text {* --------------------------------------------------------------- 
  Ejercicio 58. Demostrar
     ⊢ (p ⟶ q) ∨ (q ⟶ p)
  ------------------------------------------------------------------ *}

lemma ejercicio_58:
  "(p ⟶ q) ∨ (q ⟶ p)"
oops

end
Obtenido de «https://www.glc.us.es/~jalonso/DAO/index.php?title=RA12_Relación_1&oldid=166»