Theory Superposition_Calculus.Ground_Ctxt_Extra

theory Ground_Ctxt_Extra
  imports "Regular_Tree_Relations.Ground_Ctxt"
begin

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

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

lemma gctxt_ident_iff_eq_GHole[simp]: "ctxt⟨t⟩⇩G = t ⟷ ctxt = □⇩G"
proof (rule iffI)
  assume "ctxt⟨t⟩⇩G = t"
  hence "size (ctxt⟨t⟩⇩G) = size t"
    by argo
  thus "ctxt = □⇩G"
    using lt_size_gctxt[of ctxt t]
    by linarith
next
  show "ctxt = □⇩G ⟹ ctxt⟨t⟩⇩G = t"
    by simp
qed

end