Relación 8 - Historial de revisiones

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

2018-07-16T07:48:14Z

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

2011-03-05T13:01:19Z

2011-03-05T12:58:36Z

2011-03-05T12:56:54Z

2011-03-05T11:35:52Z

2011-03-05T11:34:13Z

2011-03-02T01:09:05Z

2011-03-02T00:57:15Z

2011-03-02T00:55:03Z

2011-03-02T00:22:31Z

@@ Línea 1: / Línea 1: @@
-<source lang="isar">
+<source lang="isabelle">
 theory Relacion_8
 imports Main Efficient_Nat Relacion_3

@@ Línea 141: / Línea 141: @@
 encontrará ningún contra ejemplo.
 *}
 text {*

@@ Línea 137: / Línea 137: @@
       suma (rev xs) = suma xs
    ---------------------------------------------------------------------
 *}

@@ Línea 88: / Línea 88: @@
    ---------------------------------------------------------------------
 *}
 text {*

@@ Línea 112: / Línea 112: @@
 lemma "aplana (rev xs) = aplana xs"
 quickcheck
 text {* El contraejemplo encontrado es xs = [[2], [1, 2]]. Esto tiene

@@ Línea 143: / Línea 143: @@
 text {*
 La siguiente definición se construye utilizando la palabra reservada
-"definition".
+"definition". Aunque se trata de una función recursiva primitiva no
 *}

← Revisión anterior		Revisión del 00:57 2 mar 2011
Línea 145:		Línea 145:
	"definition".		"definition".
	*}		*}
		+
		+
		+	definition algunos2 :: "('a => bool) => 'a list => bool" where
		+	"algunos2 P xs ≡ ¬ list_all (λx. ¬ P x) xs"

@@ Línea 135: / Línea 135: @@
    ---------------------------------------------------------------------
    Ejercicio 13. Redefinir, usando la función list_all, la función
    algunos. Llamar la nueva función algunos2 y demostrar que es
    equivalente a algunos.
    ---------------------------------------------------------------------
 *}
 end
 </source>

@@ Línea 43: / Línea 43: @@
       length (aplana xs) = suma (map length xs)
    ---------------------------------------------------------------------
 *}
@@ Línea 48: / Línea 54: @@
 lemma "length (aplana xs) = suma (map length xs)"
 by (induct xs) auto
 text {*