[opentheory-users] Local definitions in theory packages

[Mario Carneiro]

I expect that it will be impossible to remove most of the local definitions
that you are talking about, because they serve an important purpose: they
are useful for "forgetting" about constructions. Once you've proven that
the reals have the desired properties, it no longer becomes important what
sequence of embeddings was used to build the Real type in the first place,
and indeed there is an aesthetic in proofs which avoid any reference to
such "construction-dependent" properties. (This process is made explicit in
Metamath, where we derive the basic properties of the reals, then ignore
these proofs and replace them with axioms so that you can't use the
construction any more but are forced to use only the properties.) A similar
argument applies to the abstraction and representation functions - unless
you are going to be moving between the types often, you may as well forget
about these functions once the basic properties of the new type are
established.

These are new constants whose construction is mandated by the language. You
can't make a new type without getting abs,rep functions out. You can't
construct a derived type without constructing the base type first. Once you
have the constants, but you no longer need them, what are you supposed to
do with them?

Mario

On Mon, Nov 24, 2014 at 2:13 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> 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
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141124/94988d39/attachment-0001.html>