Quelle  Partial_Fun.thy   Sprache: Isabelle

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 = (\<exists> k v. f = {k \<mapsto> v}\<^sub>p)" 

lemma pfun_singleton_dom: "pfun_singleton f \<longleftrightarrow> (\<exists> 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 \<mapsto> v}\<^sub>p"
  by (auto simp add: pfun_singleton_def)

definition dest_pfsingle :: "('a \<Zpfun> 'b) \<Rightarrow> 'a \<times> 'b" where
"dest_pfsingle f = (THE (k, v). f = {k \<mapsto> v}\<^sub>p)"

lemma dest_pfsingle_maplet [simp]: "dest_pfsingle {k \<mapsto> v}\<^sub>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 \<open> Summation \<close>
    
definition pfun_sum :: "('k, 'v::comm_monoid_add) pfun \<Rightarrow> 'v" where
"pfun_sum f = sum (pfun_app f) (pdom f)"
    
lemma pfun_sum_empty [simp]: "pfun_sum {}\<^sub>p = 0"
  by (simp add: pfun_sum_def)

lemma pfun_sum_upd_1:
  assumes "finite(pdom(m))" "k \<notin> pdom(m)"
  shows "pfun_sum (m(k \<mapsto> v)\<^sub>p) = pfun_sum m + v"
proof -
  from assms(2) have "(\<Sum>x\<in>pdom m. if k = x then v else m(x)\<^sub>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 \<mapsto> v)\<^sub>p) = pfun_sum ((- {k}) \<lhd>\<^sub>p m) + v"
proof (cases "k \<notin> 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}) \<lhd>\<^sub>p m)" k v]
    by (simp add: pfun_sum_upd_1)
qed

lemma pfun_sum_dom_res_insert [simp]: 
  assumes "x \<in> pdom f" "x \<notin> A" "finite A" 
  shows "pfun_sum ((insert x A) \<lhd>\<^sub>p f) = f(x)\<^sub>p + pfun_sum (A \<lhd>\<^sub>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 \<lhd>\<^sub>p f) = pfun_sum f - (pfun_sum ((- A) \<lhd>\<^sub>p f))"
proof -
  have 1:"A \<inter> 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 \<inter> 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) \<lhd>\<^sub>p f) = pfun_sum f - pfun_sum (A \<lhd>\<^sub>p f)"
  using assms
  by (subst pfun_sum_pdom_res, simp_all add: assms)

subsection \<open> Conversions \<close>

definition list_pfun :: "'a list \<Rightarrow> nat \<Zpfun> 'a" where
"list_pfun xs = (\<lambda> i | 0 < i \<and> i \<le> length xs \<bullet> 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: "\<lbrakk> 0 < i; i \<le> length xs \<rbrakk> \<Longrightarrow> (list_pfun xs)(i)\<^sub>p = xs ! (i - 1)"
  by (simp add: list_pfun_def)

lemma pfun_graph_list_pfun: "pfun_graph (list_pfun xs) = (\<lambda> 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 \<Zpfun> 'a. \<exists> i. pdom(f) = {1..i}}"
proof (rule set_eqI, rule iffI)
  fix f :: "nat \<Zpfun> 'a"
  assume "f \<in> range list_pfun"
  thus "f \<in> {f. \<exists>i. pdom f = {1..i}}"
    by auto
next
  fix f :: "nat \<Zpfun> 'a"
  assume "f \<in> {f. \<exists>i. pdom f = {1..i}}"
  thus "f \<in> range list_pfun"
  proof (unfold list_pfun_def pabs_def image_def, transfer)
    fix f :: "nat \<Rightarrow> 'a option"
    assume "f \<in> {f. \<exists>i. dom f = {1..i}}"
    then obtain i where i:"dom f = {1..i}"
      by blast
    hence 1: "\<And>x. dom f = {Suc 0..i} \<Longrightarrow> 0 < x \<Longrightarrow> x \<le> i \<Longrightarrow> 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 = (\<lambda>xa. Some (map (the \<circ> f \<circ> nat) [1..int i] ! (xa - Suc 0))) |` {ia. 0 < ia \<and> ia \<le> length (map (the \<circ> f \<circ> nat) [1..int i])}"
      by (auto simp add: fun_eq_iff restrict_map_def)
    have 3: "(\<lambda>xa. Some (map (the \<circ> f \<circ> nat) [1..int i] ! (xa - Suc 0))) |` {ia. 0 < ia \<and> ia \<le> length (map (the \<circ> f \<circ> nat) [1..int i])} \<in> {y. \<exists>x\<in>UNIV. y = (\<lambda>xa. if xa \<in> UNIV then Some (x ! (xa - 1)) else None) |` (UNIV \<inter> {i. 0 < i \<and> i \<le> length x})}"
      by (auto simp add: fun_eq_iff restrict_map_def)
    show "f \<in> {y. \<exists>x\<in>UNIV. y = (\<lambda>xa. if xa \<in> UNIV then Some (x ! (xa - 1)) else None) |` (UNIV \<inter> {i. 0 < i \<and> i \<le> length x})}"
      using "3" f by auto
  qed
