Theory First_Order_Clause.Generic_Term_Context

theory Generic_Term_Context
  imports 
    Generic_Term
    Generic_Context
begin

locale term_context_interpretation = 
  term_interpretation where Fun = Fun +
  context_interpretation where More = More and fun_sym = fun_sym⇩c and extra = extra⇩c
for
  Fun :: "'f ⇒ 'e ⇒ 't list ⇒ 't" and
  More :: "'f ⇒ 'e ⇒ 't list ⇒ 'c ⇒ 't list ⇒ 'c" and
  fun_sym⇩c extra⇩c +
assumes apply_context [simp]: "⋀f e ls c rs t. (More f e ls c rs)⟨t⟩ = Fun f e (ls @ c⟨t⟩ # rs)"
begin

lemma is_subterm_obtain_context [elim]:
  assumes "t' ⊴ t"
  obtains c where "t = c⟨t'⟩"
  using assms 
proof (induction t' t arbitrary: thesis rule: is_subterm_eq.induct)
  case (subterm_refl t)

  then show ?case 
    by (metis apply_hole)
next
  case (subterm t' t t'')
 
  then obtain c where t': "t' = c⟨t''⟩" 
    by auto

  obtain ts1 ts2 where "subterms t = ts1 @ t' # ts2"
    by (meson split_list_first subterm.hyps(1))

  show ?case
    by (metis t' append_is_Nil_conv apply_context interpret_term is_var_subterms split_list_first
        subterm.hyps(1) subterm.prems)
qed

end

locale hole_position =
  smaller_subterms where subterms = subterms +
  "context" where apply_context = apply_context
for 
  subterms :: "'t ⇒ 't list" and
  apply_context :: "'c ⇒ 't ⇒ 't" +
fixes hole_position :: "'c ⇒ position"
assumes 
  subterm_at_hole_position [simp]: "⋀c t. c⟨t⟩ !⇩t hole_position c = t" and
  hole_position_in_positions [intro]: "⋀c t. hole_position c ∈ positions (c⟨t⟩)"

locale context_at = hole_position where apply_context = apply_context 
  for apply_context :: "'c ⇒ 't ⇒ 't" +
  fixes context_at :: "'t ⇒ position ⇒ 'c" (infixl ‹!⇩c› 64)
  assumes
    context_at_root [simp]: "t !⇩c [] = □" and
    context_at_hole [simp]: "⋀c t. c⟨t⟩ !⇩c (hole_position c) = c" and
    context_at_subterm_at [simp]: "⋀p t. p ∈ positions t ⟹ (t !⇩c p)⟨t !⇩t p⟩ = t"
begin

abbreviation replace_at (‹_⟦_ := _⟧› [70, 0, 50] 70) where
  "replace_at t p s ≡ (t !⇩c p)⟨s⟩"

lemma replace_at_hole [simp]: "c⟨t⟩⟦hole_position c := t'⟧ = c⟨t'⟩"
  by simp

lemma replace_at_id [simp]: "t⟦[] := t⟧ = t"
  by simp

end

locale replace_at_subterm =
  context_at + 
  term_interpretation +
  assumes
    replace_at_subterm [simp]: 
      "⋀f e ts i p t. Fun f e ts⟦i # p := t⟧ =
        Fun f e (take i ts @ ts ! i⟦p := t⟧ # drop (Suc i) ts)"

end