Quelle  Finite_Fun.thy

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: "S _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