1 回答
HOL types cannot depend on values. So if you want to define a quotient type for an arbitrary non-empty set S and equivalence relation equiv using quotient_type, the arbitrary part must stay at the meta-level. Thus, S and equiv can either be axiomatized or defined such that you can convince yourself that you really have captured the desired notion of arbitrary.
If you axiomatize S and equiv, then you yourself are responsible that the axioms are consistent with the other axioms of HOL. You can do that with the command axiomatization as in
axiomatization S :: "'a set" where S_not_empty: "S ≠ {}"
For Isabelle/HOL, S is then a fixed constant of which you only know that it is not empty. You will never be able to instantiate S, because the arbitrariness only exists in the set-theoretic interpretation of Isabelle/HOL.
If you do not want to add new axioms, you can use specification instead:
consts S :: "'a set"
specification (S) S_not_empty: "S ≠ {}" by auto
With specification, you have to prove that your axioms are consistent, so there is no danger here. However, S no longer is absolutely arbitrary, because it is defined in terms of the choice operator Eps, as can be seen from the generated theorem S_def.
If you really want to study the theory of quotients within Isabelle/HOL, I recommend that you do not use types, but ordinary sets. There is the quotient operator op // and some theorems in the theory Equiv_Relations which is part of the library.