Email Gateway (Aug 22 2022 at 20:13): Email Gateway (Aug 22 2022 at 20:13):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
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
Email Gateway (Aug 22 2022 at 20:13):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
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 ≠ ∅ ⟹ φ
sort(β)=HOL.type]
*)
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 (
https://github.com/xanonec/HOL-TTS-Ext).
Thank you
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
Email Gateway (Aug 22 2022 at 20:13):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I forgot to mention the references that I used in the answer:
The document "Structured Formal Development with Quotient Types in
Isabelle/HOL" by Maksym Bortin and Christoph Lüth was used a general
reference
The formula for the Local Typedef Rule was copied directly from the file
"HOL/Types_To_Sets/local_typedef.ML"
The example subsumes the content of
HOL/Types_To_Sets/Examples/Prerequisites.thy
Thank you
Email Gateway (Aug 22 2022 at 20:13):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
Thanks for your elaborate answer.
Unfortunately I know nothing about “types to sets” and the mathematics
behind it. Therefore the message I’m taking from your e-mail is that
what I want isn’t supported and making it somehow supported is
complicated and gives only a partial solution.
I think for my use case it’s easiest to just define the quotient types
manually for each individual interpretation of the locale. That said,
being able to define quotient types within locales might be very useful
in other situations; thus adding some sort of support for it might be a
good idea.
All the best,Wolfgang
Email Gateway (Aug 22 2022 at 20:13):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Wolfgang Jeltsch
Therefore the message I’m taking from your e-mail is that
I believe that the opening remark in my original email was not very clear -
I was in a rush to finish the email and was slightly careless - please
accept my apologies. However, indeed, I meant to say exactly what you
inferred from it. I would also like to provide a more clear explanation of
the opening remark using the PhD thesis Ondřej Kunčar as the general
reference. Isabelle/HOL provides two definitional primitives: one for
overloaded constants and one for types (i.e. typedef). All other
definitional mechanisms (including, e.g., quotient_type) have to be defined
in terms of these primitives, provided that one does not neglect the LCF
approach. The typedef primitive allows for the definition of new types in
terms of an isomorphism with respect to an arbitrary non-empty subset of an
existing type. typedef α k = S requires S to be a closed term, k to be a
fresh type constructor and all type variables in S need to be among the
variables in α. If one is to try to define a nullary type constructor based
on an existing fixed type variable, then the last condition will be
inevitably violated. Unfortunately, provided that there is no
misunderstanding on my part, this is exactly what you were trying to do by
calling the command quotient_type with the fixed type variable occurring in
the input term and not occurring on the lhs in the specification of the
type constructor.
Also, perhaps, I can provide an explanation for another remark from your
original email "although it does accept referring to 'a in types". When
you invoke the command quotient_type, your intention is to declare a new
type constructor. Of course, the mechanism of the declaration of new type
constructors is very different from merely using a fixed type variable as
an input to the existing type constructor. Hopefully, this clarifies why
one can refer to fixed variables when constructing new types, but not new
type constructors.
Thank you
Email Gateway (Aug 22 2022 at 20:14):From: Lawrence Paulson <lp15@cam.ac.uk>
Possibly now is a good time to plug my own paper "Defining functions on equivalence classes”, which is available* from my webpage (https://www.cl.cam.ac.uk/~lp15/papers/refereed.html). In this I outline how one can create quotient constructions quite easily using the set-theoretic primitives of Isabelle/HOL. Obviously quotient_type is easier to use, but as discussed, it wants to introduce a type and there is no reason on earth to conflate quotient constructions with types.
Larry Paulson
Email Gateway (Aug 22 2022 at 20:14):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Thanks for the pointer!
Unfortunately, I cannot download the paper via that link.
All the best,
Wolfgang
Last updated: May 01 2024 at 20:18 UTC