== Temas de ''Demostración asistida por ordenador'' ==
* [http://www.cs.us.es/~jalonso/cursos/dao-12/temas/tema-1.pdf Tema 1: Panorama de la demostración asistida por ordenador].
* [[Tema 2: Programación funcional en Isabelle]].
* [[Tema 3: Razonamiento sobre programas]].
* [[Tema 4: Deducción natural proposicional con Isabelle/HOL]].

Rel 4

2012-12-18T21:55:47Z

Jalonso: Protegió «Rel 4» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

<source lang="isar">
header {* Relación 4: Argumentación proposicional *}

theory R4
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación formalizar y demostrar la corrección de
los argumentos usando sólo las reglas básicas de deducción natural de
la lógica proposicional (sin usar el método auto).

Las reglas básicas de la deducción natural son las siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
---------------------------------------------------------------------
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación.
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente
argumento
Cuando tanto la temperatura como la presión atmosférica permanecen
contantes, no llueve. La temperatura permanece constante. Por lo
tanto, en caso de que llueva, la presión atmosférica no permanece
constante.
Usar T para "La temperatura permanece constante",
P para "La presión atmosférica permanece constante" y
L para "Llueve".
------------------------------------------------------------------ *}

lemma ejercicio_1:
assumes "T ∧ P ⟶ ¬L" and
"T"
shows "L ⟶ ¬P"
proof
assume "L"
show "¬P"
proof
assume "P"
have "T ∧ P" using `T` `P` ..
have "¬L" using assms(1) `T ∧ P` ..
thus "False" using `L` ..
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar, y demostrar la corrección, del siguiente
argumento
Siempre que un número x es divisible por 10, acaba en 0. El número
x no acaba en 0. Por lo tanto, x no es divisible por 10.
Usar D para "el número es divisible por 10" y
C para "el número acaba en cero".
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar, y demostrar la corrección, del siguiente
argumento
En cierto experimento, cuando hemos empleado un fármaco A, el
paciente ha mejorado considerablemente en el caso, y sólo en el
caso, en que no se haya empleado también un fármaco B. Además, o se
ha empleado el fármaco A o se ha empleado el fármaco B. En
consecuencia, podemos afirmar que si no hemos empleado el fármaco
B, el paciente ha mejorado considerablemente.
Usar A: Hemos empleado el fármaco A.
B: Hemos empleado el fármaco B.
M: El paciente ha mejorado notablemente.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar, y demostrar la corrección, del siguiente
argumento
Si no está el mañana ni el ayer escrito, entonces no está el mañana
escrito.
Usar M: El mañana está escrito.
A: El ayer está escrito.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar, y demostrar la corrección, del siguiente
argumento
Me matan si no trabajo y si trabajo me matan. Me matan siempre me
matan.
Usar M: Me matan.
T: Trabajo.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar, y demostrar la corrección, del siguiente
argumento
Si te llamé por teléfono, entonces recibiste mi llamada y no es
cierto que no te avisé del peligro que corrías. Por consiguiente,
como te llamé, es cierto que te avisé del peligro que corrías.
Usar T: Te llamé por teléfono.
R: Recibiste mi llamada.
P: Te avisé del peligro que corrías.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar, y demostrar la corrección, del siguiente
argumento
Si no hay control de nacimientos, entonces la población crece
ilimitadamente; pero si la población crece ilimitadamente,
aumentará el índice de pobreza. Por consiguiente, si no hay control
de nacimientos, aumentará el índice de pobreza.
Usar N: Hay control de nacimientos.
P: La población crece ilimitadamente,
I: Aumentará el índice de pobreza.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente
argumento
Si el general era leal, hubiera obedecido las órdenes, y si era
inteligente las hubiera comprendido. O el general desobedeció las
órdenes o no las comprendió. Luego, el general era desleal o no era
inteligente.
Usar L: El general es leal.
O: El general obedece las órdenes.
I: El general es inteligente.
C: El general comprende las órdenes.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar, y demostrar la corrección, del siguiente
argumento
Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo
haría. Si Dios fuera incapaz de evitar el mal, no sería
omnipotente; si no quisiera evitar el mal sería malévolo. Dios no
evita el mal. Si Dios existe, es omnipotente y no es
malévolo. Luego, Dios no existe.
Usar C: Dios es capaz de evitar el mal.
Q: Dios quiere evitar el mal.
O: Dios es omnipotente.
M: Dios es malévolo.
P: Dios evita el mal.
E: Dios existe.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar, y demostrar la corrección, del siguiente
argumento
Nadie más que Pedro, Quintín y Raúl están bajo sospecha y al menos
uno es traidor. Pedro nunca trabaja sin llevar al menos un cómplice
(que puede ser Quintín o Raúl). Raúl es leal. Por lo tanto,
Pedro es traidor.
Usar p: Pedro es traidor.
q : Quintín es traidor.
r : Raúl es traidor.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar, y demostrar la corrección, del siguiente
argumento
Si la válvula está abierta o la monitorización está preparada,
entonces se envía una señal de reconocimiento y un mensaje de
funcionamiento al controlador del ordenador. Si se envía un mensaje
de funcionamiento al controlador del ordenador o el sistema está en
estado normal, entonces se aceptan las órdenes del operador. Por lo
tanto, si la válvula está abierta, entonces se aceptan las órdenes
del operador.
Usar A: La válvula está abierta.
P : La monitorización está preparada.
R : Envía una señal de reconocimiento.
F : Envía un mensaje de funcionamiento.
N : El sistema está en estado normal.
O : Se aceptan órdenes del operador.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar, y demostrar la corrección, del siguiente
argumento
Si trabajo gano dinero, pero si no trabajo gozo de la vida. Sin
embargo, si trabajo no gozo de la vida, mientras que si no trabajo
no gano dinero. Por lo tanto, gozo de la vida si y sólo si no gano
dinero.
Usar p: Trabajo
q: Gano dinero.
r: Gozo de la vida.
------------------------------------------------------------------ *}

end
</source>

Relación 4

2012-12-18T21:55:25Z

Jalonso: Página creada con '<source lang="isar"> header {* Relación 4: Argumentación proposicional *} theory R4 imports Main begin text {* -----------------------------------------------------------...'

Rel 4

2012-12-18T21:54:21Z

Jalonso:

Rel 4

2012-12-18T21:54:05Z

Jalonso: Página creada con '<source lang="isar> header {* Relación 4: Argumentación proposicional *} theory R4 imports Main begin text {* ------------------------------------------------------------...'

<source lang="isar>
header {* Relación 4: Argumentación proposicional *}

theory R4
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación formalizar y demostrar la corrección de
los argumentos usando sólo las reglas básicas de deducción natural de
la lógica proposicional (sin usar el método auto).

Las reglas básicas de la deducción natural son las siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
---------------------------------------------------------------------
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación.
*}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar, y demostrar la corrección, del siguiente
argumento
Cuando tanto la temperatura como la presión atmosférica permanecen
contantes, no llueve. La temperatura permanece constante. Por lo
tanto, en caso de que llueva, la presión atmosférica no permanece
constante.
Usar T para "La temperatura permanece constante",
P para "La presión atmosférica permanece constante" y
L para "Llueve".
------------------------------------------------------------------ *}

lemma ejercicio_1:
assumes "T ∧ P ⟶ ¬L" and
"T"
shows "L ⟶ ¬P"
proof
assume "L"
show "¬P"
proof
assume "P"
have "T ∧ P" using `T` `P` ..
have "¬L" using assms(1) `T ∧ P` ..
thus "False" using `L` ..
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar, y demostrar la corrección, del siguiente
argumento
Siempre que un número x es divisible por 10, acaba en 0. El número
x no acaba en 0. Por lo tanto, x no es divisible por 10.
Usar D para "el número es divisible por 10" y
C para "el número acaba en cero".
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar, y demostrar la corrección, del siguiente
argumento
En cierto experimento, cuando hemos empleado un fármaco A, el
paciente ha mejorado considerablemente en el caso, y sólo en el
caso, en que no se haya empleado también un fármaco B. Además, o se
ha empleado el fármaco A o se ha empleado el fármaco B. En
consecuencia, podemos afirmar que si no hemos empleado el fármaco
B, el paciente ha mejorado considerablemente.
Usar A: Hemos empleado el fármaco A.
B: Hemos empleado el fármaco B.
M: El paciente ha mejorado notablemente.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar, y demostrar la corrección, del siguiente
argumento
Si no está el mañana ni el ayer escrito, entonces no está el mañana
escrito.
Usar M: El mañana está escrito.
A: El ayer está escrito.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar, y demostrar la corrección, del siguiente
argumento
Me matan si no trabajo y si trabajo me matan. Me matan siempre me
matan.
Usar M: Me matan.
T: Trabajo.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar, y demostrar la corrección, del siguiente
argumento
Si te llamé por teléfono, entonces recibiste mi llamada y no es
cierto que no te avisé del peligro que corrías. Por consiguiente,
como te llamé, es cierto que te avisé del peligro que corrías.
Usar T: Te llamé por teléfono.
R: Recibiste mi llamada.
P: Te avisé del peligro que corrías.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar, y demostrar la corrección, del siguiente
argumento
Si no hay control de nacimientos, entonces la población crece
ilimitadamente; pero si la población crece ilimitadamente,
aumentará el índice de pobreza. Por consiguiente, si no hay control
de nacimientos, aumentará el índice de pobreza.
Usar N: Hay control de nacimientos.
P: La población crece ilimitadamente,
I: Aumentará el índice de pobreza.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente
argumento
Si el general era leal, hubiera obedecido las órdenes, y si era
inteligente las hubiera comprendido. O el general desobedeció las
órdenes o no las comprendió. Luego, el general era desleal o no era
inteligente.
Usar L: El general es leal.
O: El general obedece las órdenes.
I: El general es inteligente.
C: El general comprende las órdenes.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar, y demostrar la corrección, del siguiente
argumento
Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo
haría. Si Dios fuera incapaz de evitar el mal, no sería
omnipotente; si no quisiera evitar el mal sería malévolo. Dios no
evita el mal. Si Dios existe, es omnipotente y no es
malévolo. Luego, Dios no existe.
Usar C: Dios es capaz de evitar el mal.
Q: Dios quiere evitar el mal.
O: Dios es omnipotente.
M: Dios es malévolo.
P: Dios evita el mal.
E: Dios existe.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar, y demostrar la corrección, del siguiente
argumento
Nadie más que Pedro, Quintín y Raúl están bajo sospecha y al menos
uno es traidor. Pedro nunca trabaja sin llevar al menos un cómplice
(que puede ser Quintín o Raúl). Raúl es leal. Por lo tanto,
Pedro es traidor.
Usar p: Pedro es traidor.
q : Quintín es traidor.
r : Raúl es traidor.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar, y demostrar la corrección, del siguiente
argumento
Si la válvula está abierta o la monitorización está preparada,
entonces se envía una señal de reconocimiento y un mensaje de
funcionamiento al controlador del ordenador. Si se envía un mensaje
de funcionamiento al controlador del ordenador o el sistema está en
estado normal, entonces se aceptan las órdenes del operador. Por lo
tanto, si la válvula está abierta, entonces se aceptan las órdenes
del operador.
Usar A: La válvula está abierta.
P : La monitorización está preparada.
R : Envía una señal de reconocimiento.
F : Envía un mensaje de funcionamiento.
N : El sistema está en estado normal.
O : Se aceptan órdenes del operador.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar, y demostrar la corrección, del siguiente
argumento
Si trabajo gano dinero, pero si no trabajo gozo de la vida. Sin
embargo, si trabajo no gozo de la vida, mientras que si no trabajo
no gano dinero. Por lo tanto, gozo de la vida si y sólo si no gano
dinero.
Usar p: Trabajo
q: Gano dinero.
r: Gozo de la vida.
------------------------------------------------------------------ *}

