How to define Subtypes in Isabelle and what they mean?

Question

The question regarding subtyping in Isabelle is very lengthy here. So my simple question is that how I can define type B to be a subtype of A if I define A as below:

typedecl A

By doing this I would like to make all operations and relations defined over A (they are not printed here) accessible to elements of type B.

A bit more complex example is to define B and C to be subtype of A such that B and C are disjoint, and every element of A is either of type B or of type C.

Thanks

Answer 1

Isabelle does not have subtypes, although some aspects of subtyping can be emulated as explained in another thread. If you want to use the same operation on different types, you may want to look into Isabelle's type classes.