Theory utp_expr_ovld

section ‹ Overloaded Expression Constructs ›

theory utp_expr_ovld
  imports utp
begin

subsection ‹ Overloadable Constants ›

text ‹ For convenience, we often want to utilise the same expression syntax for multiple constructs.
  This can be achieved using ad-hoc overloading. We create a number of polymorphic constants and then
  overload their definitions using appropriate implementations. In order for this to work,
  each collection must have its own unique type. Thus we do not use the HOL map type directly,
  but rather our own partial function type, for example. ›
  
consts
  ― ‹ Empty elements, for example empty set, nil list, 0... › 
  uempty     :: "'f"
  ― ‹ Function application, map application, list application... ›
  uapply     :: "'f ⇒ 'k ⇒ 'v"
  ― ‹ Function update, map update, list update... ›
  uupd       :: "'f ⇒ 'k ⇒ 'v ⇒ 'f"
  ― ‹ Domain of maps, lists... ›
  udom       :: "'f ⇒ 'a set"
  ― ‹ Range of maps, lists... ›
  uran       :: "'f ⇒ 'b set"
  ― ‹ Domain restriction ›
  udomres    :: "'a set ⇒ 'f ⇒ 'f"
  ― ‹ Range restriction ›
  uranres    :: "'f ⇒ 'b set ⇒ 'f"
  ― ‹ Collection cardinality ›
  ucard      :: "'f ⇒ nat"
  ― ‹ Collection summation ›
  usums      :: "'f ⇒ 'a"
  ― ‹ Construct a collection from a list of entries ›
  uentries   :: "'k set ⇒ ('k ⇒ 'v) ⇒ 'f"
  
text ‹ We need a function corresponding to function application in order to overload. ›
  
definition fun_apply :: "('a ⇒ 'b) ⇒ ('a ⇒ 'b)"
where "fun_apply f x = f x"

declare fun_apply_def [simp]

definition ffun_entries :: "'k set ⇒ ('k ⇒ 'v) ⇒ ('k, 'v) ffun" where
"ffun_entries d f = graph_ffun {(k, f k) | k. k ∈ d}"

text ‹ We then set up the overloading for a number of useful constructs for various collections. ›
  
adhoc_overloading
  uempty ⇌ 0 and
  uapply ⇌ fun_apply and uapply ⇌ nth and uapply ⇌ pfun_app and
  uapply ⇌ ffun_app and
  uupd ⇌ pfun_upd and uupd ⇌ ffun_upd and uupd ⇌ list_augment and
  udom ⇌ Domain and udom ⇌ pdom and udom ⇌ fdom and udom ⇌ seq_dom and
  udom ⇌ Range and uran ⇌ pran and uran ⇌ fran and uran ⇌ set and
  udomres ⇌ pdom_res and udomres ⇌ fdom_res and
  uranres ⇌ pran_res and udomres ⇌ fran_res and
  ucard ⇌ card and ucard ⇌ pcard and ucard ⇌ length and
  usums ⇌ list_sum and usums ⇌ Sum and usums ⇌ pfun_sum and
  uentries ⇌ pfun_entries and uentries ⇌ ffun_entries

subsection ‹ Syntax Translations ›

syntax
  "_uundef"     :: "logic" (‹⊥⇩u›)
  "_umap_empty" :: "logic" (‹[]⇩u›)
  "_uapply"     :: "('a ⇒ 'b, 'α) uexpr ⇒ utuple_args ⇒ ('b, 'α) uexpr" (‹_'(_')⇩a› [999,0] 999)
  "_umaplet"    :: "[logic, logic] => umaplet" (‹_ /↦/ _›)
  ""            :: "umaplet => umaplets"             (‹_›)
  "_UMaplets"   :: "[umaplet, umaplets] => umaplets" (‹_,/ _›)
  "_UMapUpd"    :: "[logic, umaplets] => logic" (‹_/'(_')⇩u› [900,0] 900)
  "_UMap"       :: "umaplets => logic" (‹(1[_]⇩u)›)
  "_ucard"      :: "logic ⇒ logic" (‹#⇩u'(_')›)
  "_udom"       :: "logic ⇒ logic" (‹dom⇩u'(_')›)
  "_uran"       :: "logic ⇒ logic" (‹ran⇩u'(_')›)
  "_usum"       :: "logic ⇒ logic" (‹sum⇩u'(_')›)
  "_udom_res"   :: "logic ⇒ logic ⇒ logic" (infixl ‹⊲⇩u› 85)
  "_uran_res"   :: "logic ⇒ logic ⇒ logic" (infixl ‹⊳⇩u› 85)
  "_uentries"   :: "logic ⇒ logic ⇒ logic" (‹entr⇩u'(_,_')›)

