Theory Partial_Fun

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

section ‹ Partial Functions ›

theory Partial_Fun
imports "Optics.Lenses" Map_Extra
begin

text ‹ I'm not completely satisfied with partial functions as provided by Map.thy, since they don't
        have a unique type and so we can't instantiate classes, make use of adhoc-overloading
        etc. Consequently I've created a new type and derived the laws. ›

subsection ‹ Partial function type and operations ›

typedef ('a, 'b) pfun = "UNIV :: ('a ⇀ 'b) set" ..

setup_lifting type_definition_pfun

lift_definition pfun_app :: "('a, 'b) pfun ⇒ 'a ⇒ 'b" (‹_'(_')⇩p› [999,0] 999) is 
"λ f x. if (x ∈ dom f) then the (f x) else undefined" .

lift_definition pfun_upd :: "('a, 'b) pfun ⇒ 'a ⇒ 'b ⇒ ('a, 'b) pfun"
is "λ f k v. f(k := Some v)" .

lift_definition pdom :: "('a, 'b) pfun ⇒ 'a set" is dom .

lift_definition pran :: "('a, 'b) pfun ⇒ 'b set" is ran .

lift_definition pfun_comp :: "('b, 'c) pfun ⇒ ('a, 'b) pfun ⇒ ('a, 'c) pfun" (infixl ‹∘⇩p› 55) is map_comp .

lift_definition pfun_member :: "'a × 'b ⇒ ('a, 'b) pfun ⇒ bool" (infix ‹∈⇩p› 50) is "(∈⇩m)" .

lift_definition pId_on :: "'a set ⇒ ('a, 'a) pfun" is "λ A x. if (x ∈ A) then Some x else None" .

abbreviation pId :: "('a, 'a) pfun" where
"pId ≡ pId_on UNIV"

lift_definition plambda :: "('a ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ ('a, 'b) pfun"
is "λ P f x. if (P x) then Some (f x) else None" .

lift_definition pdom_res :: "'a set ⇒ ('a, 'b) pfun ⇒ ('a, 'b) pfun" (infixl ‹⊲⇩p› 85)
is "λ A f. restrict_map f A" .

lift_definition pran_res :: "('a, 'b) pfun ⇒ 'b set ⇒ ('a, 'b) pfun" (infixl ‹⊳⇩p› 85)
is ran_restrict_map .

lift_definition pfun_graph :: "('a, 'b) pfun ⇒ ('a × 'b) set" is map_graph .

lift_definition graph_pfun :: "('a × 'b) set ⇒ ('a, 'b) pfun" is graph_map .

lift_definition pfun_entries :: "'k set ⇒ ('k ⇒ 'v) ⇒ ('k, 'v) pfun" is
"λ d f x. if (x ∈ d) then Some (f x) else None" .
    
definition pcard :: "('a, 'b) pfun ⇒ nat"
where "pcard f = card (pdom f)"

instantiation pfun :: (type, type) zero
begin
lift_definition zero_pfun :: "('a, 'b) pfun" is "Map.empty" .
instance ..
end

abbreviation pempty :: "('a, 'b) pfun" (‹{}⇩p›)
where "pempty ≡ 0"

instantiation pfun :: (type, type) plus
begin
lift_definition plus_pfun :: "('a, 'b) pfun ⇒ ('a, 'b) pfun ⇒ ('a, 'b) pfun" is "(++)" .
instance ..
end

instantiation pfun :: (type, type) minus
begin
lift_definition minus_pfun :: "('a, 'b) pfun ⇒ ('a, 'b) pfun ⇒ ('a, 'b) pfun" is "(--)" .
instance ..
end

instance pfun :: (type, type) monoid_add
  by (intro_classes, (transfer, auto)+)

instantiation pfun :: (type, type) inf
begin
lift_definition inf_pfun :: "('a, 'b) pfun ⇒ ('a, 'b) pfun ⇒ ('a, 'b) pfun" is
"λ f g x. if (x ∈ dom(f) ∩ dom(g) ∧ f(x) = g(x)) then f(x) else None" .
instance ..
end

abbreviation pfun_inter :: "('a, 'b) pfun ⇒ ('a, 'b) pfun ⇒ ('a, 'b) pfun" (infixl ‹∩⇩p› 80)
where "pfun_inter ≡ inf"

