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