Theory Utilities

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