Theory HereditarilyFinite.Finitary

theory Finitary
imports Ordinal
begin

class finitary =
  fixes hf_of :: "'a ⇒ hf"
  assumes inj: "inj hf_of"
begin
  lemma hf_of_eq_iff [simp]: "hf_of x = hf_of y ⟷ x=y"
    using inj by (auto simp: inj_on_def)
end

instantiation unit :: finitary
begin
  definition hf_of_unit_def: "hf_of (u::unit) ≡ 0"
  instance
    by intro_classes (auto simp: inj_on_def hf_of_unit_def)
end

instantiation bool :: finitary
begin
  definition hf_of_bool_def: "hf_of b ≡ if b then 1 else 0"
  instance 
    by intro_classes (auto simp: inj_on_def hf_of_bool_def)
end

instantiation nat :: finitary
begin
  definition hf_of_nat_def: "hf_of ≡ ord_of"
  instance 
    by intro_classes (auto simp: inj_on_def hf_of_nat_def)
end

instantiation int :: finitary
begin
  definition hf_of_int_def: 
    "hf_of i ≡ if i≥(0::int) then ⟨0, hf_of (nat i)⟩ else ⟨1, hf_of (nat (-i))⟩"
  instance 
    by intro_classes (auto simp: inj_on_def hf_of_int_def)
end

text ‹Strings are char lists, and are not considered separately.›
instantiation char :: finitary
begin
  definition hf_of_char_def: 
    "hf_of x ≡ hf_of (of_char x :: nat)"
  instance 
    by standard (auto simp: inj_on_def hf_of_char_def)
end

instantiation prod :: (finitary,finitary) finitary
begin
  definition hf_of_prod_def: 
    "hf_of ≡ λ(x,y). ⟨hf_of x, hf_of y⟩"
  instance 
    by intro_classes (auto simp: inj_on_def hf_of_prod_def)
end

instantiation sum :: (finitary,finitary) finitary
begin
  definition hf_of_sum_def: 
    "hf_of ≡ case_sum (HF.Inl o hf_of) (HF.Inr o hf_of)"
  instance 
    by intro_classes (auto simp: inj_on_def hf_of_sum_def split: sum.split_asm)
end

instantiation option :: (finitary) finitary
begin
  definition hf_of_option_def: 
    "hf_of ≡ case_option 0 (λx. ⦃hf_of x⦄)"
  instance 
    by intro_classes (auto simp: inj_on_def hf_of_option_def split: option.split_asm)
end

instantiation list :: (finitary) finitary
begin
  primrec hf_of_list where
    "hf_of_list Nil = 0"
  | "hf_of_list (x#xs) = ⟨hf_of x, hf_of_list xs⟩"
  
lemma [simp]: fixes x :: "'a list" shows "hf_of x = hf_of y ⟹ x = y"
  proof (induction x arbitrary: y)
    case Nil
    then show ?case by (cases y) auto
  next
    case (Cons a x)
    then show ?case by (cases y) auto
  qed

instance 
  by intro_classes (auto simp: inj_on_def)
end

end