Hi Esseger, unfortunately, it is not possible in Isabelle to define two different type class instances on the same type.
An alternative is to work on a copy of your type. There is even an example for your specific problem, "'a discrete" gives you a discrete topology on 'a: http://isabelle.in.tum.de/repos/isabelle/file/tip/src/HOL/Probability/Discrete_Topology.thy A solution in Isabelle might be to use locales, which are more flexible, but also less automated and more difficult to work with. For a similar approach see the Topology AFP-entry: http://afp.sourceforge.net/browser_info/current/AFP/Topology/Topology.html Also related, in HOL Light topologies and metrics are introduced as predicates: https://code.google.com/p/hol-light/source/detail?r=220 Btw, it may be better to ask further questions about Isabelle, Isar, and type classes on the Isabelle mailing list: [email protected] Greetings, Johannes Am Montag, den 01.06.2015, 08:25 +0200 schrieb Esseger: > Le 01/06/2015 00:18, Rob Arthan a écrit : > > > A topological space (in set theory) comprises a pair (X, O) where X is a set > > and O, the set of open subsets of X, is a subset of the powerset of X > > satisfying > > certain conditions. What is the problem in translating this into HOL? This > > has > > already been done for most (or all?) of the various incarnations of HOL. > > Sure, there is no difficulty on the mathematical side, and there is no > difficulty on the HOL side if everything is written in terms of pairs > (X,O) as you suggest. My problem is that I want to use existing > theories, in which I do not see how to write a statement on the same set > involving different topologies. > > In Isabelle/HOL/Topological_Spaces.thy, for instance, topological spaces > are implemented based on a predicate open from 'a set to bool. Then, for > instance, a function f is continuous on X, written continuous f X, if > the preimage of any open set is open in X. But this expression, > "continuous f X", only contains implicitly the reference to the topology > on X. > > So, my problem is really just a notational problem: how do I define two > different predicates 'open' on a set X, how do I write "continuous f X" > to refer to one topology in the source and another one in the target, > and so on. Of course, I do not want to reinvent the wheel and reprove > all statements in a new theory where all topologies at source and goal > are given explicitely! > > Regards, > Esseger ------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
