Quelle  Partial_Fun.thy

section ‹ Partial Functions ›

theory Partial_Fun
imports "Optics.Optics" Map_Extra "HOL-Library.Mapping"
begin

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

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"
  morphisms pfun_lookup pfun_of_map ..

type_notation pfun (infixr "🍋" 1)

setup_lifting type_definition_pfun

lemma pfun_lookup_map [simp]: "pfun_lookup (pfun_of_map f) = f"
  by (simp add: pfun_of_map_inverse)

lift_bnf ('k, pran: 'v) pfun [wits: "Map.empty :: 'k ==> 'v option"] for map: map_pfun rel: relt_pfun
  by auto

declare pfun.map_transfer [transfer_rule]

instantiation pfun :: (type, type) equal
begin

definition "HOL.equal m1 m2 ⟷ (∀k. pfun_lookup m1 k = pfun_lookup m2 k)"

instance 
  by (intro_classes, simp add: equal_pfun_def, transfer, auto)

end

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 .

lemma pran_rep_eq [transfer_rule]: "pran f = ran (pfun_lookup f)"
  by (transfer, auto simp add: ran_def)

lift_definition pfun_comp :: "('b, 'c) pfun ==> ('a, 'b) pfun ==> ('a, 'c) pfun" (infixl "∘_p" 55) is 
  "λ f g. f ∘_m g" .

lift_definition map_pfun' :: "('c ==> 'a) ==> ('b ==> 'd) ==> ('a, 'b) pfun ==> ('c, 'd) pfun"
  is "λf g m. (map_option g ∘ m ∘ f)" parametric map_parametric .

functor map_pfun'
  by (transfer, auto simp add: fun_eq_iff option.map_comp option.map_id)+

lift_definition pfun_member :: "'a × 'b ==> ('a, 'b) pfun ==> bool" (infix "∈_p" 50) is "(∈_m)" .

lift_definition pfun_inj :: "('a, 'b) pfun ==> bool" is "λ f. inj_on f (dom f)" .

lift_definition pfun_inv :: "('a, 'b) pfun ==> ('b, 'a) pfun" is map_inv .

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 pdom_res :: "'a set ==> ('a, 'b) pfun ==> ('a, 'b) pfun" (infixr "⊲_p" 85)
is "λ A f. restrict_map f A" .

abbreviation pdom_nres (infixr "-⊲_p" 85) where "pdom_nres A P ≡ (- A) ⊲_p P"

lift_definition pran_res :: "('a, 'b) pfun ==> 'b set ==> ('a, 'b) pfun" (infixl "⊳_p" 86)
is ran_restrict_map .

abbreviation pran_nres (infixr "⊳_p-" 66) where "pran_nres P A ≡ P ⊳_p (- A)"

definition pfun_image :: "'a 🍋 'b ==> 'a set ==> 'b set" where
[simp]: "pfun_image f A = pran (A ⊲_p f)"

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 ∘ mk_functional" .

definition pfun_pfun :: "'a set ==> 'b set ==> ('a 🍋 'b) set" where
"pfun_pfun A B = {f :: 'a 🍋 'b. pdom(f) ⊆ A ∧ pran(f) ⊆ B}"

definition pfun_tfun :: "'a set ==> 'b set ==> ('a 🍋 'b) set" where
"pfun_tfun A B = {f ∈ pfun_pfun A B. pdom(f) = UNIV}"

definition pfun_ffun :: "'a set ==> 'b set ==> ('a 🍋 'b) set" where
"pfun_ffun A B = {f ∈ pfun_pfun A B. finite(pdom(f))}"

definition pfun_pinj :: "'a set ==> 'b set ==> ('a 🍋 'b) set" where
"pfun_pinj A B = {f ∈ pfun_pfun A B. pfun_inj f}"

definition pfun_psurj :: "'a set ==> 'b set ==> ('a 🍋 'b) set" where
"pfun_psurj A B = {f ∈ pfun_pfun A B. pran(f) = UNIV}"

definition "pfun_finj A B = pfun_ffun A B ∩ pfun_pinj A B"
definition "pfun_tinj A B = pfun_tfun A B ∩ pfun_pinj A B"
definition "pfun_tsurj A B = pfun_tfun A B ∩ pfun_psurj A B"
definition "pfun_bij A B = pfun_tfun A B ∩ pfun_pinj A B ∩ pfun_psurj A B"

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 pfuse :: "('a 🍋 'b) ==> ('a 🍋 'c) ==> ('a 🍋 'b × 'c)"
  where "pfuse f g = pfun_entries (pdom(f) ∩ pdom(g)) (λ x. (pfun_app f x, pfun_app g x))"

lift_definition ptabulate :: "'a list ==> ('a ==> 'b) ==> ('a, 'b) pfun"
  is "λks f. (map_of (List.map (λk. (k, f k)) ks))" .

lift_definition pcombine ::
  "('b ==> 'b ==> 'b) ==> ('a, 'b) pfun ==> ('a, 'b) pfun ==> ('a, 'b) pfun"
  is "λf m1 m2 x. combine_options f (m1 x) (m2 x)" .

abbreviation "fun_pfun ≡ pfun_entries UNIV"

definition pfun_disjoint :: "'a 🍋 'b set ==> bool" where
"pfun_disjoint S = (∀ i ∈ pdom S. ∀ j ∈ pdom S. i ≠ j ⟶ pfun_app S i ∩ pfun_app S j = {})"

definition pfun_partitions :: "'a 🍋 'b set ==> 'b set ==> bool" where
"pfun_partitions S T = (pfun_disjoint S ∧ ∪ (pran S) = T)"

no_notation disj (infixr "|" 30)

definition pabs :: "'a set ==> ('a ==> bool) ==> ('a ==> 'b) ==> 'a 🍋 'b" where
"pabs A P f = (A ∩ Collect P) ⊲_p fun_pfun f"

definition pcard :: "('a, 'b) pfun ==> nat"
where "pcard f = card (pdom f)"

unbundle lattice_syntax

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

abbreviation pempty :: "('a, 'b) pfun" ("{}_p")
where "pempty ≡ bot"

instantiation pfun :: (type, type) oplus
begin
lift_definition oplus_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

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)")
  "_pabs"      :: "pttrn ==> logic ==> logic ==> logic ==> logic" ("λ _ ∈ _ | _ ∙ _" [0, 0, 0, 10] 10)
  "_pabs_mem"  :: "pttrn ==> logic ==> logic ==> logic ==> logic" ("λ _ ∈ _ ∙ _" [0, 0, 10] 10)
  "_pabs_pred" :: "pttrn ==> logic ==> logic ==> logic ==> logic" ("λ _ | _ ∙ _" [0, 0, 10] 10)
  "_pabs_tot"  :: "pttrn ==> logic ==> logic" ("λ _ ∙ _" [0, 10] 10)

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"
  "_pabs x A P f" => "CONST pabs A (λ x. P) (λ x. f)"
  "_pabs x A P f" <= "CONST pabs A (λ y. P) (λ x. f)"
  "_pabs x A P (f x)" <= "CONST pabs A (λ x. P) f"
  "_pabs_mem x A f" == "_pabs x A (CONST True) f"
  "_pabs_pred x P f" == "_pabs x (CONST UNIV) P f"
  "_pabs_tot x f" == "_pabs_pred x (CONST True) f"
  "_pabs_tot x f" <= "_pabs_mem x (CONST UNIV) f"

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_comp_left_zero [simp]: "{}_p ∘_p f = {}_p"
  by (transfer, auto)

lemma pfun_comp_right_zero [simp]: "f ∘_p {}_p = {}_p"
  by (transfer, auto)

lemma pfun_override_dist_comp:
  "(f ⊕ g) ∘_p h = (f ∘_p h) ⊕ (g ∘_p h)"
  apply (transfer)
  apply (rule ext)
  apply (simp add: map_add_def)
  apply (metis (no_types, lifting) bind.bind_lunit bind_eq_None_conv map_comp_def option.case_eq_if option.collapse)
  done

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

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

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

