Usuario discusión:Jgiraldez - Historial de revisiones

Jgiraldez: Página blanqueada

2011-02-06T23:05:21Z

Página blanqueada

Mostrar los cambios

Jgiraldez: /* RA_Relacion_2 */

2011-02-03T16:00:35Z

‎RA_Relacion_2

Jgiraldez: /* RA_Relacion_1 */

2011-02-03T16:00:21Z

‎RA_Relacion_1

Jgiraldez: /* RA_Relacion_2 */

2011-02-03T15:53:26Z

‎RA_Relacion_2

Jgiraldez: /* RA_Relacion_1 */

2011-02-03T15:53:00Z

‎RA_Relacion_1

Jgiraldez: /* RA_Relacion_1 */

2011-02-03T15:37:27Z

‎RA_Relacion_1

Mostrar los cambios

Jgiraldez: Nueva sección: /* RA_Relacion_2 */

2011-02-03T15:36:55Z

Nueva sección: ‎RA_Relacion_2

Jgiraldez: RA_Relacion_1

2011-02-03T15:35:55Z

RA_Relacion_1

Página nueva

== RA_Relacion_1 ==

theory Relacion_2
imports Main
begin

(* Demostrar o refutar los siguientes lemas usando sólo las reglas básicas
de deducción natural de la lógica proposicional y de la lógica de
predicados (allI, allE, exI y exE). *)

lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof (rule impI)
assume 1: "(∃x. ∀y. P x y)"
show "(∀y. ∃x. P x y)"
proof (rule allI)
from 1 obtain x where 2: "∀y. P x y" by (rule exE)
fix y
from 2 have 3: "P x y" by (rule allE)
from 3 show 4: "∃x. P x y" by (rule exI)
qed
qed

lemma "(∀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 a where "P a" by (rule exE)
have "P a ⟶ Q" using 1 by (rule allE)
thus "Q" using `P a` by (rule mp)
qed }
next
{ assume 2: "(∃x. P x) ⟶ Q"
show "∀x. P x ⟶ Q"
proof
fix a
show "P a ⟶ Q"
proof
assume "P a"
hence 3: "∃x. P x" by (rule exI)
from 2 and 3 show "Q" by (rule mp)
qed
qed }
qed

lemma "((∀ x. P x) ∧ (∀ x. Q x)) = (∀ x. (P x ∧ Q x))"
proof
{
assume 1: "(∀ x. P x) ∧ (∀ x. Q x)"
show "(∀ x. (P x ∧ Q x))"
proof (rule allI)
from 1 have 2: "(∀ x. P x)" by (rule conjE)
from 1 have 3: "(∀ x. Q x)" by (rule conjE)
fix a
from 2 have 4: "P a" by (rule allE)
from 3 have 5: "Q a" by (rule allE)
from 4 and 5 show 6: "(P a) ∧ (Q a)" by (rule conjI)
qed
}
next
{
assume 7: "∀ x. (P x ∧ Q x)"
show "(∀ x. P x) ∧ (∀ x. Q x)"
proof
fix a
from 7 have 8: "P a ∧ Q a" by (rule allE)
from 8 have 9: "P a" by (rule conjE)
(* seguir... *)
from 8 have 11: "Q a" by (rule allE)
(* seguir... *)
qed
}
qed

oops

lemma "((∀ x. P x) ∨ (∀ x. Q x)) = (∀ x. (P x ∨ Q x))"
oops

lemma "((∃ x. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))"
oops

lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops
(*
proof (rule impI)
assume 1: "∀x. ∃y. P x y"
show "∃y. ∀x. P x y"
proof (rule exI)
show " ∀x. P x y"
proof (rule allI)
fix x
from 1 have 2: "∃y. P x y" by (rule allE)
from 2 obtain y where 3: "P x y" by (rule exE)
thus ?thesis ..
qed
*)

lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
proof
{
assume 1: "¬ (∀ x. P x)"
show "∃ x. ¬ P x"
proof

qed
}
next
{
assume 2: "∃ x. ¬ P x"
show "¬ (∀ x. P x)"
proof

qed
}
qed

end

@@ Línea 211: / Línea 211: @@
 </source>
-== RA_Relacion_2 ==
+== RA: Relacion 2 ==
 <source lang="isar">

@@ Línea 1: / Línea 1: @@
-== RA_Relacion_1 ==
+== RA: Relacion 1 ==
 <source lang="isar">
 theory Relacion_1

@@ Línea 212: / Línea 212: @@
 == RA_Relacion_2 ==
 theory Relacion_2
