Email Gateway (Aug 19 2022 at 13:00): Email Gateway (Aug 19 2022 at 13:00):From: Andrew Boyton <Andrew.Boyton@nicta.com.au>
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.
Email Gateway (Aug 19 2022 at 13:03):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andrew,
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)
following the pattern from Big_Operators.thy for setprod,
context comm_monoid_mult
begindefinition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
where
"setprod = comm_monoid_set.F times 1"sublocale setprod!: comm_monoid_set times 1
where
"comm_monoid_set.F times 1 = setprod"
proof -
show "comm_monoid_set times 1" ..
then interpret setprod!: comm_monoid_set times 1 .
from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
qedend
I guess you should start with something like
definition sep_map_set_conj :: …
where
"sep_map_set_conj = comm_monoid_set.F (op **) □"sublocale sep_map_set_conj!: comm_monoid_set (op **) □
where
"comm_monoid_set.F (op **) □ = sep_map_set_conj"
proof -
show "comm_monoid_set.F (op **) □" …
then interpret sep_map_set_conj!: comm_monoid_set (op **) □ .
from sep_map_set_conj show "comm_monoid_set.F (op **) □ =
sep_map_set_conj" by rule
qedend
(not tested by myself).
Hope this helps,
Florian
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.
Last updated: Apr 24 2024 at 12:33 UTC