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