section ‹Utilities› theory Utilities imports "Finite-Map-Extras.Finite_Map_Extras" begin subsection ‹Utilities for lists› fun foldr1 :: "('a ⇒ 'a ⇒ 'a) ⇒ 'a list ⇒ 'a" where "foldr1 f [x] = x" | "foldr1 f (x # xs) = f x (foldr1 f xs)" | "foldr1 f [] = undefined f" abbreviation lset where "lset ≡ List.set" lemma rev_induct2 [consumes 1, case_names Nil snoc]: assumes "length xs = length ys" and "P [] []" and "⋀x xs y ys. length xs = length ys ⟹ P xs ys ⟹ P (xs @ [x]) (ys @ [y])" shows "P xs ys" using assms proof (induction xs arbitrary: ys rule: rev_induct) case (snoc x xs) then show ?case by (cases ys rule: rev_cases) simp_all qed simp subsection ‹Utilities for finite maps› no_syntax "_fmaplet" :: "['a, 'a] ⇒ fmaplet" ("_ /$$:=/ _") "_fmaplets" :: "['a, 'a] ⇒ fmaplet" ("_ /[$$:=]/ _") syntax "_fmaplet" :: "['a, 'a] ⇒ fmaplet" ("_ /↣/ _") "_fmaplets" :: "['a, 'a] ⇒ fmaplet" ("_ /[↣]/ _") lemma fmdom'_fmap_of_list [simp]: shows "fmdom' (fmap_of_list ps) = lset (map fst ps)" by (induction ps) force+ lemma fmran'_singleton [simp]: shows "fmran' {k ↣ v} = {v}" proof - have "v' ∈ fmran' {k ↣ v} ⟹ v' = v" for v' proof - assume "v' ∈ fmran' {k ↣ v}" fix k' have "fmdom' {k ↣ v} = {k}" by simp then show "v' = v" proof (cases "k' = k") case True with ‹v' ∈ fmran' {k ↣ v}› show ?thesis using fmdom'I by fastforce next case False with ‹fmdom' {k ↣ v} = {k}› and ‹v' ∈ fmran' {k ↣ v}› show ?thesis using fmdom'I by fastforce qed qed moreover have "v ∈ fmran' {k ↣ v}" by (simp add: fmran'I) ultimately show ?thesis by blast qed lemma fmran'_fmupd [simp]: assumes "m $$ x = None" shows "fmran' (m(x ↣ y)) = {y} ∪ fmran' m" using assms proof (intro subset_antisym subsetI) fix x' assume "m $$ x = None" and "x' ∈ fmran' (m(x ↣ y))" then show "x' ∈ {y} ∪ fmran' m" by (auto simp add: fmlookup_ran'_iff, metis option.inject) next fix x' assume "m $$ x = None" and "x' ∈ {y} ∪ fmran' m" then show "x' ∈ fmran' (m(x ↣ y))" by (force simp add: fmlookup_ran'_iff) qed lemma fmran'_fmadd [simp]: assumes "fmdom' m ∩ fmdom' m' = {}" shows "fmran' (m ++⇩_{f}m') = fmran' m ∪ fmran' m'" using assms proof (intro subset_antisym subsetI) fix x assume "fmdom' m ∩ fmdom' m' = {}" and "x ∈ fmran' (m ++⇩_{f}m')" then show "x ∈ fmran' m ∪ fmran' m'" by (auto simp add: fmlookup_ran'_iff) meson next fix x assume "fmdom' m ∩ fmdom' m' = {}" and "x ∈ fmran' m ∪ fmran' m'" then show "x ∈ fmran' (m ++⇩_{f}m')" using fmap_disj_comm and fmlookup_ran'_iff by fastforce qed lemma finite_fmran': shows "finite (fmran' m)" by (simp add: fmran'_alt_def) lemma fmap_of_zipped_list_range: assumes "length ks = length vs" and "m = fmap_of_list (zip ks vs)" and "k ∈ fmdom' m" shows "m $$! k ∈ lset vs" using assms by (induction arbitrary: m rule: list_induct2) auto lemma fmap_of_zip_nth [simp]: assumes "length ks = length vs" and "distinct ks" and "i < length ks" shows "fmap_of_list (zip ks vs) $$! (ks ! i) = vs ! i" using assms by (simp add: fmap_of_list.rep_eq map_of_zip_nth) lemma fmap_of_zipped_list_fmran' [simp]: assumes "distinct (map fst ps)" shows "fmran' (fmap_of_list ps) = lset (map snd ps)" using assms proof (induction ps) case Nil then show ?case by auto next case (Cons p ps) then show ?case proof (cases "p ∈ lset ps") case True then show ?thesis using Cons.prems by auto next case False obtain k and v where "p = (k, v)" by fastforce with Cons.prems have "k ∉ fmdom' (fmap_of_list ps)" by auto then have "fmap_of_list (p # ps) = {k ↣ v} ++⇩_{f}fmap_of_list ps" using ‹p = (k, v)› and fmap_singleton_comm by fastforce with Cons.prems have "fmran' (fmap_of_list (p # ps)) = {v} ∪ fmran' (fmap_of_list ps)" by (simp add: ‹p = (k, v)›) then have "fmran' (fmap_of_list (p # ps)) = {v} ∪ lset (map snd ps)" using Cons.IH and Cons.prems by force then show ?thesis by (simp add: ‹p = (k, v)›) qed qed lemma fmap_of_list_nth [simp]: assumes "distinct (map fst ps)" and "j < length ps" shows "fmap_of_list ps $$ ((map fst ps) ! j) = Some (map snd ps ! j)" using assms by (induction j) (simp_all add: fmap_of_list.rep_eq) lemma fmap_of_list_nth_split [simp]: assumes "distinct xs" and "j < length xs" and "length ys = length xs" and "length zs = length xs" shows "fmap_of_list (zip xs (take k ys @ drop k zs)) $$ (xs ! j) = (if j < k then Some (take k ys ! j) else Some (drop k zs ! (j - k)))" using assms proof (induction k arbitrary: xs ys zs j) case 0 then show ?case by (simp add: fmap_of_list.rep_eq map_of_zip_nth) next case (Suc k) then show ?case proof (cases xs) case Nil with Suc.prems(2) show ?thesis by auto next case (Cons x xs') let ?ps = "zip xs (take (Suc k) ys @ drop (Suc k) zs)" from Cons and Suc.prems(3,4) obtain y and z and ys' and zs' where "ys = y # ys'" and "zs = z # zs'" by (metis length_0_conv neq_Nil_conv) let ?ps' = "zip xs' (take k ys' @ drop k zs')" from Cons have *: "fmap_of_list ?ps = fmap_of_list ((x, y) # ?ps')" using ‹ys = y # ys'› and ‹zs = z # zs'› by fastforce also have "… = {x ↣ y} ++⇩_{f}fmap_of_list ?ps'" proof - from ‹ys = y # ys'› and ‹zs = z # zs'› have "fmap_of_list ?ps' $$ x = None" using Cons and Suc.prems(1,3,4) by (simp add: fmdom'_notD) then show ?thesis using fmap_singleton_comm by fastforce qed finally have "fmap_of_list ?ps = {x ↣ y} ++⇩_{f}fmap_of_list ?ps'" . then show ?thesis proof (cases "j = 0") case True with ‹ys = y # ys'› and Cons show ?thesis by simp next case False then have "xs ! j = xs' ! (j - 1)" by (simp add: Cons) moreover from ‹ys = y # ys'› and ‹zs = z # zs'› have "fmdom' (fmap_of_list ?ps') = lset xs'" using Cons and Suc.prems(3,4) by force moreover from False and Suc.prems(2) and Cons have "j - 1 < length xs'" using le_simps(2) by auto ultimately have "fmap_of_list ?ps $$ (xs ! j) = fmap_of_list ?ps' $$ (xs' ! (j - 1))" using Cons and * and Suc.prems(1) by auto with Suc.IH and Suc.prems(1,3,4) and Cons have **: "fmap_of_list ?ps $$ (xs ! j) = (if j - 1 < k then Some (take k ys' ! (j - 1)) else Some (drop k zs' ! ((j - 1) - k)))" using ‹j - 1 < length xs'› and ‹ys = y # ys'› and ‹zs = z # zs'› by simp then show ?thesis proof (cases "j - 1 < k") case True with False and ** show ?thesis using ‹ys = y # ys'› by auto next case False from Suc.prems(1) and Cons and ‹j - 1 < length xs'› and ‹xs ! j = xs' ! (j - 1)› have "j > 0" using nth_non_equal_first_eq by fastforce with False have "j ≥ Suc k" by simp moreover have "fmap_of_list ?ps $$ (xs ! j) = Some (drop (Suc k) zs ! (j - Suc k))" using ** and False and ‹zs = z # zs'› by fastforce ultimately show ?thesis by simp qed qed qed qed lemma fmadd_drop_cancellation [simp]: assumes "m $$ k = Some v" shows "{k ↣ v} ++⇩_{f}fmdrop k m = m" using assms proof (induction m) case fmempty then show ?case by simp next case (fmupd k' v' m') then show ?case proof (cases "k' = k") case True with fmupd.prems have "v = v'" by fastforce have "fmdrop k' (m'(k' ↣ v')) = m'" unfolding fmdrop_fmupd_same using fmdrop_idle'[OF fmdom'_notI[OF fmupd.hyps]] by (unfold True) then have "{k ↣ v} ++⇩_{f}fmdrop k' (m'(k' ↣ v')) = {k ↣ v} ++⇩_{f}m'" by simp then show ?thesis using fmap_singleton_comm[OF fmupd.hyps] by (simp add: True ‹v = v'›) next case False with fmupd.prems have "m' $$ k = Some v" by force from False have "{k ↣ v} ++⇩_{f}fmdrop k (m'(k' ↣ v')) = {k ↣ v} ++⇩_{f}(fmdrop k m')(k' ↣ v')" by (simp add: fmdrop_fmupd) also have "… = ({k ↣ v} ++⇩_{f}fmdrop k m')(k' ↣ v')" by fastforce also from fmupd.prems and fmupd.IH[OF ‹m' $$ k = Some v›] have "… = m'(k' ↣ v')" by force finally show ?thesis . qed qed lemma fmap_of_list_fmmap [simp]: shows "fmap_of_list (map2 (λv' A'. (v', f A')) xs ys) = fmmap f (fmap_of_list (zip xs ys))" unfolding fmmap_of_list using cond_case_prod_eta [where f = "λv' A'.(v', f A')" and g = "apsnd f", unfolded apsnd_conv, simplified] by (rule arg_cong) end