--- a/ProgTutorial/First_Steps.thy Thu Oct 27 18:11:52 2011 +0100
+++ b/ProgTutorial/First_Steps.thy Sat Oct 29 13:17:12 2011 +0100
@@ -644,34 +644,34 @@
"acc_incs 1 ||>> (fn x => (x, x + 2))"
"(((((\"\", 1), 2), 3), 4), 6)"}
- An example for this combinator is for example the following code
+ A more realistic example for this combinator is the following code
*}
-ML {*
-val (((one_def, two_def), three_def), ctxt') =
+ML{*val (((one_def, two_def), three_def), ctxt') =
@{context}
|> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"})
||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
- ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
-*}
-
-ML {*
- @{context}
- |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})
- ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
- ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
-*}
-
-ML {*
- val ((((One, One_thm), (Two, Two_thm)), (Three, Three_thm)), _)) =
- @{context}
- |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})
- ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
- ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})
-*}
-
+ ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*}
text {*
+ where we make three definitions, namely @{term "one \<equiv> 1::nat"}, @{term "two \<equiv> 2::nat"}
+ and @{term "three \<equiv> 3::nat"}. The point of this code is that we augment the initial
+ context with the definitions. The result we are interested in is the
+ augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing
+ information about the definitions---the function @{ML_ind add_def in Local_Defs} returns
+ both as pairs. We can use this information for example to print out the definiens and
+ the theorem corresponding to the definitions. For example for the first definition:
+
+ @{ML_response_fake [display, gray]
+ "let
+ val (one_trm, one_thm) = one_def
+in
+ pwriteln (pretty_term ctxt' one_trm);
+ pwriteln (pretty_thm ctxt' one_thm)
+end"
+ "one
+one \<equiv> 1"}
+
Recall that @{ML "|>"} is the reverse function application. Recall also that
the related reverse function composition is @{ML "#>"}. In fact all the
combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
@@ -739,13 +739,9 @@
contains further information about combinators.
\end{readmore}
- \footnote{\bf FIXME: find a good exercise for combinators}
\begin{exercise}
Find out what the combinator @{ML "K I"} does.
\end{exercise}
-
-
- \footnote{\bf FIXME: say something about calling conventions}
*}
@@ -901,7 +897,7 @@
To use it you also have to install it using \isacommand{setup} like so
*}
-setup{* term_pat_setup *}
+setup %gray {* term_pat_setup *}
text {*
The parser in Line 2 provides us with a context and a string; this string is
@@ -934,7 +930,7 @@
which can be installed with
*}
-setup{* type_pat_setup *}
+setup %gray {* type_pat_setup *}
text {*
However, a word of warning is in order: Introducing new antiquotations
@@ -1398,24 +1394,4 @@
\end{conventions}
*}
-
-
-(**************************************************)
-(* bak *)
-(**************************************************)
-
-(*
-section {* Do Not Try This At Home! *}
-
-ML {* val my_thms = ref ([]: thm list) *}
-
-attribute_setup my_thm_bad =
- {* Scan.succeed (Thm.declaration_attribute (fn th => fn ctxt =>
- (my_thms := th :: ! my_thms; ctxt))) *} "bad attribute"
-
-declare sym [my_thm_bad]
-declare refl [my_thm_bad]
-
-ML "!my_thms"
-*)
end