Relaxing sort constraints for typedef axioms · Isabelle/ML

The axiom introduced by the typedef package includes any sort constraints that are present in the provided specification (as OFCLASS premises). Since the axiom itself is conditional on the representation set being nonempty, I would argue that the sort constraints are not actually necessary.

I propose that the sort constraints for the spec should be stripped before generating the typedef axiom, then re-introduced in the resulting theorem/inhabited proof obligation.

Currently the underlying axioms for definitions are stripped of any sort constraints (although the exposed theorems have them re-introduced). This allows for some limited reasoning about types introduced with typedef that have weaker sort constraints than the original typedef specification.

typedef (overloaded) 'a not_zero = "{x :: ('a:: semiring_1). x ≠ 0 }"
  by (rule exI[of _ 1]) simp
...
instantiation not_zero :: (semiring_1) one begin
lift_definition one_not_zero :: "'a::semiring_1 not_zero" is "1::'a" by simp
...

If we later relax the arity of the "one" class instance and constraint on "Abs_not_zero":

instance not_zero :: (zero_neq_one) one by standard
setup ‹
Sign.add_const_constraint (@{const_name Abs_not_zero},SOME @{typ "'a::zero_neq_one ⇒ 'a not_zero"})
›

lemma "Abs_not_zero 1 = (1 :: 'a :: zero_neq_one not_zero)"
  unfolding
    [[axiom "Scratch.one_not_zero_inst.one_not_zero_def"]]
    [[axiom "Scratch.one_not_zero_def"]]
  by (rule refl)

lemma "Rep_not_zero (1 :: 'a :: zero_neq_one not_zero) = 1"

This requires the property y ∈ {x. x ≠ 0} ⟹ Rep_not_zero (Abs_not_zero y) = y, which comes from the type_definition
axiom from typedef. Unlike the one_not_zero definition, the type_definition axiom is conditional on the sort constraint originally provided to typedef:

term ‹OFCLASS('a, semiring_1_class) ⟹ ∃x. x ∈ {x. ¬ x = 0} ⟹
type_definition Rep_not_zero Abs_not_zero {x. ¬ x = 0}›

Although the zero_neq_one class would be sufficient to prove the type is inhabited, the OFCLASS('a, semiring_1_class) constraint on the axiom means we cannot properly interpret Rep_not_zero and Abs_not_zero without the semiring_1 constraint.

I propose that the sort constraints for the spec should be stripped (down to just type) before generating the typedef axiom, then re-introduced in the resulting theorem/inhabited proof obligation.

This change would make it possible to effectively relax the sort constraints on an existing typedef (without needing additional axioms), provided that the representation set can still be shown to be nonempty under the weaker constraint.

Stream: Isabelle/ML

Topic: Relaxing sort constraints for typedef axioms

Daniel Matichuk (Oct 12 2025 at 20:30):