Relación 4 - Historial de revisiones

WikiSysop: Texto reemplazado: «Isar» por «isabelle»

2018-07-16T12:41:07Z

Texto reemplazado: «Isar» por «isabelle»

Rammoi en 17:25 24 abr 2016

2016-04-24T17:25:10Z

Marherfer6 en 07:21 24 abr 2016

2016-04-24T07:21:48Z

Marherfer6 en 16:48 23 abr 2016

2016-04-23T16:48:56Z

Marherfer6 en 15:22 23 abr 2016

2016-04-23T15:22:57Z

Marherfer6 en 11:27 23 abr 2016

2016-04-23T11:27:30Z

Mostrar los cambios

Marherfer6 en 09:20 23 abr 2016

2016-04-23T09:20:53Z

Angruigon2: 1-22 sin el 10, 30-37 sin el 32.

2016-04-14T07:35:06Z

1-22 sin el 10, 30-37 sin el 32.

Mostrar los cambios

Carconoit en 13:08 5 abr 2016

2016-04-05T13:08:38Z

Mjoseh: Página creada con ' header {* R4: Deducción natural de primer orden } theory R4 imports Main begin text { Demostrar o refutar los siguientes lemas usando sólo las re...'

2016-04-01T08:03:40Z

Página creada con '<source lang = "Isar"> header {* R4: Deducción natural de primer orden *} theory R4 imports Main begin text {* Demostrar o refutar los siguientes lemas usando sólo las re...'

Página nueva

<source lang = "Isar">
header {* R4: Deducción natural de primer orden *}

theory R4
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
· excluded_middel:(¬P ∨ 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)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
∃x. ¬(P x) ⊢ ¬(∀x. P x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
∀x. P x ⊢ ∀y. P y
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
∀x. P x ⟶ Q x ⊢ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
∀x. P x ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
∀x y. P x y ⊢ ∀u v. P u v
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
∃x y. P x y ⟹ ∃u v. P u v
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
∃x. P a ⟶ Q x ⊢ P a ⟶ (∃x. Q x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------ *}

lemma ejercicio_10a:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
oops

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
(∃x. P x) ⟶ Q a ⊢ ∀x. P x ⟶ Q a
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
∀x. P x ⟶ Q a ⊢ ∃ x. P x ⟶ Q a
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
(∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
∀x y. P y ⟶ Q x ⊢ (∃y. P y) ⟶ (∀x. Q x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
¬(∀x. ¬(P x)) ⊢ ∃x. P x
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
∀x. ¬(P x) ⊢ ¬(∃x. P x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
∃x. P x ⊢ ¬(∀x. ¬(P x))
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
P a ⟶ (∀x. Q x) ⊢ ∀x. P a ⟶ Q x
------------------------------------------------------------------ *}

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

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)
------------------------------------------------------------------ *}

lemma ejercicio_20a:
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)"
oops

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
{∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
{∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)
------------------------------------------------------------------ *}

lemma ejercicio_24a:
"(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
oops

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
------------------------------------------------------------------ *}

lemma ejercicio_25a:
"(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
oops

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_26a:
"((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar o refutar
((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_27a:
"((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar o refutar
((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_28a:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
oops

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)"
oops

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar o refutar
(¬(∀x. P x)) ⟷ (∃x. ¬P x)
------------------------------------------------------------------ *}

lemma ejercicio_30a:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
oops

section {* Ejercicios sobre igualdad *}

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar o refutar
P a ⟹ ∀x. x = a ⟶ P x
------------------------------------------------------------------ *}

lemma ejercicio_31a:
assumes "P a"
shows "∀x. x = a ⟶ P x"
oops

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar o refutar
∃x y. R x y ∨ R y x; ¬(∃x. R x x)⟧ ⟹ ∃x y. x ≠ y
------------------------------------------------------------------ *}

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"
oops

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)
------------------------------------------------------------------ *}

lemma ejercicio_33a:
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)"
oops

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))
------------------------------------------------------------------ *}

lemma ejercicio_34a:
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))"
oops

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_35a:
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_36a:
assumes "x = f x" and
"odd (f x)"
shows "odd x"
oops

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar o refutar
{x = f x, triple (f x) (f x) x} ⊢ triple x x x
------------------------------------------------------------------ *}

lemma ejercicio_37a:
assumes "x = f x" and
"triple (f x) (f x) x"
shows "triple x x x"
oops

end

</source>

← Revisión anterior		Revisión del 12:41 16 jul 2018
Línea 1:		Línea 1:
−	<source lang = "~~Isar~~">	+	<source lang = "isabelle">
	header {* R4: Deducción natural de primer orden *}		header {* R4: Deducción natural de primer orden *}

@@ Línea 853: / Línea 853: @@
 lemma ejercicio_28a:
    "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
-oops
+proof(rule iffI)
 text {* ---------------------------------------------------------------
@@ Línea 898: / Línea 923: @@
     thus 15: "¬(∀x. P x)" by (rule ccontr)
 qed
 qed

@@ Línea 72: / Línea 72: @@
        show "Q a" using 3 2 by (rule mp)}
        qed
 qed
@@ Línea 88: / Línea 101: @@
    show "False" using `¬ (P a)` `P a` by (rule notE)
 qed
 text {* ---------------------------------------------------------------
    Ejercicio 3. Demostrar
@@ Línea 99: / Línea 124: @@
 { fix a
    show "P a" using assms by (rule allE)}
 qed
@@ Línea 116: / Línea 150: @@
      have "¬(P a)" using `P a ⟶ Q a` `¬ (Q a)` by (rule mt)}
 thus "∀x. ¬ (P x)" by (rule allI)
 qed
@@ Línea 134: / Línea 181: @@
    have "¬(Q a)" using `P a  ⟶ ¬(Q a)` `P a` by (rule mp)
 show "False" using `¬(Q a)` `Q a` by (rule notE)
 qed
@@ Línea 148: / Línea 209: @@
 have  "∀y. P a y" using assms by (rule allE)
 thus " P a b" by (rule allE)
 qed
@@ Línea 180: / Línea 253: @@
 qed
 text {* ---------------------------------------------------------------
@@ Línea 196: / Línea 279: @@
 qed
 text {* ---------------------------------------------------------------
@@ Línea 206: / Línea 299: @@
    assumes "P a ⟶ (∃x. Q x)"
    shows   "∃x. P a ⟶ Q x"
-oops
+proof-
@@ Línea 227: / Línea 337: @@
 qed
+lemma ejercicio_11a:
 text {* ---------------------------------------------------------------

@@ Línea 165: / Línea 165: @@
 qed
 text {* ---------------------------------------------------------------
    Ejercicio 5. Demostrar

@@ Línea 790: / Línea 790: @@
 lemma ejercicio_25a:
    "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
-oops
+proof (rule iffI)
 text {* ---------------------------------------------------------------
@@ Línea 799: / Línea 814: @@
 lemma ejercicio_26a:
    "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
-oops
+proof (rule iffI)
 text {* ---------------------------------------------------------------

@@ Línea 600: / Línea 600: @@
 qed
 qed
 qed
@@ Línea 866: / Línea 888: @@
 qed
 qed
-−
 text {* ---------------------------------------------------------------
@@ Línea 878: / Línea 911: @@
            "¬(∃x. R x x)"
    shows   "∃(x::'c) y. x ≠ y"
-oops
+proof-
 text {* ---------------------------------------------------------------

@@ Línea 63: / Línea 63: @@
    assumes "∀x. P x ⟶ Q x"
    shows   "(∀x. P x) ⟶ (∀x. Q x)"
-oops
+proof (rule impI)
 text {* ---------------------------------------------------------------