# Theory Regular_Tree_Relations.Ground_Ctxt

```theory Ground_Ctxt
imports Ground_Terms
begin

subsubsection ‹Ground context›

datatype (gfuns_ctxt: 'f) gctxt =
GHole ("□⇩G") | GMore 'f "'f gterm list" "'f gctxt" "'f gterm list"
declare gctxt.map_comp[simp]

fun gctxt_apply_term :: "'f gctxt ⇒ 'f gterm ⇒ 'f gterm" ("_⟨_⟩⇩G" [1000, 0] 1000) where
"□⇩G⟨s⟩⇩G = s" |
"(GMore f ss1 C ss2)⟨s⟩⇩G = GFun f (ss1 @ C⟨s⟩⇩G # ss2)"

fun hole_gpos where
"hole_gpos □⇩G = []" |
"hole_gpos (GMore f ss1 C ss2) = length ss1 # hole_gpos C"

lemma gctxt_eq [simp]: "(C⟨s⟩⇩G = C⟨t⟩⇩G) = (s = t)"
by (induct C) auto

fun gctxt_compose :: "'f gctxt ⇒ 'f gctxt ⇒ 'f gctxt" (infixl "∘⇩G⇩c" 75) where
"□⇩G ∘⇩G⇩c D = D" |
"(GMore f ss1 C ss2) ∘⇩G⇩c D = GMore f ss1 (C ∘⇩G⇩c D) ss2"

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

interpretation ctxt_monoid_mult: monoid_mult "□⇩G" "(∘⇩G⇩c)"
proof
fix C D E :: "'f gctxt"
show "C ∘⇩G⇩c D ∘⇩G⇩c E = C ∘⇩G⇩c (D ∘⇩G⇩c E)" by (induct C) simp_all
show "□⇩G ∘⇩G⇩c C = C" by simp
show "C ∘⇩G⇩c □⇩G = C" by (induct C) simp_all
qed

instantiation gctxt :: (type) monoid_mult
begin
definition [simp]: "1 = □⇩G"
definition [simp]: "(*) = (∘⇩G⇩c)"
instance by (intro_classes) (simp_all add: ac_simps)
end

lemma ctxt_ctxt_compose [simp]: "(C ∘⇩G⇩c D)⟨t⟩⇩G = C⟨D⟨t⟩⇩G⟩⇩G"
by (induct C) simp_all

lemmas ctxt_ctxt = ctxt_ctxt_compose [symmetric]

fun ctxt_of_gctxt where
"ctxt_of_gctxt □⇩G = □"
|  "ctxt_of_gctxt (GMore f ss C ts) = More f (map term_of_gterm ss) (ctxt_of_gctxt C) (map term_of_gterm ts)"

fun gctxt_of_ctxt where
"gctxt_of_ctxt □ = □⇩G"
|  "gctxt_of_ctxt (More f ss C ts) = GMore f (map gterm_of_term ss) (gctxt_of_ctxt C) (map gterm_of_term ts)"

lemma ground_ctxt_of_gctxt [simp]:
"ground_ctxt (ctxt_of_gctxt s)"
by (induct s) auto

lemma ground_ctxt_of_gctxt' [simp]:
"ctxt_of_gctxt C = More f ss D ts ⟹ ground_ctxt (More f ss D ts)"
by (induct C) auto

lemma ctxt_of_gctxt_inv [simp]:
"gctxt_of_ctxt (ctxt_of_gctxt t) = t"
by (induct t) (auto intro!: nth_equalityI)

lemma inj_ctxt_of_gctxt: "inj_on ctxt_of_gctxt X"
by (metis inj_on_def ctxt_of_gctxt_inv)

lemma gctxt_of_ctxt_inv [simp]:
"ground_ctxt C ⟹ ctxt_of_gctxt (gctxt_of_ctxt C) = C"
by (induct C) (auto 0 0 intro!: nth_equalityI)

lemma map_ctxt_of_gctxt [simp]:
"map_ctxt f g (ctxt_of_gctxt C) = ctxt_of_gctxt (map_gctxt f C)"
by (induct C) auto

lemma map_gctxt_of_ctxt [simp]:
"ground_ctxt C ⟹ gctxt_of_ctxt (map_ctxt f g C) = map_gctxt f (gctxt_of_ctxt C)"
by (induct C) auto

lemma map_gctxt_nempty [simp]:
"C ≠ □⇩G ⟹ map_gctxt f C ≠ □⇩G"
by (cases C) auto

lemma gctxt_set_funs_ctxt:
"gfuns_ctxt C = funs_ctxt (ctxt_of_gctxt C)"
using gterm_set_gterm_funs_terms
by (induct C) fastforce+

lemma ctxt_set_funs_gctxt:
assumes "ground_ctxt C"
shows "gfuns_ctxt (gctxt_of_ctxt C) = funs_ctxt C"
using assms term_set_gterm_funs_terms
by (induct C) fastforce+

lemma vars_ctxt_of_gctxt [simp]:
"vars_ctxt (ctxt_of_gctxt C) = {}"
by (induct C) auto

lemma vars_ctxt_of_gctxt_subseteq [simp]:
"vars_ctxt (ctxt_of_gctxt C) ⊆ Q ⟷ True"
by auto

lemma term_of_gterm_ctxt_apply_ground [simp]:
"term_of_gterm s = C⟨l⟩ ⟹ ground_ctxt C"
"term_of_gterm s = C⟨l⟩ ⟹ ground l"
by (metis ground_ctxt_apply ground_term_of_gterm)+

lemma term_of_gterm_ctxt_subst_apply_ground [simp]:
"term_of_gterm s = C⟨l ⋅ σ⟩ ⟹ x ∈ vars_term l ⟹ ground (σ x)"
by (meson ground_substD term_of_gterm_ctxt_apply_ground(2))

lemma gctxt_compose_HoleE:
"C ∘⇩G⇩c D = □⇩G ⟹ C = □⇩G"
"C ∘⇩G⇩c D = □⇩G ⟹ D = □⇩G"
by (cases C; cases D, auto)+

― ‹Relations between ground contexts and contexts›

lemma nempty_ground_ctxt_gctxt [simp]:
"C ≠ □ ⟹ ground_ctxt C ⟹ gctxt_of_ctxt C ≠ □⇩G"
by (induct C) auto

lemma ctxt_of_gctxt_apply [simp]:
"gterm_of_term (ctxt_of_gctxt C)⟨term_of_gterm t⟩ = C⟨t⟩⇩G"
by (induct C) (auto simp: comp_def map_idI)

lemma ctxt_of_gctxt_apply_gterm:
"gterm_of_term (ctxt_of_gctxt C)⟨t⟩ = C⟨gterm_of_term t⟩⇩G"
by (induct C) (auto simp: comp_def map_idI)

lemma ground_gctxt_of_ctxt_apply_gterm:
assumes "ground_ctxt C"
shows "term_of_gterm (gctxt_of_ctxt C)⟨t⟩⇩G = C⟨term_of_gterm t⟩" using assms
by (induct C) (auto simp: comp_def map_idI)

lemma ground_gctxt_of_ctxt_apply [simp]:
assumes "ground_ctxt C" "ground t"
shows "term_of_gterm (gctxt_of_ctxt C)⟨gterm_of_term t⟩⇩G = C⟨t⟩" using assms
by (induct C) (auto simp: comp_def map_idI)

lemma term_of_gterm_ctxt_apply [simp]:
"term_of_gterm s = C⟨l⟩ ⟹ (gctxt_of_ctxt C)⟨gterm_of_term l⟩⇩G = s"
by (metis ctxt_of_gctxt_apply_gterm gctxt_of_ctxt_inv term_of_gterm_ctxt_apply_ground(1) term_of_gterm_inv)

lemma gctxt_apply_inj_term: "inj (gctxt_apply_term C)"
by (auto simp: inj_on_def)

lemma gctxt_apply_inj_on_term: "inj_on (gctxt_apply_term C) S"
by (auto simp: inj_on_def)

lemma ctxt_of_pos_gterm [simp]:
"p ∈ gposs t ⟹ ctxt_at_pos (term_of_gterm t) p = ctxt_of_gctxt (gctxt_at_pos t p)"
by (induct t arbitrary: p) (auto simp add: take_map drop_map)

lemma gctxt_of_gpos_gterm_gsubt_at_to_gterm [simp]:
assumes "p ∈ gposs t"
shows "(gctxt_at_pos t p)⟨gsubt_at t p⟩⇩G = t" using assms
by (induct t arbitrary: p) (auto simp: comp_def min_def nth_append_Cons intro!: nth_equalityI)

text ‹The position of the hole in a context is uniquely determined›
fun ghole_pos :: "'f gctxt ⇒ pos" where
"ghole_pos □⇩G = []" |
"ghole_pos (GMore f ss D ts) = length ss # ghole_pos D"

lemma ghole_pos_gctxt_at_pos [simp]:
"p ∈ gposs t ⟹ ghole_pos (gctxt_at_pos t p) = p"
by (induct t arbitrary: p) auto

lemma ghole_pos_id_ctxt [simp]:
"C⟨s⟩⇩G = t ⟹ gctxt_at_pos t (ghole_pos C) = C"
by (induct C arbitrary: t) auto

lemma ghole_pos_in_apply:
"ghole_pos C = p ⟹ p ∈ gposs C⟨u⟩⇩G"
by (induct C arbitrary: p) (auto simp: nth_append)

lemma ground_hole_pos_to_ghole:
"ground_ctxt C ⟹ ghole_pos (gctxt_of_ctxt C) = hole_pos C"
by (induct C) auto

lemma gsubst_at_gctxt_at_eq_gtermD:
assumes "s = t" "p ∈ gposs t"
shows "gsubt_at s p = gsubt_at t p ∧ gctxt_at_pos s p = gctxt_at_pos t p" using assms
by auto

lemma gsubst_at_gctxt_at_eq_gtermI:
assumes "p ∈ gposs s" "p ∈ gposs t"
and "gsubt_at s p = gsubt_at t p"
and "gctxt_at_pos s p = gctxt_at_pos t p"
shows "s = t" using assms
using gctxt_of_gpos_gterm_gsubt_at_to_gterm by force

lemma gsubt_at_gctxt_apply_ghole [simp]:
"gsubt_at C⟨u⟩⇩G (ghole_pos C) = u"
by (induct C) auto

lemma gctxt_at_pos_gsubt_at_pos [simp]:
"p ∈ gposs t ⟹ gsubt_at (gctxt_at_pos t p)⟨u⟩⇩G p = u"
proof (induct p arbitrary: t)
case (Cons i p)
then show ?case using id_take_nth_drop
by (cases t) (auto simp: nth_append)
qed auto

lemma gfun_at_gctxt_at_pos_not_after:
assumes "p ∈ gposs t" "q ∈ gposs t" "¬ (p ≤⇩p q)"
shows "gfun_at (gctxt_at_pos t p)⟨v⟩⇩G q = gfun_at t q" using assms
proof (induct q arbitrary: p t)
case Nil
then show ?case
by (cases p; cases t) auto
next
case (Cons i q)
from Cons(4) obtain j r where [simp]: "p = j # r" by (cases p) auto
from Cons(4) have "j = i ⟹ ¬ (r ≤⇩p q)" by auto
from this Cons(2-) Cons(1)[of r "gargs t ! j"]
have "j = i ⟹ gfun_at (gctxt_at_pos (gargs t ! j) r)⟨v⟩⇩G q = gfun_at (gargs t ! j) q"
by (cases t) auto
then show ?case using Cons(2, 3)
by (cases t) (auto simp: nth_append_Cons min_def)
qed

lemma gpos_less_eq_append [simp]: "p ≤⇩p (p @ q)"
unfolding position_less_eq_def
by blast

lemma gposs_ConsE [elim]:
assumes "i # p ∈ gposs t"
obtains f ts where "t = GFun f ts" "ts ≠ []" "i < length ts" "p ∈ gposs (ts ! i)" using assms
by (cases t) force+

lemma gposs_gctxt_at_pos_not_after:
assumes "p ∈ gposs t" "q ∈ gposs t" "¬ (p ≤⇩p q)"
shows "q ∈ gposs (gctxt_at_pos t p)⟨v⟩⇩G ⟷ q ∈ gposs t" using assms
proof (induct q arbitrary: p t)
case Nil then show ?case
by (cases p; cases t) auto
next
case (Cons i q)
from Cons(4) obtain j r where [simp]: "p = j # r" by (cases p) auto
from Cons(4) have "j = i ⟹ ¬ (r ≤⇩p q)" by auto
from this Cons(2-) Cons(1)[of r "gargs t ! j"]
have "j = i ⟹ q ∈ gposs (gctxt_at_pos (gargs t ! j) r)⟨v⟩⇩G ⟷ q ∈ gposs (gargs t ! j)"
by (cases t) auto
then show ?case using Cons(2, 3)
by (cases t) (auto simp: nth_append_Cons min_def)
qed

lemma gposs_gctxt_at_pos:
"p ∈ gposs t ⟹ gposs (gctxt_at_pos t p)⟨v⟩⇩G = {q. q ∈ gposs t ∧ ¬ (p ≤⇩p q)} ∪ (@) p ` gposs v"
proof (induct p arbitrary: t)
case (Cons i p)
show ?case using Cons(1)[of "gargs t ! i"] Cons(2) gposs_gctxt_at_pos_not_after[OF Cons(2)]
by (auto simp: min_def nth_append_Cons split: if_splits elim!: gposs_ConsE)
qed auto

