theory Rew_Seq
imports Sequence TRS.Signature_Extension Term_Auxx
begin
lemma filter_idx_split:
assumes "Suc i < length (filter P xs)"
shows "∃ bef mid aft. xs = bef @ filter P xs ! i # mid @ filter P xs ! Suc i # aft ∧ (∀ x ∈ set mid. ¬ P x)"
using assms
proof (induct xs arbitrary: i rule: rev_induct)
case (snoc x xs) note IH = this show ?case
proof (cases "Suc i < length (filter P xs)")
case True
then obtain bef mid aft where
xs: "xs = bef @ filter P xs ! i # mid @ filter P xs ! Suc i # aft" and
inv: "∀x∈set mid. ¬ P x" using IH(1)[of i]
by auto
from xs True have *: "xs @ [x] = bef @ filter P (xs @ [x]) ! i # mid @ filter P (xs @ [x]) ! Suc i # (aft @ [x])"
by (auto simp: nth_append)
then show ?thesis using inv by blast
next
case False
then have i: "Suc i = length (filter P xs)" and Px: "P x" using IH(2) by (auto split:if_splits)
from i IH(2) have [simp]: "filter P xs ≠ []" by auto
have *: "filter P xs ! i = last (filter P xs)" using IH(2) i
by (auto simp: last_conv_nth intro!: arg_cong2[where ?f = "(!)"])
from filter_eq_Cons_iff[of P "rev xs" "hd (filter P (rev xs))" "tl (filter P (rev xs))"]
obtain us vs where rev_xs: "rev xs = us @ hd (filter P (rev xs)) # vs" and inv: "∀ u ∈set us. ¬ P u"
by (auto simp flip: rev_filter)
from arg_cong[OF rev_xs, of rev] have "xs @ [x] = rev vs @ last (filter P xs) # rev us @ [x]"
by (auto simp flip: rev_filter simp: hd_rev)
then show ?thesis using Px i inv
by (simp add: * nth_append)
(metis ‹xs @ [x] = rev vs @ last (filter P xs) # rev us @ [x]› set_rev)
qed
qed auto
lemma nthWhile_mctxt_of_ctxt [simp]:
"length (takeWhile (λC. num_holes C = 0) (map mctxt_of_term ss @ mctxt_of_ctxt C # ts)) = length ss"
by (induct ss) auto
lemma sum_list_nthWhile_length [simp]:
"sum_list (map num_holes Cs) = Suc 0 ⟹ length (takeWhile (λC. num_holes C = 0) Cs) < length Cs"
by (induct Cs) auto
lemma sum_list_nthWhile_bound [dest]:
"sum_list (map num_holes Ds) = Suc 0 ⟹ length Ds ≤ length (takeWhile (λC. num_holes C = 0) Ds) ⟹ False"
using leD sum_list_nthWhile_length by blast
lemma sum_list_nthWhile_wit:
"sum_list (map num_holes Ds) = Suc 0 ⟹ num_holes (Ds ! length (takeWhile (λC. num_holes C = 0) Ds)) = Suc 0"
by (smt elem_le_sum_list leD le_SucE length_map not_gr_zero nth_length_takeWhile nth_map sum_list_nthWhile_length)
fun ctxt_of_mctxt :: "('f, 'v) mctxt ⇒ ('f, 'v) ctxt" where
"ctxt_of_mctxt MHole = □"
| "ctxt_of_mctxt (MFun f Cs) = (let n = length (takeWhile (λ C. num_holes C = 0) Cs) in
(if n < length Cs then
More f (map term_of_mctxt (take n Cs)) (ctxt_of_mctxt (Cs ! n)) (map term_of_mctxt (drop (Suc n) Cs))
else undefined))"
lemma ctxt_of_mctxt_mctxt_of_ctxt [simp]:
"ctxt_of_mctxt (mctxt_of_ctxt C) = C"
by (induct C) (auto simp: Let_def comp_def nth_append)
lemma sum_list_1_E [elim]:
assumes "sum_list xs = Suc 0"
obtains i where "i < length xs" "xs ! i = Suc 0" "∀ j < length xs. j ≠ i ⟶ xs ! j = 0"
proof -
have "∃ i < length xs. xs ! i = Suc 0 ∧ (∀ j < length xs. j ≠ i ⟶ xs ! j = 0)" using assms
proof (induct xs)
case (Cons a xs) show ?case
proof (cases a)
case [simp]: 0
obtain i where "i < length xs" "xs ! i = Suc 0" "(∀ j < length xs. j ≠ i ⟶ xs ! j = 0)"
using Cons by auto
then show ?thesis using less_Suc_eq_0_disj
by (intro exI[of _ "Suc i"]) auto
next
case (Suc nat) then show ?thesis using Cons by auto
qed
qed auto
then show " (⋀i. i < length xs ⟹ xs ! i = Suc 0 ⟹ ∀j<length xs. j ≠ i ⟶ xs ! j = 0 ⟹ thesis) ⟹ thesis"
by blast
qed
lemma sum_list_1_I:
assumes "sum_list xs = Suc 0" "i < length xs" "xs ! i = Suc 0"
shows "⋀ j. j < length xs ⟹ j ≠ i ⟹ xs ! j = 0" using assms
by (metis sum_list_1_E)
lemma mctxt_of_ctxt_ctxt_of_mctxt:
"num_holes C = Suc 0 ⟹ mctxt_of_ctxt (ctxt_of_mctxt C) = C"
proof (induct C)
case (MFun f Cs)
then obtain i where nth: "i < length Cs" "i = length (takeWhile (λC. num_holes C = 0) Cs)"
using sum_list_nthWhile_length by auto
then have "0 < num_holes (Cs ! i)" unfolding nth(2)
using nth_length_takeWhile by blast
from nth(1) this have num: "num_holes (Cs ! i) = Suc 0" using MFun(2)
by (auto, metis Suc_lessI elem_le_sum_list leD length_map nth_map)
have "j < length Cs ⟹ j ≠ i ⟹ num_holes (Cs ! j) = 0" for j using num nth(1) MFun(2)
using sum_list_1_I
by (metis length_map nth_map num_holes.simps(3))
then have [simp]: "map (mctxt_of_term ∘ term_of_mctxt) (drop (Suc i) Cs) = drop (Suc i) Cs"
using MFun(2) nth(1) num
by (auto simp: comp_def intro!: nth_equalityI)
have [simp]: "map (mctxt_of_term ∘ term_of_mctxt) (take i Cs) = take i Cs"
using nth(1) unfolding nth(2) by (induct Cs) auto
show ?case using id_take_nth_drop[OF nth(1)]
by (auto simp: Let_def MFun(1)[OF nth_mem[OF nth(1)] num] simp flip: nth(2))
qed auto
lemma ctxt_of_mctxt_hole_dest:
"num_holes C = Suc 0 ⟹ ctxt_of_mctxt C = □ ⟹ C = MHole"
by (cases C) (auto simp: Let_def split!: if_splits)
lemma fill_holes_apply_ctxt:
"num_holes C = Suc 0 ⟹ fill_holes C [s] = (ctxt_of_mctxt C)⟨s⟩"
by (metis fill_holes_mctxt_of_ctxt mctxt_of_ctxt_ctxt_of_mctxt)
lemma partition_by_replicate0 [simp]:
"partition_by xs (replicate n 0 @ ys) = replicate n [] @ partition_by xs ys"
by (induct n) auto
lemma fill_holes_Nil [intro]:
"num_holes t = 0 ⟹ fill_holes t [] = term_of_mctxt t"
by (metis mctxt_of_term_fill_holes mctxt_of_term_term_of_mctxt_id)
lemma fill_holes_fill_holes_mctxt_MHole:
assumes "∀ s ∈ set ss. num_holes s = 0" "∀ t ∈ set ts. num_holes t = 0" "num_holes D = Suc (length ss + length ts)"
shows "fill_holes (fill_holes_mctxt D (ss @ MHole # ts)) [t] = fill_holes D (map term_of_mctxt ss @ t # map term_of_mctxt ts)" (is "?ls = ?rs")
proof -
have [simp]: "map num_holes ss = replicate (length ss) 0" "map num_holes ts = replicate (length ts) 0"
using assms(1, 2) by (auto intro: nth_equalityI)
have [simp]: "i < Suc (length ss + length ts) ⟹ ¬ i < length ss + length ts ⟹ ts ≠ [] ⟹ i ≠ length ss ⟹ i - Suc (length ss) = length ts - (Suc 0)" for i
by auto
have *: "map (λi. fill_holes ((ss @ MHole # ts) ! i) (partition_holes [t] (ss @ MHole # ts) ! i)) [0..<num_holes D] = map term_of_mctxt ss @ t # map term_of_mctxt ts"
using assms by (intro nth_equalityI) (auto simp: nth_append_Cons)
have inv: "length (ss @ MHole # ts) = num_holes D" "num_holes (fill_holes_mctxt D (ss @ MHole # ts)) = length [t]"
using assms by (auto simp: num_holes_fill_holes_mctxt)
show ?thesis unfolding fill_holes_mctxt_fill_holes[OF inv] * ..
qed
lemma funas_mctxt_mctxt_of_ctxt [simp]:
"funas_mctxt (mctxt_of_ctxt C) = funas_ctxt C"
by (induct C) auto
lemma funas_ctxt_of_mctxt [simp]:
"num_holes D = Suc 0 ⟹ funas_ctxt (ctxt_of_mctxt D) = funas_mctxt D"
by (metis funas_mctxt_mctxt_of_ctxt mctxt_of_ctxt_ctxt_of_mctxt)
datatype ('f, 'v) step = Apply (rules: "('f, 'v) term × ('f, 'v) term") (ctxt: "('f, 'v) ctxt") (subst: "'v ⇒ ('f, 'v) term")
type_synonym ('f, 'v) steps = "('f, 'v) step list"
definition "apply_left s ≡ (ctxt s)⟨(fst (rules s)) ⋅ (subst s)⟩"
definition "apply_right s ≡ (ctxt s)⟨(snd (rules s)) ⋅ (subst s)⟩"
abbreviation "apply_step s ≡ (apply_left s, apply_right s)"
lemmas apply_step_def = apply_right_def apply_left_def
definition "rev_step s ≡ Apply (prod.swap (rules s)) (ctxt s) (subst s)"
lemma rev_step_inverse_itself [simp]:
"rev_step (rev_step s) = s"
by (auto simp: rev_step_def)
lemma apply_step_rev_step [simp]:
"apply_left (rev_step s) = apply_right s"
"apply_right (rev_step s) = apply_left s"
by (auto simp: rev_step_def apply_step_def)
lemma rev_step_rules [simp]:
"rules (rev_step s) = prod.swap (rules s)"
by (auto simp: rev_step_def)
lemma map_rules_rev_step_commute:
"map rules (map rev_step us) = map prod.swap (map rules us)"
by auto
abbreviation "funas_tuple t ≡ funas_term (fst t) ∪ funas_term (snd t)"
definition "funas_step s = (let (l, r) = rules s in
funas_ctxt (ctxt s) ∪ funas_term l ∪ funas_term r ∪ (⋃ (funas_term ` (subst s) ` (vars_term l ∪ vars_term r))))"
lemma funas_apply_step_funas_step:
"funas_step s = funas_tuple (apply_step s)"
unfolding funas_step_def apply_step_def
by (cases s) (force simp add: funas_term_subst)
inductive_set rewrite_step :: "_ ⇒ _ ⇒ ('f, 'v) step set" for ℱ and R :: "('f, 'v) trs" where
rewrite_step [intro]: "⋀C σ l r. funas_step (Apply (l, r) C σ) ⊆ ℱ ⟹ (l, r) ∈ R ⟹ Apply (l, r) C σ ∈ rewrite_step ℱ R"
print_theorems
lemma rewrite_stepI [intro]:
"funas_tuple (apply_step s) ⊆ ℱ ⟹ rules s ∈ ℛ ⟹ s ∈ rewrite_step ℱ ℛ"
by (cases s) (auto simp: funas_apply_step_funas_step intro!: rewrite_step.intros)
lemma rewrite_stepI2 [intro]:
"funas_step s ⊆ ℱ ⟹ rules s ∈ ℛ ⟹ s ∈ rewrite_step ℱ ℛ"
by (cases s) (auto intro!: rewrite_step.intros)
lemma rewrite_step_mono:
"ℛ ⊆ 𝒮 ⟹ rewrite_step ℱ ℛ ⊆ rewrite_step ℱ 𝒮"
by (auto simp: funas_apply_step_funas_step elim!: rewrite_step.cases intro!: rewrite_stepI)
lemma funas_rewrite_step:
"s ∈ rewrite_step ℱ ℛ ⟹ funas_tuple (apply_step s) ⊆ ℱ"
by (auto simp: apply_step_def funas_apply_step_funas_step elim!: rewrite_step.cases)
lemma rewrite_step_rules [simp]:
"s ∈ rewrite_step ℱ ℛ ⟹ rules s ∈ ℛ"
by (auto elim!: rewrite_step.cases)
lemma rewrite_step_funas_ctxt [simp]:
"s ∈ rewrite_step ℱ ℛ ⟹ funas_ctxt (ctxt s) ⊆ ℱ"
by (auto simp: funas_step_def elim!: rewrite_step.cases)
lemma rewrite_step_funas_rule_l [simp]:
"s ∈ rewrite_step ℱ ℛ ⟹ funas_term (fst (rules s)) ⊆ ℱ"
by (auto simp: funas_step_def elim!: rewrite_step.cases)
lemma rewrite_step_funas_rule_r [simp]:
"s ∈ rewrite_step ℱ ℛ ⟹ funas_term (snd (rules s)) ⊆ ℱ"
by (auto simp: funas_step_def elim!: rewrite_step.cases)
lemma rewrite_step_inv:
"rev_step s ∈ rewrite_step ℱ (ℛ¯) ⟷ s ∈ rewrite_step ℱ ℛ"
using rewrite_step_rules[of s ℱ ℛ]
using rewrite_step_rules[of "rev_step s" ℱ "ℛ¯"]
by (auto simp: prod.swap_def dest: subsetD[OF funas_rewrite_step] intro!: rewrite_stepI)
lemma rewrite_step_impl_sig_rstep:
"s ∈ rewrite_step ℱ ℛ ⟹ apply_step s ∈ sig_step ℱ (rstep ℛ)"
by (auto simp: funas_apply_step_funas_step sig_step_def apply_step_def elim!: rewrite_step.cases)
lemma sig_rstep_impl_rewrite_step:
assumes "s ∈ sig_step ℱ (rstep ℛ)"
shows "∃ u ∈ rewrite_step ℱ ℛ. s = apply_step u"
proof -
obtain C l r σ where "s = (C⟨l ⋅ σ⟩, C⟨r ⋅ σ⟩)" "funas_tuple s ⊆ ℱ" "(l, r) ∈ ℛ"
using assms(1) by (auto simp: sig_step_def dest!: rstep_imp_C_s_r)
then show ?thesis
by (intro bexI[of _ "Apply (l, r) C σ"]) (auto simp: apply_step_def intro!: rewrite_stepI)
qed
lemma rewrite_step_sig_rstep_conv:
"sig_step ℱ (rstep ℛ) = apply_step ` rewrite_step ℱ ℛ"
using rewrite_step_impl_sig_rstep[of _ ℱ ℛ]
using sig_rstep_impl_rewrite_step[of _ ℱ ℛ]
by force+
definition "stepsP s t ⟷ apply_right s = apply_left t"
lemma stepsP_def': "stepsP s t ⟷ apply_left t = apply_right s" by (auto simp: stepsP_def)
abbreviation "rewrite_steps ℱ ℛ ≡ Sequence.sequence (rewrite_step ℱ ℛ) stepsP"
abbreviation "rewrite_steps_inv ℱ ℛ ≡ Sequence.sequence (rewrite_step ℱ (ℛ¯)) stepsP"
abbreviation "ground_steps ℱ ℛ ≡ Sequence.sequence {s. s ∈ rewrite_step ℱ ℛ ∧ ground (apply_left s) ∧ ground (apply_right s)} stepsP"
abbreviation "start_t xs ≡ apply_left (hd xs)"
abbreviation "end_t xs ≡ apply_right (last xs)"
abbreviation "steps_rel xs ≡ (start_t xs, end_t xs)"
lemma rewrite_steps_funasD:
"si ∈ rewrite_steps ℱ ℛ ⟹ s ∈ set si ⟹ funas_step s ⊆ ℱ"
by (metis funas_apply_step_funas_step funas_rewrite_step seq_in_I)
lemmas rewrite_steps_funas_stepD = rewrite_steps_funasD[unfolded funas_apply_step_funas_step]
lemma rewrite_steps_last_in_set:
"si ∈ rewrite_steps ℱ ℛ ⟹ last si ∈ set si"
by (metis last_in_set no_empty_seq(2))
lemma rewrite_steps_hd_in_set:
"si ∈ rewrite_steps ℱ ℛ ⟹ hd si ∈ set si"
by (metis hd_in_set no_empty_seq(2))
lemma rewrite_steps_rulesD:
"si ∈ rewrite_steps ℱ ℛ ⟹ s ∈ set si ⟹ rules s ∈ ℛ"
by (meson rewrite_step_rules seq_in_I)
lemma rev_step_idem [simp]: "rev_step ∘ rev_step = id" by auto
lemma rewrite_steps_to_inv_steps:
"xs ∈ rewrite_steps ℱ ℛ ⟹ rev (map rev_step xs) ∈ rewrite_steps ℱ (ℛ¯)"
by (induct rule: sequence_converse_induct)
(auto simp: hd_rev last_map stepsP_def rewrite_step_inv
intro!: sequence_ConsI)
lemma rewrite_steps_inv_to_steps:
"xs ∈ rewrite_steps ℱ (ℛ¯) ⟹ rev (map rev_step xs) ∈ rewrite_steps ℱ ℛ"
by (induct rule: sequence_converse_induct)
(auto simp: hd_rev last_map stepsP_def simp flip: rewrite_step_inv[of _ ℱ ℛ]
intro!: sequence_ConsI)
lemma rewrite_steps_inv_steps_conv1:
"xs ∈ rewrite_steps ℱ ℛ ⟷ rev (map rev_step xs) ∈ rewrite_steps ℱ (ℛ¯)"
using rewrite_steps_to_inv_steps[of xs ℱ ℛ]
using rewrite_steps_inv_to_steps[of "rev (map rev_step xs)" ℱ ℛ]
by (auto simp: rev_map)
lemma rewrite_steps_inv_steps_conv2:
"xs ∈ rewrite_steps ℱ (ℛ¯) ⟷ rev (map rev_step xs) ∈ rewrite_steps ℱ ℛ"
using rewrite_steps_inv_to_steps[of xs ℱ ℛ]
using rewrite_steps_to_inv_steps[of "rev (map rev_step xs)" ℱ ℛ]
by (auto simp: rev_map)
lemma start_t_rev_to_end_t [simp]:
"xs ≠ [] ⟹ start_t (rev (map rev_step xs)) = end_t xs"
by (auto simp: hd_rev last_map)
lemma end_t_rev_to_start_t [simp]:
"xs ≠ [] ⟹ end_t (rev (map rev_step xs)) = start_t xs"
by (auto simp: last_rev hd_map)
lemma rewrite_steps_impl_transcl_sig_rstep:
"xs ∈ rewrite_steps ℱ ℛ ⟹ steps_rel xs ∈ (sig_step ℱ (rstep ℛ))⇧+"
proof -
assume "xs ∈ rewrite_steps ℱ ℛ"
then have "(fst (apply_step (hd xs)), snd (apply_step (last xs))) ∈ (sig_step ℱ (rstep ℛ))⇧+"
by (intro sequence_hd_last_to_trancl[OF equalityD2[OF rewrite_step_sig_rstep_conv], where ?P = stepsP])
(auto simp: apply_step_def stepsP_def)
then show ?thesis by auto
qed
lemma sig_rsteps_to_rewrite_steps:
assumes "(s, t) ∈ (sig_step ℱ (rstep ℛ))⇧+"
shows "∃ xs ∈ rewrite_steps ℱ ℛ. (s, t) = steps_rel xs ∧
(∀i<length xs. apply_step (xs ! i) ∈ (sig_step ℱ (rstep ℛ)))"
using trancl_to_sequence[OF equalityD1[OF rewrite_step_sig_rstep_conv] _ assms, where ?P = stepsP]
by (auto simp: stepsP_def apply_step_def)
abbreviation "step_ctxt_udpate f s ≡ Apply (rules s) (f (ctxt s)) (subst s)"
abbreviation "step_subst_udpate f s ≡ Apply (rules s) (ctxt s) (f (subst s))"
lemma apply_step_cut_ctxt [simp]:
"p ≤⇩p hole_pos (ctxt s) ⟹ apply_right (step_ctxt_udpate (cut_ctxt (length p)) s) = apply_right s |_ p"
"p ≤⇩p hole_pos (ctxt s) ⟹ apply_left (step_ctxt_udpate (cut_ctxt (length p)) s) = apply_left s |_ p"
by (auto simp: apply_step_def cut_ctxt_apply_ctxt)
abbreviation "step_subst τ s ≡ Apply (rules s) (ctxt s ⋅⇩c τ) (subst s ∘⇩s τ)"
lemma step_subst_pres_stepP:
"stepsP st tu ⟹ stepsP (step_subst σ st) (step_subst σ tu)"
by (auto simp: stepsP_def apply_step_def)
(metis subst_apply_term_ctxt_apply_distrib)
lemma step_subst_pres_rewrite_step:
"s ∈ rewrite_step ℱ ℛ ⟹ (⋀ x. funas_term (σ x) ⊆ ℱ) ⟹ step_subst σ s ∈ rewrite_step ℱ ℛ"
by (auto simp: funas_apply_step_funas_step apply_step_def funas_term_subst elim!: rewrite_step.cases intro!: rewrite_stepI)+
lemma rewriting_subst_cl:
assumes "xs ∈ rewrite_steps ℱ ℛ" and "⋀ x. funas_term (σ x) ⊆ ℱ"
shows "map (step_subst σ) xs ∈ rewrite_steps ℱ ℛ" using assms
proof (induct)
case (trans_step st tu ys) then show ?case
by (auto simp: step_subst_pres_stepP intro!: sequence_ConsI[OF step_subst_pres_rewrite_step[OF trans_step(1)]])
qed (auto simp: step_subst_pres_rewrite_step)
lemma step_ctxt_pres_stepP:
"stepsP st tu ⟹ stepsP (step_ctxt_udpate ((∘⇩c) D) st) (step_ctxt_udpate ((∘⇩c) D) tu)"
by (auto simp: stepsP_def apply_step_def)
lemma step_cxtxt_pres_rewrite_step:
"s ∈ rewrite_step ℱ ℛ ⟹ (⋀ x. funas_ctxt D ⊆ ℱ) ⟹ step_ctxt_udpate ((∘⇩c) D) s ∈ rewrite_step ℱ ℛ"
by (auto simp: funas_apply_step_funas_step apply_step_def funas_term_subst elim!: rewrite_step.cases intro!: rewrite_stepI)+
lemma step_cxtxt_pres_rewrite_step':
"s ∈ rewrite_step ℱ ℛ ⟹ (⋀ x. funas_ctxt (f (ctxt s)) ⊆ ℱ) ⟹ step_ctxt_udpate f s ∈ rewrite_step ℱ ℛ"
by (auto simp: funas_apply_step_funas_step apply_step_def funas_term_subst elim!: rewrite_step.cases intro!: rewrite_stepI)+
lemma rewriting_ctxt_cl:
assumes "xs ∈ rewrite_steps ℱ ℛ" and "⋀ x. funas_ctxt D ⊆ ℱ"
shows "map (step_ctxt_udpate ((∘⇩c) D)) xs ∈ rewrite_steps ℱ ℛ" using assms
proof (induct)
case (trans_step st tu ys) then show ?case
by (auto simp: step_ctxt_pres_stepP intro!: sequence_ConsI[OF step_cxtxt_pres_rewrite_step[OF trans_step(1)]])
qed (auto simp: step_cxtxt_pres_rewrite_step)
lemma compose_sequences_union:
assumes "ss ∈ rewrite_steps ℱ ℛ" "ts ∈ rewrite_steps ℱ 𝒮" "end_t ss = start_t ts"
shows "ss @ ts ∈ rewrite_steps ℱ (ℛ ∪ 𝒮)" using assms
proof -
have "stepsP (ss ! (length ss - Suc 0)) (ts ! 0)" using assms
by (simp add: stepsP_def last_conv_nth[OF seq_not_NilD[OF assms(1)]] hd_conv_nth[OF seq_not_NilD[OF assms(2)]])
then show ?thesis using assms
using seq_property[OF assms(1)] seq_property[OF assms(2)]
apply (intro sequence_propI)
apply (auto simp add: rewrite_stepI2 rewrite_steps_funasD rewrite_steps_rulesD nth_append)
apply (metis One_nat_def Suc_lessI diff_Suc_1)
by (metis (no_types, lifting) Suc_diff_Suc Suc_lessD add_diff_inverse_nat add_less_cancel_left diff_Suc_Suc not_less_eq)
qed
lemma suffix_append_itself [simp]:
"suffix xs (ys @ xs) ⟷ True"
using suffixI by blast
lemma compose_sequences_split:
assumes "ss @ ts ∈ rewrite_steps ℱ (ℛ ∪ 𝒮)" "ss ≠ []" "ts ≠ []" "set (map rules ss) ⊆ ℛ" "set (map rules ts) ⊆ 𝒮"
shows "ss ∈ rewrite_steps ℱ ℛ" "ts ∈ rewrite_steps ℱ 𝒮"
proof -
have "ss ∈ rewrite_steps ℱ ℛ"
using assms seq_property[OF prefix_seq_in_seq[OF assms(1) _ assms(2)]]
using prefix_seq_in_seq[OF assms(1) _ assms(2)]
by (intro sequence_propI) (auto dest!: rewrite_steps_funas_stepD intro!: rewrite_stepI)
moreover have "ts ∈ rewrite_steps ℱ 𝒮"
using assms seq_property[OF suffix_seq_in_seq[OF assms(1) _ assms(3)]]
using seq_property[OF suffix_seq_in_seq[OF assms(1) _ assms(3)]]
by (intro sequence_propI) (auto dest: rewrite_steps_funas_stepD intro!: rewrite_stepI)
ultimately show "ss ∈ rewrite_steps ℱ ℛ" "ts ∈ rewrite_steps ℱ 𝒮" by simp_all
qed
end