instantiation pfun :: (type, type) override
begin
  definition compatible_pfun :: "'a 🍋 'b ==> 'a 🍋 'b ==> bool" where
  "compatible_pfun R S = ((pdom R) ⊲_p S = (pdom S) ⊲_p R)"

lemma pfun_compat_add: "(P :: 'a 🍋 'b) ## Q ==> P ⊕ Q ## R ==> P ## R"
  apply (simp add: compatible_pfun_def oplus_pfun_def)
  apply (transfer)
  using map_compat_add apply auto
  done

lemma pfun_compat_addI: "[ (P :: 'a 🍋 'b) ## Q; P ## R; Q ## R ] ==> P ⊕ Q ## R"
  apply (simp add: compatible_pfun_def oplus_pfun_def)
  apply (transfer)
  apply (simp add: restrict_map_def fun_eq_iff dom_def map_add_def option.case_eq_if)
   apply metis
  done

instance proof
  fix P Q R :: "'a 🍋 'b"
  show "P ## Q ==> P ⊕ Q ## R ==> P ## R"
    using pfun_compat_add by blast
  show "P ## Q ==> P ## R ==> Q ## R ==> P ⊕ Q ## R"
    by (simp add: pfun_compat_addI)
qed (simp_all add: compatible_pfun_def oplus_pfun_def,
    (transfer, auto simp add: map_add_subsumed2 map_add_comm_weak')+)

end

lemma pfun_indep_compat: "pdom(f) ∩ pdom(g) = {} ==> f ## g"
  unfolding compatible_pfun_def
  by (transfer, auto simp add: restrict_map_def fun_eq_iff)

lemma pfun_override_commute:
  "pdom(f) ∩ pdom(g) = {} ==> f ⊕ g = g ⊕ f"
  by (transfer, metis map_add_comm)

lemma pfun_override_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_override_fully: "pdom f ⊆ pdom g ==> f ⊕ g = g"
  by (transfer, auto simp add: map_add_def option.case_eq_if fun_eq_iff)

lemma pfun_override_res: "pdom g -⊲_p f ⊕ g = f ⊕ g"
  by (transfer, auto simp add: map_add_restrict[THEN sym])

lemma pfun_minus_override_commute:
  "pdom(g) ∩ pdom(h) = {} ==> (f - g) ⊕ h = (f ⊕ h) - g"
  by (transfer, simp add: map_minus_plus_commute)

lemma pfun_override_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_override:
  "pdom(f) ∩ pdom(g) = {} ==> (f ⊕ g) - g = f"
  apply (transfer)
  apply (simp add: map_add_def map_minus_def option.case_eq_if fun_eq_iff)
  apply (metis disjoint_iff domI domIff)
  done

lemma pfun_override_pos: "x ⊕ y = {}_p ==> x = {}_p"
  by (transfer, simp)

lemma pfun_le_override: "pdom x ∩ pdom y = {} ==> x ≤ x ⊕ y"
  by (transfer, auto simp add: map_le_iff_add)

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_override:
  "(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_in_ran [simp]: "x ∈ pdom f ==> f(x)_p ∈ pran f"
  by (transfer, auto)

lemma pfun_app_map [simp]: "(pfun_of_map f)(x)_p = (if (x ∈ dom(f)) then the (f x) else undefined)"
  by (transfer, simp)

lemma pfun_app_upd_1: "x = y ==> (f(x ↦ v)_p)(y)_p = v"
  by (transfer, simp)

lemma pfun_app_upd_2: "x ≠ y ==> (f(x ↦ v)_p)(y)_p = f(y)_p"
  by (transfer, simp)

lemma pfun_app_upd [simp]: "(f(x ↦ e)_p)(y)_p = (if (x = y) then e else f(y)_p)"
  by (metis pfun_app_upd_1 pfun_app_upd_2)

lemma pfun_graph_apply [simp]: "rel_apply (pfun_graph f) x = f(x)_p"
  by (transfer, auto simp add: rel_apply_def map_graph_def)

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_add_left [simp]: "x ∉ pdom(g) ==> f(x ↦ v)_p ⊕ g = (f ⊕ g)(x ↦ v)_p"
  by (transfer, safe, metis domD map_add_upd_left)

lemma pfun_app_add' [simp]: "e ∉ pdom g ==> (f ⊕ g)(e)_p = f(e)_p"
  by (transfer, auto)

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_upd_as_ovrd: "f(k ↦ v)_p = f ⊕ {k ↦ v}_p"
  by (transfer, simp)

lemma pfun_ovrd_single_upd: "x ∈ pdom(g) ==> f ⊕ ({x} ⊲_p g) = f(x ↦ g(x)_p)_p"
  by (transfer, auto simp add: map_add_def restrict_map_def fun_eq_iff)

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)

lemma pfun_eq_iff: "f = g ⟷ (pdom(f) = pdom(g) ∧ (∀ x ∈ pdom(f). f(x)_p = g(x)_p))"
  by (safe, transfer, simp add: map_eq_iff, metis domD option.sel)

lemma pfun_leI: "[ pdom f ⊆ pdom g; ∀x∈pdom f. f(x)_p = g(x)_p ] ==> f ⊆_p g"
  by (transfer, simp add: map_le_def, safe)
     (metis domD domI option.sel subsetD)

lemma pfun_le_iff: "(f ⊆_p g) = (pdom f ⊆ pdom g ∧ (∀x∈pdom f. f(x)_p = g(x)_p))"
  by (metis pfun_app_add pfun_leI pfun_override_minus psubseteq_dom_subset)

subsection ‹ Map laws ›

lemma map_pfun_empty [simp]: "map_pfun f {}_p = {}_p"
  by (transfer, simp)

lemma map_pfun'_empty [simp]: "map_pfun' f g {}_p = {}_p"
  unfolding map_pfun'_def by (transfer, simp add: comp_def)

lemma map_pfun_upd [simp]: "map_pfun f (g(x ↦ v)_p) = (map_pfun f g)(x ↦ f v)_p"
  by (simp add: map_pfun_def pfun_upd.rep_eq pfun_upd.abs_eq)

lemma map_pfun_apply [simp]: "x ∈ pdom G ==> (map_pfun F G)(x)_p = F(G(x)_p)"
  unfolding map_pfun_def by (auto simp add: pfun_app.rep_eq domD pdom.rep_eq)

lemma map_pfun_as_pabs: "map_pfun f g = (λ x ∈ pdom(g) ∙ f(g(x)_p))"
  by (simp add: pabs_def, transfer, auto simp add: fun_eq_iff restrict_map_def)

lemma map_pfun_ovrd [simp]: "map_pfun f (g ⊕ h) = (map_pfun f g) ⊕ (map_pfun f h)"
  by (simp add: map_pfun_def, transfer, simp add: map_add_def fun_eq_iff)
     (metis bind.bind_lunit comp_apply map_conv_bind_option option.case_eq_if)

lemma map_pfun_dres [simp]: "map_pfun f (A ⊲_p g) = A ⊲_p map_pfun f g"
  by (simp add: map_pfun_def, transfer, auto simp add: restrict_map_def)

subsection ‹ Domain laws ›

lemma pdom_zero [simp]: "pdom ⊥ = {}"
  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, simp add: map_minus_def, safe)
   apply (meson option.distinct(1))
  apply (metis domIff map_le_def option.simps(3))
  apply metis
  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_pdom_res [simp]: "pdom (A ⊲_p f) = A ∩ pdom(f)"
  by (transfer, auto)

lemma pdom_graph_pfun: "pdom (graph_pfun R) ⊆ Domain R"
  by (transfer, simp add: graph_map_dom fst_eq_Domain Domain_mk_functional)

lemma pdom_functional_graph_pfun [simp]: 
  "functional R ==> pdom (graph_pfun R) = Domain R"
  by (transfer, simp add: dom_map_graph mk_functional_fp)

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)

