1 theory FMap

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

     3 begin

     4 

     5 subsubsection {* The type of finite maps *}

     6 

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

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

     9 

    10 setup_lifting type_definition_fmap

    11 

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

    13 

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

    15 

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

    17 

    18 abbreviation the_lookup (infix "f!" 55)

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

    20 

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

    22 

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

    24   by (transfer, auto)

    25 

    26 lemma fdomIff: "(a : fdom m) = (lookup m a \<noteq> None)"

    27  by (transfer, auto)

    28 

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

    30   by (auto iff:fdomIff)

    31 

    32 lemma finite_range:

    33   assumes "finite (dom m)"

    34   shows "finite (ran m)"

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

    36   by (auto simp add: ran_def dom_def image_def)

    37 

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

    39   by transfer

    40 

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

    42   by (transfer, rule finite_range)

    43 

    44 lemma fmap_eqI[intro]:

    45   assumes "fdom a = fdom b"

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

    47   shows "a = b"

    48 using assms

    49 proof(transfer)

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

    51   assume d: "dom a = dom b"

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

    53   show "a = b"

    54   proof

    55     fix x

    56     show "a x = b x"

    57     proof(cases "a x")

    58     case None

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

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

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

    62       thus ?thesis using None by simp

    63     next

    64     case (Some y)

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

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

    67       moreover

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

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

    70       ultimately

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

    72     qed

    73   qed

    74 qed

    75 

    76 subsubsection {* Updates *}

    77 

    78 lift_definition

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

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

    81 

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

    83   by (transfer, auto)

    84 

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

    86   by (transfer, auto)

    87 

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

    89   by (transfer, auto)

    90 

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

    92   by (transfer, auto) 

    93 

    94 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)"

    95   apply (rule fmap_eqI)

    96   apply auto[1]

    97   apply (case_tac "x = a", auto)

    98   apply (case_tac "x = c", auto)

    99   done

   100 

   101 subsubsection {* Restriction *}

   102 

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

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

   105 

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

   107   by (transfer, auto)

   108 

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

   110   by (transfer, simp)

   111 

   112 lemma fmap_restr_fmap_restr[simp]:

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

   114  by (transfer, auto simp add: restrict_map_def)

   115 

   116 lemma fmap_restr_fmap_restr_subset:

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

   118  by (metis Int_absorb2 finite_subset fmap_restr_fmap_restr)

   119 

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

   121   by (rule fmap_eqI, auto)

   122 

   123 lemma fmap_restr_not_finite:

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

   125   by (transfer, simp)

   126 

   127 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)"

   128   apply (rule fmap_eqI)

   129   apply auto[1]

   130   apply (case_tac "xa = x")

   131   apply auto

   132   done

   133 

   134 subsubsection {* Deleting *}

   135 

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

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

   138 

   139 lemma fdom_fmap_delete[simp]:

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

   141   by (transfer, auto)

   142 

   143 lemma fmap_delete_fmap_upd[simp]:

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

   145   by (transfer, simp)

   146 

   147 lemma fmap_delete_noop:

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

   149   by (transfer, auto)

   150 

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

   152   by (transfer, auto)

   153 

   154 lemma fran_fmap_upd[simp]:

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

   156 by (transfer, auto simp add: ran_def)

   157  

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

   159 

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

   161   is "map_add" by auto

   162 

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

   164   by (transfer, auto)

   165 

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

   167   by (transfer, auto)

   168 

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

   170   apply transfer

   171   by (metis map_add_dom_app_simps(3))

   172 

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

   174   by (transfer, auto)

   175 

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

   177   apply transfer

   178   apply rule

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

   180   apply (auto simp add: map_add_dom_app_simps(1))

   181   done

   182 

   183 lemma fmap_add_upd_swap: 

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

   185   apply transfer

   186   by (metis map_add_upd_left)

   187 

   188 lemma fmap_add_upd: 

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

   190   apply transfer

   191   by (metis map_add_upd)

   192 

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

   194   apply (cases "finite S")

   195   apply (rule fmap_eqI)

   196   apply auto[1]

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

   198   apply auto

   199   apply (simp add: fmap_restr_not_finite)

   200   done

   201 

   202 subsubsection {* Conversion from associative lists *}

   203 

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

   205   is map_of by (rule finite_dom_map_of)

   206 

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

   208  by (transfer, simp)

   209 

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

   211   by (transfer, simp)

   212 

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

   214   by (transfer, simp)

   215 

   216 lemma lookup_fmap_of[simp]:

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

   218   by (transfer, auto)

   219 

   220 lemma fmap_delete_fmap_of[simp]:

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

   222   by (transfer, metis delete_conv')

   223 

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

   225 

   226 instantiation fmap :: (type,type) order

   227 begin

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

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

   230 

   231   lemma fmap_less_eqI[intro]:

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

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

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

   235    unfolding less_eq_fmap_def

   236    apply rule

   237    apply fact

   238    apply rule+

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

   240    apply (frule  assm2)

   241    apply (auto iff: fdomIff)

   242    done

   243   

   244   lemma fmap_less_eqD:

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

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

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

   248     using assms

   249     unfolding less_eq_fmap_def by auto

   250   

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

   252   proof(rule fmap_eqI[rule_format])

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

   254       

   255       fix v

   256       assume "v \<in> fdom x"

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

   258   

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

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

   261     qed

   262   

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

   264   proof

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

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

   267     

   268     fix v

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

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

   271     hence "lookup y v = lookup x v"

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

   273     moreover

   274     have "lookup y v = lookup z v"

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

   276     ultimately

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

   278   qed

   279   

   280   instance

   281     apply default

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

   283     apply (auto simp add: less_eq_fmap_def)[1]

   284     using fmap_trans apply assumption

   285     using fmap_antisym apply assumption

   286     done

   287 end

   288 

   289 lemma fmap_less_fdom:

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

   291   by (metis less_eq_fmap_def)

   292 

   293 lemma fmap_less_restrict:

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

   295   unfolding less_eq_fmap_def

   296   apply transfer

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

   298   by (metis option.simps(3))+

   299 

   300 lemma fmap_restr_less:

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

   302   unfolding less_eq_fmap_def

   303   by (transfer, auto)

   304 

   305 lemma fmap_upd_less[simp, intro]:

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

   307   apply (rule fmap_less_eqI)

   308   apply (auto dest: fmap_less_fdom)[1]

   309   apply (case_tac "xa = x")

   310   apply (auto dest: fmap_less_eqD)

   311   done

   312 

   313 lemma fmap_update_less[simp, intro]:

   314   "\<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'"

   315   apply (rule fmap_less_eqI)

   316   apply (auto dest: fmap_less_fdom)[1]

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

   318   apply (auto dest: fmap_less_eqD fmap_less_fdom)

   319   apply (metis fmap_less_eqD fmap_less_fdom lookup_fmap_add1 set_mp)

   320   by (metis Diff_iff Diff_triv fmap_less_eqD lookup_fmap_add2)

   321 

   322 lemma fmap_restr_le:

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

   324   assumes "S1 \<subseteq> S2"

   325   assumes [simp]:"finite S2"

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

   327 proof-

   328   have [simp]: "finite S1"

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

   330   show ?thesis

   331   proof (rule fmap_less_eqI)

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

   333       by (metis assms(1) less_eq_fmap_def)

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

   335       using `S1 \<subseteq> S2`

   336       by auto

   337   next

   338     fix x

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

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

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

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

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

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

   345       by simp

   346   qed

   347 qed

   348   

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

   350 where

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

   352 

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

   354 where

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

   356 

   357 

   358 end