Theory Finite_Fun

section ‹ Finite Functions ›

theory Finite_Fun
  imports Partial_Fun
begin

subsection ‹ Finite function type and operations ›

typedef ('a, 'b) ffun = "{f :: ('a, 'b) pfun. finite(pdom(f))}"
  morphisms pfun_of Abs_pfun
  using infinite_imp_nonempty by auto

type_notation ffun (infixr "⇻" 1)

setup_lifting type_definition_ffun

lift_definition ffun_app :: "'a ⇻ 'b ⇒ 'a ⇒ 'b" ("_'(_')⇩f" [999,0] 999) is "pfun_app" .

lift_definition ffun_upd :: "'a ⇻ 'b ⇒ 'a ⇒ 'b ⇒ 'a ⇻ 'b" is "pfun_upd" by simp

lift_definition fdom :: "'a ⇻ 'b ⇒ 'a set" is pdom .

lift_definition fran :: "'a ⇻ 'b ⇒ 'b set" is pran .

lift_definition ffun_comp :: "('b, 'c) ffun ⇒ 'a ⇻ 'b ⇒ ('a, 'c) ffun" (infixl "∘⇩f" 55) is pfun_comp by auto

lift_definition ffun_member :: "'a × 'b ⇒ 'a ⇻ 'b ⇒ bool" (infix "∈⇩f" 50) is "(∈⇩p)" .

lift_definition fdom_res :: "'a set ⇒ 'a ⇻ 'b ⇒ 'a ⇻ 'b" (infixr "⊲⇩f" 85)
is pdom_res by simp

abbreviation fdom_nres (infixr "-⊲⇩f" 85) where "fdom_nres A P ≡ (- A) ⊲⇩f P"

lift_definition fran_res :: "'a ⇻ 'b ⇒ 'b set ⇒ 'a ⇻ 'b" (infixl "⊳⇩f" 85)
is pran_res by simp

abbreviation fran_nres (infixr "⊳⇩f-" 66) where "fran_nres P A ≡ P ⊳⇩f (- A)"

lift_definition ffun_graph :: "'a ⇻ 'b ⇒ ('a × 'b) set" is pfun_graph .

lift_definition graph_ffun :: "('a × 'b) set ⇒ 'a ⇻ 'b" is
  "λ R. if (finite (Domain R)) then graph_pfun R else pempty"
  by (simp add: finite_Domain) (meson pdom_graph_pfun rev_finite_subset)

unbundle lattice_syntax

lift_definition ffun_entries :: "'a set ⇒ ('a ⇒ 'b) ⇒ 'a ⇻ 'b" 
  is "λ A f. if (finite A) then pfun_entries A f else ⊥" by simp

instantiation ffun :: (type, type) bot
begin
lift_definition bot_ffun :: "'a ⇻ 'b" is "⊥" by simp
instance ..
end

abbreviation fempty :: "'a ⇻ 'b" ("{}⇩f")
where "fempty ≡ ⊥"

instantiation ffun :: (type, type) oplus
begin
lift_definition oplus_ffun :: "'a ⇻ 'b ⇒ 'a ⇻ 'b ⇒ 'a ⇻ 'b" is "(⊕)" by simp
instance ..
end

instantiation ffun :: (type, type) minus
begin
lift_definition minus_ffun :: "'a ⇻ 'b ⇒ 'a ⇻ 'b ⇒ 'a ⇻ 'b" is "(-)"
  by (metis Dom_pfun_graph finite_Diff finite_Domain pdom_pfun_graph_finite pfun_graph_minus)
instance ..
end

instantiation ffun :: (type, type) inf
begin
lift_definition inf_ffun :: "'a ⇻ 'b ⇒ 'a ⇻ 'b ⇒ 'a ⇻ 'b" is inf
  by (meson finite_Int infinite_super pdom_inter)
instance ..
end

abbreviation ffun_inter :: "'a ⇻ 'b ⇒ 'a ⇻ 'b ⇒ 'a ⇻ 'b" (infixl "∩⇩f" 80)
where "ffun_inter ≡ inf"

instantiation ffun :: (type, type) order
begin
  lift_definition less_eq_ffun :: "'a ⇻ 'b ⇒ 'a ⇻ 'b ⇒ bool" is
  "λ f g. f ⊆⇩p g" .
  lift_definition less_ffun :: "'a ⇻ 'b ⇒ 'a ⇻ 'b ⇒ bool" is
  "λ f g. f < g" .
