theory No_Fin
imports Main "~~/src/HOL/Library/Extended"
begin

definition "no_Fin = Fin"
notation (output) no_Fin  ("_")

declaration {*
  let
    fun is_num (Const (@{const_name Num.One}, _)) = true
      | is_num (Const (@{const_name Num.Bit0}, _) $ t) = is_num t
      | is_num (Const (@{const_name Num.Bit1}, _) $ t) = is_num t
      | is_num _ = false;
  
    fun no_Fin T t = Const (@{const_name no_Fin}, T) $ t;

    fun uncheck (tm as Const (@{const_name Fin}, T) $ t) =
          (case t of
            Const (@{const_name zero_class.zero}, _) => no_Fin T t
          | Const (@{const_name one_class.one}, _) => no_Fin T t
          | Const (@{const_name numeral}, _) $ u => if is_num u then no_Fin T t else tm
          | _ => tm)
      | uncheck (t $ u) = uncheck t $ uncheck u
      | uncheck (Abs (x, T, t)) = Abs (x, T, uncheck t)
      | uncheck t = t;
  in fn _ => Syntax_Phases.term_uncheck 0 "no_Fin" (fn _ => map uncheck) end
*}

term "\<lambda>y::nat. [Fin 0, Fin 1, Fin 5, Fin x, Fin y]"

text {*
  @{term "\<lambda>y::nat. [Fin 0, Fin 1, Fin 5, Fin x, Fin y]"}
*}

end