Theory Coerce

header {* Coercion Operators *}

theory Coerce
imports Representable
begin

constdefs 
  coerce :: "'a => 'b"
  "coerce x ≡ proj (emb x)"

lemma proj_emb: "proj (emb x) = coerce x"
by (simp add: coerce_def)

text "Trivial instances of @{term coerce}"

lemma coerce_eq_id [simp]: "(coerce::'a => 'a) = id"
by (rule ext, simp add: coerce_def)

lemma coerce_eq_emb [simp]: "(coerce::'a => U) = emb"
by (rule ext, simp add: coerce_def)

lemma coerce_eq_proj [simp]: "(coerce::U => 'a) = proj"
by (rule ext, simp add: coerce_def)

text "Cancellation rules"

lemma emb_coerce [simp]:
  "emb x ::: rep_of TYPE('a) ==> emb ((coerce x)::'a) = emb x"
by (simp add: coerce_def)

lemma emb_coerce2:
  "rep_of TYPE('a) ≤ rep_of TYPE('b)
   ==> emb ((coerce::'a => 'b) x) = emb x"
by (simp add: coerce_def)

lemma coerce_idem [simp]:
  "rep_of TYPE('a) ≤ rep_of TYPE('b)
   ==> coerce ((coerce::'a => 'b) x) = coerce x"
by (simp add: coerce_def)

lemma coerce_inverse [simp]:
  "emb (x::'a) ::: rep_of TYPE('b) ==> coerce (coerce x :: 'b) = x"
by (simp only: coerce_def proj_inverse emb_inverse)

lemma coerce_type:
  "rep_of TYPE('a) ≤ rep_of TYPE('b)
   ==> emb ((coerce::'a => 'b) x) ::: rep_of TYPE('a)"
by (simp add: coerce_def)

lemma inj_coerce:
  "rep_of TYPE('a) ≤ rep_of TYPE('b)
   ==> inj (coerce::'a => 'b)"
 apply (rule inj_on_inverseI)
 apply (rule coerce_inverse)
 apply simp
done

end