Re: [isabelle] Can a couple of lemmas about map_add be added?



Thank you for the lemmas, but your proofs are more complicated than is necessary and you may benefit from the following hints:

For a start, use ==> and not --> to separate assumptions from conclusions, your lemmas is easier to apply that way (and the proof is simpler because it avoids your rule+

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)

It is also possible to prove the statements by expanding the definitions (although that is usually not the best approach):

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
Description: S/MIME Cryptographic Signature



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