end
</source>

Ejercicios

2012-12-18T21:52:53Z

Jalonso: /* Ejercicios de Demostración asistida por ordenador */

== Ejercicios de ''Demostración asistida por ordenador'' ==
En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por los alumnos del curso y no deben tomarse como definitivas.
* '''Relación 1''': Programación funcional en Isabelle. ([[Rel_1 |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Razonamiento sobre programas. ([[Rel_2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Argumentación proposicional. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).

Rel 3

2012-12-18T17:48:20Z

Jalonso: Protegió «Rel 3» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Relación 3

2012-12-18T17:48:01Z

Jalonso: Página creada con '<source lang="isar"> header {* Relación 3: Deducción natural proposicional *} theory DNLP imports Main begin text {* -----------------------------------------------------...'

Rel 3

2012-12-18T17:47:16Z

Ejercicios

2012-12-18T17:46:01Z

Jalonso: /* Ejercicios de Demostración asistida por ordenador */

== Ejercicios de ''Demostración asistida por ordenador'' ==
En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por los alumnos del curso y no deben tomarse como definitivas.
* '''Relación 1''': Programación funcional en Isabelle. ([[Rel_1 |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Razonamiento sobre programas. ([[Rel_2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).

Tema 4: Deducción natural en lógica proposicional con Isabelle/HOL

2012-12-18T17:07:58Z

Jalonso:

Tema 4: Deducción natural en lógica proposicional con Isabelle/HOL

2012-12-18T17:03:28Z

Jalonso: Página creada con '<source lang="isar"> header {* Tema 4: Deducción natural en lógica proposicional con Isabelle/HOL *} theory DNLP imports Main begin text {* En esta sección se presentan ...'

<source lang="isar">
header {* Tema 4: Deducción natural en lógica proposicional con Isabelle/HOL *}

theory DNLP
imports Main
begin

text {*
En esta sección se presentan los ejemplos del tema de deducción natural
proposicional siguiendo la presentación de Huth y Ryan en su libro
"Logic in Computer Science" http://goo.gl/qsVpY y, más concretamente,
a la forma como se explica en la asignatura de "Lógica informática" (LI)
http://goo.gl/AwDiv

La página al lado de cada ejemplo indica la página de las transparencias
de LI donde se encuentra la demostración. *}

subsection {* Reglas de la conjunción *}

text {*
Ejemplo 1 (p. 4). Demostrar que
p ∧ q, r ⊢ q ∧ r.
*}

-- "La demostración detallada es"
lemma ejemplo_1_1:
assumes 1: "p ∧ q" and
2: "r"
shows "q ∧ r"
proof -
have 3: "q" using 1 by (rule conjunct2)
show 4: "q ∧ r" using 3 2 by (rule conjI)
qed

text {*
Notas sobre el lenguaje: En la demostración anterior se ha usado
· "assumes" para indicar las hipótesis,
· "and" para separar las hipótesis,
· "shows" para indicar la conclusión,
· "proof" para iniciar la prueba,
· "qed" para terminar la pruebas,
· "-" (después de "proof") para no usar el método por defecto,
· "have" para establecer un paso,
· "using" para usar hechos en un paso,
· "by (rule ..)" para indicar la regla con la que se peueba un hecho,
· "show" para establecer la conclusión.

Notas sobre la lógica: Las reglas de la conjunción son
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
*}

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_2:
assumes 1: "p ∧ q" and
2: "r"
shows "q ∧ r"
proof -
have 3: "q" using 1 ..
show 4: "q ∧ r" using 3 2 ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· ".." para indicar que se prueba por la regla correspondiente. *}

text {* Se pueden eliminar las etiquetas como sigue *}

lemma ejemplo_1_3:
assumes "p ∧ q"
and "r"
shows "q ∧ r"
proof -
have "q" using assms(1) ..
thus "q ∧ r" using assms(2) ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "assms(n)" para indicar la hipótesis n y
· "thus" para demostrar la conclusión usando el hecho anterior. *}

text {* Se puede automatizar la demostración como sigue *}

lemma ejemplo_1_4:
assumes "p ∧ q"
and "r"
shows "q ∧ r"
using assms
by auto

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "assms" para indicar las hipótesis y
· "by auto" para demostrar la conclusión automáticamente. *}

text {* Se puede automatizar totalmente la demostración como sigue *}

lemma ejemplo_1_5:
"⟦p ∧ q; r⟧ ⟹ q ∧ r"
by auto

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "⟦ ... ⟧" para representar las hipótesis,
· ";" para separar las hipótesis y
· "⟹" para separar las hipótesis de la conclusión. *}

text {* Se puede hacer la demostración por razonamiento hacia atrás,
como sigue *}

lemma ejemplo_1_6:
assumes "p ∧ q"
and "r"
shows "q ∧ r"
proof (rule conjI)
show "q" using assms(1) by (rule conjunct2)
next
show "r" using assms(2) by this
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "proof (rule r)" para indicar que se hará la demostración con la
regla r,
· "next" para indicar el comienzo de la prueba del siguiente
subobjetivo,
· "this" para indicar el hecho actual. *}

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_7:
assumes "p ∧ q"
and "r"
shows "q ∧ r"
proof
show "q" using assms(1) ..
next
show "r" using assms(2) .
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "." para indicar por el hecho actual. *}

subsection {* Reglas de la doble negación *}

text {*
La regla de eliminación de la doble negación es
· notnotD: ¬¬ P ⟹ P

Para ajustarnos al tema de LI vamos a introducir la siguiente regla de
introducción de la doble negación
· notnotI: P ⟹ ¬¬ P
aunque, de momento, no detallamos su demostración.
*}

lemma notnotI [intro!]: "P ⟹ ¬¬ P"
by auto

text {*
Ejemplo 2. (p. 5)
p, ¬¬(q ∧ r) ⊢ ¬¬p ∧ r
*}

-- "La demostración detallada es"
lemma ejemplo_2_1:
assumes 1: "p"
and 2: "¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof -
have 3: "¬¬p" using 1 by (rule notnotI)
have 4: "q ∧ r" using 2 by (rule notnotD)
have 5: "r" using 4 by (rule conjunct2)
show 6: "¬¬p ∧ r" using 3 5 by (rule conjI)
qed

-- "La demostración estructurada es"
lemma ejemplo_2_2:
assumes "p"
and "¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof -
have "¬¬p" using assms(1) ..
have "q ∧ r" using assms(2) by (rule notnotD)
hence "r" ..
show "¬¬p ∧ r" using `¬¬p` `r` ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "hence" para indicar que se tiene por el hecho anterior y
· `...` para referenciar un hecho. *}

-- "La demostración automática es"
lemma ejemplo_2_3:
assumes "p"
and "¬¬(q ∧ r)"
shows "¬¬p ∧ r"
using assms
by auto

text {* Se puede demostrar hacia atrás *}

lemma ejemplo_2_4:
assumes "p"
and "¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof (rule conjI)
show "¬¬p" using assms(1) by (rule notnotI)
next
have "q ∧ r" using assms(2) by (rule notnotD)
thus "r" by (rule conjunct2)
qed

text {* Se puede eliminar las reglas en la demostración anterior, como
sigue: *}

lemma ejemplo_2_5:
assumes "p"
and "¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof
show "¬¬p" using assms(1) ..
next
have "q ∧ r" using assms(2) by (rule notnotD)
thus "r" ..
qed

subsection {* Regla de eliminación del condicional *}

text {*
La regla de eliminación del condicional es la regla del modus ponens
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
*}

text {*
Ejemplo 3. (p. 6) Demostar que
¬p ∧ q, ¬p ∧ q ⟶ r ∨ ¬p ⊢ r ∨ ¬p

*}

-- "La demostración detallada es"
lemma ejemplo_3_1:
assumes 1: "¬p ∧ q" and
2: "¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
proof -
show "r ∨ ¬p" using 2 1 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejemplo_3_2:
assumes 1: "¬p ∧ q" and
2: "¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
proof -
show "r ∨ ¬p" using 2 1 ..
qed

-- "La demostración automática es"
lemma ejemplo_3_3:
assumes "¬p ∧ q" and
"¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
using assms
by auto

text {*
Ejemplo 4 (p. 6) Demostrar que
p, p ⟶ q, p ⟶ (q ⟶ r) ⊢ r
*}

-- "La demostración detallada es"
lemma ejemplo_4_1:
assumes 1: "p" and
2: "p ⟶ q" and
3: "p ⟶ (q ⟶ r)"
shows "r"
proof -
have 4: "q" using 2 1 by (rule mp)
have 5: "q ⟶ r" using 3 1 by (rule mp)
show 6: "r" using 5 4 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejemplo_4_2:
assumes 1: "p" and
2: "p ⟶ q" and
3: "p ⟶ (q ⟶ r)"
shows "r"
proof -
have 4: "q" using 2 1 ..
have "q ⟶ r" using 3 1 ..
thus "r" using 4 ..
qed

-- "La demostración automática es"
lemma ejemplo_4_3:
"⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r"
by auto

subsection {* Regla derivada del modus tollens *}

text {*
Para ajustarnos al tema de LI vamos a introducir la regla del modus
tollens
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
aunque, de momento, sin detallar su demostración.
*}

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text {*
Ejemplo 5 (p. 7). Demostrar
p ⟶ (q ⟶ r), p, ¬r ⊢ ¬q
*}

-- "La demostración detallada es"
lemma ejemplo_5_1:
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p" and
3: "¬r"
shows "¬q"
proof -
have 4: "q ⟶ r" using 1 2 by (rule mp)
show "¬q" using 4 3 by (rule mt)
qed

-- "La demostración estructurada es"
lemma ejemplo_5_2:
assumes "p ⟶ (q ⟶ r)" and
"p" and
"¬r"
shows "¬q"
proof -
have "q ⟶ r" using assms(1) assms(2) ..
thus "¬q" using assms(3) by (rule mt)
qed

-- "La demostración automática es"
lemma ejemplo_5_3:
assumes "p ⟶ (q ⟶ r)" and
"p" and
"¬r"
shows "¬q"
using assms
by auto

text {*
Ejemplo 6. (p. 7) Demostrar
¬p ⟶ q, ¬q ⊢ p
*}

-- "La demostración detallada es"
lemma ejemplo_6_1:
assumes 1: "¬p ⟶ q" and
2: "¬q"
shows "p"
proof -
have 3: "¬¬p" using 1 2 by (rule mt)
show "p" using 3 by (rule notnotD)
qed

-- "La demostración automática es"
lemma ejemplo_6_2:
"⟦¬p ⟶ q; ¬q⟧ ⟹ p"
by auto

text {*
Ejercicio 7. (p. 7) Demostrar
p ⟶ ¬q, q ⊢ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_7_1:
assumes 1: "p ⟶ ¬q" and
2: "q"
shows "¬p"
proof -
have 3: "¬¬q" using 2 by (rule notnotI)
show "¬p" using 1 3 by (rule mt)
qed

-- "La demostración automática es"
lemma ejemplo_7_2:
"⟦p ⟶ ¬q; q⟧ ⟹ ¬p"
by auto

subsection {* Regla de introducción del condicional *}

text {*
La regla de introducción del condicional es
· impI: (P ⟹ Q) ⟹ P ⟶ Q
*}

text {*
Ejemplo 8. (p. 8) Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_8_1:
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof -
{ assume 2: "¬q"
have "¬p" using 1 2 by (rule mt) }
thus "¬q ⟶ ¬p" by (rule impI)
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "{ ... }" para representar una caja. *}

-- "La demostración detallada es"
lemma ejemplo_8_2:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof
assume "¬q"
show "¬p" using assms `¬q` by (rule mt)
qed

-- "La demostración automática es"
lemma ejemplo_8_3:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
using assms
by auto

text {*
Ejemplo 9. (p. 9) Demostrar
¬q ⟶ ¬p ⊢ p ⟶ ¬¬q
*}

-- "La demostración detallada es"
lemma ejemplo_9_1:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
proof -
{ assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
have "¬¬q" using 1 3 by (rule mt) }
thus "p ⟶ ¬¬q" by (rule impI)
qed

-- "La demostración hacia atrás es"
lemma ejemplo_9_2:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
proof (rule impI)
assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
show "¬¬q" using 1 3 by (rule mt)
qed

-- "La demostración automática es"
lemma ejemplo_9_3:
assumes "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
using assms
by auto

text {*
Ejemplo 10 (p. 9). Demostrar
⊢ p ⟶ p
*}

-- "La demostración detallada es"
lemma ejemplo_10_1:
"p ⟶ p"
proof -
{ assume 1: "p"
have "p" using 1 by this }
thus "p ⟶ p" by (rule impI)
qed

-- "La demostración hacia atrás es"
lemma ejemplo_10_2:
"p ⟶ p"
proof (rule impI)
qed

-- "La demostración automática es"
lemma ejemplo_10_3:
"p ⟶ p"
by auto

text {*
Ejemplo 11 (p. 10) Demostrar
⊢ (q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))
*}

-- "La demostración detallada es"
lemma ejemplo_11_1:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof -
{ assume 1: "q ⟶ r"
{ assume 2: "¬q ⟶ ¬p"
{ assume 3: "p"
have 4: "¬¬p" using 3 by (rule notnotI)
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
have "r" using 1 6 by (rule mp) }
hence "p ⟶ r" by (rule impI) }
hence "(¬q ⟶ ¬p) ⟶ p ⟶ r" by (rule impI) }
thus "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ p ⟶ r)" by (rule impI)
qed

-- "La demostración hacia atrás es"
lemma ejemplo_11_2:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "q ⟶ r"
show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "¬q ⟶ ¬p"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "¬¬p" using 3 by (rule notnotI)
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
show "r" using 1 6 by (rule mp)
qed
qed
qed

-- "La demostración hacia atrás con reglas implícitas es"
lemma ejemplo_11_3:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof
assume 1: "q ⟶ r"
show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
proof
assume 2: "¬q ⟶ ¬p"
show "p ⟶ r"
proof
assume 3: "p"
have 4: "¬¬p" using 3 ..
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
show "r" using 1 6 ..
qed
qed
qed

-- "La demostración automática es"
lemma ejemplo_11_4:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
by auto

subsection {* Reglas de la disyunción *}

text {*
Las reglas de la introducción de la disyunción son
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
La regla de elimación de la disyunción es
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
*}

text {*
Ejemplo 12 (p. 11). Demostrar
p ∨ q ⊢ q ∨ p
*}

-- "La demostración detallada es"
lemma ejemplo_12_1:
assumes "p ∨ q"
shows "q ∨ p"
proof -
have "p ∨ q" using assms by this
moreover
{ assume 2: "p"
have "q ∨ p" using 2 by (rule disjI2) }
moreover
{ assume 3: "q"
have "q ∨ p" using 3 by (rule disjI1) }
ultimately show "q ∨ p" by (rule disjE)
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "moreover" para separar los bloques y
· "ultimately" para unir los resultados de los bloques. *}

-- "La demostración detallada con reglas implícitas es"
lemma ejemplo_12_2:
assumes "p ∨ q"
shows "q ∨ p"
proof -
note `p ∨ q`
moreover
{ assume "p"
hence "q ∨ p" .. }
moreover
{ assume "q"
hence "q ∨ p" .. }
ultimately show "q ∨ p" ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "note" para copiar un hecho. *}

-- "La demostración hacia atrás es"
lemma ejemplo_12_3:
assumes 1: "p ∨ q"
shows "q ∨ p"
using 1
proof (rule disjE)
{ assume 2: "p"
show "q ∨ p" using 2 by (rule disjI2) }
next
{ assume 3: "q"
show "q ∨ p" using 3 by (rule disjI1) }
qed

-- "La demostración hacia atrás con reglas implícitas es"
lemma ejemplo_12_4:
assumes "p ∨ q"
shows "q ∨ p"
using assms
proof
{ assume "p"
thus "q ∨ p" .. }
next
{ assume "q"
thus "q ∨ p" .. }
qed

-- "La demostración automática es"
lemma ejemplo_12_5:
assumes "p ∨ q"
shows "q ∨ p"
using assms
by auto

text {*
Ejemplo 13. (p. 12) Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
*}

-- "La demostración detallada es"
lemma ejemplo_13_1:
assumes 1: "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
assume 2: "p ∨ q"
thus "p ∨ r"
proof (rule disjE)
{ assume 3: "p"
show "p ∨ r" using 3 by (rule disjI1) }
next
{ assume 4: "q"
have 5: "r" using 1 4 by (rule mp)
show "p ∨ r" using 5 by (rule disjI2) }
qed
qed

-- "La demostración estructurada es"
lemma ejemplo_13_2:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof
assume "p ∨ q"
thus "p ∨ r"
proof
{ assume "p"
thus "p ∨ r" .. }
next
{ assume "q"
have "r" using assms `q` ..
thus "p ∨ r" .. }
qed
qed

-- "La demostración automática es"
lemma ejemplo_13_3:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
using assms
by auto

subsection {* Regla de copia *}

text {*
Ejemplo 14 (p. 13). Demostrar
⊢ p ⟶ (q ⟶ p)
*}

-- "La demostración detallada es"
lemma ejemplo_14_1:
"p ⟶ (q ⟶ p)"
proof (rule impI)
assume 1: "p"
show "q ⟶ p"
proof (rule impI)
assume "q"
show "p" using 1 by this
qed
qed

-- "La demostración detallada es"
lemma ejemplo_14_2:
"p ⟶ (q ⟶ p)"
proof
assume "p"
thus "q ⟶ p" ..
qed

-- "La demostración automática es"
lemma ejemplo_14_3:
"p ⟶ (q ⟶ p)"
by auto

subsection {* Reglas de la negación *}

text {*
La regla de eliminación de lo falso es
· FalseE: False ⟹ P
La regla de eliminación de la negación es
· notE: ⟦¬P; P⟧ ⟹ R
La regla de introducción de la negación es
· notI: (P ⟹ False) ⟹ ¬P
*}

text {*
Ejemplo 15 (p. 15). Demostrar
¬p ∨ q ⊢ p ⟶ q
*}

-- "La demostración detallada es"
lemma ejemplo_15_1:
assumes 1: "¬p ∨ q"
shows "p ⟶ q"
proof (rule impI)
assume 2: "p"
note 1
thus "q"
proof (rule disjE)
{ assume 3: "¬p"
show "q" using 3 2 by (rule notE) }
next
{ assume 4: "q"
show "q" using 4 by this}
qed
qed

-- "La demostración estructurada es"
lemma ejemplo_15_2:
assumes "¬p ∨ q"
shows "p ⟶ q"
proof
assume "p"
note `¬p ∨ q`
thus "q"
proof
{ assume "¬p"
thus "q" using `p` .. }
next
{ assume "q"
thus "q" . }
qed
qed

-- "La demostración automática es"
lemma ejemplo_15_3:
assumes "¬p ∨ q"
shows "p ⟶ q"
using assms
by auto

text {*
Ejemplo 16 (p. 16). Demostrar
p ⟶ q, p ⟶ ¬q ⊢ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_16_1:
assumes 1: "p ⟶ q" and
2: "p ⟶ ¬q"
shows "¬p"
proof (rule notI)
assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "¬q" using 2 3 by (rule mp)
show False using 5 4 by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_16_2:
assumes "p ⟶ q" and
"p ⟶ ¬q"
shows "¬p"
proof
assume "p"
have "q" using assms(1) `p` ..
have "¬q" using assms(2) `p` ..
thus False using `q` ..
qed

-- "La demostración automática es"
lemma ejemplo_16_3:
assumes "p ⟶ q" and
"p ⟶ ¬q"
shows "¬p"
using assms
by auto

subsection {* Reglas del bicondicional *}

text {*
La regla de introducción del bicondicional es
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P ⟷ Q
Las reglas de eliminación del bicondicional son
· iffD1: ⟦Q ⟷ P; Q⟧ ⟹ P
· iffD2: ⟦P ⟷ Q; Q⟧ ⟹ P
*}

text {*
Ejemplo 17 (p. 17) Demostrar
*}

-- "La demostración detallada es"
lemma ejemplo_17_1:
"(p ∧ q) ⟷ (q ∧ p)"
proof (rule iffI)
{ assume 1: "p ∧ q"
have 2: "p" using 1 by (rule conjunct1)
have 3: "q" using 1 by (rule conjunct2)
show "q ∧ p" using 3 2 by (rule conjI) }
next
{ assume 4: "q ∧ p"
have 5: "q" using 4 by (rule conjunct1)
have 6: "p" using 4 by (rule conjunct2)
show "p ∧ q" using 6 5 by (rule conjI) }
qed

-- "La demostración estructurada es"
lemma ejemplo_17_2:
"(p ∧ q) ⟷ (q ∧ p)"
proof
{ assume 1: "p ∧ q"
have 2: "p" using 1 ..
have 3: "q" using 1 ..
show "q ∧ p" using 3 2 .. }
next
{ assume 4: "q ∧ p"
have 5: "q" using 4 ..
have 6: "p" using 4 ..
show "p ∧ q" using 6 5 .. }
qed

-- "La demostración automática es"
lemma ejemplo_17_3:
"(p ∧ q) ⟷ (q ∧ p)"
by auto

text {*
Ejemplo 18 (p. 18). Demostrar
p ⟷ q, p ∨ q ⊢ p ∧ q
*}

-- "La demostración detallada es"
lemma ejemplo_18_1:
assumes 1: "p ⟷ q" and
2: "p ∨ q"
shows "p ∧ q"
using 2
proof (rule disjE)
{ assume 3: "p"
have 4: "q" using 1 3 by (rule iffD1)
show "p ∧ q" using 3 4 by (rule conjI) }
next
{ assume 5: "q"
have 6: "p" using 1 5 by (rule iffD2)
show "p ∧ q" using 6 5 by (rule conjI) }
qed

-- "La demostración estructurada es"
lemma ejemplo_18_2:
assumes 1: "p ⟷ q" and
2: "p ∨ q"
shows "p ∧ q"
using 2
proof
{ assume 3: "p"
have 4: "q" using 1 3 ..
show "p ∧ q" using 3 4 .. }
next
{ assume 5: "q"
have 6: "p" using 1 5 ..
show "p ∧ q" using 6 5 .. }
qed

-- "La demostración estructurada es"
lemma ejemplo_18_3:
assumes "p ⟷ q" and
"p ∨ q"
shows "p ∧ q"
using assms
by auto

subsection {* Reglas derivadas *}

subsubsection {* Regla del modus tollens *}

text {*
Ejemplo 19 (p. 20) Demostrar la regla del modus tollens a partir de
las reglas básicas.
*}

-- "La demostración detallada es"
lemma ejemplo_20_1:
assumes 1: "F ⟶ G" and
2: "¬G"
shows "¬F"
proof (rule notI)
assume 3: "F"
have 4: "G" using 1 3 by (rule mp)
show False using 2 4 by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_20_2:
assumes 1: "F ⟶ G" and
2: "¬G"
shows "¬F"
proof
assume 3: "F"
have 4: "G" using 1 3 ..
show False using 2 4 ..
qed

-- "La demostración automática es"
lemma ejemplo_20_3:
assumes "F ⟶ G" and
"¬G"
shows "¬F"
using assms
by auto

subsubsection {* Regla de la introducción de la doble negación *}

text {*
Ejemplo 21 (p. 21) Demostrar la regla de introducción de la doble
negación a partir de las reglas básicas.
*}

-- "La demostración detallada es"
lemma ejemplo_21_1:
assumes 1: "F"
shows "¬¬F"
proof (rule notI)
assume 2: "¬F"
show False using 2 1 by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_21_2:
assumes "F"
shows "¬¬F"
proof
assume "¬F"
thus False using assms ..
qed

-- "La demostración automática es"
lemma ejemplo_21_3:
assumes "F"
shows "¬¬F"
using assms
by auto

subsubsection {* Regla de reducción al absurdo *}

text {*
La regla de reducción al absurdo en Isabelle se correponde con la
regla clásica de contradicción
· ccontr: (¬P ⟹ False) ⟹ P
*}

subsubsection {* Ley del tercio excluso *}

text {*
La ley del tercio excluso es
· excluded_middle: ¬P ∨ P
*}

text {*
Ejemplo 22 (p. 23). Demostrar la ley del tercio excluso a partir de
las reglas básicas.
*}

-- "La demostración detallada es"
lemma ejemplo_22_1:
"F ∨ ¬F"
proof (rule ccontr)
assume 1: "¬(F ∨ ¬F)"
thus False
proof (rule notE)
show "F ∨ ¬F"
proof (rule disjI2)
show "¬F"
proof (rule notI)
assume 2: "F"
hence 3: "F ∨ ¬F" by (rule disjI1)
show False using 1 3 by (rule notE)
qed
qed
qed
qed

-- "La demostración automática es"
lemma ejemplo_22_2:
"F ∨ ¬F"
using assms
by auto

text {*
Ejemplo 23 (p. 24). Demostrar
p ⟶ q ⊢ ¬p ∨ q
*}

-- "La demostración detallada es"
lemma ejemplo_23_1:
assumes 1: "p ⟶ q"
shows "¬p ∨ q"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "¬p ∨ q"
proof (rule disjE)
{ assume "¬p"
thus "¬p ∨ q" by (rule disjI1) }
next
{ assume 2: "p"
have "q" using 1 2 by (rule mp)
thus "¬p ∨ q" by (rule disjI2) }
qed
qed

-- "La demostración estructurada es"
lemma ejemplo_23_2:
assumes "p ⟶ q"
shows "¬p ∨ q"
proof -
have "¬p ∨ p" ..
thus "¬p ∨ q"
proof
{ assume "¬p"
thus "¬p ∨ q" .. }
next
{ assume "p"
have "q" using assms `p` ..
thus "¬p ∨ q" .. }
qed
qed

-- "La demostración automática es"
lemma ejemplo_23_3:
assumes "p ⟶ q"
shows "¬p ∨ q"
using assms
by auto

end
</source>

Relación 1

2012-11-28T16:56:32Z

Jalonso:

<source lang="isar">
header {* Definición de funciones *}

theory Definicion_de_funciones
imports Main
begin

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud xs = undefined"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Definir la función
intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = undefined"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 3. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa xs = undefined"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejercicio 4. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite n x = undefined"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc xs ys = undefined"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n xs = undefined"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n xs = undefined"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia xs = undefined"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux xs ys = undefined"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = undefined"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejercicio 10. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum xs = undefined"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 11. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f xs = undefined"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

end
</source>

Relación 2

2012-11-27T16:51:57Z

Jalonso: Página creada con '<source lang="isar"> header {* Relación 2: Razonamiento sobre programas *} theory R2_Razonamiento_sobre_programas imports Main begin text {* --------------------------------...'

<source lang="isar">
header {* Relación 2: Razonamiento sobre programas *}

theory R2_Razonamiento_sobre_programas
imports Main
begin

text {* ---------------------------------------------------------------
Ejercicio 1. Definir la función
sumaImpares :: nat ⇒ nat
tal que (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 5 = 25
------------------------------------------------------------------ *}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares n = undefined"

value "sumaImpares 5" -- "= 25"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
sumaImpares n = n*n
------------------------------------------------------------------- *}

lemma "sumaImpares n = n*n"
oops

text {* ---------------------------------------------------------------
Ejercicio 3. Definir la función
sumaPotenciasDeDosMasUno :: nat ⇒ nat
tal que
(sumaPotenciasDeDosMasUno n) = 1 + 2^0 + 2^1 + 2^2 + ... + 2^n.
Por ejemplo,
sumaPotenciasDeDosMasUno 3 = 16
------------------------------------------------------------------ *}

fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno n = undefined"

value "sumaPotenciasDeDosMasUno 3" -- "= 16"

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
sumaPotenciasDeDosMasUno n = 2^(n+1)
------------------------------------------------------------------- *}

lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
oops

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
copia :: nat ⇒ 'a ⇒ 'a list
tal que (copia n x) es la lista formado por n copias del elemento
x. Por ejemplo,
copia 3 x = [x,x,x]
------------------------------------------------------------------ *}

