Relación 4 - Historial de revisiones

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

2018-07-16T12:27:10Z

Texto reemplazado: «isar» por «isabelle»

Fracarmol1 en 11:10 31 mar 2015

2015-03-31T11:10:20Z

Jaialbjai en 13:52 30 mar 2015

2015-03-30T13:52:29Z

Jaialbjai en 13:42 30 mar 2015

2015-03-30T13:42:50Z

Fracarmol1 en 08:43 30 mar 2015

2015-03-30T08:43:16Z

Rocrodhue en 11:55 28 mar 2015

2015-03-28T11:55:09Z

Rocrodhue en 08:16 28 mar 2015

2015-03-28T08:16:20Z

Luicurote en 00:40 26 mar 2015

2015-03-26T00:40:40Z

Luicurote en 00:24 26 mar 2015

2015-03-26T00:24:23Z

Jaialbjai en 16:06 25 mar 2015

2015-03-25T16:06:30Z

← Revisión anterior		Revisión del 12:27 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 721: / Línea 721: @@
         (¬(∀x. P x)) ⟷ (∃x. ¬P x)
    ------------------------------------------------------------------ *}
 lemma ejercicio_30a:
    "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
-oops
+proof (rule iffI)
 section {* Ejercicios sobre igualdad *}

← Revisión anterior		Revisión del 13:52 30 mar 2015
Línea 784:		Línea 784:
	qed		qed

−	~~-- Jaime Alberto~~
−
−	~~proof -~~
−	~~have 1:"P a a a ⟶ P (f a) a (f a)" using assms(2) by (rule allE)+~~
−	~~have 2:"P a a a" using assms(1) by (rule allE)~~
−	~~show "P (f a) a (f a)" using 1 2 by (rule mp)~~
−	~~qed~~

@@ Línea 783: / Línea 783: @@
      show 5: "P (f a) a (f a)" using 4 1 by (rule mp)
 qed
 text {* ---------------------------------------------------------------

@@ Línea 732: / Línea 732: @@
         P a ⟹ ∀x. x = a ⟶ P x
    ------------------------------------------------------------------ *}
 lemma ejercicio_31a:
    assumes "P a"
    shows   "∀x. x = a ⟶ P x"
-oops
+proof (rule allI)
 text {* ---------------------------------------------------------------
@@ Línea 756: / Línea 769: @@
       ⊢ P (f a) a (f a)
    ------------------------------------------------------------------ *}
 lemma ejercicio_33a:
@@ Línea 761: / Línea 776: @@
            "∀x y z. P x y z ⟶ P (f x) y (f z)"
    shows   "P (f a) a (f a)"
-oops
+proof -
 text {* ---------------------------------------------------------------
@@ Línea 769: / Línea 790: @@
       ⊢ ∃z. P (f a) z (f (f a))
    ------------------------------------------------------------------ *}
 lemma ejercicio_34a:
@@ Línea 774: / Línea 797: @@
            "∀x y z. P x y z ⟶ P (f x) y (f z)"
    shows   "∃z. P (f a) z (f (f a))"
-oops
+proof -
 text {* ---------------------------------------------------------------
@@ Línea 782: / Línea 812: @@
       ⊢ ∃z. Qa z ∧ Q z (s (s a))
    ------------------------------------------------------------------ *}
 lemma ejercicio_35a:
@@ Línea 787: / Línea 819: @@
            "∀x y. Q x y ⟶ Q (s x) (s y)"
    shows   "∃z. Q a z ∧ Q z (s (s a))"
-oops
+proof -
 text {* ---------------------------------------------------------------
@@ Línea 793: / Línea 832: @@
       {x = f x, odd (f x)} ⊢ odd x
    ------------------------------------------------------------------ *}
 lemma ejercicio_36a:
@@ Línea 798: / Línea 839: @@
            "odd (f x)"
    shows "odd x"
-oops
+proof -
 text {* ---------------------------------------------------------------
@@ Línea 804: / Línea 847: @@
       {x = f x, triple (f x) (f x) x} ⊢ triple x x x
    ------------------------------------------------------------------ *}
 lemma ejercicio_37a:
@@ Línea 809: / Línea 854: @@
            "triple (f x) (f x) x"
    shows "triple x x x"
-oops
+proof -
+   show "triple x x x" using assms(1) assms(2) by (rule ssubst)
 end

@@ Línea 354: / Línea 354: @@
 lemma ejercicio_16a:
-   assumes "¬(∀x. ¬(P x))"
+   assumes 1:"¬(∀x. ¬(P x))"
    shows   "∃x. P x"
-oops
 text {* ---------------------------------------------------------------

← Revisión anterior		Revisión del 08:16 28 mar 2015
Línea 161:		Línea 161:

	--Jaime Alberto		--Jaime Alberto
		+
		+
		+	lemma ejercicio_6b:
		+	assumes 1: "∀x y. P x y"
		+	shows "∀u v. P u v"
		+	proof -
		+	{fix u0
		+	{fix v0
		+	have 2: "∀y. P u0 y" using 1 by (rule allE)
		+	have 3: "P u0 v0" using 2 by (rule allE)}
		+	then have 4: "∀v. P u0 v" by (rule allI)}
		+	then show "∀u v. P u v" by (rule allI)
		+	qed
		+
		+	-- Rocio Rodriguez

	text {* ---------------------------------------------------------------		text {* ---------------------------------------------------------------

@@ Línea 684: / Línea 684: @@
    "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
 oops
 text {* ---------------------------------------------------------------

@@ Línea 578: / Línea 578: @@
 lemma ejercicio_26a:
    "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
-oops
+  "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
 text {* ---------------------------------------------------------------
@@ Línea 587: / Línea 608: @@
 lemma ejercicio_27a:
    "((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
 oops

@@ Línea 597: / Línea 597: @@
 lemma ejercicio_28a:
    "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
-oops
 text {* ---------------------------------------------------------------