theory FMap

  imports Main "~~/src/HOL/Quotient_Examples/FSet" "~~/src/HOL/Library/DAList"

begin

subsubsection {* The type of finite maps *}

typedef ('a, 'b) fmap  (infixr "f\<rightharpoonup>" 1) = "{x :: 'a \<rightharpoonup> 'b. finite (dom x) }"

  proof show "empty \<in> {x. finite (dom x)}" by simp qed

setup_lifting type_definition_fmap

lift_definition fdom :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'key set" is "dom" ..

lift_definition fran :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'value set" is "ran" ..

lift_definition lookup :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'key \<Rightarrow> 'value option" is "(\<lambda> x. x)" ..

notation lookup (infixl "$" 999)

abbreviation the_lookup (infix "f!" 55)

  where "m f! x \<equiv> the (lookup m x)"

lift_definition fempty :: "'key f\<rightharpoonup> 'value" ("f\<emptyset>") is Map.empty by simp

lemma fempty_fdom[simp]: "fdom f\<emptyset> = {}"

  by (transfer, auto)

lemma fdomIff: "a \<in> fdom m \<longleftrightarrow> lookup m a \<noteq> None"

 by (transfer, auto)

lemma lookup_not_fdom: "x \<notin> fdom m \<Longrightarrow> lookup m x = None"

  by (auto iff:fdomIff)

lemma finite_range:

  assumes "finite (dom m)"

  shows "finite (ran m)"

  apply (rule finite_subset[OF _ finite_imageI[OF assms, of "\<lambda> x . the (m x)"]])

  by (auto simp add: ran_def dom_def image_def)

lemma finite_fdom[simp]: "finite (fdom m)"

  by transfer

lemma finite_fran[simp]: "finite (fran m)"

  by (transfer, rule finite_range)

lemma fmap_eqI[intro]:

  assumes "fdom a = fdom b"

  and "\<And> x. x \<in> fdom a \<Longrightarrow> a f! x = b f! x"

  shows "a = b"

using assms

proof(transfer)

  fix a b :: "'a \<rightharpoonup> 'b"

  assume d: "dom a = dom b"

  assume eq: "\<And> x. x \<in> dom a \<Longrightarrow> the (a x) = the (b x)"

  show "a = b"

  proof

    fix x

    show "a x = b x"

    proof(cases "a x")

    case None

      hence "x \<notin> dom a" by (simp add: dom_def)

      hence "x \<notin> dom b" using d by simp

      hence " b x = None"  by (simp add: dom_def)

      thus ?thesis using None by simp

    next

    case (Some y)

      hence d': "x \<in> dom ( a)" by (simp add: dom_def)

      hence "the ( a x) = the ( b x)" using eq by auto

      moreover

      have "x \<in> dom ( b)" using Some d' d by simp

      then obtain y' where " b x = Some y'" by (auto simp add: dom_def)

      ultimately

      show " a x =  b x" using Some by auto

    qed

  qed

qed

subsubsection {* Updates *}

lift_definition

  fmap_upd :: "'key f\<rightharpoonup> 'value \<Rightarrow> 'key \<Rightarrow> 'value \<Rightarrow> 'key f\<rightharpoonup> 'value" ("_'(_ f\<mapsto> _')" [900,900]900)

  is "\<lambda> m x v. m( x \<mapsto> v)"  by simp

lemma fmap_upd_fdom[simp]: "fdom (h (x f\<mapsto> v)) = insert x (fdom h)"

  by (transfer, auto)

lemma the_lookup_fmap_upd[simp]: "lookup (h (x f\<mapsto> v)) x = Some v"

  by (transfer, auto)

lemma the_lookup_fmap_upd_other[simp]: "x' \<noteq> x \<Longrightarrow> lookup (h (x f\<mapsto> v)) x' = lookup h x'"

  by (transfer, auto)

lemma fmap_upd_overwrite[simp]: "f (x f\<mapsto> y) (x f\<mapsto> z) = f (x f\<mapsto> z)"

  by (transfer, auto) 

lemma fmap_upd_twist: "a \<noteq> c \<Longrightarrow> (m(a f\<mapsto> b))(c f\<mapsto> d) = (m(c f\<mapsto> d))(a f\<mapsto> b)"

  apply (rule fmap_eqI)

  apply auto[1]

  apply (case_tac "x = a", auto)

  apply (case_tac "x = c", auto)

  done

subsubsection {* Restriction *}

lift_definition fmap_restr :: "'a set \<Rightarrow> 'a f\<rightharpoonup> 'b \<Rightarrow> 'a f\<rightharpoonup> 'b"

  is "\<lambda> S m. (if finite S then (restrict_map m S) else empty)" by auto

lemma lookup_fmap_restr[simp]: "finite S \<Longrightarrow> x \<in> S \<Longrightarrow> lookup (fmap_restr S m) x = lookup m x"

  by (transfer, auto)

lemma fdom_fmap_restr[simp]: "finite S \<Longrightarrow> fdom (fmap_restr S m) = fdom m \<inter> S"

  by (transfer, simp)

lemma fmap_restr_fmap_restr[simp]:

 "finite d1 \<Longrightarrow> finite d2 \<Longrightarrow> fmap_restr d1 (fmap_restr d2 x) = fmap_restr (d1 \<inter> d2) x"

 by (transfer, auto simp add: restrict_map_def)

lemma fmap_restr_fmap_restr_subset:

 "finite d2 \<Longrightarrow> d1 \<subseteq> d2 \<Longrightarrow> fmap_restr d1 (fmap_restr d2 x) = fmap_restr d1 x"

 by (metis Int_absorb2 finite_subset fmap_restr_fmap_restr)

lemma fmap_restr_useless: "finite S \<Longrightarrow> fdom m \<subseteq> S \<Longrightarrow> fmap_restr S m = m"

  by (rule fmap_eqI, auto)

lemma fmap_restr_not_finite:

  "\<not> finite S \<Longrightarrow> fmap_restr S \<rho> = f\<emptyset>"

  by (transfer, simp)

lemma fmap_restr_fmap_upd: "x \<in> S \<Longrightarrow> finite S \<Longrightarrow> fmap_restr S (m1(x f\<mapsto> v)) = (fmap_restr S m1)(x f\<mapsto> v)"

  apply (rule fmap_eqI)

  apply auto[1]

  apply (case_tac "xa = x")

  apply auto

  done

subsubsection {* Deleting *}

lift_definition fmap_delete :: "'a \<Rightarrow> 'a f\<rightharpoonup> 'b \<Rightarrow> 'a f\<rightharpoonup> 'b"

  is "\<lambda> x m. m(x := None)" by auto

lemma fdom_fmap_delete[simp]:

  "fdom (fmap_delete x m) = fdom m - {x}"

  by (transfer, auto)

lemma fmap_delete_fmap_upd[simp]:

  "fmap_delete x (m(x f\<mapsto> v)) = fmap_delete x m"

  by (transfer, simp)

lemma fmap_delete_noop:

  "x \<notin> fdom m \<Longrightarrow> fmap_delete x m = m"

  by (transfer, auto)

lemma fmap_upd_fmap_delete[simp]: "x \<in> fdom \<Gamma> \<Longrightarrow> (fmap_delete x \<Gamma>)(x f\<mapsto> \<Gamma> f! x) = \<Gamma>"

  by (transfer, auto)

lemma fran_fmap_upd[simp]:

  "fran (m(x f\<mapsto> v)) = insert v (fran (fmap_delete x m))"

by (transfer, auto simp add: ran_def)

subsubsection {* Addition (merging) of finite maps *}

lift_definition fmap_add :: "'a f\<rightharpoonup> 'b \<Rightarrow> 'a f\<rightharpoonup> 'b \<Rightarrow> 'a f\<rightharpoonup> 'b" (infixl "f++" 100) 

  is "map_add" by auto

lemma fdom_fmap_add[simp]: "fdom (m1 f++ m2) = fdom m1 \<union> fdom m2"

  by (transfer, auto)

lemma lookup_fmap_add1[simp]: "x \<in> fdom m2 \<Longrightarrow> lookup (m1 f++ m2) x = lookup m2 x"

  by (transfer, auto)

lemma lookup_fmap_add2[simp]:  "x \<notin> fdom m2 \<Longrightarrow> lookup (m1 f++ m2) x = lookup m1 x"

  apply transfer

  by (metis map_add_dom_app_simps(3))

lemma [simp]: "\<rho> f++ f\<emptyset> = \<rho>"

  by (transfer, auto)

lemma fmap_add_overwrite: "fdom m1 \<subseteq> fdom m2 \<Longrightarrow> m1 f++ m2 = m2"

  apply transfer

  apply rule

  apply (case_tac "x \<in> dom m2")

  apply (auto simp add: map_add_dom_app_simps(1))

  done

lemma fmap_add_upd_swap: 

  "x \<notin> fdom \<rho>' \<Longrightarrow> \<rho>(x f\<mapsto> z) f++ \<rho>' = (\<rho> f++ \<rho>')(x f\<mapsto> z)"

  apply transfer

  by (metis map_add_upd_left)

lemma fmap_add_upd: 

  "\<rho> f++ (\<rho>'(x f\<mapsto> z)) = (\<rho> f++ \<rho>')(x f\<mapsto> z)"

  apply transfer

  by (metis map_add_upd)

