[isabelle] map totality

[Lars Hupel]

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

[Traytel Dmitriy]

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

Post by Lars Hupel
Dear BNF experts,
I was wondering whether there is an elegant way to prove such properties
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 fig

[Lars Hupel]

Hi Dmitriy,

Post by Traytel 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