Theory TypeApp

header {* Type Application *}

theory TypeApp
imports Representable
begin

subsection {* Type of monotone type constructor functions *}

typedef (open) monotc = "{f::U idem => U idem. mono f}"
by (rule_tac x=id in exI, simp add: mono_def)

subsection {* Class of type constructors *}

axclass tycon < type
consts monotc :: "'f::tycon itself => monotc"

constdefs
  tc :: "'f::tycon itself => U idem => U idem"
  "tc t ≡ Rep_monotc (monotc t)"

lemma mono_tc: "mono (tc t)"
by (unfold tc_def, rule Rep_monotc [simplified])


subsection {* Type constructor for type application *}

text "The representatives of a type constructor @{typ 'f} applied
      to representable type @{typ 'a}."

typedef (open) ('a,'f)App (infixl "$" 65)
  = "{x. x ::: tc TYPE('f::tycon) (rep_of TYPE('a::rep))}"
by (simp, rule nonempty_idem)

syntax (xsymbols)
  App :: "[type, type] => type" ("(_•_)" [999,1000] 999)

declare Rep_App_inverse[simp] Rep_App_inject[simp]
        Abs_App_inverse[simp] Abs_App_inject[simp]
        Abs_App_inject[THEN iffD2,intro!]

text "The result of domain application is representable."

instance App :: (rep, tycon) rep_consts ..
defs (overloaded)
  emb_App_def: "emb ≡ Rep_App"
  proj_App_def:
    "proj::U => 'a::rep•'f::tycon ≡
      λu. Abs_App (cast (tc TYPE('f) (rep_of TYPE('a))) u)"

instance App :: (rep, tycon) rep
 apply (intro_classes, unfold emb_App_def proj_App_def)
 apply (subst cast_fixed)
  apply (rule Rep_App [simplified])
 apply (rule Rep_App_inverse)
done

lemma rep_of_App:
  "rep_of TYPE('a::rep•'m::tycon) = tc TYPE('m) (rep_of TYPE('a))"
by (simp add: rep_of_def emb_App_def proj_App_def Abs_idem_cast
         del: proj_inverse)

lemma rep_of_App_mono [simp, intro]:
  "rep_of TYPE('a) ≤ rep_of TYPE('b)
    ==> rep_of TYPE('a•'m::tycon) ≤ rep_of TYPE('b•'m)"
 apply (simp add: rep_of_App)
 apply (erule mono_tc [THEN monoD])
done

end