Dear Robert,
you can use PURE_REWRITE_TAC which uses only the given list of rewrites.
Or you can change the set basic_rewrites with the command
set_basic_rewrites.
E.g.,
let rthl = CONJUNCTS (MESON[] `~T = F /\ ~F = T`);;
set_basic_rewrites rthl;;
Marco
2015-05-21 15:18 GMT+02:00 Robert White <[email protected]>:
> Hello again,
>
> I understand that HOL is a reasoner for classical logic so there is no
> surprise when I want to prove something using rewriting I get a set of
> rules as basic_rewrites where we can find ~ ~t <=> t; there.
>
> So here comes the question, is there a way we can get intuitionistic set
> or rewriting rules in HOL Light already to do pure constructive logic
> reasoning?
>
> Thanks again.
>
> --
>
> Regards,
> Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
> INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
>
>
> ------------------------------------------------------------------------------
> One dashboard for servers and applications across Physical-Virtual-Cloud
> Widest out-of-the-box monitoring support with 50+ applications
> Performance metrics, stats and reports that give you Actionable Insights
> Deep dive visibility with transaction tracing using APM Insight.
> http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
One dashboard for servers and applications across Physical-Virtual-Cloud
Widest out-of-the-box monitoring support with 50+ applications
Performance metrics, stats and reports that give you Actionable Insights
Deep dive visibility with transaction tracing using APM Insight.
http://ad.doubleclick.net/ddm/clk/290420510;117567292;y
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
