Theory IsaFoR_Ground_Context

theory IsaFoR_Ground_Context
  imports
    Generic_Term_Context
    IsaFoR_Abstract_Context
    IsaFoR_Ground_Term
begin

type_synonym 'f gcontext = "('f, 'f gterm) actxt"

abbreviation apply_ground_context (‹_⟨_⟩⇩G› [1000, 0] 1000) where
  "c⟨t⟩⇩G ≡ GFun⟨c;t⟩"

fun context_at⇩G :: "'f gterm ⇒ pos ⇒ 'f gcontext" where
  "context_at⇩G t [] = □" |
  "context_at⇩G (GFun f ts) (i # ps) = More f (take i ts) (context_at⇩G (ts!i) ps) (drop (Suc i) ts)"

interpretation gcontext: term_context_interpretation where
  subterms = gargs and fun_sym = groot_sym and extra = "λ_. ()" and is_var = is_var and
  Fun = "λf _. GFun f" and
  hole = □ and apply_context = apply_ground_context and compose_context = "(∘⇩c)" and
  More = "λf _. More f" and fun_sym⇩c = fun_sym⇩c and extra⇩c = "λ_. ()" and subterms⇩l = subterms⇩l and
  subcontext = subcontext and subterms⇩r = subterms⇩r
proof unfold_locales
  fix c :: "'f gcontext" and t t' 
  assume "c⟨t⟩⇩G = c⟨t'⟩⇩G" 

  then show "t = t'"
    by (induction c) auto
next
  fix c :: "'f gcontext"

  show "c ≠ □ ⟷ (∃f e ls c' rs. c = More f ls c' rs)"
    by (metis actxt.distinct(1) actxt.exhaust)
qed (simp_all add: intp_actxt_compose)

interpretation gcontext: replace_at_subterm where  
  subterms = gargs and fun_sym = groot_sym and extra = "λ_. ()" and is_var = is_var and
  Fun = "λf _. GFun f" and size = size and
  hole = □ and apply_context = apply_ground_context and compose_context = "(∘⇩c)" and
  hole_position = hole_pos and context_at = context_at⇩G
proof unfold_locales
  fix c :: "'f gcontext" and t

  show "gterm.subterm_at c⟨t⟩⇩G (hole_pos c) = t"
    by (induction c) auto

  show "hole_pos c ∈ gterm.positions c⟨t⟩⇩G"
    by (induction c) auto

  show "context_at⇩G c⟨t⟩⇩G (hole_pos c) = c"
    by (induction c) auto
next
  fix p and t :: "'f gterm"
  assume "p ∈ gterm.positions t"

  then show "(context_at⇩G t p)⟨gterm.subterm_at t p⟩⇩G = t"
    by (induction t p rule: context_at⇩G.induct) (auto simp: Cons_nth_drop_Suc)
qed auto

end