Theory Finite_Fun

(******************************************************************************)
(* Project: Isabelle/UTP Toolkit                                              *)
(* File: Finite_Fun.thy                                                       *)
(* Authors: Simon Foster and Frank Zeyda                                      *)
(* Emails: simon.foster@york.ac.uk and frank.zeyda@york.ac.uk                 *)
(******************************************************************************)

section ‹ Finite Functions ›

theory Finite_Fun
imports Map_Extra Partial_Fun FSet_Extra
begin

subsection ‹ Finite function type and operations ›

typedef ('a, 'b) ffun = "{f :: ('a, 'b) pfun. finite(pdom(f))}"
  morphisms pfun_of Abs_pfun
  by (rule_tac x="{}⇩p" in exI, auto)

setup_lifting type_definition_ffun

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

lift_definition ffun_upd :: "('a, 'b) ffun ⇒ 'a ⇒ 'b ⇒ ('a, 'b) ffun" is "pfun_upd" by simp

lift_definition fdom :: "('a, 'b) ffun ⇒ 'a set" is pdom .

lift_definition fran :: "('a, 'b) ffun ⇒ 'b set" is pran .

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

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

lift_definition fdom_res :: "'a set ⇒ ('a, 'b) ffun ⇒ ('a, 'b) ffun" (infixl ‹⊲⇩f› 85)
is "pdom_res" by simp

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

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

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

instantiation ffun :: (type, type) zero
begin
lift_definition zero_ffun :: "('a, 'b) ffun" is "0" by simp
instance ..
end

abbreviation fempty :: "('a, 'b) ffun" (‹{}⇩f›)
where "fempty ≡ 0"

instantiation ffun :: (type, type) plus
begin
lift_definition plus_ffun :: "('a, 'b) ffun ⇒ ('a, 'b) ffun ⇒ ('a, 'b) ffun" is "(+)" by simp
instance ..
end

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

instance ffun :: (type, type) monoid_add
  by (intro_classes, (transfer, simp add: add.assoc)+)

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

abbreviation ffun_inter :: "('a, 'b) ffun ⇒ ('a, 'b) ffun ⇒ ('a, 'b) ffun" (infixl ‹∩⇩f› 80)
where "ffun_inter ≡ inf"

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

abbreviation ffun_subset :: "('a, 'b) ffun ⇒ ('a, 'b) ffun ⇒ bool" (infix ‹⊂⇩f› 50)
where "ffun_subset ≡ less"

abbreviation ffun_subset_eq :: "('a, 'b) ffun ⇒ ('a, 'b) ffun ⇒ 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)

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

syntax_consts
  "_FfunUpd" "_Ffun" ⇌ ffun_upd
  
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 pfun_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) ffun"
  shows "f - 0 = f"
  by (transfer, simp)

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

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

lemma ffun_plus_commute:
  "fdom(f) ∩ fdom(g) = {} ⟹ f + g = g + f"
  by (transfer, metis pfun_plus_commute)

lemma ffun_minus_plus_commute:
  "fdom(g) ∩ fdom(h) = {} ⟹ (f - g) + h = (f + h) - g"
  by (transfer, simp add: pfun_minus_plus_commute)

lemma ffun_plus_minus:
  "f ⊆⇩f g ⟹ (g - f) + f = g"
  by (transfer, simp add: pfun_plus_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_plus:
  "fdom(f) ∩ fdom(g) = {} ⟹ (f + g) - g = f"
  by (transfer, simp add: pfun_minus_plus)

lemma ffun_plus_pos: "x + y = {}⇩f ⟹ x = {}⇩f"
  by (transfer, simp add: pfun_plus_pos)

lemma ffun_le_plus: "fdom x ∩ fdom y = {} ⟹ x ≤ x + y"
  by (transfer, simp add: pfun_le_plus)

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_plus:
  "(x, y) ∈⇩f f + g ⟷ ((x ∉ fdom(g) ∧ (x, y) ∈⇩f f) ∨ (x, y) ∈⇩f g)"
  by (transfer, simp add: pfun_member_plus)

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_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)

subsection ‹ Domain laws ›

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

lemma fdom_zero [simp]: "fdom 0 = {}"
  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 fdom_graph_ffun [simp]:
  "finite (Domain R) ⟹ fdom (graph_ffun R) = Domain R"
  by (transfer, simp add: Domain_fst graph_map_dom)

subsection ‹ Range laws ›

lemma fran_zero [simp]: "fran 0 = {}"
  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 pdom_res_upd_in [simp]:
  "k ∈ A ⟹ A ⊲⇩f f(k ↦ v)⇩f = (A ⊲⇩f f)(k ↦ v)⇩f"
  by (transfer, auto)

lemma pdom_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 plus_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)

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 0 = {}"
  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 ‹ Partial Function Lens ›

definition ffun_lens :: "'a ⇒ ('b ⟹ ('a, 'b) ffun)" 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)

text ‹ Hide implementation details for finite functions ›

lifting_update ffun.lifting
lifting_forget ffun.lifting

end