diff -r 3ddf6c832c61 -r df09e49b19bf CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Wed Sep 17 19:20:06 2008 -0400 +++ b/CookBook/FirstSteps.thy Wed Sep 17 19:20:37 2008 -0400 @@ -26,8 +26,7 @@ text {* - Isabelle programming is done in Standard ML, however ML-code for Isabelle often - includes antiquotations to refer to the logical context of Isabelle. + Isabelle programming is done in Standard ML. Just like lemmas and proofs, code in Isabelle is part of a theory. If you want to follow the code written in this chapter, we assume you are working inside the theory defined by @@ -53,16 +52,39 @@ The expression inside \isacommand{ML} commands is immediately evaluated, like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of your Isabelle environment. The code inside the \isacommand{ML} command - can also contain value- and function bindings, on which the undo operation - does not have any effect. + can also contain value- and function bindings. However on such ML-commands the + undo operation behaves slightly counter-intuitive, because if you define +*} + +ML {* + val foo = true *} +text {* + then Isabelle's undo operation has no effect on the definition of + @{ML "foo"}. + + During coding you might find it necessary to quickly inspect some data + in your code. This can be done in a ``quick-and-dirty'' fashion using + @{ML "warning"}. For example +*} + +ML {* + val _ = warning "any string" +*} + +text {* + will print out the string inside the response buffer of Isabelle. +*} + + + section {* Antiquotations *} text {* - The main advantage of embedding all code in a theory is that the - code can contain references to entities that are defined on the - logical level of Isabelle. This is done using antiquotations. + The main advantage of embedding all code + in a theory is that the code can contain references to entities defined + on the logical level of Isabelle. This is done using antiquotations. For example, one can print out the name of the current theory by typing *} @@ -75,7 +97,7 @@ The name of this theory can be extrated using a the function @{ML "Context.theory_name"}. So the code above returns the string @{ML "\"CookBook\""}. - Note that antiquotations are statically scoped, that is the value is + Note, however, that antiquotations are statically scoped, that is the value is determined at ``compile-time'' not ``run-time''. For example the function *} @@ -93,6 +115,13 @@ some data structure and return it. Instead, it is literally replaced with the value representing the theory name. + In a similar way you can use antiquotations to refer to types and theorems: +*} + +ML {* @{typ "(int * nat) list"} *} +ML {* @{thm allI} *} + +text {* In the course of this introduction, we will learn more about these antoquotations: they greatly simplify Isabelle programming since one can directly access all kinds of logical elements from ML. @@ -101,46 +130,37 @@ section {* Terms *} text {* - We can simply quote Isabelle terms from ML using the @{text "@{term \}"} + Terms of Isabelle can be constructed on the ML-level using the @{text "@{term \}"} antiquotation: *} ML {* @{term "(a::nat) + b = c"} *} text {* - This shows the term @{term "(a::nat) + b = c"} in the internal - representation with all gory details. Terms are just an ML - datatype, and they are defined in @{ML_file "Pure/term.ML"}. + This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal + representation of this term. This internal represenation is just a + datatype defined in @{ML_file "Pure/term.ML"}. - The representation of terms uses deBruin indices: bound variables - are represented by the constructor @{ML Bound}, and the index refers to - the number of lambdas we have to skip until we hit the lambda that - binds the variable. The names of bound variables are kept at the - abstractions, but they should be treated just as comments. + The internal representation of terms uses the usual deBruin indices mechanism: bound + variables are represented by the constructor @{ML Bound} whose argument refers to + the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that + binds the corresponding variable. However, the names of bound variables are + kept at abstractions for printing purposes, and so should be treated just as comments. See \ichcite{ch:logic} for more details. + (FIXME: Alex why is the reference bolow given. It somehow does not read + with what is written above.) + \begin{readmore} Terms are described in detail in \ichcite{ch:logic}. Their definition and many useful operations can be found in @{ML_file "Pure/term.ML"}. \end{readmore} - In a similar way we can quote types and theorems: -*} - -ML {* @{typ "(int * nat) list"} *} -ML {* @{thm allI} *} - -text {* - In the default setup, types and theorems are printed as strings. -*} - - -text {* Sometimes the internal representation can be surprisingly different from what you see at the user level, because the layer of - parsing/type checking/pretty printing can be quite thick. + parsing/type checking/pretty printing can be quite elaborate. -\begin{exercise} + \begin{exercise} Look at the internal term representation of the following terms, and find out why they are represented like this. @@ -153,38 +173,46 @@ Hint: The third term is already quite big, and the pretty printer may omit parts of it by default. If you want to see all of it, you can use @{ML "print_depth 50"} to set the limit to a value high enough. -\end{exercise} + \end{exercise} + + \begin{exercise} + Write a function @{ML_text "rev_sum : term -> term"} that takes a + term of the form @{text "t\<^isub>1 + t\<^isub>2 + \ + t\<^isub>n"} + and returns the reversed sum @{text "t\<^isub>n + \ + t\<^isub>2 + t\<^isub>1"}. + Note that @{text "+"} associates to the left. + Try your function on some examples, and see if the result typechecks. + \end{exercise} *} -section {* Type checking *} +text {* FIXME: check possible solution *} -text {* - We can freely construct and manipulate terms, since they are just - arbitrary unchecked trees. However, we eventually want to see if a - term is wellformed in a certain context. +ML {* + exception FORM_ERROR - Type checking is done via @{ML cterm_of}, which turns a @{ML_type - term} into a @{ML_type cterm}, a \emph{certified} term. Unlike - @{ML_type term}s, which are just trees, @{ML_type - "cterm"}s are abstract objects that are guaranteed to be - type-correct, and can only be constructed via the official - interfaces. - - Type - checking is always relative to a theory context. For now we can use - the @{ML "@{theory}"} antiquotation to get hold of the theory at the current - point: + fun rev_sum term = + case term of + @{term "op +"} $ (Free (x,t1)) $ (Free (y,t2)) => + @{term "op +"} $ (Free (y,t2)) $ (Free (x,t1)) + | @{term "op +"} $ left $ (Free (x,t)) => + @{term "op +"} $ (Free (x,t)) $ (rev_sum left) + | _ => raise FORM_ERROR *} -ML {* - let - val natT = @{typ "nat"} - val zero = @{term "0::nat"}(*Const ("HOL.zero_class.zero", natT)*) - in - cterm_of @{theory} - (Const ("HOL.plus_class.plus", natT --> natT --> natT) - $ zero $ zero) - end + +text {* + \begin{exercise} + Write a function which takes two terms representing natural numbers + in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary + number representing their sum. + \end{exercise} + + \begin{exercise} + Look at the functions defined in @{ML_file "Pure/logic.ML"} and + @{ML_file "HOL/hologic.ML"} and see if they can make your life + easier. + \end{exercise} + + (FIXME what is coming next should fit with the main flow) *} ML {* @@ -204,27 +232,37 @@ another antiquotation: @{ML "@{const_name plus}"} gives just this name. - \begin{exercise} - Write a function @{ML_text "rev_sum : term -> term"} that takes a - term of the form @{text "t\<^isub>1 + t\<^isub>2 + \ + t\<^isub>n"} - and returns the reversed sum @{text "t\<^isub>n + \ + t\<^isub>2 + t\<^isub>1"}. - Note that @{text "+"} associates to the left. - Try your function on some examples, and see if the result typechecks. - \end{exercise} + FIXME: maybe explain @{text "@{prop \}"} as a special kind of terms +*} + +ML {* @{prop "True"} *} + + + + +section {* Type checking *} + +text {* + We can freely construct and manipulate terms, since they are just + arbitrary unchecked trees. However, we eventually want to see if a + term is wellformed, or type checks, relative to a theory. - \begin{exercise} - Write a function which takes two terms representing natural numbers - in unary (like @{term "Suc (Suc (Suc 0))"}), and produce the unary - number representing their sum. - \end{exercise} + Type checking is done via the function @{ML cterm_of}, which turns + a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term. + Unlike @{ML_type term}s, which are just trees, @{ML_type + "cterm"}s are abstract objects that are guaranteed to be + type-correct, and can only be constructed via the official + interfaces. - \begin{exercise} - Look at the functions defined in @{ML_file "Pure/logic.ML"} and - @{ML_file "HOL/hologic.ML"} and see if they can make your life - easier. - \end{exercise} + (FIXME: Alex what do you mean concretely by ``official interfaces'') + + Type checking is always relative to a theory context. For now we can use + the @{ML "@{theory}"} antiquotation to get hold of the current theory. + For example we can write: *} +ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *} + section {* Theorems *} text {* @@ -236,10 +274,22 @@ Using these rules, which are just ML functions, you can do simple natural deduction proofs on the ML level. For example, the statement - @{prop "(\(x::nat). P x \ Q x) \ P t \ Q t"} can be proved like +*} + + lemma + assumes assm\<^isub>1: "\(x::nat). P x \ Q x" + and assm\<^isub>2: "P t" + shows "Q t" + (*<*)oops(*>*) + +text {* + can be proved in ML like this\footnote{Note that @{text "|>"} is just reverse application. This combinator, and several variants are defined in @{ML_file "Pure/General/basics.ML"}}: + + + (FIXME: Alex why did you not use antiquotations for this?) *} ML {* @@ -271,6 +321,33 @@ end *} +ML {* + +let + val thy = @{theory} + + val assm1 = cterm_of thy @{prop "\(x::nat). P x \ Q x"} + val assm2 = cterm_of thy @{prop "((P::nat\bool) t)"} + + val Pt_implies_Qt = + assume assm1 + |> forall_elim (cterm_of thy @{term "t::nat"}); + + val Qt = implies_elim Pt_implies_Qt (assume assm2); +in + + Qt + |> implies_intr assm2 + |> implies_intr assm1 +end + +*} + +text {* + FIXME Explain this program more carefully +*} + + section {* Tactical reasoning *} text {*