Theory Ground_Term_Context

theory Ground_Term_Context
  imports First_Order_Clause.Generic_Term_Context
begin

(* TODO: Do same pattern for nonground case *)
locale ground_term_context = 
  term_context_interpretation where is_var = "λ_. False" +
  smaller_subcontext where size = size⇩c +
  replace_at_subterm where is_var = "λ_. False"
for size⇩c

(* TODO: Name *)
locale ground_term_context' = ground_term_context where
  Fun = GFun and subterms = ground_subterms and fun_sym = ground_fun_sym and
  extra = ground_extra and size = ground_size and

  hole = ground_hole and compose_context = compose_ground_context and
  apply_context = apply_ground_context and subterms⇩l = ground_subterms⇩l and
  subcontext = ground_subcontext and subterms⇩r = ground_subterms⇩r and More = GMore and
  fun_sym⇩c = ground_fun_sym⇩c and extra⇩c = ground_extra⇩c and hole_position = ground_hole_position and
  context_at = ground_context_at and size⇩c = ground_size⇩c
for 
  GFun ground_subterms ground_fun_sym ground_extra ground_hole compose_ground_context
  apply_ground_context ground_subterms⇩l ground_subcontext ground_subterms⇩r GMore ground_fun_sym⇩c
  ground_extra⇩c ground_size ground_hole_position ground_context_at ground_size⇩c


end