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)
qed (simp_all add: regset_of_nat_def regset_Nats_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.