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