lemma pdom_map_pfun [simp]: "pdom (map_pfun F G) = pdom G"
  unfolding map_pfun_def by (safe, simp_all; metis dom_map_option_comp pdom.abs_eq pdom.rep_eq)

lemma rel_comp_pfun: "R O pfun_graph f = (λ p. (fst p, pfun_app f (snd p))) ` (R ⊳_r pdom(f))"
  by (transfer, auto simp add: rel_comp_map rel_ranres_def)                      

lemma pdom_empty_iff_dom_empty: "f = {}_p ⟷ pdom f = {}"
  by (transfer, simp)

lemma empty_map_pfunD [dest!]: "{}_p = map_pfun f F ==> F = {}_p"
  by (metis pdom_empty_iff_dom_empty pdom_map_pfun)

subsection ‹ Range laws ›

lemma pran_zero [simp]: "pran ⊥ = {}"
  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_pran_res [simp]: "pran (f ⊳_p A) = pran(f) ∩ A"
  by (transfer, auto simp add: ran_restrict_map_def)

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 (simp add: pdom.rep_eq pran_rep_eq)

lemma pran_pdom: "pran F = pfun_app F ` pdom F"
  by (transfer, force simp add: dom_def)

lemma pran_override [simp]: "pran (f ⊕ g) = pran(g) ∪ pran(pdom(g) -⊲_p f)"
  by (transfer, auto simp add: restrict_map_def dom_def map_add_def option.case_eq_if)

subsection ‹ Graph laws ›

lemma pfun_graph_inv [code_unfold]: "graph_pfun (pfun_graph f) = f"
  by (transfer, simp add: mk_functional_fp)

lemma pfun_eq_graph: "f = g ⟷ pfun_graph f = pfun_graph g"
  by (metis pfun_graph_inv)

lemma Dom_pfun_graph: "Domain (pfun_graph f) = pdom f"
  by (transfer, simp add: dom_map_graph)

lemma Range_pfun_graph: "Range (pfun_graph f) = pran f"
  by (transfer, auto simp add: ran_map_graph[THEN sym] ran_def)

lemma card_pfun_graph: "finite (pdom f) ==> card (pfun_graph f) = card (pdom f)"
  by (transfer, simp add: card_map_graph dom_map_graph finite_dom_graph)

lemma functional_pfun_graph [simp]: "functional (pfun_graph f)"
  by (transfer, simp)

lemma pfun_graph_zero: "pfun_graph ⊥ = {}"
  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, simp add: map_graph_def, safe, simp_all add: domIff)
   apply (metis option.discI)
  apply (metis ifSomeE)    
  done

lemma pfun_graph_domres: "pfun_graph (A ⊲_p f) = (A ⊲_r pfun_graph f)"
  by (transfer, simp add: rel_domres_math_def map_graph_def restrict_map_def, metis option.simps(3))

lemma pfun_graph_override: "pfun_graph (f ⊕ g) = pfun_graph f ⊕ pfun_graph g"
  by (transfer, simp add: map_add_def oplus_set_def rel_domres_def map_graph_def option.case_eq_if, safe, simp_all)
     (metis option.collapse)+

lemma pfun_graph_update: "pfun_graph (f(k ↦ v)_p) = insert (k, v) ((- {k}) ⊲_r pfun_graph f)"
  by (transfer, simp add: map_graph_update)
 
lemma pfun_graph_comp: "pfun_graph (f ∘_p g) = pfun_graph g O pfun_graph f"
  by (transfer, simp add: map_graph_comp)

lemma comp_pfun_graph: "pfun_graph f O pfun_graph g = pfun_graph (g ∘_p f)"
  by (simp add: pfun_graph_comp)

lemma pfun_graph_pfun_inv: "pfun_inj f ==> pfun_graph (pfun_inv f) = (pfun_graph f)^-1"
  by (transfer, simp add: map_graph_map_inv)

lemma pfun_graph_pabs: "pfun_graph (λ x ∈ A | P x ∙ f x) = {(k, v). k ∈ A ∧ P k ∧ v = f k}"
  unfolding pabs_def by (transfer, auto simp add: map_graph_def restrict_map_def)

lemma pfun_graph_le_iff:
  "pfun_graph f ⊆ pfun_graph g ⟷ f ⊆_p g"
  by (simp add: inf.order_iff pfun_eq_graph pfun_graph_inter)

lemma pfun_member_iff [simp]: "(k, v) ∈ pfun_graph f ⟷ (k ∈ pdom(f) ∧ pfun_app f k = v)"
  by (transfer, auto simp add: map_graph_def)

lemma pfun_graph_rres: "pfun_graph (f ⊳_p A) = pfun_graph f ⊳_r A"
  by (transfer, auto simp add: map_graph_def rel_ranres_def ran_restrict_map_def)

subsection ‹ Graph Transfer Setup ›

definition cr_pfung :: "('a ↔ 'b) ==> 'a 🍋 'b ==> bool" where
"cr_pfung f g = (f = pfun_graph g)"

lemma Domainp_cr_pfung [transfer_domain_rule]: "Domainp cr_pfung = functional"
  unfolding cr_pfung_def Domainp_iff[abs_def]
  by (auto simp add: fun_eq_iff, metis graph_map_inv pfun_graph.abs_eq)

bundle pfun_graph_lifting
begin

unbundle lifting_syntax

lemma bi_unique_cr_pfung [transfer_rule]: "bi_unique cr_pfung"
  unfolding cr_pfung_def bi_unique_def by (auto simp add: pfun_eq_graph)

lemma right_total_cr_pfung [transfer_rule]: "right_total cr_pfung"
  unfolding cr_pfung_def right_total_def by simp

lemma cr_pfung_empty [transfer_rule]: "cr_pfung {} {}_p"
  unfolding cr_pfung_def by (simp add: pfun_graph_zero)

lemma cr_pfung_dom [transfer_rule]: "(cr_pfung ===> (=)) Domain pdom"
  unfolding rel_fun_def cr_pfung_def by (simp add: Dom_pfun_graph)

lemma cr_pfung_ran [transfer_rule]: "(cr_pfung ===> (=)) Range pran"
  unfolding rel_fun_def cr_pfung_def by (simp add: Range_pfun_graph)

lemma cr_pfung_id [transfer_rule]: "((=) ===> cr_pfung) Id_on pId_on"
  unfolding rel_fun_def cr_pfung_def by (simp add: pfun_graph_pId_on)

lemma cr_pfung_ovrd [transfer_rule]: "(cr_pfung ===> cr_pfung ===> cr_pfung) (⊕) (⊕)"
  unfolding rel_fun_def cr_pfung_def by (simp add: pfun_graph_override)

lemma cr_pfung_ovrd [transfer_rule]: "(cr_pfung ===> cr_pfung ===> cr_pfung) (O) (λ x y. y ∘_p x)"
  unfolding rel_fun_def cr_pfung_def by (simp add: pfun_graph_comp) 

lemma cr_pfung_dres [transfer_rule]: "((=) ===> cr_pfung ===> cr_pfung) (⊲_r) (⊲_p)"
  unfolding rel_fun_def cr_pfung_def by (simp add: pfun_graph_domres)

lemma cr_pfung_rres [transfer_rule]: "(cr_pfung ===> (=) ===> cr_pfung) (⊳_r) (⊳_p)"
  unfolding rel_fun_def cr_pfung_def by (simp add: pfun_graph_rres)

lemma cr_pfung_le [transfer_rule]: "(cr_pfung ===> cr_pfung ===> (=)) (≤) (≤)"
  unfolding rel_fun_def cr_pfung_def by (simp add: pfun_graph_le_iff)

lemma cr_pfung_update [transfer_rule]: "(cr_pfung ===> (=) ===> (=) ===> cr_pfung) (λ f k v. insert (k, v) ((- {k}) ⊲_r f)) pfun_upd"
  unfolding rel_fun_def cr_pfung_def by (simp add: pfun_graph_update)

end

