[opentheory-users] Local definitions in theory packages

[Joe Leslie-Hurd]

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.

Cheers,

Joe

______________________________________________________

$ 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.ABS_prod HOLLight.BOTTOM HOLLight.CONSTR HOLLight.FCONS
  HOLLight.FINREC HOLLight.FNIL HOLLight.IND_0 HOLLight.IND_SUC
  HOLLight.INJA HOLLight.INJF HOLLight.INJN HOLLight.INJP HOLLight.NUMFST
  HOLLight.NUMLEFT HOLLight.NUMPAIR HOLLight.NUMRIGHT HOLLight.NUMSND
  HOLLight.NUMSUM HOLLight.NUM_REP HOLLight.REP_prod HOLLight.ZBOT
  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