lemma eq_gctxt_at_pos:
assumes "p ∈ gposs s" "p ∈ gposs t"
and "⋀ q. ¬ (p ≤⇩p q) ⟹ q ∈ gposs s ⟷ q ∈ gposs t"
and "(⋀ q. q ∈ gposs s ⟹ ¬ (p ≤⇩p q) ⟹ gfun_at s q = gfun_at t q)"
shows "gctxt_at_pos s p = gctxt_at_pos t p" using assms(1, 2)
using arg_cong[where ?f = gctxt_of_ctxt, OF eq_ctxt_at_pos_by_poss, of _ "term_of_gterm s :: (_, unit) term"
"term_of_gterm t :: (_, unit) term" for s t, unfolded poss_gposs_conv fun_at_gfun_at_conv ctxt_of_pos_gterm,
OF assms]
by simp

text ‹Signature of a ground context›

fun funas_gctxt :: "'f gctxt ⇒ ('f × nat) set" where
"funas_gctxt GHole = {}" |
"funas_gctxt (GMore f ss1 D ss2) = {(f, Suc (length (ss1 @ ss2)))}
∪ funas_gctxt D ∪ ⋃(set (map funas_gterm (ss1 @ ss2)))"

lemma funas_gctxt_of_ctxt [simp]:
"ground_ctxt C ⟹ funas_gctxt (gctxt_of_ctxt C) = funas_ctxt C"
by (induct C) (auto simp: funas_gterm_gterm_of_term)

lemma funas_ctxt_of_gctxt_conv [simp]:
"funas_ctxt (ctxt_of_gctxt C) = funas_gctxt C"
by (induct C) (auto simp flip: funas_gterm_gterm_of_term)

lemma inj_gctxt_of_ctxt_on_ground:
"inj_on gctxt_of_ctxt (Collect ground_ctxt)"
using gctxt_of_ctxt_inv by (fastforce simp: inj_on_def)

lemma funas_gterm_ctxt_apply [simp]:
"funas_gterm C⟨s⟩⇩G = funas_gctxt C ∪ funas_gterm s"
by (induct C) auto

lemma funas_gctxt_compose [simp]:
"funas_gctxt (C ∘⇩G⇩c D) = funas_gctxt C ∪ funas_gctxt D"
by (induct C arbitrary: D) auto

end```