theory utp_expr_funcs
  imports utp_expr_insts
begin

syntax ― ‹ Polymorphic constructs ›
  "_uceil"      :: "logic → logic" (‹⌈_⌉_u›)
  "_ufloor"     :: "logic → logic" (‹⌊_⌋_u›)
  "_umin"       :: "logic → logic → logic" (‹min_u'(_, _')›)
  "_umax"       :: "logic → logic → logic" (‹max_u'(_, _')›)
  "_ugcd"       :: "logic → logic → logic" (‹gcd_u'(_, _')›)

translations
  ― ‹ Type-class polymorphic constructs ›
  "min_u(x, y)"  == "CONST bop (CONST min) x y"
  "max_u(x, y)"  == "CONST bop (CONST max) x y"
  "gcd_u(x, y)"  == "CONST bop (CONST gcd) x y"
  "⌈x⌉_u" == "CONST uop CONST ceiling x"
  "⌊x⌋_u" == "CONST uop CONST floor x"

syntax ― ‹ Lists / Sequences ›
  "_ucons"      :: "logic → logic → logic" (infixr ‹#_u› 65)
  "_unil"       :: "('a list, 'α) uexpr" (‹⟨⟩›)
  "_ulist"      :: "args => ('a list, 'α) uexpr"    (‹⟨(_)⟩›)
  "_uappend"    :: "('a list, 'α) uexpr → ('a list, 'α) uexpr → ('a list, 'α) uexpr" (infixr ‹^_u› 80)
  "_udconcat"   :: "logic → logic → logic" (infixr ‹^\⌢_u› 90)
  "_ulast"      :: "('a list, 'α) uexpr → ('a, 'α) uexpr" (‹last_u'(_')›)
  "_ufront"     :: "('a list, 'α) uexpr → ('a list, 'α) uexpr" (‹front_u'(_')›)
  "_uhead"      :: "('a list, 'α) uexpr → ('a, 'α) uexpr" (‹head_u'(_')›)
  "_utail"      :: "('a list, 'α) uexpr → ('a list, 'α) uexpr" (‹tail_u'(_')›)
  "_utake"      :: "(nat, 'α) uexpr → ('a list, 'α) uexpr → ('a list, 'α) uexpr" (‹take_u'(_,/ _')›)
  "_udrop"      :: "(nat, 'α) uexpr → ('a list, 'α) uexpr → ('a list, 'α) uexpr" (‹drop_u'(_,/ _')›)
  "_ufilter"    :: "('a list, 'α) uexpr → ('a set, 'α) uexpr → ('a list, 'α) uexpr" (infixl ‹🛇_u› 75)
  "_uextract"   :: "('a set, 'α) uexpr → ('a list, 'α) uexpr → ('a list, 'α) uexpr" (infixl ‹↿_u› 75)
  "_uelems"     :: "('a list, 'α) uexpr → ('a set, 'α) uexpr" (‹elems_u'(_')›)
  "_usorted"    :: "('a list, 'α) uexpr → (bool, 'α) uexpr" (‹sorted_u'(_')›)
  "_udistinct"  :: "('a list, 'α) uexpr → (bool, 'α) uexpr" (‹distinct_u'(_')›)
  "_uupto"      :: "logic → logic → logic" (‹⟨_.._⟩›)
  "_uupt"       :: "logic → logic → logic" (‹⟨_..<_\⟩›)
  "_umap"       :: "logic → logic → logic" (‹map_u›)
  "_uzip"       :: "logic → logic → logic" (‹zip_u›)

translations
  "x #_u ys" == "CONST bop (#) x ys"
  "⟨⟩"       == "«[]¬"
  "⟨x, xs⟩"  == "x #_u ⟨xs⟩"
  "⟨x⟩"      == "x #_u «[]¬"
  "x ^_u y"   == "CONST bop (@) x y"
  "A ^\<frown>_u B" == "CONST bop (^\<frown>) A B"
  "last_u(xs)" == "CONST uop CONST last xs"
  "front_u(xs)" == "CONST uop CONST butlast xs"
  "head_u(xs)" == "CONST uop CONST hd xs"
  "tail_u(xs)" == "CONST uop CONST tl xs"
  "drop_u(n,xs)" == "CONST bop CONST drop n xs"
  "take_u(n,xs)" == "CONST bop CONST take n xs"
  "elems_u(xs)" == "CONST uop CONST set xs"
  "sorted_u(xs)" == "CONST uop CONST sorted xs"
  "distinct_u(xs)" == "CONST uop CONST distinct xs"
  "xs 🛇_u A"   == "CONST bop CONST seq_filter xs A"
  "A ↿_u xs"   == "CONST bop (↿_l) A xs"
  "⟨n..k⟩" == "CONST bop CONST upto n k"
  "⟨n..<k⟩" == "CONST bop CONST upt n k"
  "map_u f xs" == "CONST bop CONST map f xs"
  "zip_u xs ys" == "CONST bop CONST zip xs ys"

