Re: [isabelle] comm_monoid_big not in Isabelle 2013-1



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
> begin
> 
> definition 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
> qed
>
> end

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
> qed
>
> end

(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.
> 

-- 

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.