*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Sublocale, subclass and execution.*From*: Jose Divasón <jose.divasonm at unirioja.es>*Date*: Thu, 9 Oct 2014 12:11:29 +0200*Sender*: jose.divason at gmail.com

Dear all, I was trying to demonstrate that any field is a euclidean (semi)ring. I can't do it by means of subclasses, because they have different fixed parameters: class field = comm_ring_1 + inverse + assumes field_inverse: "a ≠ 0 ⟹ inverse a * a = 1" assumes field_divide_inverse: "a / b = a * inverse b" class euclidean_semiring = semiring_div + fixes euclidean_size :: "'a ⇒ nat" fixes normalisation_factor :: "'a ⇒ 'a" assumes ..... (*subclass (in field) euclidean_ring*) So, I did it using sublocales (see the attached file). sublocale field ⊆ field_is_euclidean_ring: euclidean_ring _ "λa b. if b = 0 then 0 else a/b" "λa b. if b = 0 then a else 0" _ _ _ "λi. if i = 0 then 0 else 1::nat" id My problem is that, before such a sublocale I can execute functions defined in the euclidean_ring class (such as gcd_eucl for naturals and integers). On the contrary, after the sublocale those functions can't be executed anymore. Maybe I'm not understanding properly how sublocales work. The use of sublocales (and then, my problem) can be avoided creating a new class fixing (and defining) the parameters presented in the euclidean_ring class: class field_euclidean = field + euclidean_ring + assumes "euclidean_size = (λi. if i = 0 then 0 else 1::nat)" and "normalisation_factor = id" Nevertheless this is a bit unsatisfactory, because a new class has to be introduced and I should instantiate each field to this new field_euclidean class (although instances would be quite easy). In the attached file there is my Isabelle theory (Foo.thy) with further explanations. Can this proof be done using sublocales without the loss of executability? All suggestions are welcome. Thanks, Jose

**Attachment:
Foo.zip**

**Follow-Ups**:**Re: [isabelle] Sublocale, subclass and execution.***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing
- Next by Date: Re: [isabelle] Sublocale, subclass and execution.
- Previous by Thread: [isabelle] New AFP entry: Formalization of Refinement Calculus for Reactive Systems
- Next by Thread: Re: [isabelle] Sublocale, subclass and execution.
- Cl-isabelle-users October 2014 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