[opentheory-users] Local definitions in theory packages

Joe Leslie-Hurd joe at gilith.com
Mon Nov 24 19:13:08 UTC 2014

There have been several discussions on this list about symbols (i.e.,
type operators and constants) that are defined in a theory but are not
mentioned in any exported theorem, which Rob named local definitions.
Since most of the HOL family of theorem provers maintain a global
symbol table, these local definitions can cause problems if they have
clashing names.

Up until now it's been difficult to see the complete set of symbols
referred to inside a theory, but this can now be displayed with the
opentheory info --symbols command (I append the output for the most
recent version of the standard theory library: base-1.169). As can be
seen, most of the local definitions (which are the symbols in the
HOLLight namespace) are abstraction and representation functions for
type definitions, but there are also others such as those that are
used to construct the real numbers.

In my opinion it would make theories more elegant if (some of) these
local definitions could be removed, but in the meantime I'd like to
know of any instances with clashing local definitions (these could
occur either in the same theory or across different theories). My
current belief is that these should be easy to fix in a natural way,
but I need to see some concrete examples.




$ opentheory info --symbols base
3 external type operators: -> bool ind
2 external constants: = select
11 defined type operators: Data.List.list Data.Option.option Data.Pair.*
  Data.Sum.+ Data.Unit.unit HOLLight.hreal HOLLight.nadd HOLLight.recspace
  Number.Natural.natural Number.Real.real Set.set
210 defined constants: ! /\ ==> ? ?! \/ ~ cond F T Data.List.:: Data.List.@
  Data.List.[] Data.List.all Data.List.any Data.List.case.[].::
  Data.List.concat Data.List.drop Data.List.filter Data.List.foldl
  Data.List.foldr Data.List.fromSet Data.List.head Data.List.interval
  Data.List.last Data.List.length Data.List.map Data.List.member
  Data.List.nth Data.List.nub Data.List.nubReverse Data.List.null
  Data.List.replicate Data.List.reverse Data.List.tail Data.List.take
  Data.List.toSet Data.List.zip Data.List.zipWith
  Data.Option.case.none.some Data.Option.isNone Data.Option.isSome
  Data.Option.map Data.Option.none Data.Option.some Data.Pair.,
  Data.Pair.fst Data.Pair.snd Data.Sum.case.left.right Data.Sum.destLeft
  Data.Sum.destRight Data.Sum.isLeft Data.Sum.isRight Data.Sum.left
  Data.Sum.right Data.Unit.() Function.^ Function.const Function.flip
  Function.id Function.injective Function.o Function.surjective
  Function.Combinator.s Function.Combinator.w HOLLight._dest_list
  HOLLight._dest_option HOLLight._dest_rec HOLLight._dest_sum
  HOLLight._mk_list HOLLight._mk_option HOLLight._mk_rec HOLLight._mk_sum
  HOLLight.dest_hreal HOLLight.dest_nadd HOLLight.dest_num
  HOLLight.dest_real HOLLight.dest_set HOLLight.hreal_add
  HOLLight.hreal_inv HOLLight.hreal_le HOLLight.hreal_mul
  HOLLight.hreal_of_num HOLLight.is_nadd HOLLight.mk_hreal HOLLight.mk_nadd
  HOLLight.mk_num HOLLight.mk_pair HOLLight.mk_real HOLLight.nadd_add
  HOLLight.nadd_eq HOLLight.nadd_inv HOLLight.nadd_le HOLLight.nadd_mul
  HOLLight.nadd_of_num HOLLight.nadd_rinv HOLLight.one_ABS HOLLight.one_REP
  HOLLight.treal_add HOLLight.treal_eq HOLLight.treal_inv HOLLight.treal_le
  HOLLight.treal_mul HOLLight.treal_neg HOLLight.treal_of_num
  HOLLight.ZCONSTR HOLLight.ZRECSPACE Number.Natural.* Number.Natural.+
  Number.Natural.- Number.Natural.< Number.Natural.<= Number.Natural.>
  Number.Natural.>= Number.Natural.^ Number.Natural.bit0
  Number.Natural.bit1 Number.Natural.distance Number.Natural.div
  Number.Natural.even Number.Natural.factorial Number.Natural.isSuc
  Number.Natural.log Number.Natural.max Number.Natural.min
  Number.Natural.minimal Number.Natural.mod Number.Natural.odd
  Number.Natural.pre Number.Natural.suc Number.Natural.zero Number.Real.*
  Number.Real.+ Number.Real.- Number.Real./ Number.Real.< Number.Real.<=
  Number.Real.> Number.Real.>= Number.Real.^ Number.Real.~ Number.Real.abs
  Number.Real.fromNatural Number.Real.inv Number.Real.max Number.Real.min
  Number.Real.sup Relation.bigIntersect Relation.bigUnion Relation.empty
  Relation.fromSet Relation.intersect Relation.irreflexive Relation.measure
  Relation.reflexive Relation.subrelation Relation.toSet
  Relation.transitive Relation.transitiveClosure Relation.union
  Relation.universe Relation.wellFounded Set.{} Set.bigIntersect
  Set.bigUnion Set.bijections Set.choice Set.cross Set.delete
  Set.difference Set.disjoint Set.finite Set.fold Set.fromPredicate
  Set.hasSize Set.image Set.infinite Set.injections Set.insert
  Set.intersect Set.member Set.properSubset Set.rest Set.singleton Set.size
  Set.subset Set.surjections Set.union Set.universe

More information about the opentheory-users mailing list