https://www.glc.us.es/~jalonso/DAO/index.php?action=history&feed=atom&title=RA12_Relaci%C3%B3n_16
RA12 Relación 16 - Historial de revisiones
2026-09-20T08:06:31Z
Historial de revisiones para esta página en el wiki
MediaWiki 1.31.14
https://www.glc.us.es/~jalonso/DAO/index.php?title=RA12_Relaci%C3%B3n_16&diff=171&oldid=prev
Jalonso: Texto reemplazado: «"isar"» por «"isabelle"»
2018-07-15T11:51:34Z
<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 11:51 15 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 {* R16: Conjuntos mediante listas *}</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 {* R16: Conjuntos mediante listas *}</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/DAO/index.php?title=RA12_Relaci%C3%B3n_16&diff=122&oldid=prev
Jalonso: Página creada con '<source lang="isar"> header {* R16: Conjuntos mediante listas *} theory R16 imports Main begin text {* Los conjuntos finitos se pueden representar mediante listas. En est...'
2013-05-15T20:51:58Z
<p>Página creada con '<source lang="isar"> header {* R16: Conjuntos mediante listas *} theory R16 imports Main begin text {* Los conjuntos finitos se pueden representar mediante listas. En est...'</p>
<p><b>Página nueva</b></p><div><source lang="isar"><br />
header {* R16: Conjuntos mediante listas *}<br />
<br />
theory R16<br />
imports Main <br />
begin <br />
<br />
text {* <br />
Los conjuntos finitos se pueden representar mediante listas. En esta<br />
relación se define la unión y se demuestran algunas de sus<br />
propiedades. Análogamente se puede hacer con la intersección y<br />
diferencia. <br />
*} <br />
<br />
text {* <br />
--------------------------------------------------------------------- <br />
Ejercicio 1. Definir la función <br />
union_l :: "'a list ⇒ 'a list ⇒ 'a list"<br />
tal que (union_l xs ys) es la unión de las listas xs e ys. Por<br />
ejemplo, <br />
union_l [1,2] [2,3] = [1,2,3]<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
fun union_l :: "'a list ⇒ 'a list ⇒ 'a list" where<br />
"union_l xs ys = undefined"<br />
<br />
value "union_l [1::nat,2] [2,3]" -- "= [1,2,3]"<br />
<br />
text {* <br />
--------------------------------------------------------------------- <br />
Ejercicio 2. Demostrar o refutar<br />
set (union_l xs ys) = set xs ∪ set ys<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma set_union_l: "set (union_l xs ys) = set xs ∪ set ys"<br />
oops<br />
<br />
text {* <br />
--------------------------------------------------------------------- <br />
Ejercicio 3. Demostrar que si xs e ys no tienen elementos repetidos,<br />
entonces (union_l xs ys) tampoco los tiene.<br />
<br />
Indicación: Usar la función "distintc" de la teoría List.thy<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
lemma:<br />
assumes "distinct xs" <br />
"distinct ys" <br />
shows "distinct (union_l xs ys)"<br />
oops<br />
<br />
section {* Cuantificación sobre conjuntos *}<br />
<br />
text {* <br />
--------------------------------------------------------------------- <br />
Ejercicio 4. Definir un conjunto S para que se verifique que<br />
(∀x∈A. P x) ∧ (∀x∈ B. P x) ⟶ (∀x∈S. P x)<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
text {* <br />
--------------------------------------------------------------------- <br />
Ejercicio 5. Definir una propiedad P para que se verifique que<br />
∀x∈ A. P (f x) ⟹ ∀y∈ f ` A. Q y<br />
--------------------------------------------------------------------- <br />
*}<br />
<br />
end<br />
</source></div>
Jalonso