Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <7846.9208111032@frogland.inmos.co.uk>
Subject: Re: Conditional rewriting
To: Wai.Wong@uk.ac.cam.cl (Wai Wong), 
    info-hol@edu.uidaho.cs.ted (info-hol mailing list)
Date: Tue, 11 Aug 92 11:32:08 BST
In-Reply-To: <"swan.cl.ca.639:11.07.92.08.34.00"@cl.cam.ac.uk>; from "Wai Wong" at Aug 11, 92 9:33 am

Wai Wong has said:
> 
> Has anyone had a tactic which does conditional rewriting?
> By this I mean it perform something like:
> 
>   A ?- t[u']
>  ============ COND_REWRITE_TAC |- P ==> (u = v)
>   A ?- t[v']
> 
> if P is in A, otherwise,
> 
>   A ?- t[u']
>  ======================= COND_REWRITE_TAC |- P ==> (u = v)
>   A,P ?- t[v']  A ?- P
> 
> where u' mathces u and the (first) subgoal is the result of
> rewriting using the conclusion of the input theorem.

try something like

let COND_REWRITE_TAC th =
  let P = (fst o dest_imp o concl) th in
  SUPPOSE_TAC P
  THENL
  [ POP_ASSUM(\ Pth. REWRITE_TAC[MP th Pth])
   ;
    TRY(FIRST_ASSUM ACCEPT_TAC)
  ];;

where SUPPOSE_TAC is defined in the group library by

let SUPPOSE_TAC thisterm thisgoal =
(if type_of thisterm = ":bool"
 then [((thisterm.(fst thisgoal)),(snd thisgoal));((fst thisgoal),thisterm)],
      (\[goalthm;termthm].MP (DISCH thisterm goalthm) termthm)
 else fail)?failwith `SUPPOSE_TAC`;;

(haven't checked this works but think it should)

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk or des@inmos.com    tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"i speak latin to god,   spanish to men,   french to women 
		 and german to my horse."             - charles v of spain