# Theory Finite_Map

Up to index of Isabelle/HOL/ribbonproofs

theory Finite_Map
imports FSet
`header {* Finite partial functions *}theory Finite_Map imports  Main  "~~/src/HOL/Quotient_Examples/FSet"begintext {* The type of finite partial functions is obtained by restricting the   type of partial functions to those with a finite domain. We use the  lifting package to transfer several theories from the Map library to our  finite setting. *}  typedef (open) ('k, 'v) fmap = "{f :: 'k \<rightharpoonup> 'v. finite (dom f)}"by (intro exI[of _ "empty"], simp)type_synonym ('k,'v) FMAP = "('k,'v) fmap" (infix "\<rightharpoonup>⇩f" 50)setup_lifting type_definition_fmapsubsection {* Union *}lift_definition   fmap_add :: "('k \<rightharpoonup>⇩f 'v) => ('k \<rightharpoonup>⇩f 'v) => ('k \<rightharpoonup>⇩f 'v)"is "map_add"by (unfold dom_map_add, auto)abbreviation  FMAP_ADD :: "('k \<rightharpoonup>⇩f 'v) => ('k \<rightharpoonup>⇩f 'v) => ('k \<rightharpoonup>⇩f 'v)" (infixl "⊕" 100) where  "xs ⊕ ys ≡ fmap_add xs ys"lemma fmap_add_assoc:  "A ⊕ (B ⊕ C) = (A ⊕ B) ⊕ C"by (transfer, auto)subsection {* Difference *}definition  map_diff :: "('k \<rightharpoonup> 'v) => 'k fset => ('k \<rightharpoonup> 'v)"where  "map_diff f ks = restrict_map f (- fset ks)"lift_definition  fmap_diff :: "('k \<rightharpoonup>⇩f 'v) => 'k fset => ('k \<rightharpoonup>⇩f 'v)"is "map_diff"by (auto simp add: map_diff_def)abbreviation   FMAP_DIFF :: "('k \<rightharpoonup>⇩f 'v) => 'k fset => ('k \<rightharpoonup>⇩f 'v)" (infix "\<ominus>" 110) where   "xs \<ominus> ys ≡ fmap_diff xs ys"subsection {* Comprehension *}definition   make_map :: "'k fset => 'v => ('k \<rightharpoonup> 'v)"where   "make_map ks v ≡ λk. if k ∈ fset ks then Some v else None"lemma dom_make_map:   "dom (make_map ks v) = fset ks"by (smt domIff make_map_def not_Some_eq set_eqI)lift_definition  make_fmap :: "'k fset => 'v => ('k \<rightharpoonup>⇩f 'v)"is "make_map"by (unfold make_map_def dom_def, auto)abbreviation   MAKE_FMAP :: "'k fset => 'v => ('k \<rightharpoonup>⇩f 'v)" ("[ _ |=> _ ]")where  "[ ks |=> v ] ≡ make_fmap ks v"subsection {* The empty finite partial function *}lift_definition  fmap_empty :: "('k \<rightharpoonup>⇩f 'v)"is "empty"by autosubsection {* Domain *}definition  dom_fset :: "('k \<rightharpoonup> 'v) => 'k fset"where "dom_fset f ≡ THE x. fset x = dom f"lift_definition  fdom :: "('k \<rightharpoonup>⇩f 'v) => 'k fset"is "dom_fset"by autolemma inv_fset:  assumes "finite X"  shows "∃!x. fset x = X"using assms apply (induct rule: finite_induct)apply (intro ex1I[of _ "{||}"])apply (metis fset_simps(1))apply (metis fset_cong fset_simps(1))apply (metis fset_cong fset_simps(2))donelemma fset_inv_fset:  assumes "finite X"  shows "fset (THE x. fset x = X) = X"using assms by (smt inv_fset theI)lemma fset_dom_fset:  assumes "finite (dom f)"  shows "fset (dom_fset f) = dom f"by (metis dom_fset_def assms fset_inv_fset)lemma fmap_add_commute:  assumes "fdom A |∩| fdom B = {||}"  shows "A ⊕ B = B ⊕ A"using assmsapply (transfer)apply (fold fset_cong, simp add: dom_fset_def fset_inv_fset)apply (rule map_add_comm, assumption)donelemma make_fmap_union:   "[ xs |=> v ] ⊕ [ ys |=> v] = [ xs |∪| ys |=> v ]"by (transfer, auto simp add: make_map_def map_add_def)lemma fdom_union:   "fdom (xs ⊕ ys) = fdom xs |∪| fdom ys"by (transfer, fold fset_cong, auto simp add: dom_fset_def fset_inv_fset)lemma fdom_make_fmap:  "fdom [ ks |=> v ] = ks"by (transfer, auto simp add: fset_cong dom_fset_def fset_inv_fset dom_make_map)subsection {* Lookup *}lift_definition  lookup :: "('k \<rightharpoonup>⇩f 'v) => 'k => 'v"is "op o the"by autolemma lookup_make_fmap:  assumes "k ∈ fset ks"  shows "lookup [ ks |=> v ] k = v"using assms by (transfer, simp add: make_map_def)lemma lookup_make_fmap1:  "lookup [ {|k|} |=> v ] k = v"by (metis fset_simps(2) insertI1 lookup_make_fmap)lemma lookup_union1:  assumes "k |∈| fdom ys"  shows "lookup (xs ⊕ ys) k = lookup ys k"using assms by (transfer, metis in_fset fset_dom_fset map_add_dom_app_simps(1) o_apply)lemma lookup_union2:  assumes "k |∉| fdom ys"  shows "lookup (xs ⊕ ys) k = lookup xs k"using assms by (transfer, metis in_fset fset_dom_fset map_add_dom_app_simps(3) o_apply)lemma lookup_union3:  assumes "k |∉| fdom xs"  shows "lookup (xs ⊕ ys) k = lookup ys k"using assmsapply (cases "k |∈| fdom ys")apply (simp add: lookup_union1)apply transferapply (metis fset_dom_fset map_add_dom_app_simps(2) notin_fset o_apply)doneend`