Tema 8b: Deducción natural en lógica de primer orden con Isabelle/HOL

 1 ⟶ x + 1 > 0 ⊢ 1 + x > 1 ⟶ 1 + x > 0
*}

― ‹La demostración detallada es›
lemma ejemplo_9a: 
  assumes "x + 1 = 1 + x" 
          "x + 1 > 1 ⟶ x + 1 > 0"
  shows   "1 + x > 1 ⟶ 1 + x > 0"
proof -
  show "1 + x > 1 ⟶ 1 + x > 0" using assms by (rule subst)
qed

― ‹La demostración estructurada es›
lemma ejemplo_9b: 
  assumes "x + 1 = 1 + x" 
          "x + 1 > 1 ⟶ x + 1 > 0"
  shows   "1 + x > 1 ⟶ 1 + x > 0"
using assms 
by (rule subst)

― ‹La demostración automática es›
lemma ejemplo_9c: 
  assumes "x + 1 = 1 + x" 
          "x + 1 > 1 ⟶ x + 1 > 0"
  shows   "1 + x > 1 ⟶ 1 + x > 0"
using assms 
by auto

text {* 
  Ejemplo 10 (p. 27). Demostrar
     x = y, y = z ⊢ x = z
*}

― ‹La demostración detallada es›
lemma ejemplo_10a:
  assumes "x = y" 
          "y = z"
  shows   "x = z"
proof -
  show "x = z" using assms(2,1) by (rule subst)
qed

― ‹La demostración estructurada es›
lemma ejemplo_10b: 
  assumes "x = y" 
          "y = z"
  shows   "x = z"
using assms(2,1)
by (rule subst)

― ‹La demostración automática es›
lemma ejemplo_10c: 
  assumes "x = y" 
          "y = z"
  shows   "x = z"
using assms
by auto

text {* 
  Ejemplo 11 (p. 28). Demostrar
     s = t ⊢ t = s
*}

― ‹La demostración detallada es›
lemma ejemplo_11a:
  assumes "s = t"
  shows   "t = s"
proof -
  have "s = s" by (rule refl)
  with assms show "t = s" by (rule subst)
qed

― ‹La demostración automática es›
lemma ejemplo_11b:
  assumes "s = t"
  shows   "t = s"
using assms
by auto

end

De Razonamiento automático (2018-19)