qed

lemma list_pfun_le_iff_prefix [simp]: "list_pfun xs \<le> list_pfun ys \<longleftrightarrow> xs \<le> 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 \<mapsto> v)\<^sub>p \<subseteq>\<^sub>p g) = (k \<in> pdom g \<and> g(k)\<^sub>p = v \<and> (- {k}) \<lhd>\<^sub>p f \<subseteq>\<^sub>p g)"
  by (auto simp add: pfun_le_iff)

lemma pfun_upd_le_pfun_upd: "(f(k \<mapsto> v)\<^sub>p \<subseteq>\<^sub>p g(k \<mapsto> v)\<^sub>p) = ((- {k}) \<lhd>\<^sub>p f \<subseteq>\<^sub>p (- {k}) \<lhd>\<^sub>p g)"
  by (auto simp add: pfun_le_iff)

subsection \<open> Partial Function Lens \<close>

definition pfun_lens :: "'a \<Rightarrow> ('b \<Longrightarrow> ('a, 'b) pfun)" where
[lens_defs]: "pfun_lens i = \<lparr> lens_get = \<lambda> s. s(i)\<^sub>p, lens_put = \<lambda> s v. s(i \<mapsto> v)\<^sub>p \<rparr>"

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

lemma pfun_lens_src: "\<S>\<^bsub>pfun_lens i\<^esub> = {f. i \<in> pdom(f)}"
  by (simp add: lens_defs lens_source_def, transfer, force)

lemma lens_override_pfun_lens:
  "x \<in> pdom(g) \<Longrightarrow> f \<oplus>\<^sub>L g on pfun_lens x = f \<oplus> ({x} \<lhd>\<^sub>p g)"
  by (simp add: lens_defs pfun_ovrd_single_upd)

subsection \<open> Prism Functions \<close>

text \<open> We can use prisms to index a type and construct partial functions. \<close>

definition prism_fun :: "('a \<Longrightarrow>\<^sub>\<triangle> 'e) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> bool \<times> 'b) \<Rightarrow> ('e \<Zpfun> 'b)"
  where [code_unfold]: "prism_fun c A PB = (\<lambda> x\<in>build\<^bsub>c\<^esub> ` A | fst (PB (the (match\<^bsub>c\<^esub> x))) \<bullet> snd (PB (the (match\<^bsub>c\<^esub> x))))"

definition prism_fun_upd :: "('e \<Zpfun> 'b) \<Rightarrow> ('a \<Longrightarrow>\<^sub>\<triangle> 'e) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> bool \<times> 'b) \<Rightarrow> ('e \<Zpfun> 'b)"
  where [code_unfold]: "prism_fun_upd F c A PB = F \<oplus> prism_fun c A PB"

nonterminal prism_maplet and prism_maplets

syntax
  "_prism_maplet"        :: "id \<Rightarrow> pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> prism_maplet" ("_{_ \<in> _./ _} \<Rightarrow> _")
  "_prism_maplet_mem"    :: "id \<Rightarrow> pttrn \<Rightarrow> logic \<Rightarrow> logic \<Rightarrow> prism_maplet" ("_{_ \<in> _} \<Rightarrow> _")
  "_prism_maplet_simple" :: "id \<Rightarrow> pttrn \<Rightarrow> logic \<Rightarrow> prism_maplet" ("_ _ \<Rightarrow> _")
  ""                     :: "prism_maplet \<Rightarrow> prism_maplets"             ("_")
  "_prism_Maplets"       :: "[prism_maplet, prism_maplets] \<Rightarrow> prism_maplets" ("_ |/ _")
  "_prism_fun_upd"       :: "logic \<Rightarrow> prism_maplets \<Rightarrow> logic" ("_'(_')" [900, 0] 900)
  "_prism_fun"           :: "prism_maplets \<Rightarrow> logic" ("{_}\<^sub>p")

