66 

    66 

    67   During development you might find it necessary to inspect some data

    67   During development you might find it necessary to inspect some data

    68   in your code. This can be done in a ``quick-and-dirty'' fashion using 

    68   in your code. This can be done in a ``quick-and-dirty'' fashion using 

    69   the function @{ML "warning"}. For example 

    69   the function @{ML "warning"}. For example 

    70 

    70 

    72 

    72 

    73   will print out @{text [quotes] "any string"} inside the response buffer

    73   will print out @{text [quotes] "any string"} inside the response buffer

    74   of Isabelle.  This function expects a string as argument. If you develop under PolyML,

    74   of Isabelle.  This function expects a string as argument. If you develop under PolyML,

    75   then there is a convenient, though again ``quick-and-dirty'', method for

    75   then there is a convenient, though again ``quick-and-dirty'', method for

    76   converting values into strings, namely @{ML makestring}:

    76   converting values into strings, namely @{ML makestring}:

    77 

    77 

    79 

    79 

    80   However @{ML makestring} only works if the type of what is converted is monomorphic 

    80   However @{ML makestring} only works if the type of what is converted is monomorphic 

    81   and is not a function.

    81   and is not a function.

    82 

    82 

    83   The function @{ML "warning"} should only be used for testing purposes, because any

    83   The function @{ML "warning"} should only be used for testing purposes, because any

    84   output this function generates will be overwritten as soon as an error is

    84   output this function generates will be overwritten as soon as an error is

    85   raised. For printing anything more serious and elaborate, the

    85   raised. For printing anything more serious and elaborate, the

    86   function @{ML tracing} is more appropriate. This function writes all output into

    86   function @{ML tracing} is more appropriate. This function writes all output into

    87   a separate tracing buffer. For example

    87   a separate tracing buffer. For example

    88 

    88 

    90 

    90 

    91   It is also possible to redirect the ``channel'' where the string @{text "foo"} is 

    91   It is also possible to redirect the ``channel'' where the string @{text "foo"} is 

    92   printed to a separate file, e.g. to prevent ProofGeneral from choking on massive 

    92   printed to a separate file, e.g. to prevent ProofGeneral from choking on massive 

    93   amounts of trace output. This redirection can be achieved using the code

    93   amounts of trace output. This redirection can be achieved using the code

    94 *}

    94 *}

   105     (TextIO.output (stream, (strip_specials s));

   105     (TextIO.output (stream, (strip_specials s));

   106      TextIO.output (stream, "\n");

   106      TextIO.output (stream, "\n");

   107      TextIO.flushOut stream)) *}

   107      TextIO.flushOut stream)) *}

   108 

   108 

   109 text {*

   109 text {*

   111   Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 

   110   Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} 

   112   will cause that all tracing information is printed into the file @{text "foo.bar"}.

   111   will cause that all tracing information is printed into the file @{text "foo.bar"}.

   114 *}

   112 *}

   115 

   113 

   116 

   114 

   117 section {* Antiquotations *}

   115 section {* Antiquotations *}

   118 

   116 

   122   this we mean definitions, theorems, terms and so on. This kind of reference is

   120   this we mean definitions, theorems, terms and so on. This kind of reference is

   123   realised with antiquotations.  For example, one can print out the name of the current

   121   realised with antiquotations.  For example, one can print out the name of the current

   124   theory by typing

   122   theory by typing

   125 

   123 

   126   

   124   

   128  

   126  

   129   where @{text "@{theory}"} is an antiquotation that is substituted with the

   127   where @{text "@{theory}"} is an antiquotation that is substituted with the

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

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

   131   @{text FirstSteps}). The name of this theory can be extracted with

   129   @{text FirstSteps}). The name of this theory can be extracted with

   132   the function @{ML "Context.theory_name"}. 

   130   the function @{ML "Context.theory_name"}. 

   147   some data structure and return it. Instead, it is literally

   145   some data structure and return it. Instead, it is literally

   148   replaced with the value representing the theory name.

   146   replaced with the value representing the theory name.

   149 

   147 

   150   In a similar way you can use antiquotations to refer to theorems or simpsets:

   148   In a similar way you can use antiquotations to refer to theorems or simpsets:

   151 

   149 

   154 "let

   152 "let

   155   val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset}

   153   val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset}

   156 in

   154 in

   157   map #name (Net.entries rules)

   155   map #name (Net.entries rules)

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

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

   184 

   182 

   185 text {*

   183 text {*

   186   One way to construct terms of Isabelle on the ML-level is by using the antiquotation 

   184   One way to construct terms of Isabelle on the ML-level is by using the antiquotation 

   187   \mbox{@{text "@{term \<dots>}"}}. For example

   185   \mbox{@{text "@{term \<dots>}"}}. For example

   188 

   186 

   190     "@{term \"(a::nat) + b = c\"}" 

   188     "@{term \"(a::nat) + b = c\"}" 

   191     "Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}

   189     "Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}

   192 

   190 

   193   This will show the term @{term "(a::nat) + b = c"}, but printed using the internal

   191   This will show the term @{term "(a::nat) + b = c"}, but printed using the internal

   194   representation of this term. This internal representation corresponds to the 

   192   representation of this term. This internal representation corresponds to the 

   221 

   219 

   222   Hint: The third term is already quite big, and the pretty printer

   220   Hint: The third term is already quite big, and the pretty printer

   223   may omit parts of it by default. If you want to see all of it, you

   221   may omit parts of it by default. If you want to see all of it, you

   224   can use the following ML function to set the limit to a value high 

   222   can use the following ML function to set the limit to a value high 

   225   enough:

   223   enough:

   226   \end{exercise}

   226   \end{exercise}

   229 

   227 

   230   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 

   228   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 

   231   inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 

   229   inserting the invisible @{text "Trueprop"}-coercions whenever necessary. 

   232   Consider for example the pairs

   230   Consider for example the pairs

   233 

   231 

   235  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}

   233  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}

   236  

   234  

   237   where an coercion is inserted in the second component and 

   235   where an coercion is inserted in the second component and 

   238 

   236 

   240   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}

   238   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}

   241 

   239 

   243 

   241 

   244   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example

   242   Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example

   245 

   243 

   247 

   245 

   248   \begin{readmore}

   246   \begin{readmore}

   249   Types are described in detail in \isccite{sec:types}. Their

   247   Types are described in detail in \isccite{sec:types}. Their

   250   definition and many useful operations can also be found in @{ML_file "Pure/type.ML"}.

   248   definition and many useful operations can also be found in @{ML_file "Pure/type.ML"}.

   251   \end{readmore}

   249   \end{readmore}

   281 text {*

   279 text {*

   282   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 

   280   To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} 

   283   to both functions. With @{ML make_imp} we obtain the correct term involving 

   281   to both functions. With @{ML make_imp} we obtain the correct term involving 

   284   @{term "S"}, @{text "T"} and  @{text "@{typ nat}"} 

   282   @{term "S"}, @{text "T"} and  @{text "@{typ nat}"} 

   285 

   283 

   287     "Const \<dots> $ 

   285     "Const \<dots> $ 

   288     Abs (\"x\", Type (\"nat\",[]),

   286     Abs (\"x\", Type (\"nat\",[]),

   289       Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ 

   287       Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ 

   290                   (Free (\"T\",\<dots>) $ \<dots>))"}

   288                   (Free (\"T\",\<dots>) $ \<dots>))"}

   291 

   289 

   292   With @{ML make_wrong_imp} we obtain an incorrect term involving the @{term "P"} 

   290   With @{ML make_wrong_imp} we obtain an incorrect term involving the @{term "P"} 

   293   and @{text "Q"} from the antiquotation.

   291   and @{text "Q"} from the antiquotation.

   294 

   292 

   296     "Const \<dots> $ 

   294     "Const \<dots> $ 

   297     Abs (\"x\", \<dots>,

   295     Abs (\"x\", \<dots>,

   298       Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 

   296       Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 

   299                   (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}

   297                   (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}

   300 

   298 

   312   "HOL"} indicates in which theory they are defined. Guessing such internal

   310   "HOL"} indicates in which theory they are defined. Guessing such internal

   313   names can sometimes be quite hard. Therefore Isabelle provides the

   311   names can sometimes be quite hard. Therefore Isabelle provides the

   314   antiquotation @{text "@{const_name \<dots>}"} which does the expansion

   312   antiquotation @{text "@{const_name \<dots>}"} which does the expansion

   315   automatically, for example:

   313   automatically, for example:

   316 

   314 

   318 

   316 

   319   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)

   317   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)

   320 

   318 

   321   Similarly, types can be constructed manually, for example as follows:

   319   Similarly, types can be constructed manually, for example as follows:

   322 

   320 

   375 

   373 

   376   Type-checking is always relative to a theory context. For now we use

   374   Type-checking is always relative to a theory context. For now we use

   377   the @{ML "@{theory}"} antiquotation to get hold of the current theory.

   375   the @{ML "@{theory}"} antiquotation to get hold of the current theory.

   378   For example we can write

   376   For example we can write

   379 

   377 

   381 

   379 

   382   or use the antiquotation

   380   or use the antiquotation

   383 

   381 

   385 

   383 

   386   Attempting

   384   Attempting

   387 

   385 

   389 

   387 

   390   yields an error. A slightly more elaborate example is

   388   yields an error. A slightly more elaborate example is

   391 

   389 

   393 "let

   391 "let

   394   val natT = @{typ \"nat\"}

   392   val natT = @{typ \"nat\"}

   395   val zero = @{term \"0::nat\"}

   393   val zero = @{term \"0::nat\"}

   396 in

   394 in

   397   cterm_of @{theory} 

   395   cterm_of @{theory} 

   424 text {*

   422 text {*

   425   on the ML-level:\footnote{Note that @{text "|>"} is reverse

   423   on the ML-level:\footnote{Note that @{text "|>"} is reverse

   426   application. This combinator, and several variants are defined in

   424   application. This combinator, and several variants are defined in

   427   @{ML_file "Pure/General/basics.ML"}.}

   425   @{ML_file "Pure/General/basics.ML"}.}

   428 

   426 

   430 "let

   428 "let

   431   val thy = @{theory}

   429   val thy = @{theory}

   432 

   430 

   433   val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}

   431   val assm1 = cterm_of thy @{prop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}

   434   val assm2 = cterm_of thy @{prop \"(P::nat\<Rightarrow>bool) t\"}

   432   val assm2 = cterm_of thy @{prop \"(P::nat\<Rightarrow>bool) t\"}

   495   file is most code for dealing with goals?)

   493   file is most code for dealing with goals?)

   496   \end{readmore}

   494   \end{readmore}

   497 

   495 

   498   Tactics are functions that map a goal state to a (lazy)

   496   Tactics are functions that map a goal state to a (lazy)

   499   sequence of successor states, hence the type of a tactic is

   497   sequence of successor states, hence the type of a tactic is

   500   @{ML_type[display] "thm -> thm Seq.seq"}

   499   @{ML_type[display] "thm -> thm Seq.seq"}

   501   

   500   

   502   \begin{readmore}

   501   \begin{readmore}

   503   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy

   502   See @{ML_file "Pure/General/seq.ML"} for the implementation of lazy

   504   sequences. However in day-to-day Isabelle programming, one rarely 

   503   sequences. However in day-to-day Isabelle programming, one rarely 

   529   (empty in the proof at hand) 

   528   (empty in the proof at hand) 

   530   with the variables @{text xs} that will be generalised once the

   529   with the variables @{text xs} that will be generalised once the

   531   goal is proved. The @{text "tac"} is the tactic which proves the goal and which 

   530   goal is proved. The @{text "tac"} is the tactic which proves the goal and which 

   532   can make use of the local assumptions (there are none in this example).

   531   can make use of the local assumptions (there are none in this example).

   533 

   532 

   535 "let

   534 "let

   536   val ctxt = @{context}

   535   val ctxt = @{context}

   537   val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}

   536   val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}

   538 in

   537 in

   539   Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ => 

   538   Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ => 

   550   \end{readmore}

   549   \end{readmore}

   551 

   550 

   552 

   551 

   553   An alternative way to transcribe this proof is as follows 

   552   An alternative way to transcribe this proof is as follows 

   554 

   553 

   556 "let

   555 "let

   557   val ctxt = @{context}

   556   val ctxt = @{context}

   558   val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}

   557   val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}

   559 in

   558 in

   560   Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ => 

   559   Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ =>