Relación 2 - Historial de revisiones

Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»

2018-07-16T07:51:39Z

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

2011-02-14T21:56:10Z

2011-02-14T20:40:32Z

2011-02-14T20:15:52Z

2011-02-14T18:03:52Z

2011-02-14T17:57:25Z

2011-02-14T17:33:47Z

2011-02-11T02:16:45Z

2011-02-10T23:18:46Z

2011-02-10T23:02:25Z

← Revisión anterior		Revisión del 07:51 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* 2ª relación de ejercicios *}		header {* 2ª relación de ejercicios *}

@@ Línea 178: / Línea 178: @@
 text {*
    Comentario de J.A. Alonso: ¿Cómo se calcula un contraejemplo con Isabelle?
 *}

← Revisión anterior	Revisión del 20:15 14 feb 2011
Línea 190:	Línea 190:


	+
	+	-- "Ésta es una demostración detallada del anterior lema"
	+
	+	lemma "(¬ (∀ x. P x)) = (∃ x. ¬ P x)"
	+	proof (rule iffI)
	+	assume 11: "(¬ (∀ x. P x))"
	+	show "∃ x. ¬ P x"
	+	proof (rule ccontr)
	+	assume 12: "¬ (∃ x. ¬ P x)"
	+	note 11
	+	thus False
	+	proof (rule notE)
	+	show "∀ x. P x"
	+	proof (rule allI)
	+	fix x
	+	show "P x"
	+	proof (rule ccontr)
	+	assume 13: "¬ P x"
	+	from 13 have 14: "∃ x. ¬ P x " by (rule exI)
	+	from 12 and 14 show False by (rule notE)
	+	qed
	+	qed
	+	qed
	+	qed
	+	next
	+	assume 21: "∃ x. ¬ P x"
	+	show "(¬ (∀ x. P x))"
	+	proof (rule ccontr)
	+	assume 22: "¬(¬ (∀ x. P x))"
	+	from 22 have 23: "∀ x. P x" by (rule notnotD)
	+	from 21 obtain x where 24: "¬ P x" by (rule exE)
	+	from 23 have 25: "P x" by (rule allE)
	+	from 24 and 25 show False by (rule notE)
	+	qed
	+	qed

@@ Línea 176: / Línea 176: @@
      mismos padres y los mismos hermanos que>> es obvio
      que la implicación es falsa. Un contraejemplo más
-     conocido que se obtiene interpretando P como la
+     conocido se obtiene interpretando P como la
      relación <<menor o igual que>> sobre los números
      reales, de modo que el antecedente indicaría que
@@ Línea 183: / Línea 183: @@
      conjunto de los reales tiene al menos una cota superior."

@@ Línea 172: / Línea 172: @@
      (∀x. ∃y. P x y) ∧ (∀x. (P x x)) ∧ (∀x. ∀y. ((¬( x = y)) ⟶ ¬(P y x))) ∧
      ∧ (∃x. ∃y. (¬(x = y)))
-     y esto es contradictorio con (∃y. ∀x. P x y)."
+     y esto es contradictorio con (∃y. ∀x. P x y).

@@ Línea 119: / Línea 119: @@
      (∀ x. (P x ∨ Q x)) ∧ ¬(∀ x. P x ) ∧ ¬(∀ x. Q x)
      y esto es contradictorio con
-     (∀ x. P x) ∨ (∀ x. Q x)"
+     (∀ x. P x) ∨ (∀ x. Q x). Un ejemplo en lenguaje

@@ Línea 174: / Línea 174: @@
 by auto
 end
 </source>