Razonamiento automático (2015-16) - Contribuciones del usuario [es]

Documentación

2022-02-08T17:22:32Z

Jalonso:

En esta página se recogen en enlaces que sirven de documentación al curso de demostración asistida por ordenador (DAO). Los enlaces están actualizados en el [https://www.glc.us.es/~jalonso/RA2019/index.php/Documentaci%C3%B3n curso 2019-20].

== Visiones generales de la DAO ==

# J.A. Alonso. [http://goo.gl/NWk7b Razonamiento formalizado: Del sueño a la realidad de las pruebas]. ''Vestigium'', 26 de diciembre de 2012.
# J. Avigad. [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation]. ICERM, 14 de diciembre de 2012.
# 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.
# H. Geuvers [http://www.ias.ac.in/sadhana/Pdf2009Feb/3.pdf Proof assistants: History, ideas and future]. ''Sadhana'', Vol. 34-1, pp. 3-25, février 2009.
# G. Gonthier [http://www.ams.org/notices/200811/tx081101382p.pdf The four-color theorem]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1382-1393, 2008.
# 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 [https://backspaces.net/temp/Spring2010Seminar/18%20unconventional%20essays%20on%20the%20nature%20of%20mathematics.pdf#page=147 Computers and the sociology of mathematical proof].
# G. Sutcliffe. [http://tptp.org/OverviewOfATP.html What is automated theorem proving?].
# F. Wiedijk [http://www.cs.ru.nl/~freek/100/ Formalizing the «top 100» of mathematical theorems].
# F. Wiedijk [http://www.ams.org/notices/200811/tx081101408p.pdf Formal proof - Getting started]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1408-1414, 2008.
# F. Wiedijk, [https://www.cs.ru.nl/F.Wiedijk/pubs/qed2.pdf The QED manifesto revisited]. ''Studies in Logic, Grammar and Rhetoric'', Vol. 10(23), pp. 121-133, 2007.

== Referencias sobre Isabelle/HOL ==
# B. Grechuk [https://web.cs.wpi.edu/~dd/resources_isabelle/isabelle_primer_mathematicians.pdf Isabelle primer for mathematicians].
# T. Nipkow [https://isabelle.in.tum.de/doc/prog-prove.pdf Programming and proving in Isabelle/HOL].
# T. Nipkow, M. Wenzel y L.C. Paulson [https://isabelle.in.tum.de/website-Isabelle2009/dist/Isabelle/doc/tutorial.pdf A proof assistant for higher-order logic].
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic].
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html Tutorials and manuals for Isabelle].

== Lecturas complementarias ==
=== Programación funcional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/i1m-12/temas/2012-13-IM-temas-PF.pdf Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# J.A. Alonso y M.J. Hidalgo [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# G. Hutton [http://goo.gl/pKqG Programming in Haskell]. Cambridge University Press, 2007.
# M. Lipovača [http://aprendehaskell.es ¡Aprende Haskell por el bien de todos!].

=== Lógica computacional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/li-12/temas/temas-LI-2012-13.pdf Temas de "Lógica informática" (2012-13)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# R. Bornat [http://bit.ly/oithic Proof and disproof in formal logic: an introduction for programmers]. Oxford University Press, 2005.
# K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers [https://www.doc.ic.ac.uk/~susan/firstyearbook.pdf Reasoned programming]. Imperial College, 1994.
# K. Doets y J. van Eijck [https://books.google.es/books?id=YCC6lwEACAAJ&dq=The+Haskell+Road+to+Logic,+Maths+and+Programming&hl=es&sa=X&redir_esc=y The Haskell Road to Logic, Maths and Programming].
# M. Huth y M. Ryan [http://goo.gl/TMqOo Logic in computer science: Modelling and reasoning about systems]. Cambridge University Press, 2004. (Incluye el [http://www.cs.bham.ac.uk/research/lics/tutor/index.html tutor en la Red]).

== Cursos relacionados ==
=== Cursos con Isabelle/HOL ===
# Clemens Ballarin. [http://cl-informatik.uibk.ac.at/teaching/ss08/atp/introduction.php Automatic Deduction]. (Univ de Innsbruck, 2008).
# Clemens Ballarin y Gerwin Klein [http://isabelle.in.tum.de/coursematerial/IJCAR04 Introduction to the Isabelle Proof Assistant]. (en el IJCAR-2004).
# Clemens Ballarin y Tjark Weber. [http://cl-informatik.uibk.ac.at/teaching/ws06/atp/introduction.php Automated Theorem Proving in Isabelle/HOL]. (Univ. de Innsbruck, 2006-07).
# A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. [http://archiv.infsec.ethz.ch/education/permanent/csmr.html Computer-supported Modeling and Reasoning]. (ETH Zurich, 2011).
# Mads Dam. [http://www.csc.kth.se/utbildning/kth/kurser/DD2453/aform07/ Advanced formal methods]. (KTH Royal Institute of Technology, 2007).
# Jacques Fleuriot y Paul Jackson. [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/ Automated reasoning]. (Univ. de Edimburgo, 2012-13).
# Thomas Genet [http://www.irisa.fr/celtique/genet/ACF Software formal analysis and design]. (Univ. de Rennes)
# Gerwin Klein. [http://www.cse.unsw.edu.au/~kleing/teaching/thprv-04 Theorem Proving - Principles, Techniques, Applications]. (NICTA, 2004).
# Gerwin Klein. [http://www.cse.unsw.edu.au/~cs4161/index.html Advanced Topics in Software Verification]. (NICTA, 2012).
# Joao Marcos. [http://www.dimap.ufrn.br/~jmarcos/courses/LC/Ementa.htm Lógica computacional: Demonstração assistida e semi-automática de teoremas].(UFRN, 2000).
# Tobias Nipkow. [https://www21.in.tum.de/teaching/semantics/WS1920/ Semantics of programming languages]. (Univ. de Munich, 2012-13).
# Tobias Nipkow [http://isabelle.in.tum.de/coursematerial/PSV2009-1 Theorem Proving with Isabelle/HOL An Intensive Course].
# Larry Paulson. [http://www.cl.cam.ac.uk/teaching/0910/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2009-10).
# Jan-Georg Smaus. [http://www.informatik.uni-freiburg.de/~ki/teaching/ws0910/csmr/lecture.html Computer-supported modeling and reasoning]. (Univ. de Feiburgo, 2009).
# Christian Sternagel [http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php Experiments in Verification – Introduction to Isabelle/HOL]. (Univ. de Innsbruck, 2011-12).
# Tjark Weber. [http://www.cl.cam.ac.uk/teaching/1011/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2010-11).

=== Otros cursos ===
# José A. Alonso [http://www.cs.us.es/~jalonso/cursos/li-12/ Lógica informática] (Univ. de Sevilla, 2012-13).
# Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey y Assia Mahboubi [http://www.di.ens.fr/~zappa/teaching/coq/ecole11 Modelling and verifying algorithms in Coq: an introduction]. (INRIA Paris-Rocquencourt, 14-18 noviembre 2011).
# Pierre Castéran [http://www.labri.fr/perso/casteran/FM/Logique/index.html Logic (Master In Verification)] (Univ. de Burdeos, 2011-12).
# Ian Hodkinson [http://www.doc.ic.ac.uk/~imh/teaching/140_logic/logic.html Logic] (Imperial College, Londres, 2010-11).
# Peter Lucas [http://www.cs.ru.nl/~peterl/teaching/KeR/ Knowledge Representation and Reasoning] (Radboud University # egen, 2011-12).
# Larry Paulson [http://www.cl.cam.ac.uk/Teaching/current/LogicProof/ Logic and Proof] (Univ. de Cambridge, 2011-12).
# Riccardo Pucella [http://www.ccs.neu.edu/home/riccardo/courses/csu290-sp09/index.html Logic and Computation] (Northeastern University, 2009). Curso con ACL2.

== Bibliotecas de ejemplos de verificación ==
# [http://afp.sourceforge.net Archive of Formal Proofs].
# [http://www.cs.ru.nl/~freek/100 Formalizing 100 Theorems].
# [http://toccata.lri.fr/gallery Gallery of verified programs].

Sistemas

2022-02-08T12:52:13Z

Jalonso: Página creada con «== Temas utilizados en ''Razonamiento automático (2015-16)'' == En esta página se irá escribiendo enlaces a los sistemas utilizados en el curso # [http://www.cl.cam.ac.…»

== Temas utilizados en ''Razonamiento automático (2015-16)'' ==

En esta página se irá escribiendo enlaces a los sistemas utilizados en el curso
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle Isabelle/HOL].

Documentación

2022-02-08T12:50:32Z

Jalonso:

Documentación

2015-12-23T15:16:56Z

Jalonso: /* Referencias sobre Isabelle/HOL */

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

== Visiones generales de la DAO ==

# J.A. Alonso. [http://goo.gl/NWk7b Razonamiento formalizado: Del sueño a la realidad de las pruebas]. ''Vestigium'', 26 de diciembre de 2012.
# J. Avigad. [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation]. ICERM, 14 de diciembre de 2012.
# 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.
# H. Geuvers [http://www.ias.ac.in/sadhana/Pdf2009Feb/3.pdf Proof assistants: History, ideas and future]. ''Sadhana'', Vol. 34-1, pp. 3-25, février 2009.
# G. Gonthier [http://www.ams.org/notices/200811/tx081101382p.pdf The four-color theorem]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1382-1393, 2008.
# 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?].
# F. Wiedijk [http://www.cs.ru.nl/~freek/100/ Formalizing the «top 100» of mathematical theorems].
# F. Wiedijk [http://www.ams.org/notices/200811/tx081101408p.pdf Formal proof - Getting started]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1408-1414, 2008.
# F. Wiedijk, [http://www.cs.ru.nl/~freek/pubs/qed2.ps.gz The QED manifesto revisited]. ''Studies in Logic, Grammar and Rhetoric'', Vol. 10(23), pp. 121-133, 2007.

== Referencias sobre Isabelle/HOL ==
# B. Grechuk [http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf Isabelle primer for mathematicians].
# T. Nipkow [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/prog-prove.pdf Programming and proving in Isabelle/HOL]. 25 de mayo de 2015
# T. Nipkow, M. Wenzel y L.C. Paulson [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/tutorial.pdf A proof assistant for higher-order logic]. Springer-Verlag. 25 de mayo de 2015
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic]. 25 de mayo de 2015
# M. Wenzel [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/isar-ref.pdf The Isabelle/Isar Reference Manual]. 25 de mayo de 2015
# M. Wenzel [https://www.lri.fr/~wenzel/Isabelle2011-Paris/quickref.pdf The Isabelle/Isar quick reference].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref.pdf Quick Reference for Isabelle/Isar Propositional Logic].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref2.pdf Quick Reference for Isabelle/Isar More Proof Techniques].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref3.pdf Quick Reference for Isabelle/Isar First-Order Logic].
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html Tutorials and manuals for Isabelle].

== Lecturas complementarias ==
=== Programación funcional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/i1m/temas/2012-13-IM-temas-PF.pdf Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# J.A. Alonso y M.J. Hidalgo [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# G. Hutton [http://goo.gl/pKqG Programming in Haskell]. Cambridge University Press, 2007.
# M. Lipovača [http://aprendehaskell.es ¡Aprende Haskell por el bien de todos!].

=== Lógica computacional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/temas/temas-LI-2012-13.pdf Temas de "Lógica informática" (2012-13)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# R. Bornat [http://bit.ly/oithic Proof and disproof in formal logic: an introduction for programmers]. Oxford University Press, 2005.
# K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers [http://pubs.doc.ic.ac.uk/reasoned-programming/reasoned-programming.pdf Reasoned programming]. Imperial College, 1994.
# K. Doets y J. van Eijck [http://www.ldc.usb.ve/~astorga/Haskell.Road.pdf The Haskell Road to Logic, Maths and Programming].
# M. Huth y M. Ryan [http://goo.gl/TMqOo Logic in computer science: Modelling and reasoning about systems]. Cambridge University Press, 2004. (Incluye el [http://www.cs.bham.ac.uk/research/lics/tutor/index.html tutor en la Red]).

== Cursos relacionados ==
=== Cursos con Isabelle/HOL ===
# Jeremy Avigad. [http://www.phil.cmu.edu/~avigad/formal/ Logic and Formal Verification]. (Carnegie Mellon, 2009).
# Clemens Ballarin. [http://cl-informatik.uibk.ac.at/teaching/ss08/atp/introduction.php Automatic Deduction]. (Univ de Innsbruck, 2008).
# Clemens Ballarin. [http://www4.in.tum.de/~ballarin/belgrade08-tut/ Introduction to the Isabelle Proof Assistant]. (Belgrado, 2008).
# Clemens Ballarin y Gerwin Klein [http://isabelle.in.tum.de/coursematerial/IJCAR04 Introduction to the Isabelle Proof Assistant]. (en el IJCAR-2004).
# Clemens Ballarin y Tjark Weber. [http://cl-informatik.uibk.ac.at/teaching/ws06/atp/introduction.php Automated Theorem Proving in Isabelle/HOL]. (Univ. de Innsbruck, 2006-07).
# A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. [http://archiv.infsec.ethz.ch/education/permanent/csmr.html Computer-supported Modeling and Reasoning]. (ETH Zurich, 2011).
# Mads Dam. [http://www.csc.kth.se/utbildning/kth/kurser/DD2453/aform07/ Advanced formal methods]. (KTH Royal Institute of Technology, 2007).
# Jacques Fleuriot y Paul Jackson. [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/ Automated reasoning]. (Univ. de Edimburgo, 2012-13).
# Thomas Genet [http://www.irisa.fr/celtique/genet/ACF Software formal analysis and design]. (Univ. de Rennes)
# Gerwin Klein. [http://www.cse.unsw.edu.au/~kleing/teaching/thprv-04 Theorem Proving - Principles, Techniques, Applications]. (NICTA, 2004).
# Gerwin Klein. [http://www.cse.unsw.edu.au/~cs4161/index.html Advanced Topics in Software Verification]. (NICTA, 2012).
# Joao Marcos. [http://www.dimap.ufrn.br/~jmarcos/courses/LC/Ementa.htm Lógica computacional: Demonstração assistida e semi-automática de teoremas].(UFRN, 2000).
# Tobias Nipkow. [http://www4.informatik.tu-muenchen.de/~nipkow/semantics/ Semantics of programming languages]. (Univ. de Munich, 2012-13).
# Tobias Nipkow [http://isabelle.in.tum.de/coursematerial/PSV2009-1 Theorem Proving with Isabelle/HOL An Intensive Course].
# Larry Paulson. [http://www.cl.cam.ac.uk/teaching/0910/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2009-10).
# Arnd Poetzsch-Heffter. [https://softech.informatik.uni-kl.de/Homepage/SVHOL10 Specification and Verification with Higher-Order Logic].
# Viorel Preoteasa, Ralph-Johan Back y Charmi Panchal. [http://users.abo.fi/vpreotea/isabelle-2012 Introduction to mechanized reasoning with Isabelle/HOL]. (Åbo Akademi University, 2012).
# Jeremy G. Siek. [http://www.cs.colorado.edu/~siek/7000/spring07/ Practical Theorem Proving with Isabelle/Isar]. (Univ. de Colorado, 2007).
# Jeremy G. Siek. [http://ecee.colorado.edu/~siek/ecen5013/spring11/ Theorem proving in Isabelle]. (Univ. de Colorado, 2011).
# Jan-Georg Smaus. [http://www.informatik.uni-freiburg.de/~ki/teaching/ws0910/csmr/lecture.html Computer-supported modeling and reasoning]. (Univ. de Feiburgo, 2009).
# Christian Sternagel [http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php Experiments in Verification – Introduction to Isabelle/HOL]. (Univ. de Innsbruck, 2011-12).
# Tjark Weber. [http://www.cl.cam.ac.uk/teaching/1011/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2010-11).

=== Otros cursos ===
# José A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/ Lógica informática] (Univ. de Sevilla, 2012-13).
# Thorsten Altenkirch y Peter Morris [http://www.cs.nott.ac.uk/~txa/g52ifr Introduction to formal reasoning] (Univ. de Nottingham, 2010-11).
# Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey y Assia Mahboubi [http://www.di.ens.fr/~zappa/teaching/coq/ecole11 Modelling and verifying algorithms in Coq: an introduction]. (INRIA Paris-Rocquencourt, 14-18 noviembre 2011).
# Pierre Castéran [http://www.labri.fr/perso/casteran/FM/Logique/index.html Logic (Master In Verification)] (Univ. de Burdeos, 2011-12).
# Adam Chlipala [http://stellar.mit.edu/S/course/6/fa11/6.892/ Interactive computer theorem proving]. (MIT, 2012-13).
# Adam Chlipala y Armando Solar Lezama [https://stellar.mit.edu/S/course/6/fa13/6.820/index.html Foundations of program analysis]. (MIT, 2013-14).
# Robby Findler [http://www.eecs.northwestern.edu/~robby/courses/395-495-2013-fall Certified programming with dependent types]. (Northwestern, 2013-14).
# Nuno Gaspar [http://www-sop.inria.fr/members/Nuno.Gaspar/teaching/coq2012.php Verification with the Coq Proof Assistant] (INRIA Sophia Antipolis, 2012-13).
# Carlos Luna y Gustavo Betarte. [https://eva.fing.edu.uy/course/view.php?id=363 Construcción formal de programas en teoría de tipos]. (Univ. de la República, Uruguay, 2013-14).
# Michael Genesereth [http://logic.stanford.edu/classes/cs157/2011/cs157.html Computational Logic] (Univ. de Stanford, 2011-12).
# Ian Hodkinson [http://www.doc.ic.ac.uk/~imh/teaching/140_logic/logic.html Logic] (Imperial College, Londres, 2010-11).
# Peter Lucas [http://www.cs.ru.nl/~peterl/teaching/KeR/ Knowledge Representation and Reasoning] (Radboud University # egen, 2011-12).
# Larry Paulson [http://www.cl.cam.ac.uk/Teaching/current/LogicProof/ Logic and Proof] (Univ. de Cambridge, 2011-12).
# David Pichardie [http://www.irisa.fr/celtique/pichardie/teaching/M2/MDV/ Méthode de vérification] (Universidad de Rennes, 2006-07).
# Michael Winter [Logic in Computer Science] (Brock University, Ontario, Canada, 2010-11).

== Bibliotecas de ejemplos de verificación ==
# [http://afp.sourceforge.net Archive of Formal Proofs].
# [http://www.cs.ru.nl/~freek/100 Formalizing 100 Theorems].
# [http://toccata.lri.fr/gallery Gallery of verified programs].
# [http://www.cs.nott.ac.uk/~lad/research/challenges/ Induction Challenge Problems].
# [http://automatedreasoning.net/ Larry Wos' Notebooks].
# [http://www.cs.miami.edu/~tptp/ The TPTP Problem Library for Automated Theorem Proving].
# [http://www.macs.hw.ac.uk/vstte10/Competition.html The 1st Verified Software Competition].
# [https://sites.google.com/site/vstte2012/compet The 2nd Verified Software Competition].
# [http://verifythis.cost-ic0701.org VerifyThis (A collection of verification benchmarks].

== Artículos recientes ==
Están en orden cronológico inverso a la fecha de su reseña en [http://www.glc.us.es/~jalonso/vestigium/tag/resena Vestigium]:
# [http://bit.ly/1iZjgqN Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem]. L. Noschinski
# [http://bit.ly/1iJ8uVz A graph library for Isabelle]. ~ L. Noschinski
# [http://bit.ly/I0CU80 Gödel’s incompleteness theorems]. ~ L.C. Paulson
# [http://bit.ly/I0CPRN The hereditarily finite sets]. ~ L.C. Paulson
# [http://bit.ly/HBiIJI Applications of real number theorem proving in PVS]. ~ H. Gottliebsen, R. Hardy, O. Lightfoot y U. Martin
# [http://bit.ly/1awnMLB A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets]. ~ L.C. Paulson
# [http://bit.ly/19lWeYy Verified AIG algorithms in ACL2]. ~ J. Davis y S. Swords
# [http://bit.ly/GAhC00 A formal model and correctness proof for an access control policy framework]. ~ C. Wu, X. Zhang y C. Urban
# [http://bit.ly/16SMvSS The ontological argument in PVS]. ~ J. Rushby
# [http://bit.ly/1dRt9n0 Formalizing Moessner’s theorem and generalizations in Nuprl]. ~ M. Bickford, D. Kozen y A. Silva
# [http://bit.ly/1bSeDNB Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model]. ~ M. Ayala y Y. Santos
# [http://bit.ly/1feFqWE Proof assistant based on didactic considerations]. ~ J. Pais y A Tasistro
# [http://bit.ly/18tHNBi Theory exploration for interactive theorem proving]. ~ M. Johansson
# [http://bit.ly/1b0242s From Tarski to Hilbert]. ~ G. Braun y J. Narboux
# [http://bit.ly/18HaXaR Formal verification of language-based concurrent noninterference]. ~ A. Popescu, J. Hölzl y T. Nipkow
# [http://bit.ly/1aRTQsU A Traffic Alert and Collision Avoidance System(TCAS-II) Resolution Advisory Algorithm]. ~ C. Muñoz, A. Narkawicz y J. Chamberlain
# [http://bit.ly/1dNwhDI Formal verification of cryptographic security proofs]. ~ M. Berg
# [http://bit.ly/17muAUv Polygonal numbers in Mizar]. ~ A. Grabowski
# [http://bit.ly/1hk5z6L A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle]. ~ L.C. Paulson
# [http://bit.ly/1cSL0wE Steps towards verified implementations of HOL Light]. ~ M.O. Myreen, S. Owens y R. Kumar
# [http://bit.ly/16Kbgm0 Generic datatypes à la carte]. ~ S. Keuchel y T. Schrijvers
# [http://bit.ly/1bqJGx4 Proof pearl: A verified bignum implementation in x86-64 machine code]. ~ M.O. Myreen y G. Curello
# [http://bit.ly/142ow2Q Mechanized metatheory for a λ λ-calculus with trust types]. ~ R. Ribeiro, C. Camarão y L. Figueiredo
# [http://bit.ly/15WZBDy Proving soundness of combinatorial Vickrey auctions and generating verified executable code]. ~ M.B. Caminati, M. Kerber, C. Lange y C. Rowat
# [http://bit.ly/198g4n9 A computer-assisted proof of correctness of a marching cubes algorithm]. ~ A.N. Chernikov y J. Xu
# [http://bit.ly/11QA5g7 Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm]. ~ L. Lambán, J. Rubio, F.J. Martín y J.L. Ruiz
# [http://bit.ly/1cJAXYk The Königsberg bridge problem and the friendship theorem]. ~ W. Li
# [http://bit.ly/13DBK9R Formal verification of a proof procedure for the description logic ALC]. ~ M. Chaabani, M. Mezghiche y M. Strecker
# [http://bit.ly/1ep2ex9 Pratt’s primality certificates]. ~ S. Wimmer y L. Noschinski
# [http://bit.ly/13C95Ci Reasoning about higher-order relational specifications]. ~ Y. Wang, K. Chaudhuri, A. Gacek y G. Nadathur
# [http://bit.ly/18QQLcL Proofs you can believe in – Proving equivalences between Prolog semantics in Coq]. ~ J. Kriener, A. King y S. Blazy
# [http://bit.ly/19uc82J Certified, efficient and sharp univariate Taylor models in Coq]. ~ E. Martin-Dorel, L. Rideau, L. Théry, M. Mayero y I. Paşca
# [http://bit.ly/1c4Rzel Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁]. ~ M. Norrish y B. Huffman
# [http://bit.ly/14b4Akz Program verification based on Kleene algebra in Isabelle/HOL] ~ A. Armstrong, G. Struth y T. Weber
# [http://bit.ly/1aOgRKx Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)]. ~ C. Ballarin
# [http://bit.ly/11HKixj Computational verification of network programs in Coq]. ~ G. Stewart
# [http://www.glc.us.es/~jalonso/vestigium/resena-certifying-homological-algorithms-to-study-biomedical-images Certifying homological algorithms to study biomedical images]. ~ M. Poza
# [http://bit.ly/16Nks9m Formalizing cut elimination of coalgebraic logics in Coq]. ~ H. Tews
# [http://www.glc.us.es/~jalonso/vestigium/resena-the-formalization-of-syntax-based-mathematical-algorithms-using-quotation-and-evaluation/ The formalization of syntax-based mathematical algorithms using quotation and evaluation]. ~ W.M. Farmer
# [http://www.glc.us.es/~jalonso/vestigium/resena-certified-symbolic-manipulation-bivariate-simplicial-polynomials/ Certified symbolic manipulation: Bivariate simplicial polynomials]. ~ L. Lambán, F.J. Martín, J. Rubio y J.L. Ruiz
# [http://www.glc.us.es/~jalonso/vestigium/resena-solveurs-cpfd-verifies-formellement/ Solveurs CP(FD) vérifiés formellement]. ~ C Dubois y A. Gotlieb
# [http://www.glc.us.es/~jalonso/vestigium/resena-formalizing-bounded-increase/ Formalizing bounded increase]. ~ R. Thiemann
# [http://www.glc.us.es/~jalonso/vestigium/resena-formal-mathematics-on-display-a-wiki-for-flyspeck/ Formal mathematics on display: A wiki for Flyspeck]. ~ C. Tankink, C. Kaliszyk, J. Urban y H. Geuvers
# [http://www.glc.us.es/~jalonso/vestigium/resena-theorem-of-three-circles-in-coq Theorem of three circles in Coq]. ~ J. Zsidó
# [http://bit.ly/19fiWAY Certified HLints with Isabelle/HOLCF-Prelude]. ~ J. Breitner, B. Huffman, N. Mitchell y C. Sternagel
# [http://bit.ly/ZfSQrQ Automatic data refinement]. ~ P. Lammich
# [http://bit.ly/18vyjm7 The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups)]. ~ A. Mahboubi
# [http://bit.ly/114oyZV Mechanical verification of SAT refutations with extended resolution]. ~ N. Wetzler, M.J.H. Heule y W.A. Hunt Jr.
# [http://bit.ly/13H0REu Type classes and filters for mathematical analysis in Isabelle/HOL] ~ J. Hölzl, F. Immler y B. Huffman
# [http://bit.ly/10fv8wO Verifying refutations with extended resolution]. ~ M. J. H. Heule, W. A. Hunt, Jr. y N. Wetzler
# [http://bit.ly/10EcFWj A Web interface for Isabelle: The next generation]. ~ C. Lüth y M. Ring
# [http://bit.ly/18P9CSv On the formalization of continuous-time Markov chains in HOL]. ~ L. Liu, O. Hasan y S. Tahar
# [http://bit.ly/17H2mqy Formalizing Turing machines]. ~ A. Asperti y W. Ricciotti
# [http://bit.ly/YwuCeL Light-weight containers for Isabelle: efficient, extensible, nestable]. ~ A. Lochbihler
# [http://bit.ly/10XLrRA Graph theory]. ~ L. Noschinski
# [http://bit.ly/19kPEP4 A machine-checked proof of the odd order theorem]. ~ G. Gonthier et als.
# [http://goo.gl/LdihL A constructive theory of regular languages in Coq]. ~ C. Doczkal, J.O. Kaiser y G. Smolka
# [http://goo.gl/gwcwL A formal proof of Kruskal’s tree theorem in Isabelle/HOL]. ~ C. Sternagel
# [http://goo.gl/CUF3e Formalizing Knuth-Bendix orders and Knuth-Bendix completion]. ~ C. Sternagel y R. Thiemann
# [http://goo.gl/9JAfX Developing an auction theory toolbox]. ~ C. Lange, C. Rowat, W. Windsteiger y M. Kerber
# [http://goo.gl/6OfmQ Formalization of incremental simplex algorithm by stepwise refinement]. ~ M. Spasić y F. Marić
# [http://goo.gl/Guxky Coinductive pearl: Modular first-order logic completeness]. ~ J.C. Blanchette, A. Popescu y D. Traytel
# [http://goo.gl/HUOl8 A fully verified executable LTL model checker]. ~ J. Esparza et als.
# [http://goo.gl/RV54S ForMaRE - formal mathematical reasoning in economics]. ~ M. Kerber, C. Lange y C. Rowat.
# [http://goo.gl/Y7sIq AI over large formal knowledge bases: The first decade]. ~ J. Urban.
# [http://goo.gl/vvqNg Formalization of real analysis: A survey of proof assistants and libraries]. ~ S. Boldo, C. Lelay y G. Melquiond.
# [http://goo.gl/bEFYa Data refinement in Isabelle/HOL]. ~ F. Haftmann, A. Krauss, O. Kunčar y T. Nipkow
# [http://goo.gl/xTyvE Formalizing the confluence of orthogonal rewriting systems]. ~ A.C. Rocha y M. Ayala.
# [http://goo.gl/zCYHj Formalization of the complex number theory in HOL4]. ~ Z. Shi et als.
# [http://goo.gl/kM0dI Programming and reasonning with PowerLists in Coq]. ~ F. Loulergue y V. Niculescu
# [http://goo.gl/KkU6s A hierarchy of mathematical structures in ACL2]. ~ J. Heras, F.J. Martín y V. Pascual.
# [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing Machines and Computability Theory in Isabelle/HOL] ~ J. Xu, X. Zhang y C. Urban

Documentación

2015-12-23T15:15:40Z

Jalonso: /* Referencias sobre Isabelle/HOL */

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

== Visiones generales de la DAO ==

# J.A. Alonso. [http://goo.gl/NWk7b Razonamiento formalizado: Del sueño a la realidad de las pruebas]. ''Vestigium'', 26 de diciembre de 2012.
# J. Avigad. [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation]. ICERM, 14 de diciembre de 2012.
# 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.
# H. Geuvers [http://www.ias.ac.in/sadhana/Pdf2009Feb/3.pdf Proof assistants: History, ideas and future]. ''Sadhana'', Vol. 34-1, pp. 3-25, février 2009.
# G. Gonthier [http://www.ams.org/notices/200811/tx081101382p.pdf The four-color theorem]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1382-1393, 2008.
# 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?].
# F. Wiedijk [http://www.cs.ru.nl/~freek/100/ Formalizing the «top 100» of mathematical theorems].
# F. Wiedijk [http://www.ams.org/notices/200811/tx081101408p.pdf Formal proof - Getting started]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1408-1414, 2008.
# F. Wiedijk, [http://www.cs.ru.nl/~freek/pubs/qed2.ps.gz The QED manifesto revisited]. ''Studies in Logic, Grammar and Rhetoric'', Vol. 10(23), pp. 121-133, 2007.

== Referencias sobre Isabelle/HOL ==
# B. Grechuk [http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf Isabelle primer for mathematicians].
# T. Nipkow [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/prog-prove.pdf Programming and proving in Isabelle/HOL]. 25 de mayo de 2015
# T. Nipkow, M. Wenzel y L.C. Paulson [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/tutorial.pdf A proof assistant for higher-order logic]. Springer-Verlag.
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic]. 5 de diciembre de 2013.
# M. Wenzel [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/isar-ref.pdf The Isabelle/Isar Reference Manual]. 5 de diciembre de 2013.
# M. Wenzel [https://www.lri.fr/~wenzel/Isabelle2011-Paris/quickref.pdf The Isabelle/Isar quick reference].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref.pdf Quick Reference for Isabelle/Isar Propositional Logic].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref2.pdf Quick Reference for Isabelle/Isar More Proof Techniques].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref3.pdf Quick Reference for Isabelle/Isar First-Order Logic].
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html Tutorials and manuals for Isabelle2013].

== Lecturas complementarias ==
=== Programación funcional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/i1m/temas/2012-13-IM-temas-PF.pdf Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# J.A. Alonso y M.J. Hidalgo [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# G. Hutton [http://goo.gl/pKqG Programming in Haskell]. Cambridge University Press, 2007.
# M. Lipovača [http://aprendehaskell.es ¡Aprende Haskell por el bien de todos!].

=== Lógica computacional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/temas/temas-LI-2012-13.pdf Temas de "Lógica informática" (2012-13)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# R. Bornat [http://bit.ly/oithic Proof and disproof in formal logic: an introduction for programmers]. Oxford University Press, 2005.
# K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers [http://pubs.doc.ic.ac.uk/reasoned-programming/reasoned-programming.pdf Reasoned programming]. Imperial College, 1994.
# K. Doets y J. van Eijck [http://www.ldc.usb.ve/~astorga/Haskell.Road.pdf The Haskell Road to Logic, Maths and Programming].
# M. Huth y M. Ryan [http://goo.gl/TMqOo Logic in computer science: Modelling and reasoning about systems]. Cambridge University Press, 2004. (Incluye el [http://www.cs.bham.ac.uk/research/lics/tutor/index.html tutor en la Red]).

== Cursos relacionados ==
=== Cursos con Isabelle/HOL ===
# Jeremy Avigad. [http://www.phil.cmu.edu/~avigad/formal/ Logic and Formal Verification]. (Carnegie Mellon, 2009).
# Clemens Ballarin. [http://cl-informatik.uibk.ac.at/teaching/ss08/atp/introduction.php Automatic Deduction]. (Univ de Innsbruck, 2008).
# Clemens Ballarin. [http://www4.in.tum.de/~ballarin/belgrade08-tut/ Introduction to the Isabelle Proof Assistant]. (Belgrado, 2008).
# Clemens Ballarin y Gerwin Klein [http://isabelle.in.tum.de/coursematerial/IJCAR04 Introduction to the Isabelle Proof Assistant]. (en el IJCAR-2004).
# Clemens Ballarin y Tjark Weber. [http://cl-informatik.uibk.ac.at/teaching/ws06/atp/introduction.php Automated Theorem Proving in Isabelle/HOL]. (Univ. de Innsbruck, 2006-07).
# A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. [http://archiv.infsec.ethz.ch/education/permanent/csmr.html Computer-supported Modeling and Reasoning]. (ETH Zurich, 2011).
# Mads Dam. [http://www.csc.kth.se/utbildning/kth/kurser/DD2453/aform07/ Advanced formal methods]. (KTH Royal Institute of Technology, 2007).
# Jacques Fleuriot y Paul Jackson. [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/ Automated reasoning]. (Univ. de Edimburgo, 2012-13).
# Thomas Genet [http://www.irisa.fr/celtique/genet/ACF Software formal analysis and design]. (Univ. de Rennes)
# Gerwin Klein. [http://www.cse.unsw.edu.au/~kleing/teaching/thprv-04 Theorem Proving - Principles, Techniques, Applications]. (NICTA, 2004).
# Gerwin Klein. [http://www.cse.unsw.edu.au/~cs4161/index.html Advanced Topics in Software Verification]. (NICTA, 2012).
# Joao Marcos. [http://www.dimap.ufrn.br/~jmarcos/courses/LC/Ementa.htm Lógica computacional: Demonstração assistida e semi-automática de teoremas].(UFRN, 2000).
# Tobias Nipkow. [http://www4.informatik.tu-muenchen.de/~nipkow/semantics/ Semantics of programming languages]. (Univ. de Munich, 2012-13).
# Tobias Nipkow [http://isabelle.in.tum.de/coursematerial/PSV2009-1 Theorem Proving with Isabelle/HOL An Intensive Course].
# Larry Paulson. [http://www.cl.cam.ac.uk/teaching/0910/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2009-10).
# Arnd Poetzsch-Heffter. [https://softech.informatik.uni-kl.de/Homepage/SVHOL10 Specification and Verification with Higher-Order Logic].
# Viorel Preoteasa, Ralph-Johan Back y Charmi Panchal. [http://users.abo.fi/vpreotea/isabelle-2012 Introduction to mechanized reasoning with Isabelle/HOL]. (Åbo Akademi University, 2012).
# Jeremy G. Siek. [http://www.cs.colorado.edu/~siek/7000/spring07/ Practical Theorem Proving with Isabelle/Isar]. (Univ. de Colorado, 2007).
# Jeremy G. Siek. [http://ecee.colorado.edu/~siek/ecen5013/spring11/ Theorem proving in Isabelle]. (Univ. de Colorado, 2011).
# Jan-Georg Smaus. [http://www.informatik.uni-freiburg.de/~ki/teaching/ws0910/csmr/lecture.html Computer-supported modeling and reasoning]. (Univ. de Feiburgo, 2009).
# Christian Sternagel [http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php Experiments in Verification – Introduction to Isabelle/HOL]. (Univ. de Innsbruck, 2011-12).
# Tjark Weber. [http://www.cl.cam.ac.uk/teaching/1011/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2010-11).

=== Otros cursos ===
# José A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/ Lógica informática] (Univ. de Sevilla, 2012-13).
# Thorsten Altenkirch y Peter Morris [http://www.cs.nott.ac.uk/~txa/g52ifr Introduction to formal reasoning] (Univ. de Nottingham, 2010-11).
# Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey y Assia Mahboubi [http://www.di.ens.fr/~zappa/teaching/coq/ecole11 Modelling and verifying algorithms in Coq: an introduction]. (INRIA Paris-Rocquencourt, 14-18 noviembre 2011).
# Pierre Castéran [http://www.labri.fr/perso/casteran/FM/Logique/index.html Logic (Master In Verification)] (Univ. de Burdeos, 2011-12).
# Adam Chlipala [http://stellar.mit.edu/S/course/6/fa11/6.892/ Interactive computer theorem proving]. (MIT, 2012-13).
# Adam Chlipala y Armando Solar Lezama [https://stellar.mit.edu/S/course/6/fa13/6.820/index.html Foundations of program analysis]. (MIT, 2013-14).
# Robby Findler [http://www.eecs.northwestern.edu/~robby/courses/395-495-2013-fall Certified programming with dependent types]. (Northwestern, 2013-14).
# Nuno Gaspar [http://www-sop.inria.fr/members/Nuno.Gaspar/teaching/coq2012.php Verification with the Coq Proof Assistant] (INRIA Sophia Antipolis, 2012-13).
# Carlos Luna y Gustavo Betarte. [https://eva.fing.edu.uy/course/view.php?id=363 Construcción formal de programas en teoría de tipos]. (Univ. de la República, Uruguay, 2013-14).
# Michael Genesereth [http://logic.stanford.edu/classes/cs157/2011/cs157.html Computational Logic] (Univ. de Stanford, 2011-12).
# Ian Hodkinson [http://www.doc.ic.ac.uk/~imh/teaching/140_logic/logic.html Logic] (Imperial College, Londres, 2010-11).
# Peter Lucas [http://www.cs.ru.nl/~peterl/teaching/KeR/ Knowledge Representation and Reasoning] (Radboud University # egen, 2011-12).
# Larry Paulson [http://www.cl.cam.ac.uk/Teaching/current/LogicProof/ Logic and Proof] (Univ. de Cambridge, 2011-12).
# David Pichardie [http://www.irisa.fr/celtique/pichardie/teaching/M2/MDV/ Méthode de vérification] (Universidad de Rennes, 2006-07).
# Michael Winter [Logic in Computer Science] (Brock University, Ontario, Canada, 2010-11).

== Bibliotecas de ejemplos de verificación ==
# [http://afp.sourceforge.net Archive of Formal Proofs].
# [http://www.cs.ru.nl/~freek/100 Formalizing 100 Theorems].
# [http://toccata.lri.fr/gallery Gallery of verified programs].
# [http://www.cs.nott.ac.uk/~lad/research/challenges/ Induction Challenge Problems].
# [http://automatedreasoning.net/ Larry Wos' Notebooks].
# [http://www.cs.miami.edu/~tptp/ The TPTP Problem Library for Automated Theorem Proving].
# [http://www.macs.hw.ac.uk/vstte10/Competition.html The 1st Verified Software Competition].
# [https://sites.google.com/site/vstte2012/compet The 2nd Verified Software Competition].
# [http://verifythis.cost-ic0701.org VerifyThis (A collection of verification benchmarks].

== Artículos recientes ==
Están en orden cronológico inverso a la fecha de su reseña en [http://www.glc.us.es/~jalonso/vestigium/tag/resena Vestigium]:
# [http://bit.ly/1iZjgqN Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem]. L. Noschinski
# [http://bit.ly/1iJ8uVz A graph library for Isabelle]. ~ L. Noschinski
# [http://bit.ly/I0CU80 Gödel’s incompleteness theorems]. ~ L.C. Paulson
# [http://bit.ly/I0CPRN The hereditarily finite sets]. ~ L.C. Paulson
# [http://bit.ly/HBiIJI Applications of real number theorem proving in PVS]. ~ H. Gottliebsen, R. Hardy, O. Lightfoot y U. Martin
# [http://bit.ly/1awnMLB A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets]. ~ L.C. Paulson
# [http://bit.ly/19lWeYy Verified AIG algorithms in ACL2]. ~ J. Davis y S. Swords
# [http://bit.ly/GAhC00 A formal model and correctness proof for an access control policy framework]. ~ C. Wu, X. Zhang y C. Urban
# [http://bit.ly/16SMvSS The ontological argument in PVS]. ~ J. Rushby
# [http://bit.ly/1dRt9n0 Formalizing Moessner’s theorem and generalizations in Nuprl]. ~ M. Bickford, D. Kozen y A. Silva
# [http://bit.ly/1bSeDNB Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model]. ~ M. Ayala y Y. Santos
# [http://bit.ly/1feFqWE Proof assistant based on didactic considerations]. ~ J. Pais y A Tasistro
# [http://bit.ly/18tHNBi Theory exploration for interactive theorem proving]. ~ M. Johansson
# [http://bit.ly/1b0242s From Tarski to Hilbert]. ~ G. Braun y J. Narboux
# [http://bit.ly/18HaXaR Formal verification of language-based concurrent noninterference]. ~ A. Popescu, J. Hölzl y T. Nipkow
# [http://bit.ly/1aRTQsU A Traffic Alert and Collision Avoidance System(TCAS-II) Resolution Advisory Algorithm]. ~ C. Muñoz, A. Narkawicz y J. Chamberlain
# [http://bit.ly/1dNwhDI Formal verification of cryptographic security proofs]. ~ M. Berg
# [http://bit.ly/17muAUv Polygonal numbers in Mizar]. ~ A. Grabowski
# [http://bit.ly/1hk5z6L A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle]. ~ L.C. Paulson
# [http://bit.ly/1cSL0wE Steps towards verified implementations of HOL Light]. ~ M.O. Myreen, S. Owens y R. Kumar
# [http://bit.ly/16Kbgm0 Generic datatypes à la carte]. ~ S. Keuchel y T. Schrijvers
# [http://bit.ly/1bqJGx4 Proof pearl: A verified bignum implementation in x86-64 machine code]. ~ M.O. Myreen y G. Curello
# [http://bit.ly/142ow2Q Mechanized metatheory for a λ λ-calculus with trust types]. ~ R. Ribeiro, C. Camarão y L. Figueiredo
# [http://bit.ly/15WZBDy Proving soundness of combinatorial Vickrey auctions and generating verified executable code]. ~ M.B. Caminati, M. Kerber, C. Lange y C. Rowat
# [http://bit.ly/198g4n9 A computer-assisted proof of correctness of a marching cubes algorithm]. ~ A.N. Chernikov y J. Xu
# [http://bit.ly/11QA5g7 Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm]. ~ L. Lambán, J. Rubio, F.J. Martín y J.L. Ruiz
# [http://bit.ly/1cJAXYk The Königsberg bridge problem and the friendship theorem]. ~ W. Li
# [http://bit.ly/13DBK9R Formal verification of a proof procedure for the description logic ALC]. ~ M. Chaabani, M. Mezghiche y M. Strecker
# [http://bit.ly/1ep2ex9 Pratt’s primality certificates]. ~ S. Wimmer y L. Noschinski
# [http://bit.ly/13C95Ci Reasoning about higher-order relational specifications]. ~ Y. Wang, K. Chaudhuri, A. Gacek y G. Nadathur
# [http://bit.ly/18QQLcL Proofs you can believe in – Proving equivalences between Prolog semantics in Coq]. ~ J. Kriener, A. King y S. Blazy
# [http://bit.ly/19uc82J Certified, efficient and sharp univariate Taylor models in Coq]. ~ E. Martin-Dorel, L. Rideau, L. Théry, M. Mayero y I. Paşca
# [http://bit.ly/1c4Rzel Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁]. ~ M. Norrish y B. Huffman
# [http://bit.ly/14b4Akz Program verification based on Kleene algebra in Isabelle/HOL] ~ A. Armstrong, G. Struth y T. Weber
# [http://bit.ly/1aOgRKx Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)]. ~ C. Ballarin
# [http://bit.ly/11HKixj Computational verification of network programs in Coq]. ~ G. Stewart
# [http://www.glc.us.es/~jalonso/vestigium/resena-certifying-homological-algorithms-to-study-biomedical-images Certifying homological algorithms to study biomedical images]. ~ M. Poza
# [http://bit.ly/16Nks9m Formalizing cut elimination of coalgebraic logics in Coq]. ~ H. Tews
# [http://www.glc.us.es/~jalonso/vestigium/resena-the-formalization-of-syntax-based-mathematical-algorithms-using-quotation-and-evaluation/ The formalization of syntax-based mathematical algorithms using quotation and evaluation]. ~ W.M. Farmer
# [http://www.glc.us.es/~jalonso/vestigium/resena-certified-symbolic-manipulation-bivariate-simplicial-polynomials/ Certified symbolic manipulation: Bivariate simplicial polynomials]. ~ L. Lambán, F.J. Martín, J. Rubio y J.L. Ruiz
# [http://www.glc.us.es/~jalonso/vestigium/resena-solveurs-cpfd-verifies-formellement/ Solveurs CP(FD) vérifiés formellement]. ~ C Dubois y A. Gotlieb
# [http://www.glc.us.es/~jalonso/vestigium/resena-formalizing-bounded-increase/ Formalizing bounded increase]. ~ R. Thiemann
# [http://www.glc.us.es/~jalonso/vestigium/resena-formal-mathematics-on-display-a-wiki-for-flyspeck/ Formal mathematics on display: A wiki for Flyspeck]. ~ C. Tankink, C. Kaliszyk, J. Urban y H. Geuvers
# [http://www.glc.us.es/~jalonso/vestigium/resena-theorem-of-three-circles-in-coq Theorem of three circles in Coq]. ~ J. Zsidó
# [http://bit.ly/19fiWAY Certified HLints with Isabelle/HOLCF-Prelude]. ~ J. Breitner, B. Huffman, N. Mitchell y C. Sternagel
# [http://bit.ly/ZfSQrQ Automatic data refinement]. ~ P. Lammich
# [http://bit.ly/18vyjm7 The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups)]. ~ A. Mahboubi
# [http://bit.ly/114oyZV Mechanical verification of SAT refutations with extended resolution]. ~ N. Wetzler, M.J.H. Heule y W.A. Hunt Jr.
# [http://bit.ly/13H0REu Type classes and filters for mathematical analysis in Isabelle/HOL] ~ J. Hölzl, F. Immler y B. Huffman
# [http://bit.ly/10fv8wO Verifying refutations with extended resolution]. ~ M. J. H. Heule, W. A. Hunt, Jr. y N. Wetzler
# [http://bit.ly/10EcFWj A Web interface for Isabelle: The next generation]. ~ C. Lüth y M. Ring
# [http://bit.ly/18P9CSv On the formalization of continuous-time Markov chains in HOL]. ~ L. Liu, O. Hasan y S. Tahar
# [http://bit.ly/17H2mqy Formalizing Turing machines]. ~ A. Asperti y W. Ricciotti
# [http://bit.ly/YwuCeL Light-weight containers for Isabelle: efficient, extensible, nestable]. ~ A. Lochbihler
# [http://bit.ly/10XLrRA Graph theory]. ~ L. Noschinski
# [http://bit.ly/19kPEP4 A machine-checked proof of the odd order theorem]. ~ G. Gonthier et als.
# [http://goo.gl/LdihL A constructive theory of regular languages in Coq]. ~ C. Doczkal, J.O. Kaiser y G. Smolka
# [http://goo.gl/gwcwL A formal proof of Kruskal’s tree theorem in Isabelle/HOL]. ~ C. Sternagel
# [http://goo.gl/CUF3e Formalizing Knuth-Bendix orders and Knuth-Bendix completion]. ~ C. Sternagel y R. Thiemann
# [http://goo.gl/9JAfX Developing an auction theory toolbox]. ~ C. Lange, C. Rowat, W. Windsteiger y M. Kerber
# [http://goo.gl/6OfmQ Formalization of incremental simplex algorithm by stepwise refinement]. ~ M. Spasić y F. Marić
# [http://goo.gl/Guxky Coinductive pearl: Modular first-order logic completeness]. ~ J.C. Blanchette, A. Popescu y D. Traytel
# [http://goo.gl/HUOl8 A fully verified executable LTL model checker]. ~ J. Esparza et als.
# [http://goo.gl/RV54S ForMaRE - formal mathematical reasoning in economics]. ~ M. Kerber, C. Lange y C. Rowat.
# [http://goo.gl/Y7sIq AI over large formal knowledge bases: The first decade]. ~ J. Urban.
# [http://goo.gl/vvqNg Formalization of real analysis: A survey of proof assistants and libraries]. ~ S. Boldo, C. Lelay y G. Melquiond.
# [http://goo.gl/bEFYa Data refinement in Isabelle/HOL]. ~ F. Haftmann, A. Krauss, O. Kunčar y T. Nipkow
# [http://goo.gl/xTyvE Formalizing the confluence of orthogonal rewriting systems]. ~ A.C. Rocha y M. Ayala.
# [http://goo.gl/zCYHj Formalization of the complex number theory in HOL4]. ~ Z. Shi et als.
# [http://goo.gl/kM0dI Programming and reasonning with PowerLists in Coq]. ~ F. Loulergue y V. Niculescu
# [http://goo.gl/KkU6s A hierarchy of mathematical structures in ACL2]. ~ J. Heras, F.J. Martín y V. Pascual.
# [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing Machines and Computability Theory in Isabelle/HOL] ~ J. Xu, X. Zhang y C. Urban

Documentación

2015-12-23T15:12:14Z

Jalonso: /* Referencias sobre Isabelle/HOL */

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

== Visiones generales de la DAO ==

# J.A. Alonso. [http://goo.gl/NWk7b Razonamiento formalizado: Del sueño a la realidad de las pruebas]. ''Vestigium'', 26 de diciembre de 2012.
# J. Avigad. [http://www.andrew.cmu.edu/user/avigad/Talks/icerm.pdf Interactive theorem proving, automated reasoning, and mathematical computation]. ICERM, 14 de diciembre de 2012.
# 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.
# H. Geuvers [http://www.ias.ac.in/sadhana/Pdf2009Feb/3.pdf Proof assistants: History, ideas and future]. ''Sadhana'', Vol. 34-1, pp. 3-25, février 2009.
# G. Gonthier [http://www.ams.org/notices/200811/tx081101382p.pdf The four-color theorem]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1382-1393, 2008.
# 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?].
# F. Wiedijk [http://www.cs.ru.nl/~freek/100/ Formalizing the «top 100» of mathematical theorems].
# F. Wiedijk [http://www.ams.org/notices/200811/tx081101408p.pdf Formal proof - Getting started]. ''Notices of the AMS'', Vol. 55, n° 11, pp. 1408-1414, 2008.
# F. Wiedijk, [http://www.cs.ru.nl/~freek/pubs/qed2.ps.gz The QED manifesto revisited]. ''Studies in Logic, Grammar and Rhetoric'', Vol. 10(23), pp. 121-133, 2007.

== Referencias sobre Isabelle/HOL ==
# B. Grechuk [http://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf Isabelle primer for mathematicians].
# T. Nipkow [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2015/doc/prog-prove.pdf Programming and proving in Isabelle/HOL]. 25 de mayo de 2015
# T. Nipkow, M. Wenzel y L.C. Paulson [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/tutorial.pdf A proof assistant for higher-order logic]. Springer-Verlag. 5 de diciembre de 2013.
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/HOL/HOL/document.pdf Isabelle/HOL — Higher-Order Logic]. 5 de diciembre de 2013.
# M. Wenzel [http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/isar-ref.pdf The Isabelle/Isar Reference Manual]. 5 de diciembre de 2013.
# M. Wenzel [https://www.lri.fr/~wenzel/Isabelle2011-Paris/quickref.pdf The Isabelle/Isar quick reference].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref.pdf Quick Reference for Isabelle/Isar Propositional Logic].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref2.pdf Quick Reference for Isabelle/Isar More Proof Techniques].
# J. Siek [http://ecee.colorado.edu/~siek/ecen3703/spring10/quick-ref3.pdf Quick Reference for Isabelle/Isar First-Order Logic].
# [http://www.cl.cam.ac.uk/research/hvg/Isabelle/documentation.html Tutorials and manuals for Isabelle2013].

== Lecturas complementarias ==
=== Programación funcional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/i1m/temas/2012-13-IM-temas-PF.pdf Temas de "Programación funcional"]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# J.A. Alonso y M.J. Hidalgo [http://www.cs.us.es/~jalonso/publicaciones/Piensa_en_Haskell.pdf Piensa en Haskell (Ejercicios de programación funcional con Haskell)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# G. Hutton [http://goo.gl/pKqG Programming in Haskell]. Cambridge University Press, 2007.
# M. Lipovača [http://aprendehaskell.es ¡Aprende Haskell por el bien de todos!].

=== Lógica computacional ===
# J.A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/temas/temas-LI-2012-13.pdf Temas de "Lógica informática" (2012-13)]. Publicaciones del Grupo de Lógica Computacional. Universidad de Sevilla, 2012.
# R. Bornat [http://bit.ly/oithic Proof and disproof in formal logic: an introduction for programmers]. Oxford University Press, 2005.
# K. Broda, S. Eisenbach, H. Khoshnevisan y S. Vickers [http://pubs.doc.ic.ac.uk/reasoned-programming/reasoned-programming.pdf Reasoned programming]. Imperial College, 1994.
# K. Doets y J. van Eijck [http://www.ldc.usb.ve/~astorga/Haskell.Road.pdf The Haskell Road to Logic, Maths and Programming].
# M. Huth y M. Ryan [http://goo.gl/TMqOo Logic in computer science: Modelling and reasoning about systems]. Cambridge University Press, 2004. (Incluye el [http://www.cs.bham.ac.uk/research/lics/tutor/index.html tutor en la Red]).

== Cursos relacionados ==
=== Cursos con Isabelle/HOL ===
# Jeremy Avigad. [http://www.phil.cmu.edu/~avigad/formal/ Logic and Formal Verification]. (Carnegie Mellon, 2009).
# Clemens Ballarin. [http://cl-informatik.uibk.ac.at/teaching/ss08/atp/introduction.php Automatic Deduction]. (Univ de Innsbruck, 2008).
# Clemens Ballarin. [http://www4.in.tum.de/~ballarin/belgrade08-tut/ Introduction to the Isabelle Proof Assistant]. (Belgrado, 2008).
# Clemens Ballarin y Gerwin Klein [http://isabelle.in.tum.de/coursematerial/IJCAR04 Introduction to the Isabelle Proof Assistant]. (en el IJCAR-2004).
# Clemens Ballarin y Tjark Weber. [http://cl-informatik.uibk.ac.at/teaching/ws06/atp/introduction.php Automated Theorem Proving in Isabelle/HOL]. (Univ. de Innsbruck, 2006-07).
# A.D. Brucker, D. Basin, J.G. Smaus y B. Wolff. [http://archiv.infsec.ethz.ch/education/permanent/csmr.html Computer-supported Modeling and Reasoning]. (ETH Zurich, 2011).
# Mads Dam. [http://www.csc.kth.se/utbildning/kth/kurser/DD2453/aform07/ Advanced formal methods]. (KTH Royal Institute of Technology, 2007).
# Jacques Fleuriot y Paul Jackson. [http://www.inf.ed.ac.uk/teaching/courses/ar/slides/ Automated reasoning]. (Univ. de Edimburgo, 2012-13).
# Thomas Genet [http://www.irisa.fr/celtique/genet/ACF Software formal analysis and design]. (Univ. de Rennes)
# Gerwin Klein. [http://www.cse.unsw.edu.au/~kleing/teaching/thprv-04 Theorem Proving - Principles, Techniques, Applications]. (NICTA, 2004).
# Gerwin Klein. [http://www.cse.unsw.edu.au/~cs4161/index.html Advanced Topics in Software Verification]. (NICTA, 2012).
# Joao Marcos. [http://www.dimap.ufrn.br/~jmarcos/courses/LC/Ementa.htm Lógica computacional: Demonstração assistida e semi-automática de teoremas].(UFRN, 2000).
# Tobias Nipkow. [http://www4.informatik.tu-muenchen.de/~nipkow/semantics/ Semantics of programming languages]. (Univ. de Munich, 2012-13).
# Tobias Nipkow [http://isabelle.in.tum.de/coursematerial/PSV2009-1 Theorem Proving with Isabelle/HOL An Intensive Course].
# Larry Paulson. [http://www.cl.cam.ac.uk/teaching/0910/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2009-10).
# Arnd Poetzsch-Heffter. [https://softech.informatik.uni-kl.de/Homepage/SVHOL10 Specification and Verification with Higher-Order Logic].
# Viorel Preoteasa, Ralph-Johan Back y Charmi Panchal. [http://users.abo.fi/vpreotea/isabelle-2012 Introduction to mechanized reasoning with Isabelle/HOL]. (Åbo Akademi University, 2012).
# Jeremy G. Siek. [http://www.cs.colorado.edu/~siek/7000/spring07/ Practical Theorem Proving with Isabelle/Isar]. (Univ. de Colorado, 2007).
# Jeremy G. Siek. [http://ecee.colorado.edu/~siek/ecen5013/spring11/ Theorem proving in Isabelle]. (Univ. de Colorado, 2011).
# Jan-Georg Smaus. [http://www.informatik.uni-freiburg.de/~ki/teaching/ws0910/csmr/lecture.html Computer-supported modeling and reasoning]. (Univ. de Feiburgo, 2009).
# Christian Sternagel [http://cl-informatik.uibk.ac.at/teaching/ss11/eve/content.php Experiments in Verification – Introduction to Isabelle/HOL]. (Univ. de Innsbruck, 2011-12).
# Tjark Weber. [http://www.cl.cam.ac.uk/teaching/1011/L21/ Interactive Formal Verification]. (Univ. de Cambridge, 2010-11).

=== Otros cursos ===
# José A. Alonso [http://www.cs.us.es/~jalonso/cursos/li/ Lógica informática] (Univ. de Sevilla, 2012-13).
# Thorsten Altenkirch y Peter Morris [http://www.cs.nott.ac.uk/~txa/g52ifr Introduction to formal reasoning] (Univ. de Nottingham, 2010-11).
# Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey y Assia Mahboubi [http://www.di.ens.fr/~zappa/teaching/coq/ecole11 Modelling and verifying algorithms in Coq: an introduction]. (INRIA Paris-Rocquencourt, 14-18 noviembre 2011).
# Pierre Castéran [http://www.labri.fr/perso/casteran/FM/Logique/index.html Logic (Master In Verification)] (Univ. de Burdeos, 2011-12).
# Adam Chlipala [http://stellar.mit.edu/S/course/6/fa11/6.892/ Interactive computer theorem proving]. (MIT, 2012-13).
# Adam Chlipala y Armando Solar Lezama [https://stellar.mit.edu/S/course/6/fa13/6.820/index.html Foundations of program analysis]. (MIT, 2013-14).
# Robby Findler [http://www.eecs.northwestern.edu/~robby/courses/395-495-2013-fall Certified programming with dependent types]. (Northwestern, 2013-14).
# Nuno Gaspar [http://www-sop.inria.fr/members/Nuno.Gaspar/teaching/coq2012.php Verification with the Coq Proof Assistant] (INRIA Sophia Antipolis, 2012-13).
# Carlos Luna y Gustavo Betarte. [https://eva.fing.edu.uy/course/view.php?id=363 Construcción formal de programas en teoría de tipos]. (Univ. de la República, Uruguay, 2013-14).
# Michael Genesereth [http://logic.stanford.edu/classes/cs157/2011/cs157.html Computational Logic] (Univ. de Stanford, 2011-12).
# Ian Hodkinson [http://www.doc.ic.ac.uk/~imh/teaching/140_logic/logic.html Logic] (Imperial College, Londres, 2010-11).
# Peter Lucas [http://www.cs.ru.nl/~peterl/teaching/KeR/ Knowledge Representation and Reasoning] (Radboud University # egen, 2011-12).
# Larry Paulson [http://www.cl.cam.ac.uk/Teaching/current/LogicProof/ Logic and Proof] (Univ. de Cambridge, 2011-12).
# David Pichardie [http://www.irisa.fr/celtique/pichardie/teaching/M2/MDV/ Méthode de vérification] (Universidad de Rennes, 2006-07).
# Michael Winter [Logic in Computer Science] (Brock University, Ontario, Canada, 2010-11).

== Bibliotecas de ejemplos de verificación ==
# [http://afp.sourceforge.net Archive of Formal Proofs].
# [http://www.cs.ru.nl/~freek/100 Formalizing 100 Theorems].
# [http://toccata.lri.fr/gallery Gallery of verified programs].
# [http://www.cs.nott.ac.uk/~lad/research/challenges/ Induction Challenge Problems].
# [http://automatedreasoning.net/ Larry Wos' Notebooks].
# [http://www.cs.miami.edu/~tptp/ The TPTP Problem Library for Automated Theorem Proving].
# [http://www.macs.hw.ac.uk/vstte10/Competition.html The 1st Verified Software Competition].
# [https://sites.google.com/site/vstte2012/compet The 2nd Verified Software Competition].
# [http://verifythis.cost-ic0701.org VerifyThis (A collection of verification benchmarks].

== Artículos recientes ==
Están en orden cronológico inverso a la fecha de su reseña en [http://www.glc.us.es/~jalonso/vestigium/tag/resena Vestigium]:
# [http://bit.ly/1iZjgqN Proof Pearl: A probabilistic proof for the Girth-Chromatic number theorem]. L. Noschinski
# [http://bit.ly/1iJ8uVz A graph library for Isabelle]. ~ L. Noschinski
# [http://bit.ly/I0CU80 Gödel’s incompleteness theorems]. ~ L.C. Paulson
# [http://bit.ly/I0CPRN The hereditarily finite sets]. ~ L.C. Paulson
# [http://bit.ly/HBiIJI Applications of real number theorem proving in PVS]. ~ H. Gottliebsen, R. Hardy, O. Lightfoot y U. Martin
# [http://bit.ly/1awnMLB A machine-assisted proof of Gödel’s incompleteness theorems for the theory of hereditarily finite sets]. ~ L.C. Paulson
# [http://bit.ly/19lWeYy Verified AIG algorithms in ACL2]. ~ J. Davis y S. Swords
# [http://bit.ly/GAhC00 A formal model and correctness proof for an access control policy framework]. ~ C. Wu, X. Zhang y C. Urban
# [http://bit.ly/16SMvSS The ontological argument in PVS]. ~ J. Rushby
# [http://bit.ly/1dRt9n0 Formalizing Moessner’s theorem and generalizations in Nuprl]. ~ M. Bickford, D. Kozen y A. Silva
# [http://bit.ly/1bSeDNB Formalization in PVS of balancing properties necessary for the security of the Dolev-Yao cascade protocol model]. ~ M. Ayala y Y. Santos
# [http://bit.ly/1feFqWE Proof assistant based on didactic considerations]. ~ J. Pais y A Tasistro
# [http://bit.ly/18tHNBi Theory exploration for interactive theorem proving]. ~ M. Johansson
# [http://bit.ly/1b0242s From Tarski to Hilbert]. ~ G. Braun y J. Narboux
# [http://bit.ly/18HaXaR Formal verification of language-based concurrent noninterference]. ~ A. Popescu, J. Hölzl y T. Nipkow
# [http://bit.ly/1aRTQsU A Traffic Alert and Collision Avoidance System(TCAS-II) Resolution Advisory Algorithm]. ~ C. Muñoz, A. Narkawicz y J. Chamberlain
# [http://bit.ly/1dNwhDI Formal verification of cryptographic security proofs]. ~ M. Berg
# [http://bit.ly/17muAUv Polygonal numbers in Mizar]. ~ A. Grabowski
# [http://bit.ly/1hk5z6L A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle]. ~ L.C. Paulson
# [http://bit.ly/1cSL0wE Steps towards verified implementations of HOL Light]. ~ M.O. Myreen, S. Owens y R. Kumar
# [http://bit.ly/16Kbgm0 Generic datatypes à la carte]. ~ S. Keuchel y T. Schrijvers
# [http://bit.ly/1bqJGx4 Proof pearl: A verified bignum implementation in x86-64 machine code]. ~ M.O. Myreen y G. Curello
# [http://bit.ly/142ow2Q Mechanized metatheory for a λ λ-calculus with trust types]. ~ R. Ribeiro, C. Camarão y L. Figueiredo
# [http://bit.ly/15WZBDy Proving soundness of combinatorial Vickrey auctions and generating verified executable code]. ~ M.B. Caminati, M. Kerber, C. Lange y C. Rowat
# [http://bit.ly/198g4n9 A computer-assisted proof of correctness of a marching cubes algorithm]. ~ A.N. Chernikov y J. Xu
# [http://bit.ly/11QA5g7 Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm]. ~ L. Lambán, J. Rubio, F.J. Martín y J.L. Ruiz
# [http://bit.ly/1cJAXYk The Königsberg bridge problem and the friendship theorem]. ~ W. Li
# [http://bit.ly/13DBK9R Formal verification of a proof procedure for the description logic ALC]. ~ M. Chaabani, M. Mezghiche y M. Strecker
# [http://bit.ly/1ep2ex9 Pratt’s primality certificates]. ~ S. Wimmer y L. Noschinski
# [http://bit.ly/13C95Ci Reasoning about higher-order relational specifications]. ~ Y. Wang, K. Chaudhuri, A. Gacek y G. Nadathur
# [http://bit.ly/18QQLcL Proofs you can believe in – Proving equivalences between Prolog semantics in Coq]. ~ J. Kriener, A. King y S. Blazy
# [http://bit.ly/19uc82J Certified, efficient and sharp univariate Taylor models in Coq]. ~ E. Martin-Dorel, L. Rideau, L. Théry, M. Mayero y I. Paşca
# [http://bit.ly/1c4Rzel Ordinals in HOL: Transfinite arithmetic up to (and beyond) ω₁]. ~ M. Norrish y B. Huffman
# [http://bit.ly/14b4Akz Program verification based on Kleene algebra in Isabelle/HOL] ~ A. Armstrong, G. Struth y T. Weber
# [http://bit.ly/1aOgRKx Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)]. ~ C. Ballarin
# [http://bit.ly/11HKixj Computational verification of network programs in Coq]. ~ G. Stewart
# [http://www.glc.us.es/~jalonso/vestigium/resena-certifying-homological-algorithms-to-study-biomedical-images Certifying homological algorithms to study biomedical images]. ~ M. Poza
# [http://bit.ly/16Nks9m Formalizing cut elimination of coalgebraic logics in Coq]. ~ H. Tews
# [http://www.glc.us.es/~jalonso/vestigium/resena-the-formalization-of-syntax-based-mathematical-algorithms-using-quotation-and-evaluation/ The formalization of syntax-based mathematical algorithms using quotation and evaluation]. ~ W.M. Farmer
# [http://www.glc.us.es/~jalonso/vestigium/resena-certified-symbolic-manipulation-bivariate-simplicial-polynomials/ Certified symbolic manipulation: Bivariate simplicial polynomials]. ~ L. Lambán, F.J. Martín, J. Rubio y J.L. Ruiz
# [http://www.glc.us.es/~jalonso/vestigium/resena-solveurs-cpfd-verifies-formellement/ Solveurs CP(FD) vérifiés formellement]. ~ C Dubois y A. Gotlieb
# [http://www.glc.us.es/~jalonso/vestigium/resena-formalizing-bounded-increase/ Formalizing bounded increase]. ~ R. Thiemann
# [http://www.glc.us.es/~jalonso/vestigium/resena-formal-mathematics-on-display-a-wiki-for-flyspeck/ Formal mathematics on display: A wiki for Flyspeck]. ~ C. Tankink, C. Kaliszyk, J. Urban y H. Geuvers
# [http://www.glc.us.es/~jalonso/vestigium/resena-theorem-of-three-circles-in-coq Theorem of three circles in Coq]. ~ J. Zsidó
# [http://bit.ly/19fiWAY Certified HLints with Isabelle/HOLCF-Prelude]. ~ J. Breitner, B. Huffman, N. Mitchell y C. Sternagel
# [http://bit.ly/ZfSQrQ Automatic data refinement]. ~ P. Lammich
# [http://bit.ly/18vyjm7 The rooster and the butterflies (a machine-checked proof of the Jordan-Hölder theorem for finite groups)]. ~ A. Mahboubi
# [http://bit.ly/114oyZV Mechanical verification of SAT refutations with extended resolution]. ~ N. Wetzler, M.J.H. Heule y W.A. Hunt Jr.
# [http://bit.ly/13H0REu Type classes and filters for mathematical analysis in Isabelle/HOL] ~ J. Hölzl, F. Immler y B. Huffman
# [http://bit.ly/10fv8wO Verifying refutations with extended resolution]. ~ M. J. H. Heule, W. A. Hunt, Jr. y N. Wetzler
# [http://bit.ly/10EcFWj A Web interface for Isabelle: The next generation]. ~ C. Lüth y M. Ring
# [http://bit.ly/18P9CSv On the formalization of continuous-time Markov chains in HOL]. ~ L. Liu, O. Hasan y S. Tahar
# [http://bit.ly/17H2mqy Formalizing Turing machines]. ~ A. Asperti y W. Ricciotti
# [http://bit.ly/YwuCeL Light-weight containers for Isabelle: efficient, extensible, nestable]. ~ A. Lochbihler
# [http://bit.ly/10XLrRA Graph theory]. ~ L. Noschinski
# [http://bit.ly/19kPEP4 A machine-checked proof of the odd order theorem]. ~ G. Gonthier et als.
# [http://goo.gl/LdihL A constructive theory of regular languages in Coq]. ~ C. Doczkal, J.O. Kaiser y G. Smolka
# [http://goo.gl/gwcwL A formal proof of Kruskal’s tree theorem in Isabelle/HOL]. ~ C. Sternagel
# [http://goo.gl/CUF3e Formalizing Knuth-Bendix orders and Knuth-Bendix completion]. ~ C. Sternagel y R. Thiemann
# [http://goo.gl/9JAfX Developing an auction theory toolbox]. ~ C. Lange, C. Rowat, W. Windsteiger y M. Kerber
# [http://goo.gl/6OfmQ Formalization of incremental simplex algorithm by stepwise refinement]. ~ M. Spasić y F. Marić
# [http://goo.gl/Guxky Coinductive pearl: Modular first-order logic completeness]. ~ J.C. Blanchette, A. Popescu y D. Traytel
# [http://goo.gl/HUOl8 A fully verified executable LTL model checker]. ~ J. Esparza et als.
# [http://goo.gl/RV54S ForMaRE - formal mathematical reasoning in economics]. ~ M. Kerber, C. Lange y C. Rowat.
# [http://goo.gl/Y7sIq AI over large formal knowledge bases: The first decade]. ~ J. Urban.
# [http://goo.gl/vvqNg Formalization of real analysis: A survey of proof assistants and libraries]. ~ S. Boldo, C. Lelay y G. Melquiond.
# [http://goo.gl/bEFYa Data refinement in Isabelle/HOL]. ~ F. Haftmann, A. Krauss, O. Kunčar y T. Nipkow
# [http://goo.gl/xTyvE Formalizing the confluence of orthogonal rewriting systems]. ~ A.C. Rocha y M. Ayala.
# [http://goo.gl/zCYHj Formalization of the complex number theory in HOL4]. ~ Z. Shi et als.
# [http://goo.gl/kM0dI Programming and reasonning with PowerLists in Coq]. ~ F. Loulergue y V. Niculescu
# [http://goo.gl/KkU6s A hierarchy of mathematical structures in ACL2]. ~ J. Heras, F.J. Martín y V. Pascual.
# [http://www.inf.kcl.ac.uk/staff/urbanc/Publications/tm.pdf Mechanising Turing Machines and Computability Theory in Isabelle/HOL] ~ J. Xu, X. Zhang y C. Urban

Relación 2

2015-12-15T11:25:25Z

Jalonso:

<source lang="isar">
header {* R2: Razonamiento sobre programas en Isabelle/HOL *}

theory R2
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
------------------------------------------------------------------ *}

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

value "sumaImpares 5" -- "= 25"

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

-- "angfraalv"
lemma "sumaImpares n = n*n"
by (induct n) simp_all

-- "jospalhid marsoldia2"
lemma "sumaImpares n = n*n"
by (induct n) auto

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
------------------------------------------------------------------ *}

-- "angfraalv jospalhid marsoldia2"
fun sumaPotenciasDeDosMasUno :: "nat ⇒ nat" where
"sumaPotenciasDeDosMasUno 0 = 2 " |
"sumaPotenciasDeDosMasUno (Suc n) = sumaPotenciasDeDosMasUno n + 2^(Suc n)"

value "sumaPotenciasDeDosMasUno 3" -- "= 16"

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

-- "angfraalv"
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
by (induct n) simp_all

-- "jospalhid marsoldia2"
lemma "sumaPotenciasDeDosMasUno n = 2^(n+1)"
by (induct n) auto

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]
------------------------------------------------------------------ *}

-- "angfraalv marsoldia2"
fun copia :: "nat ⇒ 'a ⇒ 'a list" where
"copia 0 x = []" |
"copia (Suc n) x = (copia n x)@[x]"

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

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

value "copia2 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 ∧
----------------------------------------------------------------- *}

-- "angfraalv jospalhid marsoldia2"
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
"todos _ [] = True " |
"todos p (x#xs) = (p x ∧ todos p xs)"

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.
------------------------------------------------------------------- *}

-- "jospalhid marsoldia2"
lemma "todos (λy. y=x) (copia2 n x)"
by (induct n) auto

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

--"angfraalv jospalhid marsoldia2"
fun factR :: "nat ⇒ nat" where
"factR 0 = 1" |
"factR (Suc n) = Suc n * factR n"

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"

-- "jospalhid"
lemma fact: "factI' n x = x * factR n"
by (induct n arbitrary: x) auto

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

-- "jospalhid"
corollary "factI n = factR n"
by (simp add:fact)

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]
------------------------------------------------------------------ *}

-- "angfraalv marsoldia2"
fun amplia :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia [] y = y#[]" |
"amplia (x#xs) y = x#(amplia xs y)"

-- "jospalhid"
fun amplia2 :: "'a list ⇒ 'a ⇒ 'a list" where
"amplia2 [] y = [y]"|
"amplia2 (x#xs) y = x#(amplia xs y)"

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

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

-- "jospalhid"
lemma "amplia xs y = xs @ [y]"
by (induct xs) auto

end
</source>

Relación 3

2015-12-14T16:06:39Z

Jalonso: Página creada con '<source lang="isar"> header {* R3: Razonamiento sobre programas en Isabelle/HOL *} theory R3 imports Main begin text {* ------------------------------------------------------...'

<source lang="isar">
header {* R3: Razonamiento sobre programas en Isabelle/HOL *}

theory R3
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>

R3

2015-12-14T16:06:23Z

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

R3

2015-12-14T16:06:11Z

Ejercicios

2015-12-14T16:05:38Z

Jalonso:

== Relaciones de ejercicios ==

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/HOL. ([[R1 |Enunciado]] y [[Relación 1 | Solución colaborativa]]).
* '''Relación 2''': Razonamiento automático sobre programas en Isabelle/HOL. ([[R2 |Enunciado]] y [[Relación 2 | Solución colaborativa]]).
* '''Relación 3''': Razonamiento estructurado sobre programas en Isabelle/HOL. ([[R3 |Enunciado]] y [[Relación 3 | Solución colaborativa]]).

Tema 3: Razonamiento estructurado sobre programas en Isabelle/HOL

2015-12-14T16:04:15Z

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

<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 2a y se demostraron
automáticamente en el tema 2b. A diferencia del tema 2b, ahora
nos fijamos no sólo en el método de demostración sino en la estructura
de la prueba resaltando su semejanza con las del tema 2a. *}

section {* Razonamiento ecuacional *}

text {* ----------------------------------------------------------------
Ejemplo 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 [a,c,d] = 3
------------------------------------------------------------------- *}

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

value "longitud [a,c,d]" -- "= 3"

text {* ---------------------------------------------------------------
Ejemplo 2. Demostrar que
longitud [a,c,d] = 3
------------------------------------------------------------------- *}

lemma "longitud [a,c,d] = 3"
by simp

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 4. (p.6) Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

-- "La demostración detallada es"
lemma "intercambia (intercambia (x,y)) = (x,y)"
proof -
have "intercambia (intercambia (x,y)) = intercambia (y,x)"
by (simp only: intercambia.simps)
also have "... = (x,y)"
by (simp only: intercambia.simps)
finally show "intercambia (intercambia (x,y)) = (x,y)" by simp
qed

text {*
Notas sobre el lenguaje: En la demostración anterior se ha usado
· "proof" para iniciar la prueba,
· "-" (después de "proof") para no usar el método por defecto,
· "have" para establecer un paso,
· "by (simp only: intercambia.simps)" para indicar que sólo se usa
como regla de escritura la correspondiente a la definición de
intercambia,
· "also" para encadenar pasos ecuacionales,
· "..." para representar la igualdad anterior en un razonamiento
ecuacional,
· "finally" para indicar el último pasa de un razonamiento ecuacional,
· "show" para establecer la conclusión.
· "by simp" para indicar el método de demostración por simplificación y
· "qed" para terminar la pruebas,
*}

text {*
La definición de la función intercambia genera una regla de
simplificación
· intercambia.simps: intercambia (x,y) = (y,x)

Se puede ver con
· thm intercambia.simps
*}

-- "La demostración estructurada es"
lemma "intercambia (intercambia (x,y)) = (x,y)"
proof -
have "intercambia (intercambia (x,y)) = intercambia (y,x)" by simp
also have "... = (x,y)" by simp
finally show "intercambia (intercambia (x,y)) = (x,y)" by simp
qed

text {*
Nota: La diferencia entre las dos demostraciones es que en los dos
primeros pasos no se explicita la regla de simplificación.
*}

