New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add gen_new_specification to the kernel. #201

merged 12 commits into from Aug 5, 2015


None yet
2 participants
Copy link

xrchz commented Oct 5, 2014

My primary motivation here is to substantiate the claim that the new rule for HOL Constant Definition Done Right has been implemented in HOL4. In reality, there are a few loose ends but I think they can be left for later.

In particular:

  • While prim_new_definition has been replaced, the old new_specification remains for use in theories before pairs are defined (because gen_new_specification uses pairs to subsume new_specification). ProofPower solves this bootstrapping problem in a way described in Arthan's paper, but leaving both rules in the kernel for now is easier.
  • Also, the OpenTheory kernel and logging is not updated, but it seems to me like a) nobody uses it, and b) the OpenTheory article format is still in flux with regard to whether the new rule is primitive. I am tempted to wait and see whether an alternative implementation of proof-logging in HOL4 is worth pursuing instead (I've heard one might be coming at CPP next year).

xrchz added some commits Feb 19, 2014

start experimental implementation of revised new_specification
Based on Rob Arthan's "HOL Constant Definition Done Right". The tricky
part is deciding how and where to implement the existing definitional
rules that are theoretically subsumed by the new one.
remove Theory.new_specification and reimplement new_definition
in terms of the revised Thm.prim_specification. obviously this breaks
anything that depended on Theory.new_specification, so the next job is
to rework those things (and write a backwards-compatible version, but
later in the build sequence because it needs pairs.)
Add gen_new_specification and remove prim_constant_definition
Implement new_definition in terms of gen_prim_specification.
Leave the existing new_specification in place.
This plan of attack suggested by RDA.

Have only touched the standard kernel, and none of the theories.
Next steps would include updating the other kernels, implementing
new_specification in terms of gen_new_specification (at some point after
pairTheory), and removing uses of new_specification before pairTheory
one by one if possible/desired...
implement new_specification in terms of gen_new_specification
in pairLib - should re-export elsewhere.

This comment has been minimized.

Copy link

mn200 commented Oct 15, 2014

I'm happy in principle, but can you:

  1. write documentation in the relevant manuals and the release notes
  2. ensure it merges cleanly (by first merging master into hcddr)


Merge branch 'master' into hcddr

This comment has been minimized.

Copy link

xrchz commented Dec 7, 2014

(Issue #72 is relevant.)


This comment has been minimized.

Copy link

xrchz commented Aug 3, 2015

Where are the release notes kept that I would need to update? I'll merge in the latest version of master after #272 is merged, to get a version of this that merges cleanly.


This comment has been minimized.

Copy link

mn200 commented Aug 3, 2015

In doc/

xrchz added some commits Aug 4, 2015

Merge branch 'master' into hcddr
conflict on src/postkernel/Theory.sml, because master started checking
whether the name was valid; hopefully resolved correctly

mn200 added a commit that referenced this pull request Aug 5, 2015

Merge pull request #201 from HOL-Theorem-Prover/hcddr
Add gen_new_specification to the kernel.

@mn200 mn200 merged commit f6925ba into master Aug 5, 2015

2 checks passed

continuous-integration/travis-ci/pr The Travis CI build passed
continuous-integration/travis-ci/push The Travis CI build passed

@xrchz xrchz deleted the hcddr branch Aug 8, 2015

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment