Theory Representable

header {* Representable Types *}

theory Representable
imports FinRep Idempotent
begin

subsection {* A HOL type universe *}

datatype U = Utag nat "U list"

(*datatype U = Unil | Upair U U

consts
  Ufst :: "U => U"
  Usnd :: "U => U"

primrec
  "Ufst Unil = Unil"
  "Ufst (Upair x y) = x"

primrec
  "Usnd Unil = Unil"
  "Usnd (Upair x y) = y"
*)
subsection {* Class of representable types *}

text "Overloaded embedding and projection functions between
      a representable type and the universal domain."

axclass rep_consts < type
consts
  emb :: "'a::rep_consts => U"
  proj :: "U => 'a::rep_consts"

axclass rep < rep_consts
  emb_inverse [simp]: "proj (emb x) = x"

lemma inj_emb: "inj (emb::'a::rep => U)"
by (rule inj_on_inverseI, rule emb_inverse)

lemmas emb_inject [simp] = inj_eq [OF inj_emb, standard]


subsection {* Instances of class @{text rep} *}

subsubsection {* Universal Domain *}

text "The Universe itself is trivially representable."

instance U :: rep_consts ..
defs (overloaded)
  emb_U_def [simp]: "emb ≡ id :: U => U"
  proj_U_def [simp]: "proj ≡ id :: U => U"

instance U :: rep
by (intro_classes, simp)

subsubsection {* Representable base types *}

text "The unit type is representable."

instance unit :: rep_consts ..
defs (overloaded)
(*  emb_unit_def: "emb ≡ λx::unit. Unil" *)
  emb_unit_def: "emb ≡ λx::unit. Utag 0 []"
  proj_unit_def: "proj ≡ λu. ()"

instance unit :: rep
by (intro_classes, simp)

text "The booleans are representable"

instance bool :: rep_consts ..
defs (overloaded)
  emb_bool_def: "emb ≡ λb. if b then Utag 0 [] else Utag 1 []"
  proj_bool_def: "proj ≡ λu. u = Utag 0 []"
(*  emb_bool_def: "emb ≡ λb. if b then Unil else Upair Unil Unil"
  proj_bool_def: "proj ≡ λu. u = Unil" *)

instance bool :: rep
by (intro_classes, simp add: emb_bool_def proj_bool_def)

text "The naturals are representable"

(*
consts
  nat_emb :: "nat => U"
  nat_proj :: "U => nat"

primrec
  "nat_emb 0 = Unil"
  "nat_emb (Suc n) = Upair Unil (nat_emb n)"

primrec
  "nat_proj Unil = 0"
  "nat_proj (Upair x y) = Suc (nat_proj y)"
*)

instance nat :: rep_consts ..
defs (overloaded)
  emb_nat_def: "emb ≡ λn. Utag n []"
  proj_nat_def: "proj ≡ λu. case u of Utag n xs => n"
(*  emb_nat_def: "emb ≡ nat_emb"
  proj_nat_def: "proj ≡ nat_proj" *)

instance nat :: rep
by (intro_classes, simp add: emb_nat_def proj_nat_def)
(*by (intro_classes, unfold emb_nat_def proj_nat_def, induct_tac x, simp_all)*)


subsubsection {* Representable type constructors *}

text "Products of representable types are representable."

instance "*" :: (rep, rep) rep_consts ..
defs (overloaded)
  emb_prod_def:
    "emb ≡ λx. Utag 0 [emb (fst x), emb (snd x)]"
  proj_prod_def:
    "proj ≡ λu. case u of Utag n xs => (proj (xs!0), proj (xs!1))"

(*  emb_prod_def: "emb ≡ λx. Upair (emb (fst x)) (emb (snd x))"
  proj_prod_def: "proj ≡ λx. (proj (Ufst x), proj (Usnd x))" *)

instance "*" :: (rep, rep) rep
by (intro_classes, simp add: emb_prod_def proj_prod_def)

text "Sums of representable types are representable."

instance "+" :: (rep, rep) rep_consts ..
defs (overloaded)
  emb_sum_def: "emb ≡ λx. case x of
    Inl a => Utag 0 [emb a] |
    Inr b => Utag 1 [emb b]"
  proj_sum_def: "proj ≡ λu. case u of Utag n xs =>
    if n = 0 then Inl (proj (xs!0)) else Inr (proj (xs!0))"
(*
  emb_sum_def: "emb ≡ λx. case x of
    Inl a => Upair (emb True) (emb a) |
    Inr b => Upair (emb False) (emb b)"
  proj_sum_def: "proj ≡ λx. if proj (Ufst x)
    then Inl (proj (Usnd x))
    else Inr (proj (Usnd x))"
*)
instance "+" :: (rep, rep) rep
by (intro_classes, unfold emb_sum_def proj_sum_def, simp split: sum.split)
(*
text "Lists of representable types are representable."

consts
  list_emb :: "U list => U"
  list_proj :: "U => U list"

primrec
  "list_emb [] = Unil"
  "list_emb (x # xs) = Upair x (list_emb xs)"

primrec
  "list_proj Unil = []"
  "list_proj (Upair x y) = x # list_proj y"

instance list :: (rep) rep_consts ..
defs (overloaded)
  emb_list_def: "emb ≡ list_emb o map emb"
  proj_list_def: "proj ≡ map proj o list_proj"

instance list :: (rep) rep
by (intro_classes, unfold emb_list_def proj_list_def, induct_tac x, simp_all)
*)
text "Functions from finite to representable types are representable."

instance fun :: (finrep, rep) rep_consts ..
defs (overloaded)
  emb_fun_def: "emb ≡ λf. Utag 0 (map (emb o f) LIST)"
  proj_fun_def: "proj ≡ λu. case u of Utag n xs =>
    (λa. proj (xs ! (LEAST n. LIST ! n = a)))"
(*  emb_fun_def: "emb ≡ λf. emb (map f LIST)"
  proj_fun_def: "proj ≡ λx a. proj x ! (LEAST n. LIST ! n = a)" *)

instance fun :: (finrep, rep) rep
apply (intro_classes, simp add: emb_fun_def proj_fun_def)
apply (rename_tac f, rule ext)
apply (rule_tac x=a and xs=LIST in all_nth_imp_all_set [rule_format])
apply (subst nth_map)
apply (erule order_le_less_trans [OF Least_le [OF refl]])
apply simp_all
apply (rule_tac f=f in arg_cong)
apply (rule LeastI [OF refl])
done


subsection {* Representations of types: @{term rep_of} *}

constdefs
  rep_of :: "'a::rep itself => U idem"
  "rep_of (a::'a::rep itself) ≡ Abs_idem (λu. emb (proj u::'a))"

lemma emb_proj: "emb (proj x::'a::rep) = cast (rep_of TYPE('a)) x"
 apply (unfold rep_of_def cast_def)
 apply (simp add: Abs_idem_inverse idempotent_def)
done

lemma cast_rep_of:
  "cast (rep_of TYPE('a::rep)) = (λu. emb (proj u::'a))"
by (rule ext, simp add: emb_proj)

lemma proj_inverse [simp]:
  "x ::: rep_of TYPE('a::rep) ==> emb (proj x::'a) = x"
by (simp add: emb_proj cast_fixed)

lemma emb_in_rep_of: "emb (x::'a::rep) ::: rep_of TYPE('a)"
by (rule in_idemI, simp add: cast_rep_of)

lemma emb_in_rep_of_le [simp]:
  "rep_of TYPE('a) ≤ rep_of B ==> emb (x::'a::rep) ::: rep_of B"
by (erule subidemD, rule in_idemI, simp add: cast_rep_of)


text {* @{term "rep_of TYPE(U)"} *}

lemma rep_of_U: "rep_of TYPE(U) = Abs_idem id"
by (simp add: rep_of_def id_def)

lemma less_rep_of_U [simp, intro!]: "A ≤ rep_of TYPE(U)"
by (simp add: rep_of_U)

lemma in_rep_of_U [simp, intro!]: "x ::: rep_of TYPE(U)"
by (simp add: rep_of_U)

lemma cast_rep_of_U: "cast (rep_of TYPE(U)) = id"
by (rule ext, simp add: cast_rep_of)


subsection {* Making @{term rep} the default class *}

text {*
  From now on, free type variables are assumed to be in class
  @{term rep}, unless specified otherwise.
*}

defaultsort rep

end