instance
  by (intro_classes, (transfer, auto)+)
end

abbreviation ffun_subset :: "'a ⇻ 'b ⇒ 'a ⇻ 'b ⇒ bool" (infix "⊂⇩f" 50)
where "ffun_subset ≡ less"

abbreviation ffun_subset_eq :: "'a ⇻ 'b ⇒ 'a ⇻ 'b ⇒ bool" (infix "⊆⇩f" 50)
where "ffun_subset_eq ≡ less_eq"

instance ffun :: (type, type) semilattice_inf
  by (intro_classes, (transfer, auto)+)

lemma ffun_subset_eq_least [simp]:
  "{}⇩f ⊆⇩f f"
  by (transfer, auto)

instantiation ffun :: (type, type) size
begin

definition size_ffun :: "'a ⇻ 'b ⇒ nat" where
[simp]: "size_ffun f = card (fdom f)"

instance ..

end

syntax
  "_FfunUpd"  :: "['a ⇻ 'b, maplets] => 'a ⇻ 'b" ("_'(_')⇩f" [900,0]900)
  "_Ffun"     :: "maplets => 'a ⇻ 'b"            ("(1{_}⇩f)")

translations
  "_FfunUpd m (_Maplets xy ms)"  == "_FfunUpd (_FfunUpd m xy) ms"
  "_FfunUpd m (_maplet  x y)"    == "CONST ffun_upd m x y"
  "_Ffun ms"                     => "_FfunUpd (CONST fempty) ms"
  "_Ffun (_Maplets ms1 ms2)"     <= "_FfunUpd (_Ffun ms1) ms2"
  "_Ffun ms"                     <= "_FfunUpd (CONST fempty) ms"

subsection ‹ Algebraic laws ›

lemma ffun_comp_assoc: "f ∘⇩f (g ∘⇩f h) = (f ∘⇩f g) ∘⇩f h"
  by (transfer, simp add: pfun_comp_assoc)

lemma ffun_override_dist_comp:
  "(f ⊕ g) ∘⇩f h = (f ∘⇩f h) ⊕ (g ∘⇩f h)"
  by (transfer, simp add: pfun_override_dist_comp)

lemma ffun_minus_unit [simp]:
  fixes f :: "'a ⇻ 'b"
  shows "f - ⊥ = f"
  by (transfer, simp)

lemma ffun_minus_zero [simp]:
  fixes f :: "'a ⇻ 'b"
  shows "⊥ - f = ⊥"
  by (transfer, simp)

lemma ffun_minus_self [simp]:
  fixes f :: "'a ⇻ 'b"
  shows "f - f = ⊥"
  by (transfer, simp)

instantiation ffun :: (type, type) override
begin
  lift_definition compatible_ffun :: "'a ⇻ 'b ⇒ 'a ⇻ 'b ⇒ bool" is compatible .


instance
  by (intro_classes; transfer, simp_all add: compatible_sym override_assoc override_comm)
     (transfer, simp add: override_compat_iff)+
end
  
lemma compatible_ffun_alt_def: "R ## S = ((fdom R) ⊲⇩f S = (fdom S) ⊲⇩f R)"
  by (transfer, simp add: compatible_pfun_def)

lemma ffun_indep_compat: "fdom(f) ∩ fdom(g) = {} ⟹ f ## g"
  by (transfer, simp add: pfun_indep_compat)

lemma ffun_override_commute:
  "fdom(f) ∩ fdom(g) = {} ⟹ f ⊕ g = g ⊕ f"
  by (meson ffun_indep_compat override_comm)

lemma ffun_minus_override_commute:
  "fdom(g) ∩ fdom(h) = {} ⟹ (f - g) ⊕ h = (f ⊕ h) - g"
  by (transfer, simp add: pfun_minus_override_commute)

lemma ffun_override_minus:
  "f ⊆⇩f g ⟹ (g - f) ⊕ f = g"
  by (transfer, simp add: pfun_override_minus)

lemma ffun_minus_common_subset:
  "⟦ h ⊆⇩f f; h ⊆⇩f g ⟧ ⟹ (f - h = g - h) = (f = g)"
  by (transfer, simp add: pfun_minus_common_subset)

lemma ffun_minus_override:
  "fdom(f) ∩ fdom(g) = {} ⟹ (f ⊕ g) - g = f"
  by (transfer, simp add: pfun_minus_override)

