Re: [isabelle] How to access a locale type parameter in a quotient type definition

Dear Wolfgang Jeltsch,

I am not an expert in this subject and, hopefully, someone more
knowledgeable will correct me if I am wrong. However, as far as I know,
even the plain typedecl does not accept fixed type variables.  Of course,
internally the command quotient_type relies on the same mechanism for the
declaration of new types. Therefore, it is not possible to use the command
quotient_type to obtain the result that you need.

Anecdotally, the Local Typedef Rule (LT) axiom associated with
Types-To-Sets can be used to solve the problem that you are dealing with,
but, as far as I know, with some restrictions. Effectively, the Local
Typedef Rule (LT) states the following:

Local Typedef Rule (LT)

  Γ ⊢ (∃(Rep::β ⇒ τ) Abs. type_definition Rep Abs A) ⟹ φ
[β not in φ, Γ, A;
                       Γ ⊢ A ≠ ∅ ⟹ φ

Given that Rep, Abs and A are arbitrary (of course, A should not be empty),
it is not too difficult to define the ones suitable for a quotient type for
some relation R. Nevertheless, there is a restriction "β not in φ", which,
for your problem, might be too much to bear. In essence, you will be able
to use β as the quotient type, prove theorems about it, but these theorems
can only be used within the context with the assumption "∃(Rep::β ⇒ τ set)
Abs. type_definition Rep Abs A". To use them outside of this context, you
will need to transfer them back to the original type τ. This process can be
automated completely using the capabilities of the transfer package.
Nevertheless, I appreciate that this may be a substantial restriction for
your use case.

The example below demonstrates, vaguely, how the 'Local Quotient Rule'
might work (of course, you need to import Types-To-Sets from the main
library to run the example). If you are interested, I can add something
akin to a 'Local Quotient Rule' (which would, effectively, hide all the
ugly details in the example below and complete it with the instantiation of
all quotient theorems and transfer rules) to my extension of Types-To-Sets (

Thank you

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

(*The exposition subsumes some of the content of
  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"

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,
  and left_unique_cr_S = typedef_left_unique[OF type_definition_S cr_S_def,
  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
    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'))
      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
  then show "∀a. Abs (Abs' (rep' (rep a))) = a" by auto

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)

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)

(* 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


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


> Hi! Consider the following attempt of a locale definition: locale example =
> fixes R :: "['a, 'a] ⇒ bool"
> assumes is_equivalence: "equivp R"
> begin
> quotient_type Q = 'a / R
> end Isabelle doesn’t accept the use of the type variable `'a` in the
> quotient type definition, although it does accept referring to `'a` in
> types. How can I define a quotient type for the type `'a`? All the best,
> Wolfgang

Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.