isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:3da5f3f07d8b
+:4e2341f6599d
 now the proof:
 *}
 text_raw{*
 \begin{figure}[t]
+\begin{minipage}{\textwidth}
 \begin{isabelle}
 *}
 ML{*fun sp_tac {prems, params, asms, concl, context, schematics} =
 let
 val str_of_params = str_of_cterms context params
 in
 no_tac
 end*}
 text_raw{*
 \end{isabelle}
+\end{minipage}
 \caption{A function that prints out the various parameters provided by the tactic
 @{ML SUBPROOF}. It uses the functions defined in Section~\ref{sec:printing} for
 extracting strings from @{ML_type cterm}s and @{ML_type thm}s.\label{fig:sptac}}
 \end{figure}
 *}
 (FIXME: What about splitters? @{ML addsplits}, @{ML delsplits})
 *}
 text_raw {*
 \begin{figure}[t]
+\begin{minipage}{\textwidth}
 \begin{isabelle}*}
 ML{*fun print_ss ctxt ss =
 let
 val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
 |> implode
 |> warning
 end*}
 text_raw {*
 \end{isabelle}
+\end{minipage}
 \caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
 all printable information stored in a simpset. We are here only interested in the
 simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}
 moment we are \emph{not} interested in actually rewriting anything. We want
 that the simproc is triggered by the pattern @{term "Suc n"}. This can be
 done by adding the simproc to the current simpset as follows
 *}
-simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *}
+simproc_setup %gray fail_sp ("Suc n") = {* K fail_sp_aux *}
 text {*
 where the second argument specifies the pattern and the right-hand side
 contains the code of the simproc (we have to use @{ML K} since we ignoring
 an argument about morphisms\footnote{FIXME: what does the morphism do?}).
 Simprocs are applied from inside to outside and from left to right. You can
 see this in the proof
 *}
 lemma shows "Suc (Suc 0) = (Suc 1)"
 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*})
 (*<*)oops(*>*)
 text {*
 The simproc @{ML fail_sp'} prints out the sequence
 a theorem if the term is not @{term "Suc 0"}. The result you can see
 in the following proof
 *}
 lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)"
 apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*})
 txt{*
 where the simproc produces the goal state
+\begin{minipage}{\textwidth}
 @{subgoals[display]}
+\end{minipage}
 *}
 (*<*)oops(*>*)
 text {*
 As usual with rewriting you have to worry about looping: you already have
 text {*
 Now in the lemma
 *}
 lemma "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
 apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number_sp]) 1*})
 txt {*
 you obtain the more legible goal state
+\begin{minipage}{\textwidth}
 @{subgoals [display]}
+\end{minipage}
 *}
 (*<*)oops(*>*)
 text {*
 where the simproc rewrites all @{term "Suc"}s except in the last argument. There it cannot
 "if True \<and> P then P else True \<and> False \<Longrightarrow>
 (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
 apply(tactic {* true1_tac 1 *})
 txt {* where the tactic yields the goal state
-@{subgoals [display]}*}
+\begin{minipage}{\textwidth}
+@{subgoals [display]}
+\end{minipage}*}
 (*<*)oops(*>*)
 text {*
 As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
 the conclusion according to @{ML all_true1_conv}.

changeset 177	4e2341f6599d
parent 174	a29b81d4fa88
child 178	fb8f22dd8ad0