Theory TypeApp

section ‹Type Application›

theory TypeApp
imports HOLCF
begin

subsection ‹Class of type constructors›

text ‹In HOLCF, the type @{typ "udom defl"} consists of deflations
over the universal domain---each value of type @{typ "udom defl"}
represents a bifinite domain. In turn, values of the continuous
function type @{typ "udom defl → udom defl"} represent functions from
domains to domains, i.e.~type constructors.›

text ‹Class ‹tycon›, defined below, will be populated with
dummy types: For example, if the type ‹foo› is an instance of
class ‹tycon›, then users will never deal with any values ‹x::foo› in practice. Such types are only used with the overloaded
constant ‹tc›, which associates each type ‹'a::tycon›
with a value of type @{typ "udom defl → udom defl"}. \medskip›

class tycon =
  fixes tc :: "('a::type) itself ⇒ udom defl → udom defl"

text ‹Type @{typ "'a itself"} is defined in Isabelle's meta-logic;
it is inhabited by a single value, written @{term "TYPE('a)"}. We
define the syntax ‹TC('a)› to abbreviate ‹tc
TYPE('a)›. \medskip›

syntax  "_TC" :: "type ⇒ logic"  (‹(1TC/(1'(_')))›)

syntax_consts "_TC" ⇌ tc

translations "TC('a)" ⇌ "CONST tc TYPE('a)"


subsection ‹Type constructor for type application›

text ‹We now define a binary type constructor that models type
application: Type ‹('a, 't) app› is the result of applying the
type constructor ‹'t› (from class ‹tycon›) to the type
argument ‹'a› (from class ‹domain›).›

text ‹We define type ‹('a, 't) app› using ‹domaindef›,
a low-level type-definition command provided by HOLCF (similar to
‹typedef› in Isabelle/HOL) that defines a new domain type
represented by the given deflation. Note that in HOLCF, ‹DEFL('a)› is an abbreviation for ‹defl TYPE('a)›, where
‹defl :: ('a::domain) itself ⇒ udom defl› is an overloaded
function from the ‹domain› type class that yields the deflation
representing the given type. \medskip›

domaindef ('a,'t) app = "TC('t::tycon)⋅DEFL('a::domain)"

text ‹We define the infix syntax ‹'a⋅'t› for the type ‹('a,'t) app›. Note that for consistency with Isabelle's existing
type syntax, we have used postfix order for type application: type
argument on the left, type constructor on the right. \medskip›

type_notation app (‹(_⋅_)› [999,1000] 999)

text ‹The ‹domaindef› command generates the theorem ‹DEFL_app›: @{thm DEFL_app [where 'a="'a::domain" and 't="'t::tycon"]},
which we can use to derive other useful lemmas. \medskip›

lemma TC_DEFL: "TC('t::tycon)⋅DEFL('a) = DEFL('a⋅'t)"
by (rule DEFL_app [symmetric])

lemma DEFL_app_mono [simp, intro]:
  "DEFL('a) ⊑ DEFL('b) ⟹ DEFL('a⋅'t::tycon) ⊑ DEFL('b⋅'t)"
 apply (simp add: DEFL_app)
 apply (erule monofun_cfun_arg)
done

end