isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:3d27d77c351f
+:f8d020bbc2c0
 section {* Conversions\label{sec:conversion} *}
 text {*
 Conversions are a thin layer on top of Isabelle's inference kernel, and
 can be viewed as a controllable, bare-bone version of Isabelle's simplifier.
-One difference between conversions and the simplifier is that the former
+One difference between a conversion and the simplifier is that the former
-act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s.
+acts on @{ML_type cterm}s while the latter acts on @{ML_type thm}s.
 However, we will also show in this section how conversions can be applied
-to theorems via tactics. The type for conversions is
+to theorems and used as tactics. The type for conversions is
 *}
 ML{*type conv = cterm -> thm*}
 text {*
 "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
 If you run this example, you will notice that the actual response is the
 seemingly nonsensical @{term
 "2 + 10 \<equiv> 2 + (10::nat)"}. The reason is that the pretty-printer for
-@{ML_type cterm}s eta-normalises terms and therefore produces this output.
+@{ML_type cterm}s eta-normalises (sic) terms and therefore produces this output.
 If we get hold of the ``raw'' representation of the produced theorem,
 we obtain the expected result.
 @{ML_response [display,gray]
 "(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
 Here the conversion of @{thm [source] true_conj1} only applies
 in the first case, but fails in the second. The whole conversion
 does not fail, however, because the combinator @{ML else_conv in Conv} will then
-try out @{ML all_conv in Conv}, which always succeeds.
+try out @{ML all_conv in Conv}, which always succeeds. The same
+behaviour can also be achieved with conversion combinator @{ML_ind try_conv in Conv}.
-The conversion combinator @{ML_ind try_conv in Conv} constructs a conversion
-which is tried out on a term, but in case of failure just does nothing.
 For example
 @{ML_response_fake [display,gray]
 "let
 val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
 val ctrm = @{cterm \"True \<or> P\"}
 in
 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}.
 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
 will lift this restriction. The combinators @{ML_ind fun_conv in Conv}
 We can now apply all these functions in a conversion that recursively
 descends a term and applies a ``@{thm [source] true_conj1}''-conversion
 in all possible positions.
 *}
-ML %linenosgray{*fun all_true1_conv ctxt ctrm =
+ML %linenosgray{*fun true_conj1_conv ctxt ctrm =
 case (Thm.term_of ctrm) of
 @{term "op \<and>"} $ @{term True} $ _ =>
-(Conv.arg_conv (all_true1_conv ctxt) then_conv
+(Conv.arg_conv (true_conj1_conv ctxt) then_conv
 Conv.rewr_conv @{thm true_conj1}) ctrm
-| _ $ _ => Conv.comb_conv (all_true1_conv ctxt) ctrm
+| _ $ _ => Conv.comb_conv (true_conj1_conv ctxt) ctrm
-| Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm
+| Abs _ => Conv.abs_conv (fn (_, ctxt) => true_conj1_conv ctxt) ctxt ctrm
 | _ => Conv.all_conv ctrm*}
 text {*
 This function ``fires'' if the terms is of the form @{text "(True \<and> \<dots>)"}.
 It descends under applications (Line 6 and 7) and abstractions
 to be able to pattern-match the term. To see this
 conversion in action, consider the following example:
 @{ML_response_fake [display,gray]
 "let
-val conv = all_true1_conv @{context}
+val conv = true_conj1_conv @{context}
-val ctrm = @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
 in
 conv ctrm
 end"
 "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+*}
+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:
+*}
+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
+end*}
+text {*
+The function @{ML bottom_conv in More_Conv} traverses first the the term and
+on the ``way down'' applies the conversion, whereas @{ML top_conv in
+More_Conv} applies the on the ``way up''. To see the difference,
+assume the following two meta-equations.
+*}
+lemma conj_assoc:
+fixes A B C::bool
+shows "A \<and> (B \<and> C) \<equiv> (A \<and> B) \<and> C"
+and   "(A \<and> B) \<and> C \<equiv> A \<and> (B \<and> C)"
+by simp_all
+text {*
+and the @{ML_type cterm} @{text "(a \<and> (b \<and> c)) \<and> d"}. The reader should
+pause for a moment to be convinced that rewriting top-down and bottom-up
+according to the lemma produces two results.
+@{ML_response_fake [display, gray]
+"let
+val ctxt = @{context}
+val conv = Conv.try_conv (More_Conv.rewrs_conv @{thms conj_assoc})
+val conv_top = More_Conv.top_conv (K conv) ctxt
+val conv_bot = More_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))\",
+\"(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)\")"}
 To see how much control you have about rewriting by using conversions, let us
 make the task a bit more complicated by rewriting according to the rule
 @{text true_conj1}, but only in the first arguments of @{term If}s. Then
 the conversion should be as follows.
 *}
-ML{*fun if_true1_conv ctxt ctrm =
+ML{*fun if_true1_simple_conv ctxt ctrm =
 case Thm.term_of ctrm of
 Const (@{const_name If}, _) $ _ =>
-Conv.arg_conv (all_true1_conv ctxt) ctrm
+Conv.arg_conv (true_conj1_conv ctxt) ctrm
-| _ $ _ => Conv.comb_conv (if_true1_conv ctxt) ctrm
+| _ => Conv.no_conv ctrm
-| Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm
-| _ => Conv.all_conv ctrm *}
+val if_true1_conv = More_Conv.top_sweep_conv if_true1_simple_conv*}
 text {*
-Here is an example for this conversion:
+In the first function we only treat the top-most redex and also only the
+success case and otherwise return @{ML no_conv in Conv}.  To apply this
+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
+root and applies it to all the redexes on the way, but stops in a branch as
+soon as it found one redex.\footnote{\bf Fixme: Check with Sascha whether
+the conversion stops after a single success case, or stops in each branch
+after a success case.} Here is an example for this conversion:
 @{ML_response_fake [display,gray]
 "let
-val conv = if_true1_conv @{context}
+val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat))
-val ctrm =
+then True \<and> True else True \<and> False\"}
-@{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}
 in
-conv ctrm
+if_true1_conv @{context} ctrm
 end"
 "if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False
 \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
 *}
 text {*
 So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
 also work on theorems using the function @{ML_ind  fconv_rule in Conv}. As an example,
-consider the conversion @{ML all_true1_conv} and the lemma:
+consider the conversion @{ML true_conj1_conv} and the lemma:
 *}
 lemma foo_test:
 shows "P \<or> (True \<and> \<not>P)" by simp
 text {*
-Using the conversion @{ML all_true1_conv} you can transform this theorem into a
+Using the conversion @{ML true_conj1_conv} you can transform this theorem into a
 new theorem as follows
 @{ML_response_fake [display,gray]
 "let
-val conv = Conv.fconv_rule (all_true1_conv @{context})
+val conv = Conv.fconv_rule (true_conj1_conv @{context})
 val thm = @{thm foo_test}
 in
 conv thm
 end"
 "?P \<or> \<not> ?P"}
 \item @{ML_ind concl_conv in Conv} for applying a conversion to the
 conclusion of a goal.
 \end{itemize}
-Assume we want to apply @{ML all_true1_conv} only in the conclusion
+Assume we want to apply @{ML true_conj1_conv} only in the conclusion
 of the goal, and @{ML if_true1_conv} should only apply to the premises.
 Here is a tactic doing exactly that:
 *}
 ML{*fun true1_tac ctxt =
 CONVERSION
 (Conv.params_conv ~1 (fn ctxt =>
 (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
-Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt)*}
+Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)*}
 text {*
 We call the conversions with the argument @{ML "~1"}. This is to
 analyse all parameters, premises and conclusions. If we call them with
 a non-negative number, say @{text n}, then these conversions will
 \end{isabelle}*}
 (*<*)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}.
+the conclusion according to @{ML true_conj1_conv}.
 Conversions can 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.
 *}

changeset 405	f8d020bbc2c0
parent 404	3d27d77c351f
child 406	f399b6855546