Any chance you'll check this in to the HOL4 repository, Vincent?
On Sat, Dec 29, 2012 at 12:35 AM, Vincent Aravantinos <
[email protected]> 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/~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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
