How do I state a lemma that does not respect sort constraints (for using OFCLASS)

Question

How can I state a lemma in Isabelle/HOL that does not obey sort constraints?

To explain why that makes sense, consider the following example theory:

theory Test
imports Main
begin

class embeddable = 
  fixes embedding::"'a ⇒ nat"
  assumes "inj embedding"

lemma OFCLASS_I:
  assumes "inj (embedding::'a⇒_)"
  shows "OFCLASS('a::type,embeddable_class)"
apply intro_classes by (fact assms)

instantiation nat :: embeddable begin
definition "embedding = id"
instance
  apply (rule OFCLASS_I) unfolding embedding_nat_def by simp
end

end

This theory defines a type class "embeddable" with one type parameters "embedding". (Basically, the class embeddable characterizes countable numbers with an explicit enumeration, but I chose this simply to have a very simple example.)

To simplify instance-proofs for the type class, the theory states an auxiliary lemma OFCLASS_I that shows goals of the form OFCLASS(...,embeddable). This lemma can then be used to solve the proof obligations produced by instance.

First, why would I even want that? (In the present theory, apply (rule OFCLASS_I) does the same as the builtin apply intro_classes and hence is useless.) In more complex cases, there are two reasons for such a lemma:

• The lemma can give alternative criteria for instantiation of a type class, making subsequent proofs simpler.
• The lemma could be used in automated (ML-level) instantiations. Here using intro_classes is problematic, because the number of subgoals of intro_classes can vary depending on what instance proofs have been performed earlier. (A lemma such as OFCLASS_I has a stable, well-controlled subgoals.)

However, the above theory does not work in Isabelle/HOL (neither 2015 or 2016-RC1) because the lemma does not type-check. The sort constraint "embedding::(_::embeddable => _)" is not satisfied. However, this type contraint is not a logic necessity (it is not enforced by the logical kernel but instead of a higher level).

So, is there a clean way of stating the theory above? (I give a somewhat ugly solution in my answer, but I am looking for something cleaner.)

Answer 1

The checking of the sort constraints can be disabled temporarily on the ML-level, and reactivated afterwards. (See the complete example below.) But that solution looks very much like a hack. We have to change the sort constraints in the context, and remember to restore them afterwards.

theory Test
imports Main
begin

class embeddable = 
  fixes embedding::"'a ⇒ nat"
  assumes "inj embedding"

ML {*  
  val consts_to_unconstrain = [@{const_name embedding}]
  val consts_orig_constraints = map (Sign.the_const_constraint
                                @{theory}) consts_to_unconstrain
*}
setup {*
  fold (fn c => fn thy => Sign.add_const_constraint (c,NONE) thy) consts_to_unconstrain
*}

lemma OFCLASS_I:
  assumes "inj (embedding::'a⇒_)"
  shows "OFCLASS('a::type,embeddable_class)"
apply intro_classes by (fact assms)

(* Recover stored type constraints *)
setup {*
  fold2 (fn c => fn T => fn thy => Sign.add_const_constraint
            (c,SOME (Logic.unvarifyT_global T)) thy)
              consts_to_unconstrain consts_orig_constraints
*}

instantiation nat :: embeddable begin
definition "embedding = id"
instance
  apply (rule OFCLASS_I) unfolding embedding_nat_def by simp
end

end

This theory is accepted by Isabelle/HOL. The approach works in more complex settings (I have used it several times), but I would prefer a more elegant one.

Answer 2

The following is a different solution that does not require to "clean up" after proving the lemma (this answer requires to "repair" the sort constraints afterwards).

The idea is to define a new constant (embedding_UNCONSTRAINED in my example) that is a copy of the original sort-constrained constant (embedding), except without sort constraints (using the local_setup command below). Then the lemma is stated using embedding_UNCONSTRAINED instead of embedding. But by adding the attribute [unfolded embedding_UNCONSTRAINED_def] the lemma that is actually stored uses the constant embedding without sort constraint.

The drawback of this approach is that during the proof of the lemma, we can never explicitly write any terms containing embedding (since that will add the unwanted sort constraints). But if we need to state a subgoal containing embedding, we can always state it using embedding_UNCONSTRAINED and then use, e.g., unfolding embedding_UNCONSTRAINED to transform it into embedding.

theory Test
imports Main
begin

class embeddable = 
  fixes embedding::"'a ⇒ nat"
  assumes "inj embedding"

(* This does roughly:
   definition "embedding_UNCONSTRAINED == (embedding::('a::type)=>nat)" *)
local_setup {* 
  Local_Theory.define ((@{binding embedding_UNCONSTRAINED},NoSyn),((@{binding embedding_UNCONSTRAINED_def},[]),
      Const(@{const_name embedding},@{typ "'a ⇒ nat"}))) #> snd
*}

lemma OFCLASS_I [unfolded embedding_UNCONSTRAINED_def]:
  assumes "inj (embedding_UNCONSTRAINED::'a⇒_)"
  shows "OFCLASS('a::type,embeddable_class)"
apply intro_classes by (fact assms[unfolded embedding_UNCONSTRAINED_def])

thm OFCLASS_I (* The theorem now uses "embedding", but without sort "embeddable" *)

instantiation nat :: embeddable begin
definition "embedding = id"
instance
  apply (rule OFCLASS_I) unfolding embedding_nat_def by simp
end

end