Re: [isabelle] simplification at the ML level



Clément,

On Thursday 20 April 2006 17:44, Clement.Hurlin at esial.uhp-nancy.fr wrote:
>    I woud like to simplify goals having the following pattern : "X ==>
> False" . Like for example simplifying
> ¬ ( (a /= b) \/ (f a = b)) ==> False
> to
> (a = b /\ f b /= b) ==> False
>
> (at the ML level) But the Simp_tac tactic fails, I guess because it
> works from bottom to up.
> What should I use ?

if you just need CNF conversion, I suggest you take a look at the existing 
code in HOL/Tools/cnf_funcs.ML, and also in HOL/Tools/meson.ML.

Best,
Tjark





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.