subsection ‹ Partial Injections ›

lemma pfun_inj_empty [simp]: "pfun_inj {}_p"
  by (transfer, simp)

lemma pinj_pId_on [simp]: "pfun_inj (pId_on A)"
  by (transfer, auto simp add: inj_on_def)

lemma pfun_inj_inv_inv: "pfun_inj f ==> pfun_inv (pfun_inv f) = f"
  by (transfer, simp)

lemma pfun_inj_inv: "pfun_inj f ==> pfun_inj (pfun_inv f)"
  by (transfer, simp add: inj_map_inv)

lemma f_pfun_inv_f_apply: "[ pfun_inj f; x ∈ pran f ] ==> f(pfun_inv f(x)_p)_p = x"
  by (transfer, auto simp add: ranI)

lemma pfun_inv_f_f_apply: "[ pfun_inj f; x ∈ pdom f ] ==> pfun_inv f(f(x)_p)_p = x"
  by (transfer, auto simp add: ranI)

lemma pfun_inj_upd: "[ pfun_inj f; v ∉ pran f ] ==> pfun_inj (f(k ↦ v)_p)"
  apply (transfer, simp_all, safe)
  apply (meson f_the_inv_into_f inj_on_fun_updI)
  apply fastforce
  done

lemma pfun_inj_dres: "pfun_inj f ==> pfun_inj (A ⊲_p f)"
  by (transfer, auto simp add: inj_on_def)

lemma pfun_inj_rres: "pfun_inj f ==> pfun_inj (f ⊳_p A)"
  by (transfer, metis dom_map_inv inj_map_inv map_inv_dom_res map_inv_map_inv map_inv_ran_res ran_ran_restrict restrict_map_inj_on)

lemma pfun_inj_comp: "[ pfun_inj f; pfun_inj g ] ==> pfun_inj (f ∘_p g)"
  by (transfer, auto simp add: inj_on_def map_comp_def option.case_eq_if dom_def)

lemma pfun_inj_ovrd: "[ pfun_inj f; pfun_inj g; pran f ∩ pran g = {} ] ==> pfun_inj (f ⊕ g)"
  by (transfer, force simp add: inj_on_def map_add_def option.case_eq_if dom_def)

lemma pfun_inv_dres: "pfun_inj f ==> pfun_inv (A ⊲_p f) = (pfun_inv f) ⊳_p A"
  by (transfer, simp add: map_inv_dom_res)

lemma pfun_inv_rres: "pfun_inj f ==> pfun_inv (f ⊳_p A) = A ⊲_p (pfun_inv f)"
  by (transfer, simp add: map_inv_ran_res)

lemma pfun_inv_empty [simp]: "pfun_inv {}_p = {}_p"
  by (transfer, simp)

lemma pdom_pfun_inv [simp]: "pdom (pfun_inv f) = pran f"
  by (simp add: pran_rep_eq, transfer, simp)

lemma pfun_inv_add:
  assumes "pfun_inj f" "pfun_inj g" "pran f ∩ pran g = {}"
  shows "pfun_inv (f ⊕ g) = (pfun_inv f ⊳_p (- pdom g)) ⊕ pfun_inv g"
  using assms by (simp add: pran_rep_eq, transfer, safe, meson map_inv_add)

lemma pfun_inv_upd:
  assumes "pfun_inj f" "v ∉ pran f"
  shows "pfun_inv (f(k ↦ v)_p) = (pfun_inv ((- {k}) ⊲_p f))(v ↦ k)_p"
  using assms by (simp add: pran_rep_eq, transfer, meson map_inv_upd)

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)

lemma pdom_res_frame_update [simp]: 
  "[ x ∈ pdom(f); (-{x}) ⊲_p f = (-{x}) ⊲_p g ] ==> g(x ↦ f(x)_p)_p = f"
  by transfer (metis (mono_tags, opaque_lifting) domIff fun_upd_triv fun_upd_upd option.exhaust_sel
      restrict_complement_singleton_eq)

lemma pdres_rres_commute: "A ⊲_p (P ⊳_p B) = (A ⊲_p P) ⊳_p B"
  by (transfer, simp add: map_dres_rres_commute)

lemma pdom_nres_disjoint: "pdom(f) ∩ A = {} ==> (- A) ⊲_p f = f"
  by (metis disjoint_eq_subset_Compl inf.absorb2 pdom_res_pdom pdom_res_twice)

lemma pranres_pdom [simp]: "pdom (f ⊳_p A) ⊲_p f = f ⊳_p A"
  by (transfer, simp add: restrict_map_def fun_eq_iff ran_restrict_map_def option.case_eq_if)
     (metis (full_types, lifting) bind.bind_lunit bind.bind_lzero domIff not_None_eq)
  
lemma pdom_pranres [simp]: "pdom (f ⊳_p A) ⊆ pdom f"
  by (metis inf.absorb_iff1 inf.commute pdom_pdom_res pdom_res_pdom pdom_res_swap)

lemma pfun_split_domain: "A ⊲_p f ⊕ (- A) ⊲_p f = f"
  by (transfer, auto simp add: restrict_map_def map_add_def fun_eq_iff option.case_eq_if)

subsection ‹ Range restriction laws ›

lemma pran_res_UNIV [simp]: "f ⊳_p UNIV = f"
  by (transfer, simp add: ran_restrict_map_def)

lemma pran_res_empty [simp]: "f ⊳_p {} = {}_p"
  by (transfer, auto simp add: ran_restrict_map_def)

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_twice [simp]: "f ⊳_p A ⊳_p B = f ⊳_p (A ∩ B)"
  by (transfer, simp)

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)"
  by (transfer, auto simp add: map_add_def ran_restrict_map_def map_le_def option.case_eq_if)

lemma pcomp_ranres [simp]: "(f ∘_p g) ⊳_p A = (f ⊳_p A) ∘_p g"
  by (simp add: pfun_comp_assoc pran_res_alt_def)

lemma pranres_le: "A ⊆ B ==> f ⊳_p A ≤ f ⊳_p B"
  by (simp add: pfun_graph_le_iff[THEN sym] pfun_graph_comp pfun_graph_rres relcomp_mono rel_ranres_le)

lemma pranres_neg_ran [simp]: "P ⊳_p- pran P = {}_p"
  by (transfer, simp add: ran_restrict_map_def fun_eq_iff option.case_eq_if bind_eq_None_conv, meson option.exhaust_sel)

subsection ‹ Preimage Laws ›

lemma ppreimageI [intro!]: "[ x ∈ pdom(f); f(x)_p ∈ A ] ==> x ∈ pdom (f ⊳_p A)"
  by (metis (full_types) insertI1 pdom_upd pfun_upd_ext pran_res_upd_1)

lemma ppreimageD: "x ∈ pdom (f ⊳_p A) ==> ∃ y ∈ A. f(x)_p = y"
  by (transfer, auto simp add: ran_restrict_map_def)

lemma ppreimageE [elim!]: "[ x ∈ pdom (f ⊳_p A); ∧ y. [ x ∈ pdom(f); y ∈ A; f(x)_p = y ] ==> P ] ==> P"
  by (metis (no_types) pdom_pranres ppreimageD subsetD)

lemma mem_pimage_iff: "x ∈ pran (A ⊲_p f) ⟷ (∃ y ∈ A ∩ pdom(f). f(y)_p = x)"
  by (auto simp add: pran_pdom)

lemma ppreimage_inter [simp]: "pdom (f ⊳_p (A ∩ B)) = pdom (f ⊳_p A) ∩ pdom (f ⊳_p B)"
  by fastforce

subsection ‹ Composition ›

lemma pcomp_apply [simp]: "[ x ∈ pdom(g) ] ==> (f ∘_p g)(x)_p = f(g(x)_p)_p"
  by (transfer, auto)

lemma pcomp_mono: "[ f ≤ f'; g ≤ g' ] ==> f ∘_p g ≤ f' ∘_p g'"
  by (simp add: pfun_graph_le_iff[THEN sym] pfun_graph_comp relcomp_mono)

