Relación 7 - Historial de revisiones

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

2021-08-22T09:38:01Z

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

2011-03-04T17:32:49Z

2011-03-03T17:40:25Z

2011-03-02T11:55:40Z

2011-03-02T11:47:42Z

2011-03-02T11:21:11Z

2011-03-02T10:40:11Z

2011-02-25T10:59:07Z

2011-02-25T10:54:46Z

2011-02-25T10:48:26Z

← Revisión anterior		Revisión del 09:38 22 ago 2021
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* 7ª relación de ejercicios *}		header {* 7ª relación de ejercicios *}

@@ Línea 143: / Línea 143: @@
 *}
-lemma "veces x (borraDups xs) = (if (veces x xs) \<ge> 1 then 1 else 0)"
+lemma "veces x (borraDups xs) = (if (veces x xs) >= 1 then 1 else 0)"
 by (induct xs) auto

@@ Línea 93: / Línea 93: @@
    ---------------------------------------------------------------------
 *}
 text {*
@@ Línea 139: / Línea 142: @@
    ---------------------------------------------------------------------
 *}
 text {*

@@ Línea 176: / Línea 176: @@
    ---------------------------------------------------------------------
 *}
 end
 </source>

@@ Línea 66: / Línea 66: @@
       veces a (map f xs) = veces (f a) xs
    ---------------------------------------------------------------------
 *}

@@ Línea 80: / Línea 80: @@
    Nota: La función borraDups es equivalente a la predefinida remdups.
    ---------------------------------------------------------------------
 *}

← Revisión anterior		Revisión del 10:54 25 feb 2011
Línea 88:		Línea 88:
	\| "borraDups (x#xs) = (if veces x xs > 0 then borraDups xs else (x#borraDups xs))"		\| "borraDups (x#xs) = (if veces x xs > 0 then borraDups xs else (x#borraDups xs))"

		+
		+
		+	text {*
		+	Nota: para que no muestre error la función de evaluación
		+	hay que indicarle el tipo de los elementos de la lista.
		+	Por ejemplo:
		+	value "borraDups [1::nat,2,4,2,3]"
		+	*}

← Revisión anterior		Revisión del 10:48 25 feb 2011
Línea 116:		Línea 116:
	"distintos [] = True"		"distintos [] = True"
	\| "distintos (x#xs) = (if veces x xs > 0 then False else distintos xs)"		\| "distintos (x#xs) = (if veces x xs > 0 then False else distintos xs)"
		+
		+
		+
		+	text {*
		+	Nota: para que no muestre error la función de evaluación
		+	hay que indicarle el tipo de los elementos de la lista.
		+	Por ejemplo:
		+	value "distintos [1::nat,4,1]"
		+	*}
		+
		+
		+