# Theory Terms_Positions

section â¹Preliminariesâº
theory Terms_Positions
imports Regular_Tree_Relations.Ground_Terms
begin

subsection â¹Additional operations on terms and positionsâº

subsubsection â¹Linearityâº
fun linear_term :: "('f, 'v) term â bool" where
"linear_term (Var _) = True" |
"linear_term (Fun _ ts) = (is_partition (map vars_term ts) â§ (âtâset ts. linear_term t))"
abbreviation "linear_sys â â¡ â (l, r) â â. linear_term l â§ linear_term r"

subsubsection â¹Positions induced by contexts, by variables and by given subtermsâº

definition "possc C = {p | p t. p â poss Câ¨tâ©}"
definition "varposs s = {p | p. p â poss s â§ is_Var (s |_ p)}"
definition "poss_of_term u t = {p. p â poss t â§ t |_ p = u}"

subsubsection â¹Replacing functions symbols that aren't specified in the signature by variablesâº

definition "funas_rel â = (â (l, r) â â. funas_term l âª funas_term r)"

fun term_to_sig where
"term_to_sig â± v (Var x) = Var x"
| "term_to_sig â± v (Fun f ts) =
(if (f, length ts) â â± then Fun f (map (term_to_sig â± v) ts) else Var v)"

fun ctxt_well_def_hole_path where
"ctxt_well_def_hole_path â± Hole â· True"
| "ctxt_well_def_hole_path â± (More f ss C ts) â· (f, Suc (length ss + length ts)) â â± â§ ctxt_well_def_hole_path â± C"

fun inv_const_ctxt where
"inv_const_ctxt â± v Hole = Hole"
| "inv_const_ctxt â± v ((More f ss C ts))
= (More f (map (term_to_sig â± v) ss) (inv_const_ctxt â± v C) (map (term_to_sig â± v) ts))"

fun inv_const_ctxt' where
"inv_const_ctxt' â± v Hole = Var v"
| "inv_const_ctxt' â± v ((More f ss C ts))
= (if (f, Suc (length ss + length ts)) â â± then Fun f (map (term_to_sig â± v) ss @ inv_const_ctxt' â± v C # map (term_to_sig â± v) ts) else Var v)"

subsubsection â¹Replace term at a given position in contextsâº

fun replace_term_context_at :: "('f, 'v) ctxt â pos â ('f, 'v) term â ('f, 'v) ctxt"
("_[_ â _]â©C" [1000, 0] 1000) where
"replace_term_context_at â¡ p u = â¡"
| "replace_term_context_at (More f ss C ts) (i # ps) u =
(if i < length ss then More f (ss[i := (ss ! i)[ps â u]]) C ts
else if i = length ss then More f ss (replace_term_context_at C ps u) ts
else More f ss C (ts[(i - Suc (length ss)) := (ts ! (i - Suc (length ss)))[ps â u]]))"

abbreviation "constT c â¡ Fun c []"

subsubsection â¹Multihole context closure of a term relation as inductive setâº

definition all_ctxt_closed where
"all_ctxt_closed F r â· (âf ts ss. (f, length ss) â F â¶ length ts = length ss â¶
(âi. i < length ts â¶ (ts ! i, ss ! i) â r) â¶
(â i. i < length ts â¶ funas_term (ts ! i) âª funas_term (ss ! i) â F) â¶ (Fun f ts, Fun f ss) â r) â§
(â x. (Var x, Var x) â r)"

subsection â¹Destruction and introduction of @{const all_ctxt_closed}âº

lemma all_ctxt_closedD: "all_ctxt_closed F r â¹ (f,length ss) â F â¹ length ts = length ss
â¹ â¦â i. i < length ts â¹ (ts ! i, ss ! i) â r â§
â¹ â¦â i. i < length ts â¹ funas_term (ts ! i) â F â§
â¹ â¦â i. i < length ts â¹ funas_term (ss ! i) â F â§
â¹ (Fun f ts, Fun f ss) â r"
unfolding all_ctxt_closed_def by auto

lemma trans_ctxt_sig_imp_all_ctxt_closed: assumes tran: "trans r"
and refl: "â t. funas_term t â F â¹ (t,t) â r"
and ctxt: "â C s t. funas_ctxt C â F â¹ funas_term s â F â¹ funas_term t â F â¹ (s,t) â r â¹ (C â¨ s â©, C â¨ t â©) â r"
shows "all_ctxt_closed F r" unfolding all_ctxt_closed_def
proof (rule, intro allI impI)
fix f ts ss
assume f: "(f,length ss) â F" and
l: "length ts = length ss" and
steps: "â i < length ts. (ts ! i, ss ! i) â r" and
sig: "â i < length ts. funas_term (ts ! i) âª  funas_term (ss ! i) â F"
from sig have sig_ts: "â t. t â set ts â¹ funas_term t â F"  unfolding set_conv_nth by auto
let ?p = "Î» ss. (Fun f ts, Fun f ss) â r â§ funas_term (Fun f ss) â F"
let ?r = "Î» xsi ysi. (xsi, ysi) â r â§ funas_term ysi â F"
have init: "?p ts" by (rule conjI[OF refl], insert f sig_ts l, auto)
have "?p ss"
proof (rule parallel_list_update[where p = ?p and r = ?r, OF _ HOL.refl init l[symmetric]])
fix xs i y
assume len: "length xs = length ts"
and i: "i < length ts"
and r: "?r (xs ! i) y"
and p: "?p xs"
let ?C = "More f (take i xs) Hole (drop (Suc i) xs)"
have id1: "Fun f xs = ?C â¨ xs ! iâ©" using id_take_nth_drop[OF i[folded len]] by simp
have id2: "Fun f (xs[i := y]) = ?C â¨ y â©" using upd_conv_take_nth_drop[OF i[folded len]] by simp
from p[unfolded id1] have C: "funas_ctxt ?C â F" and xi: "funas_term (xs ! i) â F" by auto
from r have "funas_term y â F" "(xs ! i, y) â r" by auto
with ctxt[OF C xi this] C have r: "(Fun f xs, Fun f (xs[i := y])) â r"
and f: "funas_term (Fun f (xs[i := y])) â F" unfolding id1 id2 by auto
from p r tran have "(Fun f ts, Fun f (xs[i := y])) â r" unfolding trans_def by auto
with f
show "?p (xs[i := y])"  by auto
qed (insert sig steps, auto)
then show "(Fun f ts, Fun f ss) â r" ..
qed (insert refl, auto)

subsection â¹Lemmas for @{const poss} and ordering of positionsâº

lemma subst_poss_mono: "poss s â poss (s â Ï)"
by (induct s) force+

lemma par_pos_prefix [simp]:
"(i # p) â¥ (i # q) â¹ p â¥ q"

lemma pos_diff_itself [simp]: "p -â©p p = []"

lemma pos_les_eq_append_diff [simp]:
by (metis option.sel pos_diff_def position_less_eq_def remove_prefix_append)

lemma pos_diff_append_itself [simp]: "(p @ q) -â©p p = q"

lemma poss_pos_diffI:
"p â¤â©p q â¹ q â poss s â¹ q -â©p p â poss (s |_ p)"
using poss_append_poss by fastforce

lemma less_eq_poss_append_itself [simp]: "p â¤â©p (p @ q)"
using position_less_eq_def by blast

lemma poss_ctxt_apply [simp]:
"hole_pos C @ p â poss Câ¨sâ© â· p â poss s"
by (induct C) auto

lemma pos_replace_at_pres:
"p â poss s â¹ p â poss s[p â t]"
proof (induct p arbitrary: s)
case (Cons i p)
show ?case using Cons(1)[of "args s ! i"] Cons(2-)
by (cases s) auto
qed auto

lemma par_pos_replace_pres:
"p â poss s â¹ p â¥ q â¹ p â poss s[q â t]"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "args s ! i" "tl q"] Cons(2-)
by (cases s; cases q) (auto simp add: nth_list_update par_Cons_iff)
qed auto

lemma poss_of_termE [elim]:
assumes "p â poss_of_term u s"
and "p â poss s â¹ s |_ p = u â¹ P"
shows "P" using assms unfolding poss_of_term_def
by blast

lemma poss_of_term_Cons:
"i # p â poss_of_term u (Fun f ts) â¹ p â poss_of_term u (ts ! i)"
unfolding poss_of_term_def by auto

lemma poss_of_term_const_ctxt_apply:
assumes "p â poss_of_term (constT c) Câ¨sâ©"
shows "p â¥ (hole_pos C) â¨ (hole_pos C) â¤â©p p" using assms
proof (induct p arbitrary: C)
case Nil then show ?case
by (cases C) auto
next
case (Cons i p) then show ?case
by (cases C) (fastforce simp add: par_Cons_iff dest!: poss_of_term_Cons)+
qed

subsection â¹Lemmas for @{const subt_at} and @{const replace_term_at}âº

lemma subt_at_append_dist:
"p @ q â poss s â¹ s |_ (p @ q) = (s |_ p) |_ q"
proof (induct p arbitrary: s)
case (Cons i p) then show ?case
by (cases s) auto
qed auto

lemma ctxt_apply_term_subt_at_hole_pos [simp]:
"Câ¨sâ© |_ (hole_pos C @ q) = s |_ q"
by (induct C) auto