-- "La demostración automática es"
lemma "intercambia (intercambia (x,y)) = (x,y)"
by simp

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 6. (p. 9) Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

-- "La demostración detallada es"
lemma "inversa [x] = [x]"
proof -
have "inversa [x] = inversa (x#[])" by simp
also have "... = (inversa []) @ [x]" by (simp only: inversa.simps(2))
also have "... = [] @ [x]" by (simp only: inversa.simps(1))
also have "... = [x]" by (simp only: append_Nil)
finally show "inversa [x] = [x]" by simp
qed

text {*
En la demostración anterior se han usado las siguientes reglas:
· inversa.simps(1): inversa [] = []
· inversa.simps(2): inversa (x#xs) = inversa xs @ [x]
· append_Nil: [] @ ys = ys
*}

-- "La demostración estructurada es"
lemma "inversa [x] = [x]"
proof -
have "inversa [x] = inversa (x#[])" by simp
also have "... = (inversa []) @ [x]" by simp
also have "... = [] @ [x]" by simp
also have "... = [x]" by simp
finally show "inversa [x] = [x]" by simp
qed

-- "La demostración automática es"
lemma "inversa [x] = [x]"
by simp

section {* Razonamiento por inducción sobre los naturales *}

text {*
[Principio de inducción sobre los naturales] Para demostrar una
propiedad P para todos los números naturales basta probar que el 0
tiene la propiedad P y que si n tiene la propiedad P, entonces n+1
también la tiene.
⟦P 0; ⋀n. P n ⟹ P (Suc n)⟧ ⟹ P m

En Isabelle el principio de inducción sobre los naturales está
formalizado en el teorema nat.induct y puede verse con
thm nat.induct
*}

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 8. (p. 18) Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "longitud (repite n x) = n"
proof (induct n)
show "longitud (repite 0 x) = 0" by simp
next
fix n
assume HI: "longitud (repite n x) = n"
have "longitud (repite (Suc n) x) = longitud (x # (repite n x))"
by simp
also have "... = 1 + longitud (repite n x)" by simp
also have "... = 1 + n" using HI by simp
finally show "longitud (repite (Suc n) x) = Suc n" by simp
qed

text {*
Comentarios sobre la demostración anterior:
· A la derecha de proof se indica el método de la demostración.
· (induct n) indica que la demostración se hará por inducción en n.
· Se generan dos subobjetivos correspondientes a la base y el paso de
inducción:
1. longitud (repite 0 x) = 0
2. ⋀n. longitud (repite n x) = n ⟹ longitud (repite (Suc n) x) = Suc n
donde ⋀n se lee "para todo n".
· "next" indica el siguiente subobjetivo.
· "fix n" indica "sea n un número natural cualquiera"
· assume HI: "longitud (repite n x) = n" indica «supongamos que
"longitud (repite n x) = n" y sea HI la etiqueta de este supuesto».
· "using HI" usando la propiedad etiquetada con HI.
*}

-- "La demostración automática es"
lemma "longitud (repite n x) = n"
by (induct n) auto

section {* Razonamiento por inducción sobre listas *}

text {*
Para demostrar una propiedad para todas las listas basta demostrar
que la lista vacía tiene la propiedad y que al añadir un elemento a una
lista que tiene la propiedad se obtiene otra lista que también tiene la
propiedad.

En Isabelle el principio de inducción sobre listas está formalizado
mediante el teorema list.induct
⟦P [];
⋀x xs. P xs ⟹ P (x#xs)⟧
⟹ P xs
*}

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 10. (p. 24) Demostrar que
conc xs (conc ys zs) = (conc xs ys) zs
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
proof (induct xs)
show "conc [] (conc ys zs) = conc (conc [] ys) zs" by simp
next
fix x xs
assume HI: "conc xs (conc ys zs) = conc (conc xs ys) zs"
have "conc (x # xs) (conc ys zs) = x # (conc xs (conc ys zs))" by simp
also have "... = x # (conc (conc xs ys) zs)" using HI by simp
also have "... = conc (conc (x # xs) ys) zs" by simp
finally show "conc (x # xs) (conc ys zs) = conc (conc (x # xs) ys) zs" by simp
qed

text {*
Comentario sobre la demostración anterior
· (induct xs) genera dos subobjetivos:
1. conc [] (conc ys zs) = conc (conc [] ys) zs
2. ⋀a xs. conc xs (conc ys zs) = conc (conc xs ys) zs ⟹
conc (a#xs) (conc ys zs) = conc (conc (a#xs) ys) zs
*}

-- "La demostración automática es"
lemma "conc xs (conc ys zs) = conc (conc xs ys) zs"
by (induct xs) auto

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

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

text {* Encuentra el contraejemplo,
xs = [a⇣2]
ys = [a⇣1] *}

text {* ---------------------------------------------------------------
Ejemplo 12. (p. 28) Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "conc xs [] = xs"
proof (induct xs)
show "conc [] [] = []" by simp
next
fix x xs
assume HI: "conc xs [] = xs"
have "conc (x # xs) [] = x # (conc xs [])" by simp
also have "... = x # xs" using HI by simp
finally show "conc (x # xs) [] = x # xs" by simp
qed

-- "La demostración automática es"
lemma "conc xs [] = xs"
by (induct xs) auto

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

-- "La demostración automática es"
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
proof (induct xs)
show "longitud (conc [] ys) = longitud [] + longitud ys" by simp
next
fix x xs
assume HI: "longitud (conc xs ys) = longitud xs + longitud ys"
have "longitud (conc (x # xs) ys) = longitud (x # (conc xs ys))"
by simp
also have "... = 1 + longitud (conc xs ys)" by simp
also have "... = 1 + longitud xs + longitud ys" using HI by simp
also have "... = longitud (x # xs) + longitud ys" by simp
finally show "longitud (conc (x # xs) ys) =
longitud (x # xs) + longitud ys" by simp
qed

-- "La demostración automática es"
lemma "longitud (conc xs ys) = longitud xs + longitud ys"
by (induct xs) auto

section {* Inducción correspondiente a la definición recursiva *}

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 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 {*
La definición coge genera el esquema de inducción coge.induct:
⟦⋀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 {* ---------------------------------------------------------------
Ejemplo 16. (p. 35) Demostrar que
conc (coge n xs) (elimina n xs) = xs
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "conc (coge n xs) (elimina n xs) = xs"
proof (induct rule: coge.induct)
fix n
show "conc (coge n []) (elimina n []) = []" by simp
next
fix x xs
show "conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs" by simp
next
fix n x xs
assume HI: "conc (coge n xs) (elimina n xs) = xs"
have "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) =
conc (x#(coge n xs)) (elimina n xs)" by simp
also have "... = x#(conc (coge n xs) (elimina n xs))" by simp
also have "... = x#xs" using HI by simp
finally show "conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs"
by simp
qed

text {*
Comentario sobre la demostración anterior:
· (induct rule: coge.induct) indica que el método de demostración es
por el esquema de inducción correspondiente a la definición de la
función coge.
· Se generan 3 subobjetivos:
· 1. ⋀n. conc (coge n []) (elimina n []) = []
· 2. ⋀x xs. conc (coge 0 (x#xs)) (elimina 0 (x#xs)) = x#xs
· 3. ⋀n x xs.
conc (coge n xs) (elimina n xs) = xs ⟹
conc (coge (Suc n) (x#xs)) (elimina (Suc n) (x#xs)) = x#xs
*}

-- "La demostración automática es"
lemma "conc (coge n xs) (elimina n xs) = xs"
by (induct rule: coge.induct) auto

section {* Razonamiento por casos *}

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 18 (p. 39) . Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
assume "xs = []"
then show "esVacia xs = esVacia (conc xs xs)" by simp
next
fix y ys
assume "xs = y#ys"
then show "esVacia xs = esVacia (conc xs xs)" by simp
qed

text {*
Comentarios sobre la demostración anterior:
· "(cases xs)" es el método de demostración por casos según xs.
· Se generan dos subobjetivos correspondientes a los dos
constructores de listas:
· 1. xs = [] ⟹ esVacia xs = esVacia (conc xs xs)
· 2. ⋀y ys. xs = y#ys ⟹ esVacia xs = esVacia (conc xs xs)
· "then" indica "usando la propiedad anterior"
*}

-- "La demostración estructurada simplificada es"
lemma "esVacia xs = esVacia (conc xs xs)"
proof (cases xs)
case Nil
thus "esVacia xs = esVacia (conc xs xs)" by simp
next
case Cons
thus "esVacia xs = esVacia (conc xs xs)" by simp
qed

text {*
Comentarios sobre la demostración anterior:
· "case Nil" es una abreviatura de "assume xs = []"
· "case Cons" es una abreviatura de "fix y ys assume xs = y#ys"
· "thus" es una abreviatura de "then show".
*}

-- "La demostración automática es"
lemma "esVacia xs = esVacia (conc xs xs)"
by (cases xs) auto

section {* Heurística de generalización *}

text {*
Heurística de generalización: Cuando se use demostración estructural,
cuantificar universalmente las variables libres (o, equivalentemente,
considerar las variables libres como variables arbitrarias). *}

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 20. (p. 44) Demostrar que
inversaAcAux xs ys = (inversa xs) @ ys
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma inversaAcAux_es_inversa:
"inversaAcAux xs ys = (inversa xs) @ ys"
proof (induct xs arbitrary: ys)
show "⋀ys. inversaAcAux [] ys = inversa [] @ ys" by simp
next
fix a xs
assume HI: "⋀ys. inversaAcAux xs ys = inversa xs@ys"
show "⋀ys. inversaAcAux (a#xs) ys = inversa (a#xs)@ys"
proof -
fix ys
have "inversaAcAux (a#xs) ys = inversaAcAux xs (a#ys)" by simp
also have "… = inversa xs@(a#ys)" using HI by simp
also have "… = inversa (a#xs)@ys" by simp
finally show "inversaAcAux (a#xs) ys = inversa (a#xs)@ys" by simp
qed
qed

text {*
Comentarios sobre la demostración anterior:
· "(induct xs arbitrary: ys)" es el método de demostración por
inducción sobre xs usando ys como variable arbitraria.
· Se generan dos subobjetivos:
· 1. ⋀ys. inversaAcAux [] ys = inversa [] @ ys
· 2. ⋀a xs ys. (⋀ys. inversaAcAux xs ys = inversa xs @ ys) ⟹
inversaAcAux (a # xs) ys = inversa (a # xs) @ ys
· Dentro de una demostración se pueden incluir otras demostraciones.
· Para demostrar la propiedad universal "⋀ys. P(ys)" se elige una
lista arbitraria (con "fix ys") y se demuestra "P(ys)".
*}

-- "La demostración automática es"
lemma "inversaAcAux xs ys = (inversa xs)@ys"
by (induct xs arbitrary: ys) auto

text {* ---------------------------------------------------------------
Ejemplo 21. (p. 43) Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

-- "La demostración automática es"
corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)

text {*
Comentario de la demostración anterior:
· "(simp add: inversaAcAux_es_inversa)" es el método de demostración
por simplificación usando como regla de simplificación la propiedad
inversaAcAux_es_inversa.
*}

section {* Demostración por inducción para funciones de orden superior *}

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 24. (p. 45) Demostrar que
sum (map (λx. 2*x) xs) = 2 * (sum xs)
------------------------------------------------------------------- *}

-- "La demostración estructurada es"
lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
proof (induct xs)
show "sum (map (λx. 2*x) []) = 2 * (sum [])" by simp
next
fix a xs
assume HI: "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
have "sum (map (λx. 2*x) (a#xs)) = sum ((2*a)#(map (λx. 2*x) xs))"
by simp
also have "... = 2*a + sum (map (λx. 2*x) xs)" by simp
also have "... = 2*a + 2*(sum xs)" using HI by simp
also have "... = 2*(a + sum xs)" by simp
also have "... = 2*(sum (a#xs))" by simp
finally show "sum (map (λx. 2*x) (a#xs)) = 2*(sum (a#xs))" by simp
qed

-- "La demostración automática es"
lemma "sum (map (λx. 2*x) xs) = 2 * (sum xs)"
by (induct xs) auto

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

-- "La demostración estructurada es"
lemma "longitud (map f xs) = longitud xs"
proof (induct xs)
show "longitud (map f []) = longitud []" by simp
next
fix a xs
assume HI: "longitud (map f xs) = longitud xs"
have "longitud (map f (a#xs)) = longitud (f a # (map f xs))" by simp
also have "... = 1 + longitud (map f xs)" by simp
also have "... = 1 + longitud xs" using HI by simp
also have "... = longitud (a#xs)" by simp
finally show "longitud (map f (a#xs)) = longitud (a#xs)" by simp
qed

-- "La demostración automática es"
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>

Temas

2015-12-14T16:03:21Z

Jalonso:

== Temas de ''Razonamiento automático (2014-15)'' ==
* [[Tema 1: Programación funcional en Isabelle]].
* Tema 2: Razonamiento sobre programas:
** [http://www.cs.us.es/~jalonso/cursos/i1m-15/temas/tema-8.pdf Tema 2a: Razonamiento sobre programas Haskell]
** [[Tema 2b: Razonamiento automático sobre programas en Isabelle/HOL]].
* [[Tema 3: Razonamiento estructurado sobre programas en Isabelle/HOL]].

Discusión:Relación 1

2015-12-01T15:15:15Z

Jalonso:

He cambiado el sitio de los nombres de los autores para ponerlo delante de cada definición. También he numerado las distintas versiones de la misma función para que no den problemas al cargar la teoría. [[Usuario:Jalonso|José A. Alonso]] 10:14 30 nov 2015 (CET)

----

Discusión:Relación 1

2015-12-01T15:11:31Z

Jalonso:

R2

2015-12-01T11:55:06Z

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

<source lang="isar">
header {* R2: Razonamiento sobre programas en Isabelle/HOL *}

theory R2
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>

Relación 2

2015-12-01T11:54:51Z

Jalonso: Página creada con '<source lang="isar"> header {* R2: Razonamiento sobre programas en Isabelle/HOL *} theory R2 imports Main begin text {* ------------------------------------------------------...'

<source lang="isar">
header {* R2: Razonamiento sobre programas en Isabelle/HOL *}

theory R2
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>

R2

2015-12-01T11:54:35Z

<source lang="isar">
header {* R2: Razonamiento sobre programas en Isabelle/HOL *}

theory R2
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>

Ejercicios

2015-12-01T11:54:03Z

Jalonso: /* Relaciones de ejercicios */

== Relaciones de ejercicios ==

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/HOL. ([[R1 |Enunciado]] y [[Relación 1 | Solución colaborativa]]).
* '''Relación 2''': Razonamiento automático sobre programas en Isabelle/HOL. ([[R2 |Enunciado]] y [[Relación 2 | Solución colaborativa]]).

Tema 2b: Razonamiento automático sobre programas en Isabelle/HOL

2015-12-01T11:53:23Z

Jalonso: Página creada con '<source lang="isar"> header {* Tema 2: Razonamiento automático sobre programas en Isabelle/HOL *} theory T2_Razonamiento_sobre_programas imports Main begin text {* En est...'

<source lang="isar">
header {* Tema 2: Razonamiento automático sobre programas en Isabelle/HOL *}

theory T2_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://goo.gl/Imvyt *}

section {* Razonamiento ecuacional *}

text {* ----------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 2. Demostrar que
longitud [4,2,5] = 3
------------------------------------------------------------------- *}

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

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 4. (p.6) Demostrar que
intercambia (intercambia (x,y)) = (x,y)
------------------------------------------------------------------- *}

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

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 6. (p. 9) Demostrar que
inversa [x] = [x]
------------------------------------------------------------------- *}

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

section {* Razonamiento por inducción sobre los naturales *}

text {*
[Principio de inducción sobre los naturales] Para demostrar una
propiedad P para todos los números naturales basta probar que el 0
tiene la propiedad P y que si n tiene la propiedad P, entonces n+1
también la tiene.
⟦P 0; ⋀n. P n ⟹ P (Suc n)⟧ ⟹ P m

En Isabelle el principio de inducción sobre los naturales está
formalizado en el teorema nat.induct y puede verse con
thm nat.induct
*}

thm nat.induct

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 8. (p. 18) Demostrar que
longitud (repite n x) = n
------------------------------------------------------------------- *}

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

section {* Razonamiento por inducción sobre listas *}

text {*
Para demostrar una propiedad para todas las listas basta demostrar
que la lista vacía tiene la propiedad y que al añadir un elemento a una
lista que tiene la propiedad se obtiene otra lista que también tiene la
propiedad.

En Isabelle el principio de inducción sobre listas está formalizado
mediante el teorema list.induct que puede verse con
thm list.induct
*}

thm list.induct

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 10. (p. 24) 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 {* ---------------------------------------------------------------
Ejemplo 11. Refutar que
conc xs ys = conc ys xs
------------------------------------------------------------------- *}

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

text {* Encuentra el contraejemplo,
xs = [a⇣2]
ys = [a⇣1] *}

text {* ---------------------------------------------------------------
Ejemplo 12. (p. 28) Demostrar que
conc xs [] = xs
------------------------------------------------------------------- *}

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

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

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

section {* Inducción correspondiente a la definición recursiva *}

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 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 {*
La definición coge genera el esquema de inducción coge.induct:
⟦⋀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 {* ---------------------------------------------------------------
Ejemplo 16. (p. 35) 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

section {* Razonamiento por casos *}

text {*
Distinción de casos sobre listas:
· El método de distinción de casos se activa con (cases xs) donde xs
es del tipo lista.
· "case Nil" es una abreviatura de
"assume Nil: xs =[]".
· "case Cons" es una abreviatura de
"fix ? ?? assume Cons: xs = ? # ??"
donde ? y ?? son variables anónimas. *}

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 18 (p. 39) . Demostrar que
esVacia xs = esVacia (conc xs xs)
------------------------------------------------------------------- *}

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

section {* Heurística de generalización *}

text {*
Heurística de generalización: Cuando se use demostración estructural,
cuantificar universalmente las variables libres (o, equivalentemente,
considerar las variables libres como variables arbitrarias). *}

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 20. (p. 44) 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 {* ---------------------------------------------------------------
Ejemplo 21. (p. 43) Demostrar que
inversaAc xs = inversa xs
------------------------------------------------------------------- *}

-- "La demostración automática es"
corollary "inversaAc xs = inversa xs"
by (simp add: inversaAcAux_es_inversa)

section {* Demostración por inducción para funciones de orden superior *}

text {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 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 {* ---------------------------------------------------------------
Ejemplo 24. (p. 45) 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 {* ---------------------------------------------------------------
Ejemplo 25. (p. 48) 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". http://bit.ly/1gMqK0X
· 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". http://bit.ly/1gMqFKI
*}

end
</source>

Temas

2015-12-01T11:52:29Z

Jalonso:

== Temas de ''Razonamiento automático (2014-15)'' ==
* [[Tema 1: Programación funcional en Isabelle]].
* Tema 2: Razonamiento sobre programas:
** [http://www.cs.us.es/~jalonso/cursos/i1m-15/temas/tema-8.pdf Tema 2a: Razonamiento sobre programas Haskell]
** [[Tema 2b: Razonamiento automático sobre programas en Isabelle/HOL]].

Temas

2015-12-01T11:51:34Z

Jalonso:

== Temas de ''Razonamiento automático (2014-15)'' ==
* [[Tema 1: Programación funcional en Isabelle]].
* Tema 2: Razonamiento sobre programas:
** [http://www.cs.us.es/~jalonso/cursos/i1m-15/temas/tema-8t.pdf Tema 2a: Razonamiento sobre programas Haskell]
** [[Tema 2b: Razonamiento automático sobre programas en Isabelle/HOL]].

Relación 1

2015-12-01T11:50:15Z

Jalonso:

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

theory R1
imports Main
begin

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

-- "jospalhid angfraalv adacieizq"
fun factorial :: "nat ⇒ nat" where
"factorial 0 = 1" |
"factorial (Suc n) = Suc n * factorial n"

--"marsoldia2"
(*
fun factorial2 :: "nat ⇒ nat" where
"factorial2 0 = 1 " |
"factorial2 n = n * factorial2 (n-1)"
*)

value "factorial 4" -- "24"

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
------------------------------------------------------------------- *}

-- "jospalhid, marsoldia2"
fun longitud :: "'a list ⇒ nat" where
"longitud [] = 0" |
"longitud xs = 1 + longitud (tl xs)"

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

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

value "longitud2 [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)
------------------------------------------------------------------ *}

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

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

--"marsoldia2"
fun intercambia2 :: "'a × 'b ⇒ 'b × 'a" where
"intercambia2 (x,y) = (snd (x,y),fst (x,y))"

value "intercambia2 (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]
------------------------------------------------------------------ *}

-- "jospalhid angfraalv"
fun inversa :: "'a list ⇒ 'a list" where
-- "se pude usar rev xs para invertir la lista directamente"
"inversa [] = []" |
"inversa xs = last xs # inversa (butlast xs)"

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]
------------------------------------------------------------------ *}

-- "jospalhid angfraalv adacieizq"
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]"

-- "marsoldia2"
(*
fun repite2 :: "nat ⇒ 'a ⇒ 'a list" where
"repite2 0 x = []"|
"repite2 n x = x # (repite2 (n-1) x)"
*)

value "repite2 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]
------------------------------------------------------------------ *}

-- "jospalhid"
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] [] = []" |
"conc [] ys = ys" |
"conc xs [] = xs" |
"conc xs ys = hd xs # conc (tl xs) ys"

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

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

value "conc2 [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]
------------------------------------------------------------------ *}

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

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

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

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

-- "marsoldia2"
(*
fun coge3 :: "nat ⇒ 'a list ⇒ 'a list" where
"coge3 0 xs = []" |
"coge3 n [] = []" |
"coge3 n xs = (hd xs) # (coge3 (n-1) (tl xs))"
*)

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]
------------------------------------------------------------------ *}

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

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

-- "angfraalv"
fun elimina2 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina2 n xs = inversa (coge (((length xs) - n)::nat) (inversa xs))"

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

-- "marsoldia2"
fun elimina3 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina3 0 xs = xs"|
"elimina3 n [] = []"|
"elimina3 n xs = elimina3 ( n-1) (tl xs)"

value "elimina2 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
------------------------------------------------------------------ *}

-- "jospalhid angfraalv"
fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True" |
"esVacia xs = False"

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

-- "marsoldia2"
fun esVacia2 :: "'a list ⇒ bool" where
"esVacia2 [] = True" |
"esVacia2 [n] = False"

value "esVacia2 []" -- "= True"
value "esVacia2 [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]
------------------------------------------------------------------ *}

-- "angfraalv"
fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
-- "no se si he entendido bien la idea de acumular, pero funciona"
"inversaAcAux xs ys = conc ys xs "

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

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
------------------------------------------------------------------ *}

-- "jospalhid, marsoldia2"
fun sum :: "nat list ⇒ nat" where
"sum [] = 0" |
"sum xs = hd xs + sum (tl xs)"

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

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

value "sum2 [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::int,2,5] = [6,4,10]
------------------------------------------------------------------ *}