translations
  "f(c{v \<in> A. P} \<Rightarrow> B)" == "CONST prism_fun_upd f c A (\<lambda> v. (P, B))"
  "f(c{v \<in> A} \<Rightarrow> B)" == "f(c{v \<in> A. CONST True} \<Rightarrow> B)"
  "f(c v \<Rightarrow> B)" == "f(c{v \<in> CONST UNIV} \<Rightarrow> B)"
  "_prism_fun_upd m (_prism_Maplets xy ms)"  \<rightleftharpoons> "_prism_fun_upd (_prism_fun_upd m xy) ms"
  "_prism_fun ms"                            \<rightleftharpoons> "_prism_fun_upd {}\<^sub>p ms"
  "_prism_fun (_prism_Maplets ms1 ms2)"     \<leftharpoondown> "_prism_fun_upd (_prism_fun ms1) ms2"
  "_prism_Maplets ms1 (_prism_Maplets ms2 ms3)" \<leftharpoondown> "_prism_Maplets (_prism_Maplets ms1 ms2) ms3"

lemma dom_prism_fun: "wb_prism c \<Longrightarrow> pdom(prism_fun c A PB) = {build\<^bsub>c\<^esub> v | v. v \<in> A \<and> fst (PB v)}"
  by (simp add: prism_fun_def, auto)

lemma prism_fun_compat: "c \<nabla> d \<Longrightarrow> 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 \<nabla> d \<Longrightarrow> prism_fun c A PB \<oplus> prism_fun d B QB = prism_fun d B QB \<oplus> prism_fun c A PB"
  by (meson override_comm prism_fun_compat)

lemma prism_fun_apply: "\<lbrakk> wb_prism c; v \<in> A; fst (PB v) \<rbrakk> \<Longrightarrow> (prism_fun c A PB)(build\<^bsub>c\<^esub> v)\<^sub>p = snd (PB v)"
  by (simp add: prism_fun_def)

lemma prism_fun_update_app_1 [simp]: "\<lbrakk> wb_prism c; v \<in> A; P v \<rbrakk> \<Longrightarrow> (f(c{x \<in> A. P(x)} \<Rightarrow> B(x)))(build\<^bsub>c\<^esub> v)\<^sub>p = B v"
  by (simp add: prism_fun_def prism_fun_upd_def)