translations
  ― ‹ Pretty printing for adhoc-overloaded constructs ›
  "f(x)⇩a"    <= "CONST uapply f x"
  "dom⇩u(f)" <= "CONST udom f"
  "ran⇩u(f)" <= "CONST uran f"  
  "A ⊲⇩u f" <= "CONST udomres A f"
  "f ⊳⇩u A" <= "CONST uranres f A"
  "#⇩u(f)" <= "CONST ucard f"
  "f(k ↦ v)⇩u" <= "CONST uupd f k v"
  "0" <= "CONST uempty" ― ‹ We have to do this so we don't see uempty. Is there a better way of printing? ›

  ― ‹ Overloaded construct translations ›
  "f(x,y,z,u)⇩a" == "CONST bop CONST uapply f (x,y,z,u)⇩u"
  "f(x,y,z)⇩a" == "CONST bop CONST uapply f (x,y,z)⇩u"
  "f(x,y)⇩a"  == "CONST bop CONST uapply f (x,y)⇩u"  
  "f(x)⇩a"    == "CONST bop CONST uapply f x"
  "#⇩u(xs)"  == "CONST uop CONST ucard xs"
  "sum⇩u(A)" == "CONST uop CONST usums A"
  "dom⇩u(f)" == "CONST uop CONST udom f"
  "ran⇩u(f)" == "CONST uop CONST uran f"
  "[]⇩u"     => "«CONST uempty»"
  "⊥⇩u"     == "«CONST undefined»"
  "A ⊲⇩u f" == "CONST bop (CONST udomres) A f"
  "f ⊳⇩u A" == "CONST bop (CONST uranres) f A"
  "entr⇩u(d,f)" == "CONST bop CONST uentries d «f»"
  "_UMapUpd m (_UMaplets xy ms)" == "_UMapUpd (_UMapUpd m xy) ms"
  "_UMapUpd m (_umaplet  x y)"   == "CONST trop CONST uupd m x y"
  "_UMap ms"                      == "_UMapUpd []⇩u ms"
  "_UMap (_UMaplets ms1 ms2)"     <= "_UMapUpd (_UMap ms1) ms2"
  "_UMaplets ms1 (_UMaplets ms2 ms3)" <= "_UMaplets (_UMaplets ms1 ms2) ms3"

subsection ‹ Simplifications ›

lemma ufun_apply_lit [simp]: 
  "«f»(«x»)⇩a = «f(x)»"
  by (transfer, simp)

lemma lit_plus_appl [lit_norm]: "«(+)»(x)⇩a(y)⇩a = x + y" by (simp add: uexpr_defs, transfer, simp)
lemma lit_minus_appl [lit_norm]: "«(-)»(x)⇩a(y)⇩a = x - y" by (simp add: uexpr_defs, transfer, simp)
lemma lit_mult_appl [lit_norm]: "«times»(x)⇩a(y)⇩a = x * y" by (simp add: uexpr_defs, transfer, simp)
lemma lit_divide_apply [lit_norm]: "«(/)»(x)⇩a(y)⇩a = x / y" by (simp add: uexpr_defs, transfer, simp)

lemma pfun_entries_apply [simp]:
  "(entr⇩u(d,f) :: (('k, 'v) pfun, 'α) uexpr)(i)⇩a = ((«f»(i)⇩a) ◃ i ∈⇩u d ▹ ⊥⇩u)"
  by (pred_auto)
    
lemma udom_uupdate_pfun [simp]:
  fixes m :: "(('k, 'v) pfun, 'α) uexpr"
  shows "dom⇩u(m(k ↦ v)⇩u) = {k}⇩u ∪⇩u dom⇩u(m)"
  by (rel_auto)

lemma uapply_uupdate_pfun [simp]:
  fixes m :: "(('k, 'v) pfun, 'α) uexpr"
  shows "(m(k ↦ v)⇩u)(i)⇩a = v ◃ i =⇩u k ▹ m(i)⇩a"
  by (rel_auto)

subsection ‹ Indexed Assignment ›

syntax
  ― ‹ Indexed assignment ›
  "_assignment_upd" :: "svid ⇒ uexp ⇒ uexp ⇒ logic" (‹(_[_] :=/ _)› [63, 0, 0] 62)

translations
  ― ‹ Indexed assignment uses the overloaded collection update function \emph{uupd}. ›
  "_assignment_upd x k v" => "x := &x(k ↦ v)⇩u"

end