lemma subst_subt_at_dist:
"p â poss s â¹ s â Ï |_ p = s |_ p â Ï"
proof (induct p arbitrary: s)
case (Cons i p) then show ?case
by (cases s) auto
qed auto

lemma replace_term_at_subt_at_id [simp]: "s[p â (s |_ p)] = s"
proof (induct p arbitrary: s)
case (Cons i p) then show ?case
by (cases s) auto
qed auto

lemma replace_term_at_same_pos [simp]:
"s[p â u][p â t] = s[p â t]"
using position_less_refl replace_term_at_above by blast

â â¹Replacement at under substitutionâº
lemma subt_at_vars_term:
"p â poss s â¹ s |_ p = Var x â¹ x â vars_term s"
by (metis UnCI ctxt_at_pos_subt_at_id term.set_intros(3) vars_term_ctxt_apply)

lemma linear_term_varposs_subst_replace_term:
"linear_term s â¹ p â varposs s â¹ p â¤â©p q â¹
(s â Ï)[q â u] = s â (Î» x. if Var x = s |_ p then (Ï x)[q -â©p p â u] else (Ï x))"
proof (induct q arbitrary: s p)
case (Cons i q)
show ?case using Cons(1)[of "args s ! i" "tl p"] Cons(2-)
by (cases s) (auto simp: varposs_def nth_list_update term_subst_eq_conv
is_partition_alt is_partition_alt_def disjoint_iff subt_at_vars_term intro!: nth_equalityI)
qed (auto simp: varposs_def)

â â¹Replacement at context parallel to the hole positionâº
lemma par_hole_pos_replace_term_context_at:
proof (induct p arbitrary: C)
case (Cons i p)
from Cons(2) obtain f ss D ts where [simp]: "C = More f ss D ts" by (cases C) auto
show ?case using Cons(1)[of D] Cons(2)
by (auto simp: list_update_append nth_append_Cons minus_nat.simps(2) split: nat.splits)
qed auto

lemma par_pos_replace_term_at:
"p â poss s â¹ p â¥ q â¹ s[q â t] |_ p = s |_ p"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "args s ! i" "tl q"] Cons(2-)
by (cases s; cases q) (auto, metis nth_list_update par_Cons_iff)
qed auto

lemma less_eq_subt_at_replace:
"p â poss s â¹ p â¤â©p q â¹ s[q â t] |_ p = (s |_ p)[q -â©p p â t]"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "args s ! i" "tl q"] Cons(2-)
by (cases s; cases q) auto
qed auto

lemma greater_eq_subt_at_replace:
"p â poss s â¹ q â¤â©p p â¹ s[q â t] |_ p = t |_ (p -â©p q)"
proof (induct p arbitrary: s q)
case (Cons i p)
show ?case using Cons(1)[of "args s ! i" "tl q"] Cons(2-)
by (cases s; cases q) auto
qed auto

lemma replace_subterm_at_itself [simp]:
"s[p â (s |_ p)[q â t]] = s[p @ q â t]"
proof (induct p arbitrary: s)
case (Cons i p)
show ?case using Cons(1)[of "args s ! i"]
by (cases s) auto
qed auto

lemma hole_pos_replace_term_at [simp]:
proof (induct C arbitrary: p)
case (More f ss C ts) then show ?case
by (cases p) auto
qed auto

lemma ctxt_of_pos_term_apply_replace_at_ident:
assumes "p â poss s"
shows "(ctxt_at_pos s p)â¨tâ© = s[p â t]"
using assms
proof (induct p arbitrary: s)
case (Cons i p)
show ?case using Cons(1)[of "args s ! i"] Cons(2-)
by (cases s) (auto simp: nth_append_Cons intro!: nth_equalityI)
qed auto

lemma ctxt_apply_term_replace_term_hole_pos [simp]:
by (simp add: pos_diff_def position_less_eq_def remove_prefix_append)

lemma ctxt_apply_subt_at_hole_pos [simp]: "Câ¨sâ© |_ hole_pos C = s"
by (induct C) auto

lemma subt_at_imp_supteq':
assumes "p â poss s" and "s|_p = t" shows "s âµ t" using assms
proof (induct p arbitrary: s)
case (Cons i p)
from Cons(2-) show ?case using Cons(1)[of "args s ! i"]
by (cases s) force+
qed auto