lemma ffun_override_pos: "x ⊕ y = {}⇩f ⟹ x = {}⇩f"
  by (transfer, simp add: pfun_override_pos)

lemma ffun_le_override: "fdom x ∩ fdom y = {} ⟹ x ≤ x ⊕ y"
  by (transfer, simp add: pfun_le_override)

subsection ‹ Membership, application, and update ›

lemma ffun_ext: "⟦ ⋀ x y. (x, y) ∈⇩f f ⟷ (x, y) ∈⇩f g ⟧ ⟹ f = g"
  by (transfer, simp add: pfun_ext)

lemma ffun_member_alt_def:
  "(x, y) ∈⇩f f ⟷ (x ∈ fdom f ∧ f(x)⇩f = y)"
  by (transfer, simp add: pfun_member_alt_def)

lemma ffun_member_override:
  "(x, y) ∈⇩f f ⊕ g ⟷ ((x ∉ fdom(g) ∧ (x, y) ∈⇩f f) ∨ (x, y) ∈⇩f g)"
  by (transfer, simp add: pfun_member_override)

lemma ffun_member_minus:
  "(x, y) ∈⇩f f - g ⟷ (x, y) ∈⇩f f ∧ (¬ (x, y) ∈⇩f g)"
  by (transfer, simp add: pfun_member_minus)

lemma ffun_app_upd_1 [simp]: "x = y ⟹ (f(x ↦ v)⇩f)(y)⇩f = v"
  by (transfer, simp)

lemma ffun_app_upd_2 [simp]: "x ≠ y ⟹ (f(x ↦ v)⇩f)(y)⇩f = f(y)⇩f"
  by (transfer, simp)

lemma ffun_upd_ext [simp]: "x ∈ fdom(f) ⟹ f(x ↦ f(x)⇩f)⇩f = f"
  by (transfer, simp)

lemma ffun_app_add [simp]: "x ∈ fdom(g) ⟹ (f ⊕ g)(x)⇩f = g(x)⇩f"
  by (transfer, simp)

lemma ffun_upd_add [simp]: "f ⊕ g(x ↦ v)⇩f = (f ⊕ g)(x ↦ v)⇩f"
  by (transfer, simp)

lemma ffun_upd_twice [simp]: "f(x ↦ u, x ↦ v)⇩f = f(x ↦ v)⇩f"
  by (transfer, simp)

lemma ffun_upd_comm:
  assumes "x ≠ y"
  shows "f(y ↦ u, x ↦ v)⇩f = f(x ↦ v, y ↦ u)⇩f"
  using assms by (transfer, simp add: pfun_upd_comm)

lemma ffun_upd_add_left [simp]: "x ∉ fdom(g) ⟹ f(x ↦ v)⇩f ⊕ g = (f ⊕ g)(x ↦ v)⇩f"
  by (transfer, simp)

lemma ffun_app_add' [simp]: "⟦ e ∈ fdom f; e ∉ fdom g ⟧ ⟹ (f ⊕ g)(e)⇩f = f(e)⇩f"
  by (transfer, simp)

lemma ffun_upd_comm_linorder [simp]:
  fixes x y :: "'a :: linorder"
  assumes "x < y"
  shows "f(y ↦ u, x ↦ v)⇩f = f(x ↦ v, y ↦ u)⇩f"
  using assms by (transfer, auto)

lemma ffun_app_minus [simp]: "x ∉ fdom g ⟹ (f - g)(x)⇩f = f(x)⇩f"
  by (transfer, auto)

lemma ffun_upd_minus [simp]:
  "x ∉ fdom g ⟹ (f - g)(x ↦ v)⇩f = (f(x ↦ v)⇩f - g)"
  by (transfer, auto)

lemma fdom_member_minus_iff [simp]:
  "x ∉ fdom g ⟹ x ∈ fdom(f - g) ⟷ x ∈ fdom(f)"
  by (transfer, simp)

lemma fsubseteq_ffun_upd1 [intro]:
  "⟦ f ⊆⇩f g; x ∉ fdom(g) ⟧ ⟹ f ⊆⇩f g(x ↦ v)⇩f"
  by (transfer, auto)

lemma fsubseteq_ffun_upd2 [intro]:
  "⟦ f ⊆⇩f g; x ∉ fdom(f) ⟧ ⟹ f ⊆⇩f g(x ↦ v)⇩f"
  by (transfer, auto)

