CookBook/FirstSteps.thy
changeset 108 8bea3f74889d
parent 107 258ce361ba1b
child 114 13fd0a83d3c3
equal deleted inserted replaced
107:258ce361ba1b 108:8bea3f74889d
   169 in
   169 in
   170   map #name (Net.entries rules)
   170   map #name (Net.entries rules)
   171 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
   171 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
   172 
   172 
   173   The code about simpsets extracts the theorem names stored in the
   173   The code about simpsets extracts the theorem names stored in the
   174   current simpset.  We get hold of the current simpset with the antiquotation 
   174   current simpset.  You can get hold of the current simpset with the antiquotation 
   175   @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
   175   @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
   176   containing all information about the simpset. The rules of a simpset are
   176   containing all information about the simpset. The rules of a simpset are
   177   stored in a \emph{discrimination net} (a data structure for fast
   177   stored in a \emph{discrimination net} (a data structure for fast
   178   indexing). From this net we can extract the entries using the function @{ML
   178   indexing). From this net you can extract the entries using the function @{ML
   179   Net.entries}.
   179   Net.entries}.
   180 
   180 
   181 
   181 
   182   \begin{readmore}
   182   \begin{readmore}
   183   The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
   183   The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
   256   Consider for example the pairs
   256   Consider for example the pairs
   257 
   257 
   258   @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
   258   @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
   259  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
   259  Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
   260  
   260  
   261   where an coercion is inserted in the second component and 
   261   where a coercion is inserted in the second component and 
   262 
   262 
   263   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
   263   @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
   264   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
   264   "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
   265 
   265 
   266   where it is not (since it is already constructed by a meta-implication). 
   266   where it is not (since it is already constructed by a meta-implication). 
   343 
   343 
   344   @{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"}
   344   @{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"}
   345 
   345 
   346   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
   346   (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
   347 
   347 
   348   Although to some extend types of terms can be inferred, there are many
   348   Although types of terms can often be inferred, there are many
   349   situations where you need to construct types manually, especially  
   349   situations where you need to construct types manually, especially  
   350   when defining constants. For example the function returning a function 
   350   when defining constants. For example the function returning a function 
   351   type is as follows:
   351   type is as follows:
   352 
   352 
   353 *} 
   353 *} 
   385   number representing their sum.
   385   number representing their sum.
   386   \end{exercise}
   386   \end{exercise}
   387 
   387 
   388   A handy function for manipulating terms is @{ML map_types}: it takes a 
   388   A handy function for manipulating terms is @{ML map_types}: it takes a 
   389   function and applies it to every type in the term. You can, for example,
   389   function and applies it to every type in the term. You can, for example,
   390   change every @{typ nat} into an @{typ int} using the function
   390   change every @{typ nat} in a term into an @{typ int} using the function
   391 *}
   391 *}
   392 
   392 
   393 ML{*fun nat_to_int t =
   393 ML{*fun nat_to_int t =
   394   (case t of
   394   (case t of
   395      @{typ nat} => @{typ int}
   395      @{typ nat} => @{typ int}
   409 
   409 
   410 section {* Type-Checking *}
   410 section {* Type-Checking *}
   411 
   411 
   412 text {* 
   412 text {* 
   413   
   413   
   414   You can freely construct and manipulate terms, since they are just
   414   You can freely construct and manipulate @{ML_type "term"}s, since they are just
   415   arbitrary unchecked trees. However, you eventually want to see if a
   415   arbitrary unchecked trees. However, you eventually want to see if a
   416   term is well-formed, or type-checks, relative to a theory.
   416   term is well-formed, or type-checks, relative to a theory.
   417   Type-checking is done via the function @{ML cterm_of}, which converts 
   417   Type-checking is done via the function @{ML cterm_of}, which converts 
   418   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 
   418   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 
   419   Unlike @{ML_type term}s, which are just trees, @{ML_type
   419   Unlike @{ML_type term}s, which are just trees, @{ML_type
   523 
   523 
   524 *}
   524 *}
   525 
   525 
   526 section {* Storing Theorems *}
   526 section {* Storing Theorems *}
   527 
   527 
       
   528 text {* @{ML PureThy.add_thms_dynamic} *}
       
   529 
   528 section {* Theorem Attributes *}
   530 section {* Theorem Attributes *}
   529 
   531 
   530 section {* Printing Terms and Theorems\label{sec:printing} *}
   532 section {* Printing Terms and Theorems\label{sec:printing} *}
   531 
   533 
   532 text {* 
   534 text {* 
   693    #> (fn x => x + 3)*}
   695    #> (fn x => x + 3)*}
   694 
   696 
   695 text {* 
   697 text {* 
   696   which is the function composed of first the increment-by-one function and then
   698   which is the function composed of first the increment-by-one function and then
   697   increment-by-two, followed by increment-by-three. Again, the reverse function 
   699   increment-by-two, followed by increment-by-three. Again, the reverse function 
   698   composition allows one to read the code top-down.
   700   composition allows you to read the code top-down.
   699 
   701 
   700   The remaining combinators described in this section add convenience for the
   702   The remaining combinators described in this section add convenience for the
   701   ``waterfall method'' of writing functions. The combinator @{ML tap} allows
   703   ``waterfall method'' of writing functions. The combinator @{ML tap} allows
   702   one to get hold of an intermediate result (to do some side-calculations for
   704   you to get hold of an intermediate result (to do some side-calculations for
   703   instance). The function
   705   instance). The function
   704 
   706 
   705  *}
   707  *}
   706 
   708 
   707 ML %linenumbers{*fun inc_by_three x =
   709 ML %linenumbers{*fun inc_by_three x =
   708      x |> (fn x => x + 1)
   710      x |> (fn x => x + 1)
   709        |> tap (fn x => tracing (makestring x))
   711        |> tap (fn x => tracing (makestring x))
   710        |> (fn x => x + 2)*}
   712        |> (fn x => x + 2)*}
   711 
   713 
   712 text {* increments the argument first by one and then by two. In the middle (Line 3),
   714 text {* 
   713   however, it uses @{ML tap} for printing the ``plus-one'' intermediate 
   715   increments the argument first by @{text "1"} and then by @{text "2"}. In the
   714   result inside the tracing buffer. The function @{ML tap} can only
   716   middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
   715   be used for side-calculations, because any value that is computed cannot
   717   intermediate result inside the tracing buffer. The function @{ML tap} can
   716   be merged back into the ``main waterfall''. To do this, you can use the next 
   718   only be used for side-calculations, because any value that is computed
   717   combinator.
   719   cannot be merged back into the ``main waterfall''. To do this, you can use
       
   720   the next combinator.
   718 
   721 
   719   The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
   722   The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
   720   and returns the result together with the value (as a pair). For example
   723   and returns the result together with the value (as a pair). For example
   721   the function 
   724   the function 
   722 *}
   725 *}
   750 *}
   753 *}
   751 
   754 
   752 ML{*fun (x, y) |-> f = f x y*}
   755 ML{*fun (x, y) |-> f = f x y*}
   753 
   756 
   754 text {* and can be used to write the following roundabout version 
   757 text {* and can be used to write the following roundabout version 
   755   of the @{text double} function 
   758   of the @{text double} function: 
   756 *}
   759 *}
   757 
   760 
   758 ML{*fun double x =
   761 ML{*fun double x =
   759       x |>  (fn x => (x, x))
   762       x |>  (fn x => (x, x))
   760         |-> (fn x => fn y => x + y)*}
   763         |-> (fn x => fn y => x + y)*}
   762 text {*
   765 text {*
   763   Recall that @{ML "|>"} is the reverse function applications. Recall also that the related 
   766   Recall that @{ML "|>"} is the reverse function applications. Recall also that the related 
   764   reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
   767   reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
   765   @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
   768   @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
   766   composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 
   769   composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, 
   767   for example, the function @{text double} can also be written as
   770   for example, the function @{text double} can also be written as:
   768 *}
   771 *}
   769 
   772 
   770 ML{*val double =
   773 ML{*val double =
   771             (fn x => (x, x))
   774             (fn x => (x, x))
   772         #-> (fn x => fn y => x + y)*}
   775         #-> (fn x => fn y => x + y)*}