--- 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 \<dots>}"}
+ Terms of Isabelle can be constructed on the ML-level using the @{text "@{term \<dots>}"}
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 + \<dots> + t\<^isub>n"}
+ and returns the reversed sum @{text "t\<^isub>n + \<dots> + 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 + \<dots> + t\<^isub>n"}
- and returns the reversed sum @{text "t\<^isub>n + \<dots> + 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 \<dots>}"} 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 "(\<And>(x::nat). P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"} can be proved like
+*}
+
+ lemma
+ assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> 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 "\<And>(x::nat). P x \<Longrightarrow> Q x"}
+ val assm2 = cterm_of thy @{prop "((P::nat\<Rightarrow>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 {*