--- a/CookBook/FirstSteps.thy Wed Sep 17 19:20:37 2008 -0400
+++ b/CookBook/FirstSteps.thy Tue Sep 30 03:30:40 2008 -0400
@@ -64,9 +64,9 @@
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
+ During developments 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
+ the function @{ML "warning"}. For example
*}
ML {*
@@ -130,26 +130,22 @@
section {* Terms *}
text {*
- Terms of Isabelle can be constructed on the ML-level using the @{text "@{term \<dots>}"}
- antiquotation:
+ One way to construct terms of Isabelle on the ML-level is by using the antiquotation
+ @{text "@{term \<dots>}"}:
*}
ML {* @{term "(a::nat) + b = c"} *}
text {*
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
+ representation of this term. This internal represenation corresponds to the
datatype defined in @{ML_file "Pure/term.ML"}.
- 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 internal representation of terms uses the usual de-Bruijn indices mechanism where bound
+ variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} 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.)
+ kept at abstractions for printing purposes, and so should be treated only as comments.
\begin{readmore}
Terms are described in detail in \ichcite{ch:logic}. Their
@@ -174,45 +170,6 @@
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}
-
- \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}
-*}
-
-text {* FIXME: check possible solution *}
-
-ML {*
- exception FORM_ERROR
-
- 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
-*}
-
-
-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 {*
@@ -239,6 +196,77 @@
+section {* Possible Section on Construting Explicitly Terms *}
+
+text {*
+
+ There is a disadvantage of using the @{text "@{term \<dots>}"} antiquotation
+ directly in order to construct terms.
+*}
+
+ML {*
+
+ val nat = HOLogic.natT
+ val x = Free ("x", nat)
+ val t = Free ("t", nat)
+ val P = Free ("P", nat --> HOLogic.boolT)
+ val Q = Free ("Q", nat --> HOLogic.boolT)
+
+ val A1 = Logic.all x
+ (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
+ HOLogic.mk_Trueprop (Q $ x)))
+
+
+ val A2 = HOLogic.mk_Trueprop (P $ t)
+
+*}
+
+text {*
+
+ \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"} (whereby @{text "i"} might be zero)
+ and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
+ the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
+ associates to the left. Try your function on some examples, and see if
+ the result typechecks. (FIXME: clash with the type-checking section later)
+ \end{exercise}
+*}
+
+ML {*
+ fun rev_sum t =
+ let
+ fun dest_sum (Const (@{const_name plus}, _) $ u $ u') =
+ u' :: dest_sum u
+ | dest_sum u = [u]
+ in
+ foldl1 (HOLogic.mk_binop @{const_name plus}) (dest_sum t)
+ 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}
+
+*}
+
+ML {*
+ fun make_sum t1 t2 =
+ HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2)
+*}
+
+
+text {*
+ \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}
+*}
+
section {* Type checking *}
@@ -288,38 +316,9 @@
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 {*
-let
- val thy = @{theory}
- val nat = HOLogic.natT
- val x = Free ("x", nat)
- val t = Free ("t", nat)
- val P = Free ("P", nat --> HOLogic.boolT)
- val Q = Free ("Q", nat --> HOLogic.boolT)
- val A1 = Logic.all x
- (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
- HOLogic.mk_Trueprop (Q $ x)))
- |> cterm_of thy
-
- val A2 = HOLogic.mk_Trueprop (P $ t)
- |> cterm_of thy
-
- val Pt_implies_Qt =
- assume A1
- |> forall_elim (cterm_of thy t)
-
- val Qt = implies_elim Pt_implies_Qt (assume A2)
-in
- Qt
- |> implies_intr A2
- |> implies_intr A1
-end
-*}
ML {*
@@ -344,7 +343,7 @@
*}
text {*
- FIXME Explain this program more carefully
+ FIXME Explain this program more carefully (@{ML_text assume}, @{ML_text "forall_elim"} \ldots)
*}
@@ -409,6 +408,9 @@
Tactics that affect only a certain subgoal, take a subgoal number as
an integer parameter. Here we always work on the first subgoal,
following exactly the @{text "apply"} script.
+
+ (Fixme: would it make sense to explain THEN' here)
+
*}