summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Doc/Implementation/Integration.thy

author | wenzelm |

Wed Mar 25 11:39:52 2015 +0100 (2015-03-25) | |

changeset 59809 | 87641097d0f3 |

parent 59090 | a0a05a4edb36 |

child 60094 | 96a4765ba7d1 |

permissions | -rw-r--r-- |

tuned signature;

1 (*:wrap=hard:maxLineLen=78:*)

3 theory Integration

4 imports Base

5 begin

7 chapter \<open>System integration\<close>

9 section \<open>Isar toplevel \label{sec:isar-toplevel}\<close>

11 text \<open>

12 The Isar \emph{toplevel state} represents the outermost configuration that

13 is transformed by a sequence of transitions (commands) within a theory body.

14 This is a pure value with pure functions acting on it in a timeless and

15 stateless manner. Historically, the sequence of transitions was wrapped up

16 as sequential command loop, such that commands are applied one-by-one. In

17 contemporary Isabelle/Isar, processing toplevel commands usually works in

18 parallel in multi-threaded Isabelle/ML @{cite "Wenzel:2009" and

19 "Wenzel:2013:ITP"}.

20 \<close>

23 subsection \<open>Toplevel state\<close>

25 text \<open>

26 The toplevel state is a disjoint sum of empty @{text toplevel}, or @{text

27 theory}, or @{text proof}. The initial toplevel is empty; a theory is

28 commenced by a @{command theory} header; within a theory we may use theory

29 commands such as @{command definition}, or state a @{command theorem} to be

30 proven. A proof state accepts a rich collection of Isar proof commands for

31 structured proof composition, or unstructured proof scripts. When the proof

32 is concluded we get back to the (local) theory, which is then updated by

33 defining the resulting fact. Further theory declarations or theorem

34 statements with proofs may follow, until we eventually conclude the theory

35 development by issuing @{command end} to get back to the empty toplevel.

36 \<close>

38 text %mlref \<open>

39 \begin{mldecls}

40 @{index_ML_type Toplevel.state} \\

41 @{index_ML_exception Toplevel.UNDEF} \\

42 @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\

43 @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\

44 @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\

45 \end{mldecls}

47 \begin{description}

49 \item Type @{ML_type Toplevel.state} represents Isar toplevel

50 states, which are normally manipulated through the concept of

51 toplevel transitions only (\secref{sec:toplevel-transition}).

53 \item @{ML Toplevel.UNDEF} is raised for undefined toplevel

54 operations. Many operations work only partially for certain cases,

55 since @{ML_type Toplevel.state} is a sum type.

57 \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty

58 toplevel state.

60 \item @{ML Toplevel.theory_of}~@{text "state"} selects the

61 background theory of @{text "state"}, it raises @{ML Toplevel.UNDEF}

62 for an empty toplevel state.

64 \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof

65 state if available, otherwise it raises @{ML Toplevel.UNDEF}.

67 \end{description}

68 \<close>

70 text %mlantiq \<open>

71 \begin{matharray}{rcl}

72 @{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\

73 \end{matharray}

75 \begin{description}

77 \item @{text "@{Isar.state}"} refers to Isar toplevel state at that

78 point --- as abstract value.

80 This only works for diagnostic ML commands, such as @{command

81 ML_val} or @{command ML_command}.

83 \end{description}

84 \<close>

87 subsection \<open>Toplevel transitions \label{sec:toplevel-transition}\<close>

89 text \<open>

90 An Isar toplevel transition consists of a partial function on the toplevel

91 state, with additional information for diagnostics and error reporting:

92 there are fields for command name, source position, and other meta-data.

94 The operational part is represented as the sequential union of a

95 list of partial functions, which are tried in turn until the first

96 one succeeds. This acts like an outer case-expression for various

97 alternative state transitions. For example, \isakeyword{qed} works

98 differently for a local proofs vs.\ the global ending of an outermost

99 proof.

101 Transitions are composed via transition transformers. Internally, Isar

102 commands are put together from an empty transition extended by name and

103 source position. It is then left to the individual command parser to turn

104 the given concrete syntax into a suitable transition transformer that

105 adjoins actual operations on a theory or proof state.

106 \<close>

108 text %mlref \<open>

109 \begin{mldecls}

110 @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->

111 Toplevel.transition -> Toplevel.transition"} \\

112 @{index_ML Toplevel.theory: "(theory -> theory) ->

113 Toplevel.transition -> Toplevel.transition"} \\

114 @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->

115 Toplevel.transition -> Toplevel.transition"} \\

116 @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->

117 Toplevel.transition -> Toplevel.transition"} \\

118 @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) ->

119 Toplevel.transition -> Toplevel.transition"} \\

120 @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->

121 Toplevel.transition -> Toplevel.transition"} \\

122 \end{mldecls}

124 \begin{description}

126 \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic

127 function.

129 \item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory

130 transformer.

132 \item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global

133 goal function, which turns a theory into a proof state. The theory

134 may be changed before entering the proof; the generic Isar goal

135 setup includes an @{verbatim after_qed} argument that specifies how to

136 apply the proven result to the enclosing context, when the proof

137 is finished.

139 \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic

140 proof command, with a singleton result.

142 \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof

143 command, with zero or more result states (represented as a lazy

144 list).

146 \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding

147 proof command, that returns the resulting theory, after applying the

148 resulting facts to the target context.

150 \end{description}

151 \<close>

153 text %mlex \<open>The file @{"file" "~~/src/HOL/ex/Commands.thy"} shows some example

154 Isar command definitions, with the all-important theory header declarations

155 for outer syntax keywords.\<close>

158 section \<open>Theory loader database\<close>

160 text \<open>

161 In batch mode and within dumped logic images, the theory database maintains

162 a collection of theories as a directed acyclic graph. A theory may refer to

163 other theories as @{keyword "imports"}, or to auxiliary files via special

164 \emph{load commands} (e.g.\ @{command ML_file}). For each theory, the base

165 directory of its own theory file is called \emph{master directory}: this is

166 used as the relative location to refer to other files from that theory.

167 \<close>

169 text %mlref \<open>

170 \begin{mldecls}

171 @{index_ML use_thy: "string -> unit"} \\

172 @{index_ML use_thys: "string list -> unit"} \\[0.5ex]

173 @{index_ML Thy_Info.get_theory: "string -> theory"} \\

174 @{index_ML Thy_Info.remove_thy: "string -> unit"} \\

175 @{index_ML Thy_Info.register_thy: "theory -> unit"} \\

176 \end{mldecls}

178 \begin{description}

180 \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully

181 up-to-date wrt.\ the external file store; outdated ancestors are reloaded on

182 demand.

184 \item @{ML use_thys} is similar to @{ML use_thy}, but handles several

185 theories simultaneously. Thus it acts like processing the import header of a

186 theory, without performing the merge of the result. By loading a whole

187 sub-graph of theories, the intrinsic parallelism can be exploited by the

188 system to speedup loading.

190 This variant is used by default in @{tool build} @{cite "isabelle-sys"}.

192 \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value

193 presently associated with name @{text A}. Note that the result might be

194 outdated wrt.\ the file-system content.

196 \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all

197 descendants from the theory database.

199 \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an existing

200 theory value with the theory loader database and updates source version

201 information according to the file store.

203 \end{description}

204 \<close>

206 end