lemma pdom_UNIV_comp: "pdom f = UNIV ==> pdom (f ∘_p g) = pdom g"
  by simp

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

lemma pdom_pfun_entries [simp]: "pdom (pfun_entries A f) = A"
  by (transfer, auto)

lemma pran_pfun_entries [simp]: "pran (pfun_entries A f) = f ` A"
  by (transfer, simp add: ran_def, auto)

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)

lemma pdom_res_entries: "A ⊲_p pfun_entries B f = pfun_entries (A ∩ B) f"
  by (transfer, auto simp add: fun_eq_iff restrict_map_def)

lemma pfuse_empty [simp]: "pfuse {}_p g = {}_p"
  by (simp add: pfuse_def)

lemma pfuse_app [simp]:
  "[ e ∈ pdom F; e ∈ pdom G ] ==> (pfuse F G)(e)_p = (F(e)_p, G(e)_p)"
  by (metis (no_types, lifting) IntI pfun_entries_apply_1 pfuse_def)

lemma pdom_pfuse [simp]: "pdom (pfuse f g) = pdom(f) ∩ pdom(g)"
  by (auto simp add: pfuse_def)

lemma pfuse_upd: 
  "pfuse (f(k ↦ v)_p) g =
   (if k ∈ pdom g then (pfuse ((-{k}) ⊲_p f) g)(k ↦ (v, pfun_app g k))_p else pfuse f g)"
  by (simp add: pfuse_def, transfer, auto simp add: fun_eq_iff)

subsection ‹ Lambda abstraction ›

lemma pabs_cong:
  assumes "A = B" "∧ x. x ∈ A ==> P(x) = Q(x)" "∧ x. [ x ∈ A; P x ] ==> F(x) = G(x)"
  shows "(λ x ∈ A | P x ∙ F(x)) = (λ x ∈ B | Q x ∙ G(x))"
  using assms unfolding pabs_def
  by (transfer, auto simp add: restrict_map_def fun_eq_iff)

lemma pabs_apply [simp]: "[ y ∈ A; P y ] ==> (λ x ∈ A | P x ∙ f x) (y)_p = f y"
  by (simp add: pabs_def)

lemma pdom_pabs [simp]: "pdom (λ x ∈ A | P x ∙ f x) = A ∩ Collect P"
  by (simp add: pabs_def)

lemma pran_pabs [simp]: "pran (λ x ∈ A | P x ∙ f x) = {f x | x. x ∈ A ∧ P x}"
  unfolding pabs_def 
  by (transfer, auto simp add: ran_def restrict_map_def)

lemma pabs_eta [simp]: "(λ x ∈ pdom(f) ∙ f(x)_p) = f"
  by (simp add: pabs_def, transfer, auto simp add: fun_eq_iff domIff restrict_map_def)

lemma pabs_id [simp]: "(λ x ∈ A | P x ∙ x) = pId_on {x∈A. P x}"
  unfolding pabs_def by (transfer, simp add: restrict_map_def)

lemma pfun_entries_pabs: "pfun_entries A f = (λ x ∈ A ∙ f x)"
  by (simp add: pabs_def, transfer, auto)

lemma pabs_empty [simp]: "(λ x∈{} ∙ f(x)) = {}_p"
  by (simp add: pabs_def)

lemma pabs_insert_maplet: "(λ x∈insert y A ∙ f(x)) = (λ x∈A ∙ f(x)) ⊕ {y ↦ f(y)}_p"
  by (simp add: pabs_def, transfer, auto simp add: restrict_map_insert)

text ‹ This rule can perhaps be simplified ›

lemma pcomp_pabs: 
  "(λ x ∈ A | P x ∙ f x) ∘_p (λ x ∈ B | Q x ∙ g x)
    = (λ x ∈ pdom (pabs B Q g ⊳_p (A ∩ Collect P)) ∙ (f (g x)))"
proof -
  have "pabs A P f ∘_p pabs B Q g = (λ x ∈ pdom (pabs A P f ∘_p pabs B Q g) ∙ (pfun_app (pabs A P f ∘_p pabs B Q g)) x)"
    by (rule pabs_eta[THEN sym, of "(λ x ∈ A | P x ∙ f x) ∘_p (λ x ∈ B | Q x ∙ g x)"]) 
  also have "... = (λ x ∈ pdom (pabs B Q g ⊳_p (A ∩ Collect P)) ∙ (f (g x)))"
    unfolding pabs_def
    by (transfer, auto simp add: restrict_map_def map_comp_def ran_restrict_map_def fun_eq_iff)
  finally show ?thesis .
qed

lemma pabs_rres [simp]: "pabs A P f ⊳_p B = pabs A (λ x. P x ∧ f x ∈ B) f"
  by (simp add: pabs_def, transfer, auto simp add: ran_restrict_map_def restrict_map_def)

(* This law should be generalised *)

lemma pabs_simple_comp [simp]: "(λ x ∙ f x) ∘_p g(k ↦ v)_p = ((λ x ∙ f x) ∘_p g)(k ↦ f v)_p"
  by (simp add: pabs_def, transfer, auto)

lemma pabs_comp: "(λ x ∈ A ∙ f x) ∘_p g = (λ x ∈ pdom (g ⊳_p A) ∙ f (pfun_app g x))"
  by (metis pabs_eta pcomp_pabs pdom_pId_on pdom_pabs)

lemma map_pfun_pabs [simp]: "map_pfun f (λ x∈A | B(x) ∙ g(x)) = (λ x∈A | B(x) ∙ f(g(x)))"
  by (simp add: pfun_eq_iff) 

subsection ‹ Singleton Partial Functions ›

definition pfun_singleton :: "('a 🍋 'b) ==> bool" where
"pfun_singleton f = (∃ k v. f = {k ↦ v}_p)" 

lemma pfun_singleton_dom: "pfun_singleton f ⟷ (∃ k. pdom(f) = {k})"
  by (simp add: pfun_singleton_def, safe, simp_all)
     (metis insertI1 override_lzero pdom_res_pdom pfun_ovrd_single_upd)

lemma pfun_singleton_maplet [simp]:
  "pfun_singleton {k ↦ v}_p"
  by (auto simp add: pfun_singleton_def)

definition dest_pfsingle :: "('a 🍋 'b) ==> 'a × 'b" where
"dest_pfsingle f = (THE (k, v). f = {k ↦ v}_p)"

lemma dest_pfsingle_maplet [simp]: "dest_pfsingle {k ↦ v}_p = (k, v)"
  unfolding dest_pfsingle_def
  by (rule the_equality, simp_all add: prod.case_eq_if)
     (metis fst_eqD pdom_res_zero pdom_upd pdom_zero pran_upd pran_zero prod.expand singleton_insert_inj_eq sndI)

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"
proof -
  from assms(2) have "(∑x∈pdom m. if k = x then v else m(x)_p) = sum (pfun_app m) (pdom m)"
    by (auto intro!: sum.cong)
  thus ?thesis
    by (simp_all add: pfun_sum_def assms add.commute cong: sum.cong)
qed

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)
  have 2: "sum (pfun_app f) (pdom f) - sum (pfun_app f) (pdom f - A) =
    sum (pfun_app f) (pdom f) - sum (pfun_app f) (- A ∩ pdom f)"
    by (auto simp add: sum_diff Int_commute boolean_algebra_class.diff_eq assms)
  show ?thesis
    by (simp add: pfun_sum_def 1 2 sum_diff assms)
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)"
  using assms
  by (subst pfun_sum_pdom_res, simp_all add: assms)

subsection ‹ Conversions ›

definition list_pfun :: "'a list ==> nat 🍋 'a" where
"list_pfun xs = (λ i | 0 < i ∧ i ≤ length xs ∙ xs ! (i-1))"

lemma pdom_list_pfun [simp]: "pdom (list_pfun xs) = {1..length xs}"
  by (auto simp add: list_pfun_def)

