Theory First_Order_Clause.Generic_Context

theory Generic_Context
  imports Context_Notation
begin

locale "context" =
  context_notation +
  assumes
    compose_context_iff [simp]: "⋀(c :: 'c) c' (t :: 't). (c ∘⇩c c')⟨t⟩ = c⟨c'⟨t⟩⟩" and
    compose_hole [simp]: "⋀c. □ ∘⇩c c = c" "⋀c. c ∘⇩c □ = c" and
    apply_hole [simp]: "⋀t. □⟨t⟩ = t" and
    apply_context_eq: "⋀c t t'. c⟨t⟩ = c⟨t'⟩ ⟹ t = t'"

locale context_interpretation =
  "context" where apply_context = apply_context 
for apply_context :: "'c ⇒ 't ⇒ 't" +
fixes 
  More :: "'f ⇒ 'e ⇒ 't list ⇒ 'c ⇒ 't list ⇒ 'c" and
  fun_sym :: "'c ⇒ 'f" and 
  extra :: "'c ⇒ 'e" and
  subterms⇩l :: "'c ⇒ 't list" and
  subcontext :: "'c ⇒ 'c" and
  subterms⇩r :: "'c ⇒ 't list"
assumes
  context_fun_sym [simp]: "⋀f e ls c rs. fun_sym (More f e ls c rs) = f" and
  context_extra [simp]: "⋀f e ls c rs. extra (More f e ls c rs) = e" and
  subterms⇩l [simp]: "⋀f e ls c rs. subterms⇩l (More f e ls c rs) = ls" and
  subcontext [simp]: "⋀f e ls c rs. subcontext (More f e ls c rs) = c" and
  subterms⇩r [simp]: "⋀f e ls c rs. subterms⇩r (More f e ls c rs) = rs" and
  context_destruct: "⋀c. c ≠ □ ⟷ (∃f e ls c' rs. c = More f e ls c' rs)" and
  context_inject [intro]: 
    "More f⇩1 e⇩1 ls⇩1 c⇩1' rs⇩1 = More f⇩2 e⇩2 ls⇩2 c⇩2' rs⇩2 ⟹ 
      f⇩1 = f⇩2 ∧ e⇩1 = e⇩2 ∧ ls⇩1 = ls⇩2 ∧ c⇩1' = c⇩2' ∧ rs⇩1 = rs⇩2" and
  compose_context [simp]: "More f e ls c rs ∘⇩c c' = More f e ls (c ∘⇩c c') rs"
begin

lemma interpretation_not_hole [intro]: "More f e ls c' rs ≠ □"
  using context_destruct
  by fast

end

locale smaller_subcontext =
  fixes hole :: 'c and size :: "'c ⇒ nat" and subcontext :: "'c ⇒ 'c"
  assumes subcontext_smaller: "⋀c. c ≠ hole ⟹ size (subcontext c) < size c"

end