Re: [isabelle] Porting trouble: Interpretation of locale semiring_1

```Hi Peter,

> *** Partially applied constant on left hand side of equation
> *** "semiring_1.of_nat {[]} {} op \<union> ?n \<equiv>
> semiring_1.of_nat_aux (\<lambda>i. i \<union> {[]}) ?n {}"
> *** At command "done".
>
> I do not know what this error message means, nor can I find any
> documentation.
> In Isabelle2008, the proof worked well.

The fundamental problem is that interpretation still does not work as
expected with definitions relative to locales.  In your case, the
definitions of of_nat and Nats relative to locale semiring_1 make
problems.  There is a workaround pattern:

definition
"conc A B = {xs @ ys | xs ys. xs \<in> A \<and> ys \<in> B}"

interpretation lc_monoid: monoid_mult "{[]}" conc
apply unfold_locales
sorry

-- {* define explicit constants for the interpretation results of of_nat
and Nats *}

definition
"regset_of_nat = semiring_1.of_nat {[]} {} (op \<union>)"

definition
"regset_Nats = semiring_1.Nats {[]} {} (op \<union>)"

interpretation regset_semiring: semiring_1 "{[]}" conc "{}" "op
\<union>" where

-- {* fold interpretation results of of_nat and Nats to the
corresponding global constants *}

"semiring_1.of_nat {[]} {} (op \<union>) = regset_of_nat"
and "semiring_1.Nats {[]} {} (op \<union>) = regset_Nats"
proof -
show "semiring_1 {[]} conc {} (op \<union>)"
by unfold_locales (auto simp add: conc_def)

Ugly, but working;  we hope to repair this problem once and forall in
the next Isabelle release.

Hope this helps
Florian

--

Home:
http://wwwbroy.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

```

Attachment: signature.asc
Description: OpenPGP digital signature

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