190 If there is more than one term to be printed, you can use the |
190 If there is more than one term to be printed, you can use the |
191 function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} |
191 function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} |
192 to separate them. |
192 to separate them. |
193 *} |
193 *} |
194 |
194 |
195 ML{*fun pretty_terms ctxt ts = |
195 ML{*fun pretty_terms ctxt trms = |
196 Pretty.block (Pretty.commas (map (pretty_term ctxt) ts))*} |
196 Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*} |
197 |
197 |
198 text {* |
198 text {* |
199 You can also print out terms together with their typing information. |
199 You can also print out terms together with their typing information. |
200 For this you need to set the configuration value |
200 For this you need to set the configuration value |
201 @{ML_ind show_types in Syntax} to @{ML true}. |
201 @{ML_ind show_types in Syntax} to @{ML true}. |
233 |
233 |
234 text {* |
234 text {* |
235 A @{ML_type cterm} can be printed with the following function. |
235 A @{ML_type cterm} can be printed with the following function. |
236 *} |
236 *} |
237 |
237 |
238 ML{*fun pretty_cterm ctxt ct = |
238 ML{*fun pretty_cterm ctxt ctrm = |
239 pretty_term ctxt (term_of ct)*} |
239 pretty_term ctxt (term_of ctrm)*} |
240 |
240 |
241 text {* |
241 text {* |
242 Here the function @{ML_ind term_of in Thm} extracts the @{ML_type |
242 Here the function @{ML_ind term_of in Thm} extracts the @{ML_type |
243 term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can be |
243 term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can be |
244 printed again with @{ML commas in Pretty}. |
244 printed again with @{ML commas in Pretty}. |
245 *} |
245 *} |
246 |
246 |
247 ML{*fun pretty_cterms ctxt cts = |
247 ML{*fun pretty_cterms ctxt ctrms = |
248 Pretty.block (Pretty.commas (map (pretty_cterm ctxt) cts))*} |
248 Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))*} |
249 |
249 |
250 text {* |
250 text {* |
251 The easiest way to get the string of a theorem is to transform it |
251 The easiest way to get the string of a theorem is to transform it |
252 into a @{ML_type term} using the function @{ML_ind prop_of in Thm}. |
252 into a @{ML_type term} using the function @{ML_ind prop_of in Thm}. |
253 *} |
253 *} |
282 |
282 |
283 @{ML_response_fake [display, gray] |
283 @{ML_response_fake [display, gray] |
284 "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})" |
284 "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})" |
285 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"} |
285 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"} |
286 |
286 |
287 Again the function @{ML commas} helps with printing more than one theorem. |
287 Again the functions @{ML commas} and @{ML block in Pretty} help |
|
288 with printing more than one theorem. |
288 *} |
289 *} |
289 |
290 |
290 ML{*fun pretty_thms ctxt thms = |
291 ML{*fun pretty_thms ctxt thms = |
291 Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms)) |
292 Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms)) |
292 |
293 |
293 fun pretty_thms_no_vars ctxt thms = |
294 fun pretty_thms_no_vars ctxt thms = |
294 Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*} |
295 Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*} |
295 |
296 |
296 text {* |
297 text {* |
297 The printing functions for types are |
298 Printing functions for types are |
298 *} |
299 *} |
299 |
300 |
300 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty |
301 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty |
301 fun pretty_typs ctxt tys = |
302 fun pretty_typs ctxt tys = |
302 Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*} |
303 Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*} |
311 |
312 |
312 text {* |
313 text {* |
313 \begin{readmore} |
314 \begin{readmore} |
314 The simple conversion functions from Isabelle's main datatypes to |
315 The simple conversion functions from Isabelle's main datatypes to |
315 @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. |
316 @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. |
316 The references that change the printing information are declared in |
317 The configuration values that change the printing information are declared in |
317 @{ML_file "Pure/Syntax/printer.ML"}. |
318 @{ML_file "Pure/Syntax/printer.ML"}. |
318 \end{readmore} |
319 \end{readmore} |
319 |
320 |
320 Note that for printing out several ``parcels'' of information that belong |
321 Note that for printing out several ``parcels'' of information that belong |
321 together, like a warning message consisting of a term and its type, you |
322 together, like a warning message consisting of a term and its type, you |
901 text {* |
902 text {* |
902 Isabelle provides mechanisms for storing (and retrieving) arbitrary |
903 Isabelle provides mechanisms for storing (and retrieving) arbitrary |
903 data. Before we delve into the details, let us digress a bit. Conventional |
904 data. Before we delve into the details, let us digress a bit. Conventional |
904 wisdom has it that the type-system of ML ensures that an |
905 wisdom has it that the type-system of ML ensures that an |
905 @{ML_type "'a list"}, say, can only hold elements of the same type, namely |
906 @{ML_type "'a list"}, say, can only hold elements of the same type, namely |
906 @{ML_type "'a"}. Despite this wisdom, however, it is possible to implement a |
907 @{ML_type "'a"} (or whatever is substitued for it). Despite this common |
|
908 wisdom, however, it is possible to implement a |
907 universal type in ML, although by some arguably accidental features of ML. |
909 universal type in ML, although by some arguably accidental features of ML. |
908 This universal type can be used to store data of different type into a single list. |
910 This universal type can be used to store data of different type into a single list. |
909 In fact, it allows one to inject and to project data of \emph{arbitrary} type. This is |
911 In fact, it allows one to inject and to project data of \emph{arbitrary} type. This is |
910 in contrast to datatypes, which only allow injection and projection of data for |
912 in contrast to datatypes, which only allow injection and projection of data for |
911 some \emph{fixed} collection of types. In light of the conventional wisdom cited |
913 some \emph{fixed} collection of types. In light of the conventional wisdom cited |
974 contexts}. Data such as simpsets are ``global'' and therefore need to be stored |
976 contexts}. Data such as simpsets are ``global'' and therefore need to be stored |
975 in a theory (simpsets need to be maintained across proofs and even across |
977 in a theory (simpsets need to be maintained across proofs and even across |
976 theories). On the other hand, data such as facts change inside a proof and |
978 theories). On the other hand, data such as facts change inside a proof and |
977 are only relevant to the proof at hand. Therefore such data needs to be |
979 are only relevant to the proof at hand. Therefore such data needs to be |
978 maintained inside a proof context, which represents ``local'' data. |
980 maintained inside a proof context, which represents ``local'' data. |
|
981 You can think of a theory as the ``longterm memory'' of Isabelle (nothing will |
|
982 be deleted from it), and a proof-context as a ``shortterm memory'' (it dynamically |
|
983 changes according to what is needed at the time). |
979 |
984 |
980 For theories and proof contexts there are, respectively, the functors |
985 For theories and proof contexts there are, respectively, the functors |
981 @{ML_funct_ind Theory_Data} and @{ML_funct_ind Proof_Data} that help |
986 @{ML_funct_ind Theory_Data} and @{ML_funct_ind Proof_Data} that help |
982 with the data storage. Below we show how to implement a table in which you |
987 with the data storage. Below we show how to implement a table in which you |
983 can store theorems and look them up according to a string key. The |
988 can store theorems and look them up according to a string key. The |