Theory Relation_Toolkit

section ‹ Relation Toolkit ›

theory Relation_Toolkit
  imports Set_Toolkit Overriding
begin

subsection ‹ Conversions ›

text ‹ The majority of the relation toolkit is also part of HOL. We just need to generalise
  some of the syntax. ›

declare [[coercion rel_apply]]
declare [[coercion pfun_app]]
declare [[coercion pfun_of]]


text ‹ The following definition is semantically identical to @{const pfun_graph}, but is used to 
  represent coercions with associated reasoning. ›

definition rel_of_pfun :: "'a ⇸ 'b ⇒ 'a ↔ 'b" ("[_]⇩⇸") where
[code_unfold]: "rel_of_pfun = pfun_graph"

declare [[coercion rel_of_pfun]]
declare [[coercion pfun_of_pinj]]

notation pfun_of_pinj ("[_]⇩⤔")

subsection ‹ First component projection ›

text ‹ Z supports n-ary Cartesian products. We cannot support such structures directly in 
  Isabelle/HOL, but instead add the projection notations for the first and second components.
  A homogeneous finite Cartesian product type also exists in the Multivariate Analysis package. ›

abbreviation (input) "first ≡ fst"
notation first ("_.1" [999] 999)

subsection ‹ Second component projection ›

abbreviation (input) "second ≡ snd"
notation second ("_.2" [999] 999)

subsection ‹ Maplet ›

subsection ‹ Domain ›

hide_const (open) dom

consts dom :: "'f ⇒ 'a set"

adhoc_overloading
  dom ⇌ Map.dom and
  dom ⇌ Relation.Domain and
  dom ⇌ Partial_Fun.pdom and
  dom ⇌ Finite_Fun.fdom and
  dom ⇌ Partial_Inj.pidom

subsection ‹ Range ›

hide_const (open) ran

consts ran :: "'f ⇒ 'a set"

adhoc_overloading
  ran ⇌ Map.ran and
  ran ⇌ Relation.Range and
  ran ⇌ Partial_Fun.pran and
  ran ⇌ Finite_Fun.fran and
  ran ⇌ Partial_Inj.piran

subsection ‹ Identity relation ›

notation Id_on ("id[_]")

subsection ‹ Relational composition ›

notation relcomp (infixr "❙;" 75)

subsection ‹ Functional composition ›

text ‹ Composition is probably the most difficult of the Z functions to implement correctly. Firstly,
  the notation @{term "(∘)"} is already defined for HOL functions, and we need to respect that
  in order to use the HOL library functions. Secondly, Z composition can be used to compose 
  heterogeneous relations and functions, which is not easy to type infer. Consequently, we opt
  to use adhoc overloading here. ›

consts zcomp :: "'f ⇒ 'g ⇒ 'h" 

adhoc_overloading
  zcomp ⇌ Fun.comp and
  zcomp ⇌ pfun_comp and
  zcomp ⇌ ffun_comp

text ‹ Once we overload @{term Fun.comp}, we need to at least have output syntax set up. ›

notation (output) zcomp (infixl "∘" 55)

bundle Z_Relation_Syntax
begin

no_notation Fun.comp (infixl "∘" 55)
notation zcomp (infixl "∘" 55)

end

subsection ‹ Domain restriction and subtraction ›

consts dom_res :: "'a set ⇒ 'r ⇒ 'r" (infixr "◁" 85)

abbreviation ndres (infixr "⩤" 85) where "ndres A P ≡ CONST dom_res (- A) P" 

adhoc_overloading 
  dom_res ⇌ rel_domres
  and dom_res ⇌ pdom_res
  and dom_res ⇌ fdom_res
  and dom_res ⇌ pinj_dres

syntax "_ndres" :: "logic ⇒ logic ⇒ logic" 
translations "_ndres A P" == "CONST dom_res (- A) P"

subsection ‹ Range restriction and subtraction ›

consts ran_res :: "'r ⇒ 'a set ⇒ 'r" (infixl "▷" 86)

abbreviation nrres (infixl "⩥" 86) where "nrres P A ≡ CONST ran_res P (- A)"

adhoc_overloading 
  ran_res ⇌ rel_ranres
  and ran_res ⇌ pran_res
  and ran_res ⇌ fran_res
  and ran_res ⇌ pinj_rres

subsection ‹ Relational inversion ›

notation converse ("(_⇧∼)" [1000] 999)

lemma relational_inverse: "r⇧∼ = {(p.2, p.1) | p. p ∈ r}"
  by auto

