Theory Ground_Context

theory Ground_Context
  imports Ground_Term_Extra
begin

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

abbreviation (input) GHole (‹□⇩G›) where
  "□⇩G ≡ □"

abbreviation ctxt_apply_gterm (‹_⟨_⟩⇩G› [1000, 0] 1000) where
  "C⟨s⟩⇩G ≡ GFun⟨C;s⟩"

lemma le_size_gctxt: "size t ≤ size (c⟨t⟩⇩G)"
  by (induction c) simp_all

lemma lt_size_gctxt: "c ≠ □ ⟹ size t < size c⟨t⟩⇩G"
  by (induction c) force+

lemma gctxt_ident_iff_eq_GHole[simp]: "c⟨t⟩⇩G = t ⟷ c = □"
proof (rule iffI)
  assume "c⟨t⟩⇩G = t"

  hence "size (c⟨t⟩⇩G) = size t"
    by argo

  thus "c = □"
    using lt_size_gctxt[of c t]
    by linarith
next
  show "c = □ ⟹ c⟨t⟩⇩G = t"
    by simp
qed

end