*To*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] How to access a locale type parameter in a quotient type definition*From*: mailing-list anonymous <mailing.list.anonymous at gmail.com>*Date*: Tue, 9 Jul 2019 00:53:08 +0300*Cc*: wolfgang-it at jeltsch.info

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 > 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.

**Follow-Ups**:**Re: [isabelle] How to access a locale type parameter in a quotient type definition***From:*mailing-list anonymous

**Re: [isabelle] How to access a locale type parameter in a quotient type definition***From:*Wolfgang Jeltsch

- Previous by Date: [isabelle] Isabelle server: Using JSON to request that a top level command is modified
- Next by Date: Re: [isabelle] How to access a locale type parameter in a quotient type definition
- Previous by Thread: Re: [isabelle] Isabelle server: Using JSON to request that a top level command is modified
- Next by Thread: Re: [isabelle] How to access a locale type parameter in a quotient type definition
- Cl-isabelle-users July 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list