chapter {* R6: Deducción natural en lógica de primer orden *}
theory R6
imports Main
begin
text {*
Demostrar o refutar los siguientes lemas usando sólo 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
· 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
· 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⟧ ⟹ a: = 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
*}
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
text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
∀x. P x ⟶ Q x ⊢ (∀x. P x) ⟶ (∀x. Q x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_1a:
"∀x. P x ⟶ Q x ⟹ (∀x. P x) ⟶ (∀x. Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_1b:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof
assume "∀x. P x"
show "∀x. Q x"
proof
fix a
have "P a" using `∀x. P x` ..
have "P a ⟶ Q a" using assms(1) ..
thus "Q a" using `P a` ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_1c:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof (rule impI)
assume "∀x. P x"
show "∀x. Q x"
proof (rule allI)
fix a
have "P a" using `∀x. P x` by (rule allE)
have "P a ⟶ Q a" using assms(1) by (rule allE)
thus "Q a" using `P a` by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
∃x. ¬(P x) ⊢ ¬(∀x. P x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_2a: "∃x. ¬(P x) ⟹ ¬(∀x. P x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_2b:
assumes "∃x. ¬(P x)"
shows "¬(∀x. P x)"
proof
assume "∀x. P x"
obtain a where "¬(P a)" using assms(1) ..
have "P a" using `∀x. P x` ..
with `¬(P a)` show False ..
qed
― ‹La demostración detallada es›
lemma ejercicio_2c:
assumes "∃x. ¬(P x)"
shows "¬(∀x. P x)"
proof (rule notI)
assume "∀x. P x"
obtain a where "¬(P a)" using assms(1) by (rule exE)
have "P a" using `∀x. P x` by (rule allE)
with `¬(P a)` show False by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
∀x. P x ⊢ ∀y. P y
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_3a: "∀x. P x ⟹ ∀y. P y"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_3b:
assumes "∀x. P x"
shows "∀y. P y"
proof
fix a
show "P a" using assms ..
qed
― ‹La demostración estructurada es›
lemma ejercicio_3c:
assumes "∀x. P x"
shows "∀y. P y"
proof (rule allI)
fix a
show "P a" using assms by (rule allE)
qed
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
∀x. P x ⟶ Q x ⊢ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_4a:
"∀x. P x ⟶ Q x ⟹ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_4b:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof
assume "∀x. ¬(Q x)"
show "∀x. ¬(P x)"
proof
fix a
show "¬(P a)"
proof
assume "P a"
have "P a ⟶ Q a" using assms ..
hence "Q a" using `P a` ..
have "¬(Q a)" using `∀x. ¬(Q x)` ..
thus False using `Q a` ..
qed
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_4c:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof (rule impI)
assume "∀x. ¬(Q x)"
show "∀x. ¬(P x)"
proof (rule allI)
fix a
show "¬(P a)"
proof
assume "P a"
have "P a ⟶ Q a" using assms by (rule allE)
hence "Q a" using `P a` by (rule mp)
have "¬(Q a)" using `∀x. ¬(Q x)` by (rule allE)
thus False using `Q a` by (rule notE)
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
∀x. P x ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_5a:
"∀x. P x ⟶ ¬(Q x) ⟹ ¬(∃x. P x ∧ Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_5b:
assumes "∀x. P x ⟶ ¬(Q x)"
shows "¬(∃x. P x ∧ Q x)"
proof
assume "∃x. P x ∧ Q x"
then obtain a where "P a ∧ Q a" ..
hence "P a" ..
have "P a ⟶ ¬(Q a)" using assms ..
hence "¬(Q a)" using `P a` ..
have "Q a" using `P a ∧ Q a` ..
with `¬(Q a)` show False ..
qed
― ‹La demostración estructurada es›
lemma ejercicio_5c:
assumes "∀x. P x ⟶ ¬(Q x)"
shows "¬(∃x. P x ∧ Q x)"
proof (rule notI)
assume "∃x. P x ∧ Q x"
then obtain a where "P a ∧ Q a" by (rule exE)
hence "P a" by (rule conjunct1)
have "P a ⟶ ¬(Q a)" using assms by (rule allE)
hence "¬(Q a)" using `P a` by (rule mp)
have "Q a" using `P a ∧ Q a` by (rule conjunct2)
with `¬(Q a)` show False by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
∀x y. P x y ⊢ ∀u v. P u v
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_6a:
"∀x y. P x y ⟹ ∀u v. P u v"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_6b:
assumes "∀x y. P x y"
shows "∀u v. P u v"
proof
fix a
show "∀v. P a v"
proof
fix b
have "∀y. P a y" using assms ..
thus "P a b" ..
qed
qed
― ‹La demostración estructurada simplificada es›
lemma ejercicio_6b2:
assumes "∀x y. P x y"
shows "∀u v. P u v"
proof (rule allI)+
fix a b
have "∀y. P a y" using assms ..
thus "P a b" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_6c:
assumes "∀x y. P x y"
shows "∀u v. P u v"
proof (rule allI)+
fix a b
have "∀y. P a y" using assms by (rule allE)
thus "P a b" by (rule allE)
qed
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
∃x y. P x y ⟹ ∃u v. P u v
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_7a:
"∃x y. P x y ⟹ ∃u v. P u v"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_7b:
assumes "∃x y. P x y"
shows "∃u v. P u v"
proof -
obtain a where "∃y. P a y" using assms ..
then obtain b where "P a b" ..
hence "∃v. P a v" ..
thus "∃u v. P u v" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_8a:
"∃x. ∀y. P x y ⟹ ∀y. ∃x. P x y"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_8b:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
proof
fix b
obtain a where "∀y. P a y" using assms ..
hence "P a b" ..
thus "∃x. P x b" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_8c:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
proof (rule allI)
fix b
obtain a where "∀y. P a y" using assms by (rule exE)
hence "P a b" by (rule allE)
thus "∃x. P x b" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
∃x. P a ⟶ Q x ⊢ P a ⟶ (∃x. Q x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_9a:
"∃x. P a ⟶ Q x ⟹ P a ⟶ (∃x. Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_9b:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
proof
assume "P a"
obtain b where "P a ⟶ Q b" using assms ..
hence "Q b" using `P a` ..
thus "∃x. Q x" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_9c:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
proof (rule impI)
assume "P a"
obtain b where "P a ⟶ Q b" using assms by (rule exE)
hence "Q b" using `P a` by (rule mp)
thus "∃x. Q x" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_10a:
"P a ⟶ (∃x. Q x) ⟹ ∃x. P a ⟶ Q x"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_10b:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof -
have "¬(P a) ∨ P a" ..
thus "∃x. P a ⟶ Q x"
proof
assume "¬(P a)"
have "P a ⟶ Q a"
proof
assume "P a"
with `¬(P a)` show "Q a" ..
qed
thus "∃x. P a ⟶ Q x" ..
next
assume "P a"
with assms have "∃x. Q x" by (rule mp)
then obtain b where "Q b" ..
have "P a ⟶ Q b"
proof
assume "P a"
note `Q b`
thus "Q b" .
qed
thus "∃x. P a ⟶ Q x" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_10c:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof -
have "¬(P a) ∨ P a" by (rule excluded_middle)
thus "∃x. P a ⟶ Q x"
proof (rule disjE)
assume "¬(P a)"
have "P a ⟶ Q a"
proof (rule impI)
assume "P a"
with `¬(P a)` show "Q a" by (rule notE)
qed
thus "∃x. P a ⟶ Q x" by (rule exI)
next
assume "P a"
with assms have "∃x. Q x" by (rule mp)
then obtain b where "Q b" by (rule exE)
have "P a ⟶ Q b"
proof (rule impI)
assume "P a"
note `Q b`
thus "Q b" by this
qed
thus "∃x. P a ⟶ Q x" by (rule exI)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
(∃x. P x) ⟶ Q a ⊢ ∀x. P x ⟶ Q a
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_11a:
"(∃x. P x) ⟶ Q a ⟹ ∀x. P x ⟶ Q a"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_11b:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
proof
fix b
show "P b ⟶ Q a"
proof
assume "P b"
hence "∃x. P x" ..
with assms show "Q a" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_11c:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
proof (rule allI)
fix b
show "P b ⟶ Q a"
proof (rule impI)
assume "P b"
hence "∃x. P x" by (rule exI)
with assms show "Q a" by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
∀x. P x ⟶ Q a ⊢ ∃ x. P x ⟶ Q a
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_12a:
"∀x. P x ⟶ Q a ⟹ ∃x. P x ⟶ Q a"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_12b:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
proof -
have "P b ⟶ Q a" using assms ..
thus "∃x. P x ⟶ Q a" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_12c:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
proof -
have "P b ⟶ Q a" using assms by (rule allE)
thus "∃x. P x ⟶ Q a" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
(∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_13a:
"(∀x. P x) ∨ (∀x. Q x) ⟹ ∀x. P x ∨ Q x"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_13b:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
proof
fix a
note assms
thus "P a ∨ Q a"
proof
assume "∀x. P x"
hence "P a" ..
thus "P a ∨ Q a" ..
next
assume "∀x. Q x"
hence "Q a" ..
thus "P a ∨ Q a" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_13c:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
proof (rule allI)
fix a
note assms
thus "P a ∨ Q a"
proof (rule disjE)
assume "∀x. P x"
hence "P a" by (rule allE)
thus "P a ∨ Q a" by (rule disjI1)
next
assume "∀x. Q x"
hence "Q a" by (rule allE)
thus "P a ∨ Q a" by (rule disjI2)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_14a:
"∃x. P x ∧ Q x ⟹ (∃x. P x) ∧ (∃x. Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_14b:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
proof
obtain a where "P a ∧ Q a" using assms ..
hence "P a" ..
thus "∃x. P x" ..
next
obtain a where "P a ∧ Q a" using assms ..
hence "Q a" ..
thus "∃x. Q x" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_14c:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
proof (rule conjI)
obtain a where "P a ∧ Q a" using assms by (rule exE)
hence "P a" by (rule conjunct1)
thus "∃x. P x" by (rule exI)
next
obtain a where "P a ∧ Q a" using assms by (rule exE)
hence "Q a" by (rule conjunct2)
thus "∃x. Q x" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
∀x y. P y ⟶ Q x ⊢ (∃y. P y) ⟶ (∀x. Q x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_15a:
"∀x y. P y ⟶ Q x ⟹ (∃y. P y) ⟶ (∀x. Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_15b:
assumes "∀x y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
proof
assume "∃y. P y"
then obtain b where "P b" ..
show "∀x. Q x"
proof
fix a
have "∀y. P y ⟶ Q a" using assms ..
hence "P b ⟶ Q a" ..
thus "Q a" using `P b` ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_15c:
assumes "∀x y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
proof (rule impI)
assume "∃y. P y"
then obtain b where "P b" by (rule exE)
show "∀x. Q x"
proof (rule allI)
fix a
have "∀y. P y ⟶ Q a" using assms by (rule allE)
hence "P b ⟶ Q a" by (rule allE)
thus "Q a" using `P b` by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
¬(∀x. ¬(P x)) ⊢ ∃x. P x
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_16a:
"¬(∀x. ¬(P x)) ⟹ ∃x. P x"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_16b:
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
assume "P a"
hence "∃x. P x" ..
with `¬(∃x. P x)` show False ..
qed
qed
with assms show False ..
qed
― ‹La demostración detallada es›
lemma ejercicio_16c:
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
assume "P a"
hence "∃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
text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
∀x. ¬(P x) ⊢ ¬(∃x. P x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_17a:
"∀x. ¬(P x) ⟹ ¬(∃x. P x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_17b:
assumes "∀x. ¬(P x)"
shows "¬(∃x. P x)"
proof
assume "∃x. P x"
then obtain a where "P a" ..
have "¬(P a)" using assms ..
thus False using `P a` ..
qed
― ‹La demostración detallada es›
lemma ejercicio_17c:
assumes "∀x. ¬(P x)"
shows "¬(∃x. P x)"
proof (rule notI)
assume "∃x. P x"
then obtain a where "P a" by (rule exE)
have "¬(P a)" using assms by (rule allE)
thus False using `P a` by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
∃x. P x ⊢ ¬(∀x. ¬(P x))
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_18a:
"∃x. P x ⟹ ¬(∀x. ¬(P x))"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_18b:
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)` ..
thus False using `P a` ..
qed
― ‹La demostración detallada es›
lemma ejercicio_18c:
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)
thus False using `P a` by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
P a ⟶ (∀x. Q x) ⊢ ∀x. P a ⟶ Q x
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_19a:
"P a ⟶ (∀x. Q x) ⟹ ∀x. P a ⟶ Q x"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_19b:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
proof
fix b
show "P a ⟶ Q b"
proof
assume "P a"
with assms have "∀x. Q x" ..
thus "Q b" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_19c:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
proof (rule allI)
fix b
show "P a ⟶ Q b"
proof (rule impI)
assume "P a"
with assms have "∀x. Q x" by (rule mp)
thus "Q b" by (rule allE)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
{∀x y z. R x y ∧ R y z ⟶ R x z,
∀x. ¬(R x x)}
⊢ ∀x y. R x y ⟶ ¬(R y x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_20a:
"⟦∀x y z. R x y ∧ R y z ⟶ R x z; ∀x. ¬(R x x)⟧ ⟹ ∀x y. R x y ⟶ ¬(R y x)"
by metis
― ‹La demostración estructurada es›
lemma ejercicio_20b:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof (rule allI)+
fix a b
show "R a b ⟶ ¬(R b a)"
proof
assume "R a b"
show "¬(R b a)"
proof
assume "R b a"
show False
proof -
have "R a b ∧ R b a" using `R a b` `R b a` ..
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) ..
hence "∀z. R a b ∧ R b z ⟶ R a z" ..
hence "R a b ∧ R b a ⟶ R a a" ..
hence "R a a" using `R a b ∧ R b a` ..
have "¬(R a a)" using assms(2) ..
thus False using `R a a` ..
qed
qed
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_20c:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof (rule allI)+
fix a b
show "R a b ⟶ ¬(R b a)"
proof (rule impI)
assume "R a b"
show "¬(R b a)"
proof (rule notI)
assume "R b a"
show False
proof -
have "R a b ∧ R b a" using `R a b` `R b a` by (rule conjI)
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
hence "R a b ∧ R b a ⟶ R a a" by (rule allE)
hence "R a a" using `R a b ∧ R b a` by (rule mp)
have "¬(R a a)" using assms(2) by (rule allE)
thus False using `R a a` by (rule notE)
qed
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
{∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_21a:
"⟦∀x. P x ∨ Q x; ∃x. ¬(Q x); ∀x. R x ⟶ ¬(P x)⟧ ⟹ ∃x. ¬(R x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_21b:
assumes "∀x. P x ∨ Q x"
"∃x. ¬(Q x)"
"∀x. R x ⟶ ¬(P x)"
shows "∃x. ¬(R x)"
proof -
obtain a where "¬(Q a)" using assms(2) ..
have "P a ∨ Q a" using assms(1) ..
hence "P a"
proof
assume "P a"
thus "P a" .
next
assume "Q a"
with `¬(Q a)` show "P a" ..
qed
hence "¬¬(P a)" by (rule notnotI)
have "R a ⟶ ¬(P a)" using assms(3) ..
hence "¬(R a)" using `¬¬(P a)` by (rule mt)
thus "∃x. ¬(R x)" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_21c:
assumes "∀x. P x ∨ Q x"
"∃x. ¬(Q x)"
"∀x. R x ⟶ ¬(P x)"
shows "∃x. ¬(R x)"
proof -
obtain a where "¬(Q a)" using assms(2) by (rule exE)
have "P a ∨ Q a" using assms(1) by (rule allE)
hence "P a"
proof (rule disjE)
assume "P a"
thus "P a" by this
next
assume "Q a"
with `¬(Q a)` show "P a" by (rule notE)
qed
hence "¬¬(P a)" by (rule notnotI)
have "R a ⟶ ¬(P a)" using assms(3) by (rule allE)
hence "¬(R a)" using `¬¬(P a)` by (rule mt)
thus "∃x. ¬(R x)" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
{∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_22a:
"⟦∀x. P x ⟶ Q x ∨ R x; ¬(∃x. P x ∧ R x)⟧ ⟹ ∀x. P x ⟶ Q x"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_22b:
assumes "∀x. P x ⟶ Q x ∨ R x"
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
proof
fix a
show "P a ⟶ Q a"
proof
assume "P a"
have "P a ⟶ Q a ∨ R a" using assms(1) ..
hence "Q a ∨ R a" using `P a` ..
thus "Q a"
proof
assume "Q a"
thus "Q a" .
next
assume "R a"
with `P a` have "P a ∧ R a" ..
hence "∃x. P x ∧ R x" ..
with assms(2) show "Q a" ..
qed
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_22c:
assumes "∀x. P x ⟶ Q x ∨ R x"
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
proof (rule allI)
fix a
show "P a ⟶ Q a"
proof (rule impI)
assume "P a"
have "P a ⟶ Q a ∨ R a" using assms(1) by (rule allE)
hence "Q a ∨ R a" using `P a` by (rule mp)
thus "Q a"
proof (rule disjE)
assume "Q a"
thus "Q a" by this
next
assume "R a"
with `P a` have "P a ∧ R a" by (rule conjI)
hence "∃x. P x ∧ R x" by (rule exI)
with assms(2) show "Q a" by (rule notE)
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_23a:
"∃x y. R x y ∨ R y x ⟹ ∃x y. R x y"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_23b:
assumes "∃x y. R x y ∨ R y x"
shows "∃x y. R x y"
proof -
obtain a where "∃y. R a y ∨ R y a" using assms ..
then obtain b where "R a b ∨ R b a" ..
thus "∃x y. R x y"
proof
assume "R a b"
hence "∃y. R a y" ..
thus "∃ x y. R x y" ..
next
assume "R b a"
hence "∃y. R b y" ..
thus "∃ x y. R x y" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_23c:
assumes "∃x y. R x y ∨ R y x"
shows "∃x y. R x y"
proof -
obtain a where "∃y. R a y ∨ R y a" using assms by (rule exE)
then obtain b where "R a b ∨ R b a" by (rule exE)
thus "∃x y. R x y"
proof (rule disjE)
assume "R a b"
hence "∃y. R a y" by (rule exI)
thus "∃ x y. R x y" by (rule exI)
next
assume "R b a"
hence "∃y. R b y" by (rule exI)
thus "∃ x y. R x y" by (rule exI)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_24a: "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_24b: "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof
assume "∃x. ∀y. P x y"
then obtain a where "∀y. P a y" ..
show "∀y. ∃x. P x y"
proof
fix b
have "P a b" using `∀y. P a y` ..
thus "∃x. P x b" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_24c: "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof (rule impI)
assume "∃x. ∀y. P x y"
then obtain a where "∀y. P a y" by (rule exE)
show "∀y. ∃x. P x y"
proof (rule allI)
fix b
have "P a b" using `∀y. P a y` by (rule allE)
thus "∃x. P x b" by (rule exI)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_25a: "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_25b: "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
proof
assume "∀x. P x ⟶ Q"
show "(∃x. P x) ⟶ Q"
proof
assume "∃x. P x"
then obtain a where "P a" ..
have "P a ⟶ Q" using `∀x. P x ⟶ Q` ..
thus "Q" using `P a` ..
qed
next
assume "(∃x. P x) ⟶ Q"
show "∀x. P x ⟶ Q"
proof
fix b
show "P b ⟶ Q"
proof
assume "P b"
hence "∃x. P x" ..
with `(∃x. P x) ⟶ Q` show "Q" ..
qed
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_25c: "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
proof (rule iffI)
assume "∀x. P x ⟶ Q"
show "(∃x. P x) ⟶ Q"
proof (rule impI)
assume "∃x. P x"
then obtain a where "P a" by (rule exE)
have "P a ⟶ Q" using `∀x. P x ⟶ Q` by (rule allE)
thus "Q" using `P a` by (rule mp)
qed
next
assume "(∃x. P x) ⟶ Q"
show "∀x. P x ⟶ Q"
proof (rule allI)
fix b
show "P b ⟶ Q"
proof (rule impI)
assume "P b"
hence "∃x. P x" by (rule exI)
with `(∃x. P x) ⟶ Q` show "Q" by (rule mp)
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_26a: "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_26b: "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
proof
assume "(∀x. P x) ∧ (∀x. Q x)"
show "∀x. P x ∧ Q x"
proof
fix a
have "∀x. P x" using `(∀x. P x) ∧ (∀x. Q x)` ..
have "∀x. Q x" using `(∀x. P x) ∧ (∀x. Q x)` ..
hence "Q a" ..
have "P a" using `∀x. P x` ..
thus "P a ∧ Q a" using `Q a` ..
qed
next
assume "∀x. P x ∧ Q x"
have "∀x. P x"
proof
fix a
have "P a ∧ Q a" using `∀x. P x ∧ Q x` ..
thus "P a" ..
qed
moreover have "∀x. Q x"
proof
fix a
have "P a ∧ Q a" using `∀x. P x ∧ Q x` ..
thus "Q a" ..
qed
ultimately show "(∀x. P x) ∧ (∀x. Q x)" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_26c: "((∀x. P x) ∧ (∀x. Q x)) = (∀x. P x ∧ Q x)"
proof (rule iffI)
assume "(∀x. P x) ∧ (∀x. Q x)"
show "∀x. P x ∧ Q x"
proof (rule allI)
fix a
have "∀x. P x" using `(∀x. P x) ∧ (∀x. Q x)` by (rule conjunct1)
have "∀x. Q x" using `(∀x. P x) ∧ (∀x. Q x)` by (rule conjunct2)
hence "Q a" by (rule allE)
have "P a" using `∀x. P x` by (rule allE)
thus "P a ∧ Q a" using `Q a` by (rule conjI)
qed
next
assume "∀x. P x ∧ Q x"
have "∀x. P x"
proof (rule allI)
fix a
have "P a ∧ Q a" using `∀x. P x ∧ Q x` by (rule allE)
thus "P a" by (rule conjunct1)
qed
moreover have "∀x. Q x"
proof (rule allI)
fix a
have "P a ∧ Q a" using `∀x. P x ∧ Q x` by (rule allE)
thus "Q a" by (rule conjunct2)
qed
ultimately show "(∀x. P x) ∧ (∀x. Q x)" by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar o refutar
((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)
------------------------------------------------------------------ *}
lemma ejercicio_27: "((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
oops
(*
Auto Quickcheck found a counterexample:
P = {a\<^isub>1}
Q = {a\<^isub>2}
*)
text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar o refutar
((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_28a:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_28b:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
proof
assume "(∃x. P x) ∨ (∃x. Q x)"
thus "∃x. P x ∨ Q x"
proof
assume "∃x. P x"
then obtain a where "P a" ..
hence "P a ∨ Q a" ..
thus "∃x. P x ∨ Q x" ..
next
assume "∃x. Q x"
then obtain a where "Q a" ..
hence "P a ∨ Q a" ..
thus "∃x. P x ∨ Q x" ..
qed
next
assume "∃x. P x ∨ Q x"
then obtain a where "P a ∨ Q a" ..
thus "(∃x. P x) ∨ (∃x. Q x)"
proof
assume "P a"
hence "∃x. P x" ..
thus "(∃x. P x) ∨ (∃x. Q x)" ..
next
assume "Q a"
hence "∃x. Q x" ..
thus "(∃x. P x) ∨ (∃x. Q x)" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_28c:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
proof (rule iffI)
assume "(∃x. P x) ∨ (∃x. Q x)"
thus "∃x. P x ∨ Q x"
proof (rule disjE)
assume "∃x. P x"
then obtain a where "P a" by (rule exE)
hence "P a ∨ Q a" by (rule disjI1)
thus "∃x. P x ∨ Q x" by (rule exI)
next
assume "∃x. Q x"
then obtain a where "Q a" by (rule exE)
hence "P a ∨ Q a" by (rule disjI2)
thus "∃x. P x ∨ Q x" by (rule exI)
qed
next
assume "∃x. P x ∨ Q x"
then obtain a where "P a ∨ Q a" by (rule exE)
thus "(∃x. P x) ∨ (∃x. Q x)"
proof (rule disjE)
assume "P a"
hence "∃x. P x" by (rule exI)
thus "(∃x. P x) ∨ (∃x. Q x)" by (rule disjI1)
next
assume "Q a"
hence "∃x. Q x" by (rule exI)
thus "(∃x. P x) ∨ (∃x. Q x)" by (rule disjI2)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar o refutar
(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
------------------------------------------------------------------ *}
lemma ejercicio_29:
"(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
quickcheck
(*
Quickcheck found a counterexample:
P = (λx. undefined)(a\<^isub> := {b}, b := {a})
*)
oops
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar o refutar
(¬(∀x. P x)) ⟷ (∃x. ¬P x)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_30a:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_30b:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof
assume "¬(∀x. P x)"
show "∃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"
hence "∃x. ¬P x" ..
with `¬(∃x. ¬P x)` show False ..
qed
qed
with `¬(∀x. P x)` show False ..
qed
next
assume "∃x. ¬P x"
then obtain a where "¬P a" ..
show "¬(∀x. P x)"
proof
assume "∀x. P x"
hence "P a" ..
with `¬P a` show False ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_30c:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof (rule iffI)
assume "¬(∀x. P x)"
show "∃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"
hence "∃x. ¬P x" by (rule exI)
with `¬(∃x. ¬P x)` show False by (rule notE)
qed
qed
with `¬(∀x. P x)` show False by (rule notE)
qed
next
assume "∃x. ¬P x"
then obtain a where "¬P a" by (rule exE)
show "¬(∀x. P x)"
proof (rule notI)
assume "∀x. P x"
hence "P a" by (rule allE)
show False using `¬P a` `P a` by (rule notE)
qed
qed
section {* Ejercicios sobre igualdad *}
text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar o refutar
P a ⟹ ∀x. x = a ⟶ P x
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_31a:
"P a ⟹ ∀x. x = a ⟶ P x"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_31b:
assumes "P a"
shows "∀x. x = a ⟶ P x"
proof
fix b
show "b = a ⟶ P b"
proof
assume "b = a"
thus "P b" using assms by (rule ssubst)
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_31c:
assumes "P a"
shows "∀x. x = a ⟶ P x"
proof (rule allI)
fix b
show "b = a ⟶ P b"
proof (rule impI)
assume "b = a"
thus "P b" using assms by (rule ssubst)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar o refutar
∃x y. R x y ∨ R y x; ¬(∃x. R x x)⟧ ⟹ ∃x y. x ≠ y
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_32a:
fixes R :: "'c ⇒ 'c ⇒ bool"
assumes "∃x y. R x y ∨ R y x"
"¬(∃x. R x x)"
shows "∃(x::'c) y. x ≠ y"
using assms
by metis
― ‹La demostración estructurada es›
lemma ejercicio_32b:
fixes R :: "'c ⇒ 'c ⇒ bool"
assumes "∃x y. R x y ∨ R y x"
"¬(∃x. R x x)"
shows "∃(x::'c) y. x ≠ y"
proof -
obtain a where "∃y. R a y ∨ R y a" using assms(1) ..
then obtain b where "R a b ∨ R b a" ..
hence "a ≠ b"
proof
assume "R a b"
show "a ≠ b"
proof
assume "a = b"
hence "R b b" using `R a b` by (rule subst)
hence "∃x. R x x" ..
with assms(2) show False ..
qed
next
assume "R b a"
show "a ≠ b"
proof
assume "a = b"
hence "R a a" using `R b a` by (rule ssubst)
hence "∃x. R x x" ..
with assms(2) show False ..
qed
qed
hence "∃y. a ≠ y" ..
thus "∃(x::'c) y. x ≠ y" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_32c:
fixes R :: "'c ⇒ 'c ⇒ bool"
assumes "∃x y. R x y ∨ R y x"
"¬(∃x. R x x)"
shows "∃(x::'c) y. x ≠ y"
proof -
obtain a where "∃y. R a y ∨ R y a" using assms(1) by (rule exE)
then obtain b where "R a b ∨ R b a" by (rule exE)
hence "a ≠ b"
proof (rule disjE)
assume "R a b"
show "a ≠ b"
proof (rule notI)
assume "a = b"
hence "R b b" using `R a b` by (rule subst)
hence "∃x. R x x" by (rule exI)
with assms(2) show False by (rule notE)
qed
next
assume "R b a"
show "a ≠ b"
proof (rule notI)
assume "a = b"
hence "R a a" using `R b a` by (rule ssubst)
hence "∃x. R x x" by (rule exI)
with assms(2) show False by (rule notE)
qed
qed
hence "∃y. a ≠ y" by (rule exI)
thus "∃(x::'c) y. x ≠ y" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)}
⊢ P (f a) a (f a)
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_33a:
"⟦∀x. P a x x; ∀x y z. P x y z ⟶ P (f x) y (f z)⟧ ⟹ P (f a) a (f a)"
by auto
― ‹La demostración estructura es›
lemma ejercicio_33b:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "P (f a) a (f a)"
proof -
have "P a a a" using assms(1) ..
have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) ..
hence "∀z. P a a z ⟶ P (f a) a (f z)" ..
hence "P a a a ⟶ P (f a) a (f a)" ..
thus "P (f a) a (f a)" using `P a a a` ..
qed
― ‹La demostración detallada es›
lemma ejercicio_33c:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "P (f a) a (f a)"
proof -
have "P a a a" using assms(1) by (rule allE)
have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
hence "∀z. P a a z ⟶ P (f a) a (f z)" by (rule allE)
hence "P a a a ⟶ P (f a) a (f a)" by (rule allE)
thus "P (f a) a (f a)" using `P a a a` by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)⟧
⊢ ∃z. P (f a) z (f (f a))
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_34a:
"⟦∀x. P a x x; ∀x y z. P x y z ⟶ P (f x) y (f z)⟧
⟹ ∃z. P (f a) z (f (f a))"
by metis
― ‹La demostración estructura es›
lemma ejercicio_34b:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
proof -
have "P a (f a) (f a)" using assms(1) ..
have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) ..
hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
hence "P (f a) (f a) (f (f a))" using `P a (f a) (f a)` ..
thus "∃z. P (f a) z (f (f a))" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_34c:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
proof -
have "P a (f a) (f a)" using assms(1) by (rule allE)
have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
hence "P (f a) (f a) (f (f a))" using `P a (f a) (f a)` by (rule mp)
thus "∃z. P (f a) z (f (f a))" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar o refutar
{∀y. Q a y,
∀x y. Q x y ⟶ Q (s x) (s y)}
⊢ ∃z. Qa z ∧ Q z (s (s a))
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_35a:
"⟦∀y. Q a y; ∀x y. Q x y ⟶ Q (s x) (s y)⟧ ⟹ ∃z. Q a z ∧ Q z (s (s a))"
by auto
― ‹La demostración estructura es›
lemma ejercicio_35b:
assumes "∀y. Q a y"
"∀x y. Q x y ⟶ Q (s x) (s y)"
shows "∃z. Q a z ∧ Q z (s (s a))"
proof -
have "Q a (s a)" using assms(1) ..
have "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) ..
hence "Q a (s a) ⟶ Q (s a) (s (s a))" ..
hence "Q (s a) (s (s a))" using `Q a (s a)` ..
with `Q a (s a)` have "Q a (s a) ∧ Q (s a) (s (s a))" ..
thus "∃z. Q a z ∧ Q z (s (s a))" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_35c:
assumes "∀y. Q a y"
"∀x y. Q x y ⟶ Q (s x) (s y)"
shows "∃z. Q a z ∧ Q z (s (s a))"
proof -
have "Q a (s a)" using assms(1) by (rule allE)
have "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) by (rule allE)
hence "Q a (s a) ⟶ Q (s a) (s (s a))" by (rule allE)
hence "Q (s a) (s (s a))" using `Q a (s a)` by (rule mp)
with `Q a (s a)` have "Q a (s a) ∧ Q (s a) (s (s a))" by (rule conjI)
thus "∃z. Q a z ∧ Q z (s (s a))" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar o refutar
{x = f x, odd (f x)} ⊢ odd x
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_36a:
"⟦x = f x; odd (f x)⟧ ⟹ odd x"
by auto
― ‹La demostración semiautomática es›
lemma ejercicio_36b:
"⟦x = f x; odd (f x)⟧ ⟹ odd x"
by (rule ssubst)
― ‹La demostración estructurada es›
lemma ejercicio_36c:
assumes "x = f x"
"odd (f x)"
shows "odd x"
proof -
show "odd x" using assms by (rule ssubst)
qed
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar o refutar
{x = f x, triple (f x) (f x) x} ⊢ triple x x x
------------------------------------------------------------------ *}
― ‹La demostración automática es›
lemma ejercicio_37a:
"⟦x = f x; triple (f x) (f x) x⟧ ⟹ triple x x x"
by auto
― ‹La demostración semiautomática es›
lemma ejercicio_37b:
"⟦x = f x; triple (f x) (f x) x⟧ ⟹ triple x x x"
by (rule ssubst)
― ‹La demostración estructurada es›
lemma ejercicio_37c:
assumes "x = f x"
"triple (f x) (f x) x"
shows "triple x x x"
proof -
show "triple x x x" using assms by (rule ssubst)
qed
end
