https://www.glc.us.es/~jalonso/RA2014/index.php?action=history&feed=atom&title=Tema_12b%3A_Razonamiento_modular
Tema 12b: Razonamiento modular - Historial de revisiones
2026-07-17T13:53:50Z
Historial de revisiones para esta página en el wiki
MediaWiki 1.31.14
https://www.glc.us.es/~jalonso/RA2014/index.php?title=Tema_12b:_Razonamiento_modular&diff=285&oldid=prev
WikiSysop: Texto reemplazado: «"isar"» por «"isabelle"»
2018-07-16T08:14:03Z
<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 08:14 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 {* T12b: Razonamiento modular mediante entornos locales *}</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 {* T12b: Razonamiento modular mediante entornos locales *}</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/RA2014/index.php?title=Tema_12b:_Razonamiento_modular&diff=275&oldid=prev
Jalonso: Página creada con '<source lang="isar"> header {* T12b: Razonamiento modular mediante entornos locales *} theory T12b_Razonamiento_modular imports Main begin text {* Basado en http://www.cs...'
2015-01-29T12:12:10Z
<p>Página creada con '<source lang="isar"> header {* T12b: Razonamiento modular mediante entornos locales *} theory T12b_Razonamiento_modular imports Main begin text {* Basado en http://www.cs...'</p>
<p><b>Página nueva</b></p><div><source lang="isar"><br />
header {* T12b: Razonamiento modular mediante entornos locales *}<br />
<br />
theory T12b_Razonamiento_modular<br />
imports Main<br />
begin<br />
<br />
text {*<br />
Basado en <br />
http://www.cse.unsw.edu.au/~kleing/teaching/thprv-04/slides/Demo14.thy<br />
*}<br />
<br />
section {* Ejemplo 1 *}<br />
<br />
locale semi =<br />
fixes prod :: "['a, 'a] => 'a" (infixl "⋅" 70)<br />
assumes assoc: "(x ⋅ y) ⋅ z = x ⋅ (y ⋅ z)"<br />
<br />
locale group = semi +<br />
fixes one ("𝟭") and inv ("_⇧-" [100] 100)<br />
assumes l_one: "𝟭 ⋅ x = x"<br />
assumes l_inv: "x⇧-⋅ x = 𝟭"<br />
<br />
lemma (in group) r_inv: <br />
"x ⋅ x⇧- = 𝟭"<br />
proof -<br />
have "x ⋅ x⇧- = 𝟭 ⋅ (x ⋅ x⇧-)" by (simp only: l_one)<br />
also have "… = (𝟭 ⋅ x) ⋅ x⇧-" by (simp only: assoc)<br />
also have "… = (((x⇧-)⇧- ⋅ x⇧-) ⋅ x) ⋅ x⇧-" by (simp only: l_inv)<br />
also have "… = ((x⇧-)⇧- ⋅ (x⇧- ⋅ x)) ⋅ x⇧-" by (simp only: assoc)<br />
also have "… = ((x⇧-)⇧- ⋅ 𝟭) ⋅ x⇧-" by (simp only: l_inv)<br />
also have "… = (x⇧-)⇧- ⋅ (𝟭 ⋅ x⇧-)" by (simp only: assoc)<br />
also have "… = (x⇧-)⇧- ⋅ x⇧-" by (simp only: l_one)<br />
also have "… = 𝟭" by (simp only: l_inv)<br />
finally show ?thesis .<br />
qed<br />
<br />
lemma (in group) r_one: <br />
"x ⋅ 𝟭 = x"<br />
proof -<br />
have "x ⋅ 𝟭 = x ⋅ (x⇧- ⋅ x)" by (simp only: l_inv)<br />
also have "… = (x ⋅ x⇧-) ⋅ x" by (simp only: assoc)<br />
also have "… = 𝟭 ⋅ x" by (simp only: r_inv)<br />
also have "… = x" by (simp only: l_one)<br />
finally show "x ⋅ 𝟭 = x" .<br />
qed<br />
<br />
lemma (in group) l_cancel [simp]: <br />
"(x ⋅ y = x ⋅ z) = (y = z)"<br />
proof<br />
assume "x ⋅ y = x ⋅ z"<br />
then have "(x⇧- ⋅ x) ⋅ y = (x⇧- ⋅ x) ⋅ z" by (simp add: assoc)<br />
then show "y = z" by (simp add: l_inv l_one)<br />
next<br />
assume "y = z"<br />
then show "x ⋅ y = x ⋅ z" by simp<br />
qed<br />
<br />
subsection {* Exportación *}<br />
<br />
thm semi.assoc group.l_cancel<br />
<br />
subsection {* Definiciones *}<br />
<br />
locale semi2 = semi +<br />
fixes rprod (infixl "⊙" 70)<br />
defines rprod_def: "rprod x y ≡ y ⋅ x "<br />
<br />
lemma (in semi2) r_assoc:<br />
"(x ⊙ y) ⊙ z = x ⊙ (y ⊙ z)"<br />
by (simp only: rprod_def assoc)<br />
<br />
thm semi2.r_assoc<br />
<br />
end<br />
</source></div>
Jalonso