isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:ec47352e99c2
+:d820cb5873ea
 ML{*fun no_tac thm = Seq.empty*}
 text {*
 which means @{ML no_tac} always fails. The second returns the given theorem wrapped
-up in a single member sequence; it is defined as
+in a single member sequence; it is defined as
 *}
 ML{*fun all_tac thm = Seq.single thm*}
 text {*
 Seq.single thm
 end*}
 text_raw {*
 \begin{figure}[p]
+\begin{boxedminipage}{\textwidth}
 \begin{isabelle}
 *}
 lemma shows "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"
 apply(tactic {* my_print_tac @{context} *})
 \end{minipage}\medskip
 *}
 done
 text_raw {*
 \end{isabelle}
+\end{boxedminipage}
 \caption{The figure shows a proof where each intermediate goal state is
 printed by the Isabelle system and by @{ML my_print_tac}. The latter shows
 the goal state as represented internally (highlighted boxes). This
-illustrates that every goal state in Isabelle is represented by a theorem:
+tactic shows that every goal state in Isabelle is represented by a theorem:
 when you start the proof of \mbox{@{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}} the theorem is
 @{text "(\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B) \<Longrightarrow> (\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B)"}; when you finish the proof the
 theorem is @{text "\<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B"}.\label{fig:goalstates}}
 \end{figure}
 *}
 *}
 section {* Simple Tactics *}
 text {*
-Let us start with the tactic @{ML print_tac}, which is quite useful for low-level
+Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful
-debugging of tactics. It just prints out a message and the current goal state
+for low-level debugging of tactics. It just prints out a message and the current
-(unlike @{ML my_print_tac}, it prints the goal state as the user would see it).
+goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state
-For example, processing the proof
+as the user would see it.  For example, processing the proof
 *}
 lemma shows "False \<Longrightarrow> True"
 apply(tactic {* print_tac "foo message" *})
 txt{*gives:\medskip
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
 Note the number in each tactic call. Also as mentioned in the previous section, most
-basic tactics take such a number as argument; it addresses the subgoal they are analysing.
+basic tactics take such a number as argument: this argument addresses the subgoal
-In the proof below, we first split up the conjunction in  the second subgoal by
+the tacics are analysing. In the proof below, we first split up the conjunction in
-focusing on this subgoal first.
+the second subgoal by focusing on this subgoal first.
 *}
 lemma shows "Foo" and "P \<and> Q"
 apply(tactic {* rtac @{thm conjI} 2 *})
 txt {*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 text {*
-Similarly versions taking a list of theorems exist for the tactics
+Similarl versions taking a list of theorems exist for the tactics
 @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.
 Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems
 into the assumptions of the current goal state. For example
 string transformation functions from in Section~\ref{sec:printing}). Consider
 now the proof:
 *}
 text_raw{*
-\begin{figure}
+\begin{figure}[t]
 \begin{isabelle}
 *}
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} =
 let
 val str_of_params = str_of_cterms context params
 (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
 *}
 text_raw {*
-\begin{figure}[tp]
+\begin{figure}[t]
 \begin{isabelle}*}
 ML{*fun print_ss ctxt ss =
 let
 val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
 As you can see, the tactic unfolds the definitions in all subgoals.
 *}
 text_raw {*
-\begin{figure}[tp]
+\begin{figure}[p]
+\begin{boxedminipage}{\textwidth}
 \begin{isabelle} *}
 types  prm = "(nat \<times> nat) list"
 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a"  ("_ \<bullet> _" [80,80] 80)
 primrec (perm_nat)
 lemma perm_compose:
 fixes c::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "pi\<^isub>1\<bullet>(pi\<^isub>2\<bullet>c) = (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>(pi\<^isub>1\<bullet>c)"
 by (induct pi\<^isub>2) (auto)
 text_raw {*
-\end{isabelle}\medskip
+\end{isabelle}
+\end{boxedminipage}
 \caption{A simple theory about permutations over @{typ nat}. The point is that the
 lemma @{thm [source] perm_compose} cannot be directly added to the simplifier, as
 it would cause the simplifier to loop. It can still be used as a simplification
 rule if the permutation is sufficiently protected.\label{fig:perms}
 (FIXME: Uses old primrec.)}

changeset 173	d820cb5873ea
parent 172	ec47352e99c2
child 174	a29b81d4fa88