-- "jospalhid"
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []" |
"map f xs = f(hd xs) # map f (tl xs)"

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

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

value "map2 (λx. 2*x) [3::int,2,5]" -- "= [6,4,10]"
end
</source>

Discusión:Relación 1

2015-11-30T09:14:08Z

Jalonso:

Discusión:Relación 1

2015-11-30T09:11:46Z

Jalonso:

Discusión:Relación 1

2015-11-30T09:11:24Z

Jalonso:

Discusión:Relación 1

2015-11-30T09:10:12Z

Jalonso: Página creada con 'He cambiado el sitio de los nombres de los autores para ponerlo delante de cada definición. ~~~ ----'

He cambiado el sitio de los nombres de los autores para ponerlo delante de cada definición. [[Usuario:Jalonso|Jalonso]]

----

Relación 1

2015-11-30T09:09:02Z

Jalonso:

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

theory R1
imports Main
begin

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

-- "jospalhid angfraalv adacieizq"
fun factorial :: "nat ⇒ nat" where
"factorial 0 = 1" |
"factorial (Suc n) = Suc n * factorial n"

value "factorial 4" -- "24"

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
------------------------------------------------------------------- *}

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

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

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

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)
------------------------------------------------------------------ *}

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

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]
------------------------------------------------------------------ *}

-- "jospalhid angfraalv"
fun inversa :: "'a list ⇒ 'a list" where
-- "se pude usar rev xs para invertir la lista directamente"
"inversa [] = []" |
"inversa xs = last xs # inversa (butlast xs)"

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]
------------------------------------------------------------------ *}

-- "jospalhid angfraalv adacieizq"
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 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]
------------------------------------------------------------------ *}

-- "jospalhid"
fun conc :: "'a list ⇒ 'a list ⇒ 'a list" where
"conc [] [] = []" |
"conc [] ys = ys" |
"conc xs [] = xs" |
"conc xs ys = hd xs # conc (tl xs) ys"

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

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

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]
------------------------------------------------------------------ *}

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

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

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

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]
------------------------------------------------------------------ *}

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

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

-- "angfraalv"
fun elimina2 :: "nat ⇒ 'a list ⇒ 'a list" where
"elimina2 n xs = inversa (coge (((length xs) - n)::nat) (inversa xs))"

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
------------------------------------------------------------------ *}

-- "jospalhid angfraalv"
fun esVacia :: "'a list ⇒ bool" where
"esVacia [] = True" |
"esVacia xs = False"

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]
------------------------------------------------------------------ *}

-- "angfraalv"
fun inversaAcAux :: "'a list ⇒ 'a list ⇒ 'a list" where
-- "no se si he entendido bien la idea de acumular, pero funciona"
"inversaAcAux xs ys = conc ys xs "

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

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
------------------------------------------------------------------ *}

-- "jospalhid"
fun sum :: "nat list ⇒ nat" where
"sum [] = 0" |
"sum xs = hd xs + sum (tl xs)"

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

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

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]
------------------------------------------------------------------ *}

-- "jospalhid"
fun map :: "('a ⇒ 'b) ⇒ 'a list ⇒ 'b list" where
"map f [] = []" |
"map f xs = f(hd xs) # map f (tl xs)"

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

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

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