header {* R7: Deducción natural en lógica de primer orden con Isabelle/HOL *}
theory R7
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)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_1:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof (rule impI)
assume 1:"∀x. P x"
{fix a
have 2:"P a ⟶ Q a" using assms..
have "P a" using 1..
with 2 have "Q a"..}
thus "∀x. Q x"..
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
∃x. ¬(P x) ⊢ ¬(∀x. P x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_2:
assumes "∃x. ¬(P x)"
shows "¬(∀x. P x)"
proof
assume 1:"(∀x. P x)"
obtain a where 2:"¬(P a)" using assms..
have "P a" using 1..
with 2 show False..
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
∀x. P x ⊢ ∀y. P y
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_3:
assumes "∀x. P x"
shows "∀y. P y"
using assms .
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
∀x. P x ⟶ Q x ⊢ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_4:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof
assume 1:"(∀x. ¬(Q x))"
{fix a
have 2:"P a ⟶ Q a" using assms..
have "¬(Q a)" using 1..
with 2 have "¬(P a)" by (rule mt)}
thus "∀x. ¬(P x)"..
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
∀x. P x ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_5:
assumes "∀x. P x ⟶ ¬(Q x)"
shows "¬(∃x. P x ∧ Q x)"
proof
assume "(∃x. P x ∧ Q x)"
then obtain a where 1: "P a ∧ Q a"..
hence 2:"P a"..
have 3:"Q a" using 1..
have "P a ⟶ ¬(Q a)" using assms..
hence "¬(Q a)" using 2..
thus False using 3..
qed
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
∀x y. P x y ⊢ ∀u v. P u v
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_6:
assumes "∀x y. P x y"
shows "∀u v. P u v"
using assms .
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
∃x y. P x y ⟹ ∃u v. P u v
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_7:
assumes "∃x y. P x y"
shows "∃u v. P u v"
using assms .
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_8:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
proof -
obtain a where 1: "∀y. P a y" using assms..
{fix b
have "P a b" using 1..
hence "∃x. P x b"..}
thus ?thesis ..
qed
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
∃x. P a ⟶ Q x ⊢ P a ⟶ (∃x. Q x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_9:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
proof
assume 1:"P a"
obtain b where 2: "P a⟶ Q b" using 0..
hence "Q b" using 1..
thus "∃x. Q x"..
qed
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_10:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof -
have "¬(P a)∨ P a"..
moreover
{assume "¬(P a)"
hence "P a ⟶ Q a" by (rule ejercicio_40f)
hence ?thesis..}
moreover
{assume "P a"
with assms have "∃x. Q x"..
then obtain b where "Q b"..
hence "P a ⟶ Q b"..
hence ?thesis..}
ultimately
show ?thesis..
qed
text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
(∃x. P x) ⟶ Q a ⊢ ∀x. P x ⟶ Q a
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_11:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
proof-
have "¬(Q a)∨ (Q a)"..
moreover
{assume 2: "¬(Q a)"
{fix b
have 3:"¬(∃x. P x)"using 1 2 by (rule mt)
have "¬(P b)"
proof
assume "P b"
hence "∃x. P x"..
with 3 show False..
qed
hence 3:"P b⟶ Q a" by (rule ejercicio_40f)}
hence ?thesis..}
moreover
{assume 2: "Q a"
{fix b
have "P b ⟶ Q a"using 2..}
hence ?thesis ..}
ultimately
show ?thesis..
qed
text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
∀x. P x ⟶ Q a ⊢ ∃ x. P x ⟶ Q a
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_12:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
proof-
fix w
have "P w ⟶ Q a"using assms..
thus "∃x. P x ⟶ Q a"..
qed
text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
(∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_13:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
proof-
note `(∀x. P x) ∨ (∀x. Q x)`
moreover
{assume 1:"∀x. P x"
{fix a
have "P a"using 1..
hence "P a ∨ Q a"..}
hence ?thesis..}
moreover
{assume 1:"∀x. Q x"
{fix a
have "Q a"using 1..
hence "P a ∨ Q a"..}
hence ?thesis..}
ultimately
show ?thesis..
qed
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_14:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
proof-
obtain a where 1: "P a ∧ Q a" using assms..
hence "P a"..
hence 2:"∃x. P x"..
have "Q a" using 1..
hence "∃x. Q x"..
with 2 show ?thesis..
qed
text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
∀x y. P y ⟶ Q x ⊢ (∃y. P y) ⟶ (∀x. Q x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_15:
assumes "∀x y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
proof
assume "(∃y. P y)"
then obtain a where 1: "P a"..
{fix b
have "∀x. P x ⟶ Q b" using 0..
hence "P a ⟶ Q b"..
hence "Q b" using 1..}
thus "∀x. Q x"..
qed
text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
¬(∀x. ¬(P x)) ⊢ ∃x. P x
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_16:
assumes "¬(∀x. ¬(P x))"
shows "∃x. P x"
proof (rule ccontr)
assume 1: "¬?thesis"
{fix a
have "¬P a ∨ P a"..
hence "P a ∨ ¬P a" by (rule ejercicio_27)
have "¬ P a ∨ ?thesis"
proof-
note `P a ∨ ¬P a`
moreover
{assume "P a"
hence "∃x. P x"..
hence "¬ P a ∨ (∃x. P x)"..}
moreover
{assume 2:"¬P a"
hence "¬ P a ∨ (∃x. P x)"..}
ultimately
show "¬ P a ∨ (∃x. P x)"..
qed
hence "¬P a" using 1 by (rule ejercicio_42)}
hence "∀x. ¬(P x)"..
with assms show False..
qed
text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
∀x. ¬(P x) ⊢ ¬(∃x. P x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_17:
assumes "∀x. ¬(P x)"
shows "¬(∃x. P x)"
proof
assume "∃x. P x"
then obtain a where 1:"P a"..
have "¬(P a)" using assms..
thus False using 1..
qed
text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
∃x. P x ⊢ ¬(∀x. ¬(P x))
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_18:
assumes "∃x. P x"
shows "¬(∀x. ¬(P x))"
proof
obtain a where 1: "P a" using assms..
assume "(∀x. ¬(P x))"
hence "¬(P a)"..
thus False using 1..
qed
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
P a ⟶ (∀x. Q x) ⊢ ∀x. P a ⟶ Q x
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_19:
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
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)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_20:
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-
{fix a
{fix b
have "∀y x. R a y ∧ R y x ⟶ R a x" using assms(1)..
hence "∀x. R a b ∧ R b x ⟶ R a x"..
hence 1:"R a b ∧ R b a ⟶ R a a"..
have "¬ R a a" using assms(2)..
with 1 have "¬(R a b ∧ R b a)"by (rule mt)
hence 2:"¬(R a b) ∨ ¬(R b a)" by (rule ejercicio_57)
have "R a b ⟶ ¬R b a"
proof
assume "R a b"
hence "¬(¬(R a b))" by (rule notnotI)
with 2 show "¬R b a" by (rule ejercicio_43)
qed}
hence "∀x. R a x ⟶ ¬R x a"..}
thus "∀y x. R y x ⟶ ¬R x y"..
qed
text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
{∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_21:
assumes "∀x. P x ∨ Q x"
"∃x. ¬(Q x)"
"∀x. R x ⟶ ¬(P x)"
shows "∃x. ¬(R x)"
proof -
obtain a where 1: "¬ (Q a)" using assms(2)..
have "P a∨ Q a" using assms(1) ..
hence "P a" using 1 by (rule ejercicio_42)
hence 2:"¬¬P a" by (rule notnotI)
have "R a ⟶ ¬(P a)" using assms(3)..
hence "¬(R a)" using 2 by (rule mt)
thus ?thesis ..
qed
text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
{∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_22:
assumes "∀x. P x ⟶ Q x ∨ R x"
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
proof
fix a
have 1:"P a ⟶ Q a ∨ R a" using assms(1)..
show "P a ⟶ Q a"
proof -
have "¬(P a) ∨ P a"..
moreover
{assume "¬(P a)"
hence "(P a) ⟶ Q a" by (rule ejercicio_40f)}
moreover
{assume "P a"
with 1 have 2:"Q a ∨ R a"..
have "Q a"
proof (rule ccontr)
assume "¬(Q a)"
with 2 have "R a" by (rule ejercicio_43)
with `P a` have "P a ∧ R a"..
hence "∃x. P x ∧ R x"..
with assms(2) show False..
qed
hence "P a ⟶ Q a"..}
ultimately show "P a ⟶ Q a"..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_23:
assumes "∃x y. R x y ∨ R y x"
shows "∃x y. R x y"
proof-
obtain a where 1: "∃y. R a y ∨ R y a" using assms..
then obtain b where "R a b ∨ R b a"..
moreover
{assume "R a b"
hence "∃x. R a x"..
hence ?thesis..}
moreover
{assume "R b a"
hence "∃x. R b x"..
hence ?thesis..}
ultimately show ?thesis ..
qed
text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_24:
"(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof
assume "(∃x. ∀y. P x y)"
then obtain a where 1:"∀y. P a y"..
{fix b
have "P a b" using 1..
hence "∃x. P x b"..}
thus "∀y. ∃x. P x y"..
qed
text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_25:
"(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
proof
assume 1:"(∀x. P x ⟶ Q)"
show "(∃x. P x)⟶ Q"
proof
assume "(∃x. P x)"
then obtain b where "P b"..
have "P b ⟶ Q" using 1..
thus Q using `P b`..
qed
next
assume 2:"((∃x. P x) ⟶ Q)"
show "(∀x. P x ⟶ Q)"
proof
fix c
show "P c ⟶Q"
proof
assume "P c"
hence "∃x. P x"..
with 2 show Q..
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_26:
"((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
proof
assume 1:"((∀x. P x) ∧ (∀x. Q x))"
hence 2:"∀x. P x"..
have 3:"∀x. Q x" using 1..
{fix a
have 4:"P a" using 2..
have "Q a" using 3..
with 4 have "P a ∧ Q a"..}
thus "∀x. P x ∧ Q x"..
next
assume 1: "(∀x. P x ∧ Q x)"
{fix a
have "P a ∧ Q a" using 1..
hence "P a"..}
hence 2: "∀x. P x"..
{fix a
have "P a ∧ Q a" using 1..
hence "Q a"..}
hence 3: "∀x. Q x"..
with 2 show "(∀x. P x)∧(∀x. Q x)"..
qed
text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar o refutar
((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_27:
"((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
quickcheck (* Es falso *)
oops
text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar o refutar
((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_28:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
proof
assume "((∃x. P x) ∨ (∃x. Q x))"
moreover
{assume "(∃x. P x)"
then obtain a where "P a"..
hence "P a ∨ Q a"..
hence "(∃x. P x ∨ Q x)"..}
moreover
{assume "(∃x. Q x)"
then obtain a where "Q a"..
hence "P a ∨ Q a"..
hence "(∃x. P x ∨ Q x)"..}
ultimately
show "(∃x. P x ∨ Q x)" ..
next
assume "(∃x. P x ∨ Q x)"
then obtain a where "P a ∨ Q a" ..
moreover
{assume "P a"
hence "∃x. P x"..
hence "(∃x. P x) ∨ (∃y. Q y)"..}
moreover
{assume "Q a"
hence "∃x. Q x"..
hence "(∃x. P x) ∨ (∃y. Q y)"..}
ultimately
show "(∃x. P x) ∨ (∃y. Q y)" ..
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 (* Es falso*)
oops
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar o refutar
(¬(∀x. P x)) ⟷ (∃x. ¬P x)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_30:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof
assume 1:"(¬(∀x. P x))"
show 2:"(∃x. ¬P x)"
proof (rule ccontr)
assume 3:"¬(∃x. ¬P x)"
{fix a
have 4: "P a"
proof (rule ccontr)
assume "¬(P a)"
hence "∃x. ¬(P x)"..
with 3 show False..
qed}
hence "∀x. P x"..
with 1 show False..
qed
next
assume 1: "(∃x. ¬P x)"
then obtain a where 2: "¬ (P a)"..
show 3:"¬(∀x. P x)"
proof
assume "∀x. P x"
hence "P a"..
with 2 show False..
qed
qed
section {* Ejercicios sobre igualdad *}
text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar o refutar
P a ⟹ ∀x. x = a ⟶ P x
------------------------------------------------------------------ *}
lemma ejercicio_31b:
assumes "P a"
shows "∀x. x = a ⟶ P x"
proof
fix x
show "x= a ⟶ P x"
proof
assume "x= a"
hence "a = x"..
thus "P x" using assms by (rule subst)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar o refutar
∃x y. R x y ∨ R y x; ¬(∃x. R x x)⟧ ⟹ ∃x y. x ≠ y
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_32:
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 1: "∃y. R a y ∨ R y a" using assms(1)..
then obtain b where 2:"(R a b ∨ R b a)" ..
have "a≠b"
proof
assume 5:"a=b"
show False
proof (rule disjE)
show "R a b ∨ R b a" using 2.
next
assume "R a b"
with 5 have "R b b" by (rule subst)
hence "∃x. R x x"..
with assms(2) show False..
next
assume 7:"R b a"
have "b=a" using 5..
hence "R a a" using 7 by (rule subst)
hence "∃x. R x x"..
with assms(2) show False..
qed
qed
hence "∃x. a≠x"..
thus ?thesis ..
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)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_33:
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 1:"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 ?thesis using 1..
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))
------------------------------------------------------------------ *}
-- "Pedro Ros"
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 1: "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 1..
thus ?thesis..
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))
------------------------------------------------------------------ *}
lemma ejercicio_35:
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))"
oops
text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar o refutar
{x = f x, odd (f x)} ⊢ odd x
------------------------------------------------------------------ *}
lemma ejercicio_36b:
"⟦x = f x; odd (f x)⟧ ⟹ odd x"
oops
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar o refutar
{x = f x, triple (f x) (f x) x} ⊢ triple x x x
------------------------------------------------------------------ *}
lemma ejercicio_37b:
"⟦x = f x; triple (f x) (f x) x⟧ ⟹ triple x x x"
oops
end