fun copia :: "nat ⇒ 'a ⇒ 'a list" where
"copia n x = undefined"

value "copia 3 x" -- "= [x,x,x]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
tal que (todos p xs) se verifica si todos los elementos de xs cumplen
la propiedad p. Por ejemplo,
todos (λx. x>(1::nat)) [2,6,4] = True
todos (λx. x>(2::nat)) [2,6,4] = False
Nota: La conjunción se representa por ∧
----------------------------------------------------------------- *}

fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos p xs = undefined"

value "todos (λx. x>(1::nat)) [2,6,4]" -- "= True"
value "todos (λx. x>(2::nat)) [2,6,4]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar que todos los elementos de (copia n x) son
iguales a x.
------------------------------------------------------------------- *}

lemma "todos (λy. y=x) (copia n x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
factR :: nat ⇒ nat
tal que (factR n) es el factorial de n. Por ejemplo,
factR 4 = 24
------------------------------------------------------------------ *}

fun factR :: "nat ⇒ nat" where
"factR n = undefined"

value "factR 4" -- "= 24"

text {* ---------------------------------------------------------------
Ejercicio 9. Se considera la siguiente definición iterativa de la
función factorial
factI :: "nat ⇒ nat" where
factI n = factI' n 1

factI' :: nat ⇒ nat ⇒ nat" where
factI' 0 x = x
factI' (Suc n) x = factI' n (Suc n)*x
Demostrar que, para todo n y todo x, se tiene
factI' n x = x * factR n
------------------------------------------------------------------- *}

