--- a/ProgTutorial/Tactical.thy Mon Aug 03 13:53:04 2009 +0200
+++ b/ProgTutorial/Tactical.thy Mon Aug 03 14:01:57 2009 +0200
@@ -145,7 +145,7 @@
@{text "*** At command \"apply\"."}
\end{isabelle}
- This means they failed.\footnote{To be precise tactics do not produce this error
+ This means they failed.\footnote{To be precise, tactics do not produce this error
message, it originates from the \isacommand{apply} wrapper.} The reason for this
error message is that tactics
are functions mapping a goal state to a (lazy) sequence of successor states.
@@ -212,7 +212,7 @@
ML{*fun my_print_tac ctxt thm =
let
- val _ = writeln (string_of_thm_no_vars ctxt thm)
+ val _ = tracing (string_of_thm_no_vars ctxt thm)
in
Seq.single thm
end*}
@@ -528,9 +528,8 @@
safety is provided by the functions @{ML [index] FOCUS in Subgoal} and
@{ML [index] SUBPROOF}. These tactics fix the parameters
and bind the various components of a goal state to a record.
- To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
- takes a record and just prints out the content of this record (using the
- string transformation functions from in Section~\ref{sec:printing}). Consider
+ To see what happens, use the function defined in Figure~\ref{fig:sptac}, which
+ takes a record and just prints out the contents of this record. Consider
now the proof:
*}
@@ -549,11 +548,11 @@
val string_of_prems = string_of_thms_no_vars context prems
val string_of_schms = string_of_cterms context (map fst (snd schematics))
- val _ = (writeln ("params: " ^ string_of_params);
- writeln ("schematics: " ^ string_of_schms);
- writeln ("assumptions: " ^ string_of_asms);
- writeln ("conclusion: " ^ string_of_concl);
- writeln ("premises: " ^ string_of_prems))
+ val _ = (tracing ("params: " ^ string_of_params);
+ tracing ("schematics: " ^ string_of_schms);
+ tracing ("assumptions: " ^ string_of_asms);
+ tracing ("conclusion: " ^ string_of_concl);
+ tracing ("premises: " ^ string_of_prems))
in
all_tac
end*}
@@ -577,19 +576,19 @@
\begin{quote}\small
\begin{tabular}{ll}
params: & @{term x}, @{term y}\\
- schematics: & @{term z}\\
+ schematics: & @{text ?z}\\
assumptions: & @{term "A x y"}\\
conclusion: & @{term "B y x \<longrightarrow> C (z y) x"}\\
premises: & @{term "A x y"}
\end{tabular}
\end{quote}
- (FIXME: find out how nowadays the schmetics are handled)
+ (FIXME: Find out how nowadays the schematics are handled)
- Notice in the actual output the brown colour of the variables @{term x} and
- @{term y}. Although they are parameters in the original goal, they are fixed inside
- the subproof. By convention these fixed variables are printed in brown colour.
- Similarly the schematic variable @{term z}. The assumption, or premise,
+ Notice in the actual output the brown colour of the variables @{term x},
+ and @{term y}. Although they are parameters in the original goal, they are fixed inside
+ the tactic. By convention these fixed variables are printed in brown colour.
+ Similarly the schematic variable @{text ?z}. The assumption, or premise,
@{prop "A x y"} is bound as @{ML_type cterm} to the record-variable
@{text asms}, but also as @{ML_type thm} to @{text prems}.
@@ -605,7 +604,7 @@
\begin{quote}\small
\begin{tabular}{ll}
params: & @{term x}, @{term y}\\
- schematics: & @{term z}\\
+ schematics: & @{text ?z}\\
assumptions: & @{term "A x y"}, @{term "B y x"}\\
conclusion: & @{term "C (z y) x"}\\
premises: & @{term "A x y"}, @{term "B y x"}
@@ -617,15 +616,18 @@
text {*
Now also @{term "B y x"} is an assumption bound to @{text asms} and @{text prems}.
- The difference between @{ML SUBPROOF} and @{ML FOCUS in Subgoal} is that the former
- expects that the goal is solved completely, which the latter does not. One
- convenience of both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} is that we can apply the
- assumptions using the usual tactics, because the parameter @{text prems}
- contains them as theorems. With this you can easily implement a tactic that
- behaves almost like @{ML atac}:
+ The difference between the tactics @{ML SUBPROOF} and @{ML FOCUS in Subgoal}
+ is that the former expects that the goal is solved completely, which the
+ latter does not. @{ML SUBPROOF} can also not instantiate an schematic
+ variables.
+
+ One convenience of both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} is that we
+ can apply the assumptions using the usual tactics, because the parameter
+ @{text prems} contains them as theorems. With this you can easily implement
+ a tactic that behaves almost like @{ML atac}:
*}
-ML{*val atac' = SUBPROOF (fn {prems, ...} => resolve_tac prems 1)*}
+ML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*}
text {*
If you apply @{ML atac'} to the next lemma
@@ -638,19 +640,14 @@
(*<*)oops(*>*)
text {*
- The restriction in this tactic which is not present in @{ML atac} is that it
- cannot instantiate any schematic variables. This might be seen as a defect,
- but it is actually an advantage in the situations for which @{ML SUBPROOF}
- was designed: the reason is that, as mentioned before, instantiation of
- schematic variables can affect several goals and can render them
- unprovable. @{ML SUBPROOF} is meant to avoid this.
+ Notice that @{ML atac'} inside @{ML FOCUS in Subgoal} calls @{ML
+ resolve_tac} with the subgoal number @{text "1"} and also the outer call to
+ @{ML FOCUS in Subgoal} in the \isacommand{apply}-step uses @{text "1"}. This
+ is another advantage of @{ML FOCUS in Subgoal} and @{ML SUBPROOF}: the
+ addressing inside it is completely local to the tactic inside the
+ subproof. It is therefore possible to also apply @{ML atac'} to the second
+ goal by just writing:
- Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with
- the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in
- the \isacommand{apply}-step uses @{text "1"}. This is another advantage of
- @{ML SUBPROOF}: the addressing inside it is completely local to the tactic
- inside the subproof. It is therefore possible to also apply @{ML atac'} to
- the second goal by just writing:
*}
lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y"
@@ -666,7 +663,8 @@
\isccite{sec:results}.
\end{readmore}
- Similar but less powerful functions than @{ML FOCUS in Subgoal} are
+ Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively
+ @{ML SUBPROOF}, are
@{ML [index] SUBGOAL} and @{ML [index] CSUBGOAL}. They allow you to
inspect a given subgoal (the former
presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
@@ -1196,7 +1194,7 @@
["Simproc patterns:"] @ map name_ctrm procs
in
s |> cat_lines
- |> writeln
+ |> tracing
end*}
text_raw {*
\end{isabelle}
@@ -1523,7 +1521,7 @@
ML %linenosgray{*fun fail_simproc simpset redex =
let
val ctxt = Simplifier.the_context simpset
- val _ = writeln ("The redex: " ^ (string_of_cterm ctxt redex))
+ val _ = tracing ("The redex: " ^ (string_of_cterm ctxt redex))
in
NONE
end*}
@@ -1594,7 +1592,7 @@
ML{*fun fail_simproc' simpset redex =
let
val ctxt = Simplifier.the_context simpset
- val _ = writeln ("The redex: " ^ (Syntax.string_of_term ctxt redex))
+ val _ = tracing ("The redex: " ^ (Syntax.string_of_term ctxt redex))
in
NONE
end*}