Cond_rewrite.COND_REWRITE1

STRUCTURE

SYNOPSIS

A simple conditional rewriting tactic.

DESCRIPTION

COND_REWRITE1_TAC is a front end of the conditional rewriting tactic COND_REWR_TAC. The input theorem should be in the following form

   A |- !x11 ... . P1 ==> ... !xm1 ... . Pm ==> (!x ... . Q = R)

where each antecedent Pi itself may be a conjunction or disjunction. This theorem is transformed to a standard form expected by COND_REWR_TAC which carries out the actual rewriting. The transformation is performed by COND_REWR_CANON. The search function passed to COND_REWR_TAC is search_top_down. The effect of applying this tactic is to substitute into the goal instances of the right hand side of the conclusion of the input theorem Ri' for the corresponding instances of the left hand side. The search is top-down left-to-right. All matches found by the search function are substituted. New subgoals corresponding to the instances of the antecedents which do not appear in the assumption of the original goal are created. See manual page of COND_REWR_TAC for details of how the instantiation and substitution are done.

FAILURE

COND_REWRITE1_TAC th fails if th cannot be transformed into the required form by the function COND_REWR_CANON. Otherwise, it fails if no match is found or the theorem cannot be instantiated.

EXAMPLE

The following example illustrates a straightforward use of COND_REWRITE1_TAC. We use the built-in theorem LESS_MOD as the input theorem.

   #LESS_MOD;;
   Theorem LESS_MOD autoloading from theory `arithmetic` ...
   LESS_MOD = |- !n k. k < n ==> (k MOD n = k)

   |- !n k. k < n ==> (k MOD n = k)

We set up a goal

   #g"2 MOD 3 = 2";;
   "2 MOD 3 = 2"

   () : void

and then apply the tactic

   #e(COND_REWRITE1_TAC LESS_MOD);;
   OK..
   2 subgoals
   "2 = 2"
       [ "2 < 3" ]

   "2 < 3"

   () : void

SEEALSO

COND_REWR_TAC, COND_REWRITE1_CONV, COND_REWR_CONV, COND_REWR_CANON, search_top_down