fun factI' :: "nat ⇒ nat ⇒ nat" where
"factI' 0 x = x"
| "factI' (Suc n) x = factI' n (Suc n)*x"

fun factI :: "nat ⇒ nat" where
"factI n = factI' n 1"

value "factI 4" -- "= 24"

lemma fact: "factI' n x = x * factR n"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
factI n = factR n
------------------------------------------------------------------- *}

corollary "factI n = factR n"
oops

text {* ---------------------------------------------------------------
Ejercicio 11. Definir, recursivamente y sin usar (@), la función
amplia :: 'a list ⇒ 'a ⇒ 'a list
tal que (amplia xs y) es la lista obtenida añadiendo el elemento y al
final de la lista xs. Por ejemplo,
amplia [d,a] t = [d,a,t]
------------------------------------------------------------------ *}

fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia xs y = undefined"

value "amplia [d,a] t" -- "= [d,a,t]"

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
amplia xs y = xs @ [y]
------------------------------------------------------------------- *}

lemma "amplia xs y = xs @ [y]"
oops

end
</source>

Rel 2

2012-11-27T16:51:11Z

Jalonso: Protegió «Rel 2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Rel 2

2012-11-27T16:50:57Z

Ejercicios

2012-11-27T16:36:26Z

Jalonso: /* Ejercicios de Demostración asistida por ordenador */

Tema 3: Razonamiento sobre programas

2012-11-27T16:34:58Z

Jalonso: Protegió «Tema 3: Razonamiento sobre programas» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

<source lang="isar">
header {* Tema 3: Razonamiento sobre programas *}

theory T3_Razonamiento_sobre_programas
imports Main
begin

text {*
En este tema se demuestra con Isabelle las propiedades de los
programas funcionales como se expone en el tema 8 del curso
"Informática" que puede leerse en
http://www.cs.us.es/~jalonso/cursos/i1m/temas/tema-8t.pdf

Todas las demostraciones se hacen automáticamente por simplificación e
inducción.
*}

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
| "longitud (x#xs) = 1 + longitud xs"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

lemma "longitud [4,2,5] = 3"
by simp

