Theory Abstract_Context

theory Abstract_Context
  imports Generic_Term_Context
begin

datatype ('f, extra_set: 'e, term_set: 't) "context" =
  Hole (‹□›) |
  More
    (fun_sym: 'f) (extra: 'e) (subterms⇩l: "'t list") 
    (subcontext: "('f, 'e, 't) context") (subterms⇩r: "'t list")

primrec compose_context (infixl ‹∘⇩c› 75) where
  "Hole ∘⇩c c = c"
| "More f e ls C rs ∘⇩c D = More f e ls (C ∘⇩c D) rs"

fun hole_position :: "('f, 'e, 't) context ⇒ position" where
  "hole_position □ = []"
| "hole_position (More _  _ ss D _) = length ss # hole_position D"

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

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

locale abstract_context = 
  term_interpretation where Fun = Fun +
  smaller_subterms
for Fun :: "'f ⇒ 'e ⇒ 't list ⇒ 't"
begin

primrec apply_context (‹_⟨_⟩› [1000, 0] 1000) where
  "□⟨t⟩ = t"
| "(More f e ls C rs)⟨t⟩ = Fun f e (ls @ C⟨t⟩ # rs)"

lemma size_apply_context: "c ≠ □ ⟹ size t < size c⟨t⟩"
proof (induction c)
  case Hole
  then show ?case
    by argo
next
  case (More f e ls c rs)

  moreover have "size c⟨t⟩ < size (Fun f e (ls @ c⟨t⟩ # rs))"
    by (simp add: subterms_smaller)

  ultimately show ?case 
    by fastforce
qed

primrec context_at :: "'t ⇒ position ⇒ ('f, 'e, 't) context" (infixl ‹!⇩c› 64) where
  "t !⇩c [] = □"
| "t !⇩c i # ps =
   More
    (fun_sym t)
    (extra t)
    (take i (subterms t)) (subterms t ! i !⇩c ps)
    (drop (Suc i) (subterms t))"

sublocale "context" where
  hole = □ and 
  apply_context = apply_context and 
  compose_context = compose_context
proof unfold_locales
  fix c c' t

  show "(c ∘⇩c c')⟨t⟩ = c⟨c'⟨t⟩⟩"
    by (induction c) auto
next
  fix t

  show "□⟨t⟩ = t"
    by simp
next
  fix c t t'
  assume "c⟨t⟩ = c⟨t'⟩"

  then show "t = t'"
  proof(induction c)
    case Hole
    then show ?case
      by simp
  next
    case (More f e ls c rs)
    then show ?case 
      by (metis apply_context.simps(2) nth_append_length subterms)
  qed
next
  fix c :: "('f, 'extra, 't) context"
  show "c ∘⇩c □ = c"
    by (induction c) auto
qed auto

sublocale term_context_interpretation where
  hole = □ and apply_context = apply_context and compose_context = "(∘⇩c)" and
  More = More and fun_sym⇩c = context.fun_sym and extra⇩c = context.extra and subterms⇩l = subterms⇩l and
  subcontext = subcontext and subterms⇩r = subterms⇩r 
proof unfold_locales
  fix c :: "('f, 'e, 't) context"

  show "c ≠ □ ⟷ (∃f e ls c' rs. c = More f e ls c' rs)"
    by (metis context.discI context.exhaust_sel)
qed auto

sublocale replace_at_subterm where  
  hole = □ and apply_context = apply_context and compose_context = "(∘⇩c)" and
  hole_position = hole_position and context_at = context_at
proof unfold_locales
  fix c :: "('f, 'e, 't) context" and t

  show "c⟨t⟩ !⇩t hole_position c = t"
    by (induction c) auto

  show "hole_position c ∈ positions c⟨t⟩"
    by (induction c) (auto simp: term_destruct)

  show "c⟨t⟩ !⇩c hole_position c = c"
    by (induction c) auto
next
  fix p and t
  assume "p ∈ positions t"

  then show "(t !⇩c p)⟨t !⇩t p⟩ = t"
  by (induction p arbitrary: t) (auto simp: Cons_nth_drop_Suc)
qed auto

lemma context_is_subterm [intro]:
  assumes "t = c⟨t'⟩" shows "t' ⊴ t"
  using assms
  by (induction c arbitrary: t) auto

lemma is_subterm_iff_exists_context: "t' ⊴ t ⟷ (∃c. t = c⟨t'⟩)"
  by auto

end

end