https://www.glc.us.es/~jalonso/RA2014/index.php?action=history&feed=atom&title=Tema_12c%3A_Automatizaci%C3%B3n 2026-07-20T23:19:29Z 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_12c:_Automatizaci%C3%B3n&diff=293&oldid=prev 2018-07-16T08:15:55Z

<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 08:15 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>header {* T12c: Automatización *}</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>header {* T12c: Automatización *}</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;"></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;"></td></tr> </table>

WikiSysop https://www.glc.us.es/~jalonso/RA2014/index.php?title=Tema_12c:_Automatizaci%C3%B3n&diff=276&oldid=prev 2015-01-29T12:13:02Z

<p>Página creada con &#039;&lt;source lang=&quot;isar&quot;&gt; header {* T12c: Automatización *} theory T12c_Automatizacion imports Main begin section {* Lógica y conjuntos *} subsection {* Demostraciones con auto ...&#039;</p> <p><b>Página nueva</b></p><div>&lt;source lang=&quot;isar&quot;&gt;<br /> header {* T12c: Automatización *}<br /> <br /> theory T12c_Automatizacion<br /> imports Main<br /> begin<br /> <br /> section {* Lógica y conjuntos *}<br /> <br /> subsection {* Demostraciones con auto *}<br /> <br /> lemma &quot;∀x. ∃y. x=y&quot;<br /> by auto<br /> <br /> lemma &quot;A ⊆ B ∩ C ⟹ A ⊆ B ∪ C&quot;<br /> by auto<br /> <br /> subsection {* Demostraciones con fastforce *}<br /> <br /> lemma &quot;⟦ ∀xs ∈ A. ∃ys. xs = ys @ ys; us:A ⟧ ⟹ ∃n. length us = n+n&quot;<br /> by fastforce<br /> <br /> text {* Nota: Obsérvese la notación de los cuantificadores acotados: *} <br /> <br /> text {* Nota: Con auto no se puede probar el lema anterior. *}<br /> <br /> subsection {* Demostraciones con blast *}<br /> <br /> text {*<br /> Nota: Muchas propiedades de la LPO y de la teoría de conjuntos se<br /> pueden demostrar automáticamente.<br /> <br /> Prop.: Si T es total, A es antisimétrica y T es un subconjunto de A,<br /> entonces A es un subconjunto de T.<br /> *}<br /> <br /> lemma AT:<br /> &quot;⟦ ∀x y. T x y ∨ T y x;<br /> ∀x y. A x y ∧ A y x ⟶ x = y;<br /> ∀x y. T x y ⟶ A x y ⟧<br /> ⟹ ∀x y. A x y ⟶ T x y&quot;<br /> by blast<br /> <br /> text {* Nota: Con auto no se puede probar el lema anterior. *}<br /> <br /> section{* Sledgehammer *}<br /> <br /> lemma &quot;⟦xs @ ys = ys @ xs; length xs = length ys⟧ ⟹ xs = ys&quot;<br /> by (metis append_eq_conv_conj)<br /> <br /> lemma &quot;R^* ⊆ (R ∪ S)^*&quot;<br /> by (metis Un_upper1 rtrancl_mono)<br /> <br /> lemma &quot;a # xs = ys @ [a] ⟹ P&quot;<br /> oops<br /> <br /> lemma &quot;xs @ ys = ys @ xs ⟹ P&quot;<br /> oops<br /> <br /> section {* Aritmética *}<br /> <br /> lemma &quot;⟦ (a::nat) ≤ x + b; 2*x &lt; c ⟧ ⟹ 2*a+1 ≤ 2*b+c&quot;<br /> by arith<br /> <br /> end<br /> &lt;/source&gt;</div>

Jalonso