1\DOC COND_REWRITE1_TAC
2
3\TYPE {COND_REWRITE1_TAC : thm_tactic}
4
5\SYNOPSIS
6A simple conditional rewriting tactic.
7
8\KEYWORDS
9tactic, rewriting, conditional.
10
11\DESCRIBE
12{COND_REWRITE1_TAC} is a front end of the conditional rewriting
13tactic {COND_REWR_TAC}. The input theorem should be in the following form
14{
15   A |- !x11 ... . P1 ==> ... !xm1 ... . Pm ==> (!x ... . Q = R)
16}
17where each antecedent {Pi} itself may be a conjunction or disjunction.
18This theorem is transformed to a standard form expected by
19{COND_REWR_TAC} which carries out the actual rewriting.
20The transformation is performed by {COND_REWR_CANON}. The search function
21passed to {COND_REWR_TAC} is {search_top_down}. The effect of applying
22this tactic is to substitute into the goal instances of the right hand
23side of the conclusion of the input theorem {Ri'} for the
24corresponding instances of the left hand side. The search is top-down
25left-to-right. All matches found by the search function are
26substituted. New subgoals corresponding to the instances of the
27antecedents which do not appear in the assumption of the original goal
28are created. See manual page of {COND_REWR_TAC} for details of how the
29instantiation and substitution are done.
30
31\FAILURE
32{COND_REWRITE1_TAC th}  fails if {th} cannot be transformed into the
33required form by the function {COND_REWR_CANON}. Otherwise, it fails if no match
34is found or the theorem cannot be instantiated.
35
36\EXAMPLE
37The following example illustrates a straightforward use of {COND_REWRITE1_TAC}.
38We use the built-in theorem {LESS_MOD} as the input theorem.
39{
40   #LESS_MOD;;
41   Theorem LESS_MOD autoloading from theory `arithmetic` ...
42   LESS_MOD = |- !n k. k < n ==> (k MOD n = k)
43
44   |- !n k. k < n ==> (k MOD n = k)
45}
46We set up a goal
47{
48   #g"2 MOD 3 = 2";;
49   "2 MOD 3 = 2"
50
51   () : void
52}
53and then apply the tactic
54{
55   #e(COND_REWRITE1_TAC LESS_MOD);;
56   OK..
57   2 subgoals
58   "2 = 2"
59       [ "2 < 3" ]
60
61   "2 < 3"
62
63   () : void
64}
65
66\SEEALSO
67Cond_rewrite.COND_REWR_TAC, Cond_rewrite.COND_REWRITE1_CONV,
68Cond_rewrite.COND_REWR_CONV, Cond_rewrite.COND_REWR_CANON,
69Cond_rewrite.search_top_down.
70
71\ENDDOC
72
73