<div dir="ltr"><div><div><div><div>It's a scoping issue. I think that Peter Homeier's HOL-Omega<br></div>can quantify/bind the local constants used to construct datatypes,<br>for example. So its rules may provide guidance on what OpenTheory<br></div>should do.<br><br></div>Sorry, I know I am not answering the original question.<br><br></div>Konrad.<br><br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Nov 24, 2014 at 1:32 PM, Mario Carneiro <span dir="ltr"><<a href="mailto:di.gama@gmail.com" target="_blank">di.gama@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div>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.<br><br></div>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?<span class="HOEnZb"><font color="#888888"><br><br></font></span></div><span class="HOEnZb"><font color="#888888">Mario<br></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Nov 24, 2014 at 2:13 PM, Joe Leslie-Hurd <span dir="ltr"><<a href="mailto:joe@gilith.com" target="_blank">joe@gilith.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">There have been several discussions on this list about symbols (i.e.,<br>
type operators and constants) that are defined in a theory but are not<br>
mentioned in any exported theorem, which Rob named local definitions.<br>
Since most of the HOL family of theorem provers maintain a global<br>
symbol table, these local definitions can cause problems if they have<br>
clashing names.<br>
<br>
Up until now it's been difficult to see the complete set of symbols<br>
referred to inside a theory, but this can now be displayed with the<br>
opentheory info --symbols command (I append the output for the most<br>
recent version of the standard theory library: base-1.169). As can be<br>
seen, most of the local definitions (which are the symbols in the<br>
HOLLight namespace) are abstraction and representation functions for<br>
type definitions, but there are also others such as those that are<br>
used to construct the real numbers.<br>
<br>
In my opinion it would make theories more elegant if (some of) these<br>
local definitions could be removed, but in the meantime I'd like to<br>
know of any instances with clashing local definitions (these could<br>
occur either in the same theory or across different theories). My<br>
current belief is that these should be easy to fix in a natural way,<br>
but I need to see some concrete examples.<br>
<br>
Cheers,<br>
<br>
Joe<br>
<br>
______________________________________________________<br>
<br>
$ opentheory info --symbols base<br>
3 external type operators: -> bool ind<br>
2 external constants: = select<br>
11 defined type operators: Data.List.list Data.Option.option Data.Pair.*<br>
Data.Sum.+ Data.Unit.unit HOLLight.hreal HOLLight.nadd HOLLight.recspace<br>
Number.Natural.natural Number.Real.real Set.set<br>
210 defined constants: ! /\ ==> ? ?! \/ ~ cond F T Data.List.:: Data.List.@<br>
Data.List.[] Data.List.all Data.List.any Data.List.case.[].::<br>
Data.List.concat Data.List.drop Data.List.filter Data.List.foldl<br>
Data.List.foldr Data.List.fromSet Data.List.head Data.List.interval<br>
Data.List.last Data.List.length Data.List.map Data.List.member<br>
Data.List.nth Data.List.nub Data.List.nubReverse Data.List.null<br>
Data.List.replicate Data.List.reverse Data.List.tail Data.List.take<br>
Data.List.toSet Data.List.zip Data.List.zipWith<br>
Data.Option.case.none.some Data.Option.isNone Data.Option.isSome<br>
Data.Option.map Data.Option.none Data.Option.some Data.Pair.,<br>
Data.Pair.fst Data.Pair.snd Data.Sum.case.left.right Data.Sum.destLeft<br>
Data.Sum.destRight Data.Sum.isLeft Data.Sum.isRight Data.Sum.left<br>
Data.Sum.right Data.Unit.() Function.^ Function.const Function.flip<br>
Function.id Function.injective Function.o Function.surjective<br>
Function.Combinator.s Function.Combinator.w HOLLight._dest_list<br>
HOLLight._dest_option HOLLight._dest_rec HOLLight._dest_sum<br>
HOLLight._mk_list HOLLight._mk_option HOLLight._mk_rec HOLLight._mk_sum<br>
HOLLight.dest_hreal HOLLight.dest_nadd HOLLight.dest_num<br>
HOLLight.dest_real HOLLight.dest_set HOLLight.hreal_add<br>
HOLLight.hreal_inv HOLLight.hreal_le HOLLight.hreal_mul<br>
HOLLight.hreal_of_num HOLLight.is_nadd HOLLight.mk_hreal HOLLight.mk_nadd<br>
HOLLight.mk_num HOLLight.mk_pair HOLLight.mk_real HOLLight.nadd_add<br>
HOLLight.nadd_eq HOLLight.nadd_inv HOLLight.nadd_le HOLLight.nadd_mul<br>
HOLLight.nadd_of_num HOLLight.nadd_rinv HOLLight.one_ABS HOLLight.one_REP<br>
HOLLight.treal_add HOLLight.treal_eq HOLLight.treal_inv HOLLight.treal_le<br>
HOLLight.treal_mul HOLLight.treal_neg HOLLight.treal_of_num<br>
HOLLight.ABS_prod HOLLight.BOTTOM HOLLight.CONSTR HOLLight.FCONS<br>
HOLLight.FINREC HOLLight.FNIL HOLLight.IND_0 HOLLight.IND_SUC<br>
HOLLight.INJA HOLLight.INJF HOLLight.INJN HOLLight.INJP HOLLight.NUMFST<br>
HOLLight.NUMLEFT HOLLight.NUMPAIR HOLLight.NUMRIGHT HOLLight.NUMSND<br>
HOLLight.NUMSUM HOLLight.NUM_REP HOLLight.REP_prod HOLLight.ZBOT<br>
HOLLight.ZCONSTR HOLLight.ZRECSPACE Number.Natural.* Number.Natural.+<br>
Number.Natural.- Number.Natural.< Number.Natural.<= Number.Natural.><br>
Number.Natural.>= Number.Natural.^ Number.Natural.bit0<br>
Number.Natural.bit1 Number.Natural.distance Number.Natural.div<br>
Number.Natural.even Number.Natural.factorial Number.Natural.isSuc<br>
Number.Natural.log Number.Natural.max Number.Natural.min<br>
Number.Natural.minimal Number.Natural.mod Number.Natural.odd<br>
Number.Natural.pre Number.Natural.suc Number.Natural.zero Number.Real.*<br>
Number.Real.+ Number.Real.- Number.Real./ Number.Real.< Number.Real.<=<br>
Number.Real.> Number.Real.>= Number.Real.^ Number.Real.~ Number.Real.abs<br>
Number.Real.fromNatural Number.Real.inv Number.Real.max Number.Real.min<br>
Number.Real.sup Relation.bigIntersect Relation.bigUnion Relation.empty<br>
Relation.fromSet Relation.intersect Relation.irreflexive Relation.measure<br>
Relation.reflexive Relation.subrelation Relation.toSet<br>
Relation.transitive Relation.transitiveClosure Relation.union<br>
Relation.universe Relation.wellFounded Set.{} Set.bigIntersect<br>
Set.bigUnion Set.bijections Set.choice Set.cross Set.delete<br>
Set.difference Set.disjoint Set.finite Set.fold Set.fromPredicate<br>
Set.hasSize Set.image Set.infinite Set.injections Set.insert<br>
Set.intersect Set.member Set.properSubset Set.rest Set.singleton Set.size<br>
Set.subset Set.surjections Set.union Set.universe<br>
<br>
_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com" target="_blank">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
</blockquote></div><br></div>
</div></div><br>_______________________________________________<br>
opentheory-users mailing list<br>
<a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a><br>
<a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a><br>
<br></blockquote></div><br></div>