src/Doc/IsarImplementation/Integration.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 56265 785569927666
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29755
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 27597
diff changeset
     1
theory Integration
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 27597
diff changeset
     2
imports Base
d66b34e46bdf observe usual theory naming conventions;
wenzelm
parents: 27597
diff changeset
     3
begin
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     4
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     5
chapter {* System integration *}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     6
20447
5b75f1c4d7d6 more on contexts;
wenzelm
parents: 20064
diff changeset
     7
section {* Isar toplevel \label{sec:isar-toplevel} *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
     8
48974
8882fc8005ad Typo fixed.
webertj
parents: 48938
diff changeset
     9
text {* The Isar toplevel may be considered the central hub of the
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    10
  Isabelle/Isar system, where all key components and sub-systems are
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 37982
diff changeset
    11
  integrated into a single read-eval-print loop of Isar commands,
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 37982
diff changeset
    12
  which also incorporates the underlying ML compiler.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    13
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    14
  Isabelle/Isar departs from the original ``LCF system architecture''
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 37982
diff changeset
    15
  where ML was really The Meta Language for defining theories and
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 37982
diff changeset
    16
  conducting proofs.  Instead, ML now only serves as the
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    17
  implementation language for the system (and user extensions), while
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    18
  the specific Isar toplevel supports the concepts of theory and proof
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    19
  development natively.  This includes the graph structure of theories
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    20
  and the block structure of proofs, support for unlimited undo,
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    21
  facilities for tracing, debugging, timing, profiling etc.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    22
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    23
  \medskip The toplevel maintains an implicit state, which is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    24
  transformed by a sequence of transitions -- either interactively or
52788
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 51659
diff changeset
    25
  in batch-mode.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    26
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    27
  The toplevel state is a disjoint sum of empty @{text toplevel}, or
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    28
  @{text theory}, or @{text proof}.  On entering the main Isar loop we
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    29
  start with an empty toplevel.  A theory is commenced by giving a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    30
  @{text \<THEORY>} header; within a theory we may issue theory
20025
95aeaa3ef35d Isar.context ();
wenzelm
parents: 18590
diff changeset
    31
  commands such as @{text \<DEFINITION>}, or state a @{text
95aeaa3ef35d Isar.context ();
wenzelm
parents: 18590
diff changeset
    32
  \<THEOREM>} to be proven.  Now we are within a proof state, with a
95aeaa3ef35d Isar.context ();
wenzelm
parents: 18590
diff changeset
    33
  rich collection of Isar proof commands for structured proof
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    34
  composition, or unstructured proof scripts.  When the proof is
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    35
  concluded we get back to the theory, which is then updated by
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    36
  storing the resulting fact.  Further theory declarations or theorem
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    37
  statements with proofs may follow, until we eventually conclude the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    38
  theory development by issuing @{text \<END>}.  The resulting theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    39
  is then stored within the theory database and we are back to the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    40
  empty toplevel.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    41
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    42
  In addition to these proper state transformations, there are also
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    43
  some diagnostic commands for peeking at the toplevel state without
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    44
  modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    45
  \isakeyword{print-cases}).
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    46
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    47
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    48
text %mlref {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    49
  \begin{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    50
  @{index_ML_type Toplevel.state} \\
55838
e120a15b0ee6 more antiquotations;
wenzelm
parents: 53709
diff changeset
    51
  @{index_ML_exception Toplevel.UNDEF} \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    52
  @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    53
  @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    54
  @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
32833
f3716d1a2e48 explicitly Unsynchronized;
wenzelm
parents: 32189
diff changeset
    55
  @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
f3716d1a2e48 explicitly Unsynchronized;
wenzelm
parents: 32189
diff changeset
    56
  @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    57
  \end{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    58
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    59
  \begin{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    60
39864
wenzelm
parents: 39826
diff changeset
    61
  \item Type @{ML_type Toplevel.state} represents Isar toplevel
wenzelm
parents: 39826
diff changeset
    62
  states, which are normally manipulated through the concept of
wenzelm
parents: 39826
diff changeset
    63
  toplevel transitions only (\secref{sec:toplevel-transition}).  Also
wenzelm
parents: 39826
diff changeset
    64
  note that a raw toplevel state is subject to the same linearity
wenzelm
parents: 39826
diff changeset
    65
  restrictions as a theory context (cf.~\secref{sec:context-theory}).
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    66
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    67
  \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    68
  operations.  Many operations work only partially for certain cases,
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    69
  since @{ML_type Toplevel.state} is a sum type.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    70
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    71
  \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    72
  toplevel state.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    73
34931
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
    74
  \item @{ML Toplevel.theory_of}~@{text "state"} selects the
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
    75
  background theory of @{text "state"}, raises @{ML Toplevel.UNDEF}
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
    76
  for an empty toplevel state.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    77
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    78
  \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    79
  state if available, otherwise raises @{ML Toplevel.UNDEF}.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    80
32833
f3716d1a2e48 explicitly Unsynchronized;
wenzelm
parents: 32189
diff changeset
    81
  \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    82
  information for each Isar command being executed.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    83
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 39882
diff changeset
    84
  \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 37982
diff changeset
    85
  low-level profiling of the underlying ML runtime system.  For
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    86
  Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
    87
  profiling.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    88
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    89
  \end{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    90
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
    91
39882
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
    92
text %mlantiq {*
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
    93
  \begin{matharray}{rcl}
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
    94
  @{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
    95
  \end{matharray}
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
    96
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
    97
  \begin{description}
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
    98
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
    99
  \item @{text "@{Isar.state}"} refers to Isar toplevel state at that
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
   100
  point --- as abstract value.
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
   101
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
   102
  This only works for diagnostic ML commands, such as @{command
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
   103
  ML_val} or @{command ML_command}.
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
   104
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
   105
  \end{description}
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
   106
*}
ab0afd03a042 cover @{Isar.state};
wenzelm
parents: 39864
diff changeset
   107
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   108
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   109
subsection {* Toplevel transitions \label{sec:toplevel-transition} *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   110
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   111
text {*
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   112
  An Isar toplevel transition consists of a partial function on the
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   113
  toplevel state, with additional information for diagnostics and
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   114
  error reporting: there are fields for command name, source position,
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   115
  optional source text, as well as flags for interactive-only commands
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   116
  (which issue a warning in batch-mode), printing of result state,
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   117
  etc.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   118
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   119
  The operational part is represented as the sequential union of a
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   120
  list of partial functions, which are tried in turn until the first
20475
wenzelm
parents: 20451
diff changeset
   121
  one succeeds.  This acts like an outer case-expression for various
34931
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   122
  alternative state transitions.  For example, \isakeyword{qed} works
20475
wenzelm
parents: 20451
diff changeset
   123
  differently for a local proofs vs.\ the global ending of the main
wenzelm
parents: 20451
diff changeset
   124
  proof.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   125
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   126
  Toplevel transitions are composed via transition transformers.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   127
  Internally, Isar commands are put together from an empty transition
34931
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   128
  extended by name and source position.  It is then left to the
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   129
  individual command parser to turn the given concrete syntax into a
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   130
  suitable transition transformer that adjoins actual operations on a
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   131
  theory or proof state etc.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   132
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   133
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   134
text %mlref {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   135
  \begin{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   136
  @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   137
  @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   138
  Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   139
  @{index_ML Toplevel.theory: "(theory -> theory) ->
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   140
  Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   141
  @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   142
  Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   143
  @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   144
  Toplevel.transition -> Toplevel.transition"} \\
49864
34437e7245cc updated Toplevel.proofs;
wenzelm
parents: 48985
diff changeset
   145
  @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) ->
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   146
  Toplevel.transition -> Toplevel.transition"} \\
21168
0f869edd6cc1 replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents: 20491
diff changeset
   147
  @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   148
  Toplevel.transition -> Toplevel.transition"} \\
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   149
  \end{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   150
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   151
  \begin{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   152
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   153
  \item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   154
  causes the toplevel loop to echo the result state (in interactive
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   155
  mode).
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   156
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   157
  \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   158
  function.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   159
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   160
  \item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   161
  transformer.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   162
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   163
  \item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   164
  goal function, which turns a theory into a proof state.  The theory
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   165
  may be changed before entering the proof; the generic Isar goal
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   166
  setup includes an argument that specifies how to apply the proven
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   167
  result to the theory, when the proof is finished.
18558
48d5419fd191 more stuff;
wenzelm
parents: 18554
diff changeset
   168
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   169
  \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   170
  proof command, with a singleton result.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   171
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   172
  \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   173
  command, with zero or more result states (represented as a lazy
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   174
  list).
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   175
21168
0f869edd6cc1 replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents: 20491
diff changeset
   176
  \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding
0f869edd6cc1 replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents: 20491
diff changeset
   177
  proof command, that returns the resulting theory, after storing the
0f869edd6cc1 replaced Toplevel.proof_to_theory by Toplevel.end_proof;
wenzelm
parents: 20491
diff changeset
   178
  resulting facts in the context etc.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   179
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   180
  \end{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   181
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   182
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   183
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   184
section {* Theory database \label{sec:theory-database} *}
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   185
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   186
text {*
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   187
  The theory database maintains a collection of theories, together
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   188
  with some administrative information about their original sources,
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   189
  which are held in an external store (i.e.\ some directory within the
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   190
  regular file system).
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   191
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   192
  The theory database is organized as a directed acyclic graph;
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   193
  entries are referenced by theory name.  Although some additional
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   194
  interfaces allow to include a directory specification as well, this
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   195
  is only a hint to the underlying theory loader.  The internal theory
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   196
  name space is flat!
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   197
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   198
  Theory @{text A} is associated with the main theory file @{text
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   199
  A}\verb,.thy,, which needs to be accessible through the theory
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 37982
diff changeset
   200
  loader path.  Any number of additional ML source files may be
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   201
  associated with each theory, by declaring these dependencies in the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   202
  theory header as @{text \<USES>}, and loading them consecutively
39825
f9066b94bf07 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents: 37982
diff changeset
   203
  within the theory context.  The system keeps track of incoming ML
34931
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   204
  sources and associates them with the current theory.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   205
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   206
  The basic internal actions of the theory database are @{text
37982
111ce9651564 updated manual concerning theory loader;
wenzelm
parents: 37864
diff changeset
   207
  "update"} and @{text "remove"}:
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   208
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   209
  \begin{itemize}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   210
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   211
  \item @{text "update A"} introduces a link of @{text "A"} with a
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   212
  @{text "theory"} value of the same name; it asserts that the theory
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   213
  sources are now consistent with that value;
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   214
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   215
  \item @{text "remove A"} deletes entry @{text "A"} from the theory
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   216
  database.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   217
  
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   218
  \end{itemize}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   219
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   220
  These actions are propagated to sub- or super-graphs of a theory
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   221
  entry as expected, in order to preserve global consistency of the
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   222
  state of all loaded theories with the sources of the external store.
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   223
  This implies certain causalities between actions: @{text "update"}
37982
111ce9651564 updated manual concerning theory loader;
wenzelm
parents: 37864
diff changeset
   224
  or @{text "remove"} of an entry will @{text "remove"} all
111ce9651564 updated manual concerning theory loader;
wenzelm
parents: 37864
diff changeset
   225
  descendants.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   226
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   227
  \medskip There are separate user-level interfaces to operate on the
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   228
  theory database directly or indirectly.  The primitive actions then
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   229
  just happen automatically while working with the system.  In
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   230
  particular, processing a theory header @{text "\<THEORY> A
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   231
  \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   232
  sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   233
  is up-to-date, too.  Earlier theories are reloaded as required, with
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   234
  @{text update} actions proceeding in topological order according to
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   235
  theory dependencies.  There may be also a wave of implied @{text
37982
111ce9651564 updated manual concerning theory loader;
wenzelm
parents: 37864
diff changeset
   236
  remove} actions for derived theory nodes until a stable situation
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   237
  is achieved eventually.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   238
*}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   239
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   240
text %mlref {*
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   241
  \begin{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   242
  @{index_ML use_thy: "string -> unit"} \\
24173
4ba00a972eb8 theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents: 22095
diff changeset
   243
  @{index_ML use_thys: "string list -> unit"} \\
37864
814b1bca7f35 qualified Thy_Info.get_theory;
wenzelm
parents: 37306
diff changeset
   244
  @{index_ML Thy_Info.get_theory: "string -> theory"} \\
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 34931
diff changeset
   245
  @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
37982
111ce9651564 updated manual concerning theory loader;
wenzelm
parents: 37864
diff changeset
   246
  @{index_ML Thy_Info.register_thy: "theory -> unit"} \\[1ex]
40149
4c35be108990 proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents: 39882
diff changeset
   247
  @{ML_text "datatype action = Update | Remove"} \\
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 34931
diff changeset
   248
  @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   249
  \end{mldecls}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   250
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   251
  \begin{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   252
24173
4ba00a972eb8 theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents: 22095
diff changeset
   253
  \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
4ba00a972eb8 theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents: 22095
diff changeset
   254
  up-to-date wrt.\ the external file store, reloading outdated
34931
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   255
  ancestors as required.  In batch mode, the simultaneous @{ML
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   256
  use_thys} should be used exclusively.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   257
24173
4ba00a972eb8 theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents: 22095
diff changeset
   258
  \item @{ML use_thys} is similar to @{ML use_thy}, but handles
4ba00a972eb8 theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents: 22095
diff changeset
   259
  several theories simultaneously.  Thus it acts like processing the
4ba00a972eb8 theory loader: added use_thys, removed obsolete update_thy;
wenzelm
parents: 22095
diff changeset
   260
  import header of a theory, without performing the merge of the
34931
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   261
  result.  By loading a whole sub-graph of theories like that, the
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   262
  intrinsic parallelism can be exploited by the system, to speedup
fd90fb0903c0 minimal tuning of this slightly dated material;
wenzelm
parents: 34921
diff changeset
   263
  loading.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   264
37864
814b1bca7f35 qualified Thy_Info.get_theory;
wenzelm
parents: 37306
diff changeset
   265
  \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value
814b1bca7f35 qualified Thy_Info.get_theory;
wenzelm
parents: 37306
diff changeset
   266
  presently associated with name @{text A}.  Note that the result
814b1bca7f35 qualified Thy_Info.get_theory;
wenzelm
parents: 37306
diff changeset
   267
  might be outdated.
814b1bca7f35 qualified Thy_Info.get_theory;
wenzelm
parents: 37306
diff changeset
   268
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 34931
diff changeset
   269
  \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   270
  descendants from the theory database.
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   271
37982
111ce9651564 updated manual concerning theory loader;
wenzelm
parents: 37864
diff changeset
   272
  \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an
111ce9651564 updated manual concerning theory loader;
wenzelm
parents: 37864
diff changeset
   273
  existing theory value with the theory loader database and updates
111ce9651564 updated manual concerning theory loader;
wenzelm
parents: 37864
diff changeset
   274
  source version information according to the current file-system
111ce9651564 updated manual concerning theory loader;
wenzelm
parents: 37864
diff changeset
   275
  state.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   276
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 34931
diff changeset
   277
  \item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   278
  f} as a hook for theory database actions.  The function will be
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   279
  invoked with the action and theory name being involved; thus derived
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   280
  actions may be performed in associated system components, e.g.\
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   281
  maintaining the state of an editor for the theory sources.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   282
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   283
  The kind and order of actions occurring in practice depends both on
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   284
  user interactions and the internal process of resolving theory
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   285
  imports.  Hooks should not rely on a particular policy here!  Any
20451
27ea2ba48fa3 misc cleanup;
wenzelm
parents: 20447
diff changeset
   286
  exceptions raised by the hook are ignored.
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   287
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   288
  \end{description}
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   289
*}
30272
2d612824e642 regenerated document;
wenzelm
parents: 30270
diff changeset
   290
18537
2681f9e34390 "The Isabelle/Isar Implementation" manual;
wenzelm
parents:
diff changeset
   291
end