Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CookBook/FirstSteps.thy
changeset 15 9da9ba2b095b
parent 14 1c17e99f6f66
child 19 34b93dbf8c3c
equal deleted inserted replaced
14:1c17e99f6f66 15:9da9ba2b095b 
     1 theory FirstSteps
 
     1 theory FirstSteps
 
     2 imports Main
 
     2 imports Main
 
     3 uses "antiquote_setup.ML"
 
     3 uses "antiquote_setup.ML"
 
       
     4      "antiquote_setup_plus.ML"
 
     4 begin
 
     5 begin
 
     5 
     6 
     6 
       
     7 (*<*)
 
       
     8 
       
     9 
       
    10 ML {*
 
       
    11 local structure O = ThyOutput
 
       
    12 in
 
       
    13   fun check_exists f = 
       
    14     if File.exists (Path.explode ("~~/src/" ^ f)) then ()
 
       
    15     else error ("Source file " ^ quote f ^ " does not exist.")
 
       
    16   
       
    17   val _ = O.add_commands
 
       
    18    [("ML_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
 
       
    19          (check_exists name; Pretty.str name))))];
 
       
    20 
       
    21 end
 
       
    22 *}
 
       
    23 (*>*)
 
       
    24 
     7 
    25 chapter {* First Steps *}
 
     8 chapter {* First Steps *}
 
    26 
     9 
    27 
    10 
    28 text {* 
    11 text {* 
    54 
    37 
    55 text {*
 
    38 text {*
 
    56   The expression inside \isacommand{ML} commands is immediately evaluated,
 
    39   The expression inside \isacommand{ML} commands is immediately evaluated,
 
    57   like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of 
    40   like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of 
    58   your Isabelle environment. The code inside the \isacommand{ML} command 
    41   your Isabelle environment. The code inside the \isacommand{ML} command 
    59   can also contain value- and function bindings. However on such ML-commands the 
    42   can also contain value and function bindings. However on such \isacommand{ML}
 
    60   undo operation behaves slightly counter-intuitive, because if you define
 
    43   commands the undo operation behaves slightly counter-intuitive, because 
       
    44   if you define
 
    61 *}
 
    45 *}
 
    62 
    46 
    63 ML {*
 
    47 ML {*
 
    64   val foo = true
 
    48   val foo = true
 
    65 *}
 
    49 *}
 
    67 text {*
 
    51 text {*
 
    68   then Isabelle's undo operation has no effect on the definition of 
    52   then Isabelle's undo operation has no effect on the definition of 
    69   @{ML "foo"}. 
    53   @{ML "foo"}. 
    70 
    54 
    71   Once a portion of code is relatively stable, one usually wants to 
    55   Once a portion of code is relatively stable, one usually wants to 
    72   export it to a separate ML-file. Such files can be included in a 
    56   export it to a separate ML-file. Such files can then be included in a 
    73   theory using @{ML_text "uses"} in the header of the theory.
 
    57   theory by using \isacommand{uses} in the header of the theory, like
 
    74 
    58 
    75   \begin{center}
 
    59   \begin{center}
 
    76   \begin{tabular}{@ {}l}
 
    60   \begin{tabular}{@ {}l}
 
    77   \isacommand{theory} CookBook\\
 
    61   \isacommand{theory} CookBook\\
 
    78   \isacommand{imports} Main\\
 
    62   \isacommand{imports} Main\\
 
    79   \isacommand{uses} @{text "\"file_to_be_included.ML\""}\\
 
    63   \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
 
    80   \isacommand{begin}\\
 
    64   \isacommand{begin}\\
 
    81   \ldots
 
    65   \ldots
 
    82   \end{tabular}
 
    66   \end{tabular}
 
    83   \end{center}
 
    67   \end{center}
 
    84 *}
 
    68 *}
 
   107   a function.
 
    91   a function.
 
   108 *}
 
    92 *}
 
   109 
    93 
   110 text {* 
    94 text {* 
   111   The funtion warning should only be used for testing purposes, because
 
    95   The funtion warning should only be used for testing purposes, because
 
   112   the problem with this function is that any output will be
 
    96   any output this funtion generated will be overwritten, if an error is raised. 
   113   overwritten if an error is raised. For anything more serious 
    97   For printing anything more serious and elaborate, the function @{ML tracing}
 
   114   the function @{ML tracing}, which writes all output in a separate
 
    98   should be used. This function writes all output in a separate buffer.
 
   115   buffer, should be used.
 
       
   116 
       
   117 *}
 
    99 *}
 
   118 
   100 
   119 ML {* tracing "foo" *}
 
   101 ML {* tracing "foo" *}
 
   120 
   102 
   121 text {* (FIXME: complete the comment about redirecting the trace information) 
   103 text {* 
   122 
   104 
   123   In Isabelle it is possible to redirect the message channels to a 
   105   It is also possible to redirect the channel where the @{ML_text "foo"} is 
   124   separate file, e.g. to prevent Proof General from choking on massive 
   106   printed to a separate file, e.g. to prevent Proof General from choking on massive 
   125   amounts of trace output.
 
   107   amounts of trace output. This rediretion can be achieved using the code
 
   126 
   108 
   127 *}
 
   109 *}
 
   128 
   110 
   129 ML {*
 
   111 ML {*
 
   130   val strip_specials =
 
   112   val strip_specials =
 
   137   fun redirect_tracing stream =
 
   119   fun redirect_tracing stream =
 
   138   Output.tracing_fn := (fn s =>
 
   120   Output.tracing_fn := (fn s =>
 
   139     (TextIO.output (stream, (strip_specials s));
 
   121     (TextIO.output (stream, (strip_specials s));
 
   140      TextIO.output (stream, "\n");
 
   122      TextIO.output (stream, "\n");
 
   141      TextIO.flushOut stream));
 
   123      TextIO.flushOut stream));
 
       
   124 *}
 
       
   125 
       
   126 text {* 
       
   127   Calling the @{ML_text "redirect_tracing"} function with @{ML_text "(TextIO.openOut \"foo.bar\")"} 
       
   128   will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
 
       
   129 
   142 *}
 
   130 *}
 
   143 
   131 
   144 
   132 
   145 section {* Antiquotations *}
 
   133 section {* Antiquotations *}
 
   146 
   134 
   189   these antiquotations: they greatly simplify Isabelle programming since one
 
   177   these antiquotations: they greatly simplify Isabelle programming since one
 
   190   can directly access all kinds of logical elements from ML.
 
   178   can directly access all kinds of logical elements from ML.
 
   191 
   179 
   192 *}
 
   180 *}
 
   193 
   181 
   194 section {* Terms *}
 
   182 section {* Terms and Types *}
 
   195 
   183 
   196 text {*
 
   184 text {*
 
   197   One way to construct terms of Isabelle on the ML-level is by using the antiquotation 
   185   One way to construct terms of Isabelle on the ML-level is by using the antiquotation 
   198   @{text "@{term \<dots>}"}:
 
   186   @{text "@{term \<dots>}"}:
 
   199 *}
 
   187 *}
 
   236   may omit parts of it by default. If you want to see all of it, you
 
   224   may omit parts of it by default. If you want to see all of it, you
 
   237   can use the following ML funtion to set the limit to a value high 
   225   can use the following ML funtion to set the limit to a value high 
   238   enough:
 
   226   enough:
 
   239   \end{exercise}
 
   227   \end{exercise}
 
   240 *}
 
   228 *}
 
   241 ML {* print_depth 50 *} 
   229 ML {* print_depth 50 *}
 
   242 
   230 
   243 text {*
 
   231 text {*
 
   244   
   232   
   245   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
   233   The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, 
   246   inserting the invisible @{text "Trueprop"} coercions whenever necessary. 
   234   inserting the invisible @{text "Trueprop"} coercions whenever necessary. 
   248 
   236 
   249 *}
 
   237 *}
 
   250 
   238 
   251 ML {* @{term "P x"} ; @{prop "P x"} *}
 
   239 ML {* @{term "P x"} ; @{prop "P x"} *}
 
   252 
   240 
   253 text {* which needs the coercion and *}
 
   241 text {* which inserts the coercion in the latter ase and *}
 
   254 
   242 
   255 
   243 
   256 ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
 
   244 ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *}
 
   257 
   245 
   258 text {* which does not. *}
 
   246 text {* which does not. *}
 
   259 
   247 
   260 section {* Constructing Terms Manually *} 
   248 text {* (FIXME: add something about @{text "@{typ \<dots>}"}) *}
 
   261 
   249 
   262 text {*
 
   250 section {* Constructing Terms and Types Manually *} 
   263 
   251 
   264   While antiquotations are very convenient for constructing terms, they can
 
   252 text {*
 
   265   only construct fixed terms. Unfortunately, one often needs to construct terms 
   253 
       
   254   While antiquotations are very convenient for constructing terms (similarly types), 
       
   255   they can only construct fixed terms. Unfortunately, one often needs to construct them 
   266   dynamically. For example, a function that returns the implication 
   256   dynamically. For example, a function that returns the implication 
   267   @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as input terms 
   257   @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking @{term P} and @{term Q} as arguments
 
   268   can only be written as
 
   258   can only be written as
 
   269 *}
 
   259 *}
 
   270 
   260 
   271 
   261 
   272 ML {*
 
   262 ML {*
 
   279 *}
 
   269 *}
 
   280 
   270 
   281 text {*
 
   271 text {*
 
   282 
   272 
   283   The reason is that one cannot pass the arguments @{term P} and @{term Q} into 
   273   The reason is that one cannot pass the arguments @{term P} and @{term Q} into 
   284   an antiquotation, like   
   274   an antiquotation. For example this following does not work.
 
   285 *}
 
   275 *}
 
   286 
   276 
   287 ML {*
 
   277 ML {*
 
   288   fun make_imp_wrong P Q = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
   278   fun make_imp_wrong P Q = @{prop "\<And>x. P x \<Longrightarrow> Q x"} 
   289 *}
 
   279 *}
 
   290 
   280 
   291 text {*
 
   281 text {*
 
   292 
   282 
   293   To see the difference apply @{text "@{term S}"} and 
   283   To see this apply @{text "@{term S}"} and @{text "@{term T}"} to boths functions.
 
   294   @{text "@{term T}"} to the functions.
 
   284   
   295   
       
   296 
       
   297   One tricky point in constructing terms by hand is to obtain the fully qualified 
   285   One tricky point in constructing terms by hand is to obtain the fully qualified 
   298   names for constants. For example the names for @{text "zero"} or @{text "+"} are
 
   286   name for constants. For example the names for @{text "zero"} or @{text "+"} are
 
   299   more complex than one first expects, namely @{ML_text "HOL.zero_class.zero"} 
   287   more complex than one first expects, namely 
   300   and @{ML_text "HOL.plus_class.plus"}. The extra prefixes @{ML_text zero_class} 
   288 
   301   and @{ML_text plus_class} are present because these constants are defined 
   289   \begin{center}
 
   302   within type classes; the prefix @{text "HOL"} indicates in which theory they are 
   290   @{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}. 
   303   defined. Guessing such internal names can sometimes be quite hard. Therefore 
   291   \end{center}
 
   304   Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} does the expansion 
   292   
   305   automatically, for example:
 
   293   The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because 
       
   294   these constants are defined within type classes; the prefix @{text "HOL"} indicates in 
       
   295   which theory they are defined. Guessing such internal names can sometimes be quite hard. 
       
   296   Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the 
       
   297   expansion automatically, for example:
 
   306 
   298 
   307 *}
 
   299 *}
 
   308 
   300 
   309 ML {* @{const_name HOL.zero}; @{const_name  plus} *}
 
   301 ML {* @{const_name HOL.zero}; @{const_name  plus} *}
 
   310 
   302 
   326   term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
 
   318   term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
 
   327   and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
 
   319   and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
 
   328   the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
   320   the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"} 
   329   associates to the left. Try your function on some examples. 
   321   associates to the left. Try your function on some examples. 
   330   \end{exercise}
 
   322   \end{exercise}
 
   331 *}
 
   323 
   332 
   324   \begin{exercise}\label{fun:makesum}
 
   333 ML {* 
       
   334   fun rev_sum t =
 
       
   335   let
 
       
   336    fun dest_sum (Const (@{const_name plus}, _) $ u $ u') = 
       
   337                                                       u' :: dest_sum u
 
       
   338      | dest_sum u = [u]
 
       
   339    in
 
       
   340      foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
 
       
   341    end;
 
       
   342 *}
 
       
   343 
       
   344 text {*
 
       
   345   \begin{exercise}
 
       
   346   Write a function which takes two terms representing natural numbers
 
   325   Write a function which takes two terms representing natural numbers
 
   347   in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
 
   326   in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary
 
   348   number representing their sum.
 
   327   number representing their sum.
 
   349   \end{exercise}
 
   328   \end{exercise}
 
   350 
   329 
   351 *}
 
   330 *}
 
   352 
   331 
   353 ML {*
 
       
   354   fun make_sum t1 t2 =
 
       
   355       HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
 
       
   356 *}
 
       
   357 
       
   358 
       
   359 
   332 
   360 section {* Type Checking *}
 
   333 section {* Type Checking *}
 
   361 
   334 
   362 text {* 
   335 text {* 
   363   
   336   
   364   (FIXME: Should we say something about types?)
 
       
   365 
       
   366   We can freely construct and manipulate terms, since they are just
 
   337   We can freely construct and manipulate terms, since they are just
 
   367   arbitrary unchecked trees. However, we eventually want to see if a
 
   338   arbitrary unchecked trees. However, we eventually want to see if a
 
   368   term is well-formed, or type checks, relative to a theory.
 
   339   term is well-formed, or type checks, relative to a theory.
 
   369   Type checking is done via the function @{ML cterm_of}, which turns 
   340   Type checking is done via the function @{ML cterm_of}, which turns 
   370   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 
   341   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term.
isabelle-cookbook