[isabelle] Sublocale, subclass and execution.

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

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

Can this proof be done using sublocales without the loss of executability?

All suggestions are welcome.


Attachment: Foo.zip
Description: Zip archive

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