Theory Partial_Fun

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)¯"
  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: "𝒮⇘pfun_lens 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 ⟹⇩△ 'e) ⇒ 'a set ⇒ ('a ⇒ bool × 'b) ⇒ ('e ⇸ 'b)"
  where [code_unfold]: "prism_fun c A PB = (λ x∈build⇘c⇙ ` A | fst (PB (the (match⇘c⇙ x))) ∙ snd (PB (the (match⇘c⇙ x))))"

definition prism_fun_upd :: "('e ⇸ 'b) ⇒ ('a ⟹⇩△ '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⇘c⇙ 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⇘c⇙ 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⇘c⇙ 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⇘d⇙ v)⇩p = f(build⇘d⇙ 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⇘c⇙ 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 +⇩△ 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⇩1" "wb_prism c⇩2" 
    "c⇩1 = c⇩2" "A⇩1 = A⇩2" 
    "⋀ i. i ∈ A⇩1 ⟹ P⇩1 i ⟷ P⇩2 i" 
    "⋀ i. ⟦ i ∈ A⇩1; P⇩1 i ⟧ ⟹ B⇩1 i = B⇩2 i"
  shows "prism_fun c⇩1 A⇩1 (λ x. (P⇩1 x, B⇩1 x)) = prism_fun c⇩2 A⇩2 (λ y. (P⇩2 y, B⇩2 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⇘b⇙ 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