[opentheory-users] reuse lemmas in article format
Joe Leslie-Hurd
joe at gilith.com
Wed May 17 17:31:36 UTC 2017
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
More information about the opentheory-users
mailing list