Theory Z_Toolkit_Pretty

section ‹ Pretty Notation for Z ›

theory Z_Toolkit_Pretty
  imports Relation_Toolkit Number_Toolkit
  abbrevs "+>" = "⇸" and "+>" = "⤀" and "++>" = "⇻"
    and ">->" = "↣" and ">->" = "⤖" and ">+>" = "⤔" and ">++>" = "⤕"
    and "<|" = "⊲" and "<|" = "◁" and "<|" = "⩤" and "<|" = "⦉"
    and "|>" = "⊳" and "|>" = "▷" and "|>" = "⩥" and "|>" = "⦊"
    and "|`" = "↾" and "|`" = "↿" and "|`" = "⨡"
    and "O+" = "⊕"
    and ";;" = "⨾" and ";;" = "⨟"
    and "PP" = "ℙ" and "FF" = "𝔽"
begin

declare [[coercion_enabled]]

text ‹ Code generation set up ›

code_datatype pfun_of_alist

text ‹ Allow partial functions to be written with braces ›

syntax
  "_Pfun"     :: "maplets => ('a, 'b) pfun"            ("(1{_})")

bundle Z_Syntax
begin

unbundle Z_Type_Syntax

notation relcomp (infixr "⨾" 75)

end

text ‹ Relation Function Syntax ›

bundle Z_RFun_Syntax
begin

unbundle Z_Syntax

no_notation funcset (infixr "→" 60)

notation rel_tfun (infixr "→" 60)
notation rel_pfun (infixr "⇸" 60)
notation rel_ffun (infixr "⇻" 60)

end

context
  includes Z_RFun_Syntax
begin

subsection ‹ Examples ›

typ "ℙ ℕ → ℕ"
typ "ℙ ℕ ⇸ 𝔹"
term "{}"
term "P ⨾ Q"
term "A ◁ B ⩤ (P :: ℙ(ℕ) ⇸ 𝔹)"

term "ℙ ℕ → ℕ"
term "ℕ ⇻ ℕ"

end

end