lemma subt_at_imp_supteq:
assumes "p â poss s" shows "s âµ s|_p"
proof -
have "s|_p = s|_p" by auto
with assms show ?thesis by (rule subt_at_imp_supteq')
qed

subsection â¹@{const term_to_sig} invariants and distributionsâº

lemma fuans_term_term_to_sig [simp]: "funas_term (term_to_sig â± v t) â â±"
by (induct t) auto

lemma term_to_sig_id [simp]:
"funas_term t â â± â¹ term_to_sig â± v t = t"
by (induct t) (auto simp add: UN_subset_iff map_idI)

lemma term_to_sig_subst_sig [simp]:
"funas_term t â â± â¹ term_to_sig â± v (t â Ï) = t â (Î» x.  term_to_sig â± v (Ï x))"
by (induct t) auto

lemma funas_ctxt_ctxt_inv_const_ctxt_ind [simp]:
"funas_ctxt C â â± â¹ inv_const_ctxt â± v C = C"
by (induct C) (auto simp add: UN_subset_iff intro!: nth_equalityI)

lemma term_to_sig_ctxt_apply [simp]:
"ctxt_well_def_hole_path â± C â¹ term_to_sig â± v Câ¨sâ© = (inv_const_ctxt â± v C)â¨term_to_sig â± v sâ©"
by (induct C) auto

lemma term_to_sig_ctxt_apply' [simp]:
"Â¬ ctxt_well_def_hole_path â± C â¹ term_to_sig â± v Câ¨sâ© = inv_const_ctxt' â± v C"
by (induct C) auto

lemma funas_ctxt_ctxt_well_def_hole_path:
"funas_ctxt C â â± â¹ ctxt_well_def_hole_path â± C"
by (induct C) auto

subsection â¹Miscâº

lemma funas_term_subt_at:
"(f, n) â funas_term t â¹ (â p ts. p â poss t â§ t |_ p = Fun f ts â§ length ts = n)"
proof (induct t)
case (Fun g ts) note IH = this
show ?case
proof (cases "g = f â§ length ts = n")
case False
then obtain i where i: "i < length ts" "(f, n) â funas_term (ts ! i)" using IH(2)
using in_set_idx by force
from IH(1)[OF nth_mem[OF this(1)] this(2)] show ?thesis using i(1)
by (metis poss_Cons_poss subt_at.simps(2) term.sel(4))
qed auto
qed simp

lemma finite_poss: "finite (poss s)"
proof (induct s)
case (Fun f ts)
have "poss (Fun f ts) = insert [] (â (set (map2 (Î» i p. ((#) i)  p) [0..< length ts] (map poss ts))))"
by (auto simp: image_iff set_zip split: prod.splits)
then show ?case using Fun
by (auto simp del: poss.simps dest!: set_zip_rightD)
qed simp

lemma finite_varposs: "finite (varposs s)"
by (intro finite_subset[of "varposs s" "poss s"]) (auto simp: varposs_def finite_poss)

lemma gound_linear [simp]: "ground t â¹ linear_term t"
by (induct t) (auto simp: is_partition_alt is_partition_alt_def)

declare ground_substI[intro, simp]
lemma ground_ctxt_substI:
"(â x. x â vars_ctxt C â¹ ground (Ï x)) â¹ ground_ctxt (C ââ©c Ï)"
by (induct C) auto

lemma funas_ctxt_subst_apply_ctxt:
"funas_ctxt (C ââ©c Ï) = funas_ctxt C âª (â (funas_term  Ï  vars_ctxt C))"
proof (induct C)
case (More f ss C ts)
then show ?case
qed simp

lemma varposs_Var[simp]:
"varposs (Var x) = {[]}"
by (auto simp: varposs_def)

lemma varposs_Fun[simp]:
"varposs (Fun f ts) = { i # p| i p. i < length ts â§ p â varposs (ts ! i)}"
by (auto simp: varposs_def)

lemma vars_term_varposs_iff:
"x â vars_term s â· (â p â varposs s. s |_ p = Var x)"
proof (induct s)
case (Fun f ts)
show ?case using Fun[OF nth_mem]
by (force simp: in_set_conv_nth Bex_def)
qed auto

lemma vars_term_empty_ground:
"vars_term s = {} â¹ ground s"
by (metis equals0D ground_substI subst_ident)

lemma ground_subst_apply: "ground t â¹ t â Ï = t"
by (induct t) (auto intro: nth_equalityI)

lemma varposs_imp_poss:
"p â varposs s â¹ p â poss s" by (auto simp: varposs_def)

lemma varposs_empty_gound:
"varposs s = {} â· ground s"
by (induct s) (fastforce simp: in_set_conv_nth)+

lemma funas_term_subterm_atI [intro]:
"p â poss s â¹ funas_term s â â± â¹ funas_term (s |_ p) â â±"
by (metis ctxt_at_pos_subt_at_id funas_ctxt_apply le_sup_iff)

lemma varposs_ground_replace_at:
"p â varposs s â¹ ground u â¹ varposs s[p â u] = varposs s - {p}"
proof (induct p arbitrary: s)
case Nil then show ?case
by (cases s) (auto simp: varposs_empty_gound)
next
case (Cons i p)
from Cons(2) obtain f ts where [simp]: "s = Fun f ts" by (cases s) auto
from Cons(2) have var: "p â varposs (ts ! i)" by auto
from Cons(1)[OF var Cons(3)] have "j < length ts â¹ {j # q| q. q â varposs (ts[i := (ts ! i)[p â u]] ! j)} =
{j # q |q. q â varposs (ts ! j)} - {i # p}" for j
by (cases "j = i") (auto simp add: nth_list_update)
then show ?case by auto blast
qed

lemma funas_term_replace_at_upper:
"funas_term s[p â t] â funas_term s âª funas_term t"
proof (induct p arbitrary: s)
case (Cons i p)
show ?case using Cons(1)[of "args s ! i"]
by (cases s) (fastforce simp: in_set_conv_nth nth_list_update split!: if_splits)+
qed simp

lemma funas_term_replace_at_lower:
"p â poss s â¹ funas_term t â funas_term (s[p â t])"
proof (induct p arbitrary: s)
case (Cons i p)
show ?case using Cons(1)[of "args s ! i"] Cons(2-)
by (cases s) (fastforce simp: in_set_conv_nth nth_list_update split!: if_splits)+
qed simp

lemma poss_of_term_possI [intro!]:
"p â poss s â¹ s |_ p = u â¹ p â poss_of_term u s"
unfolding poss_of_term_def by blast

lemma poss_of_term_replace_term_at:
"p â poss s â¹ p â poss_of_term u s[p â u]"
proof (induct p arbitrary: s)
case (Cons i p) then show ?case
by (cases s) (auto simp: poss_of_term_def)
qed auto

lemma constT_nfunas_term_poss_of_term_empty:
"(c, 0) â funas_term t â· poss_of_term (constT c) t = {}"
unfolding poss_of_term_def
using funas_term_subt_at[of c 0 t]
using funas_term_subterm_atI[where ?â± ="funas_term t" and ?s = t, THEN subsetD]
by auto

lemma poss_of_term_poss_emptyD:
assumes "poss_of_term u s = {}"
shows "p â poss s â¹ s |_ p â  u" using assms
unfolding poss_of_term_def by blast

lemma possc_subt_at_ctxt_apply:
"p â possc C â¹ p â¥ hole_pos C â¹ Câ¨sâ© |_ p = Câ¨tâ© |_ p"
proof (induct p arbitrary: C)
case (Cons i p)
have [dest]: "length ss # p â possc (More f ss D ts) â¹ p â possc D" for f ss D ts
by (auto simp: possc_def)
show ?case using Cons
by (cases C) (auto simp: nth_append_Cons)
qed simp

end

# Theory Rewriting

section â¹Rewritingâº
theory Rewriting
imports Terms_Positions
begin

subsection â¹Basic rewrite definitionsâº

subsubsection â¹Rewrite steps with implicit signature declaration (encoded in the type)âº

inductive_set rrstep :: "('f, 'v) term rel â ('f, 'v) term rel" for â where
[intro]: "(l, r) â â â¹ (l â Ï, r â Ï) â rrstep â"

inductive_set rstep :: "('f, 'v) term rel â ('f, 'v) term rel" for â where

subsubsection â¹Restrict relations to terms induced by a given signatureâº

definition "sig_step â± â = Restr â (Collect (Î» s. funas_term s â â±))"

subsubsection â¹Rewriting under a given signature/restricted to ground termsâº

abbreviation "srrstep â± â â¡ sig_step â± (rrstep â)"
abbreviation "srstep â± â â¡ sig_step â± (rstep â)"
abbreviation "gsrstep â± â â¡ Restr (sig_step â± (rstep â)) (Collect ground)"

subsubsection â¹Rewriting sequences involving a root stepâº

abbreviation (input) relto :: "'a rel â 'a rel â 'a rel" where
"relto R S â¡ S^* O R O S^*"
definition "srsteps_with_root_step â± â â¡ relto (sig_step â± (rrstep â)) (srstep â± â)"

subsection â¹Monotonicity lawsâº

lemma Restr_mono: "Restr r A â r" by auto

lemma Restr_trancl_mono_set: "(Restr r A)â§+ â A Ã A"

lemma rrstep_rstep_mono: "rrstep â â rstep â"
by (auto intro: rstep.intros[where ?C = â¡, simplified])

lemma sig_step_mono:
"â± â ð¢ â¹ sig_step â± â â sig_step ð¢ â"
by (auto simp: sig_step_def)

lemma sig_step_mono2:
"â â â â¹ sig_step â± â â sig_step â± â"
by (auto simp: sig_step_def)

lemma srrstep_monp:
"â± â ð¢ â¹ srrstep â± â â srrstep ð¢ â"

lemma srstep_monp:
"â± â ð¢ â¹ srstep â± â â srstep ð¢ â"

lemma srsteps_monp:
"â± â ð¢ â¹ (srstep â± â)â§+ â (srstep ð¢ â)â§+"

lemma srsteps_eq_monp:
"â± â ð¢ â¹ (srstep â± â)â§* â (srstep ð¢ â)â§*"
by (meson rtrancl_mono sig_step_mono subrelI subsetD trancl_into_rtrancl)

lemma srsteps_with_root_step_sig_mono:
"â± â ð¢ â¹ srsteps_with_root_step â± â â srsteps_with_root_step ð¢ â"
unfolding srsteps_with_root_step_def
by (simp add: relcomp_mono srrstep_monp srsteps_eq_monp)

subsection â¹Introduction, elimination, and destruction rules for @{const sig_step}, @{const rstep}, @{const rrstep},
@{const srrstep}, and @{const srstep}âº

lemma sig_stepE [elim, consumes 1]:
"(s, t) â sig_step â± â â¹ â¦(s, t) â â â¹ funas_term s â â± â¹ funas_term t â â± â¹ Pâ§ â¹ P"
by (auto simp: sig_step_def)

lemma sig_stepI [intro]:
"funas_term s â â± â¹ funas_term t â â± â¹ (s, t) â â â¹ (s, t) â sig_step â± â"
by (auto simp: sig_step_def)

lemma rrstep_subst [elim, consumes 1]:
assumes "(s, t) â rrstep â"
obtains l r Ï where "(l, r) â â" "s = l â Ï" "t = r â Ï" using assms
by (meson rrstep.simps)

lemma rstep_imp_C_s_r:
assumes "(s, t) â rstep â"
shows "âC Ï l r. (l,r) â â â§ s = Câ¨lâÏâ© â§ t = Câ¨râÏâ©"using assms
by (metis rrstep.cases rstep.simps)

lemma rstep_imp_C_s_r' [elim, consumes 1]:
assumes "(s, t) â rstep â"
obtains C l r Ï where "(l,r) â â" "s = Câ¨lâÏâ©" "t = Câ¨râÏâ©" using assms
using rstep_imp_C_s_r by blast

lemma rrstep_basicI [intro]:
"(l, r) â â â¹ (l, r) â rrstep â"
by (metis rrstepp.intros rrstepp_rrstep_eq subst_apply_term_empty)

lemma rstep_ruleI [intro]:
"(l, r) â â â¹ (l, r) â rstep â"
using rrstep_rstep_mono by blast

lemma rstepI [intro]:
"(l, r) â â â¹ s = Câ¨l â Ïâ© â¹ t = Câ¨r â Ïâ© â¹ (s, t) â rstep â"

lemma rstep_substI [intro]:
"(s, t) â rstep â â¹ (s â Ï, t â Ï) â rstep â"
by (auto elim!: rstep_imp_C_s_r' simp flip: subst_subst_compose)

lemma rstep_ctxtI [intro]:
by (auto elim!: rstep_imp_C_s_r' simp flip: ctxt_ctxt_compose)

lemma srrstepD:
"(s, t) â srrstep â± â â¹ (s, t) â rrstep â â§ funas_term s â â± â§ funas_term t â â±"
by (auto simp: sig_step_def)

lemma srstepD:
"(s, t) â (srstep â± â) â¹ (s, t) â rstep â â§ funas_term s â â± â§ funas_term t â â±"
by (auto simp: sig_step_def)

lemma srstepsD:
"(s, t) â (srstep â± â)â§+ â¹ (s, t) â (rstep â)â§+ â§ funas_term s â â± â§ funas_term t â â±"
unfolding sig_step_def using trancl_mono_set[OF Restr_mono]
by (auto simp: sig_step_def dest: subsetD[OF Restr_trancl_mono_set])

subsubsection â¹Transitive and relfexive closure distribution over @{const sig_step}âº

lemma funas_rel_converse:
"funas_rel â â â± â¹ funas_rel (âÂ¯) â â±" unfolding funas_rel_def
by auto

lemma rstep_term_to_sig_r:
assumes "(s, t) â rstep â" and "funas_rel â â â±" and "funas_term s â â±"
shows "(s, term_to_sig â± v t) â rstep â"
proof -
from assms(1) obtain C l r Ï where
*: "s = Câ¨l â Ïâ©" "t = Câ¨r â Ïâ©" "(l, r) â â" by auto
from assms(2, 3) *(3) have "funas_ctxt C â â±" "funas_term l â â±" "funas_term r â â±"
by (auto simp: *(1) funas_rel_def funas_term_subst subset_eq)
then have "(term_to_sig â± v s, term_to_sig â± v t) â rstep â" using *(3)
by (auto simp: *(1, 2) funas_ctxt_ctxt_well_def_hole_path)
then show ?thesis using assms(3) by auto
qed

lemma rstep_term_to_sig_l:
assumes "(s, t) â rstep â" and "funas_rel â â â±" and "funas_term t â â±"
shows "(term_to_sig â± v s, t) â rstep â"
proof -
from assms(1) obtain C l r Ï where
*: "s = Câ¨l â Ïâ©" "t = Câ¨r â Ïâ©" "(l, r) â â" by auto
from assms(2, 3) *(3) have "funas_ctxt C â â±" "funas_term l â â±" "funas_term r â â±"
by (auto simp: *(2) funas_rel_def funas_term_subst subset_eq)
then have "(term_to_sig â± v s, term_to_sig â± v t) â rstep â" using *(3)
by (auto simp: *(1, 2) funas_ctxt_ctxt_well_def_hole_path)
then show ?thesis using assms(3) by auto
qed

lemma rstep_trancl_sig_step_r:
assumes "(s, t) â (rstep â)â§+" and "funas_rel â â â±" and "funas_term s â â±"
shows "(s, term_to_sig â± v t) â (srstep â± â)â§+" using assms
proof (induct)
case (base t)
then show ?case using subsetD[OF fuans_term_term_to_sig, of _ â± v]
by (auto simp: rstep_term_to_sig_r sig_step_def intro!: r_into_trancl)
next
case (step t u)
then have st: "(s, term_to_sig â± v t) â (srstep â± â)â§+" by auto
from step(2) obtain  C l r Ï where
*: "t = Câ¨l â Ïâ©" "u = Câ¨r â Ïâ©" "(l, r) â â" by auto
show ?case
proof (cases "ctxt_well_def_hole_path â± C")
case True
from *(3) step(4) have "funas_term l â â±" "funas_term r â â±" by (auto simp: funas_rel_def)
then have "(term_to_sig â± v t, term_to_sig â± v u) â rstep â"
using True step(2) *(3) unfolding *
by auto
then have "(term_to_sig â± v t, term_to_sig â± v u) â srstep â± â"
by (auto simp:_ sig_step_def)
then show ?thesis using st by auto
next
case False
then have "term_to_sig â± v t = term_to_sig â± v u" unfolding * by auto
then show ?thesis using st by auto
qed
qed

lemma rstep_trancl_sig_step_l:
assumes "(s, t) â (rstep â)â§+" and "funas_rel â â â±" and "funas_term t â â±"
shows "(term_to_sig â± v s, t) â (srstep â± â)â§+" using assms
proof (induct rule: converse_trancl_induct)
case (base t)
then show ?case using subsetD[OF fuans_term_term_to_sig, of _ â± v]
by (auto simp: rstep_term_to_sig_l sig_step_def intro!: r_into_trancl)
next
case (step s u)
then have st: "(term_to_sig â± v u, t) â (srstep â± â)â§+" by auto
from step(1) obtain C l r Ï where
*: "s = Câ¨l â Ïâ©" "u = Câ¨r â Ïâ©" "(l, r) â â" by auto
show ?case
proof (cases "ctxt_well_def_hole_path â± C")
case True
from *(3) step(4) have "funas_term l â â±" "funas_term r â â±" by (auto simp: funas_rel_def)
then have "(term_to_sig â± v s, term_to_sig â± v u) â rstep â"
using True step(2) *(3) unfolding *
by auto
then have "(term_to_sig â± v s, term_to_sig â± v u) â srstep â± â"
by (auto simp:_ sig_step_def)
then show ?thesis using st by auto
next
case False
then have "term_to_sig â± v s = term_to_sig â± v u" unfolding * by auto
then show ?thesis using st by auto
qed
qed

lemma rstep_srstepI [intro]:
"funas_rel â â â± â¹ funas_term s â â± â¹ funas_term t â â± â¹ (s, t) â rstep â â¹ (s, t) â srstep â± â"
by blast

lemma rsteps_srstepsI [intro]:
"funas_rel â â â± â¹ funas_term s â â± â¹ funas_term t â â± â¹ (s, t) â (rstep â)â§+ â¹ (s, t) â (srstep â± â)â§+"
using rstep_trancl_sig_step_r[of s t â â±]
by auto

lemma rsteps_eq_srsteps_eqI [intro]:
"funas_rel â â â± â¹ funas_term s â â± â¹ funas_term t â â± â¹ (s, t) â (rstep â)â§* â¹ (s, t) â (srstep â± â)â§*"

lemma rsteps_eq_relcomp_srsteps_eq_relcompI [intro]:
assumes "funas_rel â â â±" "funas_rel ð® â â±"
and funas: "funas_term s â â±" "funas_term t â â±"
and steps: "(s, t) â (rstep â)â§* O (rstep ð®)â§*"
shows "(s, t) â (srstep â± â)â§* O (srstep â± ð®)â§*"
proof -
from steps obtain u where "(s, u) â (rstep â)â§*" "(u, t) â (rstep ð®)â§*" by auto
then have "(s, term_to_sig â± v u) â (srstep â± â)â§*" "(term_to_sig â± v u, t) â (srstep â± ð®)â§*"
using rstep_trancl_sig_step_l[OF _ assms(2) funas(2), of u v]
using rstep_trancl_sig_step_r[OF _ assms(1) funas(1), of u v] funas
by (auto simp: rtrancl_eq_or_trancl)
then show ?thesis by auto
qed

subsubsection â¹Distributivity lawsâº

lemma rstep_smycl_dist:
"(rstep â)â§â = rstep (ââ§â)"
by (auto simp: sig_step_def)

lemma sig_step_symcl_dist:
"(sig_step â± â)â§â = sig_step â± (ââ§â)"
by (auto simp: sig_step_def)

lemma srstep_symcl_dist:
"(srstep â± â)â§â = srstep â± (ââ§â)"
by (auto simp: sig_step_def)

lemma Restr_smycl_dist:
"(Restr â ð)â§â = Restr (ââ§â) ð"
by auto

lemmas rew_symcl_inwards = rstep_smycl_dist sig_step_symcl_dist srstep_symcl_dist Restr_smycl_dist
lemmas rew_symcl_outwards = rew_symcl_inwards[symmetric]

lemma rstep_converse_dist:
"(rstep â)Â¯ = rstep (âÂ¯)"
by auto

lemma srrstep_converse_dist:
"(srrstep â± â)Â¯ = srrstep â± (âÂ¯)"
by (fastforce simp: sig_step_def)

lemma sig_step_converse_rstep:
"(srstep â± â)Â¯ = sig_step â± ((rstep â)Â¯)"
by (meson converse.simps set_eq_subset sig_stepE(1) sig_stepE sig_stepI subrelI)

lemma srstep_converse_dist:
"(srstep â± â)Â¯ = srstep â± (âÂ¯)"
by (auto simp: sig_step_def)

lemma Restr_converse: "(Restr â A)Â¯ = Restr (âÂ¯) A"
by auto

lemmas rew_converse_inwards = rstep_converse_dist srrstep_converse_dist sig_step_converse_rstep
srstep_converse_dist Restr_converse trancl_converse[symmetric] rtrancl_converse[symmetric]
lemmas rew_converse_outwards = rew_converse_inwards[symmetric]

lemma sig_step_rsteps_dist:
"funas_rel â â â± â¹ sig_step â± ((rstep â)â§+) = (srstep â± â)â§+"
by (auto elim!: sig_stepE dest: srstepsD)

lemma sig_step_rsteps_eq_dist:
"funas_rel â â â± â¹ sig_step â± ((rstep â)â§+) âª Id = (srstep â± â)â§*"
by (auto simp: rtrancl_eq_or_trancl sig_step_rsteps_dist)

lemma sig_step_conversion_dist:
"(srstep â± â)â§ââ§* = (srstep â± (ââ§â))â§*"
by (auto simp: rtrancl_eq_or_trancl sig_step_rsteps_dist conversion_def srstep_symcl_dist)

lemma gsrstep_conversion_dist:
"(gsrstep â± â)â§ââ§* = (gsrstep â± (ââ§â))â§*"
by (auto simp: conversion_def rew_symcl_inwards)

lemma sig_step_grstep_dist:
"gsrstep â± â = sig_step â± (Restr (rstep â) (Collect ground))"
by (auto simp: sig_step_def)

subsection â¹Substitution closure of @{const srstep}âº

lemma srstep_subst_closed:
assumes "(s, t) â srstep â± â" "â x. funas_term (Ï x) â â±"
shows "(s â Ï, t â Ï) â srstep â± â" using assms
by (auto simp: sig_step_def funas_term_subst)

lemma srsteps_subst_closed:
assumes "(s, t) â (srstep â± â)â§+" "â x. funas_term (Ï x) â â±"
shows "(s â Ï, t â Ï) â (srstep â± â)â§+" using assms(1)
proof (induct rule: trancl.induct)
case (r_into_trancl s t) show ?case
using srstep_subst_closed[OF r_into_trancl assms(2)]
by auto
next
case (trancl_into_trancl s t u)
from trancl_into_trancl(2) show ?case
using srstep_subst_closed[OF trancl_into_trancl(3) assms(2)]
by (meson rtrancl_into_trancl1 trancl_into_rtrancl)
qed

lemma srsteps_eq_subst_closed:
assumes "(s, t) â (srstep â± â)â§*" "â x. funas_term (Ï x) â â±"
shows "(s â Ï, t â Ï) â (srstep â± â)â§*" using assms srsteps_subst_closed
by (metis rtrancl_eq_or_trancl)

lemma srsteps_eq_subst_relcomp_closed:
assumes "(s, t) â (srstep â± â)â§* O (srstep â± ð®)â§*" "â x. funas_term (Ï x) â â±"
shows "(s â Ï, t â Ï) â (srstep â± â)â§* O (srstep â± ð®)â§*"
proof -
from assms(1) obtain u where "(s, u) â (srstep â± â)â§*" "(u, t) â (srstep â± ð®)â§*" by auto
then have "(s â Ï, u â Ï) â (srstep â± â)â§*" "(u â Ï, t â Ï) â (srstep â± ð®)â§*"
using assms srsteps_eq_subst_closed
by metis+
then show ?thesis by auto
qed

subsection â¹Context closure of @{const srstep}âº

lemma srstep_ctxt_closed:
assumes "funas_ctxt C â â±" and "(s, t) â srstep â± â"
by (intro sig_stepI) (auto dest: srstepD)

lemma srsteps_ctxt_closed:
assumes "funas_ctxt C â â±" and "(s, t) â (srstep â± â)â§+"
by (induct) force+

lemma srsteps_eq_ctxt_closed:
assumes "funas_ctxt C â â±" and "(s, t) â (srstep â± â)â§*"
by (metis rtrancl_eq_or_trancl)

lemma sig_steps_join_ctxt_closed:
assumes "funas_ctxt C â â±" and "(s, t) â (srstep â± â)â§â"
unfolding join_def rew_converse_inwards
by auto

text â¹The following lemma shows that every rewrite sequence either contains a root step or is root stableâº

lemma nsrsteps_with_root_step_step_on_args:
assumes "(s, t) â (srstep â± â)â§+" "(s, t) â srsteps_with_root_step â± â"
shows "â f ss ts. s = Fun f ss â§ t = Fun f ts â§ length ss = length ts â§
(â i < length ts. (ss ! i, ts ! i) â (srstep â± â)â§*)" using assms
proof (induct)
case (base t)
obtain C l r Ï where [simp]: "s = Câ¨l â Ïâ©" "t = Câ¨r â Ïâ©" and r: "(l, r) â â"
using base(1) unfolding sig_step_def
by blast
then have funas: "funas_ctxt C â â±" "funas_term (l â Ï) â â±" "funas_term (r â Ï) â â±"
using base(1) by (auto simp: sig_step_def)
from funas(2-) r have "(l â Ï, r â Ï) â srrstep â± â"
by (auto simp: sig_step_def)
then have "C = Hole â¹ False" using base(2) r
by (auto simp: srsteps_with_root_step_def)
then obtain f ss D ts where [simp]: "C = More f ss D ts" by (cases C) auto
have "(Dâ¨l â Ïâ©, Dâ¨r â Ïâ©) â (srstep â± â)" using base(1) r funas
by (auto simp: sig_step_def)
then show ?case using funas by (auto simp: nth_append_Cons)
next
case (step t u) show ?case
proof (cases "(s, t) â srsteps_with_root_step â± â â¨ (t, u) â sig_step â± (rrstep â)")
case True then show ?thesis using step(1, 2, 4)
by (auto simp add: relcomp3_I rtrancl.rtrancl_into_rtrancl srsteps_with_root_step_def)
next
case False
obtain C l r Ï where *[simp]: "t = Câ¨l â Ïâ©" "u = Câ¨r â Ïâ©" and r: "(l, r) â â"
using step(2) unfolding sig_step_def by blast
then have funas: "funas_ctxt C â â±" "funas_term (l â Ï) â â±" "funas_term (r â Ï) â â±"
using step(2) by (auto simp: sig_step_def)
from False have "C â  Hole" using funas r by (force simp: sig_step_def)
then obtain f ss D ts where c[simp]: "C = More f ss D ts" by (cases C) auto
from step(3, 1) False obtain g sss tss where
**[simp]: "s = Fun g sss" "t = Fun g tss" and l: "length sss = length tss" and
inv: "â i < length tss. (sss ! i, tss ! i) â (srstep â± â)â§*"
by auto
have [simp]: "g = f" and lc: "Suc (length ss + length ts) = length sss"
using l *(1) unfolding c using **(2) by auto
then have "â i < Suc (length ss + length ts). ((ss @ Dâ¨l â Ïâ© # ts) ! i, (ss @ Dâ¨r â Ïâ© # ts) ! i) â (srstep â± â)â§*"
using * funas r by (auto simp: nth_append_Cons r_into_rtrancl rstep.intros rstepI sig_stepI)
then have "i < length tss â¹ (sss ! i, (ss @ Dâ¨r â Ïâ© # ts) ! i) â (srstep â± â)â§*" for i
using inv * l lc funas **
by (auto simp: nth_append_Cons simp del: ** * split!: if_splits)
then show ?thesis using inv l lc * unfolding c
by auto
qed
qed

lemma rstep_to_pos_replace:
assumes "(s, t) â rstep â"
shows "â p l r Ï. p â poss s â§ (l, r) â â â§ s |_ p = l â Ï â§ t = s[p â r â Ï]"
proof -
from assms obtain C l r Ï where st: "(l, r) â â" "s = Câ¨l â Ïâ©" "t = Câ¨r â Ïâ©"
using rstep_imp_C_s_r by fastforce
from st(2, 3) have *: "t = s[hole_pos C â r â Ï]" by simp
from this st show ?thesis unfolding *
by (intro exI[of _ "hole_pos C"]) auto
qed

lemma pos_replace_to_rstep:
assumes "p â poss s" "(l, r) â â"
and "s |_ p = l â Ï" "t = s[p â r â Ï]"
shows "(s, t) â rstep â"
using assms(1, 3-) replace_term_at_subt_at_id [of s p]
by (intro rstepI[OF assms(2), of s "ctxt_at_pos s p" Ï])

end

# Theory Replace_Constant

theory Replace_Constant
imports Rewriting
begin

subsection â¹Removing/Replacing constants in a rewrite sequence that do not appear in the rewrite systemâº
lemma funas_term_const_subst_conv:
"(c, 0) â funas_term l â· Â¬ (l âµ constT c)"
proof (induct l)
case (Fun f ts) then show ?case
by auto (metis Fun_supt supteq_supt_conv term.inject(2))+

lemma fresh_const_single_step_replace:
assumes lin: "linear_sys â" and fresh: "(c, 0) â funas_rel â"
and occ: "p â poss_of_term (constT c) s" and step: "(s, t) â rstep â"
shows "(s[p â u], t) â rstep â â¨
(â q. q â poss_of_term (constT c) t â§ (s[p â u], t[q â u]) â rstep â)"
proof -
from occ have const: "p â poss s â§ s |_ p = constT c" by auto
from step obtain C l r Ï where t [simp]: "s = Câ¨l â Ïâ©" "t = Câ¨r â Ïâ©"
and rule: "(l, r) â â" by blast
from rule lin have lin: "linear_term l" "linear_term r" by fastforce+
from fresh rule have nt_lhs: "(c, 0) â funas_term l" by (auto simp: funas_rel_def)
consider (par) "p â¥ (hole_pos C)" | (below) "hole_pos C â¤â©p p" using occ
by (auto dest: poss_of_term_const_ctxt_apply)
then show ?thesis
proof cases
case par
then have possc: "p â possc C" using const t possc_def by blast
then have "p â poss_of_term (constT c) t" "(s[p â u], t[p â u]) â rstep â"
using const par_hole_pos_replace_term_context_at[OF par]
using possc_subt_at_ctxt_apply[OF possc par, of "r â Ï" "l â Ï"] rule
by auto (metis par par_pos_replace_pres replace_at_hole_pos)
then show ?thesis by blast
next
case below
then obtain q where [simp]:"p = hole_pos C @ q" and poss: "q â poss (l â Ï)"
using const position_less_eq_def
by (metis (full_types) ctxt_at_pos_hole_pos ctxt_at_pos_subt_at_pos poss_append_poss t(1))
have const: "l â Ï |_ q = constT c" using const by auto
from nt_lhs have "â r. r â varposs l â§ r â¤â©p q" using const poss
proof (induct l arbitrary: q)
case (Var x)
then show ?case by auto
next
case (Fun f ts)
from Fun(1)[OF nth_mem, of "hd q" "tl q"] Fun(2-) obtain r where
"r â varposs (ts ! hd q) â§ r â¤â©p tl q"
by (cases q) auto
then show ?case using Fun(2- 4)
by (intro exI[of _ "hd q # r"]) auto
qed
then obtain x v where varposs: "v â varposs l" "v â¤â©p q" "l |_ v = Var x"
unfolding varposs_def by blast
let ?Ï = "Î»x. if Var x = l |_ v then (Ï x)[q -â©p v â u] else Ï x"
show ?thesis
proof (cases "x â vars_term r")
case True
then obtain q' where varposs_r: "q' â varposs r" "r |_ q' = Var x"
by (metis vars_term_varposs_iff)
have "(s[p â u], t[(hole_pos C) @ q' @ (q -â©p v) â u]) â rstep â"
using lin varposs rule varposs_r
by (auto simp: linear_term_varposs_subst_replace_term intro!: rstep_ctxtI)
(smt (verit, ccfv_SIG) pos_diff_append_itself rrstep.intros rrstep_rstep_mono subset_eq term_subst_eq)
moreover have "(hole_pos C) @ q' @ q -â©p v â poss_of_term (constT c) t"
using varposs_r varposs poss const poss_pos_diffI[OF varposs(2) poss]
using subt_at_append_dist[of q' "q -â©p v" "r â Ï"]
by (auto simp: poss_append_poss varposs_imp_poss[THEN subst_subt_at_dist] varposs_imp_poss[THEN subsetD[OF subst_poss_mono]])
(metis pos_les_eq_append_diff subst_apply_term.simps(1) subst_subt_at_dist subt_at_append_dist varposs_imp_poss)
ultimately show ?thesis by auto
next
case False
then have [simp]: "r â Ï = r â ?Ï" using varposs
have "(s[p â u], t) â rstep â" using rule varposs lin
by (auto simp: linear_term_varposs_subst_replace_term)
then show ?thesis by auto
qed
qed
qed

lemma fresh_const_steps_replace:
assumes lin: "linear_sys â" and fresh: "(c, 0) â funas_rel â"
and occ: "p â poss_of_term (constT c) s" and steps: "(s, t) â (rstep â)â§+"
shows "(s[p â u], t) â (rstep â)â§+ â¨
(â q. q â poss_of_term (constT c) t â§ (s[p â u], t[q â u]) â (rstep â)â§+)"
using steps occ
proof (induct arbitrary: p rule: converse_trancl_induct)
case (base s)
from fresh_const_single_step_replace[OF lin fresh base(2, 1)] show ?case
by (meson r_into_trancl')
next
case (step s t)
from fresh_const_single_step_replace[OF lin fresh step(4, 1)]
consider (a) "(s[p â u], t) â rstep â" | (b) "âq. q â poss_of_term (constT c) t â§ (s[p â u], t[q â u]) â rstep â" by blast
then show ?case
proof cases
case a then show ?thesis using step(2)
by auto
next
case b
then obtain q where "q â poss_of_term (constT c) t" "(s[p â u], t[q â u]) â rstep â" by blast
from step(3)[OF this(1)] this(2) show ?thesis
by (metis trancl_into_trancl2)
qed
qed

lemma remove_const_lhs_steps:
assumes lin: "linear_sys â" and fresh: "(c, 0) â funas_rel â"
and const: "(c, 0) â funas_term t"
and pos: "p â poss_of_term (constT c) s"
and steps: "(s, t) â (rstep â)â§+"
shows "(s[p â u], t) â (rstep â)â§+" using steps pos const fresh_const_steps_replace
by (metis fresh funas_term_const_subst_conv lin poss_of_termE subt_at_imp_supteq)

text â¹Now we can show that we may remove a constant substitutionâº

definition const_replace_closed where
"const_replace_closed c U = (â s t u p.
p â poss_of_term (constT c) s â¶ (s, t) â U â¶
(â q. q â poss_of_term (constT c) t â§ (s[p â u], t[q â u]) â U) â¨ (s[p â u], t) â U)"

lemma const_replace_closedD:
assumes "const_replace_closed c U" "p â poss_of_term (constT c) s" "(s, t) â U"
shows "(s[p â u], t) â U â¨ (â q. q â poss_of_term (constT c) t â§ (s[p â u], t[q â u]) â U)" using assms
unfolding const_replace_closed_def by blast

lemma const_replace_closedI:
assumes "â s t u p. p â poss_of_term (constT c) s â¹ (s, t) â U â¹
(â q. q â poss_of_term (constT c) t â§ (s[p â u], t[q â u]) â U) â¨ (s[p â u], t) â U"
shows "const_replace_closed c U" using assms
unfolding const_replace_closed_def
by auto

abbreviation const_subst :: "'f â 'v â ('f, 'v) Term.term" where
"const_subst c â¡ (Î» x. Fun c [])"

lemma lin_fresh_rstep_const_replace_closed:
"linear_sys â â¹ (c, 0) â funas_rel â â¹ const_replace_closed c (rstep â)"
using fresh_const_single_step_replace[of â c]
by (intro const_replace_closedI) (auto simp: constT_nfunas_term_poss_of_term_empty, blast)

lemma const_replace_closed_symcl:
"const_replace_closed c U â¹ const_replace_closed c (Uâ§=)"
unfolding const_replace_closed_def
by (metis Un_iff pair_in_Id_conv)

lemma const_replace_closed_trancl:
"const_replace_closed c U â¹ const_replace_closed c (Uâ§+)"
proof (intro const_replace_closedI)
fix s t u p
assume const: "const_replace_closed c U" and wit: "p â poss_of_term (constT c) s"
and steps :"(s, t) â Uâ§+"
show "(âq. q â poss_of_term (constT c) t â§ (s[p â u], t[q â u]) â Uâ§+) â¨ (s[p â u], t) â Uâ§+" using steps wit
proof (induct arbitrary: p rule: converse_trancl_induct)
case (base s)
show ?case using const_replace_closedD[OF const base(2, 1)]
by blast
next
case (step s v)
from const_replace_closedD[OF const step(4, 1)]
consider (a) "(s[p â u], v) â U" | (b) "â q. q â poss_of_term (constT c) v â§ (s[p â u], v[q â u]) â U" by auto
then show ?case
proof cases
case a then show ?thesis using step(2)
by (meson trancl_into_trancl2)
next
case b
then show ?thesis using step(3, 4) by (meson trancl_into_trancl2)
qed
qed
qed

lemma const_replace_closed_rtrancl:
"const_replace_closed c U â¹ const_replace_closed c (Uâ§*)"
proof (intro const_replace_closedI)
fix s t u p
assume const: "const_replace_closed c U" and wit: "p â poss_of_term (constT c) s"
and steps :"(s, t) â Uâ§*"
show "(âq. q â poss_of_term (constT c) t â§ (s[p â u], t[q â u]) â Uâ§*) â¨ (s[p â u], t) â Uâ§*"
using const_replace_closed_trancl[OF const] wit steps
by (metis const_replace_closedD rtrancl_eq_or_trancl)
qed

lemma const_replace_closed_relcomp:
"const_replace_closed c U â¹ const_replace_closed c V â¹ const_replace_closed c (U O V)"
proof (intro const_replace_closedI)
fix s t u p
assume const: "const_replace_closed c U" "const_replace_closed c V"
and wit: "p â poss_of_term (constT c) s" and step: "(s, t) â U O V"
from step obtain w where w: "(s, w) â U" "(w, t) â V" by auto
from const_replace_closedD[OF const(1) wit this(1)]
consider (a) "(s[p â u], w) â U" | (b) "(âq. q â poss_of_term (constT c) w â§ (s[p â u], w[q â u]) â U)"
by auto
then show "(âq. q â poss_of_term (constT c) t â§ (s[p â u], t[q â u]) â U O V) â¨ (s[p â u], t) â U O V"
proof cases
case a
then show ?thesis using w(2) by auto
next
case b
then show ?thesis using const_replace_closedD[OF const(2) _ w(2)]
by (meson relcomp.simps)
qed
qed

text â¹@{const const_replace_closed} allow the removal of a fresh constant substitutionâº
lemma const_replace_closed_remove_subst_lhs:
assumes repcl: "const_replace_closed c U"
and const: "(c, 0) â funas_term t"
and steps: "(s â const_subst c, t) â U"
shows "(s, t) â U" using steps
proof (induct "card (varposs s)" arbitrary: s)
case (Suc n)
obtain p ps where vl: "varposs s = insert p ps" "p â ps" using Suc(2)
by (metis card_le_Suc_iff dual_order.refl)
let ?s = "s[p â Fun c []]" have vp: "p â varposs s" using vl by auto
then have [simp]: "?s â const_subst c = s â const_subst c"
by (induct s arbitrary: p) (auto simp: nth_list_update map_update intro!: nth_equalityI)
have "varposs ?s = ps" using vl varposs_ground_replace_at[of p s "constT c"]
by auto
then have "n = card (varposs ?s)" using vl Suc(2) by (auto simp: card_insert_if finite_varposs)
from Suc(1)[OF this] have IH: "(s[p â constT c], t) â U" "p â poss_of_term (constT c) s[p â constT c]"
using Suc(2, 3) vl poss_of_term_replace_term_at varposs_imp_poss vp
using â¹s[p â constT c] â const_subst c = s â const_subst câº
by fastforce+
show ?case using const_replace_closedD[OF repcl] const IH(2, 1)
by (metis constT_nfunas_term_poss_of_term_empty empty_iff replace_term_at_same_pos replace_term_at_subt_at_id)
qed (auto simp: ground_subst_apply card_eq_0_iff finite_varposs varposs_empty_gound)

subsubsection â¹Removal lemma applied to various rewrite relationsâº

lemma remove_const_subst_step_lhs:
assumes lin: "linear_sys â" and fresh: "(c, 0) â funas_rel â"
and const: "(c, 0) â funas_term t"
and step: "(s â const_subst c, t) â (rstep â)"
shows "(s, t) â (rstep â)"
using lin_fresh_rstep_const_replace_closed[OF lin fresh, THEN const_replace_closed_remove_subst_lhs] const step
by blast

lemma remove_const_subst_steps_lhs:
assumes lin: "linear_sys â" and fresh: "(c, 0) â funas_rel â"
and const: "(c, 0) â funas_term t"
and steps: "(s â const_subst c, t) â (rstep â)â§+"
shows "(s, t) â (rstep â)â§+"
using lin_fresh_rstep_const_replace_closed[THEN const_replace_closed_trancl,
OF lin fresh, THEN const_replace_closed_remove_subst_lhs]
using const steps
by blast

lemma remove_const_subst_steps_eq_lhs:
assumes lin: "linear_sys â" and fresh: "(c, 0) â funas_rel â"
and const: "(c, 0) â funas_term t"
and steps: "(s â const_subst c, t) â (rstep â)â§*"
shows "(s, t) â (rstep â)â§*" using steps const
by (cases "s = t") (auto simp: rtrancl_eq_or_trancl funas_term_subst ground_subst_apply vars_term_empty_ground
dest: remove_const_subst_steps_lhs[OF lin fresh const] split: if_splits)

lemma remove_const_subst_steps_rhs:
assumes lin: "linear_sys â" and fresh: "(c, 0) â funas_rel â"
and const: "(c, 0) â funas_term s"
and steps: "(s, t â const_subst c) â (rstep â)â§+"
shows "(s, t) â (rstep â)â§+"
proof -
from steps have revs: "(t â const_subst c, s) â (rstep (âÂ¯))â§+"
unfolding rew_converse_outwards by auto
have "(t, s) â (rstep (âÂ¯))â§+" using assms
by (intro remove_const_subst_steps_lhs[OF _ _ _ revs]) (auto simp: funas_rel_def)
then show ?thesis unfolding rew_converse_outwards by auto
qed

lemma remove_const_subst_steps_eq_rhs:
assumes lin: "linear_sys â" and fresh: "(c, 0) â funas_rel â"
and const: "(c, 0) â funas_term s"
and steps: "(s, t â const_subst c) â (rstep â)â§*"
shows "(s, t) â (rstep â)â§*"
using steps const
by (cases "s = t") (auto simp: rtrancl_eq_or_trancl funas_term_subst ground_subst_apply vars_term_empty_ground
dest!: remove_const_subst_steps_rhs[OF lin fresh const] split: if_splits)

text â¹Main lemmasâº
lemma const_subst_eq_ground_eq:
assumes "s â const_subst c = t â const_subst d" "c â  d"
and "(c, 0) â funas_term t" "(d, 0) â funas_term s"
shows "s = t" using assms
proof (induct s arbitrary: t)
case (Var x) then show ?case by (cases t) auto
next
case (Fun f ts)
from Fun(2-) obtain g us where [simp]: "t = Fun g us" by (cases t) auto
have [simp]: "g = f" and l: "length ts = length us" using Fun(2)
by (auto intro: map_eq_imp_length_eq)
have "i < length ts â¹ ts ! i = us ! i" for i
using Fun(1)[OF nth_mem, of i "us ! i" for i] Fun(2-) l
by (auto simp: map_eq_conv')
then show ?case using l
by (auto intro: nth_equalityI)
qed

lemma remove_const_subst_steps:
assumes "linear_sys â" and  "(c, 0) â funas_rel â" and "(d, 0) â funas_rel â"
and "c â  d" "(c, 0) â funas_term t" "(d, 0) â funas_term s"
and "(s â const_subst c, t â const_subst d) â (rstep â)â§*"
shows "(s, t) â (rstep â)â§*"
proof (cases "s â const_subst c = t â const_subst d")
case True
from const_subst_eq_ground_eq[OF this] assms(4 - 6) show ?thesis by auto
next
case False
then have step: "(s â const_subst c, t â const_subst d) â (rstep â)â§+" using assms(7)
by (auto simp: rtrancl_eq_or_trancl)
then have "(s, t â const_subst d) â (rstep â)â§+" using assms
by (intro remove_const_subst_steps_lhs[OF _ _ _ step]) (auto simp: funas_term_subst)
from remove_const_subst_steps_rhs[OF _ _ _ this] show ?thesis using assms
by auto
qed

lemma remove_const_subst_relcomp_lhs:
assumes sys: "linear_sys â" "linear_sys ð®"
and fr: "(c, 0) â funas_rel â" and fs:"(c, 0) â funas_rel ð®"
and funas: "(c, 0) â funas_term t"
and seq: "(s â const_subst c, t) â (rstep â)â§* O (rstep ð®)â§*"
shows "(s, t) â (rstep â)â§* O (rstep ð®)â§*" using seq
using lin_fresh_rstep_const_replace_closed[OF sys(1) fr, THEN const_replace_closed_rtrancl]
using lin_fresh_rstep_const_replace_closed[OF sys(2) fs, THEN const_replace_closed_rtrancl]
using const_replace_closed_relcomp
by (intro const_replace_closed_remove_subst_lhs[OF _ funas seq]) force

lemma remove_const_subst_relcomp_rhs:
assumes sys: "linear_sys â" "linear_sys ð®"
and fr: "(c, 0) â funas_rel â" and fs:"(c, 0) â funas_rel ð®"
and funas: "(c, 0) â funas_term s"
and seq: "(s, t â const_subst c) â (rstep â)â§* O (rstep ð®)â§*"
shows "(s, t) â (rstep â)â§* O (rstep ð®)â§*"
proof -
from seq have "(t â const_subst c,s) â ((rstep â)â§* O (rstep ð®)â§*)Â¯"
by auto
then have "(t â const_subst c,s) â ((rstep ð®)â§*)Â¯ O ((rstep â)â§*)Â¯"
using converse_relcomp by blast
note seq = this[unfolded rtrancl_converse[symmetric] rew_converse_inwards]
from sys fr fs have "linear_sys (ð®Â¯)" "linear_sys (âÂ¯)" "(c, 0) â funas_rel (ð®Â¯)" "(c, 0) â funas_rel (âÂ¯)"
by (auto simp: funas_rel_def)
from remove_const_subst_relcomp_lhs[OF this funas seq]
have "(t, s) â (rstep (ð®Â¯))â§* O (rstep (âÂ¯))â§*" by simp
then show ?thesis
unfolding rew_converse_outwards converse_relcomp[symmetric]
by simp
qed

lemma remove_const_subst_relcomp:
assumes sys: "linear_sys â" "linear_sys ð®"
and fr: "(c, 0) â funas_rel â" "(d, 0) â funas_rel â"
and fs:"(c, 0) â funas_rel ð®" "(d, 0) â funas_rel ð®"
and diff: "c â  d" and funas: "(c, 0) â funas_term t" "(d, 0) â funas_term s"
and seq: "(s â const_subst c, t â const_subst d) â (rstep â)â§* O (rstep ð®)â§*"
shows "(s, t) â (rstep â)â§* O (rstep ð®)â§*"
proof -
from diff funas(1) have *: "(c, 0) â funas_term (t â const_subst d)"
by (auto simp: funas_term_subst)
show ?thesis using remove_const_subst_relcomp_rhs[OF sys fr(2) fs(2) funas(2)
remove_const_subst_relcomp_lhs[OF sys fr(1) fs(1) * seq]]
by blast
qed

end
d>

# Theory Rewriting_Properties

section â¹Confluence related rewriting propertiesâº
theory Rewriting_Properties
imports Rewriting
"Abstract-Rewriting.Abstract_Rewriting"
begin

subsection â¹Confluence related ARS propertiesâº
definition "SCR_on r A â¡ (âa â A. â b c. (a, b) â r â§ (a, c) â r â¶
(â d. (b, d) â râ§= â§  (c, d) â râ§*))"

abbreviation SCR :: "'a rel â bool" where "SCR r â¡ SCR_on r UNIV"

definition NFP_on :: "'a rel â 'a set â bool" where
"NFP_on r A â· (âaâA. âb c. (a, b) â râ§* â§ (a, c) â râ§! â¶ (b, c) â râ§*)"

abbreviation NFP :: "'a rel â bool" where "NFP r â¡ NFP_on r UNIV"

definition CE_on :: "'a rel â 'a rel â 'a set â bool" where
"CE_on r s A â· (âaâA. âb. (a, b) â râ§ââ§* â· (a, b) â sâ§ââ§*)"

abbreviation CE :: "'a rel â 'a rel â bool" where "CE r s â¡ CE_on r s UNIV"

definition NE_on :: "'a rel â 'a rel â 'a set â bool" where
"NE_on r s A â· (âaâA. âb. (a, b) â râ§! â· (a, b) â sâ§!)"

abbreviation NE :: "'a rel â 'a rel â bool" where "NE r s â¡ NE_on r s UNIV"

subsection â¹Signature closure of relation to model multihole context closureâº

(* AUX lemmas *)

lemma all_ctxt_closed_sig_rsteps [intro]:
fixes â :: "('f,'v) term rel"
shows "all_ctxt_closed â± ((srstep â± â)â§*)" (is "all_ctxt_closed _ (?Râ§*)")
proof (rule trans_ctxt_sig_imp_all_ctxt_closed)
fix C :: "('f,'v) ctxt" and s t :: "('f,'v)term"
assume C: "funas_ctxt C â â±"
and s: "funas_term s â â±"
and t: "funas_term t â â±"
and steps: "(s,t) â ?Râ§*"
from steps
proof (induct)
case (step t u)
from step(2) have tu: "(t,u) â rstep â" and t: "funas_term t â â±" and u: "funas_term u â â±"
by (auto dest: srstepD)
have "(C â¨ t â©, C â¨ u â©) â ?R" by (rule sig_stepI[OF _ _ rstep_ctxtI[OF tu]], insert C t u, auto)
with step(3) show ?case by auto
qed auto
qed (auto intro: trans_rtrancl)

lemma sigstep_trancl_funas:
"(s, t) â (srstep â± ð®)â§* â¹ s â  t â¹ funas_term s â â±"
"(s, t) â (srstep â± ð®)â§* â¹ s â  t â¹ funas_term t â â±"
by (auto simp: rtrancl_eq_or_trancl dest: srstepsD)

lemma srrstep_to_srestep:
"(s, t) â srrstep â± â â¹ (s, t) â srstep â± â"
by (meson in_mono rrstep_rstep_mono sig_step_mono2)

lemma srsteps_with_root_step_srstepsD:
"(s, t) â srsteps_with_root_step â± â â¹ (s, t) â (srstep â± â)â§+"
by (auto dest: srrstep_to_srestep simp: srsteps_with_root_step_def)

lemma srsteps_with_root_step_sresteps_eqD:
"(s, t) â srsteps_with_root_step â± â â¹ (s, t) â (srstep â± â)â§*"
by (auto dest: srrstep_to_srestep simp: srsteps_with_root_step_def)

lemma symcl_srstep_conversion:
"(s, t) â srstep â± (ââ§â) â¹ (s, t) â (srstep â± â)â§ââ§*"
by (simp add: conversion_def rstep_converse_dist srstep_symcl_dist)

lemma symcl_srsteps_conversion:
"(s, t) â (srstep â± (ââ§â))â§* â¹ (s, t) â (srstep â± â)â§ââ§*"
by (simp add: conversion_def rstep_converse_dist srstep_symcl_dist)

lemma NF_srstep_args:
assumes "Fun f ss â NF (srstep â± â)" "funas_term (Fun f ss) â â±" "i < length ss"
shows "ss ! i â NF (srstep â± â)"
proof (rule ccontr)
assume "ss ! i â NF (srstep â± â)"
then obtain t where step: "(ss ! i, t) â rstep â" "funas_term t â â±"
by (auto simp: NF_def sig_step_def)
from assms(3) have [simp]: "Suc (length ss - Suc 0) = length ss" by auto
from rstep_ctxtI[OF step(1), where ?C = "ctxt_at_pos (Fun f ss)[i]"]
have "(Fun f ss, Fun f (ss[i := t])) â srstep â± â" using step(2) assms(2, 3)
by (auto simp: sig_step_def upd_conv_take_nth_drop min_def UN_subset_iff
dest: in_set_takeD in_set_dropD simp flip: id_take_nth_drop)
then show False using assms(1)
by (auto simp: NF_def)
qed

lemma all_ctxt_closed_srstep_conversions [simp]:
"all_ctxt_closed â± ((srstep â± â)â§ââ§*)"

(* END AUX *)

lemma NFP_stepD:
"NFP r â¹ (a, b) â râ§* â¹ (a, c) â râ§* â¹ c â NF r â¹ (b, c) â râ§*"
by (auto simp: NFP_on_def)

lemma NE_symmetric: "NE r s â¹ NE s r"
unfolding NE_on_def by auto

lemma CE_symmetric: "CE r s â¹ CE s r"
unfolding CE_on_def by auto

text â¹Reducing the quantification over rewrite sequences for properties @{const CR} ... to
rewrite sequences containing at least one root stepâº
lemma all_ctxt_closed_sig_reflE:
"all_ctxt_closed â± â â¹ funas_term t â â± â¹ (t, t) â â"
proof (induct t)
case (Fun f ts)
from Fun(1)[OF nth_mem  Fun(2)] Fun(3)
have "i < length ts â¹ funas_term (ts ! i) â â±" "i < length ts â¹ (ts ! i, ts ! i) â â" for i
by (auto simp: SUP_le_iff)
then show ?case using all_ctxt_closedD[OF Fun(2)] Fun(3)
by simp

lemma all_ctxt_closed_relcomp [intro]:
"(â s t. (s, t) â â â¹ s â  t â¹ funas_term s â â± â§ funas_term t â â±) â¹
(â s t. (s, t) â ð® â¹ s â  t â¹ funas_term s â â± â§ funas_term t â â±) â¹
all_ctxt_closed â± â â¹ all_ctxt_closed â± ð® â¹ all_ctxt_closed â± (â O ð®)"
proof -
assume funas:"(â s t. (s, t) â â â¹ s â  t â¹ funas_term s â â± â§ funas_term t â â±)"
"(â s t. (s, t) â ð® â¹ s â  t â¹ funas_term s â â± â§ funas_term t â â±)"
and ctxt_cl: "all_ctxt_closed â± â" "all_ctxt_closed â± ð®"
{fix f ss ts assume ass: "(f, length ss) â â±" "length ss = length ts" "â i. i < length ts â¹ (ss ! i, ts ! i) â (â O ð®)"
"â i . i < length ts â¹ funas_term (ts ! i) â â±" "âi. i < length ts â¹ funas_term (ss ! i) â â±"
from ass(2, 3) obtain us where us: "length us = length ts" "â i. i < length ts â¹ (ss ! i, us ! i) â â"
"â i. i < length ts â¹ (us ! i, ts ! i) â ð®"
using Ex_list_of_length_P[of "length ts" "Î» x i. (ss ! i, x) â â â§ (x, ts ! i) â ð®"]
by auto
from funas have fu: "â i . i < length us â¹ funas_term (us ! i) â â±" using us ass(4, 5)
by (auto simp: funas_rel_def) (metis in_mono)
have "(Fun f ss, Fun f us) â â" using ass(1, 2, 5) us(1, 2) fu
by (intro all_ctxt_closedD[OF ctxt_cl(1), of f]) auto
moreover have "(Fun f us, Fun f ts) â ð®"  using ass(1, 2, 4) us(1, 3) fu
by (intro all_ctxt_closedD[OF ctxt_cl(2), of f]) auto
ultimately have "(Fun f ss, Fun f ts) â â O ð®" by auto}
moreover
{fix x have "(Var x, Var x) â â" "(Var x, Var x) â ð®" using ctxt_cl
by (auto simp: all_ctxt_closed_def)
then have "(Var x, Var x) â â O ð®" by auto}
ultimately show ?thesis by (auto simp: all_ctxt_closed_def)
qed

abbreviation "prop_to_rel P â¡ {(s, t)| s t. P s t}"

abbreviation "prop_mctxt_cl â± P â¡ all_ctxt_closed â± (prop_to_rel P)"

lemma prop_mctxt_cl_Var:
"prop_mctxt_cl â± P â¹ P (Var x) (Var x)"

lemma prop_mctxt_cl_refl_on:
"prop_mctxt_cl â± P â¹ funas_term t â â± â¹ P t t"
using all_ctxt_closed_sig_reflE by blast

lemma prop_mctxt_cl_reflcl_on:
"prop_mctxt_cl â± P â¹ funas_term s â â± â¹ P s s"
using all_ctxt_closed_sig_reflE by blast

lemma reduction_relations_to_root_step:
assumes "â s t. (s, t) â srsteps_with_root_step â± â â¹ P s t"
and cl: "prop_mctxt_cl â± P"
and well: "funas_term s â â±" "funas_term t â â±"
and steps: "(s, t) â (srstep â± â)â§*"
shows "P s t" using steps well
proof (induct s arbitrary: t)
case (Var x)
have "(Var x, t) â (srstep â± â)â§+ â¹ (Var x, t) â srsteps_with_root_step â± â"
using nsrsteps_with_root_step_step_on_args by blast
from assms(1)[OF this] show ?case using Var cl
by (auto simp: rtrancl_eq_or_trancl dest: all_ctxt_closed_sig_reflE)
next
case (Fun f ss) note IH = this show ?case
proof (cases "Fun f ss = t")
case True show ?thesis using IH(2, 4) unfolding True
by (intro prop_mctxt_cl_reflcl_on[OF cl]) auto
next
case False
then have step: "(Fun f ss, t) â (srstep â± â)â§+" using IH(2)
by (auto simp: refl rtrancl_eq_or_trancl)
show ?thesis
proof (cases "(Fun f ss, t) â srsteps_with_root_step â± â")`