isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:0a25b35178c3
+:5e0a2b50707e
 conv ctrm
 end"
 "True \<or> P \<equiv> True \<or> P"}
 Rewriting with more than one theorem can be done using the function
-@{ML_ind rewrs_conv in More_Conv} from the structure @{ML_struct More_Conv}.
+@{ML_ind rewrs_conv in Conv} from the structure @{ML_struct Conv}.
 Apart from the function @{ML beta_conversion in Thm}, which is able to fully
 beta-normalise a term, the conversions so far are restricted in that they
 only apply to the outer-most level of a @{ML_type cterm}. In what follows we
 *}
 text {*
 Conversions that traverse terms, like @{ML true_conj1_conv} above, can be
 implemented more succinctly with the combinators @{ML_ind bottom_conv in
-More_Conv} and @{ML_ind top_conv in More_Conv}. For example:
+Conv} and @{ML_ind top_conv in Conv}. For example:
 *}
 ML{*fun true_conj1_conv ctxt =
 let
 val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
 in
-More_Conv.bottom_conv (K conv) ctxt
+Conv.bottom_conv (K conv) ctxt
 end*}
 text {*
 If we regard terms as trees with variables and constants on the top, then
-@{ML bottom_conv in More_Conv} traverses first the the term and
+@{ML bottom_conv in Conv} traverses first the the term and
 on the ``way down'' applies the conversion, whereas @{ML top_conv in
-More_Conv} applies the conversion on the ``way up''. To see the difference,
+Conv} applies the conversion on the ``way up''. To see the difference,
 assume the following two meta-equations
 *}
 lemma conj_assoc:
 fixes A B C::bool
 two results are calculated.
 @{ML_response_fake [display, gray]
 "let
 val ctxt = @{context}
-val conv = Conv.try_conv (More_Conv.rewrs_conv @{thms conj_assoc})
+val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})
-val conv_top = More_Conv.top_conv (K conv) ctxt
+val conv_top = Conv.top_conv (K conv) ctxt
-val conv_bot = More_Conv.bottom_conv (K conv) ctxt
+val conv_bot = Conv.bottom_conv (K conv) ctxt
 val ctrm = @{cterm \"(a \<and> (b \<and> c)) \<and> d\"}
 in
 (conv_top ctrm, conv_bot ctrm)
 end"
 "(\"(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))\",
 case Thm.term_of ctrm of
 Const (@{const_name If}, _) $ _ =>
 Conv.arg_conv (true_conj1_conv ctxt) ctrm
 | _ => Conv.no_conv ctrm
-val if_true1_conv = More_Conv.top_sweep_conv if_true1_simple_conv*}
+val if_true1_conv = Conv.top_sweep_conv if_true1_simple_conv*}
 text {*
 In the first function we only treat the top-most redex and also only the
 success case. As default we return @{ML no_conv in Conv}.  To apply this
 ``simple'' conversion inside a term, we use in the last line the combinator @{ML_ind
-top_sweep_conv in More_Conv}, which traverses the term starting from the
+top_sweep_conv in Conv}, which traverses the term starting from the
 root and applies it to all the redexes on the way, but stops in each branch as
 soon as it found one redex. Here is an example for this conversion:
 @{ML_response_fake [display,gray]
 text {*
 As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
 the conclusion according to @{ML true_conj1_conv}. If we only have one
 conversion that should be uniformly applied to the whole goal state, we
-can simplify @{ML true1_tac} using @{ML_ind top_conv in More_Conv}.
+can simplify @{ML true1_tac} using @{ML_ind top_conv in Conv}.
 Conversions are also be helpful for constructing meta-equality theorems.
 Such theorems are often definitions. As an example consider the following
 two ways of defining the identity function in Isabelle.
 *}
 have to construct quite large terms. Also see Recipe \ref{rec:timing} for information
 about timing.
 \end{exercise}
 \begin{readmore}
-See @{ML_file "Pure/conv.ML"} and  @{ML_file "Tools/more_conv.ML"}
+See @{ML_file "Pure/conv.ML"}
 for more information about conversion combinators.
 Some basic conversions are defined in  @{ML_file "Pure/thm.ML"},
 @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
 \end{readmore}

changeset 424	5e0a2b50707e
parent 422	e79563b14b0f
child 436	373f99b1221a