Re: [Hol-info] Improve EXISTS_TAC with by taking hints from the assumption list

[Vincent A. <vin...@gm...>]

Le 28/12/12 08:20, Michael Norrish a écrit :
> I think my first reaction to a clean implementation with test cases 
> (in a selftest.sml file, say) and documentation (a .doc file) would be 
> to accept first and ask questions later. If it turns out that 
> something really is redundant or otherwise unloved given other 
> facilities in the system it can always be removed. Michael 
Ok. For now, here is a fast translation of HINT_EXISTS_TAC for HOL4:


fun HINT_EXISTS_TAC g =
   let
     val (hs,c) = g
     val (v,c') = dest_exists c
     val (vs,c') = strip_exists c'
     fun hyp_match c h =
       if exists (C mem vs) (free_vars c)
       then fail ()
       else (match_term c h,h)
     val ((subs,_),h) = tryfind (C tryfind hs o hyp_match) (strip_conj c')
     val witness =
       case subs of
          [] => v
         |[{redex = u, residue = t}] =>
             if u = v then t else failwith "GEN_HINT_EXISTS_TAC not 
applicable"
         |_ => failwith "GEN_HINT_EXISTS_TAC not applicable"
   in
     (EXISTS_TAC witness THEN ASM_REWRITE_TAC[]) g
   end;


Cheers,
V.

-- 
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/