instantiation pfun :: (type, type) order
begin
  lift_definition less_eq_pfun :: "('a, 'b) pfun ⇒ ('a, 'b) pfun ⇒ bool" is
  "λ f g. f ⊆⇩m g" .
  lift_definition less_pfun :: "('a, 'b) pfun ⇒ ('a, 'b) pfun ⇒ bool" is
  "λ f g. f ⊆⇩m g ∧ f ≠ g" .
instance
  by (intro_classes, (transfer, auto intro: map_le_trans simp add: map_le_antisym)+)
end

abbreviation pfun_subset :: "('a, 'b) pfun ⇒ ('a, 'b) pfun ⇒ bool" (infix ‹⊂⇩p› 50)
where "pfun_subset ≡ less"

abbreviation pfun_subset_eq :: "('a, 'b) pfun ⇒ ('a, 'b) pfun ⇒ bool" (infix ‹⊆⇩p› 50)
where "pfun_subset_eq ≡ less_eq"

instance pfun :: (type, type) semilattice_inf
  by (intro_classes, (transfer, auto simp add: map_le_def dom_def)+)

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

syntax
  "_PfunUpd"  :: "[('a, 'b) pfun, maplets] => ('a, 'b) pfun" (‹_'(_')⇩p› [900,0]900)
  "_Pfun"     :: "maplets => ('a, 'b) pfun"            (‹(1{_}⇩p)›)
  "_plam"     :: "pttrn ⇒ logic ⇒ logic ⇒ logic" (‹λ _ | _ . _› [0,0,10] 10)

syntax_consts
  "_PfunUpd" "_Pfun" == pfun_upd and
  "_plam" == plambda

translations
  "_PfunUpd m (_Maplets xy ms)"  == "_PfunUpd (_PfunUpd m xy) ms"
  "_PfunUpd m (_maplet  x y)"    == "CONST pfun_upd m x y"
  "_Pfun ms"                     => "_PfunUpd (CONST pempty) ms"
  "_Pfun (_Maplets ms1 ms2)"     <= "_PfunUpd (_Pfun ms1) ms2"
  "_Pfun ms"                     <= "_PfunUpd (CONST pempty) ms"
  "λ x | P . e"                  => "CONST plambda (λ x. P) (λ x. e)"
  "λ x | P . e"                  <= "CONST plambda (λ x. P) (λ y. e)"
  "λ y | P . e"                  <= "CONST plambda (λ x. P) (λ y. e)"
  "λ y | f v y . e"              <= "CONST plambda (f v) (λ y. e)"

subsection ‹ Algebraic laws ›

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

lemma pfun_comp_left_id [simp]: "pId ∘⇩p f = f"
  by (transfer, auto)

lemma pfun_comp_right_id [simp]: "f ∘⇩p pId = f"
  by (transfer, auto)

lemma pfun_override_dist_comp:
  "(f + g) ∘⇩p h = (f ∘⇩p h) + (g ∘⇩p h)"
  apply (transfer)
  apply (rule ext)
  apply (auto simp add: map_add_def)
  apply (rename_tac f g h x)
  apply (case_tac "h x")
   apply (auto)
  apply (rename_tac f g h x y)
  apply (case_tac "g y")
   apply (auto)
  done

lemma pfun_minus_unit [simp]:
  fixes f :: "('a, 'b) pfun"
  shows "f - 0 = f"
  by (transfer, simp add: map_minus_def)

lemma pfun_minus_zero [simp]:
  fixes f :: "('a, 'b) pfun"
  shows "0 - f = 0"
  by (transfer, simp add: map_minus_def)

lemma pfun_minus_self [simp]:
  fixes f :: "('a, 'b) pfun"
  shows "f - f = 0"
  by (transfer, simp add: map_minus_def)

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

lemma pfun_plus_commute_weak:
  "(∀ k ∈ pdom(f) ∩ pdom(g). f(k)⇩p = g(k)⇩p) ⟹ f + g = g + f"
  by (transfer, simp, metis IntD1 IntD2 domD map_add_comm_weak option.sel)

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

lemma pfun_plus_minus:
  "f ⊆⇩p g ⟹ (g - f) + f = g"
  by (transfer, rule ext, auto simp add: map_le_def map_minus_def map_add_def option.case_eq_if)

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

lemma pfun_minus_plus:
  "pdom(f) ∩ pdom(g) = {} ⟹ (f + g) - g = f"
  by (transfer, simp add: map_add_def map_minus_def option.case_eq_if, rule ext, auto)
     (metis Int_commute domIff insert_disjoint(1) insert_dom)

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

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

subsection ‹ Lambda abstraction ›