subsection ‹ Relational image ›

notation Image ("_⦇_⦈" [990] 990)

lemma Image_eq: "Image r a = {p.2 | p. p ∈ r ∧ p.1 ∈ a}"
  by (auto simp add: Image_def)

subsection ‹ Overriding ›

lemma dom_override: "dom ((Q :: 'a ↔ 'b) ⊕ R) = (dom Q) ∪ (dom R)"
  by (simp add: Un_Int_distrib2)

lemma override_Un: "dom Q ∩ dom R = {} ⟹ Q ⊕ R = Q ∪ R"
  by (simp add: override_eq Int_commute rel_domres_compl_disj)

subsection ‹ Proof Support ›

text ‹ The objective of these laws is to, as much as possible, convert relational constructions
  into functional ones. The benefit is better proof automation in the more type constrained setting. ›

lemma rel_of_pfun_eq_iff [simp]: "[f]⇩⇸ = [g]⇩⇸ ⟷ f = g"
  by (simp add: pfun_eq_graph rel_of_pfun_def)

lemma rel_of_pfun_le_iff [simp]: "[f]⇩⇸ ⊆ [g]⇩⇸ ⟷ f ≤ g"
  by (simp add: pfun_graph_le_iff rel_of_pfun_def)

lemma rel_of_pfun_pabs: "[pabs A P f]⇩⇸ = {(k, v). k ∈ A ∧ P k ∧ v = f k}"
  by (simp add: rel_of_pfun_def pfun_graph_pabs)

lemma rel_of_pfun_apply [simp]: "[f]⇩⇸ x = f x"
  by (simp add: rel_of_pfun_def)

lemma rel_of_pfun_functional [simp]: "functional [f]⇩⇸"
  by (simp add: rel_of_pfun_def)

lemma rel_of_pfun_override [simp]: "[f]⇩⇸ ⊕ [g]⇩⇸ = [f ⊕ g]⇩⇸"
  by (simp add: pfun_graph_override rel_of_pfun_def)

lemma rel_of_pfun_comp [simp]: "[f]⇩⇸ O [g]⇩⇸ = [g ∘⇩p f]⇩⇸"
  by (simp add: pfun_graph_comp rel_of_pfun_def)

lemma pfun_comp_inv: "[f ∘⇩p g]⇩⇸⇧∼ = [f]⇩⇸⇧∼ O [g]⇩⇸⇧∼"
  by (metis converse_relcomp rel_of_pfun_comp)

lemma rel_of_pfun_dom [simp]: "Domain [f]⇩⇸ = pdom f"
  by (simp add: Dom_pfun_graph rel_of_pfun_def)

lemma rel_of_pfun_ran [simp]: "Range [f]⇩⇸ = pran f"
  by (simp add: Range_pfun_graph rel_of_pfun_def)

lemma rel_of_pfun_domres [simp]: "A ◁ [f]⇩⇸ = [A ◁ f]⇩⇸"
  by (simp add: pfun_graph_domres rel_of_pfun_def)

lemma rel_of_pfun_ranres [simp]: "[f]⇩⇸ ▷ A = [f ▷ A]⇩⇸"
  by (simp add: rel_of_pfun_def pfun_graph_rres)

lemma rel_of_pfun_image [simp]: "[f]⇩⇸ ⦇ A ⦈ = pfun_image f A"
  by (simp add: Image_as_rel_domres)

lemma rel_of_pfun_member_iff [simp]:
  "(k, v) ∈ [f]⇩⇸ ⟷ (k ∈ dom f ∧ f k = v)"
  by (simp add: rel_of_pfun_def)

lemma rel_of_pinj_conv [simp]: "[[f]⇩⤔]⇩⇸¯ = [[pinv f]⇩⤔]⇩⇸"
  by (simp add: pfun_graph_pfun_inv pinv.rep_eq rel_of_pfun_def)

lemma dom_pinv [simp]: "dom [pinv f]⇩⤔ = ran [f]⇩⤔"
  by (simp add: pinv.rep_eq)

lemma ran_pinv [simp]: "ran [pinv f]⇩⤔ = dom [f]⇩⤔"
  by (metis dom_pinv pinv_pinv)

lemma pfun_inj_rel_conv [simp]: "pfun_inj f ⟹ [f]⇩⇸⇧∼ = [pfun_inv f]⇩⇸"
  by (simp add: pfun_graph_pfun_inv rel_of_pfun_def)

end