CookBook/Intro.thy
author Christian Urban <urbanc@in.tum.de>
Mon, 24 Nov 2008 02:51:08 +0100
changeset 49 a0edabf14457
parent 44 dee4b3e66dfe
child 50 3d4b49921cdb
permissions -rw-r--r--
added more material
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory Intro
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
imports Main
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
begin
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
chapter {* Introduction *}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
text {*
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
     9
  The purpose of this cookbook is to guide the reader through the
11
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
    10
  first steps of Isabelle programming, and to provide recipes for
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
  solving common problems. 
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
*}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
section {* Intended Audience and Prior Knowledge *}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    16
text {* 
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    17
  This cookbook targets an audience who already knows how to use Isabelle
6
007e09485351 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 5
diff changeset
    18
  for writing theories and proofs. We also assume that readers are 
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
    19
  familiar with Standard ML, the programming language in which  
11
733614e236a3 tuned and updated antquote_setup.ML
Christian Urban <urbanc@in.tum.de>
parents: 6
diff changeset
    20
  most of Isabelle is implemented. If you are unfamiliar with either of
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
  these two subjects, you should first work through the Isabelle/HOL
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 12
diff changeset
    22
  tutorial \cite{isa-tutorial} or Paulson's book on Standard ML
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
  \cite{paulson-ml2}.
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
*}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    27
section {* Existing Documentation *}
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
text {*
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
  
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
    31
  The following documentation about Isabelle programming already exists (and is
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
    32
  part of the distribution of Isabelle):
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
  \begin{description}
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    35
  \item[The Implementation Manual] describes Isabelle
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    36
  from a high-level perspective, documenting both the underlying
6
007e09485351 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 5
diff changeset
    37
  concepts and some of the interfaces. 
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    39
  \item[The Isabelle Reference Manual] is an older document that used
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    40
  to be the main reference of Isabelle at a time when all proof scripts 
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    41
  were written on the ML level. Many parts of this manual are outdated 
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    42
  now, but some  parts, particularly the chapters on tactics, are still 
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    43
  useful.
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    45
  \item[The Isar Reference Manual] is also an older document that provides
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    46
  material about Isar and its implementation. Some material in it
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
    47
  is still useful.
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    48
  \end{description}
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    49
12
2f1736cb8f26 various changes by Alex and Christian
Christian Urban <urbanc@in.tum.de>
parents: 11
diff changeset
    50
  Then of course there is:
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    51
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    52
  \begin{description}
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    53
  \item[The code] is of course the ultimate reference for how
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
  things really work. Therefore you should not hesitate to look at the
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
  way things are actually implemented. More importantly, it is often
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
  good to look at code that does similar things as you want to do, to
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
  learn from other people's code.
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
  \end{description}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
  Since Isabelle is not a finished product, these manuals, just like
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    61
  the implementation itself, are always under construction. This can
5
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    62
  be difficult and frustrating at times, especially when interfaces changes
e91f54791e14 minor modifiations to the Intro and FirstSteps chapters
Christian Urban <urbanc@in.tum.de>
parents: 2
diff changeset
    63
  occur frequently. But it is a reality that progress means changing
2
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
  things (FIXME: need some short and convincing comment that this
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
  is a strategy, not a problem that should be solved).
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    66
*}
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    67
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    68
978a3c2ed7ce split the document into smaller pieces;
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
end