# HG changeset patch # User paulson # Date 1385395209 0 # Node ID 3936fb5803d683b31e229e81289f0318225ebf07 # Parent cb17feba74e0ab23731832fde2d8aa8848f5a86f tweaks to the documentation diff -r cb17feba74e0 -r 3936fb5803d6 src/Doc/Tutorial/document/rules.tex --- a/src/Doc/Tutorial/document/rules.tex Mon Nov 25 14:50:31 2013 +0000 +++ b/src/Doc/Tutorial/document/rules.tex Mon Nov 25 16:00:09 2013 +0000 @@ -1,4 +1,4 @@ -%!TEX root = ../tutorial.tex +%!TEX root = root.tex \chapter{The Rules of the Game} \label{chap:rules} @@ -33,6 +33,8 @@ one symbol only. For predicate logic this can be done, but when users define their own concepts they typically have to refer to other symbols as well. It is best not to be dogmatic. +Our system is not based on pure natural deduction, but includes elements from the sequent calculus +and free-variable tableaux. Natural deduction generally deserves its name. It is easy to use. Each proof step consists of identifying the outermost symbol of a formula and @@ -240,13 +242,14 @@ of a conjunction. Rules of this sort (where the conclusion is a subformula of a premise) are called \textbf{destruction} rules because they take apart and destroy a premise.% -\footnote{This Isabelle terminology has no counterpart in standard logic texts, +\footnote{This Isabelle terminology is not used in standard logic texts, although the distinction between the two forms of elimination rule is well known. Girard \cite[page 74]{girard89},\index{Girard, Jean-Yves|fnote} for example, writes ``The elimination rules [for $\disj$ and $\exists$] are very bad. What is catastrophic about them is the parasitic presence of a formula [$R$] -which has no structural link with the formula which is eliminated.''} +which has no structural link with the formula which is eliminated.'' +These Isabelle rules are inspired by the sequent calculus.} The first proof step applies conjunction introduction, leaving two subgoals: diff -r cb17feba74e0 -r 3936fb5803d6 src/Doc/manual.bib --- a/src/Doc/manual.bib Mon Nov 25 14:50:31 2013 +0000 +++ b/src/Doc/manual.bib Mon Nov 25 16:00:09 2013 +0000 @@ -194,7 +194,7 @@ @incollection{basin91, author = {David Basin and Matt Kaufmann}, title = {The {Boyer-Moore} Prover and {Nuprl}: An Experimental - Comparison}, + Comparison}, crossref = {huet-plotkin91}, pages = {89-119}} @@ -472,7 +472,7 @@ @book{constable86, author = {R. L. Constable and others}, title = {Implementing Mathematics with the Nuprl Proof - Development System}, + Development System}, publisher = Prentice, year = 1986} @@ -505,7 +505,7 @@ @incollection{dybjer91, author = {Peter Dybjer}, title = {Inductive Sets and Families in {Martin-L{\"o}f's} Type - Theory and Their Set-Theoretic Semantics}, + Theory and Their Set-Theoretic Semantics}, crossref = {huet-plotkin91}, pages = {280-306}} @@ -533,7 +533,7 @@ @InProceedings{felty91a, Author = {Amy Felty}, Title = {A Logic Program for Transforming Sequent Proofs to Natural - Deduction Proofs}, + Deduction Proofs}, crossref = {extensions91}, pages = {157-178}} @@ -566,9 +566,9 @@ @inproceedings{OBJ, author = {K. Futatsugi and J.A. Goguen and Jean-Pierre Jouannaud - and J. Meseguer}, + and J. Meseguer}, title = {Principles of {OBJ2}}, - booktitle = POPL, + booktitle = POPL, year = 1985, pages = {52-66}} @@ -576,7 +576,7 @@ @book{gallier86, author = {J. H. Gallier}, - title = {Logic for Computer Science: + title = {Logic for Computer Science: Foundations of Automatic Theorem Proving}, year = 1986, publisher = {Harper \& Row}} @@ -605,8 +605,8 @@ author = {Jean-Yves Girard}, title = {Proofs and Types}, year = 1989, - publisher = CUP, - note = {Translated by Yves LaFont and Paul Taylor}} + publisher = CUP, + note = {Translated by Yves Lafont and Paul Taylor}} @Book{mgordon-hol, editor = {M. J. C. Gordon and T. F. Melham}, @@ -777,21 +777,21 @@ @article{huet78, author = {G. P. Huet and B. Lang}, - title = {Proving and Applying Program Transformations Expressed with + title = {Proving and Applying Program Transformations Expressed with Second-Order Patterns}, journal = acta, volume = 11, - year = 1978, + year = 1978, pages = {31-55}} @inproceedings{huet88, author = {G{\'e}rard Huet}, title = {Induction Principles Formalized in the {Calculus of - Constructions}}, + Constructions}}, booktitle = {Programming of Future Generation Computers}, editor = {K. Fuchi and M. Nivat}, year = 1988, - pages = {205-216}, + pages = {205-216}, publisher = {Elsevier}} @inproceedings{Huffman-Kuncar:2013:lifting_transfer, @@ -843,7 +843,7 @@ %K @InProceedings{kammueller-locales, - author = {Florian Kamm{\"u}ller and Markus Wenzel and + author = {Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson}, title = {Locales: A Sectioning Concept for {Isabelle}}, crossref = {tphols99}} @@ -944,7 +944,7 @@ author = {Gavin Lowe}, title = {Breaking and Fixing the {Needham}-{Schroeder} Public-Key Protocol using {CSP} and {FDR}}, - booktitle = {Tools and Algorithms for the Construction and Analysis + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems: second international workshop, TACAS '96}, editor = {T. Margaria and B. Steffen}, series = {LNCS 1055}, @@ -978,7 +978,7 @@ @incollection{melham89, author = {Thomas F. Melham}, title = {Automating Recursive Type Definitions in Higher Order - Logic}, + Logic}, pages = {341-386}, crossref = {birtwistle89}} @@ -1057,7 +1057,7 @@ @InProceedings{NaraschewskiW-TPHOLs98, author = {Wolfgang Naraschewski and Markus Wenzel}, - title = + title = {Object-Oriented Verification based on Record Subtyping in Higher-Order Logic}, crossref = {tphols98}} @@ -1190,8 +1190,8 @@ @book{nordstrom90, author = {Bengt {Nordstr{\"o}m} and Kent Petersson and Jan Smith}, title = {Programming in {Martin-L{\"o}f}'s Type Theory. An - Introduction}, - publisher = {Oxford University Press}, + Introduction}, + publisher = {Oxford University Press}, year = 1990} %O @@ -1251,7 +1251,7 @@ @InProceedings{paulson-COLOG, author = {Lawrence C. Paulson}, title = {A Formulation of the Simple Theory of Types (for - {Isabelle})}, + {Isabelle})}, pages = {246-274}, crossref = {colog88}, url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}} @@ -1304,7 +1304,7 @@ %replaces paulson-final @Article{paulson-mscs, author = {Lawrence C. Paulson}, - title = {Final Coalgebras as Greatest Fixed Points + title = {Final Coalgebras as Greatest Fixed Points in {ZF} Set Theory}, journal = {Mathematical Structures in Computer Science}, year = 1999, @@ -1337,9 +1337,9 @@ crossref = {milner-fest}} @book{milner-fest, - title = {Proof, Language, and Interaction: + title = {Proof, Language, and Interaction: Essays in Honor of {Robin Milner}}, - booktitle = {Proof, Language, and Interaction: + booktitle = {Proof, Language, and Interaction: Essays in Honor of {Robin Milner}}, publisher = MIT, year = 2000, @@ -1427,7 +1427,7 @@ @book{paulson87, author = {Lawrence C. Paulson}, title = {Logic and Computation: Interactive proof with Cambridge - LCF}, + LCF}, year = 1987, publisher = CUP} @@ -1470,7 +1470,7 @@ @article{pelletier86, author = {F. J. Pelletier}, title = {Seventy-five Problems for Testing Automatic Theorem - Provers}, + Provers}, journal = JAR, volume = 2, pages = {191-216}, @@ -1486,13 +1486,13 @@ publisher = CUP, year = 1993} -@Article{pitts94, +@Article{pitts94, author = {Andrew M. Pitts}, title = {A Co-induction Principle for Recursively Defined Domains}, journal = TCS, - volume = 124, + volume = 124, pages = {195-219}, - year = 1994} + year = 1994} @Article{plaisted90, author = {David A. Plaisted}, @@ -1561,7 +1561,7 @@ @inproceedings{saaltink-fme, author = {Mark Saaltink and Sentot Kromodimoeljo and Bill Pase and Dan Craigen and Irwin Meisels}, - title = {An {EVES} Data Abstraction Example}, + title = {An {EVES} Data Abstraction Example}, pages = {578-596}, crossref = {fme93}} @@ -1897,7 +1897,7 @@ author = {A. N. Whitehead and B. Russell}, title = {Principia Mathematica}, year = 1962, - publisher = CUP, + publisher = CUP, note = {Paperback edition to *56, abridged from the 2nd edition (1927)}} @@ -1982,9 +1982,9 @@ @book{birtwistle89, editor = {Graham Birtwistle and P. A. Subrahmanyam}, title = {Current Trends in Hardware Verification and Automated - Theorem Proving}, + Theorem Proving}, booktitle = {Current Trends in Hardware Verification and Automated - Theorem Proving}, + Theorem Proving}, publisher = {Springer}, year = 1989} @@ -1997,9 +1997,9 @@ @Proceedings{cade12, editor = {Alan Bundy}, - title = {Automated Deduction --- {CADE}-12 + title = {Automated Deduction --- {CADE}-12 International Conference}, - booktitle = {Automated Deduction --- {CADE}-12 + booktitle = {Automated Deduction --- {CADE}-12 International Conference}, year = 1994, series = {LNAI 814}, @@ -2059,7 +2059,7 @@ title = {Extensions of Logic Programming}, booktitle = {Extensions of Logic Programming}, year = 1991, - series = {LNAI 475}, + series = {LNAI 475}, publisher = {Springer}} @proceedings{cade10, @@ -2078,9 +2078,9 @@ year = 1993} @book{wos-fest, - title = {Automated Reasoning and its Applications: + title = {Automated Reasoning and its Applications: Essays in Honor of {Larry Wos}}, - booktitle = {Automated Reasoning and its Applications: + booktitle = {Automated Reasoning and its Applications: Essays in Honor of {Larry Wos}}, publisher = MIT, year = 1997,