Relación 5 - Historial de revisiones

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

2018-07-16T08:13:04Z

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

2014-11-20T15:11:47Z

2014-11-20T14:19:24Z

2014-11-20T14:18:35Z

2014-11-20T10:32:22Z

2014-11-20T09:19:17Z

2014-11-20T07:57:33Z

2014-11-19T15:04:22Z

2014-11-19T10:02:51Z

2014-11-19T10:00:50Z

← Revisión anterior		Revisión del 08:13 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R5: Cuantificadores sobre listas *}		header {* R5: Cuantificadores sobre listas *}

@@ Línea 19: / Línea 19: @@
 *}
---"jeshorcob,javrodviv1,juacorvic,davoremar, marnajgom, domcadgom"
+--"jeshorcob,javrodviv1,juacorvic,davoremar, marnajgom, domcadgom, carvelcab"
 fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "todos p [] = True"
@@ Línea 47: / Línea 47: @@
 (* Errata. Debe ser False el caso base seguro porque si no,
   la función devuelve siempre True*)
---"jeshorcob,javrodviv1,juacorvic,davoremar, marnajgom, domcadgom"
+--"jeshorcob,javrodviv1,juacorvic,davoremar, marnajgom, domcadgom, carvelcab"
 fun algunos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
    "algunos p [] = False"
@@ Línea 81: / Línea 81: @@
 *}
---"jeshorcob,javrodviv1,davoremar, marnajgom, domcadgom"
+--"jeshorcob,javrodviv1,davoremar, marnajgom, domcadgom, carvelcab"
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
 by (induct xs) auto
@@ Línea 110: / Línea 110: @@
 qed
--- "juacorvic, marnajgom, domcadgom" (*Muy parecida a la solución anterior*)
+-- "juacorvic, marnajgom, domcadgom, carvelcab" (*Muy parecida a la solución anterior*)
 lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
 proof (induct xs)

@@ Línea 968: / Línea 968: @@
    also have "... = (aa =a ∨  estaEn a xs) " using HI by simp
    also have "... = estaEn a (aa # xs)" using HI2 by simp (*marnajgom: te faltaba using HI2*)
    finally show "estaEn a (borraDuplicados (aa # xs)) = estaEn a (aa # xs)" by simp
 qed

@@ Línea 917: / Línea 917: @@
 qed
 text {*
    ---------------------------------------------------------------------

@@ Línea 853: / Línea 853: @@
 (*Nota: así conseguimos demostrar el caso de que el elemento 'a' no esté repetido
 en la lista. Que pasa con la demostración para el caso de una lista cuyos los elementos
-sean todos duplicados. Por ejemplo [1::1,1,1,1,1,1].
+sean todos duplicados. Por ejemplo [1::nat,1,1,1,1,1,1].
 Esto no se reduce:
    have "length (borraDuplicados (a # xs)) ≤ length (borraDuplicados xs)" by simp

@@ Línea 738: / Línea 738: @@
 -- "juacorvic"
-(*Igual pero con n paso más*)
+(*Igual pero con 1 paso más*)
 lemma length_borraDuplicados:
     "length (borraDuplicados xs) ≤ length xs"

@@ Línea 712: / Línea 712: @@
 *}
--- "javrodviv1, jeshorcob"
+-- "javrodviv1, jeshorcob, juacorvic"
 lemma "length (borraDuplicados xs) ≤ length xs"
 by (induct xs) auto
@@ Línea 737: / Línea 737: @@
 qed
 text {*
    ---------------------------------------------------------------------
@@ Línea 744: / Línea 766: @@
 *}
--- "javrodviv1"
+-- "javrodviv1, juacorvic"
 lemma "estaEn a (borraDuplicados xs) = estaEn a xs"
 by (induct xs) auto