chapter ‹Tema 4a: Deducción natural en lógica de primer orden›
theory T4a_Deduccion_natural_en_logica_de_primer_orden
imports Main
begin
text ‹El objetivo de este tema es presentar la deducción natural en
lógica de primer orden con Isabelle/HOL. La presentación se
basa en los ejemplos de tema 4 del curso LMF que se encuentra
en http://goo.gl/uJj8d (que a su vez se basa en el libro de
Huth y Ryan "Logic in Computer Science" http://goo.gl/qsVpY ).
La página al lado de cada ejemplo indica la página de las
transparencias de LMF donde se encuentra la demostración.›
section ‹Reglas del cuantificador universal›
text ‹Las reglas del cuantificador universal son
· allE: ⟦∀x. P x; P a ⟹ R⟧ ⟹ R
· allI: (⋀x. P x) ⟹ ∀x. P x
›
subsection ‹Ejemplo 1›
text ‹Ejemplo 1 (p. 10). Demostrar que
P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c)
›
subsubsection ‹Demostración detallada›
― ‹La demostración detallada es›
lemma ejemplo_1a:
assumes 1: "P(c)" and
2: "∀x. (P(x) ⟶ ¬Q(x))"
shows "¬Q(c)"
proof -
have 3: "P(c) ⟶ ¬Q(c)" using 2 by (rule allE)
show 4: "¬Q(c)" using 3 1 by (rule mp)
qed
subsubsection ‹Demostración estructurada›
― ‹La demostración estructurada es›
lemma ejemplo_1b:
assumes "P(c)"
"∀x. (P(x) ⟶ ¬Q(x))"
shows "¬Q(c)"
proof -
have "P(c) ⟶ ¬Q(c)" using assms(2) ..
then show "¬Q(c)" using assms(1) ..
qed
subsubsection ‹Demostración automática›
― ‹La demostración automática es›
lemma ejemplo_1c:
assumes "P(c)"
"∀x. (P(x) ⟶ ¬Q(x))"
shows "¬Q(c)"
using assms
by auto
subsubsection ‹Demostración aplicativa›
lemma ejemplo_1d:
"⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)"
apply (erule allE) (* da ⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c *)
apply (erule mp) (* da P c ⟹ P c *)
apply assumption (* da No subgoals! *)
done
text ‹Explicaciones
apply (erule allE)
+ Objetivo: "⟦P(c); ∀x. (P(x) ⟶ ¬Q(x))⟧ ⟹ ¬Q(c)"
+ allE: "⟦∀x. ?P x; ?P ?x ⟹ ?R⟧ ⟹ ?R"
+ Unificador de ("¬Q(c)", "∀x. (P(x) ⟶ ¬Q(x))") y
("?R", "∀x. ?P x")
es ?R / ¬Q(c)
?P x / P(x) ⟶ ¬Q(x)
+ Nuevo objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c"
apply (erule mp)
+ Objetivo: "⟦P c; P ?x ⟶ ¬ Q ?x⟧ ⟹ ¬ Q c"
+ mp: "⟦?P ⟶ ?Q; ?P⟧ ⟹ ?Q"
+ Unificador de ("¬ Q c", "P ?x ⟶ ¬ Q ?x") y
("?Q", "?P ⟶ ?Q")
es ?Q / ¬ Q c
?P / P c
+ Nuevo objetivo: "P c ⟹ P c"
›
subsection ‹Ejemplo 2›
text ‹Ejemplo 2 (p. 11). Demostrar que
∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x)
›
subsubsection ‹Demostración detallada›
― ‹La demostración detallada es›
lemma ejemplo_2a:
assumes 1: "∀x. (P x ⟶ ¬(Q x))" and
2: "∀x. P x"
shows "∀x. ¬(Q x)"
proof -
{ fix a
have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
have 4: "P a" using 2 by (rule allE)
have 5: "¬(Q a)" using 3 4 by (rule mp) }
then show "∀x. ¬(Q x)" by (rule allI)
qed
― ‹La demostración detallada hacia atrás es›
lemma ejemplo_2b:
assumes 1: "∀x. (P x ⟶ ¬(Q x))" and
2: "∀x. P x"
shows "∀x. ¬(Q x)"
proof (rule allI)
fix a
have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
have 4: "P a" using 2 by (rule allE)
show 5: "¬(Q a)" using 3 4 by (rule mp)
qed
subsubsection ‹Demostración estructurada›
― ‹La demostración estructurada es›
lemma ejemplo_2c:
assumes "∀x. (P x ⟶ ¬(Q x))"
"∀x. P x"
shows "∀x. ¬(Q x)"
proof
fix a
have "P a" using assms(2) ..
have "P a ⟶ ¬(Q a)" using assms(1) ..
then show "¬(Q a)" using ‹P a› ..
qed
subsubsection ‹Demostración automática›
― ‹La demostración automática es›
lemma ejemplo_2d:
assumes "∀x. (P x ⟶ ¬(Q x))"
"∀x. P x"
shows "∀x. ¬(Q x)"
using assms
by auto
subsubsection ‹Demostración aplicativa›
lemma ejemplo_2e:
"⟦∀x. (P x ⟶ ¬(Q x)); ∀y. P y⟧ ⟹ ∀z. ¬(Q z)"
apply (rule allI) (* da ⋀z. ⟦P (?x2 z) ⟶ ¬ Q (?x2 z);
P (?y4 z)⟧
⟹ ¬ Q z*)
apply (erule allE)+ (* da ⋀z. ⟦P (?x2 z) ⟶ ¬ Q (?x2 z);
P (?y4 z)⟧
⟹ ¬ Q z *)
apply (erule mp) (* da ⋀z. P (?y4 z) ⟹ P z *)
apply assumption (* da No subgoals! *)
done
section ‹Reglas del cuantificador existencial›
text ‹Las reglas del cuantificador existencial son
· exI: P a ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
En la regla exE la nueva variable se introduce mediante la declaración
"obtain ... where ... by (rule exE)"
›
subsection ‹Ejemplo 3›
text ‹Ejemplo 3 (p. 12). Demostrar que
∀x. P x ⊢ ∃x. P x
›
subsubsection ‹Demostración detallada›
― ‹La demostración detallada es›
lemma ejemplo_3a:
assumes "∀x. P x"
shows "∃x. P x"
proof -
fix a
have "P a" using assms by (rule allE)
then show "∃x. P x" by (rule exI)
qed
subsubsection ‹Demostración estructurada›
― ‹La demostración estructurada es›
lemma ejemplo_3b:
assumes "∀x. P x"
shows "∃x. P x"
proof -
fix a
have "P a" using assms ..
then show "∃x. P x" ..
qed
― ‹La demostración estructurada se puede simplificar›
lemma ejemplo_3c:
assumes "∀x. P x"
shows "∃x. P x"
proof (rule exI)
fix a
show "P a" using assms ..
qed
― ‹La demostración estructurada se puede simplificar aún más›
lemma ejemplo_3d:
assumes "∀x. P x"
shows "∃x. P x"
proof
fix a
show "P a" using assms ..
qed
subsubsection ‹Demostración automática›
― ‹La demostración automática es›
lemma ejemplo_3e:
assumes "∀x. P x"
shows "∃x. P x"
using assms
by auto
subsubsection ‹Demostración aplicativa›
lemma ejemplo_3f:
"∀x. P x ⟹ ∃y. P y"
apply (erule allE) (* da P ?x ⟹ ∃y. P y *)
apply (erule exI) (* da No subgoals! *)
done
subsection ‹Ejemplo 4›
text ‹Ejemplo 4 (p. 13). Demostrar
∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x
›
subsubsection ‹Demostración detallada›
― ‹La demostración detallada es›
lemma ejemplo_4a:
assumes 1: "∀x. (P x ⟶ Q x)" and
2: "∃x. P x"
shows "∃x. Q x"
proof -
obtain a where 3: "P a" using 2 by (rule exE)
have 4: "P a ⟶ Q a" using 1 by (rule allE)
have 5: "Q a" using 4 3 by (rule mp)
then show 6: "∃x. Q x" by (rule exI)
qed
subsubsection ‹Demostración estructurada›
― ‹La demostración estructurada es›
lemma ejemplo_4b:
assumes "∀x. (P x ⟶ Q x)"
"∃x. P x"
shows "∃x. Q x"
proof -
obtain a where "P a" using assms(2) ..
have "P a ⟶ Q a" using assms(1) ..
then have "Q a" using ‹P a› ..
then show "∃x. Q x" ..
qed
subsubsection ‹Demostración automática›
― ‹La demostración automática es›
lemma ejemplo_4c:
assumes "∀x. (P x ⟶ Q x)"
"∃x. P x"
shows "∃x. Q x"
using assms
by auto
subsubsection ‹Demostración aplicativa›
lemma ejemplo_4f:
"⟦∀x. P x ⟶ Q x; ∃y. P y⟧ ⟹ ∃z. Q z"
apply (erule exE) (* da ⋀y. ⟦∀x. P x ⟶ Q x; P y⟧ ⟹ ∃z. Q z *)
apply (erule allE) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ ∃z. Q z *)
apply (rule exI) (* da ⋀y. ⟦P y; P (?x2 y) ⟶ Q (?x2 y)⟧ ⟹ Q (?z4 y) *)
apply (erule mp) (* da ⋀y. P y ⟹ P (?x2 y) *)
apply assumption (* da No subgoals! *)
done
section ‹Demostración de equivalencias›
subsection ‹Ejemplo 5.1›
text ‹Ejemplo 5.1 (p. 15). Demostrar
¬∀x. P x ⊢ ∃x. ¬(P x)›
subsubsection ‹Demostración detallada›
― ‹La demostración detallada es›
lemma ejemplo_5_1a:
assumes "¬(∀x. P(x))"
shows "∃x. ¬P(x)"
proof (rule ccontr)
assume "¬(∃x. ¬P(x))"
have "∀x. P(x)"
proof (rule allI)
fix a
show "P(a)"
proof (rule ccontr)
assume "¬P(a)"
then have "∃x. ¬P(x)" by (rule exI)
with ‹¬(∃x. ¬P(x))› show False by (rule notE)
qed
qed
with assms show False by (rule notE)
qed
subsubsection ‹Demostración estructurada›
― ‹La demostración estructurada es›
lemma ejemplo_5_1b:
assumes "¬(∀x. P(x))"
shows "∃x. ¬P(x)"
proof (rule ccontr)
assume "¬(∃x. ¬P(x))"
have "∀x. P(x)"
proof
fix a
show "P(a)"
proof (rule ccontr)
assume "¬P(a)"
then have "∃x. ¬P(x)" ..
with ‹¬(∃x. ¬P(x))› show False ..
qed
qed
with assms show False ..
qed
subsubsection ‹Demostración automática›
― ‹La demostración automática es›
lemma ejemplo_5_1c:
assumes "¬(∀x. P(x))"
shows "∃x. ¬P(x)"
using assms
by auto
subsubsection ‹Demostración aplicativa›
lemma ejemplo_5_1d: "¬(∀x. P x) ⟹ ∃y. ¬P y"
apply (rule ccontr) (* da ⟦¬ (∀x. P x); ∄y. ¬ P y⟧ ⟹ False *)
apply (erule notE) (* da ∄y. ¬ P y ⟹ ∀x. P x *)
apply (rule allI) (* da ⋀x. ∄y. ¬ P y ⟹ P x *)
apply (rule ccontr) (* da ⋀x. ⟦∄y. ¬ P y; ¬ P x⟧ ⟹ False *)
apply (erule notE) (* da ⋀x. ¬ P x ⟹ ∃y. ¬ P y *)
apply (erule exI) (* da No subgoals! *)
done
text ‹
Ejemplo 5.2 (p. 16). Demostrar
∃x. ¬(P x) ⊢ ¬∀x. P x›
― ‹La demostración detallada es›
lemma ejemplo_5_2a:
assumes "∃x. ¬P(x)"
shows "¬(∀x. P(x))"
proof (rule notI)
assume "∀x. P(x)"
obtain a where "¬P(a)" using assms by (rule exE)
have "P(a)" using ‹∀x. P(x)› by (rule allE)
with ‹¬P(a)› show False by (rule notE)
qed
― ‹La demostración estructurada es›
lemma ejemplo_5_2b:
assumes "∃x. ¬P(x)"
shows "¬(∀x. P(x))"
proof
assume "∀x. P(x)"
obtain a where "¬P(a)" using assms ..
have "P(a)" using ‹∀x. P(x)› ..
with ‹¬P(a)› show False ..
qed
― ‹La demostración automática es›
lemma ejemplo_5_2c:
assumes "∃x. ¬P(x)"
shows "¬(∀x. P(x))"
using assms
by auto
text ‹
Ejemplo 5.3 (p. 17). Demostrar
⊢ ¬∀x. P x ⟷ ∃x. ¬(P x)›
― ‹La demostración detallada es›
lemma ejemplo_5_3a:
"(¬(∀x. P(x))) ⟷ (∃x. ¬P(x))"
proof (rule iffI)
assume "¬(∀x. P(x))"
then show "∃x. ¬P(x)" by (rule ejemplo_5_1a)
next
assume "∃x. ¬P(x)"
then show "¬(∀x. P(x))" by (rule ejemplo_5_2a)
qed
― ‹La demostración automática es›
lemma ejemplo_5_3b:
"(¬(∀x. P(x))) ⟷ (∃x. ¬P(x))"
by auto
text ‹
Ejemplo 6.1 (p. 18). Demostrar
∀x. P(x) ∧ Q(x) ⊢ (∀x. P(x)) ∧ (∀x. Q(x))›
― ‹La demostración detallada es›
lemma ejemplo_6_1a:
assumes "∀x. P(x) ∧ Q(x)"
shows "(∀x. P(x)) ∧ (∀x. Q(x))"
proof (rule conjI)
show "∀x. P(x)"
proof (rule allI)
fix a
have "P(a) ∧ Q(a)" using assms by (rule allE)
then show "P(a)" by (rule conjunct1)
qed
next
show "∀x. Q(x)"
proof (rule allI)
fix a
have "P(a) ∧ Q(a)" using assms by (rule allE)
then show "Q(a)" by (rule conjunct2)
qed
qed
― ‹La demostración estructurada es›
lemma ejemplo_6_1b:
assumes "∀x. P(x) ∧ Q(x)"
shows "(∀x. P(x)) ∧ (∀x. Q(x))"
proof
show "∀x. P(x)"
proof
fix a
have "P(a) ∧ Q(a)" using assms ..
then show "P(a)" ..
qed
next
show "∀x. Q(x)"
proof
fix a
have "P(a) ∧ Q(a)" using assms ..
then show "Q(a)" ..
qed
qed
― ‹La demostración automática es›
lemma ejemplo_6_1c:
assumes "∀x. P(x) ∧ Q(x)"
shows "(∀x. P(x)) ∧ (∀x. Q(x))"
using assms
by auto
text ‹
Ejemplo 6.2 (p. 19). Demostrar
(∀x. P(x)) ∧ (∀x. Q(x)) ⊢ ∀x. P(x) ∧ Q(x)›
― ‹La demostración detallada es›
lemma ejemplo_6_2a:
assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
shows "∀x. P(x) ∧ Q(x)"
proof (rule allI)
fix a
have "∀x. P(x)" using assms by (rule conjunct1)
then have "P(a)" by (rule allE)
have "∀x. Q(x)" using assms by (rule conjunct2)
then have "Q(a)" by (rule allE)
with ‹P(a)› show "P(a) ∧ Q(a)" by (rule conjI)
qed
― ‹La demostración estructurada es›
lemma ejemplo_6_2b:
assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
shows "∀x. P(x) ∧ Q(x)"
proof
fix a
have "∀x. P(x)" using assms ..
then have "P(a)" by (rule allE)
have "∀x. Q(x)" using assms ..
then have "Q(a)" ..
with ‹P(a)› show "P(a) ∧ Q(a)" ..
qed
― ‹La demostración automática es›
lemma ejemplo_6_2c:
assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
shows "∀x. P(x) ∧ Q(x)"
using assms
by auto
text ‹
Ejemplo 6.3 (p. 20). Demostrar
⊢ ∀x. P(x) ∧ Q(x) ⟷ (∀x. P(x)) ∧ (∀x. Q(x))›
― ‹La demostración detallada es›
lemma ejemplo_6_3a:
"(∀x. P(x) ∧ Q(x)) ⟷ ((∀x. P(x)) ∧ (∀x. Q(x)))"
proof (rule iffI)
assume "∀x. P(x) ∧ Q(x)"
then show "(∀x. P(x)) ∧ (∀x. Q(x))" by (rule ejemplo_6_1a)
next
assume "(∀x. P(x)) ∧ (∀x. Q(x))"
then show "∀x. P(x) ∧ Q(x)" by (rule ejemplo_6_2a)
qed
text ‹
Ejemplo 7.1 (p. 21). Demostrar
(∃x. P(x)) ∨ (∃x. Q(x)) ⊢ ∃x. P(x) ∨ Q(x)›
― ‹La demostración detallada es›
lemma ejemplo_7_1a:
assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
shows "∃x. P(x) ∨ Q(x)"
using assms
proof (rule disjE)
assume "∃x. P(x)"
then obtain a where "P(a)" by (rule exE)
then have "P(a) ∨ Q(a)" by (rule disjI1)
then show "∃x. P(x) ∨ Q(x)" by (rule exI)
next
assume "∃x. Q(x)"
then obtain a where "Q(a)" by (rule exE)
then have "P(a) ∨ Q(a)" by (rule disjI2)
then show "∃x. P(x) ∨ Q(x)" by (rule exI)
qed
― ‹La demostración estructurada es›
lemma ejemplo_7_1b:
assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
shows "∃x. P(x) ∨ Q(x)"
using assms
proof
assume "∃x. P(x)"
then obtain a where "P(a)" ..
then have "P(a) ∨ Q(a)" ..
then show "∃x. P(x) ∨ Q(x)" ..
next
assume "∃x. Q(x)"
then obtain a where "Q(a)" ..
then have "P(a) ∨ Q(a)" ..
then show "∃x. P(x) ∨ Q(x)" ..
qed
― ‹La demostración automática es›
lemma ejemplo_7_1c:
assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
shows "∃x. P(x) ∨ Q(x)"
using assms
by auto
text ‹
Ejemplo 7.2 (p. 22). Demostrar
∃x. P(x) ∨ Q(x) ⊢ (∃x. P(x)) ∨ (∃x. Q(x))›
― ‹La demostración detallada es›
lemma ejemplo_7_2a:
assumes "∃x. P(x) ∨ Q(x)"
shows "(∃x. P(x)) ∨ (∃x. Q(x))"
proof -
obtain a where "P(a) ∨ Q(a)" using assms by (rule exE)
then show "(∃x. P(x)) ∨ (∃x. Q(x))"
proof (rule disjE)
assume "P(a)"
then have "∃x. P(x)" by (rule exI)
then show "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI1)
next
assume "Q(a)"
then have "∃x. Q(x)" by (rule exI)
then show "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI2)
qed
qed
― ‹La demostración estructurada es›
lemma ejercicio_7_2b:
assumes "∃x. P(x) ∨ Q(x)"
shows "(∃x. P(x)) ∨ (∃x. Q(x))"
proof -
obtain a where "P(a) ∨ Q(a)" using assms ..
then show "(∃x. P(x)) ∨ (∃x. Q(x))"
proof
assume "P(a)"
then have "∃x. P(x)" ..
then show "(∃x. P(x)) ∨ (∃x. Q(x))" ..
next
assume "Q(a)"
then have "∃x. Q(x)" ..
then show "(∃x. P(x)) ∨ (∃x. Q(x))" ..
qed
qed
― ‹La demostración automática es›
lemma ejercicio_7_2c:
assumes "∃x. P(x) ∨ Q(x)"
shows "(∃x. P(x)) ∨ (∃x. Q(x))"
using assms
by auto
text ‹
Ejemplo 7.3 (p. 23). Demostrar
⊢ ((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))›
― ‹La demostración detallada es›
lemma ejemplo_7_3a:
"((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))"
proof (rule iffI)
assume "(∃x. P(x)) ∨ (∃x. Q(x))"
then show "∃x. P(x) ∨ Q(x)" by (rule ejemplo_7_1a)
next
assume "∃x. P(x) ∨ Q(x)"
then show "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule ejemplo_7_2a)
qed
― ‹La demostración automática es›
lemma ejemplo_7_3b:
"((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))"
using assms
by auto
text ‹
Ejemplo 8.1 (p. 24). Demostrar
∃x y. P(x,y) ⊢ ∃y x. P(x,y)›
― ‹La demostración detallada es›
lemma ejemplo_8_1a:
assumes "∃x y. P(x,y)"
shows "∃y x. P(x,y)"
proof -
obtain a where "∃y. P(a,y)" using assms by (rule exE)
then obtain b where "P(a,b)" by (rule exE)
then have "∃x. P(x,b)" by (rule exI)
then show "∃y x. P(x,y)" by (rule exI)
qed
― ‹La demostración estructurada es›
lemma ejemplo_8_1b:
assumes "∃x y. P(x,y)"
shows "∃y x. P(x,y)"
proof -
obtain a where "∃y. P(a,y)" using assms ..
then obtain b where "P(a,b)" ..
then have "∃x. P(x,b)" ..
then show "∃y x. P(x,y)" ..
qed
― ‹La demostración automática es›
lemma ejemplo_8_1c:
assumes "∃x y. P(x,y)"
shows "∃y x. P(x,y)"
using assms
by auto
text ‹
Ejemplo 8.2. Demostrar
∃y x. P(x,y) ⊢ ∃x y. P(x,y)›
― ‹La demostración detallada es›
lemma ejemplo_8_2a:
assumes "∃y x. P(x,y)"
shows "∃x y. P(x,y)"
proof -
obtain b where "∃x. P(x,b)" using assms by (rule exE)
then obtain a where "P(a,b)" by (rule exE)
then have "∃y. P(a,y)" by (rule exI)
then show "∃x y. P(x,y)" by (rule exI)
qed
― ‹La demostración estructurada es›
lemma ejemplo_8_2b:
assumes "∃y x. P(x,y)"
shows "∃x y. P(x,y)"
proof -
obtain b where "∃x. P(x,b)" using assms ..
then obtain a where "P(a,b)" ..
then have "∃y. P(a,y)" ..
then show "∃x y. P(x,y)" ..
qed
― ‹La demostración estructurada es›
lemma ejemplo_8_2c:
assumes "∃y x. P(x,y)"
shows "∃x y. P(x,y)"
using assms
by auto
text ‹
Ejemplo 8.3 (p. 25). Demostrar
⊢ (∃x y. P(x,y)) ⟷ (∃y x. P(x,y))›
― ‹La demostración detallada es›
lemma ejemplo_8_3a:
"(∃x y. P(x,y)) ⟷ (∃y x. P(x,y))"
proof (rule iffI)
assume "∃x y. P(x,y)"
then show "∃y x. P(x,y)" by (rule ejemplo_8_1a)
next
assume "∃y x. P(x,y)"
then show "∃x y. P(x,y)" by (rule ejemplo_8_2a)
qed
― ‹La demostración automática es›
lemma ejemplo_8_3b:
"(∃x y. P(x,y)) ⟷ (∃y x. P(x,y))"
by auto
section ‹Reglas de la igualdad›
text ‹
Las reglas básicas de la igualdad son:
· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
›
text ‹
Ejemplo 9 (p. 27). Demostrar
x + 1 = 1 + x, x + 1 > 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