lemma psubseteq_pfun_upd3 [intro]:
  "⟦ f ⊆⇩f g; g(x)⇩f = v ⟧ ⟹ f ⊆⇩f g(x ↦ v)⇩f"
  by (transfer, auto)

lemma fsubseteq_dom_subset:
  "f ⊆⇩f g ⟹ fdom(f) ⊆ fdom(g)"
  by (transfer, auto simp add: psubseteq_dom_subset)

lemma fsubseteq_ran_subset:
  "f ⊆⇩f g ⟹ fran(f) ⊆ fran(g)"
  by (transfer, simp add: psubseteq_ran_subset)

lemma fdom_res_apply [simp]:
  "x ∈ A ⟹ (A ⊲⇩f f)(x)⇩f = f(x)⇩f"
  by (transfer, simp)

subsection ‹ Domain laws ›

lemma fdom_finite [simp]: "finite(fdom(f))"
  by (transfer, simp)

lemma fdom_zero [simp]: "fdom ⊥ = {}"
  by (transfer, simp)

lemma fdom_plus [simp]: "fdom (f ⊕ g) = fdom f ∪ fdom g"
  by (transfer, auto)

lemma fdom_inter: "fdom (f ∩⇩f g) ⊆ fdom f ∩ fdom g"
  by (transfer, meson pdom_inter)

lemma fdom_comp [simp]: "fdom (g ∘⇩f f) = fdom (f ⊳⇩f fdom g)"
  by (transfer, auto)

lemma fdom_upd [simp]: "fdom (f(k ↦ v)⇩f) = insert k (fdom f)"
  by (transfer, simp)

lemma fdom_fdom_res [simp]: "fdom (A ⊲⇩f f) = A ∩ fdom(f)"
  by (transfer, auto)

lemma ffun_fdom_antires_upd [simp]:
  "k ∈ A ⟹ ((- A) ⊲⇩f m)(k ↦ v)⇩f = ((- (A - {k})) ⊲⇩f m)(k ↦ v)⇩f"
  by (transfer, simp)

lemma fdom_res_UNIV [simp]: "UNIV ⊲⇩f f = f"
  by (transfer, simp)

lemma fdom_graph_ffun [simp]:
  "⟦ functional R; finite (Domain R) ⟧ ⟹ fdom (graph_ffun R) = Domain R"
  by (transfer, simp add: Domain_fst graph_map_dom)

lemma pdom_pfun_of [simp]: "pdom (pfun_of f) = fdom f"
  by (transfer, simp)

lemma finite_pdom_ffun [simp]: "finite (pdom (pfun_of f))"
  by (transfer, simp)

subsection ‹ Range laws ›

lemma fran_zero [simp]: "fran ⊥ = {}"
  by (transfer, simp)

lemma fran_upd [simp]: "fran (f(k ↦ v)⇩f) = insert v (fran ((- {k}) ⊲⇩f f))"
  by (transfer, auto)

lemma fran_fran_res [simp]: "fran (f ⊳⇩f A) = fran(f) ∩ A"
  by (transfer, auto)

lemma fran_comp [simp]: "fran (g ∘⇩f f) = fran (fran f ⊲⇩f g)"
  by (transfer, auto)

subsection ‹ Domain restriction laws ›

lemma fdom_res_zero [simp]: "A ⊲⇩f {}⇩f = {}⇩f"
  by (transfer, auto)

lemma fdom_res_empty [simp]:
  "({} ⊲⇩f f) = {}⇩f"
  by (transfer, auto)

lemma fdom_res_fdom [simp]:
  "fdom(f) ⊲⇩f f = f"
  by (transfer, auto)

lemma fdom_res_upd_in [simp]:
  "k ∈ A ⟹ A ⊲⇩f f(k ↦ v)⇩f = (A ⊲⇩f f)(k ↦ v)⇩f"
  by (transfer, auto)

lemma fdom_res_upd_out [simp]:
  "k ∉ A ⟹ A ⊲⇩f f(k ↦ v)⇩f = A ⊲⇩f f"
  by (transfer, auto)

lemma fdom_res_override [simp]: "A ⊲⇩f (f ⊕ g) = (A ⊲⇩f f) ⊕ (A ⊲⇩f g)"
  by (metis fdom_res.rep_eq pdom_res_override pfun_of_inject oplus_ffun.rep_eq)

lemma fdom_res_minus [simp]: "A ⊲⇩f (f - g) = (A ⊲⇩f f) - g"
  by (transfer, auto)

