Email Gateway (Aug 22 2022 at 14:04): Email Gateway (Aug 22 2022 at 14:04):From: Andrea Giugliano <ag400@leicester.ac.uk>
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
Email Gateway (Aug 22 2022 at 14:04):From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s
Last updated: Apr 23 2024 at 20:15 UTC