--- 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)
+
*}
--- a/CookBook/Intro.thy Wed Sep 17 19:20:37 2008 -0400
+++ b/CookBook/Intro.thy Tue Sep 30 03:30:40 2008 -0400
@@ -7,7 +7,7 @@
text {*
The purpose of this cookbook is to guide the reader through the
- first steps in Isabelle programming, and to provide recipes for
+ first steps of Isabelle programming, and to provide recipes for
solving common problems.
*}
@@ -17,7 +17,7 @@
This cookbook targets an audience who already knows how to use Isabelle
for writing theories and proofs. We also assume that readers are
familiar with the Standard ML, the programming language in which
- most of Isabelle is implemented. If you are unfamiliar with any of
+ most of Isabelle is implemented. If you are unfamiliar with either of
these two subjects, you should first work through the Isabelle/HOL
tutorial \cite{isa-tutorial} and Paulson's book on Standard ML
\cite{paulson-ml2}.
--- a/CookBook/antiquote_setup.ML Wed Sep 17 19:20:37 2008 -0400
+++ b/CookBook/antiquote_setup.ML Tue Sep 30 03:30:40 2008 -0400
@@ -1,5 +1,5 @@
(* Title: Doc/antiquote_setup.ML
- ID: $Id: antiquote_setup.ML,v 1.30 2008/09/16 12:39:56 wenzelm Exp $
+ ID: $Id: antiquote_setup.ML,v 1.32 2008/09/29 10:31:56 haftmann Exp $
Author: Makarius
Auxiliary antiquotations for the Isabelle manuals.
@@ -75,7 +75,7 @@
else txt1 ^ ": " ^ txt2;
val txt' = if kind = "" then txt else kind ^ " " ^ txt;
val _ = writeln (ml (txt1, txt2));
- val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2));
+ val _ = ML_Context.eval_in (SOME ctxt) false Position.none (ml (txt1, txt2));
in
"\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
((if ! O.source then str_of_source src else txt')
@@ -205,7 +205,8 @@
entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" @
entity_antiqs no_check "isatt" "executable" @
entity_antiqs (K check_tool) "isatt" "tool" @
- entity_antiqs (K (File.exists o Path.explode)) "isatt" "file");
+ entity_antiqs (K (File.exists o Path.explode)) "isatt" "file" @
+ entity_antiqs (K ThyInfo.known_thy) "" "theory");
end;
Binary file cookbook.pdf has changed