Relación 4 - Historial de revisiones

Pedrosrei en 19:06 18 mar 2013

2013-03-18T19:06:46Z

2013-03-17T15:19:35Z

2013-03-17T15:14:22Z

2013-03-11T20:34:38Z

2013-03-11T18:49:41Z

2013-03-11T18:49:00Z

2013-03-11T18:10:42Z

2013-03-11T17:25:34Z

2013-03-11T15:47:38Z

2013-03-11T15:39:23Z

@@ Línea 253: / Línea 253: @@
         E: Dios existe.
    ------------------------------------------------------------------ *}
-text {* Pedro. Cambio O por W para que me funcione. Y defino otra regla básica *}
+text {* Pedro. Cambio O por W para que me funcione. Y defino otra regla básica negconj *}
-lemma negconj: "¬(P∧Q) ⟹ ¬P ∨ ¬Q"
+lemma negconj:
-by auto
+  assumes "¬(p ∧ q)"
 lemma ejercicio_10:

@@ Línea 301: / Línea 301: @@
 :"¬r"
 shows "p"
 oops

@@ Línea 348: / Línea 348: @@
         r: Gozo de la vida.
    ------------------------------------------------------------------ *}
 end
 </source>

@@ Línea 321: / Línea 321: @@
         O : Se aceptan órdenes del operador.
    ------------------------------------------------------------------ *}
 text {* ---------------------------------------------------------------
    Ejercicio 12. Formalizar, y demostrar la corrección, del siguiente

@@ Línea 292: / Línea 292: @@
    ------------------------------------------------------------------ *}
 text {* No es cierto como se demuestra con {¬p,q,¬r}. Además isabelle me dice que es mentira al
-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 *}:
+hacerlo con auto, podemos hacer que Pedro sea traidor (p) pero no es siempre cierto, puede serlo
 lemma ejercicio_10a:

@@ Línea 216: / Línea 216: @@
         C: El general comprende las órdenes.
    ------------------------------------------------------------------ *}
+text {* Pedro. Por alguna razón he tenido que cambiar O por P para que funcione *}
 lemma ejercicio_8a:
 assumes 1: "L⟶ P" and
@@ Línea 253: / Línea 253: @@
         E: Dios existe.
    ------------------------------------------------------------------ *}
 text {* ---------------------------------------------------------------
    Ejercicio 10. Formalizar, y demostrar la corrección, del siguiente

@@ Línea 195: / Línea 195: @@
         I: Aumentará el índice de pobreza.
    ------------------------------------------------------------------ *}
+lemma ejercicio_7a:
 text {* ---------------------------------------------------------------
    Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente