Theory Regular_Tree_Relations.Ground_Closure

theory Ground_Closure
  imports Ground_Terms
begin

subsubsection ‹Multihole context closure›

text ‹Computing the multihole context closure of a given relation›
inductive_set gmctxt_cl :: "('f × nat) set  'f gterm rel  'f gterm rel" for   where
  base [intro]: "(s, t)    (s, t)  gmctxt_cl  "
| step [intro]: "length ss = length ts  ( i < length ts. (ss ! i, ts ! i)  gmctxt_cl  )  (f, length ss)   
    (GFun f ss, GFun f ts)  gmctxt_cl  "

lemma gmctxt_cl_idemp [simp]:
  "gmctxt_cl  (gmctxt_cl  ) = gmctxt_cl  "
proof -
  {fix s t assume "(s, t)  gmctxt_cl  (gmctxt_cl  )"
    then have "(s, t)  gmctxt_cl  "
      by (induct) (auto intro: gmctxt_cl.step)}
  then show ?thesis by auto
qed

lemma gmctxt_cl_refl:
  "funas_gterm t    (t, t)  gmctxt_cl  "
  by (induct t) (auto simp: SUP_le_iff intro!: gmctxt_cl.step)

lemma gmctxt_cl_swap:
  "gmctxt_cl  (prod.swap ` ) = prod.swap ` gmctxt_cl  " (is "?Ls = ?Rs")
proof -
  {fix s t assume "(s, t)  ?Ls" then have "(s, t)  ?Rs"
      by induct auto}
  moreover
  {fix s t assume "(s, t)  ?Rs"
    then have "(t, s)  gmctxt_cl  " by auto
    then have "(s, t)  ?Ls" by induct auto}
  ultimately show ?thesis by auto
qed

lemma gmctxt_cl_mono_funas:
  assumes "  𝒢" shows "gmctxt_cl    gmctxt_cl 𝒢 "
proof -
  {fix s t assume "(s, t)  gmctxt_cl  " then have "(s, t)  gmctxt_cl 𝒢 "
      by induct (auto simp: subsetD[OF assms])}
  then show ?thesis by auto
qed

lemma gmctxt_cl_mono_rel:
  assumes "𝒫  " shows "gmctxt_cl  𝒫  gmctxt_cl  "
proof -
  {fix s t assume "(s, t)  gmctxt_cl  𝒫" then have "(s, t)  gmctxt_cl  " using assms
      by induct auto}
  then show ?thesis by auto
qed

definition gcomp_rel :: "('f × nat) set  'f gterm rel  'f gterm rel  'f gterm rel" where
  "gcomp_rel  R S = (R O gmctxt_cl  S)  (gmctxt_cl  R O S)"

definition gtrancl_rel :: "('f × nat) set  'f gterm rel  'f gterm rel" where
  "gtrancl_rel   = (gmctxt_cl  )+ O  O (gmctxt_cl  )+"

lemma gcomp_rel:
  "gmctxt_cl  (gcomp_rel   𝒮) = gmctxt_cl   O gmctxt_cl  𝒮" (is "?Ls = ?Rs")
proof
  { fix s u assume "(s, u)  gmctxt_cl  ( O gmctxt_cl  𝒮  gmctxt_cl   O 𝒮)"
     then have "t. (s, t)  gmctxt_cl    (t, u)  gmctxt_cl  𝒮"
    proof (induct)
      case (step ss ts f)
      from Ex_list_of_length_P[of _ "λ u i. (ss ! i, u)  gmctxt_cl    (u, ts ! i)  gmctxt_cl  𝒮"]
      obtain us where l: "length us = length ts" and
        inv: " i < length ts. (ss ! i, us ! i)  gmctxt_cl    (us ! i, ts ! i)  gmctxt_cl  𝒮"
        using step(2, 3) by blast
      then show ?case using step(1, 3)
        by (intro exI[of _ "GFun f us"]) auto
    qed auto}
  then show "?Ls  ?Rs" unfolding gcomp_rel_def
    by auto
next
  {fix s t u assume "(s, t)  gmctxt_cl  " "(t, u)  gmctxt_cl  𝒮"
    then have "(s, u)  gmctxt_cl  ( O gmctxt_cl  𝒮  gmctxt_cl   O 𝒮)"
    proof (induct arbitrary: u rule: gmctxt_cl.induct)
      case (step ss ts f)
      then show ?case
      proof (cases "(GFun f ts, u)  𝒮")
        case True
        then have "(GFun f ss, u)  gmctxt_cl   O 𝒮" using gmctxt_cl.step[OF step(1) _ step(3)] step(2)
          by auto
        then show ?thesis by auto
      next
        case False
        then obtain us where u[simp]: "u = GFun f us" and l: "length ts = length us"
          using step(4) by (cases u) (auto elim: gmctxt_cl.cases)
        have "i < length us 
         (ss ! i, us ! i)  gmctxt_cl  ( O gmctxt_cl  𝒮  gmctxt_cl   O 𝒮)" for i
          using step(1, 2, 4) False by (auto elim: gmctxt_cl.cases)
        then show ?thesis using l step(1, 3)
          by auto
      qed
    qed auto}
  then show "?Rs  ?Ls"
    by (auto simp: gcomp_rel_def)
qed

subsubsection ‹Signature closed property›

definition all_ctxt_closed :: "('f × nat) set  'f gterm rel  bool" where
  "all_ctxt_closed F r  ( f ts ss. (f, length ss)  F  length ss = length ts 
    (i. i < length ts  (ss ! i, ts ! i)  r) 
    (GFun f ss, GFun f ts)  r)"

lemma all_ctxt_closedI:
  assumes " f ss ts. (f, length ss)    length ss = length ts 
     ( i < length ts. (ss ! i, ts ! i)  r)  (GFun f ss, GFun f ts)  r"
  shows "all_ctxt_closed  r" using assms
  unfolding all_ctxt_closed_def by auto

lemma all_ctxt_closedD:
  "all_ctxt_closed F r  (f, length ss)  F  length ss = length ts 
    ( i < length ts. (ss ! i, ts ! i)  r)  (GFun f ss, GFun f ts)  r"
  by (auto simp: all_ctxt_closed_def)

lemma all_ctxt_closed_refl_on:
  assumes "all_ctxt_closed  r" "s  𝒯G "
  shows "(s, s)  r" using assms(2)
  by (induct) (auto simp: all_ctxt_closedD[OF assms(1)])

lemma gmctxt_cl_is_all_ctxt_closed [simp]:
  "all_ctxt_closed  (gmctxt_cl  )"
  unfolding all_ctxt_closed_def
  by auto

lemma all_ctxt_closed_gmctxt_cl_idem [simp]:
  assumes "all_ctxt_closed  "
  shows "gmctxt_cl   = "
proof -
  {fix s t assume "(s, t)  gmctxt_cl  " then have "(s, t)  "
    proof (induct)
      case (step ss ts f)
      show ?case using step(2) all_ctxt_closedD[OF assms step(3, 1)]
        by auto
    qed auto}
  then show ?thesis by auto
qed


subsubsection ‹Transitive closure preserves @{const all_ctxt_closed}

text ‹induction scheme for transitive closures of lists›

inductive_set trancl_list for  where
  base[intro, Pure.intro] : "length xs = length ys 
      ( i < length ys. (xs ! i, ys ! i)  )  (xs, ys)  trancl_list "
| list_trancl [Pure.intro]: "(xs, ys)  trancl_list   i < length ys  (ys ! i, z)   
    (xs, ys[i := z])  trancl_list "

lemma trancl_list_appendI [simp, intro]:
  "(xs, ys)  trancl_list   (x, y)    (x # xs, y # ys)  trancl_list "
proof (induct rule: trancl_list.induct)
  case (base xs ys)
  then show ?case using less_Suc_eq_0_disj
    by (intro trancl_list.base) auto
next
  case (list_trancl xs ys i z)
  from list_trancl(3) have *: "y # ys[i := z] = (y # ys)[Suc i := z]" by auto
  show ?case using list_trancl unfolding *
    by (intro trancl_list.list_trancl) auto
qed

lemma trancl_list_append_tranclI [intro]:
  "(x, y)  +  (xs, ys)  trancl_list   (x # xs, y # ys)  trancl_list "
proof (induct rule: trancl.induct)
  case (trancl_into_trancl a b c)
  then have "(a # xs, b # ys)  trancl_list " by auto
  from trancl_list.list_trancl[OF this, of 0 c]
  show ?case using trancl_into_trancl(3)
    by auto
qed auto

lemma trancl_list_conv:
  "(xs, ys)  trancl_list   length xs = length ys  ( i < length ys. (xs ! i, ys ! i)  +)" (is "?Ls  ?Rs")
proof
  assume "?Ls" then show ?Rs
  proof (induct)
    case (list_trancl xs ys i z)
    then show ?case
      by auto (metis nth_list_update trancl.trancl_into_trancl)
  qed auto
next
  assume ?Rs then show ?Ls
  proof (induct ys arbitrary: xs)
    case Nil
    then show ?case by (cases xs) auto
  next
    case (Cons y ys)
    from Cons(2) obtain x xs' where *: "xs = x # xs'" and
      inv: "(x, y)  +"
      by (cases xs) auto
    show ?case using Cons(1)[of "tl xs"] Cons(2) unfolding *
      by (intro trancl_list_append_tranclI[OF inv]) force
  qed
qed

lemma trancl_list_induct [consumes 2, case_names base step]:
  assumes "length ss = length ts" " i < length ts. (ss ! i, ts ! i)  +"
    and "xs ys. length xs = length ys   i < length ys. (xs ! i, ys ! i)    P xs ys"
    and "xs ys i z. length xs = length ys   i < length ys. (xs ! i, ys ! i)  +  P xs ys
       i < length ys  (ys ! i, z)    P xs (ys[i := z])"
  shows "P ss ts" using assms
  by (intro trancl_list.induct[of ss ts  P]) (auto simp: trancl_list_conv)

lemma trancl_list_all_step_induct [consumes 2, case_names base step]:
  assumes "length ss = length ts" " i < length ts. (ss ! i, ts ! i)  +"
    and base: "xs ys. length xs = length ys   i < length ys. (xs ! i, ys ! i)    P xs ys"
    and steps: "xs ys zs. length xs = length ys  length ys = length zs 
        i < length zs. (xs ! i, ys ! i)  +   i < length zs. (ys ! i, zs ! i)    ys ! i = zs ! i 
       P xs ys  P xs zs"
  shows "P ss ts" using assms(1, 2)
proof (induct rule: trancl_list_induct)
case (step xs ys i z)
  then show ?case
    by (intro steps[of xs ys "ys[i := z]"])
       (auto simp: nth_list_update)
qed (auto simp: base)

lemma all_ctxt_closed_trancl:
  assumes  "all_ctxt_closed  " "  𝒯G  × 𝒯G "
  shows "all_ctxt_closed  (+)"
proof -
  {fix f ss ts assume sig: "(f, length ss)  " and
      steps: "length ss = length ts" "i<length ts. (ss ! i, ts ! i)  +"
    have "(GFun f ss, GFun f ts)  +" using steps sig
    proof (induct rule: trancl_list_induct)
      case (base ss ts)
      then show ?case using all_ctxt_closedD[OF assms(1) base(3, 1, 2)]
        by auto
    next
      case (step ss ts i t')
      from step(2) have "j < length ts  ts ! j  𝒯G " for j using assms(2)
        by (metis (no_types, lifting) SigmaD2 subset_iff trancl.simps)
      from this[THEN all_ctxt_closed_refl_on[OF assms(1)]]
      have "(GFun f ts, GFun f (ts[i := t']))  " using step(1, 4-)
        by (intro all_ctxt_closedD[OF assms(1)]) (auto simp: nth_list_update)
      then show ?case using step(3, 6)
        by auto
    qed}
  then show ?thesis by (intro all_ctxt_closedI)
qed

end