syntax ― ‹ Sets ›
  "_ufinite"    :: "logic → logic" (‹finite_u'(_')›)
  "_uempset"    :: "('a set, 'α) uexpr" (‹{}_u›)
  "_uset"       :: "args => ('a set, 'α) uexpr" (‹{(_)}_u›)
  "_uunion"     :: "('a set, 'α) uexpr → ('a set, 'α) uexpr → ('a set, 'α) uexpr" (infixl ‹∪_u› 65)
  "_uinter"     :: "('a set, 'α) uexpr → ('a set, 'α) uexpr → ('a set, 'α) uexpr" (infixl ‹∩_u› 70)
  "_uinsert"    :: "logic → logic → logic" (‹insert_u›)
  "_uimage"     :: "logic → logic → logic" (‹_(_)_u› [10,0] 10)
  "_usubset"    :: "('a set, 'α) uexpr → ('a set, 'α) uexpr → (bool, 'α) uexpr" (infix ‹⊂_u› 50)
  "_usubseteq"  :: "('a set, 'α) uexpr → ('a set, 'α) uexpr → (bool, 'α) uexpr" (infix ‹⊆_u› 50)
  "_uconverse"  :: "logic → logic" (‹(_^~)› [1000] 999)
  "_ucarrier"   :: "type → logic" (‹[_]_T›)
  "_uid"        :: "type → logic" (‹id[_]›)
  "_uproduct"   :: "logic → logic → logic" (infixr ‹×_u› 80)
  "_urelcomp"   :: "logic → logic → logic" (infixr ‹;_u› 75)

translations
  "finite_u(x)" == "CONST uop (CONST finite) x"
  "{}_u"      == "«{}¬"
  "insert_u x xs" == "CONST bop CONST insert x xs"
  "{x, xs}_u" == "insert_u x {xs}_u"
  "{x}_u"     == "insert_u x «{}¬"
  "A ∪_u B"   == "CONST bop (∪) A B"
  "A ∩_u B"   == "CONST bop (∩) A B"
  "f(A)_u"     == "CONST bop CONST image f A"
  "A ⊂_u B"   == "CONST bop (⊂) A B"
  "f ⊂_u g"   <= "CONST bop (⊂_p) f g"
  "f ⊂_u g"   <= "CONST bop (⊂_f) f g"
  "A ⊆_u B"   == "CONST bop (⊆) A B"
  "f ⊆_u g"   <= "CONST bop (⊆_p) f g"
  "f ⊆_u g"   <= "CONST bop (⊆_f) f g"
  "P^~"        == "CONST uop CONST converse P"
  "['a]_T"     == "«CONST set_of TYPE('a)¬"
  "id['a]"    == "«CONST Id_on (CONST set_of TYPE('a))¬"
  "A ×_u B"    == "CONST bop CONST Product_Type.Times A B"
  "A ;_u B"    == "CONST bop CONST relcomp A B"

syntax ― ‹ Partial functions ›
  "_umap_plus"  :: "logic → logic → logic" (infixl ‹⊕_u› 85)
  "_umap_minus" :: "logic → logic → logic" (infixl ‹⊖_u› 85)

translations
  "f ⊕_u g"   => "(f :: ((_, _) pfun, _) uexpr) + g"
  "f ⊖_u g"   => "(f :: ((_, _) pfun, _) uexpr) - g"
  
syntax ― ‹ Sum types ›
  "_uinl"       :: "logic → logic" (‹inl_u'(_')›)
  "_uinr"       :: "logic → logic" (‹inr_u'(_')›)
  
translations
  "inl_u(x)" == "CONST uop CONST Inl x"
  "inr_u(x)" == "CONST uop CONST Inr x"

subsection ‹ Lifting set collectors ›

text ‹ We provide syntax for various types of set collectors, including intervals and the Z-style
 set comprehension which is purpose built as a new lifted definition. ›
  
syntax
  "_uset_atLeastAtMost" :: "('a, 'α) uexpr → ('a, 'α) uexpr → ('a set, 'α) uexpr" (‹(1{_.._}_u)›)
  "_uset_atLeastLessThan" :: "('a, 'α) uexpr → ('a, 'α) uexpr → ('a set, 'α) uexpr" (‹(1{_..<_}_u)›)
  "_uset_compr" :: "pttrn → ('a set, 'α) uexpr → (bool, 'α) uexpr → ('b, 'α) uexpr → ('b set, 'α) uexpr" (‹(1{_ :/ _ |/ _ ∙/ _}_u)›)
  "_uset_compr_nset" :: "pttrn → (bool, 'α) uexpr → ('b, 'α) uexpr → ('b set, 'α) uexpr" (‹(1{_ |/ _ ∙/ _}_u)›)

lift_definition ZedSetCompr ::
  "('a set, 'α) uexpr → ('a → (bool, 'α) uexpr × ('b, 'α) uexpr) → ('b set, 'α) uexpr"
is "λ A PF b. { snd (PF x) b | x. x ∈ A b ∧ fst (PF x) b}" .

translations
  "{x..y}_u" == "CONST bop CONST atLeastAtMost x y"
  "{x..<y}_u" == "CONST bop CONST atLeastLessThan x y"
  "{x | P ∙ F}_u" == "CONST ZedSetCompr (CONST lit CONST UNIV) (λ x. (P, F))"
  "{x : A | P ∙ F}_u" == "CONST ZedSetCompr A (λ x. (P, F))"

subsection ‹ Lifting limits ›
  
text ‹ We also lift the following functions on topological spaces for taking function limits,
 and describing continuity. ›

definition ulim_left :: "'a::order_topology → ('a → 'b) → 'b::t2_space" where
[uexpr_defs]: "ulim_left = (λ p f. Lim (at_left p) f)"

definition ulim_right :: "'a::order_topology → ('a → 'b) → 'b::t2_space" where
[uexpr_defs]: "ulim_right = (λ p f. Lim (at_right p) f)"

definition ucont_on :: "('a::topological_space → 'b::topological_space) → 'a set → bool" where
[uexpr_defs]: "ucont_on = (λ f A. continuous_on A f)"

syntax
  "_ulim_left"  :: "id → logic → logic → logic" (‹lim_u'(_ → _^-')'(_')›)
  "_ulim_right" :: "id → logic → logic → logic" (‹lim_u'(_ → _⁺')'(_')›)
  "_ucont_on"   :: "logic → logic → logic" (infix ‹cont-on_u› 90)

translations
  "lim_u(x → p^-)(e)" == "CONST bop CONST ulim_left p (λ x ∙ e)"
  "lim_u(x → p⁺)(e)" == "CONST bop CONST ulim_right p (λ x ∙ e)"
  "f cont-on_u A"     == "CONST bop CONST continuous_on A f"

lemma uset_minus_empty [simp]: "x - {}_u = x"
  by (simp add: uexpr_defs, transfer, simp)

lemma uinter_empty_1 [simp]: "x ∩_u {}_u = {}_u"
  by (transfer, simp)

lemma uinter_empty_2 [simp]: "{}_u ∩_u x = {}_u"
  by (transfer, simp)

lemma uunion_empty_1 [simp]: "{}_u ∪_u x = x"
  by (transfer, simp)

lemma uunion_insert [simp]: "(bop insert x A) ∪_u B = bop insert x (A ∪_u B)"
  by (transfer, simp)

lemma ulist_filter_empty [simp]: "x 🛇_u {}_u = ⟨⟩"
  by (transfer, simp)

lemma tail_cons [simp]: "tail_u(⟨x⟩ ^_u xs) = xs"
  by (transfer, simp)

lemma uconcat_units [simp]: "⟨⟩ ^_u xs = xs" "xs ^_u ⟨⟩ = xs"
  by (transfer, simp)+

end