Using the type-to-sets approach for defining quotients

Question

Isabelle has some automation for quotient reasoning through the quotient package. I would like to see if that automation is of any use for my example. The relevant definitions is:

definition e_proj where "e_proj = e'_aff_bit // gluing"

So I try to write:

typedef e_aff_t = e'_aff_bit
quotient_type e_proj_t = "e'_aff_bit" / "gluing

However, I get the error:

Extra type variables in representing set: "'a" The error(s) above occurred in typedef "e_aff_t"

Because as Manuel Eberl explains here, we cannot have type definitions that depend on type parameters. In the past, I was suggested to use the type-to-sets approach.

How would that approach work in my example? Would it lead to more automation?

Answer 1

In the past, I was suggested to use the type-to-sets approach ...

The suggestion that was made in my previous answer was to use the standard set-based infrastructure for reasoning about quotients. I only mentioned that there exist other options for completeness.

---

I still believe that it is best not to use Types-To-Sets, provided that the definition of a quotient type is the only reason why you wish to use Types-To-Sets:

1. Even with Types-To-Sets, you will only be able to mimic the behavior of a quotient type in a local context with certain additional assumptions. Upon leaving the local context, the theorems that use locally defined quotient types would need to be converted to the set-based theorems that would inevitably rely on the standard set-based infrastructure for reasoning about quotients.
2. One would need to develop additional Isabelle/ML infrastructure before Local Typedef Rule can be used to define quotient types locally conveniently. It should not be too difficult to develop an infrastructure that is useable, but it would take some time to develop something that is universally applicable. Personally, I do not consider this application to be sufficiently important to invest my time in it.

In my view, it is only viable to use Types-To-Sets for the definition of quotient types locally if you are already using Types-To-Sets for its intended purpose in a given development. Then, the possibility of using the framework for the definition of quotient types locally can be seen as a 'value-added benefit'.

---

For completeness, I provide an example that I developed for an answer on the mailing list some time ago. Of course, this is merely the demonstration of the concept, not a solution that can be used for work that is meant to be published in some form. To make this useable, one would need to convert this development to an Isabelle/ML command that would take care of all the details automatically.

theory Scratch
  imports Main
    "HOL-Types_To_Sets.Prerequisites"
    "HOL-Types_To_Sets.Types_To_Sets"
begin


locale local_typedef =
  fixes R :: "['a, 'a] ⇒ bool"
  assumes is_equivalence: "equivp R"
begin

(*The exposition subsumes some of the content of
 HOL/Types_To_Sets/Examples/Prerequisites.thy*)
context
  fixes S and s :: "'s itself"
  defines S: "S ≡ {x. ∃u. x = {v. R u v}}"
  assumes Ex_type_definition_S:
    "∃(Rep::'s ⇒ 'a set) (Abs::'a set ⇒ 's). type_definition Rep Abs S"
begin

definition "rep = fst (SOME (Rep::'s ⇒ 'a set, Abs). type_definition Rep
Abs S)"
definition "Abs = snd (SOME (Rep::'s ⇒ 'a set, Abs). type_definition Rep
Abs S)"

definition "rep' a = (SOME x. a ∈ S ⟶ x ∈ a)"
definition "Abs' x = (SOME a. a ∈ S ∧ a = {v. R x v})"

definition "rep'' = rep' o rep"
definition "Abs'' = Abs o Abs'"

lemma type_definition_S: "type_definition rep Abs S"
  unfolding Abs_def rep_def split_beta'
  by (rule someI_ex) (use Ex_type_definition_S in auto)

lemma rep_in_S[simp]: "rep x ∈ S"
  and rep_inverse[simp]: "Abs (rep x) = x"
  and Abs_inverse[simp]: "y ∈ S ⟹ rep (Abs y) = y"
  using type_definition_S
  unfolding type_definition_def by auto

definition cr_S where "cr_S ≡ λs b. s = rep b"
lemmas Domainp_cr_S = type_definition_Domainp[OF type_definition_S
cr_S_def, transfer_domain_rule]
lemmas right_total_cr_S = typedef_right_total[OF type_definition_S
cr_S_def, transfer_rule]
  and bi_unique_cr_S = typedef_bi_unique[OF type_definition_S cr_S_def,
transfer_rule]
  and left_unique_cr_S = typedef_left_unique[OF type_definition_S cr_S_def,
transfer_rule]
  and right_unique_cr_S = typedef_right_unique[OF type_definition_S
cr_S_def, transfer_rule]

lemma cr_S_rep[intro, simp]: "cr_S (rep a) a" by (simp add: cr_S_def)
lemma cr_S_Abs[intro, simp]: "a∈S ⟹ cr_S a (Abs a)" by (simp add: cr_S_def)

(* this part was sledgehammered - please do not pay attention to the
(absence of) proof style *)
lemma r1: "∀a. Abs'' (rep'' a) = a"
  unfolding Abs''_def rep''_def comp_def
proof-
  {
    fix s'
    note repS = rep_in_S[of s']
    then have "∃x. x ∈ rep s'" using S equivp_reflp is_equivalence by force
    then have "rep' (rep s') ∈ rep s'"
      using repS unfolding rep'_def by (metis verit_sko_ex')
    moreover with is_equivalence repS have "rep s' = {v. R (rep' (rep s'))
v}"
      by (smt CollectD S equivp_def)
    ultimately have arr: "Abs' (rep' (rep s')) = rep s'"
      unfolding Abs'_def by (smt repS some_sym_eq_trivial verit_sko_ex')
    have "Abs (Abs' (rep' (rep s'))) = s'" unfolding arr by (rule
rep_inverse)
  }
  then show "∀a. Abs (Abs' (rep' (rep a))) = a" by auto
qed

lemma r2: "∀a. R (rep'' a) (rep'' a)"
  unfolding rep''_def rep'_def
  using is_equivalence unfolding equivp_def by blast

lemma r3: "∀r s. R r s = (R r r ∧ R s s ∧ Abs'' r = Abs'' s)"
  apply(intro allI)
  apply standard
  subgoal unfolding Abs''_def Abs'_def
    using is_equivalence unfolding equivp_def by auto
  subgoal unfolding Abs''_def Abs'_def
    using is_equivalence unfolding equivp_def
    by (smt Abs''_def Abs'_def CollectD S comp_apply local.Abs_inverse
mem_Collect_eq someI_ex)
  done

definition cr_Q where "cr_Q = (λx y. R x x ∧ Abs'' x = y)"

lemma quotient_Q: "Quotient R Abs'' rep'' cr_Q"
  unfolding Quotient_def
  apply(intro conjI)
  subgoal by (rule r1)
  subgoal by (rule r2)
  subgoal by (rule r3)
  subgoal by (rule cr_Q_def)
  done

(* instantiate the quotient lemmas from the theory Lifting *)
lemmas Q_Quotient_abs_rep = Quotient_abs_rep[OF quotient_Q]
(*...*)

(* prove the statements about the quotient type 's *)
(*...*)

(* transfer the results back to 'a using the capabilities of transfer -
not demonstrated in the example *)
lemma aa: "(a::'a) = (a::'a)"
  by auto

end

thm aa[cancel_type_definition]
(* this shows {x. ∃u. x = {v. R u v}} ≠ {} ⟹ ?a = ?a *)

end

---