Ver el código de «Ejercicios del tema 4» - Demostración asistida por ordenador (2011-12)

<source lang="isar">
theory Relacion_10
imports Main 
begin 

section {* Deducción natural de primer orden *}

text {* Los ejercicios de esta relación deben de resolverse usando sólo
  las reglas básicas de la deducción natural proposicional y de primer 
  orden:
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  . notnotI:    P ⟹ ¬¬ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · mt:         ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  · 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
  · allI:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  · allE:       (⋀x. P x) ⟹ ∀x. P x
  · exI:        P x ⟹ ∃x. P x
  · exE:        ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
*}

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

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

lemma ejercicio_1:
  assumes "∀x. P x ⟶ Q x" 
  shows "(∀x. P x) ⟶ (∀x. Q x)"
oops

lemma ejercicio_2:
  assumes "∃x. ¬P x" 
  shows " ¬(∀x. P x)"
oops

lemma ejercicio_3:
  assumes "∀x. P x" 
  shows "∀y. P y"
oops

lemma ejercicio_4:
  assumes "∀x. P x ⟶ Q x" 
  shows "(∀x. ¬Q x) ⟶ (∀x. ¬P x)"
oops

lemma ejercicio_5:
  assumes "∀x. P x ⟶ ¬Q x" 
  shows "¬(∃x. P x ∧ Q x)"
oops

lemma ejercicio_6:
  assumes "∀x. ∀y. P x y" 
  shows "∀u. ∀v. P u v"
oops

lemma ejercicio_7:
  assumes "∃x. ∃y. P x y" 
  shows "∃u. ∃v. P u v"
oops

lemma ejercicio_8:
  assumes "∃x. ∀y. P x y" 
  shows "∀y. ∃x. P x y"
oops

lemma ejercicio_9:
  assumes "∃x. P a ⟶ Q x" 
  shows "P a ⟶ (∃x. Q x)"
oops

lemma ejercicio_10:
  assumes "P a ⟶ (∃x. Q x)" 
  shows "∃x. P a ⟶ Q x"
oops

lemma ejercicio_11:
  assumes "(∃x. P x) ⟶ Q a" 
  shows "∀x. P x ⟶ Q a"
oops

lemma ejercicio_12:
  assumes "∀x. P x ⟶ Q a" 
  shows "∃x. P x ⟶ Q a"
oops

lemma ejercicio_13:
  assumes "(∀x. P x) ∨ (∀x. Q x)" 
  shows "∀x. P x ∨ Q x"
oops

lemma ejercicio_14:
  assumes "∃x. P x ∧ Q x" 
  shows "(∃x. P x) ∧ (∃x. Q x)"
oops

lemma ejercicio_15:
  assumes "∀x.∀y. P y ⟶ Q x" 
  shows "(∃y. P y) ⟶ (∀x. Q x)"
oops

lemma ejercicio_16:
  assumes "¬(∀x. ¬P x)" 
  shows "∃x. P x"
oops

lemma ejercicio_17:
  assumes "∀x. ¬P x" 
  shows "¬(∃x. P x)"
oops

lemma ejercicio_18:
  assumes "∃x. P x" 
  shows "¬(∀x. ¬P x)"
oops

lemma ejercicio_19:
  assumes "P a ⟶ (∀x. Q x)" 
  shows "∀x. P a ⟶ Q x"
oops

lemma ejercicio_20:
  assumes "∀x.∀y.∀z. R x y ∧ R y z ⟶ R x z" and
          "∀x. ¬R x x"
  shows "∀x.∀y. R x y ⟶ ¬R y x"
oops

lemma ejercicio_21:
  assumes "∀x. P x ∨ Q x" and
          "∃x. ¬Q x" and
          "∀x. R x ⟶ ¬P x"
  shows "∃x. ¬R x"
oops

lemma ejercicio_22:
  assumes "∀x. P x ⟶ Q x ∨ R x" and
          "¬(∃x. P x ∧ R x)"
  shows "∀x. P x ⟶ Q x"
oops

lemma ejercicio_23:
  assumes "∃x.∃y. R x y ∨ R y x" 
  shows "∃x.∃y. R x y"
oops

end
</source>