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