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
  "GsG = s" |
  "(GMore f ss1 C ss2)sG = GFun f (ss1 @ CsG # ss2)"

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

lemma gctxt_eq [simp]: "(CsG = CtG) = (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_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" "(∘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)tG = CDtGG"
  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 = Cl  ground_ctxt C"
  "term_of_gterm s = Cl  ground l"
  by (metis ground_ctxt_apply ground_term_of_gterm)+

lemma term_of_gterm_ctxt_subst_apply_ground [simp]:
  "term_of_gterm s = Cl  σ  x  vars_term l  ground (σ x)"
  by (meson ground_substD 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 = CtG"
  by (induct C) (auto simp: comp_def map_idI)

lemma ctxt_of_gctxt_apply_gterm:
  "gterm_of_term (ctxt_of_gctxt C)t = Cgterm_of_term tG"
  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)tG = Cterm_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 tG = Ct" using assms
  by (induct C) (auto simp: comp_def map_idI)

lemma term_of_gterm_ctxt_apply [simp]:
  "term_of_gterm s = Cl  (gctxt_of_ctxt C)gterm_of_term lG = 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 pG = 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]:
  "CsG = 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 CuG"
  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 CuG (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)uG 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)vG 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)vG 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)vG  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)vG  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)vG = {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 CsG = 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

end