lemma prism_fun_update_app_2 [simp]: "\<lbrakk> wb_prism c; wb_prism d; d \<nabla> c \<rbrakk> \<Longrightarrow> (f(c{x \<in> A. P(x)} \<Rightarrow> B(x)))(build\<^bsub>d\<^esub> v)\<^sub>p = f(build\<^bsub>d\<^esub> v)\<^sub>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 \<in> A. P(x)} \<Rightarrow> g(x) | c{x \<in> A. P(x)} \<Rightarrow> h(x)) = f(c{x \<in> A. P(x)} \<Rightarrow> 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 \<nabla> d \<Longrightarrow> f(c{x \<in> A. P(x)} \<Rightarrow> g(x) | d{y \<in> B. Q(y)} \<Rightarrow> h(y)) 
            = f(d{y \<in> B. Q(y)} \<Rightarrow> h(y) | c{x \<in> A. P(x)} \<Rightarrow> 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) \<union> (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: "\<lbrakk> wb_prism c; x \<in> A; fst (PB x) \<rbrakk> \<Longrightarrow> build\<^bsub>c\<^esub> x \<in> 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 \<nabla> d"
  shows "prism_fun c A PB \<oplus> prism_fun d B QB = prism_fun (c +\<^sub>\<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:
  "\<lbrakk> wb_prism c; wb_prism d; c \<nabla> d \<rbrakk> \<Longrightarrow> pdom(prism_fun c A P\<sigma>) \<inter> pdom(prism_fun d B Q\<rho>) = {}"
  by (auto simp add: dom_prism_fun prism_diff_build)

lemma prism_fun_cong: "\<lbrakk> c = d; A = B; PB = QB \<rbrakk> \<Longrightarrow> prism_fun c A PB = prism_fun d B QB"
  by blast

lemma prism_fun_cong2: 
  assumes 
    "wb_prism c\<^sub>1" "wb_prism c\<^sub>2" 
    "c\<^sub>1 = c\<^sub>2" "A\<^sub>1 = A\<^sub>2" 
    "\<And> i. i \<in> A\<^sub>1 \<Longrightarrow> P\<^sub>1 i \<longleftrightarrow> P\<^sub>2 i" 
    "\<And> i. \<lbrakk> i \<in> A\<^sub>1; P\<^sub>1 i \<rbrakk> \<Longrightarrow> B\<^sub>1 i = B\<^sub>2 i"
  shows "prism_fun c\<^sub>1 A\<^sub>1 (\<lambda> x. (P\<^sub>1 x, B\<^sub>1 x)) = prism_fun c\<^sub>2 A\<^sub>2 (\<lambda> y. (P\<^sub>2 y, B\<^sub>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 (\<lambda> x. (B x, C x))) = prism_fun a A (\<lambda> x. (B x, f (C x)))"
  by (simp add: prism_fun_def)

lemma prism_fun_as_map:
  "wb_prism b \<Longrightarrow> 
   prism_fun b A PB = pfun_of_map (\<lambda> x. case match\<^bsub>b\<^esub> x of None \<Rightarrow> None | Some x \<Rightarrow> if x \<in> A \<and> 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 \<open> Code Generator \<close>

subsubsection \<open> Associative Lists \<close>

lemma relt_pfun_iff: 
  "relt_pfun R f g \<longleftrightarrow> (pdom(f) = pdom(g) \<and> (\<forall> x\<in>pdom(f). R (f(x)\<^sub>p) (g(x)\<^sub>p)))"
  by (transfer, auto simp add: rel_map_iff)

lift_definition pfun_of_alist :: "('a \<times> 'b) list \<Rightarrow> 'a \<Zpfun> '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 [] = {}\<^sub>p"
  by (transfer, simp)

lemma pfun_of_alist_Cons [simp]: "pfun_of_alist (p # ps) = pfun_of_alist ps(fst p \<mapsto> snd p)\<^sub>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]: "{}\<^sub>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 \<in> 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 (\<lambda> (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 (\<lambda> 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 \<lhd>\<^sub>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) \<Longrightarrow> pfun_of_alist xs \<rhd>\<^sub>p A = pfun_of_alist (filter (\<lambda>(k, v). v \<in> A) xs)"
  by (induct xs, auto)

lemma pran_res_alist [code]: "pfun_of_alist xs \<rhd>\<^sub>p A = pfun_of_alist (filter (\<lambda>(k, v). v \<in> A) (AList.clearjunk xs))"
  by (metis distinct_clearjunk pfun_of_alist_clearjunk pran_res_alist_distinct)

lemma pdom_res_set_map [code]:
  "set xs \<lhd>\<^sub>p (pfun_of_map m) = pfun_of_alist (map (\<lambda> x. (x, the (m x))) (filter (\<lambda> x. m x \<noteq> 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 \<oplus> 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 (\<lambda> k. (k, f *Copyright c 2007SUSE Linux Products 
  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 \<lhd>\<^sub>p pfun_entries (set bs) f = 
    pfun_of_alist (map (\<lambda> k. (k, f k)) (filter (\<lambda>x. x \<in> A) bs))"
  by (metis inter_set_filter pdom_res_entries pfun_entries_alist)

lemma pfun_alist_oplus_map [code *wakeuppath.
  "pfun_of_alistxs\opluspfun_of_map  = pfun_of_map (\lambda .fk None <>map_of xsk|Some  <>Some v)"
  ( :map_add_defoplus_pfun.pfun_of_alistabs_eq

lemma pfun_map_oplus_alist [code]: 
  "pfun_of_map f \<oplus> pfun_of_alist xs = pfun_of_map (\<lambda> k. if k \<in> set (map fst xs) then map_of xs k else f k)"
  byendif
     ( map_of_eq_None_iffoption.case_eq_ifoption.exhaustoption.sel)

lemma pfun_singleton_alist [  depth+;
  by simp

lemma dest_pfsingle_alist [
   simp

text\open>Adapted from Mapping theory \<close>

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

lemma pcombine_alist [code]:
  pcombine f(fun_of_alist  xs)(pfun_of_alist ys) =
     ptabulate (remdups (map fst xs @ map fst ys))
       \lambda>.the(ombine_options f (map_of xs x) (map_of ys x)))"
   transfer
  apply (rule ext)
  (ulesym)
  subgoal for f xs ys x
    apply (cases "map_of xs x";  kn_from: //n3
       apply (force  *kn_to:  //n2/n3/n4n5
         * [2] whenkn_fromis on adifferenthierarchyandneedtofind common
    done
  done

lemma pfun_comp_alist [code]: "pfun_of_alist ys \<circ>\<^ *result:  /../../n5
  by (transfer, simp add: compose_conv')

lemma equal_pfun  *kn_to:  n1/n2/n3         [depth=3
  "HOL.equal (pfun_of_alist xs) (pfun_of_alist *
    (let ks = map fst xs; ls = map fst ys
     in (\<forall>l\<in>set ls. l \< *
  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 (etis 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 static intkernfs_path_from_node_locked(struct kernfs_node*n_to,
   struct kernfs_node *kn_from,

 \>     bemodelledfinitely,as lists,or  totalfunctions
  
 strscpybuf /" buflen)
  @java.lang.StringIndexOutOfBoundsException: Index 0 out of bounds for length 0

lemma
  by (auto simp const char name;

lemma pabs_coset [ode]:
  "pabs kernfs_name -obtain the name of a given node
ef,transfer, auto)

lemma pfun_app_of_map [code*
the_defjava.lang.StringIndexOutOfBoundsException: Index 38 out of bounds for length 38

lemma graph_pfun_set [code]: 
  "java.lang.StringIndexOutOfBoundsException: Index 12 out of bounds for length 2
  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]: "(\<lambda> x \<bullet> f x) = pfun_entries (List.coset []) f"
  by  Thisfunctioncan becalled from any context.

declare {
                 
lemma java.lang.StringIndexOutOfBoundsException: Index 10 out of bounds for length 3
  by auto

> Useful foroptimisingrelationalcompositionscontaining partial functions \close>

declare  *kernfs_path_from_node - build path of node @to relative to @from.

text \<open> Fusing associative lists \<close>

fun pfuse_alist :: "('k \<times> 'a) list \<Rightarrow> ('k \<Zpfun> 'b) \<Rightarrow> ('k \ *buflen:size of @buf
"fuse_alist [ f =["|
" *be  thesame kernfs-. @from is not parent of @to then a relative
   (if k \<in> pdom f then (  path (which includes '.s java.lang.StringIndexOutOfBoundsException: Range [40, 33) out of bounds for length 70

lemma java.lang.StringIndexOutOfBoundsException: Index 11 out of bounds for length 2
  "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   \'  On ,- isreturned.
  done

 if(){
  "fuse ( xs)  = p (clearjunk xs) g)"
   m  pfuse_pfun_of_alist_auxjava.lang.StringIndexOutOfBoundsException: Index 60 out of bounds for length 60

subsection \<open> Notation \<close>

bundleZ_Pfun_Notation
begin

no_notation Stream.stream.Cons"(nfixr <open>#<close>65)

funcset( \rightarrow"60)

notation  @   
notation pfun_pfun (infixr "\<Zpfun>" 60)
notation pfun_ffun (infixr "\<Zffun>" java.lang.StringIndexOutOfBoundsException: Index 1 out of bounds for length 1
otation pfun_pinj i \<Zpinj"60
notation pfun_finj (infixr   sz =E2BIG)
notationpfun_psurj(nfixr \Zpsurj> 60java.lang.StringIndexOutOfBoundsException: Index 43 out of bounds for length 43
return;
notation pfun_bij ( * kernfs_name_hash -kernfs_name_hash-hashof n+@name

java.lang.StringIndexOutOfBoundsException: Index 7 out of bounds for length 3
pdom_nres infixr "Z"86)

 pran_res(infixl "Z"86
notation pran_nres (infixl "\<Znrres>" 86)

pempty "\mapsto>"

endifhash>kn>java.lang.StringIndexOutOfBoundsException: Range [21, 20) out of bounds for length 21

ion forfunctions <>

lifting_update  *kernfs_rwsem exclusive
ng_forgetpfunlifting

end