Theory IsaFoR_Abstract_Context

theory IsaFoR_Abstract_Context
  imports 
    First_Order_Terms.Subterm_and_Context
    Generic_Context
begin

fun fun_sym⇩c :: "('f, 't) actxt ⇒ 'f" where
  "fun_sym⇩c (More f _ _ _) = f"

fun subterms⇩l :: "('f, 't) actxt ⇒ 't list" where
  "subterms⇩l (More _ ls _ _) = ls"

fun subcontext :: "('f, 't) actxt ⇒ ('f, 't) actxt" where
  "subcontext (More _ _ c _) = c"

fun subterms⇩r :: "('f, 't) actxt ⇒ 't list" where
  "subterms⇩r (More _ _ _ rs) = rs"

interpretation abstract_context: smaller_subcontext where
  hole = □ and subcontext = subcontext and size = size
proof unfold_locales
  fix c :: "('f, 't) actxt"
  assume "c ≠ □"

  then show "size (subcontext c) < size c"
    by (cases c) auto
qed

end