Theory Ground_ctxt

theory Ground_ctxt
imports Ground_Terms Term_Rewriting
theory Ground_ctxt
  imports TRS.Term_More Ground_Terms TRS.Term_Rewriting
begin

subsection ‹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)"

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 "∘Gc" 75) where
  "□G ∘Gc D = D" |
  "(GMore f ss1 C ss2) ∘Gc D = GMore f ss1 (C ∘Gc D) ss2"

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

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

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

lemma ctxt_ctxt_compose [simp]: "(C ∘Gc 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_subst term_of_gterm_ctxt_apply_ground(2))



lemma gctxt_compose_HoleE:
 "C ∘Gc D = □G ⟹ C = □G"
 "C ∘Gc 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 gsubt_at_to_gctxt:
  "p ∈ gposs s ⟹ ∃ C u. gsubt_at s p = u ∧ C⟨u⟩G = s"
  by auto (metis gsubt_at_to_subt_at subt_at_imp_ctxt term_of_gterm_ctxt_apply)

lemma ctxt_of_pos_gterm [simp]:
  "p ∈ gposs t ⟹ ctxt_of_pos_term p (term_of_gterm t) = ctxt_of_gctxt (gctxt_of_pos_gterm p t)"
  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_of_pos_gterm p t)⟨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_of_pos_gterm [simp]:
  "p ∈ gposs t ⟹ ghole_pos (gctxt_of_pos_gterm p t) = p"
  by (induct t arbitrary: p) auto

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


text ‹Signature of a ground context›

fun funas_gctxt :: "'f gctxt ⇒ 'f sig" 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 ∘Gc D) = funas_gctxt C ∪ funas_gctxt D"
  by (induct C arbitrary: D) auto

interpretation gctxt: rel_closure "gctxt_apply_term" "□G" "(∘Gc)" by (standard) auto

end