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



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
Am Dienstag, den 09.07.2019, 00:53 +0300 schrieb mailing-list anonymous:
> 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
> 
> 



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