0

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

Community
  • 1
  • 1
qartal
  • 2,024
  • 19
  • 31

1 Answers1

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.

Community
  • 1
  • 1
Andreas Lochbihler
  • 4,998
  • 12
  • 10
  • thanks, Is there any theorem prover based on a logic which support subtyping that I can use? – qartal Nov 11 '14 at 14:14