https://www.glc.us.es/~jalonso/RA2010/index.php?action=history&feed=atom&title=Rel_8 2026-07-19T01:04:03Z Historial de revisiones para esta página en el wiki MediaWiki 1.31.14 https://www.glc.us.es/~jalonso/RA2010/index.php?title=Rel_8&diff=319&oldid=prev 2018-07-16T07:49:38Z

<p>Texto reemplazado: «&quot;isar&quot;» por «&quot;isabelle&quot;»</p> <table class="diff diff-contentalign-left" data-mw="interface"> <col class="diff-marker" /> <col class="diff-content" /> <col class="diff-marker" /> <col class="diff-content" /> <tr class="diff-title" lang="es"> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="2" style="background-color: #fff; color: #222; text-align: center;">Revisión del 07:49 16 jul 2018</td> </tr><tr><td colspan="2" class="diff-lineno" id="mw-diff-left-l1" >Línea 1:</td> <td colspan="2" class="diff-lineno">Línea 1:</td></tr> <tr><td class='diff-marker'>−</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #ffe49c; vertical-align: top; white-space: pre-wrap;"><div>&lt;source lang=&quot;<del class="diffchange diffchange-inline">isar</del>&quot;&gt;</div></td><td class='diff-marker'>+</td><td style="color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #a3d3ff; vertical-align: top; white-space: pre-wrap;"><div>&lt;source lang=&quot;<ins class="diffchange diffchange-inline">isabelle</ins>&quot;&gt;</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>theory Relacion_8</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>theory Relacion_8</div></td></tr> <tr><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>imports Main Efficient_Nat Relacion_3</div></td><td class='diff-marker'>&#160;</td><td style="background-color: #f8f9fa; color: #222; font-size: 88%; border-style: solid; border-width: 1px 1px 1px 4px; border-radius: 0.33em; border-color: #eaecf0; vertical-align: top; white-space: pre-wrap;"><div>imports Main Efficient_Nat Relacion_3</div></td></tr> </table>

Jalonso https://www.glc.us.es/~jalonso/RA2010/index.php?title=Rel_8&diff=206&oldid=prev 2011-03-01T20:18:28Z

<p>Protegió «<a href="/~jalonso/RA2010/index.php/Rel_8" title="Rel 8">Rel 8</a>» ([edit=sysop] (indefinido) [move=sysop] (indefinido))</p> <table class="diff diff-contentalign-left" data-mw="interface"> <tr class="diff-title" lang="es"> <td colspan="1" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td> <td colspan="1" style="background-color: #fff; color: #222; text-align: center;">Revisión del 20:18 1 mar 2011</td> </tr><tr><td colspan="2" class="diff-notice" lang="es"><div class="mw-diff-empty">(Sin diferencias)</div> </td></tr></table>

Jalonso https://www.glc.us.es/~jalonso/RA2010/index.php?title=Rel_8&diff=204&oldid=prev 2011-03-01T20:16:57Z

<p>Página creada con &#039;&lt;source lang=&quot;isar&quot;&gt; theory Relacion_8 imports Main Efficient_Nat Relacion_3 begin section {* Suma y aplanamiento de listas *} text {* -----------------------------------...&#039;</p> <p><b>Página nueva</b></p><div>&lt;source lang=&quot;isar&quot;&gt;<br /> theory Relacion_8<br /> imports Main Efficient_Nat Relacion_3<br /> begin <br /> <br /> section {* Suma y aplanamiento de listas *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 1. Definir la función <br /> suma :: &quot;nat list ⇒ nat&quot; <br /> tal que (suma xs) es la suma de los elementos de la lista de números<br /> naturales xs. Por ejemplo, <br /> suma [3::nat,2,4] = 9<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 2. Definir la función <br /> aplana :: &quot;&#039;a list list ⇒ &#039;a list&quot;<br /> tal que (aplana xss) es la obtenida concatenando los miembros de la <br /> lista de listas &quot;xss&quot;. Por ejemplo,<br /> aplana [[2,3], [4,5], [7,9]] = [2,3,4,5,7,9]<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 3. Demostrar o refutar<br /> length (aplana xs) = suma (map length xs)<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 4. Demostrar o refutar<br /> suma (xs @ ys) = suma xs + suma ys<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 5. Demostrar o refutar<br /> aplana (xs @ ys) = (aplana xs) @ (aplana ys)<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 6. Demostrar o refutar<br /> aplana (map rev (rev xs)) = rev (aplana xs)<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 7. Demostrar o refutar<br /> aplana (rev (map rev xs)) = rev (aplana xs)<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 8. Demostrar o refutar<br /> list_all (list_all P) xs = list_all P (aplana xs)<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 9. Demostrar o refutar<br /> aplana (rev xs) = aplana xs<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 10. Demostrar o refutar<br /> suma (rev xs) = suma xs<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {*<br /> --------------------------------------------------------------------- <br /> Ejercicio 11. Buscar un predicado P para que se verifique la siguiente <br /> propiedad <br /> list_all P xs ⟶ length xs ≤ suma xs<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 12. Demostrar o refutar<br /> algunos (algunos P) xs = algunos P (aplana xs)<br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> text {* <br /> --------------------------------------------------------------------- <br /> Ejercicio 13. Redefinir, usando la función list_all, la función<br /> algunos. Llamar la nueva función algunos2 y demostrar que es <br /> equivalente a algunos. <br /> --------------------------------------------------------------------- <br /> *}<br /> <br /> end <br /> &lt;/source&gt;</div>

Jalonso