Use kernel compute feature in HOL4 simplifier, decision procedures, and EVAL

[myreen]

Use kernel compute feature in HOL4 simplifier, decision procedures, and EVAL

[xrchz]

Have you considered recording the OpenTheory proofs by adding additional assumptions to the recorded theory corresponding to facts produced by the compute rule? I think OpenTheory kinda supports oracles like that.

[oskarabrahamsson]

This code will run very often. Maybe it would be worth the effort to go with (2)?

[xrchz]

An option to record a standard HOL proof (either of your 1 or 2) is probably good to have too though.

[myreen]

Have you considered recording the OpenTheory proofs by adding additional assumptions to the recorded theory corresponding to facts produced by the compute rule? I think OpenTheory kinda supports oracles like that.

This is a very good point! An importer could then either try to prove these equations with its evaluation mechanism or just take them as assumptions.

[oskarabrahamsson]

Have you considered recording the OpenTheory proofs by adding additional assumptions to the recorded theory corresponding to facts produced by the compute rule? I think OpenTheory kinda supports oracles like that.

This is a nice suggestion. There's this thing: https://www.gilith.com/opentheory/article.html#axiomCommand

[binghe]

Have you considered recording the OpenTheory proofs by adding additional assumptions to the recorded theory corresponding to facts produced by the compute rule? I think OpenTheory kinda supports oracles like that.

This is a nice suggestion. There's this thing: https://www.gilith.com/opentheory/article.html#axiomCommand

A well-shaped exported OT article, when combined all together, should only have 3 very axioms corresponding to the standard HOL theory. The extra assumptions (as axioms) that OpenTheory importers have to prove, if they are too many (e.g. case-by-case arithmetics equations), I feel this will render the entire OT exporting facility less useful. Thus I think simply disabling the new computation primitives for OT kernel, is still the best option.