Theory Function_Toolkit

section ‹ Function Toolkit ›

theory Function_Toolkit
  imports Relation_Toolkit
begin

subsection ‹ Partial Functions ›

lemma partial_functions: "X →⇩p Y = {f ∈ X ↔ Y. ∀ p ∈ f. ∀ q ∈ f. p.1 = q.1 ⟶ p.2 = q.2}"
  by (auto simp add: rel_pfun_def single_valued_def)

notation size ("#_" [999] 999)

instantiation set :: (type) size
begin
definition [simp]: "size A = card A"
instance ..
end

instantiation pfun :: (type, type) size
begin

definition size_pfun :: "('a ⇸ 'b) ⇒ nat" where
"size_pfun f = card (pfun_graph f)"

instance ..

end

lemma size_finite_pfun: "finite (pdom f) ⟹ #f = #(dom f)"
  by (simp add: card_pfun_graph size_pfun_def)

lemma card_pfun_empty [simp]: "#{}⇩p = 0"
  by (simp add: size_pfun_def pfun_graph_zero)

lemma card_pfun_update [simp]: "finite (dom f) ⟹ #(f(k ↦ v)⇩p) = (if (k ∈ dom f) then #f else #f + 1)"
  by (auto simp add: size_pfun_def pfun_graph_update Dom_pfun_graph rel_domres_compl_disj)
     (metis card_pfun_graph insert_absorb pdom_upd pfun_graph_update)

subsection ‹ Total Functions ›

text ‹ One issue that emerges in this encoding is the treatment of total functions. In Z, a total
  function is a particular kind of partial function whose domain covers the type universe. In HOL,
  a total function is one of the basic types. Typically, one wishes to apply total functions, 
  partial functions, and finite functions to values using the notation @{term "f x"}. In order
  to implement this, we need to coerce the given function @{term f} to a total function, since
  this is fundamental to HOL's application construct. However, that means that we can't also
  coerce a total function to a partial function, as expected by Z, since this would lead to
  a cycle. Consequently, we actually need to create a new ``total function'' type, different
  to the HOL one, to break the cycle. We therefore consider the HOL total function type
  to be meta-logical with respect to Z.  ›

declare [[coercion pfun_of_tfun]]

subsection ‹ Disjointness ›

consts 
  disjoint :: "'f ⇒ bool"

adhoc_overloading 
  disjoint ⇌ rel_disjoint and
  disjoint ⇌ pfun_disjoint and 
  disjoint ⇌ list_disjoint 

subsection ‹ Partitions ›

consts partitions :: "'f ⇒ 'a set ⇒ bool" (infix "partitions" 65)

adhoc_overloading
  partitions ⇌ rel_partitions and
  partitions ⇌ pfun_partitions and
  partitions ⇌ list_partitions

end