lemma pran_list_pfun [simp]: "pran (list_pfun xs) = set xs"
  by (simp add: list_pfun_def, safe, simp_all)
     (metis One_nat_def Suc_leI diff_Suc_1 in_set_conv_nth zero_less_Suc)

lemma pfun_app_list_pfun: "[ 0 < i; i ≤ length xs ] ==> (list_pfun xs)(i)_p = xs ! (i - 1)"
  by (simp add: list_pfun_def)

lemma pfun_graph_list_pfun: "pfun_graph (list_pfun xs) = (λ i. (i, xs ! (i - 1))) ` {1..length xs}"
  by (simp add: list_pfun_def pfun_graph_pabs, auto)

lemma range_list_pfun:
  "range list_pfun = {f :: nat 🍋 'a. ∃ i. pdom(f) = {1..i}}"
proof (rule set_eqI, rule iffI)
  fix f :: "nat 🍋 'a"
  assume "f ∈ range list_pfun"
  thus "f ∈ {f. ∃i. pdom f = {1..i}}"
    by auto
next
  fix f :: "nat 🍋 'a"
  assume "f ∈ {f. ∃i. pdom f = {1..i}}"
  thus "f ∈ range list_pfun"
  proof (unfold list_pfun_def pabs_def image_def, transfer)
    fix f :: "nat ==> 'a option"
    assume "f ∈ {f. ∃i. dom f = {1..i}}"
    then obtain i where i:"dom f = {1..i}"
      by blast
    hence 1: "∧x. dom f = {Suc 0..i} ==> 0 < x ==> x ≤ i ==> f x = Some (the (f x))"
      by (metis Suc_leI atLeastAtMost_iff domIff option.exhaust_sel)
    with i have 2:"f 0 = None"
      using atLeastAtMost_iff not_one_le_zero by blast
    from i 1 2 have f: "f = (λxa. Some (map (the ∘ f ∘ nat) [1..int i] ! (xa - Suc 0))) |` {ia. 0 < ia ∧ ia ≤ length (map (the ∘ f ∘ nat) [1..int i])}"
      by (auto simp add: fun_eq_iff restrict_map_def)
    have 3: "(λxa. Some (map (the ∘ f ∘ nat) [1..int i] ! (xa - Suc 0))) |` {ia. 0 < ia ∧ ia ≤ length (map (the ∘ f ∘ nat) [1..int i])} ∈ {y. ∃x∈UNIV. y = (λxa. if xa ∈ UNIV then Some (x ! (xa - 1)) else None) |` (UNIV ∩ {i. 0 < i ∧ i ≤ length x})}"
      by (auto simp add: fun_eq_iff restrict_map_def)
    show "f ∈ {y. ∃x∈UNIV. y = (λxa. if xa ∈ UNIV then Some (x ! (xa - 1)) else None) |` (UNIV ∩ {i. 0 < i ∧ i ≤ length x})}"
      using "3" f by auto
  qed
qed

lemma list_pfun_le_iff_prefix [simp]: "list_pfun xs ≤ list_pfun ys ⟷ xs ≤ ys"
  apply (simp add: pfun_le_iff, safe, simp_all add: pfun_app_list_pfun list_le_prefix_iff)
  apply (metis Suc_leI Suc_le_mono atLeastAtMost_iff diff_Suc_Suc le0 minus_nat.diff_0)
  apply (metis Suc_le_D Suc_le_eq diff_Suc_Suc diff_zero)
  done

lemma pfun_upd_le_iff: "(f(k ↦ v)_p ⊆_p g) = (k ∈ pdom g ∧ g(k)_p = v ∧ (- {k}) ⊲_p f ⊆_p g)"
  by (auto simp add: pfun_le_iff)

lemma pfun_upd_le_pfun_upd: "(f(k ↦ v)_p ⊆_p g(k ↦ v)_p) = ((- {k}) ⊲_p f ⊆_p (- {k}) ⊲_p g)"
  by (auto simp add: pfun_le_iff)

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: "S _i = {f. i ∈ pdom(f)}"
  by (simp add: lens_defs lens_source_def, transfer, force)

lemma lens_override_pfun_lens:
  "x ∈ pdom(g) ==> f ⊕_L g on pfun_lens x = f ⊕ ({x} ⊲_p g)"
  by (simp add: lens_defs pfun_ovrd_single_upd)

subsection ‹ Prism Functions ›

text ‹ We can use prisms to index a type and construct partial functions. ›

definition prism_fun :: "('a ==>_\<triangle> 'e) ==> 'a set ==> ('a ==> bool × 'b) ==> ('e 🍋 'b)"
  where [code_unfold]: "prism_fun c A PB = (λ x∈build ` A | fst (PB (the (match x))) ∙ snd (PB (the (match x))))"

definition prism_fun_upd :: "('e 🍋 'b) ==> ('a ==>_\<triangle> 'e) ==> 'a set ==> ('a ==> bool × 'b) ==> ('e 🍋 'b)"
  where [code_unfold]: "prism_fun_upd F c A PB = F ⊕ prism_fun c A PB"

nonterminal prism_maplet and prism_maplets

syntax
  "_prism_maplet"        :: "id ==> pttrn ==> logic ==> logic ==> logic ==> prism_maplet" ("_{_ ∈ _./ _} ==> _")
  "_prism_maplet_mem"    :: "id ==> pttrn ==> logic ==> logic ==> prism_maplet" ("_{_ ∈ _} ==> _")
  "_prism_maplet_simple" :: "id ==> pttrn ==> logic ==> prism_maplet" ("_ _ ==> _")
  ""                     :: "prism_maplet ==> prism_maplets"             ("_")
  "_prism_Maplets"       :: "[prism_maplet, prism_maplets] ==> prism_maplets" ("_ |/ _")
  "_prism_fun_upd"       :: "logic ==> prism_maplets ==> logic" ("_'(_')" [900, 0] 900)
  "_prism_fun"           :: "prism_maplets ==> logic" ("{_}_p")

translations
  "f(c{v ∈ A. P} ==> B)" == "CONST prism_fun_upd f c A (λ v. (P, B))"
  "f(c{v ∈ A} ==> B)" == "f(c{v ∈ A. CONST True} ==> B)"
  "f(c v ==> B)" == "f(c{v ∈ CONST UNIV} ==> B)"
  "_prism_fun_upd m (_prism_Maplets xy ms)"  ⇌ "_prism_fun_upd (_prism_fun_upd m xy) ms"
  "_prism_fun ms"                            ⇌ "_prism_fun_upd {}_p ms"
  "_prism_fun (_prism_Maplets ms1 ms2)"     ↽ "_prism_fun_upd (_prism_fun ms1) ms2"
  "_prism_Maplets ms1 (_prism_Maplets ms2 ms3)" ↽ "_prism_Maplets (_prism_Maplets ms1 ms2) ms3"

lemma dom_prism_fun: "wb_prism c ==> pdom(prism_fun c A PB) = {build v | v. v ∈ A ∧ fst (PB v)}"
  by (simp add: prism_fun_def, auto)

lemma prism_fun_compat: "c ∇ d ==> prism_fun c A PB ## prism_fun d B QB"
  by (auto intro!: pfun_indep_compat simp add: prism_fun_def prism_diff_build)

lemma prism_fun_commute: "c ∇ d ==> prism_fun c A PB ⊕ prism_fun d B QB = prism_fun d B QB ⊕ prism_fun c A PB"
  by (meson override_comm prism_fun_compat)

lemma prism_fun_apply: "[ wb_prism c; v ∈ A; fst (PB v) ] ==> (prism_fun c A PB)(build v)_p = snd (PB v)"
  by (simp add: prism_fun_def)

lemma prism_fun_update_app_1 [simp]: "[ wb_prism c; v ∈ A; P v ] ==> (f(c{x ∈ A. P(x)} ==> B(x)))(build v)_p = B v"
  by (simp add: prism_fun_def prism_fun_upd_def)