lemma plambda_app [simp]: "(λ x | P x . f x)(v)⇩p = (if (P v) then (f v) else undefined)"
  by (transfer, auto)

lemma plambda_eta [simp]: "(λ x | x ∈ pdom(f). f(x)⇩p) = f"
  by (transfer; auto simp add: domIff)

lemma plambda_id [simp]: "(λ x | P x . x) = pId_on {x. P x}"
  by (transfer, simp)

subsection ‹ Membership, application, and update ›

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

lemma pfun_member_alt_def:
  "(x, y) ∈⇩p f ⟷ (x ∈ pdom f ∧ f(x)⇩p = y)"
  by (transfer, auto simp add: map_member_alt_def map_apply_def)

lemma pfun_member_plus:
  "(x, y) ∈⇩p f + g ⟷ ((x ∉ pdom(g) ∧ (x, y) ∈⇩p f) ∨ (x, y) ∈⇩p g)"
  by (transfer, simp add: map_member_plus)

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

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

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

lemma pfun_upd_ext [simp]: "x ∈ pdom(f) ⟹ f(x ↦ f(x)⇩p)⇩p = f"
  by (transfer, simp add: domIff)

lemma pfun_app_add [simp]: "x ∈ pdom(g) ⟹ (f + g)(x)⇩p = g(x)⇩p"
  by (transfer, auto)

lemma pfun_upd_add [simp]: "f + g(x ↦ v)⇩p = (f + g)(x ↦ v)⇩p"
  by (transfer, simp)

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

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

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

lemma pfun_app_minus [simp]: "x ∉ pdom g ⟹ (f - g)(x)⇩p = f(x)⇩p"
  by (transfer, auto simp add: map_minus_def)

lemma pfun_app_empty [simp]: "{}⇩p(x)⇩p = undefined"
  by (transfer, simp)

lemma pfun_app_not_in_dom: 
  "x ∉ pdom(f) ⟹ f(x)⇩p = undefined"
  by (transfer, simp)

lemma pfun_upd_minus [simp]:
  "x ∉ pdom g ⟹ (f - g)(x ↦ v)⇩p = (f(x ↦ v)⇩p - g)"
  by (transfer, auto simp add: map_minus_def)

lemma pdom_member_minus_iff [simp]:
  "x ∉ pdom g ⟹ x ∈ pdom(f - g) ⟷ x ∈ pdom(f)"
  by (transfer, simp add: domIff map_minus_def)

lemma psubseteq_pfun_upd1 [intro]:
  "⟦ f ⊆⇩p g; x ∉ pdom(g) ⟧ ⟹ f ⊆⇩p g(x ↦ v)⇩p"
  by (transfer, auto simp add: map_le_def dom_def)

lemma psubseteq_pfun_upd2 [intro]:
  "⟦ f ⊆⇩p g; x ∉ pdom(f) ⟧ ⟹ f ⊆⇩p g(x ↦ v)⇩p"
  by (transfer, auto simp add: map_le_def dom_def)

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

lemma psubseteq_dom_subset:
  "f ⊆⇩p g ⟹ pdom(f) ⊆ pdom(g)"
  by (transfer, auto simp add: map_le_def dom_def)

lemma psubseteq_ran_subset:
  "f ⊆⇩p g ⟹ pran(f) ⊆ pran(g)"
  by (transfer, auto simp add: map_le_def dom_def ran_def, fastforce)

subsection ‹ Domain laws ›

lemma pdom_zero [simp]: "pdom 0 = {}"
  by (transfer, simp)

lemma pdom_pId_on [simp]: "pdom (pId_on A) = A"
  by (transfer, auto)

lemma pdom_plus [simp]: "pdom (f + g) = pdom f ∪ pdom g"
  by (transfer, auto)

lemma pdom_minus [simp]: "g ≤ f ⟹ pdom (f - g) = pdom f - pdom g"
  apply (transfer, auto simp add: map_minus_def)
  apply (meson option.distinct(1))
  apply (metis domIff map_le_def option.simps(3))
  done

lemma pdom_inter: "pdom (f ∩⇩p g) ⊆ pdom f ∩ pdom g"
  by (transfer, auto simp add: dom_def)

lemma pdom_comp [simp]: "pdom (g ∘⇩p f) = pdom (f ⊳⇩p pdom g)"
  by (transfer, auto simp add: ran_restrict_map_def)

lemma pdom_upd [simp]: "pdom (f(k ↦ v)⇩p) = insert k (pdom f)"
  by (transfer, simp)

