1 theory FirstSteps

     1 theory FirstSteps

     2 imports Base

     2 imports Base

     3 begin

     3 begin

     4 

     4 

     5 chapter {* First Steps *}

     5 chapter {* First Steps *}

     6 

     7 

     7 text {*

     8 text {*

     8   Isabelle programming is done in ML. Just like lemmas and proofs, ML-code

     9   Isabelle programming is done in ML. Just like lemmas and proofs, ML-code

     9   in Isabelle is part of a theory. If you want to follow the code given in

    10   in Isabelle is part of a theory. If you want to follow the code given in

    10   this chapter, we assume you are working inside the theory starting with

    11   this chapter, we assume you are working inside the theory starting with

   108 

   109 

   109 text {*

   110 text {*

   110 

   111 

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

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

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

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

   114 

   115 

   115   @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}

   116   @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}

   116 

   117 

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

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

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

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

   714   writeln (Syntax.string_of_term @{context} omega)

   715   writeln (Syntax.string_of_term @{context} omega)

   715 end"

   716 end"

   716   "x x"}

   717   "x x"}

   717 

   718 

   718   with the raw ML-constructors.

   719   with the raw ML-constructors.

   719   Sometimes the internal representation of terms can be surprisingly different

   721   Sometimes the internal representation of terms can be surprisingly different

   720   from what you see at the user-level, because the layers of

   722   from what you see at the user-level, because the layers of

   721   parsing/type-checking/pretty printing can be quite elaborate. 

   723   parsing/type-checking/pretty printing can be quite elaborate. 

   722 

   724 

   723   \begin{exercise}

   725   \begin{exercise}

   779   definition and many useful operations are implemented 

   781   definition and many useful operations are implemented 

   780   in @{ML_file "Pure/type.ML"}.

   782   in @{ML_file "Pure/type.ML"}.

   781   \end{readmore}

   783   \end{readmore}

   782 *}

   784 *}

   783 

   785 

   785 

   787 

   786 text {*

   788 text {*

   787   While antiquotations are very convenient for constructing terms, they can

   789   While antiquotations are very convenient for constructing terms, they can

   788   only construct fixed terms (remember they are ``linked'' at compile-time).

   790   only construct fixed terms (remember they are ``linked'' at compile-time).

   789   However, you often need to construct terms dynamically. For example, a

   791   However, you often need to construct terms dynamically. For example, a

   874 

   876 

   875   @{ML_response_fake [display, gray]

   877   @{ML_response_fake [display, gray]

   876   "subst_free [(@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})] 

   878   "subst_free [(@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})] 

   877   @{term \"(\<lambda>x::nat. x)\"}"

   879   @{term \"(\<lambda>x::nat. x)\"}"

   878   "Free (\"x\", \"nat\")"}

   880   "Free (\"x\", \"nat\")"}

   879 

   891 

   880   \begin{readmore}

   892   \begin{readmore}

   881   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and

   893   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and

   882   @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 

   894   @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms 

   883   and types easier.\end{readmore}

   895   and types easier.\end{readmore}

   895   \begin{exercise}\label{fun:makesum}

   907   \begin{exercise}\label{fun:makesum}

   896   Write a function which takes two terms representing natural numbers

   908   Write a function which takes two terms representing natural numbers

   897   in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the

   909   in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the

   898   number representing their sum.

   910   number representing their sum.

   899   \end{exercise}

   911   \end{exercise}

   901   There are a few subtle issues with constants. They usually crop up when

   917   There are a few subtle issues with constants. They usually crop up when

   902   pattern matching terms or types, or when constructing them. While it is perfectly ok

   918   pattern matching terms or types, or when constructing them. While it is perfectly ok

   903   to write the function @{text is_true} as follows

   919   to write the function @{text is_true} as follows

   904 *}

   920 *}

   905 

   921 

  1001 

  1017 

  1002   \begin{readmore}

  1018   \begin{readmore}

  1003   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};

  1019   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};

  1004   functions about signatures in @{ML_file "Pure/sign.ML"}.

  1020   functions about signatures in @{ML_file "Pure/sign.ML"}.

  1005   \end{readmore}

  1021   \end{readmore}

  1007   Although types of terms can often be inferred, there are many

  1027   Although types of terms can often be inferred, there are many

  1008   situations where you need to construct types manually, especially  

  1028   situations where you need to construct types manually, especially  

  1009   when defining constants. For example the function returning a function 

  1029   when defining constants. For example the function returning a function 

  1010   type is as follows:

  1030   type is as follows:

  1011 

  1031 

  1014 ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}

  1034 ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}

  1015 

  1035 

  1016 text {* This can be equally written with the combinator @{ML "-->"} as: *}

  1036 text {* This can be equally written with the combinator @{ML "-->"} as: *}

  1017 

  1037 

  1018 ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}

  1038 ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}

  1019 

  1046 

  1020 text {*

  1047 text {*

  1021   A handy function for manipulating terms is @{ML map_types}: it takes a 

  1048   A handy function for manipulating terms is @{ML map_types}: it takes a 

  1022   function and applies it to every type in a term. You can, for example,

  1049   function and applies it to every type in a term. You can, for example,

  1023   change every @{typ nat} in a term into an @{typ int} using the function:

  1050   change every @{typ nat} in a term into an @{typ int} using the function:

  1549   \emph{not} the received way of doing such things. The received way is to 

  1576   \emph{not} the received way of doing such things. The received way is to 

  1550   start a ``data slot'', below called @{text MyThmsData}, generated by the functor 

  1577   start a ``data slot'', below called @{text MyThmsData}, generated by the functor 

  1551   @{text GenericDataFun}:

  1578   @{text GenericDataFun}:

  1552 *}

  1579 *}

  1553 

  1580 

  1555  (type T = thm list

  1582  (type T = thm list

  1556   val empty = []

  1583   val empty = []

  1557   val extend = I

  1584   val extend = I

  1558   fun merge _ = Thm.merge_thms) *}

  1585   fun merge _ = Thm.merge_thms) *}

  1559 

  1586