[isabelle] comm_monoid_big not in Isabelle 2013-1



Hi

I'm trying to port some of my proofs to Isabelle 2013-1 (from Isabelle 2013).

I'm working on extending an abstract separation algebra (as previously released in AFP).

I've first showed that separation conjunction is an interpretation of comm_monoid_mult, and then defined a function sep_map_set_conj which would map a predicate over a set, and then fold the set using separation conjunction. (I've defined similar things for lists as well.)

interpretation sep: comm_monoid_mult "op **" □
  by unfold_locales (simp add: sep_conj_ac)+

definition
  sep_map_set_conj :: "('b ⇒ 'a::sep_algebra ⇒ bool) ⇒ 'b set ⇒ ('a ⇒ bool)"
where
  "sep_map_set_conj g S ≡ sep.setprod g S"


This all works fine in Isabelle 2013-1.

I then previously showed that sep_map_set_conj interprets comm_monoid_big, which gave me a lot of nice lemmas for free.

interpretation sep: comm_monoid_big "op ∧*" □ sep_map_set_conj
  by unfold_locales (simp add: sep_map_set_conj_def sep.setprod_def)

Reading the NEWS file, and browsing the sources I can see that fold_image has changed and things have been cleaned up (which I welcome completely), but I can't seem to seem to find a replacement for comm_monoid_big.

Wondering for any advice for fixing this. I can make sep_map_set_conj an abbreviation of setprod, which gives me a lot of things for free, although this seems a little inelegant. Of course, I am quite possibly doing it the wrong way, and I'm happy to change the definitions to make things easier.

Kind regards
Andrew Boyton


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


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