lemma pdom_plamda [simp]: "pdom (λ x | P x . f x) = {x. P x}"
  by (transfer, auto)

lemma pdom_pdom_res [simp]: "pdom (A ⊲⇩p f) = A ∩ pdom(f)"
  by (transfer, auto)

lemma pdom_graph_pfun [simp]: "pdom (graph_pfun R) = Domain R"
  by (transfer, simp add: Domain_fst graph_map_dom)

lemma pdom_pran_res_finite [simp]:
  "finite (pdom f) ⟹ finite (pdom (f ⊳⇩p A))"
  by (transfer, auto)

lemma pdom_pfun_graph_finite [simp]:
  "finite (pdom f) ⟹ finite (pfun_graph f)"
  by (transfer, simp add: finite_dom_graph)

subsection ‹ Range laws ›

lemma pran_zero [simp]: "pran 0 = {}"
  by (transfer, simp)

lemma pran_pId_on [simp]: "pran (pId_on A) = A"
  by (transfer, auto simp add: ran_def)

lemma pran_upd [simp]: "pran (f(k ↦ v)⇩p) = insert v (pran ((- {k}) ⊲⇩p f))"
  by (transfer, auto simp add: ran_def restrict_map_def)

lemma pran_plamda [simp]: "pran (λ x | P x . f x) = {f x | x. P x}"
  by (transfer, auto simp add: ran_def)

lemma pran_pran_res [simp]: "pran (f ⊳⇩p A) = pran(f) ∩ A"
  by (transfer, auto)

lemma pran_comp [simp]: "pran (g ∘⇩p f) = pran (pran f ⊲⇩p g)"
  by (transfer, auto simp add: ran_def restrict_map_def)

lemma pran_finite [simp]: "finite (pdom f) ⟹ finite (pran f)"
  by (transfer, auto)

subsection ‹ Domain restriction laws ›

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

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

lemma pdom_res_pdom [simp]:
  "pdom(f) ⊲⇩p f = f"
  by (transfer, auto)

lemma pdom_res_UNIV [simp]: "UNIV ⊲⇩p f = f"
  by (transfer, auto)
    
lemma pdom_res_alt_def: "A ⊲⇩p f =  f ∘⇩p pId_on A"
  by (transfer, rule ext, auto simp add: restrict_map_def)

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

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

lemma pdom_antires_insert_notin [simp]:
  "k ∉ pdom(f) ⟹ (- insert k A) ⊲⇩p f = (- A) ⊲⇩p f"
  by (transfer, auto simp add: restrict_map_def)
 
lemma pdom_res_override [simp]: "A ⊲⇩p (f + g) = (A ⊲⇩p f) + (A ⊲⇩p g)"
  by (simp add: pdom_res_alt_def pfun_override_dist_comp)

lemma pdom_res_minus [simp]: "A ⊲⇩p (f - g) = (A ⊲⇩p f) - g"
  by (transfer, auto simp add: map_minus_def restrict_map_def)

lemma pdom_res_swap: "(A ⊲⇩p f) ⊳⇩p B = A ⊲⇩p (f ⊳⇩p B)"
  by (transfer, auto simp add: restrict_map_def ran_restrict_map_def)

lemma pdom_res_twice [simp]: "A ⊲⇩p (B ⊲⇩p f) = (A ∩ B) ⊲⇩p f"
  by (transfer, auto simp add: Int_commute)

lemma pdom_res_comp [simp]: "A ⊲⇩p (g ∘⇩p f) =  g ∘⇩p (A ⊲⇩p f)"
  by (simp add: pdom_res_alt_def pfun_comp_assoc)

lemma pdom_res_apply [simp]:
  "x ∈ A ⟹ (A ⊲⇩p f)(x)⇩p = f(x)⇩p"
  by (transfer, auto)
    
subsection ‹ Range restriction laws ›

lemma pran_res_zero [simp]: "{}⇩p ⊳⇩p A = {}⇩p"
  by (transfer, auto simp add: ran_restrict_map_def)

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

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

lemma pran_res_alt_def: "f ⊳⇩p A = pId_on A ∘⇩p f"
  by (transfer, rule ext, auto simp add: ran_restrict_map_def)

lemma pran_res_override: "(f + g) ⊳⇩p A ⊆⇩p (f ⊳⇩p A) + (g ⊳⇩p A)"
  apply (transfer, auto simp add: map_add_def ran_restrict_map_def map_le_def)
  apply (rename_tac f g A a y x)
  apply (case_tac "g a")
   apply (auto)
  done

