29   Isabelle programming is done in Standard ML, however ML-code for Isabelle often

    29   Isabelle programming is done in Standard ML.

    30   includes antiquotations to refer to the logical context of Isabelle. 

    56   can also contain value- and function bindings, on which the undo operation 

    55   can also contain value- and function bindings. However on such ML-commands the 

    57   does not have any effect. 

    56   undo operation behaves slightly counter-intuitive, because if you define

    58 *}

    57 *}

    58 

    59 ML {*

    60   val foo = true

    61 *}

    62 

    63 text {*

    64   then Isabelle's undo operation has no effect on the definition of 

    65   @{ML "foo"}. 

    66 

    67   During coding you might find it necessary to quickly inspect some data

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

    69   @{ML "warning"}. For example

    70 *}

    71 

    72 ML {*

    73   val _ = warning "any string"

    74 *}

    75 

    76 text {*

    77   will print out the string inside the response buffer of Isabelle.

    78 *}

    79 

    80 

    63   The main advantage of embedding all code in a theory is that the

    85   The main advantage of embedding all code 

    64   code can contain references to entities that are defined on the

    86   in a theory is that the code can contain references to entities defined 

    65   logical level of Isabelle. This is done using antiquotations.

    87   on the logical level of Isabelle. This is done using antiquotations.

    78   Note that antiquotations are statically scoped, that is the value is

   100   Note, however, that antiquotations are statically scoped, that is the value is

   104   We can simply quote Isabelle terms from ML using the @{text "@{term \<dots>}"} 

   133   Terms of Isabelle can be constructed on the ML-level using the @{text "@{term \<dots>}"} 

   111   This shows the term @{term "(a::nat) + b = c"} in the internal

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

   112   representation with all gory details. Terms are just an ML

   141   representation of this term. This internal represenation is just a 

   113   datatype, and they are defined in @{ML_file "Pure/term.ML"}.

   142   datatype defined in @{ML_file "Pure/term.ML"}.

   115   The representation of terms uses deBruin indices: bound variables

   144   The internal representation of terms uses the usual deBruin indices mechanism: bound 

   116   are represented by the constructor @{ML Bound}, and the index refers to

   145   variables are represented by the constructor @{ML Bound} whose argument refers to

   117   the number of lambdas we have to skip until we hit the lambda that

   146   the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that

   118   binds the variable. The names of bound variables are kept at the

   147   binds the corresponding variable. However, the names of bound variables are 

   119   abstractions, but they should be treated just as comments. 

   148   kept at abstractions for printing purposes, and so should be treated just as comments. 

   141   parsing/type checking/pretty printing can be quite thick. 

   161   parsing/type checking/pretty printing can be quite elaborate. 

   142 

   162 

   143 \begin{exercise}

   163   \begin{exercise}

   156 \end{exercise}

   176   \end{exercise}

   157 *}

   177 

   158 

   178   \begin{exercise}

   159 section {* Type checking *}

   179   Write a function @{ML_text "rev_sum : term -> term"} that takes a

   160 

   180   term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"}

   161 text {* 

   181   and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}.

   162   We can freely construct and manipulate terms, since they are just

   182   Note that @{text "+"} associates to the left.

   163   arbitrary unchecked trees. However, we eventually want to see if a

   183   Try your function on some examples, and see if the result typechecks.

   164   term is wellformed in a certain context.

   184   \end{exercise}

   165 

   185 *}

   166   Type checking is done via @{ML cterm_of}, which turns a @{ML_type

   186 

   167   term} into a  @{ML_type cterm}, a \emph{certified} term. Unlike

   187 text {* FIXME: check possible solution *}

   168   @{ML_type term}s, which are just trees, @{ML_type

   188 

   169   "cterm"}s are abstract objects that are guaranteed to be

   189 ML {* 

   170   type-correct, and can only be constructed via the official

   190   exception FORM_ERROR 

   171   interfaces.

   191 

   172 

   192   fun rev_sum term =

   173   Type

   193     case term of

   174   checking is always relative to a theory context. For now we can use

   194        @{term "op +"} $ (Free (x,t1)) $ (Free (y,t2)) => 

   175   the @{ML "@{theory}"} antiquotation to get hold of the theory at the current

   195                    @{term "op +"} $ (Free (y,t2)) $ (Free (x,t1))

   176   point:

   196     |  @{term "op +"} $ left $ (Free (x,t)) => 

   177 *}

   197                    @{term "op +"} $ (Free (x,t)) $ (rev_sum left)

   178 

   198     |  _ => raise FORM_ERROR

   179 ML {*

   199 *}

   180   let

   200 

   181     val natT = @{typ "nat"}

   201 

   182     val zero = @{term "0::nat"}(*Const ("HOL.zero_class.zero", natT)*)

   202 text {*

   183   in

   203   \begin{exercise}

   184     cterm_of @{theory} 

   204   Write a function which takes two terms representing natural numbers

   185         (Const ("HOL.plus_class.plus", natT --> natT --> natT) 

   205   in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary

   186          $ zero $ zero)

   206   number representing their sum.

   187   end

   207   \end{exercise}

   208 

   209   \begin{exercise}

   210   Look at the functions defined in @{ML_file "Pure/logic.ML"} and

   211   @{ML_file "HOL/hologic.ML"} and see if they can make your life

   212   easier.

   213   \end{exercise}

   214 

   215   (FIXME what is coming next should fit with the main flow)

   207   \begin{exercise}

   235   FIXME: maybe explain @{text "@{prop \<dots>}"} as a special kind of terms 

   208   Write a function @{ML_text "rev_sum : term -> term"} that takes a

   236 *}

   209   term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"}

   237 

   210   and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}.

   238 ML {* @{prop "True"} *}

   211   Note that @{text "+"} associates to the left.

   239 

   212   Try your function on some examples, and see if the result typechecks.

   240 

   213   \end{exercise}

   241 

   214 

   242 

   215   \begin{exercise}

   243 section {* Type checking *}

   216   Write a function which takes two terms representing natural numbers

   244 

   217   in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary

   245 text {* 

   218   number representing their sum.

   246   We can freely construct and manipulate terms, since they are just

   219   \end{exercise}

   247   arbitrary unchecked trees. However, we eventually want to see if a

   220 

   248   term is wellformed, or type checks, relative to a theory.

   221   \begin{exercise}

   249 

   222   Look at the functions defined in @{ML_file "Pure/logic.ML"} and

   250   Type checking is done via the function @{ML cterm_of}, which turns 

   223   @{ML_file "HOL/hologic.ML"} and see if they can make your life

   251   a @{ML_type term} into a  @{ML_type cterm}, a \emph{certified} term. 

   224   easier.

   252   Unlike @{ML_type term}s, which are just trees, @{ML_type

   225   \end{exercise}

   253   "cterm"}s are abstract objects that are guaranteed to be

   226 *}

   254   type-correct, and can only be constructed via the official

   255   interfaces.

   256 

   257   (FIXME: Alex what do you mean concretely by ``official interfaces'')

   258 

   259   Type checking is always relative to a theory context. For now we can use

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

   261   For example we can write:

   262 *}

   263 

   264 ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *}

   239   @{prop "(\<And>(x::nat). P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"} can be proved like

   277 *}

   278 

   279   lemma 

   280    assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 

   281    and     assm\<^isub>2: "P t"

   282    shows "Q t"

   283    (*<*)oops(*>*) 

   284 

   285 text {*

   286   can be proved in ML like