lemma fmap_restr_add: "fmap_restr S (m1 f++ m2) = fmap_restr S m1 f++ fmap_restr S m2"

  apply (cases "finite S")

  apply (rule fmap_eqI)

  apply auto[1]

  apply (case_tac "x \<in> fdom m2")

  apply auto

  apply (simp add: fmap_restr_not_finite)

  done

subsubsection {* Conversion from associative lists *}

lift_definition fmap_of :: "('a \<times> 'b) list \<Rightarrow> 'a f\<rightharpoonup> 'b"

  is map_of by (rule finite_dom_map_of)

lemma fmap_of_Nil[simp]: "fmap_of [] = f\<emptyset>"

 by (transfer, simp)

lemma fmap_of_Cons[simp]: "fmap_of (p # l) = (fmap_of l)(fst p f\<mapsto> snd p)" 

  by (transfer, simp)

lemma fmap_of_append[simp]: "fmap_of (l1 @ l2) = fmap_of l2 f++ fmap_of l1"

  by (transfer, simp)

lemma lookup_fmap_of[simp]:

  "lookup (fmap_of m) x = map_of m x"

  by (transfer, auto)

lemma fmap_delete_fmap_of[simp]:

  "fmap_delete x (fmap_of m) = fmap_of (AList.delete x m)"

  by (transfer, metis delete_conv')

subsubsection {* Less-than-relation for extending finite maps *}

instantiation fmap :: (type,type) order

begin

  definition "\<rho> \<le> \<rho>' = ((fdom \<rho> \<subseteq> fdom \<rho>') \<and> (\<forall>x \<in> fdom \<rho>. lookup \<rho> x = lookup \<rho>' x))"

  definition "(\<rho>::'a f\<rightharpoonup> 'b) < \<rho>' = (\<rho> \<noteq> \<rho>' \<and> \<rho> \<le> \<rho>')"

  lemma fmap_less_eqI[intro]:

    assumes assm1: "fdom \<rho> \<subseteq> fdom \<rho>'"

      and assm2:  "\<And> x. \<lbrakk> x \<in> fdom \<rho> ; x \<in> fdom \<rho>'  \<rbrakk> \<Longrightarrow> \<rho> f! x = \<rho>' f! x "

     shows "\<rho> \<le> \<rho>'"

   unfolding less_eq_fmap_def

   apply rule

   apply fact

   apply rule+

   apply (frule subsetD[OF `_ \<subseteq> _`])

   apply (frule  assm2)

   apply (auto iff: fdomIff)

   done

  lemma fmap_less_eqD:

    assumes "\<rho> \<le> \<rho>'"

    assumes "x \<in> fdom \<rho>"

    shows "lookup \<rho> x = lookup \<rho>' x"

    using assms

    unfolding less_eq_fmap_def by auto

  lemma fmap_antisym: assumes  "(x:: 'a f\<rightharpoonup> 'b) \<le> y" and "y \<le> x" shows "x = y "

  proof(rule fmap_eqI[rule_format])

      show "fdom x = fdom y" using `x \<le> y` and `y \<le> x` unfolding less_eq_fmap_def by auto

      fix v

      assume "v \<in> fdom x"

      hence "v \<in> fdom y" using `fdom _ = _` by simp

      thus "x f! v = y f! v"

        using `x \<le> y` `v \<in> fdom x` unfolding less_eq_fmap_def by simp

    qed

  lemma fmap_trans: assumes  "(x:: 'a f\<rightharpoonup> 'b) \<le> y" and "y \<le> z" shows "x \<le> z"

  proof

    show "fdom x \<subseteq> fdom z" using `x \<le> y` and `y \<le> z` unfolding less_eq_fmap_def

      by -(rule order_trans [of _ "fdom y"], auto)

    fix v

    assume "v \<in> fdom x" and "v \<in> fdom z"

    hence "v \<in> fdom y" using `x \<le> y`  unfolding less_eq_fmap_def by auto

    hence "lookup y v = lookup x v"

      using `x \<le> y` `v \<in> fdom x` unfolding less_eq_fmap_def by auto

    moreover

    have "lookup y v = lookup z v"

      by (rule fmap_less_eqD[OF `y \<le> z`  `v \<in> fdom y`])

    ultimately

    show "x f! v = z f! v" by auto

  qed

  instance

    apply default

    using fmap_antisym apply (auto simp add: less_fmap_def)[1]

    apply (auto simp add: less_eq_fmap_def)[1]

    using fmap_trans apply assumption

    using fmap_antisym apply assumption

    done

end

lemma fmap_less_fdom:

  "\<rho>1 \<le> \<rho>2 \<Longrightarrow> fdom \<rho>1 \<subseteq> fdom \<rho>2"

  by (metis less_eq_fmap_def)

lemma fmap_less_restrict:

  "\<rho>1 \<le> \<rho>2 \<longleftrightarrow> \<rho>1 = fmap_restr (fdom \<rho>1) \<rho>2"

  unfolding less_eq_fmap_def

  apply transfer

  apply (auto simp add:restrict_map_def split:option.split_asm)

  by (metis option.simps(3))+

lemma fmap_restr_less:

  "fmap_restr S \<rho> \<le> \<rho>"

  unfolding less_eq_fmap_def

  by (transfer, auto)

lemma fmap_upd_less[simp, intro]:

  "\<rho>1 \<le> \<rho>2 \<Longrightarrow> v1 = v2 \<Longrightarrow> \<rho>1(x f\<mapsto> v1) \<le> \<rho>2(x f\<mapsto> v2)"

  apply (rule fmap_less_eqI)

  apply (auto dest: fmap_less_fdom)[1]

  apply (case_tac "xa = x")

  apply (auto dest: fmap_less_eqD)

  done

lemma fmap_update_less[simp, intro]:

  "\<rho>1 \<le> \<rho>1' \<Longrightarrow> \<rho>2 \<le> \<rho>2' \<Longrightarrow>  (fdom \<rho>2' - fdom \<rho>2) \<inter> fdom \<rho>1 = {} \<Longrightarrow> \<rho>1 f++ \<rho>2 \<le> \<rho>1' f++ \<rho>2'"

  apply (rule fmap_less_eqI)

  apply (auto dest: fmap_less_fdom)[1]

  apply (case_tac "x \<in> fdom \<rho>2")

  apply (auto dest: fmap_less_eqD fmap_less_fdom)

  apply (metis fmap_less_eqD fmap_less_fdom lookup_fmap_add1 set_mp)

  by (metis Diff_iff Diff_triv fmap_less_eqD lookup_fmap_add2)

lemma fmap_restr_le:

  assumes "\<rho>1 \<le> \<rho>2"

  assumes "S1 \<subseteq> S2"

  assumes [simp]:"finite S2"

  shows "fmap_restr S1 \<rho>1 \<le> fmap_restr S2 \<rho>2"

proof-

  have [simp]: "finite S1"

    by (rule finite_subset[OF `S1 \<subseteq> S2` `finite S2`])

  show ?thesis

  proof (rule fmap_less_eqI)

    have "fdom \<rho>1 \<subseteq> fdom \<rho>2"

      by (metis assms(1) less_eq_fmap_def)

    thus "fdom (fmap_restr S1 \<rho>1) \<subseteq> fdom (fmap_restr S2 \<rho>2)"

      using `S1 \<subseteq> S2`

      by auto

  next

    fix x

    assume "x \<in> fdom (fmap_restr S1 \<rho>1) "

    hence [simp]:"x \<in> fdom \<rho>1" and [simp]:"x \<in> S1" and [simp]: "x \<in> S2"

      by (auto intro: set_mp[OF `S1 \<subseteq> S2`])

    have "\<rho>1 f! x = \<rho>2 f! x"

      by (metis `x \<in> fdom \<rho>1` assms(1) less_eq_fmap_def)

    thus "(fmap_restr S1 \<rho>1) f! x = (fmap_restr S2 \<rho>2) f! x"

      by simp

  qed

qed

fun alookup

where

  "alookup k [] = None"

| "alookup k ((x, y) # xs) = (if (k = x) then Some y else alookup k xs)"

definition fdom_to_list :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> 'a list"

where

  "fdom_to_list f = (THE xs. set xs = fdom f \<and> sorted xs \<and> distinct xs)"

lemma

  "fdom f = set (fdom_to_list f)"

unfolding fdom_to_list_def

apply(subgoal_tac "finite (fdom f)")

apply(drule finite_sorted_distinct_unique)

apply(drule theI')

apply(simp_all)

done

definition fmap_to_alist :: "('a :: linorder) f\<rightharpoonup> 'b \<Rightarrow> ('a \<times> 'b) list"

where

  "fmap_to_alist f = [(x, f f! x). x \<leftarrow> fdom_to_list f]"

lemma

  shows "(f $ k) = alookup k (fmap_to_alist f)" 

thm finite_dom_map_of

apply(transfer)

apply(simp add: fmap_to_alist_def)

thm lookup_def

apply(rule theI2)

apply(induct k xs\<equiv>"fmap_to_alist f" rule: alookup.induct)

apply(simp add: fmap_to_alist_def fmapdom_to_list_def)

thm theD1

end