Theory Polymorphic_Ground_Term

theory Polymorphic_Ground_Term
  imports 
    IsaFoR_Ground_Term
    Generic_Term
begin

datatype ('f, 'tyf) poly_gterm =
  PGFun (fun_sym: 'f) (type_args: "'tyf gterm list") (args: "('f, 'tyf) poly_gterm list")

interpretation poly_gterm: term_interpretation where
  Fun = PGFun and fun_sym = fun_sym and subterms = args and extra = type_args and
  is_var = is_var and size = size
proof unfold_locales
  fix t t' :: "('f, 'tyf) poly_gterm"
  assume "t' ∈ set (poly_gterm.args t)"

  then show "size t' < size t"
    by (induction t arbitrary: t') (auto simp: elem_size_size_list_size less_SucI trans_less_add2)
qed (auto intro: poly_gterm.exhaust)

end