lemma fdom_res_swap: "(A ⊲⇩f f) ⊳⇩f B = A ⊲⇩f (f ⊳⇩f B)"
  by (transfer, simp add: pdom_res_swap)

lemma fdom_res_twice [simp]: "A ⊲⇩f (B ⊲⇩f f) = (A ∩ B) ⊲⇩f f"
  by (transfer, auto)

lemma fdom_res_comp [simp]: "A ⊲⇩f (g ∘⇩f f) =  g ∘⇩f (A ⊲⇩f f)"
  by (transfer, simp)

lemma ffun_split_domain: "A ⊲⇩f f ⊕ (- A) ⊲⇩f f = f"
  by (transfer, simp add: pfun_split_domain)

subsection ‹ Range restriction laws ›

lemma fran_res_zero [simp]: "{}⇩f ⊳⇩f A = {}⇩f"
  by (transfer, auto)

lemma fran_res_upd_1 [simp]: "v ∈ A ⟹ f(x ↦ v)⇩f ⊳⇩f A = (f ⊳⇩f A)(x ↦ v)⇩f"
  by (transfer, auto)

lemma fran_res_upd_2 [simp]: "v ∉ A ⟹ f(x ↦ v)⇩f ⊳⇩f A = ((- {x}) ⊲⇩f f) ⊳⇩f A"
  by (transfer, auto)

lemma fran_res_override: "(f ⊕ g) ⊳⇩f A ⊆⇩f (f ⊳⇩f A) ⊕ (g ⊳⇩f A)"
  by (transfer, simp add: pran_res_override)

subsection ‹ Graph laws ›

lemma ffun_graph_inv: "graph_ffun (ffun_graph f) = f"
  by (transfer, auto simp add: pfun_graph_inv finite_Domain)

lemma ffun_graph_zero: "ffun_graph ⊥ = {}"
  by (transfer, simp add: pfun_graph_zero)

lemma ffun_graph_minus: "ffun_graph (f - g) = ffun_graph f - ffun_graph g"
  by (transfer, simp add: pfun_graph_minus)

lemma ffun_graph_inter: "ffun_graph (f ∩⇩f g) = ffun_graph f ∩ ffun_graph g"
  by (transfer, simp add: pfun_graph_inter)

subsection ‹ Conversions ›

lift_definition list_ffun :: "'a list ⇒ nat ⇻ 'a" is
list_pfun by simp

lemma fdom_list_ffun [simp]: "fdom (list_ffun xs) = {1..length xs}"
  by (transfer, auto)

lemma fran_list_ffun [simp]: "fran (list_ffun xs) = set xs"
  by (transfer, simp)

lemma ffun_app_list_ffun: "⟦ 0 < i; i < length xs ⟧ ⟹ (list_ffun xs)(i)⇩f = xs ! (i - 1)"
  by (transfer, simp add: pfun_app_list_pfun)

lemma range_list_ffun: "range list_ffun = {f. ∃ i. fdom(f) = {1..i}}"
  by (transfer, auto simp add: range_list_pfun)

subsection ‹ Finite Function Lens ›

definition ffun_lens :: "'a ⇒ ('b ⟹ 'a ⇻ 'b)" where
[lens_defs]: "ffun_lens i = ⦇ lens_get = λ s. s(i)⇩f, lens_put = λ s v. s(i ↦ v)⇩f ⦈"

lemma ffun_lens_mwb [simp]: "mwb_lens (ffun_lens i)"
  by (unfold_locales, simp_all add: ffun_lens_def)

lemma ffun_lens_src: "𝒮⇘ffun_lens i⇙ = {f. i ∈ fdom(f)}"
  by (auto simp add: lens_defs lens_source_def, metis ffun_upd_ext)

subsection ‹ Notation ›

bundle Z_Ffun_Notation
begin

no_notation "Stream.stream.SCons" (infixr ‹##› 65)

no_notation funcset (infixr "→" 60)

notation fdom_res (infixr "◁" 86)
notation fdom_nres (infixr "⩤" 86)

notation fran_res (infixl "▷" 86)
notation fran_nres (infixl "⩥" 86)

notation fempty ("{↦}")

syntax "_Ffun"     :: "maplets => logic" ("(1{_})")

end


text ‹ Hide implementation details for finite functions ›

lifting_update ffun.lifting
lifting_forget ffun.lifting

end