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



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




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