@@ Línea 332: / Línea 333: @@
 end

@@ Línea 1: / Línea 1: @@
 == RA_Relacion_1 ==
+<source lang="isar">
 theory Relacion_1
 imports Main
@@ Línea 208: / Línea 208: @@
 end
 == RA_Relacion_2 ==

← Revisión anterior		Revisión del 15:36 3 feb 2011
Línea 1:		Línea 1:
	== RA_Relacion_1 ==		== RA_Relacion_1 ==
		+
		+	theory Relacion_2
		+	imports Main
		+	begin
		+
		+	(* Demostrar o refutar los siguientes lemas usando sólo las reglas básicas
		+	de deducción natural de la lógica proposicional y de la lógica de
		+	predicados (allI, allE, exI y exE). *)
		+
		+
		+	lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
		+	proof (rule impI)
		+	assume 1: "(∃x. ∀y. P x y)"
		+	show "(∀y. ∃x. P x y)"
		+	proof (rule allI)
		+	from 1 obtain x where 2: "∀y. P x y" by (rule exE)
		+	fix y
		+	from 2 have 3: "P x y" by (rule allE)
		+	from 3 show 4: "∃x. P x y" by (rule exI)
		+	qed
		+	qed
		+
		+	lemma "(∀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 a where "P a" by (rule exE)
		+	have "P a ⟶ Q" using 1 by (rule allE)
		+	thus "Q" using `P a` by (rule mp)
		+	qed }
		+	next
		+	{ assume 2: "(∃x. P x) ⟶ Q"
		+	show "∀x. P x ⟶ Q"
		+	proof
		+	fix a
		+	show "P a ⟶ Q"
		+	proof
		+	assume "P a"
		+	hence 3: "∃x. P x" by (rule exI)
		+	from 2 and 3 show "Q" by (rule mp)
		+	qed
		+	qed }
		+	qed
		+
		+	lemma "((∀ x. P x) ∧ (∀ x. Q x)) = (∀ x. (P x ∧ Q x))"
		+	proof
		+	{
		+	assume 1: "(∀ x. P x) ∧ (∀ x. Q x)"
		+	show "(∀ x. (P x ∧ Q x))"
		+	proof (rule allI)
		+	from 1 have 2: "(∀ x. P x)" by (rule conjE)
		+	from 1 have 3: "(∀ x. Q x)" by (rule conjE)
		+	fix a
		+	from 2 have 4: "P a" by (rule allE)
		+	from 3 have 5: "Q a" by (rule allE)
		+	from 4 and 5 show 6: "(P a) ∧ (Q a)" by (rule conjI)
		+	qed
		+	}
		+	next
		+	{
		+	assume 7: "∀ x. (P x ∧ Q x)"
		+	show "(∀ x. P x) ∧ (∀ x. Q x)"
		+	proof
		+	fix a
		+	from 7 have 8: "P a ∧ Q a" by (rule allE)
		+	from 8 have 9: "P a" by (rule conjE)
		+	(* seguir... *)
		+	from 8 have 11: "Q a" by (rule allE)
		+	(* seguir... *)
		+	qed
		+	}
		+	qed
		+
		+	oops
		+
		+	lemma "((∀ x. P x) ∨ (∀ x. Q x)) = (∀ x. (P x ∨ Q x))"
		+	oops
		+
		+	lemma "((∃ x. P x) ∨ (∃ x. Q x)) = (∃ x. (P x ∨ Q x))"
		+	oops
		+
		+	lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
		+	oops
		+	(*
		+	proof (rule impI)
		+	assume 1: "∀x. ∃y. P x y"
		+	show "∃y. ∀x. P x y"
		+	proof (rule exI)
		+	show " ∀x. P x y"
		+	proof (rule allI)
		+	fix x
		+	from 1 have 2: "∃y. P x y" by (rule allE)
		+	from 2 obtain y where 3: "P x y" by (rule exE)
		+	thus ?thesis ..
		+	qed
		+	*)
		+
		+	lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
		+	proof
		+	{
		+	assume 1: "¬ (∀ x. P x)"
		+	show "∃ x. ¬ P x"
		+	proof
		+
		+
		+	qed
		+	}
		+	next
		+	{
		+	assume 2: "∃ x. ¬ P x"
		+	show "¬ (∀ x. P x)"
		+	proof
		+
		+	qed
		+	}
		+	qed
		+
		+	end
		+
		+	== RA_Relacion_2 ==

	theory Relacion_2		theory Relacion_2