43   \<open>\<verbclose>\<close>\isanewline

    43   \<open>\<verbclose>\<close>\isanewline

    44   \<open>> 7\<close>\smallskip

    44   \<open>> 7\<close>\smallskip

    45   \end{graybox}

    45   \end{graybox}

    46   \end{isabelle}

    46   \end{isabelle}

    47 

    47 

    52   and you see the evaluated result in the ``Output'' window.

    50   and you see the evaluated result in the ``Output'' window.

    53 

    51 

    54   As mentioned in the Introduction, we will drop the \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> scaffolding whenever we show code. The lines

    52   As mentioned in the Introduction, we will drop the \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> scaffolding whenever we show code. The lines

    55   prefixed with @{text [quotes] ">"} are not part of the code, rather they

    53   prefixed with @{text [quotes] ">"} are not part of the code, rather they

    56   indicate what the response is when the code is evaluated.  There are also

    54   indicate what the response is when the code is evaluated.  There are also

    93 text \<open>

    91 text \<open>

    94   During development you might find it necessary to inspect data in your

    92   During development you might find it necessary to inspect data in your

    95   code. This can be done in a ``quick-and-dirty'' fashion using the function

    93   code. This can be done in a ``quick-and-dirty'' fashion using the function

    96   @{ML_ind writeln in Output}. For example

    94   @{ML_ind writeln in Output}. For example

    97 

    95 

    99 

    97 

   100   will print out @{text [quotes] "any string"}.  

    98   will print out @{text [quotes] "any string"}.  

   101   This function expects a string as argument. If you develop under

    99   This function expects a string as argument. If you develop under

   102   PolyML, then there is a convenient, though again ``quick-and-dirty'', method

   100   PolyML, then there is a convenient, though again ``quick-and-dirty'', method

   103   for converting values into strings, namely the antiquotation 

   101   for converting values into strings, namely the antiquotation 

   104   \<open>@{make_string}\<close>:

   102   \<open>@{make_string}\<close>:

   105 

   103 

   107 

   105 

   108   However, \<open>@{make_string}\<close> only works if the type of what

   106   However, \<open>@{make_string}\<close> only works if the type of what

   109   is converted is monomorphic and not a function. 

   107   is converted is monomorphic and not a function. 

   110 

   108 

   111   You can print out error messages with the function @{ML_ind error in Library}; 

   109   You can print out error messages with the function @{ML_ind error in Library}; 

   112   for example:

   110   for example:

   113 

   111 

   115   "if 0 = 1 then true else (error \"foo\")" 

   113   "if 0 = 1 then true else (error \"foo\")" 

   116 "*** foo

   114 "*** foo

   117 ***"}

   115 ***"}

   118 

   116 

   119   This function raises the exception \<open>ERROR\<close>, which will then 

   117   This function raises the exception \<open>ERROR\<close>, which will then 

   126   Most often you want to inspect contents of Isabelle's basic data structures,

   124   Most often you want to inspect contents of Isabelle's basic data structures,

   127   namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}

   125   namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}

   128   and @{ML_type thm}. Isabelle provides elaborate pretty-printing functions,

   126   and @{ML_type thm}. Isabelle provides elaborate pretty-printing functions,

   129   which we will explain in more detail in Section \ref{sec:pretty}. For now

   127   which we will explain in more detail in Section \ref{sec:pretty}. For now

   130   we just use the functions @{ML_ind writeln in Pretty}  from the structure

   128   we just use the functions @{ML_ind writeln in Pretty}  from the structure

   133 \<close>

   131 \<close>

   134 

   132 

   135 ML %grayML\<open>val pretty_term = Syntax.pretty_term

   133 ML %grayML\<open>val pretty_term = Syntax.pretty_term

   136 val pwriteln = Pretty.writeln\<close>

   134 val pwriteln = Pretty.writeln\<close>

   137 

   135 

   138 text \<open>

   136 text \<open>

   139   They can be used as follows

   137   They can be used as follows

   140 

   138 

   142   "pwriteln (pretty_term @{context} @{term \"1::nat\"})"

   140   "pwriteln (pretty_term @{context} @{term \"1::nat\"})"

   143   "\"1\""}

   141   "\"1\""}

   144 

   142 

   145   If there is more than one term to be printed, you can use the 

   143   If there is more than one term to be printed, you can use the 

   146   function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} 

   144   function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} 

   159 ML %grayML\<open>val show_types_ctxt = Config.put show_types true @{context}\<close>

   157 ML %grayML\<open>val show_types_ctxt = Config.put show_types true @{context}\<close>

   160 

   158 

   161 text \<open>

   159 text \<open>

   162   Now by using this context @{ML pretty_term} prints out

   160   Now by using this context @{ML pretty_term} prints out

   163 

   161 

   165   "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"

   163   "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"

   166   "(1::nat, x::'a)"}

   164   "(1::nat, x::'a)"}

   167 

   165 

   168   where \<open>1\<close> and \<open>x\<close> are displayed with their inferred types.

   166   where \<open>1\<close> and \<open>x\<close> are displayed with their inferred types.

   169   Other configuration values that influence

   167   Other configuration values that influence

   203   \<open>?Q\<close> and so on. They are instantiated by Isabelle when a theorem is applied.

   201   \<open>?Q\<close> and so on. They are instantiated by Isabelle when a theorem is applied.

   204   For example, the theorem 

   202   For example, the theorem 

   205   @{thm [source] conjI} shown below can be used for any (typable) 

   203   @{thm [source] conjI} shown below can be used for any (typable) 

   206   instantiation of \<open>?P\<close> and \<open>?Q\<close>. 

   204   instantiation of \<open>?P\<close> and \<open>?Q\<close>. 

   207 

   205 

   209   "pwriteln (pretty_thm @{context} @{thm conjI})"

   207   "pwriteln (pretty_thm @{context} @{thm conjI})"

   210   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}

   208   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}

   211 

   209 

   212   However, to improve the readability when printing theorems, we

   210   However, to improve the readability when printing theorems, we

   213   can switch off the question marks as follows:

   211   can switch off the question marks as follows:

   221 end\<close>

   219 end\<close>

   222 

   220 

   223 text \<open>

   221 text \<open>

   224   With this function, theorem @{thm [source] conjI} is now printed as follows:

   222   With this function, theorem @{thm [source] conjI} is now printed as follows:

   225 

   223 

   227   "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"

   225   "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"

   228   "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}

   226   "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}

   229   

   227   

   230   Again the functions @{ML commas} and @{ML block in Pretty} help 

   228   Again the functions @{ML commas} and @{ML block in Pretty} help 

   231   with printing more than one theorem. 

   229   with printing more than one theorem. 

   264   Note that for printing out several ``parcels'' of information that belong

   262   Note that for printing out several ``parcels'' of information that belong

   265   together, like a warning message consisting of a term and its type, you

   263   together, like a warning message consisting of a term and its type, you

   266   should try to print these parcels together in a single string. Therefore do

   264   should try to print these parcels together in a single string. Therefore do

   267   \emph{not} print out information as

   265   \emph{not} print out information as

   268 

   266 

   270 "pwriteln (Pretty.str \"First half,\"); 

   268 "pwriteln (Pretty.str \"First half,\"); 

   271 pwriteln (Pretty.str \"and second half.\")"

   269 pwriteln (Pretty.str \"and second half.\")"

   272 "First half,

   270 "First half,

   273 and second half."}

   271 and second half."}

   274 

   272 

   275   but as a single string with appropriate formatting. For example

   273   but as a single string with appropriate formatting. For example

   276 

   274 

   278 "pwriteln (Pretty.str (\"First half,\" ^ \"\\n\" ^ \"and second half.\"))"

   276 "pwriteln (Pretty.str (\"First half,\" ^ \"\\n\" ^ \"and second half.\"))"

   279 "First half,

   277 "First half,

   280 and second half."}

   278 and second half."}

   281   

   279   

   282   To ease this kind of string manipulations, there are a number

   280   To ease this kind of string manipulations, there are a number

   283   of library functions in Isabelle. For example,  the function 

   281   of library functions in Isabelle. For example,  the function 

   284   @{ML_ind cat_lines in Library} concatenates a list of strings 

   282   @{ML_ind cat_lines in Library} concatenates a list of strings 

   285   and inserts newlines in between each element. 

   283   and inserts newlines in between each element. 

   286 

   284 

   288   "pwriteln (Pretty.str (cat_lines [\"foo\", \"bar\"]))"

   286   "pwriteln (Pretty.str (cat_lines [\"foo\", \"bar\"]))"

   289   "foo

   287   "foo

   290 bar"}

   288 bar"}

   291 

   289 

   292   Section \ref{sec:pretty} will explain the infrastructure that Isabelle 

   290   Section \ref{sec:pretty} will explain the infrastructure that Isabelle 

   387   This function takes a term and a context as arguments. If the term is of function

   385   This function takes a term and a context as arguments. If the term is of function

   388   type, then @{ML "apply_fresh_args"} returns the term with distinct variables 

   386   type, then @{ML "apply_fresh_args"} returns the term with distinct variables 

   389   applied to it. For example, below three variables are applied to the term 

   387   applied to it. For example, below three variables are applied to the term 

   390   @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:

   388   @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:

   391 

   389 

   393 "let

   391 "let

   394   val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}

   392   val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}

   395   val ctxt = @{context}

   393   val ctxt = @{context}

   396 in 

   394 in 

   397   apply_fresh_args trm ctxt

   395   apply_fresh_args trm ctxt

   414   

   412   

   415   Functions like @{ML apply_fresh_args} are often needed when constructing

   413   Functions like @{ML apply_fresh_args} are often needed when constructing

   416   terms involving fresh variables. For this the infrastructure helps

   414   terms involving fresh variables. For this the infrastructure helps

   417   tremendously to avoid any name clashes. Consider for example:

   415   tremendously to avoid any name clashes. Consider for example:

   418 

   416 

   420 "let

   418 "let

   421   val trm = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}

   419   val trm = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}

   422   val ctxt = @{context}

   420   val ctxt = @{context}

   423 in

   421 in

   424   apply_fresh_args trm ctxt 

   422   apply_fresh_args trm ctxt 

   460   my_note @{binding "bar_conjunct2"} @{thm conjunct2}

   458   my_note @{binding "bar_conjunct2"} @{thm conjunct2}

   461 end\<close>

   459 end\<close>

   462 

   460 

   463 text \<open>

   461 text \<open>

   464   The function @{ML_text "my_note"} in line 3 is just a wrapper for the function 

   462   The function @{ML_text "my_note"} in line 3 is just a wrapper for the function 

   466   it stores a theorem under a name. 

   464   it stores a theorem under a name. 

   467   In lines 5 to 6 we call this function to give alternative names for the three

   465   In lines 5 to 6 we call this function to give alternative names for the three

   468   theorems. The point of @{ML "#>"} is that you can sequence such function calls. 

   466   theorems. The point of @{ML "#>"} is that you can sequence such function calls. 

   469 

   467 

   470   The remaining combinators we describe in this section add convenience for

   468   The remaining combinators we describe in this section add convenience for

   587 text \<open>

   585 text \<open>

   588   The purpose of Line 2 is to just pair up the argument with a dummy value (since

   586   The purpose of Line 2 is to just pair up the argument with a dummy value (since

   589   @{ML ||>>} operates on pairs). Each of the next three lines just increment 

   587   @{ML ||>>} operates on pairs). Each of the next three lines just increment 

   590   the value by one, but also nest the intermediate results to the left. For example 

   588   the value by one, but also nest the intermediate results to the left. For example 

   591 

   589 

   593   "acc_incs 1"

   591   "acc_incs 1"

   594   "((((\"\", 1), 2), 3), 4)"}

   592   "((((\"\", 1), 2), 3), 4)"}

   595 

   593 

   596   You can continue this chain with:

   594   You can continue this chain with:

   597   

   595   

   599   "acc_incs 1 ||>> (fn x => (x, x + 2))"

   597   "acc_incs 1 ||>> (fn x => (x, x + 2))"

   600   "(((((\"\", 1), 2), 3), 4), 6)"}

   598   "(((((\"\", 1), 2), 3), 4), 6)"}

   601 

   599 

   602   An example where this combinator is useful is as follows

   600   An example where this combinator is useful is as follows

   603 

   601 

   605   "let

   603   "let

   606   val ((names1, names2), _) =

   604   val ((names1, names2), _) =

   607     @{context}

   605     @{context}

   608     |> Variable.variant_fixes (replicate 4 \"x\")

   606     |> Variable.variant_fixes (replicate 4 \"x\")

   609     ||>> Variable.variant_fixes (replicate 5 \"x\")

   607     ||>> Variable.variant_fixes (replicate 5 \"x\")

   639   augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing 

   637   augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing 

   640   information about the definitions---the function @{ML_ind define in Local_Defs} returns

   638   information about the definitions---the function @{ML_ind define in Local_Defs} returns

   641   both as pairs. We can use this information for example to print out the definiens and 

   639   both as pairs. We can use this information for example to print out the definiens and 

   642   the theorem corresponding to the definitions. For example for the first definition:

   640   the theorem corresponding to the definitions. For example for the first definition:

   643 

   641 

   645   "let 

   643   "let 

   646   val (one_trm, (_, one_thm)) = one_def

   644   val (one_trm, (_, one_thm)) = one_def

   647 in

   645 in

   648   pwriteln (pretty_term ctxt' one_trm);

   646   pwriteln (pretty_term ctxt' one_trm);

   649   pwriteln (pretty_thm ctxt' one_thm)

   647   pwriteln (pretty_thm ctxt' one_thm)

   673   plumbing is also needed in situations where a function operates over lists, 

   671   plumbing is also needed in situations where a function operates over lists, 

   674   but one calculates only with a single element. An example is the function 

   672   but one calculates only with a single element. An example is the function 

   675   @{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check 

   673   @{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check 

   676   a list of terms. Consider the code:

   674   a list of terms. Consider the code:

   677 

   675 

   679   "let

   677   "let

   680   val ctxt = @{context}

   678   val ctxt = @{context}

   681 in

   679 in

   682   map (Syntax.parse_term ctxt) [\"m + n\", \"m * n\", \"m - (n::nat)\"] 

   680   map (Syntax.parse_term ctxt) [\"m + n\", \"m * n\", \"m - (n::nat)\"] 

   683   |> Syntax.check_terms ctxt

   681   |> Syntax.check_terms ctxt

   694   check_terms in Syntax} needs plumbing. This can be done with the function

   692   check_terms in Syntax} needs plumbing. This can be done with the function

   695   @{ML_ind singleton in Library}.\footnote{There is already a function @{ML check_term in

   693   @{ML_ind singleton in Library}.\footnote{There is already a function @{ML check_term in

   696   Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented 

   694   Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented 

   697   in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example

   695   in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example

   698 

   696 

   700   "let 

   698   "let 

   701   val ctxt = @{context}

   699   val ctxt = @{context}

   702 in

   700 in

   703   Syntax.parse_term ctxt \"m - (n::nat)\" 

   701   Syntax.parse_term ctxt \"m - (n::nat)\" 

   704   |> singleton (Syntax.check_terms ctxt)

   702   |> singleton (Syntax.check_terms ctxt)

   743   except in Appendix \ref{rec:docantiquotations} where we show how to

   741   except in Appendix \ref{rec:docantiquotations} where we show how to

   744   implement your own document antiquotations.}  Syntactically antiquotations

   742   implement your own document antiquotations.}  Syntactically antiquotations

   745   are indicated by the @{ML_text @}-sign followed by text wrapped in \<open>{\<dots>}\<close>.  For example, one can print out the name of the current theory with

   743   are indicated by the @{ML_text @}-sign followed by text wrapped in \<open>{\<dots>}\<close>.  For example, one can print out the name of the current theory with

   746   the code

   744   the code

   747   

   745   

   749  

   747  

   750   where \<open>@{theory}\<close> is an antiquotation that is substituted with the

   748   where \<open>@{theory}\<close> is an antiquotation that is substituted with the

   751   current theory (remember that we assumed we are inside the theory 

   749   current theory (remember that we assumed we are inside the theory 

   752   \<open>First_Steps\<close>). The name of this theory can be extracted using

   750   \<open>First_Steps\<close>). The name of this theory can be extracted using

   753   the function @{ML_ind theory_name in Context}. 

   751   the function @{ML_ind theory_name in Context}. 

   771   difference between a theory and a context is will be described in Chapter

   769   difference between a theory and a context is will be described in Chapter

   772   \ref{chp:advanced}.) A context is for example needed to use the

   770   \ref{chp:advanced}.) A context is for example needed to use the

   773   function @{ML print_abbrevs in Proof_Context} that list of all currently

   771   function @{ML print_abbrevs in Proof_Context} that list of all currently

   774   defined abbreviations. For example

   772   defined abbreviations. For example

   775 

   773 

   777   "Proof_Context.print_abbrevs false @{context}"

   775   "Proof_Context.print_abbrevs false @{context}"

   778 "\<dots>

   776 "\<dots>

   779 INTER \<equiv> INFI

   777 INTER \<equiv> INFI

   780 Inter \<equiv> Inf

   778 Inter \<equiv> Inf

   781 \<dots>"}

   779 \<dots>"}

   783   The precise output of course depends on the abbreviations that are

   781   The precise output of course depends on the abbreviations that are

   784   currently defined; this can change over time.

   782   currently defined; this can change over time.

   785   You can also use antiquotations to refer to proved theorems: 

   783   You can also use antiquotations to refer to proved theorems: 

   786   \<open>@{thm \<dots>}\<close> for a single theorem

   784   \<open>@{thm \<dots>}\<close> for a single theorem

   787 

   785 

   789 

   787 

   790   and \<open>@{thms \<dots>}\<close> for more than one

   788   and \<open>@{thms \<dots>}\<close> for more than one

   791 

   789 

   793   "@{thms conj_ac}" 

   791   "@{thms conj_ac}" 

   794 "(?P \<and> ?Q) = (?Q \<and> ?P)

   792 "(?P \<and> ?Q) = (?Q \<and> ?P)

   795 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)

   793 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)

   796 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  

   794 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  

   797 

   795 

   798   The thm-antiquotations can also be used for manipulating theorems. For 

   796   The thm-antiquotations can also be used for manipulating theorems. For 

   799   example, if you need the version of the theorem @{thm [source] refl} that 

   797   example, if you need the version of the theorem @{thm [source] refl} that 

   800   has a meta-equality instead of an equality, you can write

   798   has a meta-equality instead of an equality, you can write

   801 

   799 

   803   "@{thm refl[THEN eq_reflection]}"

   801   "@{thm refl[THEN eq_reflection]}"

   804   "?x \<equiv> ?x"}

   802   "?x \<equiv> ?x"}

   805 

   803 

   806   The point of these antiquotations is that referring to theorems in this way

   804   The point of these antiquotations is that referring to theorems in this way

   807   makes your code independent from what theorems the user might have stored

   805   makes your code independent from what theorems the user might have stored

   816 ML %grayML\<open>val foo_thms = @{lemma "True" and "False \<Longrightarrow> P" by simp_all}\<close>

   814 ML %grayML\<open>val foo_thms = @{lemma "True" and "False \<Longrightarrow> P" by simp_all}\<close>

   817 

   815 

   818 text \<open>

   816 text \<open>

   819   The result can be printed out as follows.

   817   The result can be printed out as follows.

   820 

   818 

   822 "foo_thms |> pretty_thms_no_vars @{context}

   820 "foo_thms |> pretty_thms_no_vars @{context}

   823          |> pwriteln"

   821          |> pwriteln"

   824   "True, False \<Longrightarrow> P"}

   822   "True, False \<Longrightarrow> P"}

   825 

   823 

   826   You can also refer to the current simpset via an antiquotation. To illustrate 

   824   You can also refer to the current simpset via an antiquotation. To illustrate 

   840   The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all

   838   The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all

   841   information stored in the simpset, but here we are only interested in the names of the

   839   information stored in the simpset, but here we are only interested in the names of the

   842   simp-rules. Now you can feed in the current simpset into this function. 

   840   simp-rules. Now you can feed in the current simpset into this function. 

   843   The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.

   841   The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.

   844 

   842 

   846   "get_thm_names_from_ss @{context}" 

   844   "get_thm_names_from_ss @{context}" 

   847   "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}

   845   "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}

   848 

   846 

   849   Again, this way of referencing simpsets makes you independent from additions

   847   Again, this way of referencing simpsets makes you independent from additions

   850   of lemmas to the simpset by the user, which can potentially cause loops in your

   848   of lemmas to the simpset by the user, which can potentially cause loops in your

   855   difficult to read. In the next chapter we describe how to construct

   853   difficult to read. In the next chapter we describe how to construct

   856   terms with the (built-in) antiquotation \<open>@{term \<dots>}\<close>.  A restriction

   854   terms with the (built-in) antiquotation \<open>@{term \<dots>}\<close>.  A restriction

   857   of this antiquotation is that it does not allow you to use schematic

   855   of this antiquotation is that it does not allow you to use schematic

   858   variables in terms. If you want to have an antiquotation that does not have

   856   variables in terms. If you want to have an antiquotation that does not have

   859   this restriction, you can implement your own using the function @{ML_ind

   857   this restriction, you can implement your own using the function @{ML_ind

   861   for the antiquotation \<open>term_pat\<close> is as follows.

   859   for the antiquotation \<open>term_pat\<close> is as follows.

   862 \<close>

   860 \<close>

   863 

   861 

   864 ML %linenosgray\<open>val term_pat_setup = 

   862 ML %linenosgray\<open>val term_pat_setup = 

   865 let

   863 let

   884   transformed into a term using the function @{ML_ind read_term_pattern in

   882   transformed into a term using the function @{ML_ind read_term_pattern in

   885   Proof_Context} (Line 5); the next two lines transform the term into a string

   883   Proof_Context} (Line 5); the next two lines transform the term into a string

   886   so that the ML-system can understand it. (All these functions will be explained

   884   so that the ML-system can understand it. (All these functions will be explained

   887   in more detail in later sections.) An example for this antiquotation is:

   885   in more detail in later sections.) An example for this antiquotation is:

   888 

   886 

   890   "@{term_pat \"Suc (?x::nat)\"}"

   888   "@{term_pat \"Suc (?x::nat)\"}"

   891   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}

   889   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}

   892 

   890 

   893   which shows the internal representation of the term \<open>Suc ?x\<close>. Similarly

   891   which shows the internal representation of the term \<open>Suc ?x\<close>. Similarly

   894   we can write an antiquotation for type patterns. Its code is

   892   we can write an antiquotation for type patterns. Its code is

   980 end\<close>

   978 end\<close>

   981 

   979 

   982 text \<open>

   980 text \<open>

   983   The data can be retrieved with the projection functions defined above.

   981   The data can be retrieved with the projection functions defined above.

   984   

   982   

   986 "project_int (nth foo_list 0); 

   984 "project_int (nth foo_list 0); 

   987 project_bool (nth foo_list 1)" 

   985 project_bool (nth foo_list 1)" 

   988 "13

   986 "13

   989 true"}

   987 true"}

   990 

   988 

   991   Notice that we access the integer as an integer and the boolean as

   989   Notice that we access the integer as an integer and the boolean as

   992   a boolean. If we attempt to access the integer as a boolean, then we get 

   990   a boolean. If we attempt to access the integer as a boolean, then we get 

   993   a runtime error. 

   991   a runtime error. 

   994 

   992 

   996 "project_bool (nth foo_list 0)"  

   994 "project_bool (nth foo_list 0)"  

   997 "*** exception Match raised"}

   995 "*** exception Match raised"}

   998 

   996 

   999   This runtime error is the reason why ML is still type-sound despite

   997   This runtime error is the reason why ML is still type-sound despite

  1000   containing a universal type.

   998   containing a universal type.

  1010   You can think of a theory as the ``longterm memory'' of Isabelle (nothing will

  1008   You can think of a theory as the ``longterm memory'' of Isabelle (nothing will

  1011   be deleted from it), and a proof-context as a ``shortterm memory'' (it

  1009   be deleted from it), and a proof-context as a ``shortterm memory'' (it

  1012   changes according to what is needed at the time).

  1010   changes according to what is needed at the time).

  1013 

  1011 

  1014   For theories and proof contexts there are, respectively, the functors 

  1012   For theories and proof contexts there are, respectively, the functors 

  1016   with the data storage. Below we show how to implement a table in which you

  1014   with the data storage. Below we show how to implement a table in which you

  1017   can store theorems and look them up according to a string key. The

  1015   can store theorems and look them up according to a string key. The

  1018   intention in this example is to be able to look up introduction rules for logical

  1016   intention in this example is to be able to look up introduction rules for logical

  1019   connectives. Such a table might be useful in an automatic proof procedure

  1017   connectives. Such a table might be useful in an automatic proof procedure

  1020   and therefore it makes sense to store this data inside a theory.  

  1018   and therefore it makes sense to store this data inside a theory.  

  1022   The code for the table is:

  1020   The code for the table is:

  1023 \<close>

  1021 \<close>

  1024 

  1022 

  1025 ML %linenosgray\<open>structure Data = Theory_Data

  1023 ML %linenosgray\<open>structure Data = Theory_Data

  1026   (type T = thm Symtab.table

  1024   (type T = thm Symtab.table

  1062 text \<open>

  1060 text \<open>

  1063   The use of the command \isacommand{setup} makes sure the table in the 

  1061   The use of the command \isacommand{setup} makes sure the table in the 

  1064   \emph{current} theory is updated (this is explained further in 

  1062   \emph{current} theory is updated (this is explained further in 

  1065   Section~\ref{sec:theories}). The lookup can now be performed as follows.

  1063   Section~\ref{sec:theories}). The lookup can now be performed as follows.

  1066 

  1064 

  1068 "lookup @{theory} \"conj\""

  1066 "lookup @{theory} \"conj\""

  1069 "SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}

  1067 "SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}

  1070 

  1068 

  1071   An important point to note is that these tables (and data in general)

  1069   An important point to note is that these tables (and data in general)

  1072   need to be treated in a purely functional fashion. Although

  1070   need to be treated in a purely functional fashion. Although

  1076 setup %gray \<open>update "conj" @{thm TrueI}\<close>

  1074 setup %gray \<open>update "conj" @{thm TrueI}\<close>

  1077 

  1075 

  1078 text \<open>

  1076 text \<open>

  1079   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}

  1077   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}

  1080   

  1078   

  1082 "lookup @{theory} \"conj\""

  1080 "lookup @{theory} \"conj\""

  1083 "SOME \"True\""}

  1081 "SOME \"True\""}

  1084 

  1082 

  1085   there are no references involved. This is one of the most fundamental

  1083   there are no references involved. This is one of the most fundamental

  1086   coding conventions for programming in Isabelle. References  

  1084   coding conventions for programming in Isabelle. References  

  1098 

  1096 

  1099 text \<open>

  1097 text \<open>

  1100   We initialise the reference with the empty list. Consequently a first 

  1098   We initialise the reference with the empty list. Consequently a first 

  1101   lookup produces @{ML "ref []" in Unsynchronized}.

  1099   lookup produces @{ML "ref []" in Unsynchronized}.

  1102 

  1100 

  1104   "WrongRefData.get @{theory}"

  1102   "WrongRefData.get @{theory}"

  1105   "ref []"}

  1103   "ref []"}

  1106 

  1104 

  1107   For updating the reference we use the following function

  1105   For updating the reference we use the following function

  1108 \<close>

  1106 \<close>

  1120 

  1118 

  1121 text \<open>

  1119 text \<open>

  1122   A lookup in the current theory gives then the expected list 

  1120   A lookup in the current theory gives then the expected list 

  1123   @{ML "ref [1]" in Unsynchronized}.

  1121   @{ML "ref [1]" in Unsynchronized}.

  1124 

  1122 

  1126   "WrongRefData.get @{theory}"

  1124   "WrongRefData.get @{theory}"

  1127   "ref [1]"}

  1125   "ref [1]"}

  1128 

  1126 

  1129   So far everything is as expected. But, the trouble starts if we attempt to

  1127   So far everything is as expected. But, the trouble starts if we attempt to

  1130   backtrack to the ``point'' before the \isacommand{setup}-command. There, we

  1128   backtrack to the ``point'' before the \isacommand{setup}-command. There, we

  1132   reference, Isabelle has no control over it. So it is not empty, but still

  1130   reference, Isabelle has no control over it. So it is not empty, but still

  1133   @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the

  1131   @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the

  1134   \isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in

  1132   \isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in

  1135   Unsynchronized}, but

  1133   Unsynchronized}, but

  1136 

  1134 

  1138   "WrongRefData.get @{theory}"

  1136   "WrongRefData.get @{theory}"

  1139   "ref [1, 1]"}

  1137   "ref [1, 1]"}

  1140 

  1138 

  1141   Now imagine how often you go backwards and forwards in your proof 

  1139   Now imagine how often you go backwards and forwards in your proof 

  1142   scripts.\footnote{The same problem can be triggered in the Jedit GUI by

  1140   scripts.\footnote{The same problem can be triggered in the Jedit GUI by

  1152   directed graphs in @{ML_file "Pure/General/graph.ML"}, and 

  1150   directed graphs in @{ML_file "Pure/General/graph.ML"}, and 

  1153   tables and symtables in @{ML_file "Pure/General/table.ML"}.

  1151   tables and symtables in @{ML_file "Pure/General/table.ML"}.

  1154   \end{readmore}

  1152   \end{readmore}

  1155 

  1153 

  1156   Storing data in a proof context is done in a similar fashion. As mentioned

  1154   Storing data in a proof context is done in a similar fashion. As mentioned

  1158   following code we can store a list of terms in a proof context.

  1156   following code we can store a list of terms in a proof context.

  1159 \<close>

  1157 \<close>

  1160 

  1158 

  1161 ML %grayML\<open>structure Data = Proof_Data

  1159 ML %grayML\<open>structure Data = Proof_Data

  1162   (type T = term list

  1160   (type T = term list

  1179 

  1177 

  1180 text \<open>

  1178 text \<open>

  1181   Next we start with the context generated by the antiquotation 

  1179   Next we start with the context generated by the antiquotation 

  1182   \<open>@{context}\<close> and update it in various ways. 

  1180   \<open>@{context}\<close> and update it in various ways. 

  1183 

  1181 

  1185 "let

  1183 "let

  1186   val ctxt0 = @{context}

  1184   val ctxt0 = @{context}

  1187   val ctxt1 = ctxt0 |> update @{term \"False\"}

  1185   val ctxt1 = ctxt0 |> update @{term \"False\"}

  1188                     |> update @{term \"True \<and> True\"} 

  1186                     |> update @{term \"True \<and> True\"} 

  1189   val ctxt2 = ctxt0 |> update @{term \"1::nat\"}

  1187   val ctxt2 = ctxt0 |> update @{term \"1::nat\"}

  1222 text \<open>

  1220 text \<open>

  1223   \footnote{\bf FIXME: say more about generic contexts.}

  1221   \footnote{\bf FIXME: say more about generic contexts.}

  1224 

  1222 

  1225   There are two special instances of the data storage mechanism described 

  1223   There are two special instances of the data storage mechanism described 

  1226   above. The first instance implements named theorem lists using the functor

  1224   above. The first instance implements named theorem lists using the functor

  1228   is such a common task.  To obtain a named theorem list, you just declare

  1226   is such a common task.  To obtain a named theorem list, you just declare

  1229 \<close>

  1227 \<close>

  1230 

  1228 

  1231 ML %grayML\<open>structure FooRules = Named_Thms

  1229 ML %grayML\<open>structure FooRules = Named_Thms

  1232   (val name = @{binding "foo"} 

  1230   (val name = @{binding "foo"} 

  1233    val description = "Theorems for foo")\<close>

  1231    val description = "Theorems for foo")\<close>

  1234 

  1232 

  1235 text \<open>

  1233 text \<open>

  1237 \<close>

  1235 \<close>

  1238 

  1236 

  1239 setup %gray \<open>FooRules.setup\<close>

  1237 setup %gray \<open>FooRules.setup\<close>

  1240 

  1238 

  1241 text \<open>

  1239 text \<open>

  1271 

  1269 

  1272 text \<open>

  1270 text \<open>

  1273   The rules in the list can be retrieved using the function 

  1271   The rules in the list can be retrieved using the function 

  1274   @{ML FooRules.get}:

  1272   @{ML FooRules.get}:

  1275 

  1273 

  1277   "FooRules.get @{context}" 

  1275   "FooRules.get @{context}" 

  1278   "[\"True\", \"?C\",\"?B\"]"}

  1276   "[\"True\", \"?C\",\"?B\"]"}

  1279 

  1277 

  1280   Note that this function takes a proof context as argument. This might be 

  1278   Note that this function takes a proof context as argument. This might be 

  1281   confusing, since the theorem list is stored as theory data. It becomes clear by knowing

  1279   confusing, since the theorem list is stored as theory data. It becomes clear by knowing

  1308 

  1306 

  1309 text \<open>

  1307 text \<open>

  1310   On the ML-level these values can be retrieved using the 

  1308   On the ML-level these values can be retrieved using the 

  1311   function @{ML_ind get in Config} from a proof context

  1309   function @{ML_ind get in Config} from a proof context

  1312 

  1310 

  1314   "Config.get @{context} bval" 

  1312   "Config.get @{context} bval" 

  1315   "true"}

  1313   "true"}

  1316 

  1314 

  1317   or directly from a theory using the function @{ML_ind get_global in Config}

  1315   or directly from a theory using the function @{ML_ind get_global in Config}

  1318 

  1316 

  1320   "Config.get_global @{theory} bval" 

  1318   "Config.get_global @{theory} bval" 

  1321   "true"}

  1319   "true"}

  1322 

  1320 

  1323   It is also possible to manipulate the configuration values

  1321   It is also possible to manipulate the configuration values

  1324   from the ML-level with the functions @{ML_ind put in Config}

  1322   from the ML-level with the functions @{ML_ind put in Config}

  1325   and @{ML_ind put_global in Config}. For example

  1323   and @{ML_ind put_global in Config}. For example

  1326 

  1324 

  1328   "let

  1326   "let

  1329   val ctxt = @{context}

  1327   val ctxt = @{context}

  1330   val ctxt' = Config.put sval \"foo\" ctxt

  1328   val ctxt' = Config.put sval \"foo\" ctxt

  1331   val ctxt'' = Config.put sval \"bar\" ctxt'

  1329   val ctxt'' = Config.put sval \"bar\" ctxt'

  1332 in

  1330 in