--- a/CookBook/FirstSteps.thy Mon Oct 20 06:22:11 2008 +0000
+++ b/CookBook/FirstSteps.thy Mon Oct 27 18:48:52 2008 +0100
@@ -5,7 +5,8 @@
chapter {* First Steps *}
-text {*
+text {*
+
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
@@ -27,11 +28,11 @@
The easiest and quickest way to include code in a theory is
by using the \isacommand{ML} command. For example\smallskip
-\isacommand{ML}
-@{ML_text "{"}@{ML_text "*"}\isanewline
+\isa{\isacommand{ML}
+\isacharverbatimopen\isanewline
\hspace{5mm}@{ML "3 + 4"}\isanewline
-@{ML_text "*"}@{ML_text "}"}\isanewline
-@{ML_text "> 7"}\smallskip
+\isacharverbatimclose\isanewline
+@{ML_text "> 7"}\smallskip}
Expressions inside \isacommand{ML} commands are immediately evaluated,
like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of
@@ -40,15 +41,15 @@
commands the undo operation behaves slightly counter-intuitive, because
if you define\smallskip
-\isacommand{ML}
-@{ML_text "{"}@{ML_text "*"}\isanewline
-@{ML_text "val foo = true"}\isanewline
-@{ML_text "*"}@{ML_text "}"}\isanewline
-@{ML_text "> true"}\smallskip
+\isa{\isacommand{ML}
+\isacharverbatimopen\isanewline
+\hspace{5mm}@{ML_text "val foo = true"}\isanewline
+\isacharverbatimclose\isanewline
+@{ML_text "> true"}\smallskip}
then Isabelle's undo operation has no effect on the definition of
@{ML_text "foo"}. Note that from now on we will drop the
- \isacommand{ML} @{ML_text "{"}@{ML_text "* \<dots> *"}@{ML_text "}"} whenever
+ \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
we show code and its response.
Once a portion of code is relatively stable, one usually wants to
@@ -65,7 +66,8 @@
\end{tabular}
\end{center}
- Note that from now on we are going to drop the the
+ Note that from now on we are going to drop the
+ \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}.
*}
@@ -100,25 +102,22 @@
It is also possible to redirect the channel where the @{ML_text "foo"} is
printed to a separate file, e.g. to prevent Proof General from choking on massive
amounts of trace output. This rediretion can be achieved using the code
-*}
-
-ML {*
- val strip_specials =
- let
- fun strip ("\^A" :: _ :: cs) = strip cs
- | strip (c :: cs) = c :: strip cs
- | strip [] = [];
- in implode o strip o explode end;
- fun redirect_tracing stream =
- Output.tracing_fn := (fn s =>
+@{ML_decl [display]
+"val strip_specials =
+let
+ fun strip (\"\\^A\" :: _ :: cs) = strip cs
+ | strip (c :: cs) = c :: strip cs
+ | strip [] = [];
+in implode o strip o explode end;
+
+fun redirect_tracing stream =
+ Output.tracing_fn := (fn s =>
(TextIO.output (stream, (strip_specials s));
- TextIO.output (stream, "\n");
- TextIO.flushOut stream));
-*}
+ TextIO.output (stream, \"\\n\");
+ TextIO.flushOut stream));"}
-text {*
- Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
+ Calling @{ML_text "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
*}
@@ -143,13 +142,9 @@
Note, however, that antiquotations are statically scoped, that is the value is
determined at ``compile-time'', not ``run-time''. For example the function
-*}
+ @{ML_decl [display]
+ "fun not_current_thyname () = Context.theory_name @{theory}"}
-ML {*
- fun not_current_thyname () = Context.theory_name @{theory}
-*}
-
-text {*
does \emph{not} return the name of the current theory, if it is run in a
different theory. Instead, the code above defines the constant function
that always returns the string @{ML_text "FirstSteps"}, no matter where the
@@ -160,7 +155,6 @@
In a similar way you can use antiquotations to refer to theorems or simpsets:
-
@{ML [display] "@{thm allI}"}
@{ML [display] "@{simpset}"}
@@ -240,7 +234,7 @@
text {*
- @{ML_response [display] "@{typ \"bool \<Rightarrow> nat\"}" "Type \<dots>"}
+ @{ML_response_fake [display] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
(FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} does not print the
internal representation. Is there a reason for this, that needs to be explained
@@ -263,29 +257,19 @@
dynamically. For example, a function that returns the implication
@{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"}
as arguments can only be written as
-*}
-
-ML {*
- fun make_imp P Q tau =
+@{ML_decl [display]
+"fun make_imp P Q tau =
let
- val x = Free ("x",tau)
+ val x = Free (\"x\",tau)
in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x),
HOLogic.mk_Trueprop (Q $ x)))
- end
-*}
-
-text {*
+ end"}
The reason is that one cannot pass the arguments @{term P}, @{term Q} and
@{term "tau"} into an antiquotation. For example the following does not work.
-*}
-ML {*
- fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"}
-*}
-
-text {*
+ @{ML_decl [display] "fun make_wrong_imp P Q tau = @{prop \"\<And>x. P x \<Longrightarrow> Q x\"}"}
To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"}
to both functions.
@@ -397,18 +381,16 @@
application. This combinator, and several variants are defined in
@{ML_file "Pure/General/basics.ML"}.}
-*}
-
-ML {*
-let
+@{ML_response_fake [display]
+"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 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"});
+ |> forall_elim (cterm_of thy @{term \"t::nat\"});
val Qt = implies_elim Pt_implies_Qt (assume assm2);
in
@@ -416,10 +398,7 @@
Qt
|> implies_intr assm2
|> implies_intr assm1
-end
-*}
-
-text {*
+end" "(FIXME)"}
This code-snippet constructs the following proof:
@@ -507,51 +486,43 @@
with the variables @{text xs} that will be generalised once the
goal is proved. The @{text "tac"} is the tactic which proves the goal and which
can make use of the local assumptions.
-*}
-
-
-ML {*
-let
+@{ML_response_fake [display]
+"let
val ctxt = @{context}
- val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
+ val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
in
- Goal.prove ctxt ["P", "Q"] [] goal (fn _ =>
+ Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ =>
eresolve_tac [disjE] 1
THEN resolve_tac [disjI2] 1
THEN assume_tac 1
THEN resolve_tac [disjI1] 1
THEN assume_tac 1)
-end
-*}
-
-text {*
+end" "(FIXME)"}
\begin{readmore}
To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.
\end{readmore}
-*}
-
-text {* An alternative way to transcribe this proof is as follows *}
+ An alternative way to transcribe this proof is as follows
-ML {*
-let
+@{ML_response_fake [display]
+"let
val ctxt = @{context}
- val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
+ val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
in
- Goal.prove ctxt ["P", "Q"] [] goal (fn _ =>
+ Goal.prove ctxt [\"P\", \"Q\"] [] goal (fn _ =>
(eresolve_tac [disjE]
THEN' resolve_tac [disjI2]
THEN' assume_tac
THEN' resolve_tac [disjI1]
THEN' assume_tac) 1)
-end
+end" "(FIXME)"}
+
+ (FIXME: are there any advantages/disadvantages about this way?)
*}
-text {* (FIXME: are there any advantages/disadvantages about this way?) *}
-
section {* Storing Theorems *}
section {* Theorem Attributes *}