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