[opentheory-users] reuse lemmas in article format

[Joe Leslie-Hurd]

Hi Francois,

The short answer is: it's not possible, it's up to the system to map
theorems to names and vice versa.

The reason is that different systems will have different names for the
same theorem, and I didn't want to create standard names for every
theorem like we do for type operators and constants.

Here's one way to do that. When I made a HOL Light interface to
OpenTheory, I added some extra files to my packages, for example:

$ opentheory info --files natural-prime
natural-prime.thy
hol-light.int
hol-light.art
haskell.int
haskell.art
haskell-test.art

The hol-light.int contains the name mappings of type operators and
constants from OpenTheory to HOL Light:

$ cat `opentheory info --directory natural-prime`/hol-light.int
###############################################################################
# HOL Light interpretation for prime natural numbers
###############################################################################

# Number

# Number.Natural

const "Number.Natural.prime" as "HOLLight.prime"

# Number.Natural.Prime

const "Number.Natural.Prime.all" as "HOLLight.primes"
const "Number.Natural.Prime.below" as "HOLLight.primes_below"

# Number.Natural.Prime.Sieve

type "Number.Natural.Prime.Sieve.sieve" as "HOLLight.sieve"

const "Number.Natural.Prime.Sieve.dest" as "HOLLight.dest_sieve"
const "Number.Natural.Prime.Sieve.increment" as "HOLLight.inc_sieve"
const "Number.Natural.Prime.Sieve.increment.inc" as
"HOLLight.inc_counters_sieve"
const "Number.Natural.Prime.Sieve.initial" as "HOLLight.init_sieve"
const "Number.Natural.Prime.Sieve.invariant" as "HOLLight.is_sieve"
const "Number.Natural.Prime.Sieve.invariant.inv" as "HOLLight.is_counters_sieve"
const "Number.Natural.Prime.Sieve.max" as "HOLLight.max_sieve"
const "Number.Natural.Prime.Sieve.mk" as "HOLLight.mk_sieve"
const "Number.Natural.Prime.Sieve.next" as "HOLLight.next_sieve"
const "Number.Natural.Prime.Sieve.primes" as "HOLLight.primes_sieve"

The hol-light.art file annotates each theorem with its HOL Light name:

$ opentheory info `opentheory info --directory natural-prime`/hol-light.art
...
59 theorems:
  |- let prime_zero <- ~Number.Natural.prime 0 in prime_zero
  |- let prime_one <- ~Number.Natural.prime 1 in prime_one
  |- let prime_two <- Number.Natural.prime 2 in prime_two
  |- let prime_three <- Number.Natural.prime 3 in prime_three
  |- let primes_below_zero <-
         Number.Natural.Prime.below 0 = Data.List.[] in
     primes_below_zero
  |- let primes_src <-
         Number.Natural.Prime.all =
         Data.Stream.unfold Number.Natural.Prime.Sieve.next
           Number.Natural.Prime.Sieve.initial in
     primes_src
...

Then when reading the theorems into HOL Light from the main article
file you can compare each one against a file like this to recover its
system name.

Hope that helps,

Joe