Hi Ramana, sure, I'll do it asap. Le 11/02/2013 10:15, Ramana Kumar a écrit :
Any chance you'll check this in to the HOL4 repository, Vincent?On Sat, Dec 29, 2012 at 12:35 AM, Vincent Aravantinos <vincent.aravanti...@gmail.com <mailto:vincent.aravanti...@gmail.com>> wrote: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/ <http://users.encs.concordia.ca/%7Evincent/>
-- Vincent Aravantinos Postdoctoral Fellow, Concordia University, Hardware Verification Group http://users.encs.concordia.ca/~vincent
------------------------------------------------------------------------------ Free Next-Gen Firewall Hardware Offer Buy your Sophos next-gen firewall before the end March 2013 and get the hardware for free! Learn more. http://p.sf.net/sfu/sophos-d2d-feb
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
