Cond_rewrite.COND_REWRITE1

STRUCTURE

SYNOPSIS

A simple conditional rewriting conversion.

DESCRIPTION

COND_REWRITE1_CONV is a front end of the conditional rewriting conversion COND_REWR_CONV. 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_CONV which carries out the actual rewriting. The transformation is performed by COND_REWR_CANON. The search function passed to COND_REWR_CONV is search_top_down. The effect of applying the conversion COND_REWRITE1_CONV ths th to a term tm is to derive a theorem

  A' |- tm = tm[R'/Q']

where the right hand side of the equation is obtained by rewriting the input term tm with an instance of the conclusion of the input theorem. The theorems in the list ths are used to discharge the assumptions generated from the antecedents of the input theorem.

FAILURE

COND_REWRITE1_CONV ths th fails if th cannot be transformed into the required form by 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_CONV. 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)

   #COND_REWRITE1_CONV [] LESS_MOD "2 MOD 3";;
   2 < 3 |- 2 MOD 3 = 2

   #let less_2_3 = REWRITE_RULE[LESS_MONO_EQ;LESS_0]
   #(REDEPTH_CONV num_CONV "2 < 3");;
   less_2_3 = |- 2 < 3

   #COND_REWRITE1_CONV [less_2_3] LESS_MOD "2 MOD 3";;
   |- 2 MOD 3 = 2

In the first example, an empty theorem list is supplied to COND_REWRITE1_CONV so the resulting theorem has an assumption 2 < 3. In the second example, a list containing a theorem |- 2 < 3 is supplied, the resulting theorem has no assumptions.

SEEALSO

COND_REWR_TAC, COND_REWRITE1_TAC, COND_REWR_CONV, COND_REWR_CANON, search_top_down