# HG changeset patch
# User haftmann
# Date 1118060067 -7200
# Node ID 322e2a3335d4c43e2e0f44d2892ab8bbbde6b15f
# Parent f9f2e16435936157b39f7d87652d349991d8520b
(cvs removed)
diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/Contents
--- a/Admin/page/Contents Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-Learning Isabelle
- tutorial Tutorial on Isabelle/HOL
- isar-overview Tutorial on Isar
- locales Tutorial on Locales
-
-Reference Manuals
- isar-ref The Isabelle/Isar Reference Manual
- ref The Isabelle Reference Manual
- system The Isabelle System Manual
-
-Logics
- logics Isabelle's Logics: overview and misc logics
- logics-HOL Isabelle's Logics: HOL
- logics-ZF Isabelle's Logics: FOL and ZF
-
-Specific Topics
- axclass Tutorial on Axiomatic Type Classes
- ind-defs (Co)Inductive Definitions in ZF
diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/DISTNAME
--- a/Admin/page/DISTNAME Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Isabelle2004
diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/HOWTO
--- a/Admin/page/HOWTO Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-This file describes how to change and regenerate the Isabelle web pages.
-See the bottom of the file for a short overview of the setup.
-
-== Changes to main ==
-
-To make changes to the content of the main pages:
-
- * Edit or add the appropriate Admin/page/main-content/*.content files
- * Run "make clean main" in Admin/page/
- * Check generated html in Admin/page/main/
- * Check changes in main-content into cvs
- * Run "make pub-main" to publish to the Munich web site
- * Run "mirror-main" in Cambridge to synchronize
-
-
-== Changes to dist ==
-
-These should be rare and are a bit more involved at the moment. The
-principle is the same as for the main pages, but the script needs
-access to the distribution files to calculate sizes etc:
-
- * Edit or add the appropriate Admin/page/dist-content/*.content files
- * Make sure the Isabelle package files are available in directory Admin/page.
- On sunbroy2, the following does the trick (in directory Admin/page):
-
- ln -s /home/html/isabelle/html-data/dist/contrib
- for f in /home/html/isabelle/html-data/dist/*.tar.gz; do ln -s $f; done
-
- * Run "make clean dist" in Admin/page/
- * Check generated html in Admin/page/dist/
- * Check changes in dist-content into cvs
- * Run "make pub-dist" to publish to the Munich web site
- (will only copy *.html files, will not update other distribution files)
- * Run "mirror-dist" in Cambridge and notify other mirrors to synchronize
-
-
-== Overview ==
-
-The pages are separated into two sets:
- * main, for the main home page in Munich and Cambridge, and
- * dist, for the current Isabelle distribution more widely mirrored.
-
-Both are generated by a script (genpage) that takes *.content files and
-puts them into a common template.
-
-This is supposed to achieve the following:
- * separation of layout and content
- * automatic consistency between contents of distribution and web
- page, including name of the distribution, file sizes of download
- packages, and documentation generated from isabelle/Doc
-
-For this the web page generation script needs access to the following
-support files:
-
-Admin/page/DISTNAME (name of the distribution, e.g. Isabelle2004)
-Admin/page/Contents (same as Distribution/doc/Contents at the time
- of the Isabelle release)
-
-Both files are set to the right values automatically by makedist when
-the Isabelle distribution is generated and maintained manually in
-between releases by the release manager in Admin/page in CVS. (In
-between releases Admin/page/Contents can be different from
-Distribution/doc/Contents)
diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/Makefile
--- a/Admin/page/Makefile Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-# -- makefile for Isabelle web pages (dist and main)
-# -- $Id$
-
-# --- force shell
-SHELL=bash
-
-# --- check parameters
-ifeq ($(tidy),)
- TIDYCMD=:
-else
- TIDYCMD=tidy -q -i -asxhtml --doctype auto --indent-spaces 2 --wrap 80 \
- --logical-emphasis yes --gnu-emacs yes --write-back yes
-endif
-
-# --- external tools
-
-GENPAGE = ./bin/genpage
-MKCONTENT = ./bin/mkcontents
-
-# ---
-# --- genpage stuff
-
-# --- directories for main isabelle pages
-
-MAIN_CONTENT = main-content
-MAIN_LAYOUT = main-layout
-MAIN_TARGET = main
-
-# --- directories for isabelle distribution pages
-
-DIST_CONTENT = dist-content
-DIST_LAYOUT = dist-layout
-DIST_TARGET = dist
-
-# --- name of genpage template file
-TEMPLATE_NAME = template.html
-
-# ---
-# --- doc content generation
-
-# --- location of the Contents file of the Isabelle documentation
-DOC_CONTENT_FILE = Contents
-
-# --- target include files with documentation links
-DOC_CONTENTS_MAIN = docu-contents.main
-DOC_CONTENTS_DIST = docu-contents.dist
-
-# --- target directories for publishing to web site
-MAIN_PUB_MIRROR_SRC=sunbroy2.informatik.tu-muenchen.de:/home/proj/isabelle-repository/www/
-MAIN_PUB_DEST=sunbroy2.informatik.tu-muenchen.de:/home/html/isabelle/html-data/
-DIST_PUB_DEST=sunbroy2.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/
-
-# ---
-# --- begin rules
-
-all: clean main dist install weblint
-
-main:
- @$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)
- @env DISTNAME=`cat DISTNAME` \
- $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
- -@cd $(MAIN_TARGET); \
- for html in *.html; \
- do $(TIDYCMD) $$html; \
- done
-
-pub-main: main
- @echo "Publishing main pages (*.html only)."
- scp main/*.html $(MAIN_PUB_MIRROR_SRC)
- scp main/*.html $(MAIN_PUB_DEST)
-
-dist:
- @$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
- @env DISTNAME=`cat DISTNAME` \
- $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
- -@cd $(MAIN_TARGET); \
- for html in *.html; \
- do $(TIDYCMD) $$html; \
- done
-
-pub-dist: dist
- @echo "Publishing dist pages (*.html only)."
- scp dist/*.html $(DIST_PUB_DEST)
-
-install: main dist
- @cp -R dist/. ..
- @mkdir -p ../../main-`cat DISTNAME`/.
- @cp -R main/. ../../main-`cat DISTNAME`/.
-
-weblint:
- -weblint -x netscape -d extension-attribute -e img-size $(MAIN_TARGET)
- -weblint -x netscape -d extension-attribute -e img-size $(DIST_TARGET)
-
-clean:
- @rm -rf $(MAIN_TARGET)
- @rm -rf $(DIST_TARGET)
- @rm -rf $(DOC_CONTENTS_MAIN)
- @rm -rf $(DOC_CONTENTS_DIST)
- @find . -name "*~" -type f -print | xargs rm -f
diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/bin/genpage
--- a/Admin/page/bin/genpage Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,420 +0,0 @@
-#!/usr/bin/perl -w
-
-# Genpage - Webpage Generator.
-#
-# Copyright (C) Joe Vaughan
Thanks to -Norbert Vöker -and Viorel Preoteasa -whose efforts helped a lot to get Isabelle run this way.
- -Cygwin is a POSIX emulation layer for Windows; it contains ports of a large -collection of common Unix software (shells, perl, gcc, X11, latex, ImageMagick, -…).
- -To install it, get the installer from the -Cygwin website and run it. It will ask you -which packages to install, and then downloads and installs them. -Please make sure you install everything needed by Isabelle; it is hard to give -a concise list of packages here since the bundling of Cygwin packages may vary -over time, but installing the base packages, perl, make, xemacs and x-server -should be a good choice for the beginning.
- -By default, cygwin installs to c:\cygwin; you may choose an arbitrary -location, but it is recommended that it does not include any space or exotic -characters. This directory will then become the root directory of the Cygwin -filesystem tree, i.e. the Cygwin path /opt/smlnj -will be mapped to Windows path c:\cygwin\opt\smlnj.
- -After installation, open a Cygwin shell window (normally the installer -makes a shortcut for you).
- -Now we are ready to get and build SML/NJ; -before this, set the environment variable SMLNJ_CYGWIN_RUNTIME to 1: - -
- - export SMLNJ_CYGWIN_RUNTIME=1 - -- -
- (or - - setenv SMLNJ_CYGWIN_RUNTIME 1 - - for c shells). -- -This setting will tell the build process that it should not attempt -to build SML/NJ natively for Win32 but for Cygwin instead (see further -CYGWININSTALL). - -
So far, this setup was tested using the working version 110.53 -of SML/NJ from http://smlnj.cs.uchicago.edu/dist/working/110.53/. -SML/NJ provides a nice installer enabling you to download and build it. -Read INSTALL -to learn about the different possibilites to do this. The default packages -should be sufficient.
- -In the following, it is assumed that you install SML/NJ to Cygwin path /opt/smlnj; -if you choose an other -location, some tweaking in the etc/settings file -may be neccessary later.
- -Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable -must be set to 1 (later on a convenient mechanism to make this the default -is proposed).
- -Download the latest Isabelle and ProofGeneral release packages. -Assuming that you are in the directory where -you downloaded the files, install them into /opt by typing into the -bash shell: - -
- - tar -C /usr/opt -xvzf- -During extraction, one inconvenience may occur, see below. - -
- tar -C /usr/opt -xvzf
- -
The location /opt again is just a proposal; if you choose other -locations, some tweaking in the etc/settings file -may be neccessary later.
- -Edit the file /opt/Isabelle/etc/settings; first, uncomment the lines -about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order the -cygwin version of SMLNJ is used. As mentioned above, the path variables for -the ML system and ProofGeneral may need adjustions, depending on your different -installation locations.
- -Take heed of the setting of ISABELLE_HOME_USER; by default, this is -~/isabelle. To detect which Windows path this will be mapped to, -type into the Cygwin bash shell: - -
- - cygpath --windows ~/isabelle - -- -If you don't like this location to be the isabelle home directory, consider -setting of ISABELLE_HOME_USER to another value; use cygpath --unix -<winpath> to detect which Cygwin path a given Windows path is mapped to. - -
A typical change could look like this: - -
- from- -
- - # Standard ML of New Jersey 110 or later
- #ML_SYSTEM=smlnj-110
- #ML_HOME="$ISABELLE_HOME/../smlnj/bin"
- #ML_OPTIONS="@SMLdebug=/dev/null"
- #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
- -
- to- - - -
- - # Standard ML of New Jersey 110 or later
- SMLNJ_CYGWIN_RUNTIME=1
- ML_SYSTEM=smlnj-110
- ML_HOME="$ISABELLE_HOME/../smlnj/bin"
- ML_OPTIONS="@SMLdebug=/dev/null"
- ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX") - -
Now we can compile some logics. Start the cygwin shell (if not still -running) and type: - -
- - cd /opt/Isabelle- - -
- build HOL
- build ZF - -
The compilation process may take some time (depending on -how fast the computer is). Before building a logic image the build -program shows some variables and expects user input – just hit enter. - -
On Linux, Isabelle can be started by two scripts located in Isabelle/bin: -Isabelle and isabelle. Isabelle attempts to start -ProofGeneral with XEmacs, and isabelle starts it in an SML shell session. -However Windows treats the two names as one. To get around this just copy -/opt/Isabelle/bin/isabelle to /opt/Isabelle/bin/Isabell. -The script /opt/Isabelle/bin/Isabell will start Isabelle with ProofGeneral.
- -Now everything should be ready. To test, start the cygwin shell and type - -
- startx & -- -This will start the cygwin X server and an X shell window. In the X shell window, -type - -
- /opt/Isabelle/bin/Isabell &. -- -This will start the ProofGeneral interface for Isabelle. After a while -an empty buffer Scratch.thy is created. You can turn on -X-Symbol from the menu Proof-General &rarrow; Options. - -
Load one of your favorite theories and test your Isabelle installation -by proving something.
- -To simplify starting ProofGeneral, consider writing a Windows command script, -e.g. - -
- @bash startx -geometry 30x4 -iconic -e Isabell -- -and assigning a shortcut in the start menu to it. - -
With the current Isabelle release (Isabelle 2004), there are two inconveniencies: -
- - AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -) - -- - with - -
- - AUTHOR="default author name" - -- -
To get around these inconveniencies, consider using a recent developer snapshot -of Isabelle; both will be fixed in the next Isabelle release.
- -As indicated above, Isabelle does not run -neatly with Poly/ML on Windows, for two -reasons: -
If you know how to circumvent (fully or partially) any of these problems, -please let us know.
- diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/dist-content/packages.content --- a/Admin/page/dist-content/packages.content Mon Jun 06 14:12:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,141 +0,0 @@ -%title% -Isabelle Packages - -%body% - -- -The following source and binary packages of -provide everything required for easy installation of the full Isabelle -working environment on common Unix platforms (e.g. Linux, Darwin, Solaris) - -
- -A minimal Isabelle installation requires only bash -and perl (usually provided by the operating system), and a -suitable implementation of Standard ML (e.g. Poly/ML as included below). A -comfortable Isabelle working environment demands further user -interface support, as provided by Proof General (please register). The Proof General -distribution now includes the X-Symbol package. It -should be used with a recent version of XEmacs 21 or GNU Emacs 21 (with -Mule enabled). - -
- - -
-While XEmacs 21 is not included here, most operating system -distributions already provide a suitable package, although not -installed by default. Some of the packages below are platform -dependent; we include binaries for Linux/x86, Solaris/Sparc, and -Darwin/PPC (MacOS X). -
-Short installation instructions are near the -bottom of this page. For more information, see the file INSTALL in -.tar.gz. - -
- - -
- -
- -A typical Linux/x86 site installation of Isabelle/HOL works as -follows. By using GNU tar, the archives are uncompressed and -unpacked into the /usr/local directory (this location may be -changed to anything appropriate). - -
-
-
- tar -C /usr/local -xzf
-
- tar -C /usr/local -xzf
-
- tar -C /usr/local -xzf
-
- tar -C /usr/local -xzf
-
- tar -C /usr/local -xzf
-
-
-
-
- -Users may now invoke Isabelle without further ado, e.g. run the main -executable /usr/local/Isabelle/bin/Isabelle to launch the -Proof General interface for Isabelle/Isar. Note that there is a -separate option in the Proof General Options menu to enable -X-Symbol. - -
- -If Emacs appears to hang when the prover process is started, see the -Proof General FAQ -for advice. - -
Although Isabelle is natively designed for Unix environments -(e.g. Solaris, Linux), it may also run under similar, Unix-like -platforms. The following installation instructions are hints -contributed by Isabelle users. Feel free to contact us for any -suggestions, corrections or improvements.
- - - diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/dist-content/past.content --- a/Admin/page/dist-content/past.content Mon Jun 06 14:12:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -%title% -Isabelle Past Releases - -%body% -- -Past releases of Isabelle are available from the Cambridge archive: - -
-
- |
-
-
-
-
- -
|
- |||
-
|
-
What is Isabelle? | -
Isabelle is a popular generic theorem proving - environment developed at Cambridge University (Larry Paulson) - and TU Munich (Tobias - Nipkow). See the Isabelle homepage for - more information. |
Where can I find documentation? | -
This - way, please. Also have a look at the theory - library. |
Is it available for download? | -
Yes, it is - available from several mirror - sites. It should run on most recent Unix systems (Solaris, - Linux, MacOS X, etc.). |
There are lots of arrows in Isabelle. What's the - difference between ->, =>, -->, - and ==> ? | -
Isabelle uses the => arrow for the function
- type (contrary to most functional languages which use
- ->). So a => b is the type of a function
- that takes an element of a as input and gives you an
- element of b as output. The long arrow -->
- and ==> are object and meta level
- implication. Roughly speaking, the meta level implication
- should only be used when stating theorems where it separates
- the assumptions from the conclusion. Whenever you need an
- implication inside a HOL formula, use --> .
- |
Where do I have to put those double quotes? |
Isabelle distinguishes between inner - and outer syntax. The outer syntax comes from the - Isabelle framework, the inner syntax is the one in between - quotation marks and comes from the object logic (in this case HOL). - With time the distinction between the two becomes obvious, but in - the beginning the following rules of thumb may work: types should - be inside quotation marks, formulas and lemmas should be inside - quotation marks, rules and equations (e.g. for definitions) should - be inside quotation marks, commands like lemma, - consts, primrec, constdefs, - apply, done are without quotation marks, as are - the names of constants in constant definitions (consts - and constdefs) - |
What is "No such - constant: _case_syntax" supposed to tell - me? |
You get this message if - you use a case construct on a datatype and have a typo in the - names of the constructor patterns or if the order of the - constructors in the case pattern is different from the order in - which they where defined (in the datatype definition). - |
Why doesn't Isabelle understand my - equation? |
Isabelle's equality = binds - relatively strongly, so an equation like a = b & c might - not be what you intend. Isabelle parses it as (a = b) & - c. If you want it the other way around, you must set - explicit parentheses as in a = (b & c). This also applies - to e.g. primrec definitions (see below). |
What does it mean "not a proper - equation"? |
Most commonly this is an instance of the - question above. The primrec command (and others) expect - equations as input, and since equality binds strongly in Isabelle, - something like f x = b & c is not what you might expect - it to be: Isabelle parses it as (f x = b) & c (which is - indeed not a proper equation). To turn it into an equation you - must set explicit parentheses: f x = (b & c). |
What does it mean - "Not a meta-equality (==)"? |
This usually occurs if - you use = for constdefs. The constdefs - and defs commands expect not equations, but meta - equivalences. Just use the \<equiv> or == - signs instead of =. |
What does "empty result sequence" - mean? |
It means that the applied proof method (or - tactic) was unsuccessful. It did not transform the goal in any - way, or simply just failed to do anything. You must try another - tactic (or give the one you used more hints or lemmas to work - with) |
The Simplifier doesn't want to apply my - rule, what's wrong? |
- Most commonly this is a typing problem. The rule you want to apply - may require a more special (or just plain different) type from - what you have in the current goal. Use the ProofGeneral menu - Isabelle/Isar -> Settings -> Show Types and the - thm command on the rule you want to apply to find out if - the types are what you expect them to be (also take a look at the - types in your goal). Show Sorts, Show Constants, - and Trace Simplifier in the same menu may also be - helpful. - |
If I do auto, it leaves me a goal - False. Is my theorem wrong? |
Not necessarily. It just means that - auto transformed the goal into something that is not - provable any more. That could be due to auto doing - something stupid, or e.g. due to some earlier step in the proof - that lost important information. It is of course also possible - that the goal was never provable in the first place. |
Why does lemma - "1+1=2" fail? |
Because it is not - necessarily true. Isabelle does not assume that 1 and 2 are - natural numbers. Try "(1::nat)+1=2" - instead. |
Can Isabelle find - counterexamples? |
-
- For arithmetic goals, - Otherwise, negate the proposition - and instantiate (some) variables with concrete values. You may - also need additional assumptions about these values. For example, - True & False ~= True | False is a counterexample of A - & B = A | B, and A = ~B ==> A & B ~= A | B is - another one. Sometimes Isabelle can help you to find the - counterexample: just negate the proposition and do auto - or simp. If lucky, you are left with the assumptions you - need for the counterexample to work. - - |
ProofGeneral appears to hang when Isabelle is started. |
X-Symbol doesn't seem to work. What can I - do? |
The most common reason why X-Symbol doesn't - work is: it's not switched on yet. Assuming you are using - ProofGeneral and have installed the X-Symbol package, you still - need to turn X-Symbol on in ProofGeneral: select the menu items - Proof-General -> Options -> X-Symbol and (if you want to - save the setting for future sessions) select Options -> Save - Options in XEmacs. |
How do I input those X-Symbols anyway? |
- There are lots of ways to input x-symbols. The one that always
- works is writing it out in plain text (e.g. for the 'and' symbol
- type \<and>). For common symbols you can try to "paint
- them in ASCII" and if the xsymbol package recognizes them it will
- automatically convert them into their graphical
- representation. Examples: --> is converted into the long
- single arrow, /\ is converted into the 'and' symbol, the
- sequence =_ into the equivalence sign, <_ into
- less-or-equal, [| into opening semantic brackets, and so
- on. For greek characters, the rotate command works well:
- to input α type a and then C-.
- (control and . ). You can also display the
- grid-of-characters in the x-symbol menu to get an overview of the
- available graphical representations (not all of them already have
- a meaning in Isabelle, though).
- |
I want to generate one of those flashy LaTeX - documents. How? |
You will need to work with the - isatool command for this (in a Unix shell). The easiest - way to get to a document is the following: use isatool - mkdir to set up a new directory. The command will also create - a file called IsaMakefile in the current directory. Put - your theory file(s) into the new directory and edit the file - ROOT.ML in there (following the comments) to tell - Isabelle which of the theories to load (and in which order). Go - back to the parent directory (where the IsaMakefile is) - and type isatool make. Isabelle should then process your - theories and tell you where to find the finished document. For - more information on generating documents see the Isabelle Tutorial, Chapter 4. - |
I have a large formalization with many - theories. Must I process all of them all of the time? |
No, you can tell Isabelle to build a so-called - heap image. This heap image can contain your preloaded - theories. To get one, set up a directory with a ROOT.ML - file (as for generating a document) and use the command - isatool usedir -b HOL MyImage in that directory to create - an image MyImage using the parent logic HOL. - You should then be able to invoke Isabelle with Isabelle -l - MyImage and have everything that is loaded in ROOT.ML - instantly available. |
Does Isabelle run on Windows? |
After a fashion, yes, - but Isabelle is not being developed for Windows. A friendly user - (Norbert Völker) has managed to get a minimal Isabelle environment - to work on it. See the description on his - website. Be warned, though: emphasis is on minimal, - working with Windows is no fun at all. To enjoy Isabelle in its - full beauty it is recommended to get a Linux distribution (they - are inexpensive, any reasonably recent one should work, dualboot - Windows/Linux should pose no problems). - |
- -
- -These pages provide general information on Isabelle, more specific -information is available from the local pages - -
- -
We will collect theorems -sent to isabelle-lemmas@cl.cam.ac.uk. -Accepted material will be included in the Isabelle sources, with -credit given to the author. Note that the Isabelle sources are -distributed under the BSD license. Lemmas should be general, useful, -and not too large. For larger developments you might want to consider -a submission to the Archive of Formal -Proofs. - - -
- -
- -
-New features in include -ring
for non-commutative rings in HOL-Algebra.rat
of the rational numbers available in HOL-Complex.specification
command for definition by specification.finalconsts
prevents constants being given a definition later.arith
now generates counterexamples for reals as well.quickcheck
command
- to search for counterexamples of executable goals.
- (see HOL/ex/Quickcheck_Examples.thy)refute
command
- to search for finite countermodels of goals.
- (see HOL/ex/Refute_Examples.thy)
--The distribution is available -from several mirror sites. It includes -source and binary packages and browsable documentation. You can also -browse the Isabelle theory library -online. For the curious, there is a nightly generated development snapshot -available. - -
- -
- -Isabelle/HOL is currently the best developed object logic, including -an extensive library of (concrete) mathematics, and various packages -for advanced definitional concepts (like (co-)inductive sets and -types, well-founded recursion etc.). The distribution also includes -some large applications, for example correctness proofs of -cryptographic protocols (HOL/Auth) or communication -protocols (HOLCF/IOA). - -
- -Isabelle/ZF provides another starting point for applications, with a -slightly less developed library. Its definitional packages are -similar to those of Isabelle/HOL. Untyped ZF provides more advanced -constructions for sets than simply-typed HOL. - -
- -There are a few minor object logics that may serve as further -examples: CTT is an extensional -version of Martin-Löf's Type Theory, Cube is Barendregt's Lambda Cube. -There are also some sequent calculus examples under Sequents, including modal and -linear logics. Again see the Isabelle -theory library for other examples. - - -
-Isabelle is a generic proof -assistant. It allows mathematical formulas to be expressed in a formal -language and provides tools for proving those formulas in a logical -calculus. The main application is the formalization of mathematical proofs -and in particular formal verification, which includes proving the -correctness of computer hardware or software and proving properties of -computer languages and protocols. -
- -Compared with similar tools, Isabelle's distinguishing feature is -its flexibility. Most proof assistants are built around a single -formal calculus, typically higher-order logic. Isabelle has the -capacity to accept a variety of formal calculi. The distributed -version supports higher-order logic but also axiomatic set theory and -several other formalisms. Isabelle provides -excellent notational support: new notations can be introduced, using -normal mathematical symbols. Proofs can be written in a structured -notation based upon traditional proof style, or more straightforwardly -as sequences of commands. Definitions and proofs may include TeX -source, from which Isabelle can automatically generate typeset -documents.
- -The main limitation of all such systems is that proving theorems -requires much effort from an expert user. Isabelle incorporates some -tools to improve the user's productivity by automating some parts of -the proof process. In particular, Isabelle's classical -reasoner can perform long chains of reasoning steps to prove -formulas. The simplifier can reason with and about equations. -Linear arithmetic facts are proved automatically. Isabelle is -closely integrated with the Proof -General user interface, which eases the task of writing and -maintaining proof scripts.
- -A hyperlinked preview demonstrating Isabelle and Proof -General is provided in -QuickTime format, -and also as a non-hyperlinked PDF file. - -Isabelle comes with large theories of formally verified -mathematics, including elementary number theory (for example, Gauss's -law of quadratic reciprocity), analysis (basic properties of limits, -derivatives and integrals), algebra (up to Sylow's theorem) and set -theory (the relative consistency of the Axiom of Choice). Also -provided are numerous examples arising from research into formal -verification. Isabelle is distributed free of -charge to academic users.
- -Ample documentation is available, -including a Tutorial published -by Springer-Verlag. Several papers -on the design of Isabelle are available. There is also a list of past -and present projects -undertaken using Isabelle.
- -Isabelle is a joint project between Lawrence C. Paulson -(University of Cambridge, UK) and Tobias Nipkow (Technical -University of Munich, Germany).
diff -r f9f2e1643593 -r 322e2a3335d4 Admin/page/main-layout/navigation.html --- a/Admin/page/main-layout/navigation.html Mon Jun 06 14:12:07 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -
-
- |
-
-
-
-
-
- - -
-
-
|
- ||
-
|
-