text {* ---------------------------------------------------------------
Ejercicio 3. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

lemma "intercambia (intercambia (x,y)) = (x,y)"
by simp

text {* ---------------------------------------------------------------
Ejercicio 5. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
| "inversa (x#xs) = inversa xs @ [x]"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

lemma "inversa [x] = [x]"
by simp

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
| "repite (Suc n) x = x # (repite n x)"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

lemma "longitud (repite n x) = n"
by (induct n) auto

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
| "conc (x#xs) ys = x # (conc xs ys)"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

lemma "conc xs ys = conc ys xs"
quickcheck
oops

text {* Encuentra el contraejemplo,
xs = [a\<^isub>2]
ys = [a\<^isub>1] *}

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

lemma "conc xs [] = xs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}

lemma "longitud (conc xs ys) = longitud xs + longitud ys"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 14. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []"
| "coge 0 xs = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 15. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: coge.induct) auto

text {* coge.induct es el esquema de inducción asociado a la definición
de la función coge.
⟦⋀n. P n [];
⋀x xs. P 0 (x#xs);
⋀n x xs. P n xs ⟹ P (Suc n) (x#xs)⟧
⟹ P n x
Puede verse usando "thm coge.induct". *}

text {* ---------------------------------------------------------------
Ejercicio 17. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
| "esVacia (x#xs) = False"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

lemma "esVacia xs = esVacia (conc xs xs)"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 19. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar que
inversaAcAux xs ys = (inversa xs)@ys
------------------------------------------------------------------- *}

lemma inversaAcAux_es_inversa:
"inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)

text {* ---------------------------------------------------------------
Ejercicio 22. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 23. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f (x#xs) = (f x) # map f xs"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}

lemma "longitud (map f xs) = longitud xs"
by (induct xs) auto

section {* Referencias *}

text {*
· J.A. Alonso. "Razonamiento sobre programas" http://goo.gl/R06O3
· G. Hutton. "Programming in Haskell". Cap. 13 "Reasoning about
programms".
· S. Thompson. "Haskell: the Craft of Functional Programming, 3rd
Edition. Cap. 8 "Reasoning about programms".
· L. Paulson. "ML for the Working Programmer, 2nd Edition". Cap. 6.
"Reasoning about functional programs".
*}

end
</source>

Tema 3: Razonamiento sobre programas

2012-11-27T16:34:36Z

Jalonso:

Tema 3: Razonamiento sobre programas

2012-11-27T16:34:21Z

Jalonso: Página creada con '<source lang="isar"> header {* Razonamiento sobre programas *} theory T3_Razonamiento_sobre_programas imports Main begin text {* En este tema se demuestra con Isabelle las...'

<source lang="isar">
header {* Razonamiento sobre programas *}

theory T3_Razonamiento_sobre_programas
imports Main
begin

text {*
En este tema se demuestra con Isabelle las propiedades de los
programas funcionales como se expone en el tema 8 del curso
"Informática" que puede leerse en
http://www.cs.us.es/~jalonso/cursos/i1m/temas/tema-8t.pdf

Todas las demostraciones se hacen automáticamente por simplificación e
inducción.
*}

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0"
| "longitud (x#xs) = 1 + longitud xs"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar que
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

lemma "longitud [4,2,5] = 3"
by simp

text {* ---------------------------------------------------------------
Ejercicio 3. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = (y,x)"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

lemma "intercambia (intercambia (x,y)) = (x,y)"
by simp

text {* ---------------------------------------------------------------
Ejercicio 5. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa [] = []"
| "inversa (x#xs) = inversa xs @ [x]"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

lemma "inversa [x] = [x]"
by simp

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite 0 x = []"
| "repite (Suc n) x = x # (repite n x)"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

lemma "longitud (repite n x) = n"
by (induct n) auto

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] ys = ys"
| "conc (x#xs) ys = x # (conc xs ys)"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

lemma "conc xs ys = conc ys xs"
quickcheck
oops

text {* Encuentra el contraejemplo,
xs = [a\<^isub>2]
ys = [a\<^isub>1] *}

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

lemma "conc xs [] = xs"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar que
longitud (conc xs ys) = longitud xs + longitud ys
------------------------------------------------------------------- *}

lemma "longitud (conc xs ys) = longitud xs + longitud ys"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 14. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n [] = []"
| "coge 0 xs = []"
| "coge (Suc n) (x#xs) = x # (coge n xs)"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 15. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n [] = []"
| "elimina 0 xs = xs"
| "elimina (Suc n) (x#xs) = elimina n xs"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: coge.induct) auto

text {* coge.induct es el esquema de inducción asociado a la definición
de la función coge.
⟦⋀n. P n [];
⋀x xs. P 0 (x#xs);
⋀n x xs. P n xs ⟹ P (Suc n) (x#xs)⟧
⟹ P n x
Puede verse usando "thm coge.induct". *}

text {* ---------------------------------------------------------------
Ejercicio 17. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True"
| "esVacia (x#xs) = False"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

lemma "esVacia xs = esVacia (conc xs xs)"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 19. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux [] ys = ys"
| "inversaAcAux (x#xs) ys = inversaAcAux xs (x#ys)"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = inversaAcAux xs []"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar que
inversaAcAux xs ys = (inversa xs)@ys
------------------------------------------------------------------- *}

lemma inversaAcAux_es_inversa:
"inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)

text {* ---------------------------------------------------------------
Ejercicio 22. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum [] = 0"
| "sum (x#xs) = x + sum xs"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 23. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []"
| "map f (x#xs) = (f x) # map f xs"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
by (induct xs) auto

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar que
longitud (map f xs) = longitud xs
------------------------------------------------------------------- *}

lemma "longitud (map f xs) = longitud xs"
by (induct xs) auto

section {* Referencias *}

text {*
· J.A. Alonso. "Razonamiento sobre programas" http://goo.gl/R06O3
· G. Hutton. "Programming in Haskell". Cap. 13 "Reasoning about
programms".
· S. Thompson. "Haskell: the Craft of Functional Programming, 3rd
Edition. Cap. 8 "Reasoning about programms".
· L. Paulson. "ML for the Working Programmer, 2nd Edition". Cap. 6.
"Reasoning about functional programs".
*}

end
</source>

Tema 2: Programación funcional en Isabelle

2012-11-27T16:27:53Z

Jalonso:

<source lang="isar">
header {* Tema 2: Programación funcional en Isabelle *}

theory T2_Programacion_funcional_en_Isabelle
imports Main
begin

section {* Introducción *}

text {* Esta notas son una introducción a la demostración asistida
utilizando el sistema Isabelle/HOL/Isar. La versión de Isabelle
utilizada es la 2012.

En este capítulos se presenta el lenguaje funcional que está
incluido en Isabelle. El lenguaje funcional es muy parecido a
Haskell. *}

section {* Números naturales, enteros y booleanos *}

text {* En Isabelle están definidos los número naturales con la sintaxis
de Peano usando dos constructores: 0 (cero) y Suc (el sucesor).

Los números como el 1 son abreviaturas de los correspondientes en la
notación de Peano, en este caso "Suc 0".

El tipo de los números naturales es nat.

Por ejemplo, el siguiente del 0 es el 1. *}

value "Suc 0" -- "= 1"

text {* En Isabelle está definida la suma de los números naturales:
(x + y) es la suma de x e y.

Por ejemplo, la suma de los números naturales 1 y 2 es el número
natural 3. *}

value "(1::nat) + 2" -- "= 3"

text {* La notación del par de dos puntos se usa para asignar un tipo a
un término (por ejemplo, (1::nat) significa que se considera que 1 es
un número natural).

En Isabelle está definida el producto de los números naturales:
(x * y) es el producto de x e y.

Por ejemplo, el producto de los números naturales 2 y 3 es el número
natural 6. *}

value "(2::nat) * 3" -- "= 6"

text {* En Isabelle está definida la división de números naturales:
(n div m) es el cociente entero de x entre y.

Por ejemplo, la división natural de 7 entre 3 es 2. *}

value "(7::nat) div 3" -- "= 2"

text {* En Isabelle está definida el resto de división de números
naturales: (n mod m) es el resto de dividir n entre m.

Por ejemplo, el resto de dividir 7 entre 3 es 1. *}

value "(7::nat) mod 3" -- "= 1"

text {* En Isabelle también están definidos los números enteros. El tipo
de los enteros se representa por int.

Por ejemplo, la suma de 1 y -2 es el número entero -1. *}

value "(1::int) + -2" -- "= -1"

text {* Los numerales están sobrecargados. Por ejemplo, el 1 puede ser
un natural o un entero, dependiendo del contexto.

Isabelle resuelve ambigüedades mediante inferencia de tipos.

A veces, es necesario usar declaraciones de tipo para resolver la
ambigüedad.

En Isabelle están definidos los valores booleanos (True y False), las
conectivas (¬, ∧, ∨, ⟶ y ↔) y los cuantificadores (∀ y ∃).

El tipo de los booleanos es bool. *}

text {* La conjunción de dos fórmulas verdaderas es verdadera. *}
value "True ∧ True" -- "= True"

text {* La conjunción de un fórmula verdadera y una falsa es falsa. *}
value "True ∧ False" -- "= False"

text {* La disyunción de una fórmula verdadera y una falsa es
verdadera. *}
value "True ∨ False" -- "= True"

text {* La disyunción de dos fórmulas falsas es falsa. *}
value "False ∨ False" -- "= False"

text {* La negación de una fórmula verdadera es falsa. *}
value "¬True" -- "= False"

text {* Una fórmula falsa implica una fórmula verdadera. *}
value "False ⟶ True" -- "= True"

text {* Un lema introduce una proposición seguida de una demostración.

Isabelle dispone de varios procedimientos automáticos para generar
demostraciones, uno de los cuales es el de simplificación (llamado
simp).

El procedimiento simp aplica un conjunto de reglas de reescritura, que
inicialmente contiene un gran número de reglas relativas a los objetos
definidos. *}

text {* Ej. de simp: Todo elemento es igual a sí mismo. *}
lemma "∀x. x = x"
by simp

text {* Ej. de simp: Existe un elemento igual a 1. *}
lemma "∃x. x = 1"
by simp

section {* Definiciones no recursivas *}

text {* La disyunción exclusiva de A y B se verifica si una es verdadera
y la otra no lo es. *}

definition xor :: "bool ⇒ bool ⇒ bool" where
"xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"

text {* Prop.: La disyunción exclusiva de dos fórmulas verdaderas es
falsa.

Dem.: Por simplificación, usando la definición de la disyunción
exclusiva.
*}

lemma "xor True True = False"
by (simp add: xor_def)

text {* Se añade la definición de la disyunción exclusiva al conjunto de
reglas de simplificación automáticas. *}

declare xor_def[simp]

lemma "xor True False = True"
by simp

section {* Definiciones locales *}

text {* Se puede asignar valores a variables locales mediante 'let' y
usarlo en las expresiones dentro de 'in'.

Por ejemplo, si x es el número natural 3, entonces "x*x=9". *}

value "let x = 3::nat in x * x" -- "= 9"

section {* Pares *}

text {* Un par se representa escribiendo los elementos entre paréntesis
y separados por coma.

El tipo de los pares es el producto de los tipos.

La función fst devuelve el primer elemento de un par y la snd el
segundo.

Por ejemplo, si p es el par de números naturales (2,3), entonces la
suma del primer elemento de p y 1 es igual al segundo elemento de
p. *}

value "let p = (2,3)::nat × nat in fst p + 1 = snd p"

section {* Listas *}

text {* Una lista se representa escribiendo los elementos entre
corchetes y separados por comas.

La lista vacía se representa por [].

Todos los elementos de una lista tienen que ser del mismo tipo.

El tipo de las listas de elementos del tipo a es (a list).

El término (x#xs) representa la lista obtenida añadiendo el elemento x
al principio de la lista xs.

Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista
vacía los elementos c, b y a es [a,b,c]. *}

value "a#(b#(c#[]))" -- "= [a,b,c]"

text {* Funciones de descomposión de listas:
· (hd xs) es el primer elemento de la lista xs.
· (tl xs) es el resto de la lista xs.

Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es a
y el resto de xs es [b,c]. *}

value "let xs = [a,b,c] in hd xs = a ∧ tl xs = [b,c]" -- "= True"

text {* (length xs) es la longitud de la lista xs. Por ejemplo, la
longitud de la lista [1,2,3] es 3. *}

value "length [1,2,3]" -- "= 3"

text {* En la sesión 47 de "Isabelle/HOL — Higher-Order Logic"
http://goo.gl/sFsFF se encuentran más definiciones y propiedades de
las listas. *}

section {* Registros *}

text {* Un registro es una colección de campos y valores.

Por ejemplo, los puntos del plano se pueden representar mediante
registros con dos campos, las coordenadas, con valores enteros. *}

record punto =
coordenada_x :: int
coordenada_y :: int

text {* Ejemplo, el punto pt tiene de coordenadas 3 y 7. *}

definition pt :: punto where
"pt ≡ (|coordenada_x = 3, coordenada_y = 7|)"

text {* Ejemplo, la coordenada x del punto pt es 3. *}

value "coordenada_x pt" -- "= 3"

text {* Ejemplo, sea pt2 el punto obtenido a partir del punto pt
cambiando el valor de su coordenada x por 4. Entonces la coordenada x
del punto pt2 es 4. *}

value "let pt2 = pt(|coordenada_x:=4|) in coordenada_x (pt2)" -- "= 4"

section {* Funciones anónimas *}

text {* En Isabelle pueden definirse funciones anónimas.

Por ejemplo, el valor de la función que a un número le asigna su doble
aplicada a 1 es 2. *}

value "(λx. x + x) 1::nat" -- "= 2"

section {* Condicionales *}

text {* El valor absoluto del entero x es x, si "x ≥ 0" y es -x en caso
contrario. *}

definition absoluto :: "int ⇒ int" where
"absoluto x ≡ (if x ≥ 0 then x else -x)"

text {* Ejemplo, el valor absoluto de -3 es 3. *}

value "absoluto(-3)" -- "= 3"

text {* Def.: Un número natural n es un sucesor si es de la forma
(Suc m). *}

definition es_sucesor :: "nat ⇒ bool" where
"es_sucesor n ≡ (case n of
0 ⇒ False
| Suc m ⇒ True)"

text {* Ejemplo, el número 3 es sucesor. *}

value "es_sucesor 3" -- "= True"

section {* Tipos de datos y definiciones recursivas *}

text {* Una lista de elementos de tipo a es la lista Vacia o se obtiene
añadiendo, con Cons, un elemento de tipo a a una lista de elementos de
tipo a. *}

datatype 'a Lista = Vacia | Cons 'a "'a Lista"

text {* (conc xs ys) es la concatenación de las lista xs e ys. Por
ejemplo,
conc (Cons a (Cons b Vacia)) (Cons c Vacia)
= Cons a (Cons b (Cons c Vacia))
*}

fun conc :: "'a Lista ⇒ 'a Lista ⇒ 'a Lista" where
"conc Vacia ys = ys"
| "conc (Cons x xs) ys = Cons x (conc xs ys)"

value "conc (Cons a (Cons b Vacia)) (Cons c Vacia)"
-- "= Cons a (Cons b (Cons c Vacia))"

text {* (suma n) es la suma de los primeros n números naturales. Por
ejemplo,
suma 3 = 6
*}

fun suma :: "nat ⇒ nat" where
"suma 0 = 0"
| "suma (Suc m) = (Suc m) + suma m"

value "suma 3" -- "= 6"

text {* (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 3 = 9
*}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n"

value "sumaImpares 3" -- "= 9"

end
</source>

Tema 2: Programación funcional en Isabelle

2012-11-27T16:22:23Z

Jalonso: Protegió «Tema 2: Programación funcional en Isabelle» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

<source lang="isar">
header {* Tema 2: Programación funcional en Isabelle *}

theory Programacion_funcional_en_Isabelle
imports Main
begin

section {* Introducción *}

text {* Esta notas son una introducción a la demostración asistida
utilizando el sistema Isabelle/HOL/Isar. La versión de Isabelle
utilizada es la 2012.

En este capítulos se presenta el lenguaje funcional que está
incluido en Isabelle. El lenguaje funcional es muy parecido a
Haskell. *}

section {* Números naturales, enteros y booleanos *}

text {* En Isabelle están definidos los número naturales con la sintaxis
de Peano usando dos constructores: 0 (cero) y Suc (el sucesor).

Los números como el 1 son abreviaturas de los correspondientes en la
notación de Peano, en este caso "Suc 0".

El tipo de los números naturales es nat.

Por ejemplo, el siguiente del 0 es el 1. *}

value "Suc 0" -- "= 1"

text {* En Isabelle está definida la suma de los números naturales:
(x + y) es la suma de x e y.

Por ejemplo, la suma de los números naturales 1 y 2 es el número
natural 3. *}

value "(1::nat) + 2" -- "= 3"

text {* La notación del par de dos puntos se usa para asignar un tipo a
un término (por ejemplo, (1::nat) significa que se considera que 1 es
un número natural).

En Isabelle está definida el producto de los números naturales:
(x * y) es el producto de x e y.

Por ejemplo, el producto de los números naturales 2 y 3 es el número
natural 6. *}

value "(2::nat) * 3" -- "= 6"

text {* En Isabelle está definida la división de números naturales:
(n div m) es el cociente entero de x entre y.

Por ejemplo, la división natural de 7 entre 3 es 2. *}

value "(7::nat) div 3" -- "= 2"

text {* En Isabelle está definida el resto de división de números
naturales: (n mod m) es el resto de dividir n entre m.

Por ejemplo, el resto de dividir 7 entre 3 es 1. *}

value "(7::nat) mod 3" -- "= 1"

text {* En Isabelle también están definidos los números enteros. El tipo
de los enteros se representa por int.

Por ejemplo, la suma de 1 y -2 es el número entero -1. *}

value "(1::int) + -2" -- "= -1"

text {* Los numerales están sobrecargados. Por ejemplo, el 1 puede ser
un natural o un entero, dependiendo del contexto.

Isabelle resuelve ambigüedades mediante inferencia de tipos.

A veces, es necesario usar declaraciones de tipo para resolver la
ambigüedad.

En Isabelle están definidos los valores booleanos (True y False), las
conectivas (¬, ∧, ∨, ⟶ y ↔) y los cuantificadores (∀ y ∃).

El tipo de los booleanos es bool. *}

text {* La conjunción de dos fórmulas verdaderas es verdadera. *}
value "True ∧ True" -- "= True"

text {* La conjunción de un fórmula verdadera y una falsa es falsa. *}
value "True ∧ False" -- "= False"

text {* La disyunción de una fórmula verdadera y una falsa es
verdadera. *}
value "True ∨ False" -- "= True"

text {* La disyunción de dos fórmulas falsas es falsa. *}
value "False ∨ False" -- "= False"

text {* La negación de una fórmula verdadera es falsa. *}
value "¬True" -- "= False"

text {* Una fórmula falsa implica una fórmula verdadera. *}
value "False ⟶ True" -- "= True"

text {* Un lema introduce una proposición seguida de una demostración.

Isabelle dispone de varios procedimientos automáticos para generar
demostraciones, uno de los cuales es el de simplificación (llamado
simp).

El procedimiento simp aplica un conjunto de reglas de reescritura, que
inicialmente contiene un gran número de reglas relativas a los objetos
definidos. *}

text {* Ej. de simp: Todo elemento es igual a sí mismo. *}
lemma "∀x. x = x"
by simp

text {* Ej. de simp: Existe un elemento igual a 1. *}
lemma "∃x. x = 1"
by simp

section {* Definiciones no recursivas *}

text {* La disyunción exclusiva de A y B se verifica si una es verdadera
y la otra no lo es. *}

definition xor :: "bool ⇒ bool ⇒ bool" where
"xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"

text {* Prop.: La disyunción exclusiva de dos fórmulas verdaderas es
falsa.

Dem.: Por simplificación, usando la definición de la disyunción
exclusiva.
*}

lemma "xor True True = False"
by (simp add: xor_def)

text {* Se añade la definición de la disyunción exclusiva al conjunto de
reglas de simplificación automáticas. *}

declare xor_def[simp]

lemma "xor True False = True"
by simp

section {* Definiciones locales *}

text {* Se puede asignar valores a variables locales mediante 'let' y
usarlo en las expresiones dentro de 'in'.

Por ejemplo, si x es el número natural 3, entonces "x*x=9". *}

value "let x = 3::nat in x * x" -- "= 9"

section {* Pares *}

text {* Un par se representa escribiendo los elementos entre paréntesis
y separados por coma.

El tipo de los pares es el producto de los tipos.

La función fst devuelve el primer elemento de un par y la snd el
segundo.

Por ejemplo, si p es el par de números naturales (2,3), entonces la
suma del primer elemento de p y 1 es igual al segundo elemento de
p. *}

value "let p = (2,3)::nat × nat in fst p + 1 = snd p"

section {* Listas *}

text {* Una lista se representa escribiendo los elementos entre
corchetes y separados por comas.

La lista vacía se representa por [].

Todos los elementos de una lista tienen que ser del mismo tipo.

El tipo de las listas de elementos del tipo a es (a list).

El término (x#xs) representa la lista obtenida añadiendo el elemento x
al principio de la lista xs.

Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista
vacía los elementos c, b y a es [a,b,c]. *}

value "a#(b#(c#[]))" -- "= [a,b,c]"

text {* Funciones de descomposión de listas:
· (hd xs) es el primer elemento de la lista xs.
· (tl xs) es el resto de la lista xs.

Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es a
y el resto de xs es [b,c]. *}

value "let xs = [a,b,c] in hd xs = a ∧ tl xs = [b,c]" -- "= True"

text {* (length xs) es la longitud de la lista xs. Por ejemplo, la
longitud de la lista [1,2,3] es 3. *}

value "length [1,2,3]" -- "= 3"

text {* En la sesión 47 de "Isabelle/HOL — Higher-Order Logic"
http://goo.gl/sFsFF se encuentran más definiciones y propiedades de
las listas. *}

section {* Registros *}

text {* Un registro es una colección de campos y valores.

Por ejemplo, los puntos del plano se pueden representar mediante
registros con dos campos, las coordenadas, con valores enteros. *}

record punto =
coordenada_x :: int
coordenada_y :: int

text {* Ejemplo, el punto pt tiene de coordenadas 3 y 7. *}

definition pt :: punto where
"pt ≡ (|coordenada_x = 3, coordenada_y = 7|)"

text {* Ejemplo, la coordenada x del punto pt es 3. *}

value "coordenada_x pt" -- "= 3"

text {* Ejemplo, sea pt2 el punto obtenido a partir del punto pt
cambiando el valor de su coordenada x por 4. Entonces la coordenada x
del punto pt2 es 4. *}

value "let pt2 = pt(|coordenada_x:=4|) in coordenada_x (pt2)" -- "= 4"

section {* Funciones anónimas *}

text {* En Isabelle pueden definirse funciones anónimas.

Por ejemplo, el valor de la función que a un número le asigna su doble
aplicada a 1 es 2. *}

value "(λx. x + x) 1::nat" -- "= 2"

section {* Condicionales *}

text {* El valor absoluto del entero x es x, si "x ≥ 0" y es -x en caso
contrario. *}

definition absoluto :: "int ⇒ int" where
"absoluto x ≡ (if x ≥ 0 then x else -x)"

text {* Ejemplo, el valor absoluto de -3 es 3. *}

value "absoluto(-3)" -- "= 3"

text {* Def.: Un número natural n es un sucesor si es de la forma
(Suc m). *}

definition es_sucesor :: "nat ⇒ bool" where
"es_sucesor n ≡ (case n of
0 ⇒ False
| Suc m ⇒ True)"

text {* Ejemplo, el número 3 es sucesor. *}

value "es_sucesor 3" -- "= True"

section {* Tipos de datos y definiciones recursivas *}

text {* Una lista de elementos de tipo a es la lista Vacia o se obtiene
añadiendo, con Cons, un elemento de tipo a a una lista de elementos de
tipo a. *}

datatype 'a Lista = Vacia | Cons 'a "'a Lista"

text {* (conc xs ys) es la concatenación de las lista xs e ys. Por
ejemplo,
conc (Cons a (Cons b Vacia)) (Cons c Vacia)
= Cons a (Cons b (Cons c Vacia))
*}

fun conc :: "'a Lista ⇒ 'a Lista ⇒ 'a Lista" where
"conc Vacia ys = ys"
| "conc (Cons x xs) ys = Cons x (conc xs ys)"

value "conc (Cons a (Cons b Vacia)) (Cons c Vacia)"
-- "= Cons a (Cons b (Cons c Vacia))"

text {* (suma n) es la suma de los primeros n números naturales. Por
ejemplo,
suma 3 = 6
*}

fun suma :: "nat ⇒ nat" where
"suma 0 = 0"
| "suma (Suc m) = (Suc m) + suma m"

value "suma 3" -- "= 6"

text {* (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 3 = 9
*}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n"

value "sumaImpares 3" -- "= 9"

end
</source>

Rel 1

2012-11-27T16:18:24Z

Jalonso: Protegió «Rel 1» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

<source lang="isar">
header {* Relación 1: Programación funcional en Isabelle *}

theory Programacion_funcional_en_Isabelle
imports Main
begin

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud xs = undefined"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = undefined"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 3. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa xs = undefined"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejercicio 4. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite n x = undefined"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc xs ys = undefined"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n xs = undefined"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n xs = undefined"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia xs = undefined"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux xs ys = undefined"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = undefined"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejercicio 10. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum xs = undefined"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 11. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f xs = undefined"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

end
</source>

Rel 1

2012-11-27T16:18:06Z

Jalonso: Página creada con '<source lang="isar"> header {* Relación 1: Programación funcional en Isabelle *} theory Programacion_funcional_en_Isabelle imports Main begin text {* ----------------------...'

Ejercicios

2012-11-27T16:16:57Z

Jalonso: /* Ejercicios de Demostración asistida por ordenador */

Relación 1

2012-11-27T16:12:56Z

Jalonso: Página creada con '<source lang="isar"> header {* Definición de funciones *} theory Definicion_de_funciones imports Main begin text {* ---------------------------------------------------------...'

<source lang="isar">
header {* Definición de funciones *}

theory Definicion_de_funciones
imports Main
begin

text {* ----------------------------------------------------------------
Ejercicio 1. Definir, por recursión, la función
longitud :: 'a list ⇒ nat
tal que (longitud xs) es la longitud de la listas xs. Por ejemplo,
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

fun longitud :: "'a list ⇒ nat" where
"longitud xs = undefined"

value "longitud [4,2,5]" -- "= 3"

text {* ---------------------------------------------------------------
Ejercicio 2. Definir la función
fun intercambia :: 'a × 'b ⇒ 'b × 'a
tal que (intercambia p) es el par obtenido intercambiando las
componentes del par p. Por ejemplo,
intercambia (u,v) = (v,u)
------------------------------------------------------------------ *}

fun intercambia :: "'a × 'b ⇒ 'b × 'a" where
"intercambia (x,y) = undefined"

value "intercambia (u,v)" -- "= (v,u)"

text {* ---------------------------------------------------------------
Ejercicio 3. Definir, por recursión, la función
inversa :: 'a list ⇒ 'a list
tal que (inversa xs) es la lista obtenida invirtiendo el orden de los
elementos de xs. Por ejemplo,
inversa [a,d,c] = [c,d,a]
------------------------------------------------------------------ *}

fun inversa :: "'a list ⇒ 'a list" where
"inversa xs = undefined"

value "inversa [a,d,c]" -- "= [c,d,a]"

text {* ---------------------------------------------------------------
Ejercicio 4. Definir la función
repite :: nat ⇒ 'a ⇒ 'a list
tal que (repite n x) es la lista formada por n copias del elemento
x. Por ejemplo,
repite 3 a = [a,a,a]
------------------------------------------------------------------ *}

fun repite :: "nat ⇒ 'a ⇒ 'a list" where
"repite n x = undefined"

value "repite 3 a" -- "= [a,a,a]"

text {* ---------------------------------------------------------------
Ejercicio 5. Definir la función
conc :: 'a list ⇒ 'a list ⇒ 'a list
tal que (conc xs ys) es la concatención de las listas xs e ys. Por
ejemplo,
conc [a,d] [b,d,a,c] = [a,d,b,d,a,c]
------------------------------------------------------------------ *}

fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc xs ys = undefined"

value "conc [a,d] [b,d,a,c]" -- "= [a,d,b,d,a,c]"

text {* ---------------------------------------------------------------
Ejercicio 6. Definir la función
coge :: nat ⇒ 'a list ⇒ 'a list
tal que (coge n xs) es la lista de los n primeros elementos de xs. Por
ejemplo,
coge 2 [a,c,d,b,e] = [a,c]
------------------------------------------------------------------ *}

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
"coge n xs = undefined"

value "coge 2 [a,c,d,b,e]" -- "= [a,c]"

text {* ---------------------------------------------------------------
Ejercicio 7. Definir la función
elimina :: nat ⇒ 'a list ⇒ 'a list
tal que (elimina n xs) es la lista obtenida eliminando los n primeros
elementos de xs. Por ejemplo,
elimina 2 [a,c,d,b,e] = [d,b,e]
------------------------------------------------------------------ *}

fun elimina :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina n xs = undefined"

value "elimina 2 [a,c,d,b,e]" -- "= [d,b,e]"

text {* ---------------------------------------------------------------
Ejercicio 8. Definir la función
esVacia :: 'a list ⇒ bool
tal que (esVacia xs) se verifica si xs es la lista vacía. Por ejemplo,
esVacia [] = True
esVacia [1] = False
------------------------------------------------------------------ *}

fun esVacia :: "'a list ⇒ bool" where
"esVacia xs = undefined"

value "esVacia []" -- "= True"
value "esVacia [1]" -- "= False"

text {* ---------------------------------------------------------------
Ejercicio 9. Definir la función
inversaAc :: 'a list ⇒ 'a list
tal que (inversaAc xs) es a inversa de xs calculada usando
acumuladores. Por ejemplo,
inversaAc [a,c,b,e] = [e,b,c,a]
------------------------------------------------------------------ *}

fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
"inversaAcAux xs ys = undefined"

fun inversaAc :: "'a list ⇒ 'a list" where
"inversaAc xs = undefined"

value "inversaAc [a,c,b,e]" -- "= [e,b,c,a]"

text {* ---------------------------------------------------------------
Ejercicio 10. Definir la función
sum :: nat list ⇒ nat
tal que (sum xs) es la suma de los elementos de xs. Por ejemplo,
sum [3,2,5] = 10
------------------------------------------------------------------ *}

fun sum :: "nat list ⇒ nat" where
"sum xs = undefined"

value "sum [3,2,5]" -- "= 10"

text {* ---------------------------------------------------------------
Ejercicio 11. Definir la función
map :: ('a ⇒ 'b) ⇒ 'a list ⇒ 'b list
tal que (map f xs) es la lista obtenida aplicando la función f a los
elementos de xs. Por ejemplo,
map (λx. 2*x) [3,2,5] = [6,4,10]
------------------------------------------------------------------ *}

fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f xs = undefined"

value "map (λx. 2*x) [3::nat,2,5]" -- "= [6,4,10]"

end
</source>

Ejercicios

2012-11-27T16:10:29Z

Jalonso: /* Ejercicios de Demostración asistida por ordenador */

Ejercicios

2012-11-27T16:07:51Z

Jalonso: Página creada con '== Ejercicios de ''Demostración asistida por ordenador'' == En esta sección se publicarán las relaciones de ejercicios. Las soluciones se escriben de forma colaborativa por l...'

Tema 2: Programación funcional en Isabelle

2012-11-27T16:04:01Z

Jalonso:

Tema 2: Programación funcional en Isabelle

2012-11-27T16:02:10Z

Jalonso:

Tema 2: Programación funcional en Isabelle

2012-11-27T16:01:31Z

Jalonso: Página creada con 'header {* Tema 2: Programación funcional en Isabelle *} theory Programacion_funcional_en_Isabelle imports Main begin section {* Introducción *} text {* Esta notas son una ...'

header {* Tema 2: Programación funcional en Isabelle *}

theory Programacion_funcional_en_Isabelle
imports Main
begin

section {* Introducción *}

text {* Esta notas son una introducción a la demostración asistida
utilizando el sistema Isabelle/HOL/Isar. La versión de Isabelle
utilizada es la 2012.

En este capítulos se presenta el lenguaje funcional que está
incluido en Isabelle. El lenguaje funcional es muy parecido a
Haskell. *}

section {* Números naturales, enteros y booleanos *}

text {* En Isabelle están definidos los número naturales con la sintaxis
de Peano usando dos constructores: 0 (cero) y Suc (el sucesor).

Los números como el 1 son abreviaturas de los correspondientes en la
notación de Peano, en este caso "Suc 0".

El tipo de los números naturales es nat.

Por ejemplo, el siguiente del 0 es el 1. *}

value "Suc 0" -- "= 1"

text {* En Isabelle está definida la suma de los números naturales:
(x + y) es la suma de x e y.

Por ejemplo, la suma de los números naturales 1 y 2 es el número
natural 3. *}

value "(1::nat) + 2" -- "= 3"

text {* La notación del par de dos puntos se usa para asignar un tipo a
un término (por ejemplo, (1::nat) significa que se considera que 1 es
un número natural).

En Isabelle está definida el producto de los números naturales:
(x * y) es el producto de x e y.

Por ejemplo, el producto de los números naturales 2 y 3 es el número
natural 6. *}

value "(2::nat) * 3" -- "= 6"

text {* En Isabelle está definida la división de números naturales:
(n div m) es el cociente entero de x entre y.

Por ejemplo, la división natural de 7 entre 3 es 2. *}

value "(7::nat) div 3" -- "= 2"

text {* En Isabelle está definida el resto de división de números
naturales: (n mod m) es el resto de dividir n entre m.

Por ejemplo, el resto de dividir 7 entre 3 es 1. *}

value "(7::nat) mod 3" -- "= 1"

text {* En Isabelle también están definidos los números enteros. El tipo
de los enteros se representa por int.

Por ejemplo, la suma de 1 y -2 es el número entero -1. *}

value "(1::int) + -2" -- "= -1"

text {* Los numerales están sobrecargados. Por ejemplo, el 1 puede ser
un natural o un entero, dependiendo del contexto.

Isabelle resuelve ambigüedades mediante inferencia de tipos.

A veces, es necesario usar declaraciones de tipo para resolver la
ambigüedad.

En Isabelle están definidos los valores booleanos (True y False), las
conectivas (¬, ∧, ∨, ⟶ y ↔) y los cuantificadores (∀ y ∃).

El tipo de los booleanos es bool. *}

text {* La conjunción de dos fórmulas verdaderas es verdadera. *}
value "True ∧ True" -- "= True"

text {* La conjunción de un fórmula verdadera y una falsa es falsa. *}
value "True ∧ False" -- "= False"

text {* La disyunción de una fórmula verdadera y una falsa es
verdadera. *}
value "True ∨ False" -- "= True"

text {* La disyunción de dos fórmulas falsas es falsa. *}
value "False ∨ False" -- "= False"

text {* La negación de una fórmula verdadera es falsa. *}
value "¬True" -- "= False"

text {* Una fórmula falsa implica una fórmula verdadera. *}
value "False ⟶ True" -- "= True"

text {* Un lema introduce una proposición seguida de una demostración.

Isabelle dispone de varios procedimientos automáticos para generar
demostraciones, uno de los cuales es el de simplificación (llamado
simp).

El procedimiento simp aplica un conjunto de reglas de reescritura, que
inicialmente contiene un gran número de reglas relativas a los objetos
definidos. *}

text {* Ej. de simp: Todo elemento es igual a sí mismo. *}
lemma "∀x. x = x"
by simp

text {* Ej. de simp: Existe un elemento igual a 1. *}
lemma "∃x. x = 1"
by simp

section {* Definiciones no recursivas *}

text {* La disyunción exclusiva de A y B se verifica si una es verdadera
y la otra no lo es. *}

definition xor :: "bool ⇒ bool ⇒ bool" where
"xor A B ≡ (A ∧ ¬B) ∨ (¬A ∧ B)"

text {* Prop.: La disyunción exclusiva de dos fórmulas verdaderas es
falsa.

Dem.: Por simplificación, usando la definición de la disyunción
exclusiva.
*}

lemma "xor True True = False"
by (simp add: xor_def)

text {* Se añade la definición de la disyunción exclusiva al conjunto de
reglas de simplificación automáticas. *}

declare xor_def[simp]

lemma "xor True False = True"
by simp

section {* Definiciones locales *}

text {* Se puede asignar valores a variables locales mediante 'let' y
usarlo en las expresiones dentro de 'in'.

Por ejemplo, si x es el número natural 3, entonces "x*x=9". *}

value "let x = 3::nat in x * x" -- "= 9"

section {* Pares *}

text {* Un par se representa escribiendo los elementos entre paréntesis
y separados por coma.

El tipo de los pares es el producto de los tipos.

La función fst devuelve el primer elemento de un par y la snd el
segundo.

Por ejemplo, si p es el par de números naturales (2,3), entonces la
suma del primer elemento de p y 1 es igual al segundo elemento de
p. *}

value "let p = (2,3)::nat × nat in fst p + 1 = snd p"

section {* Listas *}

text {* Una lista se representa escribiendo los elementos entre
corchetes y separados por comas.

La lista vacía se representa por [].

Todos los elementos de una lista tienen que ser del mismo tipo.

El tipo de las listas de elementos del tipo a es (a list).

El término (x#xs) representa la lista obtenida añadiendo el elemento x
al principio de la lista xs.

Por ejemplo, la lista obtenida añadiendo sucesivamente a la lista
vacía los elementos c, b y a es [a,b,c]. *}

value "a#(b#(c#[]))" -- "= [a,b,c]"

text {* Funciones de descomposión de listas:
· (hd xs) es el primer elemento de la lista xs.
· (tl xs) es el resto de la lista xs.

Por ejemplo, si xs es la lista [a,b,c], entonces el primero de xs es a
y el resto de xs es [b,c]. *}

value "let xs = [a,b,c] in hd xs = a ∧ tl xs = [b,c]" -- "= True"

text {* (length xs) es la longitud de la lista xs. Por ejemplo, la
longitud de la lista [1,2,3] es 3. *}

value "length [1,2,3]" -- "= 3"

text {* En la sesión 47 de "Isabelle/HOL — Higher-Order Logic"
http://goo.gl/sFsFF se encuentran más definiciones y propiedades de
las listas. *}

section {* Registros *}

text {* Un registro es una colección de campos y valores.

Por ejemplo, los puntos del plano se pueden representar mediante
registros con dos campos, las coordenadas, con valores enteros. *}

record punto =
coordenada_x :: int
coordenada_y :: int

text {* Ejemplo, el punto pt tiene de coordenadas 3 y 7. *}

definition pt :: punto where
"pt ≡ (|coordenada_x = 3, coordenada_y = 7|)"

text {* Ejemplo, la coordenada x del punto pt es 3. *}

value "coordenada_x pt" -- "= 3"

text {* Ejemplo, sea pt2 el punto obtenido a partir del punto pt
cambiando el valor de su coordenada x por 4. Entonces la coordenada x
del punto pt2 es 4. *}

value "let pt2 = pt(|coordenada_x:=4|) in coordenada_x (pt2)" -- "= 4"

section {* Funciones anónimas *}

text {* En Isabelle pueden definirse funciones anónimas.

Por ejemplo, el valor de la función que a un número le asigna su doble
aplicada a 1 es 2. *}

value "(λx. x + x) 1::nat" -- "= 2"

section {* Condicionales *}

text {* El valor absoluto del entero x es x, si "x ≥ 0" y es -x en caso
contrario. *}

definition absoluto :: "int ⇒ int" where
"absoluto x ≡ (if x ≥ 0 then x else -x)"

text {* Ejemplo, el valor absoluto de -3 es 3. *}

value "absoluto(-3)" -- "= 3"

text {* Def.: Un número natural n es un sucesor si es de la forma
(Suc m). *}

definition es_sucesor :: "nat ⇒ bool" where
"es_sucesor n ≡ (case n of
0 ⇒ False
| Suc m ⇒ True)"

text {* Ejemplo, el número 3 es sucesor. *}

value "es_sucesor 3" -- "= True"

section {* Tipos de datos y definiciones recursivas *}

text {* Una lista de elementos de tipo a es la lista Vacia o se obtiene
añadiendo, con Cons, un elemento de tipo a a una lista de elementos de
tipo a. *}

datatype 'a Lista = Vacia | Cons 'a "'a Lista"

text {* (conc xs ys) es la concatenación de las lista xs e ys. Por
ejemplo,
conc (Cons a (Cons b Vacia)) (Cons c Vacia)
= Cons a (Cons b (Cons c Vacia))
*}

fun conc :: "'a Lista ⇒ 'a Lista ⇒ 'a Lista" where
"conc Vacia ys = ys"
| "conc (Cons x xs) ys = Cons x (conc xs ys)"

value "conc (Cons a (Cons b Vacia)) (Cons c Vacia)"
-- "= Cons a (Cons b (Cons c Vacia))"

text {* (suma n) es la suma de los primeros n números naturales. Por
ejemplo,
suma 3 = 6
*}

fun suma :: "nat ⇒ nat" where
"suma 0 = 0"
| "suma (Suc m) = (Suc m) + suma m"

value "suma 3" -- "= 6"

text {* (sumaImpares n) es la suma de los n primeros números
impares. Por ejemplo,
sumaImpares 3 = 9
*}

fun sumaImpares :: "nat ⇒ nat" where
"sumaImpares 0 = 0"
| "sumaImpares (Suc n) = (2 * (Suc n) - 1) + sumaImpares n"

value "sumaImpares 3" -- "= 9"
text {* Prop.: La suma de los n primeros numeros impares es n\<^sup>2
Dem.: Por inducción en n. *}

lemma "sumaImpares n = n * n"
by (induct n) auto

end

Temas

2012-11-27T15:59:33Z

Jalonso: /* Temas de Demostración asistida por ordenador */

Documentación

2012-11-23T22:01:48Z

Jalonso: /* Visiones generales del DAO */

En esta página se recogen en enlaces que sirven de documentación al seminario de demostración asistida por ordenador (DAO).

== Visiones generales de la DAO ==

# M. Davis. [http://www.cs.nyu.edu/cs/faculty/davism/early.ps The early history of automated deduction].
# J.P. Delahaye [http://interstices.info/jcms/int_63417/du-reve-a-la-realite-des-preuves Du rêve à la réalité des preuves]. ''Interstices'', 8 de julio de 2012.
# J. Germoni [http://images.math.cnrs.fr/Coq-et-caracteres.html Coq et caractères: Preuve formelle du théorème de Feit et Thompson]. ''Images des Mathématiques'', CNRS, 23 de noviembre de 2012.
# T. Hales. [http://www.ams.org/notices/200811/tx081101370p.pdf Formal proof]. ''Notices of AMS'', Vol. 55, N. 11 (2008) pp. 1370-1380.
# J. Harrison. [http://www.cl.cam.ac.uk/~jrh13/papers/ab.html A short survey of automated reasoning]. ''Lecture Notes in Computer Science'', Vol. 4545, pp. 334-349, 2007.
# J. Harrison. [http://www.ams.org/notices/200811/tx081101395p.pdf Formal proof: Theory and practice]. ''Notices of the AMS'', Vol. 55, N. 11 (2008) p.1395-1406.
# G. Kolata. [http://www.nytimes.com/library/cyber/week/1210math.html Computer math proof shows reasoning power]. ''The New York Times'', 10 de diciembre de 1996.
# D. MacKenzie [http://www.bcs.org/server.php?show=ConWebDoc.4364 Computers and the sociology of mathematical proof].
# G. Sutcliffe. [http://www.cs.miami.edu/~tptp/OverviewOfATP.html What is automated theorem proving?].