Re: [isabelle] Status of HOL/Import



On Tue, Jul 12, 2011 at 5:05 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:
> Alas, nobody has been using this for some time and it has fallen into
> disrepair. If you can get it to work again, you are very welcome!

I pushed the changes to the repository. Apart from small modifications
to existing compat theorems that made it work with current HOL Light
and adapting to current Isabelle the changes are:

I added about 100 new constant maps along with compat theorems which
means many theorems can be translated to ones talking about Isabelle
constants, in particular theorems about lists, sets (union, ...)  and
number theory (gcd, ...) are translated now.

I also tried to add maps for reals and integers; this works only
partially so I do not enable it by default in the build. Enabling
those allows translating theorems that talk about reals and integers
to Isabelle reals and integers but it fails for more complicated types
that are based on reals, mostly because I have not been able to map
'mk_real'. Without these maps all theorems are translated correctly to
copies or reals and integers.

I also needed to update 'smart_string_of_thm' as it was failing for
all theorems and I was getting the fully bracketed output.

Cezary

> Am 12/07/2011 09:56, schrieb Cezary Kaliszyk:
>> Dear all,
>>
>> After some struggling I succeeded running HOL/Import for HOLLight.
>> (I wanted to port some of my older HOL-Light developments)
>>
>> The files present in the current repository version of Isabelle
>> seem not to have been updated for quite a while (they still use
>> the syntax "theory = ... + ..." which doesn't work for a while).
>> Also the generation script refers to HOLLight constants not present
>> at least since early 2005.
>>
>> Is anyone using HOL/Import or the theorems translated from HOLLight
>> or can I update the generation and compatibility scripts to work
>> with current Isabelle and svn HOLLight, add some constant maps
>> and update the generated theorems?
>>
>> Cezary
>
>





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