src/Pure/Thy/README
author wenzelm
Fri, 21 Nov 1997 15:35:37 +0100
changeset 4273 c9b577c8f7a1
parent 592 9154d8410514
permissions -rw-r--r--
comment;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
592
9154d8410514 documentation on theories
lcp
parents:
diff changeset
     1
    ID:         $Id$
9154d8410514 documentation on theories
lcp
parents:
diff changeset
     2
    Directory:  Pure/Thy
9154d8410514 documentation on theories
lcp
parents:
diff changeset
     3
    Author:     Carsten Clasohm
9154d8410514 documentation on theories
lcp
parents:
diff changeset
     4
    Copyright   1994 TU Muenchen
9154d8410514 documentation on theories
lcp
parents:
diff changeset
     5
9154d8410514 documentation on theories
lcp
parents:
diff changeset
     6
4273
c9b577c8f7a1 comment;
wenzelm
parents: 592
diff changeset
     7
FIXME FIXME FIXME FIXME FIXME Warning: not quite up-to-date!
c9b577c8f7a1 comment;
wenzelm
parents: 592
diff changeset
     8
c9b577c8f7a1 comment;
wenzelm
parents: 592
diff changeset
     9
592
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    10
Conventions for theory- and filenames:
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    11
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    12
- Files for theory T are named T.thy and T.ML where only one of these two
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    13
  must exist.
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    14
- Either T.thy or T.ML must define a ML structure containing an element
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    15
  named thy (the theory).
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    16
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    17
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    18
Information stored about loaded theories:
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    19
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    20
- name of the theory
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    21
- absolute path of the theory's files
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    22
- time of last modification for .thy and .ML file
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    23
  (updated when the files are read)
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    24
- names of all read theories that depend on the theory
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    25
- the theory as a ML object
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    26
- theorems
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    27
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    28
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    29
How to rebuild the theory hierarchy:
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    30
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    31
The database not only contains theories read from files but also the 
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    32
'mother of all theories' - Pure. By retrieving this theory's child list
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    33
(i.e. the names of all theories that are extensions of it) one can build the 
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    34
hierarchy by recursively repeating this procedure.
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    35
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    36
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    37
The datatype used:
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    38
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    39
Information is stored in the variable loaded_thys which has type
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    40
"thy_info Symtab.table ref", i.e. as an unbalanced binary tree with
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    41
the theory names as keys and entries of type thy_info:
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    42
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    43
datatype thy_info = ThyInfo of {path: string,
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    44
                                children: string list,
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    45
                                thy_time: string option,
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    46
                                ml_time: string option,
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    47
                                theory: theory option,
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    48
                                thms: thm Symtab.table};
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    49
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    50
path: absolute path of directory where the files where located when the theory
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    51
      was last read
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    52
children: names of all read theories that are descendants of this theory
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    53
thy_time: If T.thy existed this contains information about the file which
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    54
  looks like this: Some "-rw-r--r--  1 clasohm       232 Aug 19 11:10 ".
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    55
  Else it is 'None'.
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    56
ml_time: same for T.ML
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    57
theory: ML object containing the theory. As entries in loaded_thys are created
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    58
  before the theory has been read this may be 'None' in case of an error
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    59
  during use_thy "T".
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    60
thms: theorems
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    61
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    62
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    63
An entry may look like this:
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    64
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    65
   ("Fun",
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    66
      ThyInfo
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    67
         {path = "/disk1/usr/stud/clasohm/isabelle/HOL/./",
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    68
            thms = ?,
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    69
            theory = Some {Pure, HOL, Ord, Set},
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    70
            ml_time = Some "-rw-r--r--  1 clasohm      6076 Aug 30 10:04 ",
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    71
            children = ["Prod", "subset"],
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    72
            thy_time =
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    73
            Some "-rw-r--r--  1 clasohm       243 Aug 19 11:02 "})
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    74
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    75
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    76
Notes:
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    77
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    78
In general all theories contained in loaded_thys are linked with Pure.
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    79
Though stray theories are possible they are removed from loaded_thys 
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    80
automatically as soon as update(); is used.
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    81
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    82
Cycles in the hierarchy are not allowed and it is guaranteed that
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    83
loaded_thys doesn't contain one. On the other hand this is possible
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    84
(with all lines representing downward arrows):
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    85
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    86
     A
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    87
    / \
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    88
   B   C
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    89
   |   |
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    90
   \   D
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    91
    \ /
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    92
     E
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    93
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    94
Isabelle first searches for theory files in the directory stored in
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    95
thy_info's path component. But in case they have been moved meanwhile
9154d8410514 documentation on theories
lcp
parents:
diff changeset
    96
the variable load_path (string list ref) is used to find them.