lemma prism_fun_update_app_2 [simp]: "[ wb_prism c; wb_prism d; d ∇ c ] ==> (f(c{x ∈ A. P(x)} ==> B(x)))(build v)_p = f(build v)_p"
  by (simp add: prism_fun_def prism_fun_upd_def image_iff prism_diff_build)

lemma prism_fun_update_cancel [simp]: "f(c{x ∈ A. P(x)} ==> g(x) | c{x ∈ A. P(x)} ==> h(x)) = f(c{x ∈ A. P(x)} ==> h(x))"
  by (simp add: prism_fun_def prism_fun_upd_def override_assoc[THEN sym] pfun_override_fully)

lemma prism_fun_update_commute: 
  "c ∇ d ==> f(c{x ∈ A. P(x)} ==> g(x) | d{y ∈ B. Q(y)} ==> h(y))
            = f(d{y ∈ B. Q(y)} ==> h(y) | c{x ∈ A. P(x)} ==> g(x))"
  by (simp add: prism_fun_upd_def override_assoc[THEN sym] prism_fun_commute)

lemma case_sum_Plus: "case_sum f g ` (A <+> B) = (f`A) ∪ (g`B)"
  by (simp add: image_iff Plus_def, metis (no_types, lifting) image_Un image_cong image_image sum.case(1) sum.case(2))

lemma build_in_dom_prism_fun: "[ wb_prism c; x ∈ A; fst (PB x) ] ==> build x ∈ pdom (prism_fun c A PB)"
  by (auto simp add: dom_prism_fun)
  
lemma prism_fun_combine:
  assumes "wb_prism c" "wb_prism d" "c ∇ d"
  shows "prism_fun c A PB ⊕ prism_fun d B QB = prism_fun (c +_\<triangle> d) (A <+> B) (case_sum PB QB)"
  using assms
  apply (simp add: pfun_eq_iff dom_prism_fun sum.case_eq_if prism_diff_build build_in_dom_prism_fun)
  apply safe
           apply (simp_all add: add: build_in_dom_prism_fun prism_diff_build prism_fun_apply)
      apply (metis InlI build_plus_Inl sum.disc(1) sum.sel(1))
     apply (metis InrI build_plus_Inr sum.disc(2) sum.sel(2))
    apply metis
   apply (metis InlI build_in_dom_prism_fun build_plus_Inl old.sum.simps(5) pfun_app_add prism_fun_apply prism_fun_commute
      prism_plus_wb)
  apply (metis InrI build_plus_Inr old.sum.simps(6) prism_fun_apply prism_plus_wb)
  done

lemma prism_diff_implies_indep_funs:
  "[ wb_prism c; wb_prism d; c ∇ d ] ==> pdom(prism_fun c A Pσ) ∩ pdom(prism_fun d B Qρ) = {}"
  by (auto simp add: dom_prism_fun prism_diff_build)

lemma prism_fun_cong: "[ c = d; A = B; PB = QB ] ==> prism_fun c A PB = prism_fun d B QB"
  by blast

lemma prism_fun_cong2: 
  assumes 
    "wb_prism c₁" "wb_prism c₂" 
    "c₁ = c₂" "A₁ = A₂" 
    "∧ i. i ∈ A₁ ==> P₁ i ⟷ P₂ i" 
    "∧ i. [ i ∈ A₁; P₁ i ] ==> B₁ i = B₂ i"
  shows "prism_fun c₁ A₁ (λ x. (P₁ x, B₁ x)) = prism_fun c₂ A₂ (λ y. (P₂ y, B₂ y))"
  using assms
  by (auto intro!: pabs_cong simp add: prism_fun_def)

lemma map_pfun_prism_fun [simp]: "map_pfun f (prism_fun a A (λ x. (B x, C x))) = prism_fun a A (λ x. (B x, f (C x)))"
  by (simp add: prism_fun_def)

lemma prism_fun_as_map:
  "wb_prism b ==>
   prism_fun b A PB = pfun_of_map (λ x. case match x of None ==> None | Some x ==> if x ∈ A ∧ fst (PB x) then Some (snd (PB x)) else None)"
  by (simp add: prism_fun_def pfun_eq_iff domIff pdom.abs_eq option.case_eq_if, safe, simp_all)
     (metis (no_types, lifting) image_iff option.collapse option.distinct(1) wb_prism.build_match, metis option.discI)

subsection ‹ Code Generator ›

subsubsection ‹ Associative Lists ›

lemma relt_pfun_iff: 
  "relt_pfun R f g ⟷ (pdom(f) = pdom(g) ∧ (∀ x∈pdom(f). R (f(x)_p) (g(x)_p)))"
  by (transfer, auto simp add: rel_map_iff)

lift_definition pfun_of_alist :: "('a × 'b) list ==> 'a 🍋 'b" is map_of .

lemma pfun_of_alist_clearjunk: "pfun_of_alist xs = pfun_of_alist (AList.clearjunk xs)"
  by (transfer, simp add: map_of_clearjunk)

lemma pfun_of_alist_Nil [simp]: "pfun_of_alist [] = {}_p"
  by (transfer, simp)

lemma pfun_of_alist_Cons [simp]: "pfun_of_alist (p # ps) = pfun_of_alist ps(fst p ↦ snd p)_p"
  by (transfer, metis (full_types) map_of.simps(2))

lemma dom_pfun_alist [simp, code]: "pdom (pfun_of_alist xs) = set (map fst xs)"
  by (transfer, simp add: dom_map_of_conv_image_fst)

lemma ran_pfun_alist [simp, code]: "pran (pfun_of_alist xs) = set (remdups (map snd (AList.clearjunk xs)))"
  apply (transfer, safe, simp_all)
   apply (safe, simp_all)
   apply (metis ranI ran_map_of)
  apply (metis distinct_clearjunk map_of_clearjunk map_of_eq_Some_iff)
  done

lemma map_graph_map_of: "map_graph (map_of xs) = set (AList.clearjunk xs)"
  by (metis graph_def graph_map_of map_graph_def)

lemma pfun_graph_alist [code]: "pfun_graph (pfun_of_alist xs) = set (AList.clearjunk xs)"
  by (transfer, meson map_graph_map_of)

lemma empty_pfun_alist [code]: "{}_p = pfun_of_alist []"
  by (transfer, simp)

