Email Gateway (Aug 22 2022 at 18:07): Email Gateway (Aug 22 2022 at 18:07):From: Lars Hupel <hupel@in.tum.de>
Dear BNF experts,
I was wondering whether there is an elegant way to prove such properties
about BNFs:
lemma fmmap_total:
assumes "⋀k v. fmlookup m k = Some v ⟹ (∃v'. f v' = v)"
obtains m' where "m = fmmap f m'"
(this is for finite maps, but it could equally well work for lists)
I can prove this easily by induction, but it feels like there should be
a simpler way. Unfortunately, I can't figure it out.
Cheers
Lars
Email Gateway (Aug 22 2022 at 18:07):From: Traytel Dmitriy <traytel@inf.ethz.ch>
Hi Lars,
The following lemma uses only the BNF properties of the map and set functions and bounded choice. This proof could be in principle automated for arbitrary BNFs.
lemma fmmap_total_aux:
assumes "∀v ∈ fmran' m. ∃v'. f v' = v"
obtains m' where "m = fmmap f m'"
apply atomize_elim
apply (insert bchoice[OF assms])
apply (erule exE)
subgoal for g
apply (intro exI[of _ "fmmap g m"])
apply (auto simp only: fmap.map_comp o_apply fmap.map_ident cong: fmap.map_cong)
done
done
Your actual lemma is a direct consequence but uses the fmap-specific fmlookup instead of the general BNF set function:
lemma fmmap_total:
assumes "⋀k v. fmlookup m k = Some v ⟹ (∃v'. f v' = v)"
obtains m' where "m = fmmap f m'"
apply (rule fmmap_total; auto intro: assms)
done
Hope that helps,
Dmitriy
Email Gateway (Aug 22 2022 at 18:08):From: Lars Hupel <hupel@in.tum.de>
Hi Dmitriy,
The following lemma uses only the BNF properties of the map and set functions and bounded choice. This proof could be in principle automated for arbitrary BNFs.
thanks for that. It didn't occur to me to use "bchoice". I agree that it
could be automated, but it's probably a lemma that is too specific to be
of common use.
Cheers
Lars
Last updated: Apr 26 2024 at 20:16 UTC