Theory utp_expr_funcs

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 ⇧⌢⇩u B" == "CONST bop (⇧⌢) 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