*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Can a couple of lemmas about map_add be added?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 9 Sep 2016 13:10:29 +0200*In-reply-to*: <87oa3yk0gj.fsf@leicester.ac.uk>*References*: <87oa3yk0gj.fsf@leicester.ac.uk>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.3.0

Both proofs are found automatically by sledgehammer: lemma map_addE1: "map_le f g ==> f++g = g" by (simp add: map_add_le_mapI map_le_antisym) lemma map_addE2: "map_le f g ==> (g++f = g)" by (metis map_addE1 map_le_iff_map_add_commute)

lemma map_addE1: "map_le f g ==> (f++g = g)" by (force simp add: map_le_def map_add_def fun_eq_iff split: option.split) The key trick here is to split the case expression automatically. Tobias On 08/09/2016 15:03, Andrea Giugliano wrote:

Hello everyone, I am working with the Map theory, and I found really useful these lemmas: lemma map_addE1: "map_le f g --> (f++g = g)" apply (simp add:map_le_def) apply (simp add:map_add_def) apply rule+ apply (case_tac " g x",force,force) done lemma map_addE2: "map_le f g --> (g++f = g)" apply (simp add:map_le_def) apply (simp add:map_add_def) apply rule+ apply (case_tac " f x",force,force) done Maybe someone can add them to the Map theory? Thanks, Andrea Giugliano

**Attachment:
smime.p7s**

**References**:**[isabelle] Can a couple of lemmas about map_add be added?***From:*Andrea Giugliano

- Previous by Date: Re: [isabelle] Reconciling FinFuns in Distro and AFP
- Next by Date: Re: [isabelle] Reconciling FinFuns in Distro and AFP
- Previous by Thread: [isabelle] Can a couple of lemmas about map_add be added?
- Next by Thread: [isabelle] new in the AFP: Iptables_Semantics
- Cl-isabelle-users September 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list