[opentheory-users] removing definitions from theories

[Joe Leslie-Hurd]

Hi Ramana,

I've just released a new version of the opentheory tool, namely

$ opentheory -v
opentheory 1.3 (release 20160204)

which includes support for a --skip-definitions flag when generating
article files. This switch replaces defined symbols with external
symbols and definition theorems with theory assumptions.

For example, here is the unit theory with and without definitions:

$ opentheory info --article unit | opentheory info --theory article:-
2 external type operators: -> bool
8 external constants: = select ! /\ ==> ? ?! T
13 assumptions:
  |- T
  |- !t. t ==> t
  |- (?) = \p. p ((select) p)
  |- !t. (!x. t) <=> t
  |- (!) = \p. p = \x. T
  |- !t. (t <=> T) <=> t
  |- !t. T /\ t <=> t
  |- (==>) = \p q. p /\ q <=> p
  |- !x y. x = y <=> y = x
  |- (/\) = \p q. (\f. f p q) = \f. f T T
  |- (?) = \p. !q. (!x. p x ==> q) ==> q
  |- !f g. (!x. f x = g x) <=> f = g
  |- !p. (?!x. p x) <=> (?x. p x) /\ !x x'. p x /\ p x' ==> x = x'
1 defined type operator: Data.Unit.unit
1 defined constant: Data.Unit.()
5 theorems:
  |- !v. v = Data.Unit.()
  |- !f g. f = g
  |- !e. ?fn. fn Data.Unit.() = e
  |- !e. ?!fn. fn Data.Unit.() = e
  |- !p. p Data.Unit.() ==> !x. p x

$ opentheory info --skip-definitions --article unit | opentheory info
--theory article:-
3 external type operators: -> bool Data.Unit.unit
10 external constants: = ! /\ ==> ? ?! T Data.Unit.() HOLLight.one_ABS
  HOLLight.one_REP
14 assumptions:
  |- T
  |- !t. t ==> t
  |- !t. (!x. t) <=> t
  |- (!) = \p. p = \x. T
  |- (\a. HOLLight.one_ABS (HOLLight.one_REP a)) = \a. a
  |- !t. (t <=> T) <=> t
  |- !t. T /\ t <=> t
  |- (==>) = \p q. p /\ q <=> p
  |- (\r. HOLLight.one_REP (HOLLight.one_ABS r) <=> r) =
     \r. let b <- r in b
  |- !x y. x = y <=> y = x
  |- (/\) = \p q. (\f. f p q) = \f. f T T
  |- (?) = \p. !q. (!x. p x ==> q) ==> q
  |- !f g. (!x. f x = g x) <=> f = g
  |- !p. (?!x. p x) <=> (?x. p x) /\ !x x'. p x /\ p x' ==> x = x'
5 theorems:
  |- !v. v = Data.Unit.()
  |- !f g. f = g
  |- !e. ?fn. fn Data.Unit.() = e
  |- !e. ?!fn. fn Data.Unit.() = e
  |- !p. p Data.Unit.() ==> !x. p x

Hopefully this will help with your HOL4 interface project.

Cheers,

Joe

On Tue, Feb 2, 2016 at 9:54 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> Sorry I didn't reply sooner - I'm actually working right now on adding
> functionality to the opentheory tool to replace definitions with
> theory assumptions.
>
> Your plan seems sensible to me. And it's definitely an argument for
> using Rob's new constant definition primitive as much as possible,
> since classical definitions of the form |- c = t are often rather
> esoteric.
>
> I'll let you know when I have something working.
>
> Cheers,
>
> Joe
>
> On Tue, Feb 2, 2016 at 9:48 PM, Ramana Kumar <ramana at member.fsf.org> wrote:
>> Hi Joe,
>>
>> Do you have any comments on the plan I described?
>>
>> And/or would you be able to add the definition-removing functionality to the
>> opentheory tool?
>>
>> Thanks,
>> Ramana
>>
>> On 30 January 2016 at 12:57, Ramana Kumar <ramana at member.fsf.org> wrote:
>>>
>>> I am trying to build a compatibility bridge between HOL4's standard
>>> library and the OpenTheory standard library.
>>>
>>> I've thought about (and started trying) various approaches.
>>>
>>> The latest idea (due mostly to Michael Norrish) is:
>>>
>>> Record a theory containing the HOL4 standard library, entirely in the HOL4
>>> namespace, depending only on the axioms of HOL.
>>> Remove from this theory all definitions of things that are already in the
>>> OpenTheory standard library. The constants should then become ungrounded,
>>> and where they were defined the article should instead add the definitional
>>> axioms as axioms.
>>> Instantiate all the ungrounded constants with constants from the
>>> OpenTheory standard library, and then also add the OpenTheory standard
>>> library.
>>> Prove any remaining axioms.
>>>
>>> The feature I requested is for step 2. I realise now that I need to be
>>> able to remove definitions selectively, not just remove them all. There may
>>> be some way to accomplish that even if the primitive functionality is to
>>> remove them all, though.
>>>
>>> On 30 January 2016 at 03:52, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>>>
>>>> Hi Ramana,
>>>>
>>>> There's currently no tool support for this, but I don't think it would
>>>> be too difficult to implement. What is your use-case?
>>>>
>>>> Cheers,
>>>>
>>>> Joe
>>>>
>>>> On Fri, Jan 29, 2016 at 12:36 AM, Ramana Kumar <ramana at member.fsf.org>
>>>> wrote:
>>>> > Hi,
>>>> >
>>>> > Is it possible to take a theory that makes definitions of
>>>> > types/constants,
>>>> > and then re-present the same theory _without_ making the definitions
>>>> > (instead taking them as ungrounded constants, and the definitional
>>>> > theorems
>>>> > as axioms).
>>>> >
>>>> > I know there is already this command:
>>>> >
>>>> > opentheory info --theorems ...
>>>> >
>>>> > which removes all the proofs, but it still keeps the definitions in.
>>>> >
>>>> > Can I also remove the definitions?
>>>> >
>>>> > In essence, I want a totally axiomatic presentation of a theory.
>>>> >
>>>> > Thanks,
>>>> > Ramana
>>>> >
>>>> > _______________________________________________
>>>> > opentheory-users mailing list
>>>> > opentheory-users at gilith.com
>>>> > http://www.gilith.com/opentheory/mailing-list
>>>> >
>>>>
>>>> _______________________________________________
>>>> opentheory-users mailing list
>>>> opentheory-users at gilith.com
>>>> http://www.gilith.com/opentheory/mailing-list
>>>
>>>
>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>