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"
begin

text {* 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_fmap

subsection {* 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 auto

subsection {* 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 auto

lemma 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))
done

lemma 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 assms
apply (transfer)
apply (fold fset_cong, simp add: dom_fset_def fset_inv_fset)
apply (rule map_add_comm, assumption)
done

lemma 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 auto

lemma 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 assms
apply (cases "k |∈| fdom ys")
apply (simp add: lookup_union1)
apply transfer
apply (metis fset_dom_fset map_add_dom_app_simps(2) notin_fset o_apply)
done


end