[isabelle] comm_monoid_big not in Isabelle 2013-1
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)+
sep_map_set_conj :: "('b ⇒ 'a::sep_algebra ⇒ bool) ⇒ 'b set ⇒ ('a ⇒ bool)"
"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.
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