lemma update_pfun_alist [code]: "pfun_upd (pfun_of_alist xs) k v = pfun_of_alist (AList.update k v xs)"
  by transfer (simp add: update_conv')

lemma apply_pfun_alist [code]: 
  "pfun_app (pfun_of_alist xs) k = (if k ∈ set (map fst xs) then the (map_of xs k) else undefined)"
  apply (transfer, simp, safe)
  apply (metis map_of_eq_None_iff option.distinct(1))
  apply (metis eq_fst_iff weak_map_of_SomeI)
  done

lemma map_of_Cons_code [code]:
  "pfun_lookup (pfun_of_alist []) k = None"
  "pfun_lookup (pfun_of_alist ((l, v) # ps)) k = (if l = k then Some v else map_of ps k)"
  by (transfer, simp)+

lemma map_pfun_alist [code]: 
  "map_pfun f (pfun_of_alist m) = pfun_of_alist (map (λ (k, v). (k, f v)) m)"
  by (transfer, simp add: map_of_map)

lemma map_pfun_of_map [code]: "map_pfun f (pfun_of_map g) = pfun_of_map (λ x. map_option f (g x))"
  by (auto simp add: map_pfun_def pfun_of_map_inject fun_eq_iff)

lemma pdom_res_alist [code]:
  "A ⊲_p (pfun_of_alist m) = pfun_of_alist (AList.restrict A m)"
  by (transfer, simp add: restr_conv')

lemma pran_res_alist_distinct: 
  "distinct (map fst xs) ==> pfun_of_alist xs ⊳_p A = pfun_of_alist (filter (λ(k, v). v ∈ A) xs)"
  by (induct xs, auto)

lemma pran_res_alist [code]: "pfun_of_alist xs ⊳_p A = pfun_of_alist (filter (λ(k, v). v ∈ A) (AList.clearjunk xs))"
  by (metis distinct_clearjunk pfun_of_alist_clearjunk pran_res_alist_distinct)

lemma pdom_res_set_map [code]:
  "set xs ⊲_p (pfun_of_map m) = pfun_of_alist (map (λ x. (x, the (m x))) (filter (λ x. m x ≠ None) xs))"
proof (induct xs)
  case Nil
  then show ?case by auto
next
  case (Cons a xs)
  then show ?case 
      by (simp, safe; transfer)
         (simp add: restrict_map_insert, metis Int_insert_right_if0 Map.restrict_restrict domIff map_restrict_dom)
qed

lemma plus_pfun_alist [code]: "pfun_of_alist f ⊕ pfun_of_alist g = pfun_of_alist (g @ f)"
  by (transfer, simp)

lemma pfun_entries_alist [code]: "pfun_entries (set ks) f = pfun_of_alist (map (λ k. (k, f k)) ks)"
  by (auto simp add: pfun_eq_iff apply_pfun_alist map_of_map prod.case_eq_if image_iff map_of_map_restrict)

lemma pdom_res_entries_alist [code]:
  "A ⊲_p pfun_entries (set bs) f =
    pfun_of_alist (map (λ k. (k, f k)) (filter (λx. x ∈ A) bs))"
  by (metis inter_set_filter pdom_res_entries pfun_entries_alist)

lemma pfun_alist_oplus_map [code]: 
  "pfun_of_alist xs ⊕ pfun_of_map f = pfun_of_map (λ k. case f k of None ==> map_of xs k | Some v ==> Some v)"
  by (simp add: map_add_def oplus_pfun.abs_eq pfun_of_alist.abs_eq)

lemma pfun_map_oplus_alist [code]: 
  "pfun_of_map f ⊕ pfun_of_alist xs = pfun_of_map (λ k. if k ∈ set (map fst xs) then map_of xs k else f k)"
  by (simp add: map_add_def oplus_pfun.abs_eq pfun_of_alist.abs_eq)
     (metis map_of_eq_None_iff option.case_eq_if option.exhaust option.sel)

lemma pfun_singleton_alist [code]: "pfun_singleton (pfun_of_alist [(k, v)]) = True"
  by simp

lemma dest_pfsingle_alist [code]: "dest_pfsingle (pfun_of_alist [(k, v)]) = (k, v)"
  by simp

text ‹ Adapted from Mapping theory ›

lemma ptabulate_alist [code]: "ptabulate ks f = pfun_of_alist (map (λk. (k, f k)) ks)"
  by transfer (simp add: map_of_map_restrict)

lemma pcombine_alist [code]:
  "pcombine f (pfun_of_alist xs) (pfun_of_alist ys) =
     ptabulate (remdups (map fst xs @ map fst ys))
       (λx. the (combine_options f (map_of xs x) (map_of ys x)))"
  apply transfer
  apply (rule ext)
  apply (rule sym)
  subgoal for f xs ys x
    apply (cases "map_of xs x"; cases "map_of ys x"; simp)
       apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
        dest: map_of_SomeD split: option.splits)+
    done
  done

lemma pfun_comp_alist [code]: "pfun_of_alist ys ∘_p pfun_of_alist xs = pfun_of_alist (AList.compose xs ys)"
  by (transfer, simp add: compose_conv')

lemma equal_pfun [code]:
  "HOL.equal (pfun_of_alist xs) (pfun_of_alist ys) ⟷
    (let ks = map fst xs; ls = map fst ys
     in (∀l∈set ls. l ∈ set ks) ∧ (∀k∈set ks. k ∈ set ls ∧ map_of xs k = map_of ys k))"
  apply (simp add: equal_pfun_def, transfer, safe, simp_all)
  apply (metis map_of_eq_None_iff option.distinct(1) weak_map_of_SomeI)
  apply (metis domI domIff map_of_eq_None_iff weak_map_of_SomeI)
  apply (metis (no_types, lifting) image_iff map_of_eq_None_iff)
  done

lemma set_inter_Collect: "set xs ∩ Collect P = set (filter P xs)"
  by (auto)

text ‹ Partial abstractions can either be modelled finitely, as lists, or infinitely as total functions.
 We therefore allow both of these as possibilities. If an abstraction is over a finite set, then
 it is compiled to an associative list. Otherwise, it becomes an enriched total function via
 @{const pfun_entries}. ›

lemma pabs_set [code]: "pabs (set xs) P f = pfun_of_alist (map (λk. (k, f k)) (filter P xs))"
  by (auto simp add: pfun_eq_iff apply_pfun_alist map_of_map prod.case_eq_if image_iff map_of_map_restrict)

lemma pabs_coset [code]: 
  "pabs (List.coset A) P f = pfun_of_map (λ x. if x ∈ List.coset A ∧ P x then Some (f x) else None)"
  by (simp add: pabs_def, transfer, auto)

lemma pfun_app_of_map [code]: "pfun_app (pfun_of_map f) x = the (f x)"
  by (simp add: domIff option.the_def)

lemma graph_pfun_set [code]: 
  "graph_pfun (set xs) = pfun_of_alist (filter (λ(x, y). length (remdups (map snd (AList.restrict {x} xs))) = 1) xs)"
  by (transfer, simp only: comp_def mk_functional_alist)
     (metis graph_map_set mk_functional mk_functional_alist)

lemma pabs_basic_pfun_entries [code_unfold]: "(λ x ∙ f x) = pfun_entries (List.coset []) f"
  by (metis UNIV_coset pfun_entries_pabs)

declare pdom_pfun_entries [code]
                 
lemma pfun_app_entries [code]: "pfun_app (pfun_entries A f) x = (if x ∈ A then f x else undefined)"
  by auto

text ‹ Useful for optimising relational compositions containing partial functions ›

declare rel_comp_pfun [code_unfold]

text ‹ Fusing associative lists ›

fun pfuse_alist :: "('k × 'a) list ==> ('k 🍋 'b) ==> ('k × ('a × 'b)) list" where
"pfuse_alist [] f = []" |
"pfuse_alist ((k, v) # ps) f =
   (if k ∈ pdom f then (k, (v, pfun_app f k)) # pfuse_alist ps f else pfuse_alist ps f)"   

lemma pfuse_pfun_of_alist_aux: 
  "pfuse (pfun_of_alist xs) g = pfun_of_alist (pfuse_alist xs g)"
  apply (induct xs)
  apply (simp_all add: pfuse_upd, safe, simp_all)
  apply (metis (no_types, lifting) disjoint_iff_not_equal pdom_nres_disjoint pfun_upd_ext pfun_upd_twice pfuse_upd singletonD)
  done

lemma pfuse_pfun_of_alist [code]: 
  "pfuse (pfun_of_alist xs) g = pfun_of_alist (pfuse_alist (AList.clearjunk xs) g)"
  by (metis pfun_of_alist_clearjunk pfuse_pfun_of_alist_aux)

subsection ‹ Notation ›

bundle Z_Pfun_Notation
begin

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

no_notation funcset (infixr "→" 60)

notation pfun_tfun (infixr "→" 60)
notation pfun_pfun (infixr "🍋" 60)
notation pfun_ffun (infixr "🍋" 60)
notation pfun_pinj (infixr "🍋" 60)
notation pfun_finj (infixr "🍋" 60)
notation pfun_psurj (infixr "🍋" 60)
notation pfun_tinj (infixr "🍋" 60)
notation pfun_bij (infixr "🍋" 60)

notation pdom_res (infixr "🍋" 86)
notation pdom_nres (infixr "🍋" 86)

notation pran_res (infixl "🍋" 86)
notation pran_nres (infixl "🍋" 86)

notation pempty ("{↦}")

end

text ‹ Hide implementation details for partial functions ›

lifting_update pfun.lifting
lifting_forget pfun.lifting

end