Relación 4 - Historial de revisiones

Pedrosrei en 07:16 19 mar 2013

2013-03-19T07:16:19Z

Raumonpaj en 23:02 18 mar 2013

2013-03-18T23:02:27Z

Raumonpaj en 22:37 18 mar 2013

2013-03-18T22:37:12Z

Raumonpaj en 22:31 18 mar 2013

2013-03-18T22:31:39Z

Raumonpaj en 22:21 18 mar 2013

2013-03-18T22:21:09Z

Pedrosrei en 21:33 18 mar 2013

2013-03-18T21:33:00Z

Pedrosrei en 21:30 18 mar 2013

2013-03-18T21:30:26Z

Pedrosrei en 21:28 18 mar 2013

2013-03-18T21:28:17Z

Pedrosrei en 19:11 18 mar 2013

2013-03-18T19:11:00Z

Pedrosrei en 19:05 18 mar 2013

2013-03-18T19:05:10Z

Mostrar los cambios

@@ Línea 122: / Línea 122: @@
 lemma ejercicio_3a:
-   assumes 1:"A⟶ ((M⟶ ¬B)∧(¬B⟶ M))" and
+   assumes 1:"A⟶ (M⟷ ¬B)" and
-:"A ∨ B"  and
+:"A ∨ B"
    shows "¬B⟶ M"
 proof
    assume "¬B"
    have "A" using 2 `¬B` by (rule or1)
-   have "((M⟶ ¬B)∧(¬B⟶ M))" using 1 `A`..
+   have "(M⟷ ¬B)" using 1 `A`..
    hence "(¬B⟶ M)" ..
    thus "M" using `¬B` ..

@@ Línea 197: / Línea 197: @@
    assume "¬T"
    show "M" using 1 `¬T` ..
 qed

@@ Línea 152: / Línea 152: @@
    assume "B"
     {assume "¬B"
-     have False using `¬B` `B`..
+     have "M" using `¬B` `B`..}
    thus "¬B ⟶ M"..
 qed

@@ Línea 145: / Línea 145: @@
    assume "A"
     {assume "¬B"
      have "¬B ∧ A" using `¬B` `A`..
-     with `¬B ∧ A ⟶ A ∧ M` have "A ∧ M"..
+     with assms(1) have "A ∧ M"..
      hence "M"..}
    thus "¬B ⟶ M"..

← Revisión anterior		Revisión del 22:21 18 mar 2013
Línea 135:		Línea 135:
	qed		qed

		+	-- "Raúl Montes Pajuelo"
		+
		+	lemma ejercicio_3b:
		+	assumes "A ∧ M ⟷ ¬B ∧ A"
		+	"A ∨ B"
		+	shows "¬B ⟶ M"
		+	using assms (2)
		+	proof
		+	assume "A"
		+	{assume "¬B"
		+	have "¬B ∧ A ⟶ A ∧ M" using assms (1)..
		+	have "¬B ∧ A" using `¬B` `A`..
		+	with `¬B ∧ A ⟶ A ∧ M` have "A ∧ M"..
		+	hence "M"..}
		+	thus "¬B ⟶ M"..
		+	next
		+	assume "B"
		+	{assume "¬B"
		+	have False using `¬B` `B`..
		+	hence "M"..}
		+	thus "¬B ⟶ M"..
		+	qed

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

@@ Línea 103: / Línea 103: @@
         M: El paciente ha mejorado notablemente.
    ------------------------------------------------------------------ *}
-text {* Pedro Ros. Si alguien consigue una demostración sin usar or1 e igual de corta, por favor que la ponga. *}
+text {* Pedro Ros. Si alguien consigue una demostración sin usar or1 e igual de corta,
 lemma or1:
    assumes "p∨q"

@@ Línea 371: / Línea 371: @@
        hence 6: "F∨N" ..
        show "W" using 2 6 ..
 qed

@@ Línea 55: / Línea 55: @@
         L para "Llueve".
    ------------------------------------------------------------------ *}
 lemma ejercicio_1:
    assumes "T ∧ P ⟶ ¬L" and
@@ Línea 78: / Línea 80: @@
         C para "el número acaba en cero".
    ------------------------------------------------------------------ *}
 lemma ejercicio_2:
    assumes "D⟶ C" and
@@ Línea 85: / Línea 89: @@
 show "¬D" using assms(1) assms(2) by (rule mt)
 qed
 text {* ---------------------------------------------------------------
    Ejercicio 3. Formalizar, y demostrar la corrección, del siguiente
@@ Línea 107: / Línea 112: @@
         A: El ayer está escrito.
    ------------------------------------------------------------------ *}
--- "Pedro"
+-- "Pedro Ros"
 lemma ejercicio_4a:
 "(¬M ∧ ¬A)⟶ ¬ M"
@@ Línea 124: / Línea 129: @@
    ------------------------------------------------------------------ *}
-text {* Pedro. Defino la ley del tercero exluido *}
+text {* Pedro Ros. Defino la ley del tercero exluido demostrada en la relación 3 ya. *}
 lemma LEM: "P ∨ ¬P"
 by auto
@@ Línea 152: / Línea 157: @@
         P: Te avisé del peligro que corrías.
    ------------------------------------------------------------------ *}
 lemma ejercicio_6:
 assumes "T⟶ (R∧ ¬¬P)"
@@ Línea 173: / Línea 179: @@
         I: Aumentará el índice de pobreza.
    ------------------------------------------------------------------ *}
 lemma ejercicio_7a:
 assumes 1:"¬N⟶ P" and
@@ Línea 233: / Línea 240: @@
    ------------------------------------------------------------------ *}
 text {* Pedro. Cambio O por W para que me funcione. Y defino otra regla básica *}
-lemma negconj: "¬(P∧Q) ⟹ ¬P ∨ ¬Q"
+lemma negconj:
-by auto
+  assumes "¬(p ∧ q)"
 lemma ejercicio_10:
@@ Línea 273: / Línea 299: @@
 hacerlo con auto, podemos hacer que Pedro sea traidor (p) pero no es siempre cierto, puede serlo
 Quintín sólo, o Quintín y Pedro, lo que está claro que el traidor es Quintín siempre. aun así lo
-formalizo *}
+formalizo y con quickcheck (para que los usuarios de jedit, puedan verlo) *}
 lemma ejercicio_10a:
@@ Línea 282: / Línea 308: @@
 quickcheck
 oops
 text {* ---------------------------------------------------------------
    Ejercicio 11. Formalizar, y demostrar la corrección, del siguiente
@@ Línea 299: / Línea 326: @@
         O : Se aceptan órdenes del operador.
    ------------------------------------------------------------------ *}
-text {* Pedro. Cambio W por O *}
+text {* Pedro Ros. Cambio W por O *}
 lemma ejercicio_11:
@@ Línea 315: / Línea 342: @@
        show "W" using 2 6 ..
 qed
 text {* ---------------------------------------------------------------
    Ejercicio 12. Formalizar, y demostrar la corrección, del siguiente
@@ Línea 326: / Línea 354: @@
         r: Gozo de la vida.
    ------------------------------------------------------------------ *}
 lemma ejercicio_12:
 assumes 1:"(p⟶q)∧(¬p⟶r)" and
@@ Línea 350: / Línea 380: @@
    qed
 qed
 end
 </source>