https://www.glc.us.es/~jalonso/RA2013/index.php?action=history&feed=atom&title=R6
R6 - Historial de revisiones
2026-07-17T11:57:07Z
Historial de revisiones para esta página en el wiki
MediaWiki 1.31.14
https://www.glc.us.es/~jalonso/RA2013/index.php?title=R6&diff=661&oldid=prev
WikiSysop: Texto reemplazado: «isar» por «isabelle»
2018-07-16T15:46:10Z
<p>Texto reemplazado: «isar» por «isabelle»</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 15:46 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><source lang="<del class="diffchange diffchange-inline">isar</del>"></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><source lang="<ins class="diffchange diffchange-inline">isabelle</ins>"></div></td></tr>
<tr><td class='diff-marker'> </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>header {* R6: Sustitución, inversión y eliminación *}</div></td><td class='diff-marker'> </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>header {* R6: Sustitución, inversión y eliminación *}</div></td></tr>
<tr><td class='diff-marker'> </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;"></td><td class='diff-marker'> </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;"></td></tr>
</table>
WikiSysop
https://www.glc.us.es/~jalonso/RA2013/index.php?title=R6&diff=279&oldid=prev
Jalonso: Protegió «R6» ([edit=sysop] (indefinido) [move=sysop] (indefinido))
2013-12-11T21:28:27Z
<p>Protegió «<a href="/~jalonso/RA2013/index.php/R6" title="R6">R6</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 21:28 11 dic 2013</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/RA2013/index.php?title=R6&diff=277&oldid=prev
Jalonso en 21:27 11 dic 2013
2013-12-11T21:27:37Z
<p></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 21:27 11 dic 2013</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><source lang="isar></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><source lang="isar<ins class="diffchange diffchange-inline">"</ins>></div></td></tr>
<tr><td class='diff-marker'> </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>header {* R6: Sustitución, inversión y eliminación *}</div></td><td class='diff-marker'> </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>header {* R6: Sustitución, inversión y eliminación *}</div></td></tr>
<tr><td class='diff-marker'> </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;"></td><td class='diff-marker'> </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;"></td></tr>
</table>
Jalonso
https://www.glc.us.es/~jalonso/RA2013/index.php?title=R6&diff=276&oldid=prev
Jalonso: Página creada con '<source lang="isar> header {* R6: Sustitución, inversión y eliminación *} theory R6 imports Main begin section {* Sustitución, inversión y eliminación *} text {* --...'
2013-12-11T21:27:21Z
<p>Página creada con '<source lang="isar> header {* R6: Sustitución, inversión y eliminación *} theory R6 imports Main begin section {* Sustitución, inversión y eliminación *} text {* --...'</p>
<p><b>Página nueva</b></p><div><source lang="isar><br />
header {* R6: Sustitución, inversión y eliminación *}<br />
<br />
theory R6<br />
imports Main <br />
begin<br />
<br />
section {* Sustitución, inversión y eliminación *}<br />
<br />
text {* <br />
--------------------------------------------------------------------- <br />
Ejercicio 1. Definir la función <br />
sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list"<br />
tal que (sust x y zs) es la lista obtenida sustituyendo cada<br />
occurrencia de x por y en la lista zs. Por ejemplo,<br />
sust (1::nat) 2 [1,2,3,4,1,2,3,4] = [2,2,3,4,2,2,3,4]<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
fun sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where<br />
"sust x y zs = undefined"<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 2.1. Demostrar o refutar automáticamente <br />
sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 2.2. Demostrar o refutar detalladamente<br />
sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma sust_append: <br />
"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 3.1. Demostrar o refutar automáticamente<br />
rev (sust x y zs) = sust x y (rev zs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"rev(sust x y zs) = sust x y (rev zs)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 3.2. Demostrar o refutar detalladamente<br />
rev (sust x y zs) = sust x y (rev zs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma rev_sust: <br />
"rev(sust x y zs) = sust x y (rev zs)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 4. Demostrar o refutar:<br />
sust x y (sust u v zs) = sust u v (sust x y zs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"sust x y (sust u v zs) = sust u v (sust x y zs)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 5. Demostrar o refutar:<br />
sust y z (sust x y zs) = sust x z zs<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"sust y z (sust x y zs) = sust x z zs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 6. Definir la función<br />
borra :: "'a ⇒ 'a list ⇒ 'a list"<br />
tal que (borra x ys) es la lista obtenida borrando la primera<br />
ocurrencia del elemento x en la lista ys. Por ejemplo,<br />
borra (2::nat) [1,2,3,2] = [1,3,2]<br />
<br />
Nota: La función borra es equivalente a la predefinida remove1. <br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
fun borra :: "'a ⇒ 'a list ⇒ 'a list" where<br />
"borra x ys = undefined"<br />
<br />
text {* <br />
--------------------------------------------------------------------- <br />
Ejercicio 7. Definir la función<br />
borraTodas :: "'a ⇒ 'a list ⇒ 'a list"<br />
tal que (borraTodas x ys) es la lista obtenida borrando todas las<br />
ocurrencias del elemento x en la lista ys. Por ejemplo,<br />
borraTodas (2::nat) [1,2,3,2] = [1,3]<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
fun borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where<br />
"borraTodas x ys = undefined"<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 8.1. Demostrar o refutar automáticamente<br />
borra x (borraTodas x xs) = borraTodas x xs<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borra x (borraTodas x xs) = borraTodas x xs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 8.2. Demostrar o refutar detalladamente <br />
borra x (borraTodas x xs) = borraTodas x xs<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borra x (borraTodas x xs) = borraTodas x xs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 9.1. Demostrar o refutar automáticamente<br />
borraTodas x (borraTodas x xs) = borraTodas x xs<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borraTodas x (borraTodas x xs) = borraTodas x xs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 9.2. Demostrar o refutar detalladamente<br />
borraTodas x (borraTodas x xs) = borraTodas x xs<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borraTodas x (borraTodas x xs) = borraTodas x xs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 10.1. Demostrar o refutar automáticamente<br />
borraTodas x (borra x xs) = borraTodas x xs<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borraTodas x (borra x xs) = borraTodas x xs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 10.2. Demostrar o refutar detalladamente<br />
borraTodas x (borra x xs) = borraTodas x xs<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borraTodas x (borra x xs) = borraTodas x xs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 11.1. Demostrar o automáticamente<br />
borra x (borra y xs) = borra y (borra x xs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borra x (borra y xs) = borra y (borra x xs)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 11.2. Demostrar o refutar detalladamente<br />
borra x (borra y xs) = borra y (borra x xs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borra x (borra y xs) = borra y (borra x xs)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 12.1. Demostrar o refutar automáticamente<br />
borraTodas x (borra y xs) = borra y (borraTodas x xs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borraTodas x (borra y xs) = borra y (borraTodas x xs)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 12.2. Demostrar o refutar detalladamente<br />
borraTodas x (borra y xs) = borra y (borraTodas x xs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borraTodas x (borra y xs) = borra y (borraTodas x xs)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 13. Demostrar o refutar:<br />
borra y (sust x y xs) = borra x xs<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borra y (sust x y xs) = borra x xs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 14. Demostrar o refutar:<br />
borraTodas y (sust x y xs) = borraTodas x xs"<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borraTodas y (sust x y xs) = borraTodas x xs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 15.1. Demostrar o refutar automáticamente<br />
sust x y (borraTodas x zs) = borraTodas x zs<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"sust x y (borraTodas x zs) = borraTodas x zs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 15.2. Demostrar o refutar detalladamente<br />
sust x y (borraTodas x zs) = borraTodas x zs<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"sust x y (borraTodas x zs) = borraTodas x zs"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 16. Demostrar o refutar:<br />
sust x y (borraTodas z zs) = borraTodas z (sust x y zs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"sust x y (borraTodas z zs) = borraTodas z (sust x y zs)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 17. Demostrar o refutar:<br />
rev (borra x xs) = borra x (rev xs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"rev (borra x xs) = borra x (rev xs)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 18.1. Demostrar o refutar automáticamente<br />
borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 18.2. Demostrar o refutar detalladamente<br />
borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 19.1. Demostrar o refutar automáticamente<br />
rev (borraTodas x xs) = borraTodas x (rev xs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"rev (borraTodas x xs) = borraTodas x (rev xs)"<br />
oops<br />
<br />
text {*<br />
--------------------------------------------------------------------- <br />
Ejercicio 19.2. Demostrar o refutar detalladamente<br />
rev (borraTodas x xs) = borraTodas x (rev xs)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma <br />
"rev (borraTodas x xs) = borraTodas x (rev xs)"<br />
oops<br />
<br />
end <br />
</source></div>
Jalonso