subsection ‹ Graph laws ›

lemma pfun_graph_inv: "graph_pfun (pfun_graph f) = f"
  by (transfer, simp)

lemma pfun_graph_zero: "pfun_graph 0 = {}"
  by (transfer, simp add: map_graph_def)

lemma pfun_graph_pId_on: "pfun_graph (pId_on A) = Id_on A"
  by (transfer, auto simp add: map_graph_def)

lemma pfun_graph_minus: "pfun_graph (f - g) = pfun_graph f - pfun_graph g"
  by (transfer, simp add: map_graph_minus)

lemma pfun_graph_inter: "pfun_graph (f ∩⇩p g) = pfun_graph f ∩ pfun_graph g"
  apply (transfer, auto simp add: map_graph_def)
   apply (metis option.discI)+
  done

subsection ‹ Entries ›
  
lemma pfun_entries_empty [simp]: "pfun_entries {} f = {}⇩p"
  by (transfer, simp)

lemma pfun_entries_apply_1 [simp]: 
  "x ∈ d ⟹ (pfun_entries d f)(x)⇩p = f x"
  by (transfer, auto)

lemma pfun_entries_apply_2 [simp]: 
  "x ∉ d ⟹ (pfun_entries d f)(x)⇩p = undefined"
  by (transfer, auto)

subsection ‹ Summation ›
    
definition pfun_sum :: "('k, 'v::comm_monoid_add) pfun ⇒ 'v" where
"pfun_sum f = sum (pfun_app f) (pdom f)"
    
lemma pfun_sum_empty [simp]: "pfun_sum {}⇩p = 0"
  by (simp add: pfun_sum_def)

lemma pfun_sum_upd_1:
  assumes "finite(pdom(m))" "k ∉ pdom(m)"
  shows "pfun_sum (m(k ↦ v)⇩p) = pfun_sum m + v"
  by (simp_all add: pfun_sum_def assms, metis add.commute assms(2) pfun_app_upd_2 sum.cong)

lemma pfun_sums_upd_2:
  assumes "finite(pdom(m))"
  shows "pfun_sum (m(k ↦ v)⇩p) = pfun_sum ((- {k}) ⊲⇩p m) + v"
proof (cases "k ∉ pdom(m)")
  case True
  then show ?thesis 
    by (simp add: pfun_sum_upd_1 assms)
next
  case False
  then show ?thesis
    using assms pfun_sum_upd_1[of "((- {k}) ⊲⇩p m)" k v]
    by (simp add: pfun_sum_upd_1)
qed

lemma pfun_sum_dom_res_insert [simp]: 
  assumes "x ∈ pdom f" "x ∉ A" "finite A" 
  shows "pfun_sum ((insert x A) ⊲⇩p f) = f(x)⇩p + pfun_sum (A ⊲⇩p f)"
  using assms by (simp add: pfun_sum_def)
  
lemma pfun_sum_pdom_res:
  fixes f :: "('a,'b::ab_group_add) pfun"
  assumes "finite(pdom f)"
  shows "pfun_sum (A ⊲⇩p f) = pfun_sum f - (pfun_sum ((- A) ⊲⇩p f))"
proof -
  have 1:"A ∩ pdom(f) = pdom(f) - (pdom(f) - A)"
    by (auto)
  show ?thesis
    apply (simp add: pfun_sum_def)
    apply (subst 1)
    apply (subst sum_diff)
      apply (auto simp add: sum_diff Diff_subset Int_commute boolean_algebra_class.diff_eq assms)
    done
qed
  
lemma pfun_sum_pdom_antires [simp]:
  fixes f :: "('a,'b::ab_group_add) pfun"
  assumes "finite(pdom f)"
  shows "pfun_sum ((- A) ⊲⇩p f) = pfun_sum f - pfun_sum (A ⊲⇩p f)"
  by (subst pfun_sum_pdom_res, simp_all add: assms)

subsection ‹ Partial Function Lens ›

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

lemma pfun_lens_mwb [simp]: "mwb_lens (pfun_lens i)"
  by (unfold_locales, simp_all add: pfun_lens_def)

lemma pfun_lens_src: "𝒮⇘pfun_lens i⇙ = {f. i ∈ pdom(f)}"
  by (auto simp add: lens_defs lens_source_def, transfer, force)

text ‹ Hide implementation details for partial functions ›

lifting_update pfun.lifting
lifting_forget pfun.lifting

end