Theory TRS.Q_Restricted_Rewriting
theory Q_Restricted_Rewriting
imports Sharp_Syntax
begin
subsection ‹Q-Restricted Rewriting›
definition NF_subst :: "bool ⇒ ('f, 'v) rule ⇒ ('f, 'v) subst ⇒ ('f, 'v) terms ⇒ bool"
where
"NF_subst b lr σ Q ⟷ (b ⟶ σ ` vars_rule lr ⊆ NF_terms Q)"
lemma NF_subst_False[simp]: "NF_subst False lr σ Q = True"
unfolding NF_subst_def by simp
lemma NF_subst_Empty[simp]: "NF_subst nfs lr σ {} = True"
unfolding NF_subst_def by simp
lemma NF_subst_right: "nfs ⟹ NF_subst nfs (s,t) σ Q ⟹ σ ` vars_term t ⊆ NF_terms Q"
unfolding NF_subst_def vars_rule_def by auto
lemma NF_substI[intro]: assumes "⋀ x . nfs ⟹ x ∈ vars_term l ∨ x ∈ vars_term r ⟹ σ x ∈ NF_terms Q"
shows "NF_subst nfs (l,r) σ Q"
unfolding NF_subst_def
proof (intro impI allI subsetI)
fix t
assume nfs and t: "t ∈ σ ` (vars_rule (l,r))"
then obtain x where t: "t = σ x" and x: "x ∈ vars_rule (l,r)" by auto
from x assms[OF ‹nfs›, of x] show "t ∈ NF_terms Q" unfolding t
unfolding vars_rule_def by simp
qed
inductive_set
qrstep :: "bool ⇒ ('f, 'v) terms ⇒ ('f, 'v) trs ⇒ ('f, 'v) term rel"
for nfs and Q and R
where
subst[intro]: "∀u⊲s ⋅ σ. u ∈ NF_terms Q ⟹ (s, t) ∈ R ⟹ NF_subst nfs (s,t) σ Q ⟹ (s ⋅ σ, t ⋅ σ) ∈ qrstep nfs Q R" |
ctxt[intro]: "(s, t) ∈ qrstep nfs Q R ⟹ (C⟨s⟩, C⟨t⟩) ∈ qrstep nfs Q R"
hide_fact (open)
qrstep.ctxt qrstep.subst
qrstepp.ctxt qrstepp.subst
lemma qrstep_id[intro]: "∀ u ⊲ s. u ∈ NF_terms Q ⟹ (s,t) ∈ R ⟹ NF_subst nfs (s,t) Var Q ⟹ (s,t) ∈ qrstep nfs Q R"
using qrstep.subst[of s Var Q t R nfs] by auto
lemma supteq_qrstep_subset:
"{⊵} O qrstep nfs Q R ⊆ qrstep nfs Q R O {⊵}"
(is "?lhs ⊆ ?rhs")
proof
fix s t
assume "(s, t) ∈ ?lhs"
then obtain u where "s ⊵ u" and "(u, t) ∈ qrstep nfs Q R" by auto
from ‹s ⊵ u› obtain C where s: "s = C⟨u⟩" by auto
from qrstep.ctxt[OF ‹(u, t) ∈ qrstep nfs Q R›]
have "(s, C⟨t⟩) ∈ qrstep nfs Q R" by (simp add: s)
moreover have "C⟨t⟩ ⊵ t" by simp
ultimately show "(s, t) ∈ ?rhs" by auto
qed
definition
qrstep_r_p_s ::
"bool ⇒ ('f, 'v) terms ⇒ ('f, 'v) trs ⇒ ('f, 'v) rule ⇒ pos ⇒ ('f, 'v) subst ⇒ ('f, 'v) trs"
where
"qrstep_r_p_s nfs Q R r p σ ≡ {(s, t).
(∀u⊲fst r ⋅ σ. u ∈ NF_terms Q) ∧
p ∈ poss s ∧ r ∈ R ∧ s |_ p = fst r ⋅ σ ∧ t = replace_at s p (snd r ⋅ σ) ∧ NF_subst nfs r σ Q}"
definition
irstep :: "bool ⇒ ('f, 'v) trs ⇒ ('f, 'v) term rel"
where
"irstep nfs R ≡ qrstep nfs (lhss R) R"
lemma qrstep_rstep_conv[simp]: "qrstep nfs {} R = rstep R"
proof (intro equalityI subrelI)
fix s t
assume "(s, t) ∈ rstep R"
then obtain C l r σ where s: "s = C ⟨ l ⋅ σ ⟩" and t: "t = C ⟨ r ⋅ σ ⟩"
and lr: "(l,r) ∈ R" by auto
show "(s, t) ∈ qrstep nfs {} R" unfolding s t
by (rule qrstep.ctxt[OF qrstep.subst[OF _ lr]], auto)
next
fix s t assume "(s, t) ∈ qrstep nfs {} R" then show "(s, t) ∈ rstep R"
by (induct) auto
qed
lemma qrstep_trancl_ctxt:
assumes "(s, t) ∈ (qrstep nfs Q R)⇧+"
shows "(C⟨s⟩, C⟨t⟩) ∈ (qrstep nfs Q R)⇧+"
using assms by (induct) (auto intro: trancl_into_trancl)
text ‹
The inductive definition really corresponds to the intuitive definition of
Q-restricted rewriting.
›
lemma qrstepE':
assumes "(s, t) ∈ qrstep nfs Q R"
shows "∃C σ l r. (∀u⊲l⋅σ. u ∈ NF_terms Q) ∧ (l, r) ∈ R ∧ s = C⟨l ⋅ σ⟩ ∧ t = C⟨r ⋅ σ⟩ ∧ NF_subst nfs (l,r) σ Q"
using assms proof (induct rule: qrstep.induct)
case (ctxt s t C)
then obtain D σ l r where nf: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and lr: "(l, r) ∈ R" and s: "s = D⟨l ⋅ σ⟩" and t: "t = D⟨r ⋅ σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q" by auto
let ?C = "C ∘⇩c D"
have s: "C⟨s⟩ = ?C⟨l ⋅ σ⟩" by (simp add: s)
have t: "C⟨t⟩ = ?C⟨r ⋅ σ⟩" by (simp add: t)
show ?case using nf lr s t nfs by blast
next
case (subst s σ t)
show ?case
apply (rule exI[of _ Hole])
using subst by auto
qed
lemma qrstepE[elim]:
assumes "(s, t) ∈ qrstep nfs Q R"
and "⋀C σ l r. ⟦∀u⊲l⋅σ. u ∈ NF_terms Q; (l, r) ∈ R; s = C⟨l ⋅ σ⟩; t = C⟨r ⋅ σ⟩; NF_subst nfs (l,r) σ Q⟧ ⟹ P"
shows "P"
using qrstepE'[of s t nfs Q R] and assms by auto
lemma qrstepI[intro]:
assumes nf: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and lr: "(l, r) ∈ R"
and s: "s = C⟨l ⋅ σ⟩"
and t: "t = C⟨r ⋅ σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q"
shows "(s, t) ∈ qrstep nfs Q R"
unfolding s t
by (rule qrstep.ctxt[OF qrstep.subst[OF nf lr nfs]])
text‹Every Q-step takes place at a specific position and using a specific
rule and specific substitution.›
lemma qrstep_qrstep_r_p_s_conv:
"(s, t) ∈ qrstep nfs Q R ⟷ (∃r p σ. (s, t) ∈ qrstep_r_p_s nfs Q R r p σ)"
proof
assume "∃r p σ. (s, t) ∈ qrstep_r_p_s nfs Q R r p σ"
then obtain l r p σ where NF_terms: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and p: "p ∈ poss s" and lr: "(l, r) ∈ R"
and s: "s |_ p = l ⋅ σ"
and t: "t = replace_at s p (r ⋅ σ)"
and nfs: "NF_subst nfs (l,r) σ Q"
unfolding qrstep_r_p_s_def by auto
from ctxt_supt_id[OF p] have s: "s = (ctxt_of_pos_term p s)⟨l ⋅ σ⟩" unfolding s
by simp
from s t NF_terms lr nfs show "(s, t) ∈ qrstep nfs Q R" by auto
next
assume "(s, t) ∈ qrstep nfs Q R"
then obtain C l r σ where "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q"
by auto
let ?p = "hole_pos C"
have "∀u⊲l ⋅ σ. u ∈ NF_terms Q" by fact
moreover have "?p ∈ poss s" unfolding s by simp
moreover have "(l, r) ∈ R" by fact
moreover have "s |_ ?p = l ⋅ σ" by (simp add: s)
moreover have "t = replace_at s ?p (r ⋅ σ)" by (simp add: s t)
ultimately have "(s, t) ∈ qrstep_r_p_s nfs Q R (l, r) ?p σ"
by (simp add: qrstep_r_p_s_def nfs)
then show "∃r p σ. (s, t) ∈ qrstep_r_p_s nfs Q R r p σ" by auto
qed
lemma qrstep_induct[case_names IH, induct set: qrstep]:
assumes "(s, t) ∈ qrstep nfs Q R"
and IH: "⋀C σ l r. ∀u⊲l ⋅ σ. u ∈ NF_terms Q ⟹ (l, r) ∈ R ⟹ NF_subst nfs (l,r) σ Q ⟹ P C⟨l ⋅ σ⟩ C⟨r ⋅ σ⟩"
shows "P s t"
proof -
from ‹(s, t) ∈ qrstep nfs Q R› obtain C σ l r where NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q"
by auto
from IH[OF NF ‹(l, r) ∈ R› nfs] show ?thesis unfolding s t .
qed
lemma qrstep_rule_conv: "((s,t) ∈ qrstep nfs Q R) = (∃ lr ∈ R. (s,t) ∈ qrstep nfs Q {lr})" (is "?l = ?r")
proof
assume ?r then show ?l by auto
next
assume ?l then show ?r by blast
qed
lemma qrstep_empty_r[simp]: "qrstep nfs Q {} = {}"
using qrstep_rule_conv[of _ _ nfs Q "{}"] by auto
lemma qrstep_union: "qrstep nfs Q (R ∪ R') = qrstep nfs Q R ∪ qrstep nfs Q R'"
using qrstep_rule_conv[of _ _ nfs Q R]
qrstep_rule_conv[of _ _ nfs Q "R'"]
qrstep_rule_conv[of _ _ nfs Q "R ∪ R'"]
by auto
lemma qrstep_all_mono: assumes R: "R ⊆ R'" and Q: "NF_terms Q ⊆ NF_terms Q'" and n: "Q ≠ {} ⟹ nfs' ⟹ nfs"
shows "qrstep nfs Q R ⊆ qrstep nfs' Q' R'"
proof
fix s t assume "(s, t) ∈ qrstep nfs Q R"
then obtain C σ l r where "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and "(l, r) ∈ R"
and "s = C⟨l ⋅ σ⟩" and "t = C⟨r ⋅ σ⟩" and nfs: "NF_subst nfs (l,r) σ Q" by auto
moreover with n Q R have "∀u⊲l ⋅ σ. u ∈ NF_terms Q'"
and "NF_subst nfs' (l,r) σ Q'" and "(l,r) ∈ R'" unfolding NF_subst_def by auto
ultimately show "(s, t) ∈ qrstep nfs' Q' R'" by auto
qed
lemma qrstep_rules_mono:
assumes "R ⊆ R'" shows "qrstep nfs Q R ⊆ qrstep nfs Q R'"
by (rule qrstep_all_mono[OF assms], auto)
lemma qrstep_mono:
assumes 1: "R ⊆ R'" and 2: "NF_terms Q ⊆ NF_terms Q'"
shows "qrstep nfs Q R ⊆ qrstep nfs Q' R'"
by (rule qrstep_all_mono[OF 1 2])
lemma qrstep_NF_anti_mono:
assumes "Q ⊆ Q'" shows "qrstep nfs Q' R ⊆ qrstep nfs Q R"
by (rule qrstep_mono[OF subset_refl NF_terms_anti_mono[OF assms]])
lemma qrstep_Id: "qrstep nfs Q Id ⊆ Id"
proof -
have "qrstep nfs Q Id ⊆ qrstep nfs {} Id"
by (rule qrstep_mono, auto)
also have "... ⊆ Id" using rstep_id by auto
finally show ?thesis by auto
qed
lemma NF_terms_subset_criterion:
"Q' ∩ NF_terms Q = {} ⟷ NF_terms Q ⊆ NF_terms Q'" (is "?lhs = ?rhs")
proof
assume "?rhs" then show "?lhs"
proof (rule contrapos_pp)
assume "¬ ?lhs"
then obtain q where "q ∈ Q'" and "q ∈ NF_terms Q" by auto
from ‹q ∈ Q'› have "q ∉ NF_terms Q'" by auto
with ‹q ∈ NF_terms Q› show "¬ NF_terms Q ⊆ NF_terms Q'" by blast
qed
next
assume "?lhs" then show "?rhs"
proof (rule contrapos_pp)
assume "¬ ?rhs"
then obtain t where NF: "t ∈ NF_terms Q" and "t ∉ NF_terms Q'" by auto
then obtain s where "(t, s) ∈ rstep (Id_on Q')" by (auto simp: NF_def)
then obtain C q σ where "q ∈ Q'" and t: "t = C⟨q ⋅ σ⟩" by auto
have "q ∈ NF_terms Q"
proof
fix D l τ
assume q: "q = D ⟨ l ⋅ τ ⟩" and l: "l ∈ Q"
have "(t,t) ∈ rstep (Id_on Q)" unfolding t q
by (rule rstepI[of l l _ _ "C ∘⇩c (D ⋅⇩c σ)" "τ ∘⇩s σ"], insert l, auto)
then have "t ∉ NF_terms Q" by auto
with ‹t ∈ NF_terms Q› show False by blast
qed
with ‹q ∈ Q'› show "Q' ∩ NF_terms Q ≠ {}" by auto
qed
qed
lemma qrstep_subset_rstep[intro,simp]: "qrstep nfs Q R ⊆ rstep R"
by (simp only: qrstep_rstep_conv[symmetric, of R nfs], rule qrstep_NF_anti_mono, auto)
lemma qrstep_into_rstep: "(s,t) ∈ qrstep nfs Q R ⟹ (s,t) ∈ rstep R"
using qrstep_subset_rstep by auto
lemma qrsteps_into_rsteps: "(s,t) ∈ (qrstep nfs Q R)⇧* ⟹ (s,t) ∈ (rstep R)⇧*"
using rtrancl_mono[OF qrstep_subset_rstep] by auto
lemma qrstep_preserves_funas_terms:
assumes r: "funas_term r ⊆ F"
and sF: "funas_term s ⊆ F" and step: "(s,t) ∈ qrstep nfs Q {(l,r)}" and vars: "vars_term r ⊆ vars_term l"
shows "funas_term t ⊆ F"
proof -
from step obtain C σ where
s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" by auto
have fs: "funas_term s = funas_ctxt C ∪ funas_term l ∪ ⋃(funas_term ` σ ` vars_term l)" unfolding s using funas_term_subst by auto
have "funas_term t = funas_ctxt C ∪ funas_term r ∪ ⋃(funas_term ` σ ` vars_term r)" unfolding t using funas_term_subst by auto
then have "funas_term t ⊆ funas_ctxt C ∪ funas_term r ∪ ⋃(funas_term ` σ ` vars_term l)" using ‹vars_term r ⊆ vars_term l› by auto
with ‹funas_term r ⊆ F› ‹funas_term s ⊆ F›
show ?thesis unfolding fs by force
qed
lemma ctxt_of_pos_term_qrstep_below:
assumes step: "(s,t) ∈ qrstep_r_p_s nfs Q R r p' σ" and le: "p ≤⇩p p'"
shows "ctxt_of_pos_term p s = ctxt_of_pos_term p t"
proof -
from step[unfolded qrstep_r_p_s_def] have p': "p' ∈ poss s" and t: "t = replace_at s p' (snd r ⋅ σ)" by auto
show ?thesis unfolding t
proof (rule ctxt_of_pos_term_replace_at_below[OF _ le, of s, symmetric])
from p' le show "p ∈ poss s" unfolding prefix_def by auto
qed
qed
lemma parallel_qrstep_subt_at:
fixes p :: pos
assumes step: "(s,t) ∈ qrstep_r_p_s nfs Q R lr p σ"
and par: "p ⊥ q"
and q: "q ∈ poss s"
shows "s |_ q = t |_ q ∧ q ∈ poss t"
proof -
note step = step[unfolded qrstep_r_p_s_def]
from step have t: "t = replace_at s p (snd lr ⋅ σ)" and p: "p ∈ poss s" by auto
show ?thesis unfolding t
by (rule conjI, rule parallel_replace_at_subt_at[symmetric, OF par p q], insert
parallel_poss_replace_at[OF par p] q, auto)
qed
lemma qrstep_subt_at_gen:
assumes step: "(s, t) ∈ qrstep_r_p_s nfs Q R lr (p @ q) σ"
shows "(s |_ p, t |_ p) ∈ qrstep_r_p_s nfs Q R lr q σ"
proof -
from step[unfolded qrstep_r_p_s_def]
have NF: "∀ u ⊲ fst lr ⋅ σ. u ∈ NF_terms Q"
and pq: "p @ q ∈ poss s"
and lr: "lr ∈ R"
and s: "s |_ (p @ q) = fst lr ⋅ σ"
and t: "t = replace_at s (p @ q) (snd lr ⋅ σ)"
and nfs: "NF_subst nfs lr σ Q"
by auto
from pq[unfolded poss_append_poss] have p: "p ∈ poss s" and q: "q ∈ poss (s |_ p)" by auto
show ?thesis
unfolding qrstep_r_p_s_def
apply (intro CollectI, unfold split)
apply (intro conjI NF q lr nfs)
subgoal by (rule s[unfolded subt_at_append[OF p]])
subgoal by (unfold t ctxt_of_pos_term_append[OF p], simp add: replace_at_subt_at[OF p])
done
qed
lemma qrstep_r_p_s_imp_poss:
assumes step: "(s,t) ∈ qrstep_r_p_s nfs Q R lr p σ"
shows "p ∈ poss s ∧ p ∈ poss t"
proof -
from step[unfolded qrstep_r_p_s_def]
have ps: "p ∈ poss s"
and t: "t = replace_at s p (snd lr ⋅ σ)"
by auto
have pt: "p ∈ poss t" unfolding t
using hole_pos_ctxt_of_pos_term[OF ps]
hole_pos_poss[of "ctxt_of_pos_term p s"] by auto
with ps show ?thesis by auto
qed
lemma qrstep_subt_at:
assumes step: "(s, t) ∈ qrstep_r_p_s nfs Q R lr p σ"
shows "(s |_ p, t |_ p) ∈ qrstep_r_p_s nfs Q R lr [] σ"
by (rule qrstep_subt_at_gen, insert step, simp)
lemma parallel_qrstep_poss:
fixes q :: pos
assumes par: "q ⊥ p"
and q: "q ∈ poss s"
and step: "(s, t) ∈ qrstep_r_p_s nfs Q R r p σ"
shows "q ∈ poss t"
proof -
from step[unfolded qrstep_r_p_s_def]
have t: "t = replace_at s p (snd r ⋅ σ)" and p: "p ∈ poss s" by auto
from parallel_poss_replace_at[OF parallel_pos_sym[OF par] p]
show ?thesis unfolding t using q by simp
qed
lemma parallel_qrstep_ctxt_to_term_list:
fixes q :: pos
assumes par: "q ⊥ p"
and poss: "q ∈ poss s"
and step: "(s, t) ∈ qrstep_r_p_s nfs Q R r p σ"
shows "∃p'. p' ≤⇩p p ∧ (∃ i. i < length (ctxt_to_term_list (ctxt_of_pos_term q s)) ∧
ctxt_to_term_list (ctxt_of_pos_term q s) ! i = s |_ p' ∧
ctxt_to_term_list (ctxt_of_pos_term q t) =
(ctxt_to_term_list (ctxt_of_pos_term q s))[i := t |_ p'])"
proof -
from parallel_remove_prefix[OF par] obtain pp i1 i2 q1 q2 where
q: "q = pp @ i1 # q1" and p: "p = pp @ i2 # q2" and i12: "i1 ≠ i2"
by blast
let ?p1 = "i1 # q1"
let ?p2 = "i2 # q2"
let ?c = "ctxt_of_pos_term"
let ?cc = "λ p t. ctxt_to_term_list (?c p t)"
note qr_def = qrstep_r_p_s_def
show ?thesis unfolding p q
proof (intro exI, intro conjI)
show "pp @ [i2] ≤⇩p pp @ ?p2" unfolding prefix_def by simp
next
show "∃ i < length (?cc (pp @ ?p1) s).
?cc (pp @ ?p1) s ! i = s |_ (pp @ [i2]) ∧
?cc (pp @ ?p1) t = (?cc (pp @ ?p1) s) [ i := t |_ (pp @ [i2])]"
using step poss unfolding p q
proof (induct pp arbitrary: s t)
case (Cons i p s t)
from Cons(2) have step: "(s,t) ∈ qrstep_r_p_s nfs Q R r ([i] @ (p @ ?p2)) σ" by simp
note istep = qrstep_subt_at_gen[OF step]
note step = step[unfolded qr_def]
from step have p2: "i # p @ ?p2 ∈ poss s" by auto
then obtain f ss where s: "s = Fun f ss" by (cases s, auto)
with p2 have iss: "i < length ss" by auto
from p2[unfolded s] have p2i: "p @ [i2] ∈ poss (ss ! i)" by simp
from p2i iss have ip2: "i # p ∈ poss s" unfolding s by simp
from iss have si: "s |_ [i] = ss ! i" unfolding s by simp
from Cons(3) have "p @ ?p1 ∈ poss (s |_ [i])" unfolding s using iss by simp
from Cons(1)[OF istep this]
obtain i' where i': "i' < length (?cc (p @ ?p1) (s |_ [i]))" and
id1: "?cc (p @ ?p1) (s |_ [i]) ! i' = s |_ [i] |_ (p @ [i2])" and
id2: "?cc (p @ ?p1) (t |_ [i]) = (?cc (p @ ?p1) (s |_ [i]))[i' := t |_ [i]
|_ (p @ [i2])]" by blast
from step have tp2: "t = replace_at s (i # p @ ?p2) (snd r ⋅ σ)" by simp
have ipless: "i # (p @ [i2]) ≤⇩p i # p @ ?p2" by simp
have ipt: "i # (p @ [i2]) ∈ poss t" unfolding tp2
by (rule replace_at_below_poss[OF p2 ipless])
have "t = replace_at t (i # (p @ [i2])) (t |_ (i # (p @ [i2])))"
by (rule ctxt_supt_id[symmetric, OF ipt])
also have "... = replace_at (Fun f ss) (i # (p @ [i2])) (t |_ (i # (p @
[i2])))" (is "_ = ?t")
unfolding s[symmetric]
using ctxt_of_pos_term_qrstep_below[OF Cons(2), of "i # (p @ [i2])"] ipless by auto
finally have t: "t = ?t" .
have "t |_ [i] = ?t |_ [i]" using t by simp
also have "... = replace_at (ss ! i) (p @ [i2]) (t |_ (i # (p @ [i2])))" (is "_ = ?ti")
using iss by (simp add: nth_append)
finally have ti: "t |_ [i] = ?ti" .
have cs: "?c ((i # p) @ ?p2) s = More f (take i ss) (?c (p @ ?p2) (ss ! i)) (drop (Suc i) ss)"
unfolding s by simp
have i'': "i' < length (?cc ((i # p) @ ?p1) s)" using i' unfolding s si by simp
show ?case
proof (rule exI[of _ i'], intro conjI, rule i'')
show "?cc ((i # p) @ ?p1) s ! i' = s |_ ((i # p) @ [i2])"
unfolding s using si id1 i' by (simp add: nth_append)
next
from iss have min: "min (length ss) i = i" by simp
note i' = i'[unfolded si]
have i'': "i' < length (?cc (p @ i1 # q1) (ss ! i) @ take i ss @ drop (Suc i) ss)"
using i' by simp
have "?cc ((i # p) @ ?p1) t = ?cc ((i # p) @ ?p1) ?t" using t by simp
also have "... = (?cc ((i # p) @ ?p1) s) [i' := t |_ (i # (p @ [i2]))]"
unfolding s using min id2 i' iss si
unfolding ti
by (simp add: replace_at_subt_at[OF p2i] upd_conv_take_nth_drop[OF i''] upd_conv_take_nth_drop[OF i'] nth_append)
finally show "?cc ((i # p) @ i1 # q1) t = (?cc ((i # p) @ i1 # q1) s)
[i' := t |_ ((i # p) @ [i2])]" by simp
qed
next
case Nil
have eps: "⋀ p. [] @ p = p" "⋀ t. t |_ [] = t" by auto
note Empty = Nil[unfolded eps]
note step = Empty[unfolded qr_def]
from step have p2: "i2 # q2 ∈ poss s" by auto
from Empty have p1: "i1 # q1 ∈ poss s" by simp
then obtain f ss where s: "s = Fun f ss" by (cases s, auto)
from s p2 have i2: "i2 < length ss" by auto
from s p1 have i1: "i1 < length ss" by auto
from step have t: "t = replace_at (Fun f ss) (i2 # q2) (snd r ⋅ σ)" unfolding s by simp
have rσ: "snd r ⋅ σ = t |_ (i2 # q2)" unfolding t
by (rule replace_at_subt_at[symmetric], insert p2, unfold s)
have tt: "t = replace_at (Fun f ss) (i2 # q2) (t |_ (i2 # q2))" (is "t = ?t")
unfolding rσ[symmetric] unfolding t ..
have "t |_ [i2] = ?t |_ [i2]" using tt by simp
also have "... = replace_at (ss ! i2) q2 (t |_ (i2 # q2))" (is "_ = ?ti")
using i2 by (simp add: nth_append)
finally have ti: "t |_ [i2] = ?ti" .
have i2ss: "take i2 ss @ ss ! i2 # drop (Suc i2) ss = ss"
using upd_conv_take_nth_drop[OF i2, symmetric] list_update_id by auto
let ?n = "length (?cc q1 (ss ! i1))"
from i1 have min1: "min (length ss) i1 = i1" by simp
from i2 have min2: "min (length ss) i2 = i2" by simp
from i12 have i12: "i1 < i2 ∨ i2 < i1" by auto
obtain i2' where i2': "i2' = (if i1 < i2 then i2 - Suc 0 else i2)" by auto
{
from i12
have "(take i1 ss @ drop (Suc i1) ss) ! i2' = ss ! i2"
proof
assume "i2 < i1"
then show ?thesis by (auto simp: nth_append i2' i2)
next
assume i12: "i1 < i2"
then have "i2 = Suc i1 + (i2 - Suc i1)" by simp
then obtain k where i2k: "i2 = Suc i1 + k" by blast
from i2[unfolded i2k] have "Suc i1 + k ≤ length ss" by simp
then show ?thesis
by (metis (no_types, lifting) Suc_less_eq Suc_pred i2k add_gr_0 add_leD1 diff_Suc_Suc
diff_add_inverse i12 i2' length_take min1 not_add_less1 nth_append nth_drop zero_less_Suc)
qed
} note i2'id = this
from tt have tt: "⋀ p. ?cc p t = ?cc p ?t" by simp
show ?case unfolding eps s ti unfolding tt
proof (rule exI[of _ "?n + i2'"], intro conjI)
show "?cc (i1 # q1) (Fun f ss) ! (?n + i2') = Fun f ss |_ [i2]"
by (simp add: i2'id)
next
from i1 have len: "i1 + (length ss - Suc i1) = length ss - Suc 0" by auto
from i12 have
i2'len: "i2' < length ss - Suc 0" unfolding i2' using i1 i2 by auto
show "length (?cc q1 (ss ! i1)) + i2' < length (?cc (i1 # q1) (Fun f ss))"
by (auto simp: i2 i1 min1 len i2'len)
next
from i12
show "?cc (i1 # q1) ?t = (?cc (i1 # q1) (Fun f ss)) [?n + i2' := ?ti]"
proof
assume i12: "i2 < i1"
then have len: "?n + i2' < length (?cc (i1 # q1) (Fun f ss))"
unfolding i2' using min1 i1 i2 by simp
from i12 have min12: "min i2 i1 = i2" "min i1 i2 = i2" by auto
have drop: "drop (Suc i2) ss ! (i1 - Suc i2) = ss ! i1" using i12 i1 by simp
from i12 have "i1 = Suc i2 + (i1 - Suc i2)" by simp
then obtain k where i1k: "i1 = Suc i2 + k" by blast
show ?thesis using i12
unfolding upd_conv_take_nth_drop[OF len]
unfolding i2'
by (simp add: min12 i1 i2 min1 min2 nth_append drop, simp add: i1k ac_simps take_drop)
next
assume i12: "i1 < i2"
then have len: "?n + i2' < length (?cc (i1 # q1) (Fun f ss))"
unfolding i2' using min1 i1 i2 by simp
from i12 have min12: "min i2 i1 = i1" "min i1 i2 = i1" by auto
from i12 have "i2 = Suc i1 + (i2 - Suc i1)" by simp
then obtain k where i2k: "i2 = Suc i1 + k" by blast
have minik: "min i1 (i1 + k) = i1" by simp
show ?thesis using i12
unfolding upd_conv_take_nth_drop[OF len]
unfolding i2'
by (simp add: min12 i1 i2 min1 min2 nth_append, simp add: i2k take_drop ac_simps minik)
qed
qed
qed
qed
qed
lemma parallel_qrstep:
fixes p1 :: pos
assumes p12: "p1 ⊥ p2"
and p1: "p1 ∈ poss t"
and p2: "p2 ∈ poss t"
and step2: "t |_ p2 = l2 ⋅ σ2" "∀ u ⊲ l2 ⋅ σ2. u ∈ NF_terms Q" "(l2,r2) ∈ R" "NF_subst nfs (l2,r2) σ2 Q"
shows "(replace_at t p1 v, replace_at (replace_at t p1 v) p2 (r2 ⋅ σ2)) ∈ qrstep nfs Q R" (is "(?one,?two) ∈ _")
proof -
show ?thesis unfolding qrstep_qrstep_r_p_s_conv
proof (intro exI)
show "(?one,?two) ∈ qrstep_r_p_s nfs Q R (l2,r2) p2 σ2"
unfolding qrstep_r_p_s_def
apply (intro CollectI, unfold split fst_conv snd_conv)
apply (unfold parallel_replace_at_subt_at[OF p12 p1 p2])
apply (unfold parallel_poss_replace_at[OF p12 p1])
apply (intro conjI step2(2) refl p2)
by (insert step2, auto)
qed
qed
lemma parallel_qrstep_swap:
fixes p1 :: pos
assumes p12: "p1 ⊥ p2"
and two: "(t, s) ∈ qrstep_r_p_s nfs Q1 R1 r1 p1 σ1 O qrstep_r_p_s nfs Q2 R2 r2 p2 σ2"
shows "(t, s) ∈ qrstep_r_p_s nfs Q2 R2 r2 p2 σ2 O qrstep_r_p_s nfs Q1 R1 r1 p1 σ1"
proof -
let ?R1 = "qrstep_r_p_s nfs Q1 R1"
let ?R2 = "qrstep_r_p_s nfs Q2 R2"
from two obtain u where tu: "(t,u) ∈ ?R1 r1 p1 σ1" and us: "(u,s) ∈ ?R2 r2 p2 σ2" by auto
from tu[unfolded qrstep_r_p_s_def]
have step1: "t |_ p1 = fst r1 ⋅ σ1" "∀ u ⊲ fst r1 ⋅ σ1. u ∈ NF_terms Q1" and r1: "r1 ∈ R1"
and p1: "p1 ∈ poss t" and u: "u = replace_at t p1 (snd r1 ⋅ σ1)"
and nfs1: "NF_subst nfs r1 σ1 Q1" by auto
from us[unfolded qrstep_r_p_s_def, simplified]
have step2: "u |_ p2 = fst r2 ⋅ σ2" "∀ u ⊲ fst r2 ⋅ σ2. u ∈ NF_terms Q2" and r2: "r2 ∈ R2"
and p2: "p2 ∈ poss u" and s: "s = replace_at u p2 (snd r2 ⋅ σ2)"
and nfs2: "NF_subst nfs r2 σ2 Q2" by auto
from parallel_poss_replace_at[OF p12 p1] p2 have p2': "p2 ∈ poss t" unfolding u by simp
have one: "(t,replace_at t p2 (snd r2 ⋅ σ2)) ∈ ?R2 r2 p2 σ2" (is "(t,?t) ∈ _") unfolding qrstep_r_p_s_def
apply (intro CollectI, unfold split)
apply (unfold step2(1)[symmetric] u parallel_replace_at_subt_at[OF p12 p1 p2'])
apply (intro conjI p2' r2 refl nfs2)
by (metis p1 p12 p2' parallel_replace_at_subt_at step2(1) step2(2) u)
have p21: "p2 ⊥ p1" by (rule parallel_pos_sym[OF p12])
have p1': "p1 ∈ poss ?t" using parallel_poss_replace_at[OF p21 p2'] p1 by simp
have two: "(?t,replace_at ?t p1 (snd r1 ⋅ σ1)) ∈ ?R1 r1 p1 σ1" (is "(_,?t') ∈ _") unfolding qrstep_r_p_s_def
apply (intro CollectI, unfold split)
apply (intro conjI p1' r1 nfs1 refl)
subgoal by (rule step1(2))
subgoal by (unfold step1(1)[symmetric] parallel_replace_at_subt_at[OF p21 p2' p1], simp)
done
with one have steps: "(t,?t') ∈ ?R2 r2 p2 σ2 O ?R1 r1 p1 σ1" by auto
have "s = ?t'" unfolding s u
by (rule parallel_replace_at[OF p12 p1 p2'])
then show ?thesis using steps by auto
qed
lemma normalize_subterm_qrsteps_count:
assumes p: "p ∈ poss t"
and steps: "(t, s) ∈ (qrstep nfs Q R)^^n"
and s: "s ∈ NF_terms Q"
shows "∃ n1 n2 u. (t |_ p, u) ∈ (qrstep nfs Q R)^^n1 ∧ u ∈ NF_terms Q ∧ (replace_at t p u, s) ∈ (qrstep nfs Q R)^^n2 ∧ n = n1 + n2"
proof -
let ?Q = "λ n n1 n2 t u s. (t |_ p, u) ∈ (qrstep nfs Q R)^^n1 ∧ u ∈ NF_terms Q ∧ (replace_at t p u, s) ∈ (qrstep nfs Q R)^^n2 ∧ n = n1 + n2"
let ?P = "λ n t s. (∃ n1 n2 u. ?Q n n1 n2 t u s)"
have "?P n t s" using steps s p
proof (induct n arbitrary: t s)
case 0
then have t: "t ∈ NF_terms Q" and p: "p ∈ poss t" and s: "s = t" by auto
show "∃ n1 n2 u. ?Q 0 n1 n2 t u s"
proof (rule exI[of _ 0], rule exI[of _ 0], rule exI[of _ "t |_ p"], intro conjI)
from p have "t |_ p ⊴ t" by (rule subt_at_imp_supteq)
from NF_subterm[OF t this]
show "t |_ p ∈ NF_terms Q" .
next
have "replace_at t p (t |_ p) = t" using p by (rule ctxt_supt_id)
then show "(replace_at t p (t |_ p),s) ∈ (qrstep nfs Q R)^^0" unfolding s by simp
qed auto
next
case (Suc n)
then have p: "p ∈ poss t" by simp
from relpow_Suc_D2[OF Suc(2)] obtain u where tu: "(t,u) ∈ qrstep nfs Q R" and us: "(u,s) ∈ qrstep nfs Q R ^^ n" by auto
note ind = Suc(1)[OF us Suc(3)]
from tu[unfolded qrstep_qrstep_r_p_s_conv]
obtain r p' σ where tu': "(t,u) ∈ qrstep_r_p_s nfs Q R r p' σ" by auto
from tu'[unfolded qrstep_r_p_s_def]
have NF: "∀ u ⊲ fst r ⋅ σ. u ∈ NF_terms Q" and p': "p' ∈ poss t" and r: "r ∈ R" and t: "t |_ p' = fst r ⋅ σ"
and u: "u = replace_at t p' (snd r ⋅ σ)"
and nfsr: "NF_subst nfs r σ Q" by auto
from pos_cases have cases: "p ≤⇩p p' ∨ p' <⇩p p ∨ p ⊥ p'" .
{
assume pp': "p ≤⇩p p'"
then obtain p'' where p'': "p' = p @ p''" unfolding prefix_def by auto
from p' p'' have tp'': "p'' ∈ poss (t |_ p)" by simp
from t have t: "t |_ p |_ p'' = fst r ⋅ σ" unfolding p'' subt_at_append[OF p] .
from replace_at_below_poss[OF p' pp'] have pu: "p ∈ poss u" unfolding u .
from ind[OF this] obtain n1 n2 w where steps1: "(u |_ p, w) ∈ qrstep nfs Q R ^^ n1" and w: "w ∈ NF_terms Q"
and steps2: "(replace_at u p w, s) ∈ qrstep nfs Q R ^^ n2" and sum: "n = n1 + n2" by auto
have tu: "ctxt_of_pos_term p t = ctxt_of_pos_term p u" unfolding u by
(simp add: ctxt_of_pos_term_replace_at_below[OF p pp'])
have "(t |_ p, u |_ p) ∈ qrstep_r_p_s nfs Q R r p'' σ" unfolding qrstep_r_p_s_def
apply (intro CollectI, unfold split)
apply (intro conjI NF tp'' r t nfsr)
by (unfold u p'' ctxt_of_pos_term_append[OF p], simp add: replace_at_subt_at[OF p])
then have "(t |_ p, u |_ p) ∈ qrstep nfs Q R" unfolding qrstep_qrstep_r_p_s_conv by blast
from relpow_Suc_I2[OF this steps1] have steps1: "(t |_ p, w) ∈ qrstep nfs Q R ^^ Suc n1" .
have ?case
apply (intro exI conjI)
apply (rule steps1)
apply (rule w)
apply (unfold tu, rule steps2)
by (unfold sum, simp)
} note above = this
{
assume p'p: "p' <⇩p p"
from less_pos_imp_supt[OF p'p p] have "t |_ p ⊲ t |_ p'" .
with NF[unfolded t[symmetric]] have tp: "t |_ p ∈ NF_terms Q" by blast
have steps1: "(t |_ p, t |_ p) ∈ qrstep nfs Q R ^^ 0" by simp
have ?case
apply (intro exI conjI)
apply (rule steps1)
apply (rule tp)
apply (unfold ctxt_supt_id[OF p], rule Suc(2))
by simp
} note below = this
{
assume pp': "p ⊥ p'"
from parallel_pos_sym[OF this] have p'p: "p' ⊥ p" .
from parallel_poss_replace_at[OF this p'] p have pu: "p ∈ poss u" unfolding u by blast
from ind[OF this] obtain n1 n2 w where steps1: "(u |_ p, w) ∈ qrstep nfs Q R ^^ n1" and w: "w ∈ NF_terms Q"
and steps2: "(replace_at u p w, s) ∈ qrstep nfs Q R ^^ n2" and sum: "n = n1 + n2" by auto
from parallel_replace_at_subt_at[OF p'p p' p] have uptp: "u |_ p = t |_ p" unfolding u .
have ?case
proof (intro exI conjI, rule steps1[unfolded uptp], rule w)
show "Suc n = n1 + Suc n2" unfolding sum by simp
next
from r have r: "(fst r, snd r) ∈ R" by simp
have "(replace_at t p w, replace_at u p w) ∈ qrstep nfs Q R" unfolding u
unfolding parallel_replace_at[OF p'p p' p]
by (rule parallel_qrstep[OF pp' p p' t NF r], insert nfsr, auto)
from relpow_Suc_I2[OF this steps2]
show "(replace_at t p w, s) ∈ qrstep nfs Q R ^^ (Suc n2)" .
qed
} note parallel = this
from cases above below parallel show ?case by blast
qed
then show ?thesis by auto
qed
lemma normalize_subterm_qrsteps:
assumes p: "p ∈ poss t"
and steps: "(t, s) ∈ (qrstep nfs Q R)⇧*"
and s: "s ∈ NF_terms Q"
shows "∃ u. (t |_ p, u) ∈ (qrstep nfs Q R)⇧* ∧ u ∈ NF_terms Q ∧ (replace_at t p u, s) ∈ (qrstep nfs Q R)⇧*"
proof -
from rtrancl_imp_relpow[OF steps] obtain n where steps: "(t,s) ∈ qrstep nfs Q R ^^ n" by auto
from normalize_subterm_qrsteps_count[OF p steps s]
obtain n1 n2 u where steps1: "(t |_ p, u) ∈ qrstep nfs Q R ^^ n1" and u: "u ∈ NF_terms Q"
and steps2: "(replace_at t p u, s) ∈ qrstep nfs Q R ^^ n2" by auto
from relpow_imp_rtrancl[OF steps1] relpow_imp_rtrancl[OF steps2] u show ?thesis by blast
qed
lemma parallel_qrstep_r_p_s:
fixes p1 :: pos
assumes p12: "p1 ⊥ p2"
and p1: "p1 ∈ poss t"
and step: "(t, s) ∈ qrstep_r_p_s nfs Q R lr p2 σ"
shows "(replace_at t p1 w, replace_at s p1 w) ∈ qrstep nfs Q R" (is "(?one,?two) ∈ _")
proof -
note d = qrstep_r_p_s_def
from step[unfolded d] have NF: "∀ u ⊲ fst lr ⋅ σ. u ∈ NF_terms Q"
and p2: "p2 ∈ poss t" and lr: "lr ∈ R" and subt: "t |_ p2 = fst lr ⋅ σ"
and s: "s = replace_at t p2 (snd lr ⋅ σ)"
and nfs: "NF_subst nfs lr σ Q" by auto
show ?thesis unfolding qrstep_qrstep_r_p_s_conv
proof (intro exI)
show "(?one,?two) ∈ qrstep_r_p_s nfs Q R lr p2 σ"
unfolding d
apply (intro CollectI, unfold split fst_conv snd_conv)
apply (unfold parallel_replace_at_subt_at[OF p12 p1 p2])
apply (intro conjI NF subt lr nfs)
using s parallel_poss_replace_at[OF p12 p1] p2 parallel_replace_at[OF p12 p1 p2]
by auto
qed
qed
text ‹the advantage of the following lemma is the fact, that w.l.o.g. for
termination analysis one can first reduce the argument s of the context to Q-normal form›
lemma normalize_subterm_SN:
assumes SN_s: "SN_on (qrstep nfs Q R) {s}"
and SN_replace: "⋀ t. (s,t) ∈ (qrstep nfs Q R)⇧* ⟹ t ∈ NF_terms Q ⟹ SN_on (qrstep nfs Q R) { C⟨t⟩ }"
and SN_C: "SN_on (qrstep nfs Q R) (set (ctxt_to_term_list C))"
shows "SN_on (qrstep nfs Q R) { C⟨s⟩ }" (is "SN_on ?R _")
proof
fix f
assume "f 0 ∈ {C⟨s⟩}" and steps: "∀ i. (f i, f (Suc i)) ∈ ?R"
then have zero: "f 0 = C⟨s⟩" by auto
from choice[OF steps[unfolded qrstep_qrstep_r_p_s_conv]]
obtain lr where "∀ i. ∃ p σ. (f i, f (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) p σ" by auto
from choice[OF this] obtain p where "∀ i. ∃ σ. (f i, f (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) (p i) σ" by auto
from choice[OF this] obtain σ where steps: "⋀ i. (f i, f (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) (p i) (σ i)" by auto
let ?p = "hole_pos C"
{
fix i
assume below_or_par: "⋀ j. j < i ⟹ ?p ≤⇩p p j ∨ ?p ⊥ p j"
{
fix j
assume j: "j ≤ i"
then have "?p ∈ poss (f j) ∧ (s,f j |_ ?p) ∈ ?R⇧*"
proof (induct j)
case 0
show ?case unfolding zero by simp
next
case (Suc j)
then have p: "?p ∈ poss (f j)" and ssteps: "(s, f j |_ ?p) ∈ ?R⇧*" by auto
from Suc(2) have "j < i" by auto
from below_or_par[OF this]
show ?case
proof
assume True: "?p ≤⇩p p j"
then obtain q where q: "?p @ q = p j" unfolding prefix_def by auto
from qrstep_subt_at_gen[OF steps[of j, unfolded q[symmetric]]]
have step: "(f j |_ ?p, f (Suc j) |_ ?p) ∈ ?R" unfolding qrstep_qrstep_r_p_s_conv by blast
from steps[of j, unfolded qrstep_r_p_s_def]
have id: "f (Suc j) = replace_at (f j) (p j) (snd (lr j) ⋅ σ j)" and pi: "p j ∈ poss (f j)" by auto
from replace_at_below_poss[OF pi True] ssteps step
show ?thesis unfolding id by auto
next
assume par: "?p ⊥ p j"
from parallel_qrstep_subt_at[OF steps[of j] parallel_pos_sym[OF par] p] ssteps
show ?thesis by auto
qed
qed
}
then have "?p ∈ poss (f i) ∧ (s, f i |_ ?p) ∈ ?R⇧*" by auto
} note poss_rewrite = this
show False
proof (cases "∃ i. p i <⇩p ?p")
case False
{
fix i
from False have "¬ (p i <⇩p ?p)" by auto
with pos_cases[of ?p "p i"] have "?p ≤⇩p p i ∨ ?p ⊥ p i" by auto
} note below_or_par = this
from poss_rewrite[OF this]
have p: "⋀ i. ?p ∈ poss (f i)" ..
from below_or_par
have "(INFM i. ?p ≤⇩p p i) ∨ ¬ (INFM i. ?p ≤⇩p p i)" by auto
then show False
proof
assume inf: "INFM i. ?p ≤⇩p p i"
let ?i = "λ i. ?p ≤⇩p p i"
interpret infinitely_many ?i
by (unfold_locales, rule inf)
obtain g where g: "g = (λ i. f i |_ ?p)" by auto
{
fix i
from index_p[of i]
obtain q where q: "?p @ q = p (index i)" unfolding prefix_def by auto
from qrstep_subt_at_gen[OF steps[of "index i", unfolded q[symmetric]]]
have "(g (index i), g (Suc (index i))) ∈ ?R" unfolding g qrstep_qrstep_r_p_s_conv by blast
} note gsteps = this
{
fix i
assume "¬ ?i i"
with below_or_par[of i] have par: "?p ⊥ p i" by simp
from parallel_qrstep_subt_at[OF steps[of i] parallel_pos_sym[OF par] p]
have "g i = g (Suc i)" unfolding g by simp
} note gid = this
obtain h where h: "h = (λ i. g (index i))" by auto
{
fix i
from index_ordered[of i] have "Suc (index i) ≤ index (Suc i)" by simp
then have "∃ j. index (Suc i) = Suc (index i) + j" by arith
then obtain j where id: "index (Suc i) = Suc (index i) + j" by auto
{
fix j
assume "Suc (index i) + j ≤ index (Suc i)"
then have "g (Suc (index i)) = g (Suc (index i) + j)"
proof (induct j)
case 0 show ?case by simp
next
case (Suc j)
then have "g (Suc (index i)) = g (Suc (index i) + j)" by simp
also have "... = g (Suc (Suc (index i) + j))"
by (rule gid[OF index_not_p_between, of i], insert Suc(2), auto)
finally show ?case by simp
qed
}
from this[of j] have "g (Suc (index i)) = h (Suc i)" unfolding h id by simp
with gsteps[of i] have "(h i, h (Suc i)) ∈ ?R" unfolding h by simp
}
then have "¬ SN_on ?R {h 0}" by auto
then have nSN: "¬ SN_on ?R {g (index 0)}" unfolding h .
obtain iz where iz: "iz = index 0" by auto
from gid[OF index_not_p_start] have "⋀ i. i < iz ⟹ g i = g (Suc i)" unfolding iz by auto
then have "g 0 = g iz"
by (induct iz, auto)
with nSN have nSN: "¬ SN_on ?R {g 0}" unfolding iz by simp
with SN_s show False unfolding g zero by simp
next
assume inf: "¬ (INFM i. ?p ≤⇩p p i)"
let ?cc = "λ i. ctxt_to_term_list (ctxt_of_pos_term ?p (f i))"
let ?step = "λ i j n. j < n ∧ (?cc i ! j, ?cc (Suc i) ! j) ∈ ?R ∧ (∀ k. k ≠ j ⟶ ?cc (Suc i) ! k = ?cc i ! k) ∧ length (?cc (Suc i)) = n"
{
fix i
assume "?p ⊥ p i"
from parallel_qrstep_ctxt_to_term_list[OF this p steps]
obtain p' j where p': "p' ≤⇩p p i" and j: "j < length (?cc i)"
and i: "?cc i ! j = f i |_ p'"
and si: "?cc (Suc i) = (?cc i) [ j := f (Suc i) |_ p']" by blast+
from si have len: "length (?cc (Suc i)) = length (?cc i)" by simp
from p' obtain q where p': "p' @ q = p i" unfolding prefix_def by metis
then have pi: "p i = p' @ q" by simp
from qrstep_subt_at_gen[OF steps[of i, unfolded pi]]
have "(?cc i ! j, ?cc (Suc i) ! j) ∈ qrstep_r_p_s nfs Q R (lr i) q (σ i)" unfolding i si using j
by auto
then have step: "(?cc i ! j, ?cc (Suc i) ! j) ∈ ?R" unfolding qrstep_qrstep_r_p_s_conv by blast
have id: "∀ k. k ≠ j ⟶ ?cc (Suc i) ! k = ?cc i ! k" unfolding si by auto
from step id j have "∃ j. ?step i j (length (?cc i))"
unfolding len by blast
} note par_step = this
{
fix i
assume "¬ (?p ⊥ p i)"
with below_or_par have "?p ≤⇩p p i" by auto
from ctxt_of_pos_term_qrstep_below[OF steps this]
have "?cc (Suc i) = ?cc i" by simp
} note below_step = this
obtain n where n: "n = length (?cc 0)" by simp
{
fix i
have "length (?cc i) = n"
proof (induct i)
case 0 show ?case unfolding n by simp
next
case (Suc i)
then show ?case
using below_step[of i] par_step[of i]
by (cases "?p ⊥ p i", auto)
qed
} note len = this
from par_step have par_step: "⋀ i. ?p ⊥ p i ⟹ (∃ j. ?step i j n)" unfolding len by simp
from inf obtain k where par: "⋀ j. j ≥ k ⟹ ¬ ?p ≤⇩p p j" unfolding INFM_nat_le by auto
with below_or_par have par: "⋀ j. j ≥ k ⟹ ?p ⊥ p j" by auto
let ?jstep = "λ i j. (?cc (i + k) ! j, ?cc (Suc i + k) ! j) ∈ ?R"
{
fix i
have "i + k ≥ k" by simp
from par_step[OF par[OF this]]
obtain j where j: "j < n" and step: "?jstep i j" by auto
then have "∃ j < n. ?jstep i j" by blast
}
then have "∀ i. ∃ j < n. ?jstep i j" by blast
from inf_pigeonhole_principle[OF this] obtain j where j: "j < n" and steps: "⋀ i. ∃ i' ≥ i. ?jstep i' j" by blast
let ?t = "λ i. ?cc i ! j"
{
fix i
have "(?t i, ?t (Suc i)) ∈ ?R^="
proof (cases "?p ⊥ p i")
case False
from below_step[OF this] show ?thesis by simp
next
case True
from par_step[OF this]
obtain k where "?step i k n" by auto
then show ?thesis by (cases "k = j", auto)
qed
} then have rsteps: "∀ i. (?t i, ?t (Suc i)) ∈ Id ∪ ?R" by blast
from j[unfolded len[of 0, symmetric]] have t0: "?t 0 ∈ set (ctxt_to_term_list C)"
unfolding zero set_conv_nth by auto
with SN_C have SN: "SN_on ?R {?t 0}" unfolding SN_on_def by simp
from non_strict_ending[OF rsteps] SN
obtain k'' where "∀ k' ≥ k''. (?t k', ?t (Suc k')) ∉ ?R" by blast
with steps[of k''] show False by auto
qed
next
case True
let ?P = "λ i. p i <⇩p ?p"
from LeastI_ex[of ?P, OF True] have "?P (LEAST i. ?P i)" .
then obtain i where i: "i = (LEAST i. ?P i)" and pi: "?P i" by auto
{
fix j
assume j: "j < i"
from not_less_Least[OF this[unfolded i]] have "¬ ?P j" .
with pos_cases[of ?p "p j"] have "?p ≤⇩p p j ∨ ?p ⊥ p j" by auto
} note below_or_par = this
from poss_rewrite[OF this]
have p: "?p ∈ poss (f i)" and rewr: "(s,f i |_ ?p) ∈ ?R⇧*" by auto
from steps[of i, unfolded qrstep_r_p_s_def] have NF: "⋀ u. u ⊲ f i |_ p i ⟹ u ∈ NF_terms Q" by auto
from NF[OF less_pos_imp_supt[OF pi p]] have NF: "f i |_ ?p ∈ NF_terms Q" .
from SN_replace[OF rewr NF] have SN: "SN_on ?R {C⟨f i |_ ?p⟩}" .
{
fix w
from below_or_par have "(C⟨w⟩,replace_at (f i) ?p w) ∈ ?R⇧*"
proof (induct i)
case 0
show ?case unfolding zero by simp
next
case (Suc i)
then have steps': "(C⟨w⟩, replace_at (f i) ?p w) ∈ ?R⇧*" by auto
from poss_rewrite[OF Suc(2)] have p: "?p ∈ poss (f i)" by auto
from Suc(2)[of i] have "?p ≤⇩p p i ∨ ?p ⊥ p i" by auto
then have "(replace_at (f i) ?p w, replace_at (f (Suc i)) ?p w) ∈ ?R⇧*"
proof
assume "?p ⊥ p i"
from parallel_qrstep_r_p_s[OF this p steps[of i]]
show ?thesis by auto
next
assume "?p ≤⇩p p i"
from ctxt_of_pos_term_replace_at_below[OF p this]
have "replace_at (f (Suc i)) ?p w = replace_at (f i) ?p w"
using steps[of i, unfolded qrstep_r_p_s_def] by auto
then show ?thesis by auto
qed
with steps' show ?case by auto
qed
}
from this[of "f i |_ ?p"] have steps': "(C⟨f i |_ ?p⟩, f i) ∈ ?R⇧*"
unfolding ctxt_supt_id[OF p] .
obtain g where g: "g = (λ j. f (j + i))" by auto
from steps_preserve_SN_on[OF steps' SN] have SN: "SN_on ?R {g 0}" unfolding g by auto
{
fix j
from steps[of "j + i"] have "(f (j + i), f (Suc (j + i))) ∈ ?R"
unfolding qrstep_qrstep_r_p_s_conv by blast
then have "(g j, g (Suc j)) ∈ ?R" unfolding g by auto
}
then have "¬ SN_on ?R {g 0}" by auto
with SN show False by simp
qed
qed
lemma NF_rstep_supt_args_conv:
"(∀u⊲t. u ∈ NF (rstep R)) = (∀u∈set (args t). u ∈ NF (rstep R))"
proof (cases t)
case (Var x) show ?thesis unfolding Var by auto
next
case (Fun f ts)
show ?thesis (is "?lhs = ?rhs")
proof
assume "?lhs" then show "?rhs" by (auto simp: Fun)
next
assume "?rhs" show "?lhs"
proof (intro allI impI)
fix u assume "u ⊲ t"
from supt_Fun_imp_arg_supteq[OF this[unfolded Fun]]
obtain t where "t ∈ set ts" and "t ⊵ u" by best
from ‹?rhs›[unfolded Fun] and ‹t ∈ set ts› have "t ∈ NF (rstep R)" by simp
from this and ‹t ⊵ u› show "u ∈ NF (rstep R)" by (rule NF_subterm)
qed
qed
qed
lemma NF_terms_args_conv:
"(∀u∈set (args t). u ∈ NF_terms T) = (∀u⊲t. u ∈ NF_terms T)"
using NF_rstep_supt_args_conv[symmetric,of t "Id_on T"] .
lemma ctxt_closed_qrstep [intro]: "ctxt.closed (qrstep nfs Q R)"
unfolding ctxt.closed_def
proof (rule subrelI)
fix s t
assume "(s, t) ∈ ctxt.closure (qrstep nfs Q R)"
then show "(s, t) ∈ qrstep nfs Q R" by induct auto
qed
lemma qrsteps_ctxt_closed:
assumes "(s, t) ∈ (qrstep nfs Q R)⇧*"
shows "(C⟨s⟩, C⟨t⟩) ∈ (qrstep nfs Q R)⇧*"
by (rule ctxt.closedD[OF _ assms], blast)
lemma not_NF_rstep_minimal:
assumes "s ∉ NF (rstep R)"
shows "∃t⊴s. t ∉ NF (rstep R) ∧ (∀u⊲t. u ∈ NF (rstep R))"
using assms proof (induct s rule: subterm_induct)
case (subterm v)
then show ?case
proof (cases "∀w⊲v. w ∈ NF (rstep R)")
case True with subterm(2) show ?thesis by auto
next
case False
then obtain w where "v ⊳ w" and "w ∉ NF (rstep R)" by auto
with subterm(1) obtain t where "w ⊵ t" and notNF: "t ∉ NF (rstep R)"
and NF: "∀u⊲t. u ∈ NF (rstep R)" by auto
from ‹v ⊳ w› and ‹w ⊵ t› have "v ⊵ t" using supt_supteq_trans[of v w t] by auto
with notNF and NF show ?thesis by auto
qed
qed
lemma Var_NF_terms: assumes no_lhs_var: "⋀ l. l ∈ Q ⟹ is_Fun l"
shows "Var x ∈ NF_terms Q"
proof (rule ccontr)
assume "Var x ∉ NF_terms Q"
then obtain l C σ where l: "l ∈ Q" and x: "Var x = C ⟨ l ⋅ σ ⟩" by blast
from x have "Var x = l ⋅ σ" by (cases C, auto)
with no_lhs_var[OF l] show False by auto
qed
lemma rstep_imp_irstep:
assumes st: "(s, t) ∈ rstep R" and no_lhs_var: "⋀ l r. nfs ⟹ (l,r) ∈ R ⟹ is_Fun l"
shows "∃u. (s, u) ∈ irstep nfs R"
proof -
from assms have "s ∉ NF (rstep R)" by auto
from not_NF_rstep_minimal[OF this] obtain u where "s ⊵ u" and notNF: "u ∉ NF (rstep R)"
and NF: "∀w⊲u. w ∈ NF (rstep R)" by auto
from notNF obtain v where "(u, v) ∈ rstep R" by auto
then obtain l r C σ where "(l, r) ∈ R" and u: "u = C⟨l ⋅ σ⟩" and v: "v = C⟨r ⋅ σ⟩" by auto
from u have "u ⊵ l ⋅ σ" by auto
have nf: "∀w⊲l ⋅ σ. w ∈ NF (rstep R)"
proof (intro allI impI)
fix w assume "l ⋅ σ ⊳ w"
with ‹u ⊵ l ⋅ σ› have "u ⊳ w" by (rule supteq_supt_trans)
with NF show "w ∈ NF (rstep R)" by auto
qed
let ?sigma = "λ x. if x ∈ vars_term l then σ x else Var x"
obtain v where v: "v = C ⟨ r ⋅ ?sigma ⟩" by auto
have lsig: "l ⋅ σ = l ⋅ ?sigma"
by (rule term_subst_eq, auto)
have "NF_subst nfs (l,r) ?sigma (lhss R)"
unfolding NF_subst_def
proof (intro impI subsetI)
fix t
assume nfs: nfs
assume "t ∈ ?sigma ` vars_rule (l,r)"
then obtain x where x: "x ∈ vars_rule (l,r)" and t: "t = ?sigma x" by auto
show "t ∈ NF_terms (lhss R)"
proof (cases "x ∈ vars_term l")
case True
then have "Var x ⊴ l" by auto
with no_lhs_var[OF nfs ‹(l,r) ∈ R›] have "Var x ⊲ l" by (cases l, auto)
then have "Var x ⋅ σ ⊲ l ⋅ σ" by (rule supt_subst)
with nf show ?thesis unfolding t using True by simp
next
case False
then have t: "t = Var x" unfolding t by auto
show ?thesis unfolding t
by (rule Var_NF_terms, insert no_lhs_var[OF nfs], auto)
qed
qed
with nf ‹(l, r) ∈ R› and u and v have "(u, v) ∈ irstep nfs R"
unfolding irstep_def and NF_terms_lhss[symmetric, of R] lsig by blast
from ‹s ⊵ u› obtain C where "s = C⟨u⟩" by auto
from ‹(u, v) ∈ irstep nfs R› have "(C⟨u⟩, C⟨v⟩) ∈ irstep nfs R" unfolding irstep_def by auto
then show ?thesis unfolding ‹s = C⟨u⟩› by best
qed
lemma NF_irstep_NF_rstep:
assumes no_lhs_var: "⋀ l r. nfs ⟹ (l,r) ∈ R ⟹ is_Fun l"
shows "NF (irstep nfs R) = NF (rstep R)"
proof -
have "irstep nfs R ⊆ rstep R" unfolding irstep_def ..
from NF_anti_mono[OF this] have "NF (rstep R) ⊆ NF (irstep nfs R)" .
moreover have "NF (irstep nfs R) ⊆ NF (rstep R)"
proof
fix s assume "s ∈ NF (irstep nfs R)" show "s ∈ NF (rstep R)"
proof (rule ccontr)
assume "s ∉ NF (rstep R)"
then obtain t where "(s, t) ∈ rstep R" by auto
from rstep_imp_irstep[OF this no_lhs_var, of nfs]
obtain u where "(s, u) ∈ irstep nfs R" by force
with ‹s ∈ NF (irstep nfs R)› show False by auto
qed
qed
ultimately show ?thesis by simp
qed
definition
applicable_rule :: "('f, 'v) terms ⇒ ('f, 'v) rule ⇒ bool"
where
"applicable_rule Q lr ≡ ∀s⊲fst lr. s ∈ NF_terms Q"
lemma applicable_rule_empty: "applicable_rule {} lr"
unfolding applicable_rule_def by auto
lemma only_applicable_rules:
assumes "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
shows "applicable_rule Q (l, r)"
unfolding applicable_rule_def
proof (intro allI impI)
fix s assume "fst (l, r) ⊳ s"
then have "l ⊳ s" by simp
then have "l ⋅ σ ⊳ s ⋅ σ" by (rule supt_subst)
with assms have "s ⋅ σ ∈ NF_terms Q" by simp
from NF_instance[OF this] show "s ∈ NF_terms Q" .
qed
definition
applicable_rules :: "('f, 'v) terms ⇒ ('f, 'v) trs ⇒ ('f, 'v) trs"
where
"applicable_rules Q R ≡ {(l, r) | l r. (l, r) ∈ R ∧ applicable_rule Q (l, r)}"
lemma applicable_rules_union: "applicable_rules Q (R ∪ S) = applicable_rules Q R ∪ applicable_rules Q S"
unfolding applicable_rules_def by auto
lemma applicable_rules_empty[simp]:
"applicable_rules {} R = R"
unfolding applicable_rules_def using applicable_rule_empty by auto
lemma applicable_rules_subset: "applicable_rules Q R ⊆ R"
unfolding applicable_rules_def applicable_rule_def by auto
lemma qrstep_applicable_rules: "qrstep nfs Q (applicable_rules Q R) = qrstep nfs Q R"
proof -
let ?U = "applicable_rules Q R"
show ?thesis
proof
show "qrstep nfs Q ?U ⊆ qrstep nfs Q R" by (rule qrstep_rules_mono[OF applicable_rules_subset])
next
show "qrstep nfs Q R ⊆ qrstep nfs Q ?U"
proof (rule subrelI)
fix s t
assume "(s,t) ∈ qrstep nfs Q R"
then obtain l r C σ where "(l, r) ∈ R" and NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q" by auto
with only_applicable_rules[OF NF] have "(l, r) ∈ ?U" by (auto simp: applicable_rules_def)
with NF and ‹(l, r) ∈ R› and s and t and nfs show "(s, t) ∈ qrstep nfs Q ?U" by auto
qed
qed
qed
lemma ndef_applicable_rules: "¬ defined R x ⟹ ¬ defined (applicable_rules Q R) x"
unfolding defined_def applicable_rules_def by auto
lemma nvar_qrstep_Fun:
assumes nvar: "∀ (l, r) ∈ R. is_Fun l"
and step: "(s, t) ∈ qrstep nfs Q R"
shows "∃f ts. s = Fun f ts"
proof (cases s)
case (Var x)
from step obtain C σ l r where x: "Var x = C⟨l ⋅ σ⟩" and lr: "(l, r) ∈ R" unfolding Var
by auto
from nvar lr obtain f ls where l: "l = Fun f ls" by (cases l, auto)
then show ?thesis using x by (cases C, auto)
qed auto
text ‹weakly well-formedness (all applicable rules are well-formed).›
definition
wwf_rule :: "('f, 'v) terms ⇒ ('f, 'v) rule ⇒ bool"
where
"wwf_rule Q lr ≡
applicable_rule Q lr ⟶ (is_Fun (fst lr) ∧ vars_term (snd lr) ⊆ vars_term (fst lr))"
definition
wwf_qtrs :: "('f, 'v) terms ⇒ ('f, 'v) trs ⇒ bool"
where
"wwf_qtrs Q R ≡ ∀(l, r)∈R. applicable_rule Q (l, r) ⟶ (is_Fun l ∧ vars_term r ⊆ vars_term l)"
lemma wwf_qtrs_wwf_rules: "wwf_qtrs Q R = (∀(l, r)∈R. wwf_rule Q (l, r))"
unfolding wwf_qtrs_def wwf_rule_def by auto
lemma wwf_qtrs_wf_trs: "wwf_qtrs Q R = wf_trs (applicable_rules Q R)"
unfolding wwf_qtrs_def wf_trs_def applicable_rules_def by force
lemma wwf_qtrs_empty: "wwf_qtrs {} R = wf_trs R"
unfolding wwf_qtrs_wf_trs applicable_rules_empty by simp
lemma left_Var_imp_not_SN_qrstep:
assumes xr: "(Var x, r) ∈ R" and nfs: "¬ nfs" shows "¬ (SN_on (qrstep nfs Q R) {t})"
proof -
have steps: "∀t. ∃s. (t, s) ∈ qrstep nfs Q R"
proof
fix t
show "∃s. (t, s) ∈ qrstep nfs Q R"
proof (induct t)
case (Var y)
let ?xt = "subst x (Var y)"
let ?rxt = "r ⋅ ?xt"
have NF: "∀u⊲Var x ⋅ ?xt. u ∈ NF_terms Q" by auto
have "(Var x ⋅ ?xt, ?rxt) ∈ qrstep nfs Q R"
by (rule qrstep.subst[OF NF xr, of nfs], insert nfs, simp)
then show ?case by auto
next
case (Fun f ss)
show ?case
proof (cases ss)
case Nil
let ?xt = "subst x (Fun f ss)"
let ?rxt = "r ⋅ ?xt"
have "∀u⊲Var x ⋅ ?xt. u ∈ NF_terms Q" unfolding Nil by auto
from qrstep.subst[OF this xr, of nfs]
have "(Var x ⋅ ?xt, ?rxt) ∈ qrstep nfs Q R" using nfs by simp
then show ?thesis by auto
next
case (Cons s ts)
with Fun obtain t where step: "(s, t) ∈ qrstep nfs Q R" by auto
let ?C = "More f [] □ ts"
from Cons have id: "Fun f ss = ?C⟨s⟩" by auto
have "(?C⟨s⟩, ?C⟨t⟩) ∈ ctxt.closure (qrstep nfs Q R)" by (blast intro: step)
with ctxt_closed_qrstep[of nfs Q R]
have "(Fun f ss, ?C⟨t⟩) ∈ qrstep nfs Q R"
unfolding ctxt.closed_def id by auto
then show ?thesis by auto
qed
qed
qed
from choice[OF this]
obtain f where steps: "⋀ t. (t, f t) ∈ qrstep nfs Q R" by blast
show ?thesis
by (rule steps_imp_not_SN_on, rule steps)
qed
lemma ctxt_compose_Suc: "(C ^ Suc i)⟨t⟩ = (C ^ i)⟨C⟨t⟩⟩"
using ctxt_power_compose_distr[of C i "Suc 0"] by simp
lemma SN_on_imp_wwf_rule:
assumes SN: "SN_on (qrstep nfs Q R) {t}"
and t: "t = C⟨l ⋅ σ⟩" and lr: "(l, r) ∈ R" and NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and nfs: "¬ nfs"
shows "wwf_rule Q (l, r)"
proof (cases "vars_term r ⊆ vars_term l")
case True
from left_Var_imp_not_SN_qrstep[of _ _ R nfs Q t] lr SN nfs have "is_Fun l" by (induct l) auto
with True show ?thesis unfolding wwf_rule_def by auto
next
case False
then obtain x where "x ∈ vars_term r - vars_term l" by auto
then have not_in_l: "x ∉ vars_term l" by auto
from only_applicable_rules[OF NF] have "applicable_rule Q (l,r)" .
let ?δ = "(λy. if y = x then l ⋅ σ else σ y)"
have "l ⋅ σ = l ⋅ (σ |s (vars_term l))" by (rule coincidence_lemma)
also have "… = l ⋅ (?δ |s (vars_term l))"
proof (rule arg_cong[of _ _ "(⋅) l"])
show "σ |s vars_term l = ?δ |s vars_term l"
proof -
have main: "(if y ∈ vars_term l then σ y else Var y) =
(if y ∈ vars_term l then if y = x then l ⋅ σ else σ y else Var y)" for y
by (cases "y = x", auto simp: not_in_l)
show ?thesis unfolding subst_restrict_def by (rule ext, simp add: main)
qed
qed
also have "… = l ⋅ ?δ" by (rule coincidence_lemma[symmetric])
finally have lsld: "l ⋅ σ = l ⋅?δ" .
from ‹x ∈ vars_term r - vars_term l› have in_r: "x ∈ vars_term r" by auto
from supteq_Var[OF in_r] obtain C where "r = C⟨Var x⟩" by auto
then have "r ⋅ ?δ = (C ⋅⇩c ?δ)⟨l ⋅ ?δ⟩" by (auto simp: lsld)
then obtain C where rd: "r ⋅ ?δ = C⟨l ⋅ ?δ⟩" by auto
obtain ls where ls: "l ⋅ σ = ls" by auto
obtain f where f: "⋀i. f i = (C^i)⟨l ⋅ ?δ⟩" by auto
have steps: "chain (qrstep nfs Q R) f"
proof
fix i
show "(f i, f (Suc i)) ∈ qrstep nfs Q R"
proof
show "∀u⊲l ⋅ ?δ. u ∈ NF_terms Q" unfolding lsld[symmetric] by fact
show "(l, r) ∈ R" by fact
show "f i = (C^i)⟨l ⋅ ?δ⟩" by fact
show "f (Suc i) = (C ^ i)⟨r ⋅ ?δ⟩" using f[of "Suc i", unfolded ctxt_compose_Suc rd[symmetric]] .
qed (insert nfs, auto)
qed
have start: "f 0 = l ⋅ σ"
by (simp add: f lsld[symmetric] ls)
from start steps have nSN: "¬ (SN_on (qrstep nfs Q R) {l ⋅ σ})" unfolding SN_on_def by auto
from not_SN_subt_imp_not_SN[OF ctxt_closed_qrstep nSN ctxt_imp_supteq] SN[simplified t]
have False ..
then show ?thesis ..
qed
lemma SN_imp_wwf_qtrs:
assumes "SN (qrstep nfs Q R)" and nfs: "¬ nfs" shows "wwf_qtrs Q R"
proof (rule ccontr)
assume "¬ wwf_qtrs Q R"
then obtain l r where lr: "(l, r) ∈ R" and not_wwf: "¬ wwf_rule Q (l, r)"
unfolding wwf_qtrs_wwf_rules by auto
then have applicable: "applicable_rule Q (l, r)" unfolding wwf_rule_def by auto
from assms have SN: "SN_on (qrstep nfs Q R) {l}" unfolding SN_defs by auto
from SN_on_imp_wwf_rule[OF SN _ lr _ nfs, of □ Var] and not_wwf
have "¬ (∀u⊲l. u ∈ NF_terms Q)" by auto
then obtain u where "l ⊳ u" and not_NF: "u ∉ NF_terms Q" by auto
from not_NF obtain v where "(u, v) ∈ rstep (Id_on Q)" by auto
from ‹l ⊳ u› obtain D where "D ≠ □" and "l = D⟨u⟩" by auto
with applicable[unfolded applicable_rule_def] and ‹(u, v) ∈ rstep (Id_on Q)› show False by auto
qed
lemma left_Var_applicable: "applicable_rule Q (Var x,r)"
unfolding applicable_rule_def using Var_supt[of x] by auto
lemma wwf_qtrs_imp_left_fun:
assumes "wwf_qtrs Q R" and "(l, r) ∈ R" shows "∃f ls. l = Fun f ls"
using assms unfolding wwf_qtrs_def
using left_Var_applicable[of Q _ r] by (cases l) auto
lemma wwf_var_cond:
assumes wwf: "wwf_qtrs Q R" shows "∀(l, r)∈R. is_Fun l"
using wwf_qtrs_imp_left_fun[OF wwf] by auto
definition
rqrstep :: "bool ⇒ ('f, 'v) terms ⇒ ('f, 'v) trs ⇒ ('f, 'v) term rel"
where
"rqrstep nfs Q R =
{(s, t). ∃l r σ. (∀u⊲l ⋅ σ. u ∈ NF_terms Q) ∧ (l, r) ∈ R ∧ s = l ⋅ σ ∧ t = r ⋅ σ ∧ NF_subst nfs (l,r) σ Q}"
lemma rqrstep_union: "rqrstep nfs Q (R ∪ S) = rqrstep nfs Q R ∪ rqrstep nfs Q S"
unfolding rqrstep_def by blast
lemma rqrstep_rrstep_conv[simp]:
"rqrstep nfs {} R = rrstep R"
by (auto simp: rrstep_def' rqrstep_def)
definition
nrqrstep :: "bool ⇒ ('f, 'v) terms ⇒ ('f, 'v) trs ⇒ ('f, 'v) term rel"
where
"nrqrstep nfs Q R =
{(s, t). ∃l r C σ.
(∀u⊲l ⋅ σ. u ∈ NF_terms Q) ∧ (l, r) ∈ R ∧ C ≠ □ ∧ s = C⟨l ⋅ σ⟩ ∧ t = C⟨r ⋅ σ⟩ ∧ NF_subst nfs (l,r) σ Q}"
lemma rqrstepI[intro]:
assumes "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and "(l, r) ∈ R"
and "s = l ⋅ σ" and "t = r ⋅ σ"
and "NF_subst nfs (l,r) σ Q"
shows "(s, t) ∈ rqrstep nfs Q R"
using assms unfolding rqrstep_def by auto
lemma nrqrstepI[intro]:
assumes "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and "(l, r) ∈ R"
and "C ≠ □" and "s = C⟨l ⋅ σ⟩" and "t = C⟨r ⋅ σ⟩"
and "NF_subst nfs (l,r) σ Q"
shows "(s, t) ∈ nrqrstep nfs Q R"
using assms unfolding nrqrstep_def by auto
lemma rqrstepE[elim]:
assumes "(s, t) ∈ rqrstep nfs Q R"
and "⋀l r σ. ⟦∀u⊲l ⋅ σ. u ∈ NF_terms Q; (l, r) ∈ R; s = l ⋅ σ; t = r ⋅ σ; NF_subst nfs (l,r) σ Q⟧ ⟹ P"
shows "P"
using assms unfolding rqrstep_def by auto
lemma nrqrstepE[elim]:
assumes "(s, t) ∈ nrqrstep nfs Q R"
and "⋀l r C σ.
⟦∀u⊲l ⋅ σ. u ∈ NF_terms Q; (l, r) ∈ R; C ≠ □; s = C⟨l ⋅ σ⟩; t = C⟨r ⋅ σ⟩; NF_subst nfs (l,r) σ Q⟧ ⟹ P"
shows "P"
using assms unfolding nrqrstep_def by auto
lemma rqrstep_all_mono:
assumes R: "R ⊆ R'" and Q: "NF_terms Q ⊆ NF_terms Q'" and n: "Q ≠ {} ⟹ nfs' ⟹ nfs"
shows "rqrstep nfs Q R ⊆ rqrstep nfs' Q' R'"
proof
fix s t
assume "(s,t) ∈ rqrstep nfs Q R"
then obtain l r σ where s: "s = l ⋅ σ" and t: "t = r ⋅ σ" and lr: "(l,r) ∈ R"
and NF: "⋀ u. u ⊲ l ⋅ σ ⟹ u ∈ NF_terms Q"
and nfs: "NF_subst nfs (l,r) σ Q"
by auto
from nfs n Q have nfs: "NF_subst nfs' (l,r) σ Q'" unfolding NF_subst_def by auto
from NF Q have NF: "⋀ u. u ⊲ l ⋅ σ ⟹ u ∈ NF_terms Q'" by auto
from lr R have lr: "(l,r) ∈ R'" by auto
from s t lr NF nfs show "(s,t) ∈ rqrstep nfs' Q' R'" by auto
qed
lemma rqrstep_mono:
assumes R: "R ⊆ R'" and Q: "NF_terms Q ⊆ NF_terms Q'"
shows "rqrstep nfs Q R ⊆ rqrstep nfs Q' R'"
by (rule rqrstep_all_mono[OF R Q])
lemma nrqrstep_all_mono:
assumes "NF_terms Q ⊆ NF_terms Q'" and "R ⊆ R'" and "Q ≠ {} ⟹ nfs' ⟹ nfs"
shows "nrqrstep nfs Q R ⊆ nrqrstep nfs' Q' R'"
proof
fix s t
assume "(s,t) ∈ nrqrstep nfs Q R"
then obtain l r C σ
where nf: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and lr: "(l, r) ∈ R" and id: "C ≠ □" "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q"
by auto
from assms nfs have nfs: "NF_subst nfs' (l,r) σ Q'" unfolding NF_subst_def by auto
show "(s,t) ∈ nrqrstep nfs' Q' R'"
by (rule nrqrstepI[OF _ _ id], insert nf nfs lr assms, unfold NF_subst_def, auto)
qed
lemma nrqrstep_mono:
assumes "NF_terms Q ⊆ NF_terms Q'" and "R ⊆ R'"
shows "nrqrstep nfs Q R ⊆ nrqrstep nfs Q' R'"
by (rule nrqrstep_all_mono[OF assms])
lemma nrqrstep_imp_Fun_qrstep: assumes "(s,t) ∈ nrqrstep nfs Q R"
shows "∃ f bef aft si ti. s = Fun f (bef @ si # aft) ∧ t = Fun f (bef @ ti # aft) ∧ (si,ti) ∈ qrstep nfs Q R"
proof -
from nrqrstepE[OF assms] obtain l r C σ where
nf: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and lr: "(l, r) ∈ R" and C: "C ≠ □"
and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" and nfs: "NF_subst nfs (l, r) σ Q" .
from C obtain f bef D aft where C: "C = More f bef D aft" by (cases C, auto)
from qrstepI[OF nf lr refl refl nfs, of D] show ?thesis unfolding s t C by auto
qed
lemma qrstep_funas_term: assumes wwf: "wwf_qtrs Q R"
and RF: "funas_trs R ⊆ F"
and sF: "funas_term s ⊆ F"
and step: "(s,t) ∈ qrstep nfs Q R"
shows "funas_term t ⊆ F"
proof -
from qrstepE[OF step] obtain C σ l r
where nf: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and lr: "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" and nfs: "NF_subst nfs (l, r) σ Q" .
from only_applicable_rules[OF nf] lr wwf[unfolded wwf_qtrs_def] have vars: "vars_term r ⊆ vars_term l" by auto
from RF lr have rF: "funas_term r ⊆ F"
unfolding funas_trs_def funas_rule_def [abs_def] by force
from sF show ?thesis unfolding s t using vars rF by (force simp: funas_term_subst)
qed
lemma qrsteps_funas_term: assumes wwf: "wwf_qtrs Q R"
and RF: "funas_trs R ⊆ F"
and sF: "funas_term s ⊆ F"
and steps: "(s,t) ∈ (qrstep nfs Q R)⇧*"
shows "funas_term t ⊆ F"
using steps
proof (induct)
case base
show ?case by fact
next
case (step t u)
from qrstep_funas_term[OF wwf RF step(3) step(2)] show ?case .
qed
lemma nrqrstep_funas_args_term: assumes wwf: "wwf_qtrs Q R"
and RF: "funas_trs R ⊆ F"
and sF: "funas_args_term s ⊆ F"
and step: "(s,t) ∈ nrqrstep nfs Q R"
shows "funas_args_term t ⊆ F"
proof -
from nrqrstep_imp_Fun_qrstep[OF step] obtain
f bef aft si ti where s: "s = Fun f (bef @ si # aft)" and t: "t = Fun f (bef @ ti # aft)" and step: "(si, ti) ∈ qrstep nfs Q R"
by blast
from sF s have "funas_term si ⊆ F" unfolding funas_args_term_def by force
from qrstep_funas_term[OF wwf RF this step] show ?thesis using sF unfolding s t funas_args_term_def by force
qed
lemma qrstep_iff_rqrstep_or_nrqrstep:
"qrstep nfs Q R = rqrstep nfs Q R ∪ nrqrstep nfs Q R" (is "?step = ?root ∪ ?nonroot")
proof
show "?step ⊆ ?root ∪ ?nonroot"
proof
fix s t assume "(s, t) ∈ ?step"
then obtain C l r σ where NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and
in_R: "(l, r) ∈ R" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
and "NF_subst nfs (l,r) σ Q" by auto
then show "(s, t) ∈ ?root ∪ ?nonroot" by (cases "C = □") auto
qed
next
show "?root ∪ ?nonroot ⊆ ?step"
proof (intro subrelI, elim UnE)
fix s t assume "(s, t) ∈ rqrstep nfs Q R"
then obtain l r σ where NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and
in_R: "(l, r) ∈ R" and s: "s = □⟨l ⋅ σ⟩" and t: "t = □⟨r ⋅ σ⟩"
and "NF_subst nfs (l,r) σ Q" by auto
then show "(s, t) ∈ qrstep nfs Q R" using qrstepI[of l σ Q r R s □ t] by simp
next
fix s t assume "(s, t) ∈ nrqrstep nfs Q R" then show "(s, t) ∈ qrstep nfs Q R" by auto
qed
qed
lemma qrstep_imp_ctxt_nrqrstep:
assumes "(s,t) ∈ qrstep nfs Q R"
shows "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ nrqrstep nfs Q R"
using assms
proof
fix C σ l r
assume nf: "∀ u ⊲ l ⋅ σ. u ∈ NF_terms Q" and
lr:"(l,r) ∈ R"
and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q"
have C: "More f bef C aft ≠ □" by auto
show ?thesis
unfolding nrqrstep_def
apply (intro CollectI, unfold split)
apply (intro exI conjI)
apply (rule nf)
apply (rule lr)
apply (rule C)
by (auto simp: s t nfs)
qed
lemma qrsteps_imp_ctxt_nrqrsteps:
assumes "(s,t) ∈ (qrstep nfs Q R)⇧*"
shows "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ (nrqrstep nfs Q R)⇧*"
using assms
proof (induct)
case (step t u)
from step(3) qrstep_imp_ctxt_nrqrstep[OF step(2), of f bef aft]
show ?case by auto
qed simp
lemma ctxt_closed_nrqrstep [intro]: "ctxt.closed (nrqrstep nfs Q R)"
proof (rule one_imp_ctxt_closed)
fix f bef s t aft
assume "(s,t) ∈ nrqrstep nfs Q R"
from this[unfolded nrqrstep_def] obtain l r C σ
where NF: "∀ u ⊲ l ⋅ σ. u ∈ NF_terms Q" and lr: "(l,r) ∈ R" and C: "C ≠ □"
and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r ⋅ σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q" by auto
show "(Fun f (bef @ s # aft), Fun f (bef @ t # aft)) ∈ nrqrstep nfs Q R"
proof (rule nrqrstepI[OF NF lr _ _ _ nfs])
show "More f bef C aft ≠ □" by simp
qed (insert s t, auto)
qed
lemma nrqrstep_union: "nrqrstep nfs Q (R ∪ S) = nrqrstep nfs Q R ∪ nrqrstep nfs Q S"
unfolding nrqrstep_def by blast
lemma nrqrstep_imp_arg_qrstep:
assumes "(s, t) ∈ nrqrstep nfs Q R"
shows "∃ i < length (args s). (args s ! i, args t ! i) ∈ (qrstep nfs Q R)"
proof -
from assms obtain l r C σ where NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and in_R: "(l, r) ∈ R" and ne: "C ≠ □" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q" by auto
from ne obtain f ss1 D ss2 where C: "C = More f ss1 D ss2" by (cases C) auto
let ?i = "length ss1"
show ?thesis
by (rule exI[of _ ?i], unfold s C t, insert in_R NF nfs, auto)
qed
lemma nrqrstep_imp_arg_qrsteps:
assumes "(s, t) ∈ nrqrstep nfs Q R"
shows "(args s ! i, args t ! i) ∈ (qrstep nfs Q R)^="
proof -
from assms obtain l r C σ where NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and in_R: "(l, r) ∈ R" and ne: "C ≠ □" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
and nfs: "NF_subst nfs (l,r) σ Q" by auto
from ne obtain f ss1 D ss2 where C: "C = More f ss1 D ss2" by (cases C) auto
let ?i = "length ss1"
have "i < ?i ∨ i = ?i ∨ i > ?i" by auto
then show ?thesis
proof (elim disjE)
assume "i < ?i"
with append_Cons_nth_left[OF this] show ?thesis by (simp add: s t C)
next
assume "i = ?i"
with append_Cons_nth_middle[OF this] show ?thesis using NF in_R s t nfs by (auto simp: C)
next
assume "i > ?i"
with append_Cons_nth_right[OF this] show ?thesis by (simp add: s t C)
qed
qed
lemma nrqrsteps_imp_arg_qrsteps:
assumes "(s, t) ∈ (nrqrstep nfs Q R)⇧*" shows "(args s ! i, args t ! i) ∈ (qrstep nfs Q R)⇧*"
using assms proof (induct rule: rtrancl_induct)
case (step u v)
with nrqrstep_imp_arg_qrsteps[of u v nfs Q R i] show ?case by auto
qed simp
lemma nrqrsteps_imp_arg_qrsteps_count:
assumes "(s, t) ∈ (nrqrstep nfs Q R)^^n" shows "∃ m. m ≤ n ∧ (args s ! i, args t ! i) ∈ (qrstep nfs Q R)^^m"
using assms proof (induct n arbitrary: t)
case (Suc n u)
from Suc(2) obtain t where st: "(s, t) ∈ (nrqrstep nfs Q R)^^n" and tu: "(t,u) ∈ nrqrstep nfs Q R" by auto
from Suc(1)[OF st] obtain m where m: "m ≤ n" and st: "(args s ! i, args t ! i) ∈ (qrstep nfs Q R)^^m" by auto
from nrqrstep_imp_arg_qrsteps[OF tu, of i] have "(args t ! i, args u ! i) ∈ Id ∪ qrstep nfs Q R" (is "?tu ∈ _") by auto
then show ?case
proof
assume "?tu ∈ Id" with st m show ?case by (intro exI[of _ m], auto)
next
assume "?tu ∈ qrstep nfs Q R" with st m show ?case by (intro exI[of _ "Suc m"], auto)
qed
qed simp
lemma nrqrstep_preserves_root:
assumes "(s, t) ∈ nrqrstep nfs Q R"
shows "root s = root t"
using assms
proof (standard, goal_cases)
case (1 l r C σ)
hence t: "t = C⟨r ⋅ σ⟩" and "C ≠ □" and s: "s = C⟨l ⋅ σ⟩" by auto
then obtain f ss1 D ss2 where "C = More f ss1 D ss2" by (cases C) auto
then show ?thesis unfolding s t by auto
qed
lemma nrqrsteps_preserve_root:
assumes "(s,t) ∈ (nrqrstep nfs Q R)⇧*"
shows "root s = root t"
using assms by induct (auto simp: nrqrstep_preserves_root)
lemma nrqrstep_preserves_root_fun:
assumes step: "(Fun f ss, t) ∈ nrqrstep nfs Q R"
shows "∃ts. t = Fun f ts"
using nrqrstep_preserves_root[OF step] by (cases t, auto)
lemma nrqrsteps_preserve_root_fun:
assumes step: "(Fun f ss, t) ∈ (nrqrstep nfs Q R)⇧*"
shows "∃ts. t = Fun f ts"
using nrqrsteps_preserve_root[OF step] by (cases t, auto)
lemma nrqrstep_num_args:
assumes "(s, t) ∈ nrqrstep nfs Q R" shows "num_args s = num_args t"
proof -
from assms obtain l r C σ where "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and "(l, r) ∈ R" and "C ≠ □" and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩" by auto
show ?thesis unfolding s t by (cases C) (auto simp: ‹C ≠ □›)
qed
lemma nrqrsteps_num_args:
assumes "(s, t) ∈ (nrqrstep nfs Q R)⇧*" shows "num_args s = num_args t"
using assms by (induct rule: rtrancl.induct) (auto simp: nrqrstep_num_args)
context
fixes shp :: "'f ⇒ 'f"
begin
interpretation sharp_syntax .
lemma nrqrstep_imp_sharp_qrstep:
assumes step: "(s,t) ∈ nrqrstep nfs Q R"
shows "(♯ s, ♯ t) ∈ nrqrstep nfs Q R"
proof -
let ?qr = "qrstep nfs Q R"
let ?nr = "nrqrstep nfs Q R"
let ?Q = "Q"
let ?R = "R"
let ?Iqr = "nrqrstep nfs ?Q ?R"
from step obtain l r C σ where C: "C ≠ □" and lr: "(l,r) ∈ R" and s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩"
and NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" "NF_subst nfs (l,r) σ Q"
unfolding nrqrstep_def rstep_r_c_s_def by auto
from C obtain D f bef aft where C: "C = More f bef D aft" by (cases C, auto)
let ?Dl = "D⟨l ⋅ σ⟩"
let ?Dr = "D⟨r ⋅ σ⟩"
let ?C = "More (♯ f) bef □ aft"
from s t C have s: "s = Fun f (bef @ ?Dl # aft)" and t: "t = Fun f (bef @ ?Dr # aft)" by auto
from lr NF have "(?Dl,?Dr) ∈ ?qr" by auto
from qrstep_imp_ctxt_nrqrstep[OF this]
have "(?C⟨?Dl⟩,?C⟨?Dr⟩) ∈ ?Iqr" by simp
with s t show ?thesis by auto
qed
lemma nrqrsteps_imp_sharp_qrsteps:
assumes step: "(s,t) ∈ (nrqrstep nfs Q R)⇧*"
shows "(♯ s, ♯ t) ∈ (nrqrstep nfs Q R)⇧*"
using step
proof (induct rule: rtrancl_induct)
case (step u v)
from nrqrstep_imp_sharp_qrstep[OF step(2)] and step(3)
show ?case by auto
qed simp
end
lemma qrstep_imp_nrqrstep:
assumes nvar: "∀(l, r)∈R. is_Fun l"
and ndef: "¬ defined (applicable_rules Q R) (the (root s))"
and step: "(s, t) ∈ qrstep nfs Q R"
shows "(s, t) ∈ nrqrstep nfs Q R"
proof -
from step[unfolded qrstep_iff_rqrstep_or_nrqrstep]
show ?thesis
proof
assume "(s,t) ∈ rqrstep nfs Q R"
then show ?thesis
proof
fix l r σ
assume lr: "(l,r) ∈ R" and id: "s = l ⋅ σ" and
nf: "∀ u ⊲ l ⋅ σ. u ∈ NF_terms Q"
with nvar have "is_Fun l" by auto
then obtain f ll where l: "l = Fun f ll" by (cases l, auto)
with id obtain ss where s: "s = Fun f ss" "length ll = length ss" by (cases s, auto)
from only_applicable_rules[OF nf] lr have ulr: "(l,r) ∈ applicable_rules Q R"
unfolding applicable_rules_def by auto
from id[unfolded l s] ndef[unfolded s] ulr[unfolded l]
have False unfolding defined_def by force
then show ?thesis by simp
qed
qed
qed
lemma qrsteps_imp_nrqrsteps:
assumes nvar: "∀(l, r)∈R. is_Fun l"
and ndef: "¬ defined (applicable_rules Q R) (the (root s))"
and steps: "(s,t) ∈ (qrstep nfs Q R)⇧*"
shows "(s,t) ∈ (nrqrstep nfs Q R)⇧*"
using steps
proof (induct)
case (step t u)
have "(t,u) ∈ nrqrstep nfs Q R"
proof (rule qrstep_imp_nrqrstep[OF nvar _ step(2)])
show "¬ defined (applicable_rules Q R) (the (root t))"
using ndef unfolding nrqrsteps_num_args[OF step(3)]
nrqrsteps_preserve_root[OF step(3)]
.
qed
with step(3) show ?case by auto
qed simp
lemma rel_qrsteps_imp_rel_nrqrsteps:
assumes nvar: "∀(l, r)∈R ∪ Rw. is_Fun l"
and ndef: "¬ defined (applicable_rules Q (R ∪ Rw)) (the (root s))"
and steps: "(s,t) ∈ (qrstep nfs Q (R ∪ Rw))⇧* O (qrstep nfs Q R) O (qrstep nfs Q (R ∪ Rw))⇧*"
shows "(s,t) ∈ (nrqrstep nfs Q (R ∪ Rw))⇧* O nrqrstep nfs Q R O (nrqrstep nfs Q (R ∪ Rw))⇧*"
proof -
let ?Rw = "qrstep nfs Q (R ∪ Rw)"
let ?R = "qrstep nfs Q R"
let ?Rwb = "nrqrstep nfs Q (R ∪ Rw)"
let ?Rb = "nrqrstep nfs Q R"
from steps obtain u v where su: "(s,u) ∈ ?Rw⇧*" and uv: "(u,v) ∈ ?R" and vt: "(v,t) ∈ ?Rw⇧*" by blast
from qrsteps_imp_nrqrsteps[OF nvar ndef su] have su: "(s,u) ∈ ?Rwb⇧*" .
note ndef = ndef[unfolded nrqrsteps_preserve_root[OF su]]
then have ndefR: "¬ defined (applicable_rules Q R) (the (root u))" unfolding defined_def applicable_rules_def by auto
have uv: "(u,v) ∈ ?Rb"
by (rule qrstep_imp_nrqrstep[OF _ ndefR uv], insert nvar, auto)
note ndef = ndef[unfolded nrqrstep_preserves_root[OF uv]]
from qrsteps_imp_nrqrsteps[OF nvar ndef vt] have vt: "(v,t) ∈ ?Rwb⇧*" .
from su uv vt show ?thesis by auto
qed
lemma nrqrstep_nrrstep[simp]: "nrqrstep nfs {} = nrrstep"
by (intro ext, unfold nrrstep_def' nrqrstep_def, auto)
lemma args_steps_imp_nrqrsteps:
assumes steps: "⋀ i. i < length ss ⟹ (ts ! i, ss ! i) ∈ (qrstep nfs Q R)⇧*"
and len: "length ts = length ss"
shows "(Fun f ts, Fun f ss) ∈ (nrqrstep nfs Q R)⇧*"
by (rule args_steps_imp_steps_gen[OF qrsteps_imp_ctxt_nrqrsteps len steps], auto)
lemma qrsteps_rqrstep_cases_n:
assumes "(Fun f ss, t) ∈ (qrstep nfs Q R)^^n"
shows "(∃ts.
length ts = length ss ∧
t = Fun f ts ∧
(∀i<length ss. ∃m ≤ n. (ss ! i, ts ! i) ∈ (qrstep nfs Q R)^^m) ∧
(Fun f ss, t) ∈ (nrqrstep nfs Q R)^^n)
∨ (∃m1 < n. ∃m2 < n. (Fun f ss, t) ∈ (nrqrstep nfs Q R)^^m1 O (rqrstep nfs Q R) O (qrstep nfs Q R)^^m2)"
using assms proof (induct n arbitrary: t)
case 0 then show ?case by auto
next
let ?QR = "qrstep nfs Q R"
let ?RQR = "rqrstep nfs Q R"
let ?NRQR = "nrqrstep nfs Q R"
case (Suc m)
then obtain u where su:"(Fun f ss, u) ∈ ?QR ^^ m" and ut:"(u, t) ∈ ?QR" by auto
from Suc(1)[OF su] show ?case
proof
assume "∃m1 < m. ∃m2 < m. (Fun f ss, u) ∈ ?NRQR^^m1 O ?RQR O ?QR^^m2"
then obtain v m1 m2 where sv:"(Fun f ss, v) ∈ ?NRQR^^m1 O ?RQR ∧ m1 < m" and "(v, u) ∈ ?QR^^m2 ∧ m2 < m" by auto
with ‹(u, t) ∈ ?QR› have "(v, t) ∈ ?QR^^(Suc m2) ∧ Suc m2 < Suc m" by auto
with sv have "(Fun f ss, t) ∈ ?NRQR^^m1 O ?RQR O ?QR ^^ Suc m2 ∧ m1 < Suc m ∧ Suc m2 < Suc m" by auto
then show ?thesis by metis
next
assume "∃us. length us = length ss ∧ u = Fun f us ∧ (∀i<length ss. ∃k ≤ m. (ss!i, us!i) ∈ ?QR^^k) ∧ (Fun f ss, u) ∈ ?NRQR ^^ m"
then obtain us where len: "length us = length ss" and u: "u = Fun f us"
and isteps: "∀i<length ss. ∃k ≤ m. (ss!i, us!i) ∈ ?QR^^k" and nrsteps:"(Fun f ss, u) ∈ ?NRQR ^^ m" by auto
from ut have "(u, t) ∈ ?RQR ∨ (u, t) ∈ ?NRQR" unfolding qrstep_iff_rqrstep_or_nrqrstep by simp
then show ?thesis
proof
assume "(u, t) ∈ ?RQR"
with ‹(Fun f ss, u) ∈ ?NRQR^^m› have "(Fun f ss, t) ∈ ?NRQR^^m O ?RQR" by blast
then have "(Fun f ss, t) ∈ ?NRQR^^m O ?RQR O ?QR ^^ 0" by auto
then show ?thesis by blast
next
assume ut:"(u, t) ∈ ?NRQR"
then have st:"(Fun f ss, t) ∈ ?NRQR ^^ Suc m" using nrsteps by auto
have *: "(Fun f ss, t) ∈ ?NRQR⇧*" by (rule relpow_imp_rtrancl[OF st])
{
fix i
assume "i < length ss"
with isteps obtain k where k: "k ≤ m" and ssus:"(ss ! i, us ! i) ∈ ?QR^^k" by auto
from nrqrstep_imp_arg_qrsteps[OF ut] u have "(us ! i, args t ! i) ∈ ?QR^=" by auto
then have "us ! i = args t ! i ∨ (us ! i, args t ! i) ∈ ?QR" by auto
then have "∃k ≤ Suc m. (ss ! i, args t ! i) ∈ ?QR^^k"
proof
assume "us ! i = args t ! i"
then have "(ss ! i, args t ! i) ∈ ?QR^^k" using ssus by auto
then show ?thesis using k le_SucI by fast
next
assume "(us ! i, args t ! i) ∈ ?QR"
with ssus have "(ss ! i, args t ! i) ∈ ?QR^^(Suc k)" by auto
then show ?thesis using k Suc_le_mono by blast
qed
}
then show ?thesis using nrqrsteps_num_args[OF *] nrqrsteps_preserve_root_fun[OF *] st by auto
qed
qed
qed
lemma qrsteps_rqrstep_cases_nrqrstep:
assumes "(Fun f ss, t) ∈ (qrstep nfs Q R)⇧*"
shows "(∃ts.
length ts = length ss ∧
t = Fun f ts ∧
(∀i<length ss. (ss ! i, ts ! i) ∈ (qrstep nfs Q R)⇧*))
∨ (Fun f ss, t) ∈ (nrqrstep nfs Q R)⇧* O (rqrstep nfs Q R) O (qrstep nfs Q R)⇧*"
using assms proof (induct)
case base then show ?case by auto
next
case (step u t)
then have "(∃ts. length ts = length ss ∧ u = Fun f ts
∧ (∀i<length ss. (ss!i, ts!i) ∈ (qrstep nfs Q R)⇧*))
∨ (Fun f ss, u) ∈ (nrqrstep nfs Q R)⇧* O rqrstep nfs Q R O (qrstep nfs Q R)⇧*" by simp
then show ?case
proof
assume "(Fun f ss, u) ∈ (nrqrstep nfs Q R)⇧* O rqrstep nfs Q R O (qrstep nfs Q R)⇧*"
then obtain v where "(Fun f ss, v) ∈ (nrqrstep nfs Q R)⇧* O rqrstep nfs Q R"
and "(v, u) ∈ (qrstep nfs Q R)⇧*" by auto
with ‹(u, t) ∈ qrstep nfs Q R› have "(v, t) ∈ (qrstep nfs Q R)⇧*" by auto
with ‹(Fun f ss, v) ∈ (nrqrstep nfs Q R)⇧* O rqrstep nfs Q R› show ?thesis by auto
next
assume "∃ts. length ts = length ss ∧ u = Fun f ts
∧ (∀i<length ss. (ss!i, ts!i) ∈ (qrstep nfs Q R)⇧*)"
then obtain ts where len: "length ts = length ss" and u: "u = Fun f ts"
and steps: "∀i<length ss. (ss!i, ts!i) ∈ (qrstep nfs Q R)⇧*" by auto
from len steps have "(Fun f ss, u) ∈ (nrqrstep nfs Q R)⇧*" unfolding u
by (simp add: args_steps_imp_nrqrsteps)
from ‹(u, t) ∈ qrstep nfs Q R› have "(u, t) ∈ rqrstep nfs Q R ∨ (u, t) ∈ nrqrstep nfs Q R"
unfolding qrstep_iff_rqrstep_or_nrqrstep by simp
then show ?thesis
proof
assume "(u, t) ∈ rqrstep nfs Q R"
with ‹(Fun f ss, u) ∈ (nrqrstep nfs Q R)⇧*› have "(Fun f ss, t) ∈ (nrqrstep nfs Q R)⇧* O rqrstep nfs Q R"
by auto
then show ?thesis by auto
next
assume "(u, t) ∈ nrqrstep nfs Q R"
from nrqrstep_preserves_root[OF this[unfolded u]]
obtain us where t: "t = Fun f us" by (cases t, auto)
from nrqrstep_num_args[OF ‹(u, t) ∈ nrqrstep nfs Q R›]
have "num_args u = num_args t" by simp
then have "length ts = length us" unfolding u t by simp
with len have len': "length ss = length ts" by simp
from nrqrstep_imp_arg_qrsteps[OF ‹(u, t) ∈ nrqrstep nfs Q R›]
have "∀i<length ts. (ts!i, args t ! i) ∈ (qrstep nfs Q R)^=" unfolding u by auto
then have "∀i<length ts. (ts!i, us!i) ∈ (qrstep nfs Q R)^=" unfolding t by simp
then have next_steps: "∀i<length ts. (ts!i, us!i) ∈ (qrstep nfs Q R)⇧*" by auto
have "length us = length ss" using ‹length ts = length us› and len by simp
moreover have "t = Fun f us" by fact
moreover have "∀i<length ss. (ss!i, us!i) ∈ (qrstep nfs Q R)⇧*"
proof (intro allI impI)
fix i assume "i < length ss"
with steps have "(ss ! i, ts ! i) ∈ (qrstep nfs Q R)⇧*" by simp
moreover from ‹i < length ss› and next_steps have "(ts!i, us!i) ∈ (qrstep nfs Q R)⇧*"
unfolding len' by simp
ultimately show "(ss ! i, us ! i) ∈ (qrstep nfs Q R)⇧*" by auto
qed
ultimately show ?thesis by auto
qed
qed
qed
lemma qrsteps_rqrstep_cases:
assumes "(Fun f ss, t) ∈ (qrstep nfs Q R)⇧*"
shows "(∃ts.
length ts = length ss ∧
t = Fun f ts ∧
(∀i<length ss. (ss ! i, ts ! i) ∈ (qrstep nfs Q R)⇧*))
∨ (Fun f ss, t) ∈ (qrstep nfs Q R)⇧* O (rqrstep nfs Q R) O (qrstep nfs Q R)⇧*"
proof -
have "(nrqrstep nfs Q R)⇧* ⊆ (qrstep nfs Q R)⇧*" unfolding qrstep_iff_rqrstep_or_nrqrstep
by regexp
then show ?thesis
using qrsteps_rqrstep_cases_nrqrstep[OF assms] by auto
qed
lemma nondef_root_imp_arg_qrsteps:
assumes steps: "(Fun f ss, t) ∈ (qrstep nfs Q R)⇧*"
and vars: "∀(l, r)∈R. is_Fun l"
and ndef: "¬ defined R (f, length ss)"
shows "∃ ts. length ts = length ss ∧ t = Fun f ts ∧ (∀i<length ss. (ss ! i, ts ! i) ∈ (qrstep nfs Q R)⇧*)"
proof -
from qrsteps_rqrstep_cases[OF steps]
show ?thesis
proof
assume "(Fun f ss, t) ∈ (qrstep nfs Q R)⇧* O rqrstep nfs Q R O (qrstep nfs Q R)⇧*"
then obtain u v where su: "(Fun f ss, u) ∈ (qrstep nfs Q R)⇧*" and uv: "(u,v) ∈ rqrstep nfs Q R" by auto
from first_step[OF _ su uv, unfolded qrstep_iff_rqrstep_or_nrqrstep, OF Un_commute]
obtain u v where su: "(Fun f ss, u) ∈ (nrqrstep nfs Q R)⇧*" and uv: "(u,v) ∈ rqrstep nfs Q R" by auto
from nrqrsteps_preserve_root[OF su] nrqrsteps_num_args[OF su] obtain us where u: "u = Fun f us"
and us: "length ss = length us" by (cases u, auto)
from uv[unfolded u] rqrstep_def obtain l r σ where lr: "(l,r) ∈ R" and fus: "Fun f us = l ⋅ σ" by auto
from vars[THEN bspec[OF _ lr]] fus obtain ls where "l = Fun f ls" by (cases l, auto)
with fus lr have "defined R (f,length ss)" unfolding us defined_def by auto
with ndef
show ?thesis by auto
qed simp
qed
lemmas args_qrsteps_imp_qrsteps = args_steps_imp_steps[OF ctxt_closed_qrstep]
lemmas qrstep_imp_map_rstep = rstep_imp_map_rstep[OF qrstep_into_rstep]
lemmas qrsteps_imp_map_rsteps = rsteps_imp_map_rsteps[OF qrsteps_into_rsteps]
lemma NF_imp_subt_NF: assumes "t ∈ NF_terms Q" shows "∀u⊲t. u ∈ NF_terms Q"
proof(intro allI impI)
fix u
assume t: "t ⊳ u"
{
fix v
assume uv: "(u,v) ∈ rstep (Id_on Q)"
from t obtain C where t: "t = C⟨u⟩" by auto
from uv have "(t,C⟨v⟩) ∈ rstep (Id_on Q)" unfolding t by auto
with assms have False by auto
}
thus "u ∈ NF_terms Q" by auto
qed
lemma qrstep_diff: assumes "R ⊆ S" shows "qrstep nfs Q R - qrstep nfs Q (D ∩ S) ⊆ qrstep nfs Q (R - D)" (is "?L ⊆ ?R")
proof -
{
fix s t
assume "(s,t) ∈ ?L"
then have yes: "(s,t) ∈ qrstep nfs Q R" and no: "(s,t) ∉ qrstep nfs Q (D ∩ S)" by auto
from yes no have "(s,t) ∈ ?R"
unfolding qrstep_rule_conv[where R = R]
unfolding qrstep_rule_conv[where R = "D ∩ S"]
unfolding qrstep_rule_conv[where R = "R - D"]
using assms
by blast
}
then show ?thesis by auto
qed
lemma wwf_qtrs_qrstep_Fun:
assumes "wwf_qtrs Q R" and "(s, t) ∈ qrstep nfs Q R"
shows "∃f ss. s = Fun f ss"
proof -
from assms obtain C σ l r where "(l, r) ∈ R" and "s = C⟨l ⋅ σ⟩" by auto
from wwf_qtrs_imp_left_fun[OF assms(1) ‹(l, r) ∈ R›]
obtain f ls where l: "l = Fun f ls" by auto
show ?thesis unfolding ‹s = C⟨l ⋅ σ⟩› l by (induct C) simp_all
qed
lemma qrstep_preserves_undefined_root:
assumes ndef: "¬ defined (applicable_rules Q R) (the (root s))"
and nvar: "∀(l,r) ∈ R. is_Fun l"
and step: "(s, t) ∈ qrstep nfs Q R"
shows "¬ defined (applicable_rules Q R) (the (root t))"
proof -
from qrstep_imp_nrqrstep[OF nvar ndef step] have step: "(s,t) ∈ nrqrstep nfs Q R"
.
from ndef[unfolded nrqrstep_preserves_root[OF step] nrqrstep_num_args[OF step]] show ?thesis .
qed
lemma qrsteps_preserve_undefined_root:
assumes ndef: "¬ defined (applicable_rules Q R) (the (root s))"
and nvar: "∀(l,r) ∈ R. is_Fun l"
and step: "(s, t) ∈ (qrstep nfs Q R)⇧*"
shows "¬ defined (applicable_rules Q R) (the (root t))"
proof -
from qrsteps_imp_nrqrsteps[OF nvar ndef step] have step: "(s,t) ∈ (nrqrstep nfs Q R)⇧*"
.
from ndef[unfolded nrqrsteps_preserve_root[OF step] nrqrsteps_num_args[OF step]] show ?thesis .
qed
lemma wf_trs_imp_wwf_qtrs:
assumes "wf_trs R" shows "wwf_qtrs Q R"
using assms by (auto simp: wwf_qtrs_def wf_trs_def)
lemma SN_on_imp_qrstep_wf_rules:
assumes "SN_on (qrstep nfs Q R) {s}" and "(s, t) ∈ qrstep nfs Q R" and nfs: "¬ nfs"
shows "(s, t) ∈ qrstep nfs Q (wf_rules R)"
using ‹(s, t) ∈ qrstep nfs Q R›
proof
fix C σ l r
assume NF_terms: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
and "(l, r) ∈ R"
and s: "s = C⟨l ⋅ σ⟩" and t: "t = C⟨r ⋅ σ⟩"
show ?thesis
proof (cases "(l, r) ∈ wf_rules R")
case True then show ?thesis unfolding s t using NF_terms nfs by auto
next
case False
with ‹(l, r) ∈ R›
have "is_Var l ∨ (∃x. x ∈ vars_term r - vars_term l)"
unfolding wf_rules_def wf_rule_def by auto
then show ?thesis
proof
assume "is_Var l"
then obtain x where l: "l = Var x" by auto
from left_Var_imp_not_SN_qrstep[OF ‹(l, r) ∈ R›[unfolded l]]
and assms show ?thesis by simp
next
assume "∃x. x ∈ vars_term r - vars_term l"
then obtain x where "x ∈ vars_term r - vars_term l"
and empty: "vars_term l ∩ {x} = {}" by auto
with SN_on_imp_wwf_rule[OF assms(1) s ‹(l, r) ∈ R› NF_terms nfs]
and only_applicable_rules[OF NF_terms]
show ?thesis unfolding wwf_rule_def by auto
qed
qed
qed
lemma SN_on_imp_qrsteps_wf_rules:
assumes "(s, t) ∈ (qrstep nfs Q R)⇧*" and "SN_on (qrstep nfs Q R) {s}" and nfs: "¬ nfs"
shows "(s, t) ∈ (qrstep nfs Q (wf_rules R))⇧*"
using ‹(s, t) ∈ (qrstep nfs Q R)⇧*›
proof (induct)
case base show ?case ..
next
case (step u v)
from steps_preserve_SN_on[OF ‹(s, u) ∈ (qrstep nfs Q R)⇧*› ‹SN_on (qrstep nfs Q R) {s}›]
have "SN_on (qrstep nfs Q R) {u}" .
from SN_on_imp_qrstep_wf_rules[OF this ‹(u, v) ∈ qrstep nfs Q R› nfs]
have "(u, v) ∈ qrstep nfs Q (wf_rules R)" .
with ‹(s, u) ∈ (qrstep nfs Q (wf_rules R))⇧*› show ?case ..
qed
lemmas wwf_qtrs_wf_rules = wf_trs_imp_wwf_qtrs[OF wf_trs_wf_rules]
lemmas qrstep_wf_rules_subset = qrstep_mono[OF wf_rules_subset subset_refl]
lemma SN_on_qrstep_imp_SN_on_supt_union_qrstep:
"SN_on (qrstep nfs Q R) {t} ⟹ SN_on ({⊳} ∪ qrstep nfs Q R) {t}"
by (rule SN_on_r_imp_SN_on_supt_union_r[OF ctxt_closed_qrstep])
lemma supt_qrstep_subset:
"{⊳} O qrstep nfs Q R ⊆ qrstep nfs Q R O {⊳}"
using supteq_qrstep_subset[of nfs Q R, unfolded supteq_supt_set_conv] by best
lemma supt_Un_qrstep_trancl_subset:
"({⊳} ∪ qrstep nfs Q R)⇧+ ⊆ (qrstep nfs Q R)⇧* O {⊵}"
(is "?lhs ⊆ ?rhs")
proof
fix s t
assume "(s, t) ∈ ?lhs"
then show "(s, t) ∈ ?rhs"
proof (induct s t)
case (r_into_trancl s t)
then show ?case by (rule UnE) auto
next
case (trancl_into_trancl s t u)
from ‹(t, u) ∈ {⊳} ∪ qrstep nfs Q R›
show ?case
proof
assume "t ⊳ u"
with ‹(s, t) ∈ (qrstep nfs Q R)⇧* O {⊵}›
show ?case using supteq_trans[of _ t u] by auto
next
assume "(t, u) ∈ qrstep nfs Q R"
from ‹(s, t) ∈ (qrstep nfs Q R)⇧* O {⊵}›
obtain v where "(s, v) ∈ (qrstep nfs Q R)⇧*" and "v ⊵ t" by blast
with ‹(t, u) ∈ qrstep nfs Q R› have "(v, u) ∈ {⊵} O qrstep nfs Q R" by blast
with supteq_qrstep_subset[of nfs Q R]
have "(v, u) ∈ qrstep nfs Q R O {⊵}" by blast
with rtrancl.rtrancl_into_rtrancl[OF ‹(s, v) ∈ (qrstep nfs Q R)⇧*›]
show ?case by blast
qed
qed
qed
lemma supteq_Un_qrstep_trancl_subset:
"({⊵} ∪ qrstep nfs Q R)⇧+ ⊆ (qrstep nfs Q R)⇧* O {⊵}"
(is "?lhs ⊆ ?rhs")
proof
fix s t
assume "(s, t) ∈ ?lhs"
then show "(s, t) ∈ ?rhs"
proof (induct s t)
case (r_into_trancl s t)
then show ?case by (rule UnE) auto
next
case (trancl_into_trancl s t u)
from ‹(t, u) ∈ {⊵} ∪ qrstep nfs Q R›
show ?case
proof
assume "t ⊵ u"
with ‹(s, t) ∈ (qrstep nfs Q R)⇧* O {⊵}›
show ?case using supteq_trans[of _ t u] by auto
next
assume "(t, u) ∈ qrstep nfs Q R"
from ‹(s, t) ∈ (qrstep nfs Q R)⇧* O {⊵}›
obtain v where "(s, v) ∈ (qrstep nfs Q R)⇧*" and "v ⊵ t" by blast
with ‹(t, u) ∈ qrstep nfs Q R› have "(v, u) ∈ {⊵} O qrstep nfs Q R" by blast
with supteq_qrstep_subset[of nfs Q R]
have "(v, u) ∈ qrstep nfs Q R O {⊵}" by blast
with rtrancl.rtrancl_into_rtrancl[OF ‹(s, v) ∈ (qrstep nfs Q R)⇧*›]
show ?case by blast
qed
qed
qed
lemma supteq_Un_qrstep_rtrancl_subset:
"({⊵} ∪ qrstep nfs Q R)⇧* ⊆ (qrstep nfs Q R)⇧* O {⊵}"
proof -
from supteq_Un_qrstep_trancl_subset[of nfs Q R]
have "Id ∪ ({⊵} ∪ qrstep nfs Q R)⇧* O ({⊵} ∪ qrstep nfs Q R) ⊆ (qrstep nfs Q R)⇧* O {⊵}"
unfolding rtrancl_comp_trancl_conv
unfolding supteq_supt_set_conv by auto
then show ?thesis by auto
qed
lemma supt_Un_qrstep_subset:
"{⊳} ∪ qrstep nfs Q R ⊆ (qrstep nfs Q R)⇧* O {⊵}"
by auto
lemma supt_Un_qrstep_rtrancl_subset:
"({⊳} ∪ qrstep nfs Q R)⇧* ⊆ (qrstep nfs Q R)⇧* O {⊵}"
(is "?lhs ⊆ ?rhs")
proof
fix s t assume "(s, t) ∈ ?lhs"
then show "(s, t) ∈ ?rhs"
proof (induct s t)
case (rtrancl_refl t)
show ?case by auto
next
case (rtrancl_into_rtrancl s t u)
from ‹(t, u) ∈ {⊳} ∪ qrstep nfs Q R›
show ?case
proof
assume "t ⊳ u"
then have "t ⊵ u" by auto
with ‹(s, t) ∈ ?rhs› show ?case
using supteq_trans by blast
next
assume "(t, u) ∈ qrstep nfs Q R"
from ‹(s, t) ∈ ?rhs›
obtain v where "(s, v) ∈ (qrstep nfs Q R)⇧*" and "v ⊵ t" by auto
with ‹(t, u) ∈ qrstep nfs Q R› have "(v, u) ∈ {⊵} O qrstep nfs Q R" by auto
with supteq_qrstep_subset have "(v, u) ∈ qrstep nfs Q R O {⊵}" by blast
with rtrancl.rtrancl_into_rtrancl[OF ‹(s, v) ∈ (qrstep nfs Q R)⇧*›]
show ?case by auto
qed
qed
qed
lemma qrsteps_comp_supteq_subset:
"(qrstep nfs Q R)⇧* O {⊵} ⊆ ({⊵} ∪ qrstep nfs Q R)⇧*"
by regexp
lemma qrsteps_comp_supteq_subset':
"(qrstep nfs Q R)⇧* O {⊵} ⊆ ({⊵} ∪ qrstep nfs Q R)⇧+"
by regexp
lemma qrsteps_comp_supteq_supt_subset:
"(qrstep nfs Q R)⇧* O {⊵} ⊆ ({⊳} ∪ qrstep nfs Q R)⇧*"
unfolding supteq_supt_set_conv by (regexp)
lemma qrsteps_comp_supteq_conv:
"(qrstep nfs Q R)⇧* O {⊵} = ({⊵} ∪ qrstep nfs Q R)⇧+"
using qrsteps_comp_supteq_subset' supteq_Un_qrstep_trancl_subset by blast
lemma qrsteps_comp_supteq_conv':
"(qrstep nfs Q R)⇧* O {⊵} = ({⊵} ∪ qrstep nfs Q R)⇧*"
using qrsteps_comp_supteq_subset supteq_Un_qrstep_rtrancl_subset by blast
lemma qrsteps_comp_supteq_conv'':
"(qrstep nfs Q R)⇧* O {⊵} = ({⊳} ∪ qrstep nfs Q R)⇧*"
using qrsteps_comp_supteq_supt_subset supt_Un_qrstep_rtrancl_subset by blast
lemmas supteq_Un_qrstep_trancl_conv = qrsteps_comp_supteq_conv[symmetric]
lemmas supteq_Un_qrstep_rtrancl_conv = qrsteps_comp_supteq_conv'[symmetric]
lemmas supt_Un_qrstep_rtrancl_conv = qrsteps_comp_supteq_conv''[symmetric]
lemma rhs_free_vars_imp_sig_qrstep_not_SN_on:
assumes R: "(l,r) ∈ applicable_rules Q R" and free: "¬ vars_term r ⊆ vars_term l"
and F: "funas_trs R ⊆ F"
and nfs: "¬ nfs"
shows "¬ SN_on (sig_step F (qrstep nfs Q R)) {l}"
proof -
from free obtain x where x: "x ∈ vars_term r - vars_term l" by auto
then have "x ∈ vars_term r" by simp
from supteq_Var[OF this] have "r ⊵ Var x" .
then obtain C where r: "C⟨Var x⟩ = r" by auto
let ?σ = "λy. if y = x then l else Var y"
let ?t = "λi. ((C ⋅⇩c ?σ)^i)⟨l⟩"
from R have R': "(l,r) ∈ R" unfolding applicable_rules_def by auto
from rhs_wf[OF R' F] have wf_r: "funas_term r ⊆ F" by fast
from lhs_wf[OF R' F] have wf_l: "funas_term l ⊆ F" by fast
from wf_r[unfolded r[symmetric]]
have wf_C: "funas_ctxt C ⊆ F" by simp
from x have neq: "∀y∈vars_term l. y ≠ x" by auto
have "l⋅?σ = l ⋅ Var"
by (rule term_subst_eq, insert neq, auto)
then have l: "l⋅ ?σ = l" by simp
have rsigma: "r⋅?σ = (C ⋅⇩c ?σ)⟨l⟩" unfolding r[symmetric] by simp
from wf_C have wf_C: "funas_ctxt (C ⋅⇩c ?σ) ⊆ F" using wf_l by auto
show ?thesis
proof (rule wf_loop_imp_sig_ctxt_rel_not_SN[OF _ wf_l wf_C ctxt_closed_qrstep])
show "(l,(C ⋅⇩c ?σ)⟨l⟩) ∈ qrstep nfs Q R"
proof (rule qrstepI[OF _ R', of ?σ _ _ Hole], unfold l rsigma)
show "∀u⊲l. u ∈ NF_terms Q" using R unfolding applicable_rules_def applicable_rule_def by auto
qed (insert nfs, auto)
qed
qed
lemma lhs_var_imp_sig_qrstep_not_SN:
assumes rule: "(Var x, r) ∈ R" and F: "funas_trs R ⊆ F" and nfs: "¬ nfs"
shows "¬ SN (sig_step F (qrstep nfs Q R))"
proof -
from get_var_or_const[of r]
obtain C t where r: "r = C⟨t⟩" and args: "args t = []" by auto
from rhs_wf[OF rule subset_refl] F have wfr: "funas_term r ⊆ F" by auto
from wfr[unfolded r] F
have wfC: "funas_ctxt C ⊆ F" and wft: "funas_term t ⊆ F" by auto
let ?σ = "(λx. t)"
from wfC wft have wfC: "funas_ctxt (C ⋅⇩c ?σ) ⊆ F" by auto
have tsig: "t ⋅ ?σ = t" using args by (cases t, auto)
have "¬ SN_on (sig_step F (qrstep nfs Q R)) {t}"
proof (rule wf_loop_imp_sig_ctxt_rel_not_SN[OF _ wft wfC ctxt_closed_qrstep])
show "(t,(C ⋅⇩c ?σ)⟨t⟩) ∈ qrstep nfs Q R"
by (rule qrstepI[OF _ rule, of ?σ _ _ Hole], unfold NF_terms_args_conv[symmetric] r, auto simp: nfs tsig args)
qed
then show ?thesis unfolding SN_def by auto
qed
lemma SN_sig_qrstep_imp_wwf_trs: assumes SN: "SN (sig_step F (qrstep nfs Q R))" and F: "funas_trs R ⊆ F" and nfs: "¬ nfs"
shows "wwf_qtrs Q R"
proof (rule ccontr)
assume "¬ wwf_qtrs Q R"
then obtain l r where R: "(l,r) ∈ applicable_rules Q R"
and not_wf: "(∀f ts. l ≠ Fun f ts) ∨ ¬(vars_term r ⊆ vars_term l)" unfolding wwf_qtrs_def applicable_rules_def
by auto
from not_wf have "¬ SN (sig_step F (qrstep nfs Q R))"
proof
assume free: "¬ vars_term r ⊆ vars_term l"
from rhs_free_vars_imp_sig_qrstep_not_SN_on[OF R free F nfs] show ?thesis unfolding SN_on_def by auto
next
assume "∀f ts. l ≠ Fun f ts"
then obtain x where l:"l = Var x" by (cases l) auto
with R have "(Var x,r) ∈ R" unfolding l applicable_rules_def by simp
from lhs_var_imp_sig_qrstep_not_SN[OF this F nfs] show ?thesis .
qed
with assms show False by blast
qed
lemma linear_term_weak_match_match:
assumes "linear_term t" and "weak_match s t"
shows "∃σ. s = t ⋅ σ"
using assms
proof (induct t arbitrary: s)
case (Var x) then show ?case by auto
next
case (Fun f ts)
note Fun' = this
show ?case
proof (cases s)
case (Var y) show ?thesis using Fun by (simp add: Var)
next
case (Fun g ss)
from Fun' have "f = g" and len: "length ss = length ts" by (simp add: Fun)+
from Fun' have "∀i<length ts. weak_match (ss ! i) (ts ! i)" by (simp add: len Fun)
with Fun' have "∀i. ∃σ. i < length ts ⟶ (ss ! i) = (ts ! i) ⋅ σ" by auto
from choice[OF this] obtain τ where substs: "∀i<length ts. ss ! i = (ts ! i) ⋅ τ i" by blast
from subst_merge[OF Fun'(2)[unfolded linear_term.simps, THEN conjunct1]]
obtain σ where vars: "∀i<length ts. ∀x∈vars_term (ts ! i). σ x = τ i x" ..
have "∀i<length ts. (ts ! i) ⋅ σ = (ts ! i) ⋅ τ i"
proof (intro allI impI)
fix i assume "i < length ts"
with vars have "∀x∈vars_term (ts ! i). σ x = τ i x" by simp
then show "(ts ! i) ⋅ σ = (ts ! i) ⋅ τ i" unfolding term_subst_eq_conv .
qed
with substs have "∀i<length ss. (ts ! i) ⋅ σ = ss ! i" by (simp add: len)
with map_nth_eq_conv[OF len[symmetric], of "λt. t ⋅ σ"]
have "map (λt. t ⋅ σ) ts = ss" by simp
then have "s = Fun f ts ⋅ σ" by (simp add: Fun ‹f = g›)
then show ?thesis by auto
qed
qed
lemma NF_terms_instance:
assumes "∀s⊲l ⋅ σ. s ∈ NF_terms Q"
shows "∀s⊲l. s ∈ NF_terms Q"
proof (intro allI impI)
fix s assume "l ⊳ s"
then have "l ⋅ σ ⊳ s ⋅ σ" by (rule supt_subst)
with assms have "s ⋅ σ ∈ NF_terms Q" by simp
from NF_instance[OF this] show "s ∈ NF_terms Q" .
qed
lemma NF_terms_ctxt:
assumes "∀s⊲C⟨l⟩. s ∈ NF_terms Q"
shows "∀s⊲l. s ∈ NF_terms Q"
proof (intro impI allI)
fix s assume "l ⊳ s"
from ctxt_imp_supteq[of C l] have "C⟨l⟩ ⊵ l" .
from this and ‹l ⊳ s› have "s ⊲ C⟨l⟩" by (rule supteq_supt_trans)
with assms show "s ∈ NF_terms Q" by simp
qed
lemma Q_subset_R_imp_same_NF:
assumes subset: "NF_trs R ⊆ NF_terms Q"
and no_lhs_var: "⋀ l r. nfs ⟹ (l,r) ∈ R ⟹ is_Fun l"
shows "NF_trs R = NF (qrstep nfs Q R)"
proof
show "NF_trs R ⊆ NF (qrstep nfs Q R)"
by (rule NF_anti_mono, auto)
next
show "NF (qrstep nfs Q R) ⊆ NF_trs R"
proof
fix t
assume NFt: "t ∈ NF (qrstep nfs Q R)"
show "t ∈ NF_trs R"
proof (rule ccontr)
assume "t ∉ NF_trs R"
then obtain s where "(t,s) ∈ rstep R" by auto
from rstep_imp_irstep[OF this no_lhs_var, of nfs] obtain s where step: "(t,s) ∈ qrstep nfs (lhss R) R" unfolding irstep_def by force
have "(t,s) ∈ qrstep nfs Q R"
by (rule set_mp[OF qrstep_mono step], insert subset, auto)
with NFt show False by auto
qed
qed
qed
lemma all_ctxt_closed_qrsteps[intro]: "all_ctxt_closed F ((qrstep nfs Q R)⇧*)"
by (rule trans_ctxt_imp_all_ctxt_closed[OF trans_rtrancl refl_rtrancl], blast)
lemma subst_qrsteps_imp_qrsteps: fixes σ :: "('f,'v)subst"
assumes "⋀ x. x ∈ vars_term t ⟹ (σ x,τ x) ∈ (qrstep nfs Q R)⇧*"
shows "(t ⋅ σ, t ⋅ τ) ∈ (qrstep nfs Q R)⇧*"
using all_ctxt_closed_subst_step[OF all_ctxt_closed_qrsteps, of t σ τ,
OF assms] .
lemma subst_qrsteps_imp_qrsteps_at_pos: fixes σ :: "('f,'v)subst"
assumes "p ∈ poss l"
and "⋀ x. x ∈ vars_term l ⟹ (σ x, τ x) ∈ (qrstep nfs Q R)⇧*"
shows "(l |_ p ⋅ σ, l |_ p ⋅ τ) ∈ (qrstep nfs Q R)⇧*"
proof -
{
fix y
assume a:"y ∈ vars_term (l |_ p)"
from supteq_trans[OF subt_at_imp_supteq[OF assms(1)] vars_term_supteq(1)[OF a]]
have "y ∈ vars_term l" using subteq_Var_imp_in_vars_term by fast
with assms have "(σ y, τ y) ∈ (qrstep nfs Q R)⇧*" by blast
}
then show ?thesis using subst_qrsteps_imp_qrsteps by blast
qed
lemma instance_weak_match:
"s = t ⋅ σ ⟹ weak_match s t"
by (induct s t rule: weak_match.induct) auto
text ‹For linear terms, matching and weak matching are the same.›
lemma linear_term_weak_match_instance_conv:
assumes "linear_term t"
shows "weak_match s t ⟷ (∃σ. s = t ⋅ σ)"
using linear_term_weak_match_match[OF assms] and instance_weak_match by blast
lemma qrsteps_rules_conv:
"((s,t) ∈ (qrstep nfs Q R)⇧*) = (∃ n ts lr. ts 0 = s ∧ ts n = t ∧ (∀i<n. (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i} ∧ lr i ∈ R))" (is "?L = ?R")
proof
assume ?L
from this[unfolded rtrancl_fun_conv] obtain n ts where first: "ts 0 = s" and last: "ts n = t" and steps: "⋀ i. i < n ⟹ (ts i, ts (Suc i)) ∈ qrstep nfs Q R" by auto
{
fix i
assume i: "i < n"
from steps[OF this, unfolded qrstep_rule_conv[where R = R]]
have "∃ lr. lr ∈ R ∧ (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr}" by auto
}
then have "∀i. ∃ lr. i < n ⟶ lr ∈ R ∧ (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr}" by auto
from choice[OF this] obtain lr where lr: "⋀ i. i < n ⟹ lr i ∈ R" and steps: "⋀ i. i < n ⟹ (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i}" by auto
show ?R using first last lr steps by blast
next
assume ?R
then obtain n ts lr where first: "ts 0 = s" and last: "ts n = t"
and steps: "∀i<n. (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i} ∧ lr i ∈ R"
by auto
from steps have steps: "∀i<n. (ts i, ts (Suc i)) ∈ qrstep nfs Q R"
unfolding qrstep_rule_conv[where R = R] by auto
show ?L unfolding rtrancl_fun_conv using first last steps by blast
qed
lemma qrsteps_rules_conv':
assumes left: "((s,t) ∈ (qrstep nfs Q R)⇧* O qrstep nfs Q R' O (qrstep nfs Q R)⇧*)"
shows "(∃ n ts lr i. ts 0 = s ∧ ts n = t ∧ (∀i<n. (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i} ∧ lr i ∈ R ∪ R') ∧ i < n ∧ lr i ∈ R')" (is "?Right")
proof -
let ?Q = "qrstep nfs Q"
let ?R = "?Q R"
let ?R' = "?Q R'"
show ?thesis
proof -
from left
obtain u v where su: "(s, u) ∈ ?R⇧*" and uv: "(u,v) ∈ ?R'" and vt: "(v,t) ∈ ?R⇧*" by auto
from su[unfolded qrsteps_rules_conv]
obtain lr ts n where first: "ts 0 = s" and last: "ts n = u" and steps: "⋀ i. i < n ⟹ (ts i, ts (Suc i)) ∈ ?Q {lr i}" and lr: "⋀ i. i < n ⟹ lr i ∈ R"
by blast
from vt[unfolded qrsteps_rules_conv]
obtain lr' ts' n' where first': "ts' 0 = v" and last': "ts' n' = t" and steps': "⋀ i. i < n' ⟹ (ts' i, ts' (Suc i)) ∈ ?Q {lr' i}" and lr': "⋀ i. i < n' ⟹ lr' i ∈ R"
by blast
from uv[unfolded qrstep_rule_conv[where R = R']] obtain lr'' where lr'': "lr'' ∈ R'" and uv: "(u,v) ∈ qrstep nfs Q {lr''}" by auto
let ?lr = "λ i. if i < n then lr i else if i = n then lr'' else lr' (i - Suc n)"
let ?ts = "λ i. if i ≤ n then ts i else ts' (i - Suc n)"
let ?n = "Suc (n + n')"
show ?Right
proof (intro exI conjI)
show "∀i < ?n. (?ts i, ?ts (Suc i)) ∈ ?Q {?lr i} ∧ ?lr i ∈ R ∪ R'"
proof (intro allI impI)
fix i
assume i: "i < ?n"
show "(?ts i, ?ts (Suc i)) ∈ ?Q {?lr i} ∧ ?lr i ∈ R ∪ R'"
proof (cases "i < n")
case True
with steps lr show ?thesis by simp
next
case False
show ?thesis
proof (cases "i = n")
case True
with uv lr'' first' last show ?thesis by simp
next
case False
with ‹¬ i < n› have "i > n" by auto
then have "i = Suc n + (i - Suc n)" by auto
then obtain k where i': "i = Suc n + k" by auto
with i have k: "k < n'" by auto
from steps'[OF k] lr'[OF k] show ?thesis unfolding i'
by simp
qed
qed
qed
next
show "?ts 0 = s" using first by auto
next
show "?ts ?n = t" using last' by auto
next
show "n < ?n" by auto
next
show "?lr n ∈ R'" using lr'' by auto
qed
qed
qed
lemma qrsteps_rules_conv'':
assumes first: "ts 0 = s"
and last: "ts n = t"
and steps: "⋀ i. i < n ⟹ (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i}"
and lr: "⋀ i. i < n ⟹ lr i ∈ R' ∪ R"
and i: "i < n"
and i': "lr i ∈ R'"
shows "(s, t) ∈ (qrstep nfs Q (R' ∪ R))⇧* O qrstep nfs Q R' O (qrstep nfs Q (R' ∪ R))⇧*"
proof -
let ?Q = "qrstep nfs Q"
let ?R = "?Q (R' ∪ R)"
let ?R' = "?Q R'"
have one: "(s,ts i) ∈ ?R⇧*"
unfolding qrsteps_rules_conv using first steps lr i
by (intro exI[of _ i] exI[of _ ts] exI[of _ lr], auto)
have two: "(ts i, ts (Suc i)) ∈ ?R'"
unfolding qrstep_rule_conv[where R = R'] using steps[OF i] i' by auto
from i have n: "n = (n - Suc i) + Suc i" by auto
then obtain k where n: "n = k + Suc i" by auto
have three: "(ts (Suc i), t) ∈ ?R⇧*"
unfolding qrsteps_rules_conv using insert last lr steps n
by (intro exI[of _ k] exI[of _ "shift ts (Suc i)"] exI[of _ "shift lr (Suc i)"], auto)
from one two three
show ?thesis by auto
qed
lemma normalize_subst_qrsteps_inn_partial:
fixes Q R R' σ nfs b
defines τ: "τ ≡ λ x. if b x then some_NF (qrstep nfs Q R') (σ x) else σ x"
assumes UNF: "UNF (qrstep nfs Q R')"
and R': "⋀ x u. x ∈ vars_term t ⟹ b x ⟹ (σ x,u) ∈ (qrstep nfs Q R)⇧* ⟹ (σ x,u) ∈ (qrstep nfs Q R')⇧*"
and steps: "(t ⋅ σ,s) ∈ (qrstep nfs Q R)⇧*"
and s: "s ∈ NF_terms Q"
and inn: "NF_terms Q ⊆ NF_trs R'"
shows "(∀x ∈ vars_term t. (σ x, τ x) ∈ (qrstep nfs Q R')⇧* ∧ (b x ⟶ τ x ∈ NF_terms Q)) ∧ (t ⋅ τ, s) ∈ (qrstep nfs Q R)⇧*"
using steps s R'
proof (induct t arbitrary: s)
case (Var x)
let ?QR = "qrstep nfs Q R"
let ?QR' = "qrstep nfs Q R'"
from Var(2) inn have sNF: "s ∈ NF_trs R'" by auto
with NF_anti_mono[OF qrstep_mono[OF subset_refl, of Q "{}" nfs R']]
have sNF': "s ∈ NF ?QR'" by auto
show ?case
proof (cases "b x")
case True
from Var(1) Var(3)[OF _ True] have steps: "(σ x, s) ∈ ?QR'⇧*" by auto
from some_NF_UNF[OF UNF steps sNF'] have s: "s = τ x" unfolding τ using True by auto
then show ?thesis using steps Var(2) by auto
next
case False
then show ?thesis using steps Var unfolding τ by auto
qed
next
case (Fun f ts)
let ?QR = "qrstep nfs Q R"
let ?QR' = "qrstep nfs Q R'"
let ?P = "λ ss i. (∀ x ∈ vars_term (ts ! i). (σ x, τ x) ∈ ?QR'⇧* ∧ (b x ⟶ τ x ∈ NF_terms Q)) ∧ (ts ! i ⋅ τ, ss ! i) ∈ ?QR⇧*"
{
fix ss
assume len: "length ss = length ts"
and steps: "⋀ i. i < length ts ⟹ (ts ! i ⋅ σ, ss ! i) ∈ ?QR⇧*"
and NF: "⋀ i. i < length ts ⟹ ss ! i ∈ NF_terms Q"
let ?p = "?P ss"
{
fix i
assume i: "i < length ts"
with len have mem: "ts ! i ∈ set ts" by auto
have "?p i"
by (rule Fun(1)[OF mem steps[OF i] NF[OF i] Fun(4)], insert mem, auto)
} note p = this
then have "∀ i < length ts. ?p i" by auto
} note main = this
{
fix s
assume steps: "(Fun f ts ⋅ σ, s) ∈ (nrqrstep nfs Q R)⇧*" and NF: "⋀ u. u ⊲ s ⟹ u ∈ NF_terms Q"
from nrqrsteps_preserve_root[OF steps]
obtain ss where s: "s = Fun f ss" and len: "length ss = length ts" by (cases s, auto)
note main = main[OF len]
{
fix i
assume i: "i < length ts"
from nrqrsteps_imp_arg_qrsteps[OF steps, of i] i len
have steps: "(ts ! i ⋅ σ, ss ! i) ∈ ?QR⇧*" unfolding s by auto
have NF: "ss ! i ∈ NF_terms Q"
by (rule NF, unfold s, insert i len, auto)
note steps NF
}
note main = main[OF this]
then have τ: "⋀ i. i < length ts ⟹ ?P ss i" by blast
have "(∀x∈vars_term (Fun f ts).
(σ x, τ x) ∈ ?QR'⇧* ∧ (b x ⟶ τ x ∈ NF_terms Q)) ∧
(Fun f ts ⋅ τ, s) ∈ ?QR⇧*"
proof (intro conjI, intro ballI)
fix x
assume "x ∈ vars_term (Fun f ts)"
then obtain i where i: "i < length ts" and x: "x ∈ vars_term (ts ! i)"
by (auto simp: set_conv_nth)
with τ show "(σ x, τ x) ∈ ?QR'⇧* ∧ (b x ⟶ τ x ∈ NF_terms Q)" by auto
next
from len have len: "length (map (λ t. t ⋅ τ) ts) = length ss" by simp
show "(Fun f ts ⋅ τ, s) ∈ ?QR⇧*" unfolding s
using τ[THEN conjunct2]
using args_qrsteps_imp_qrsteps[OF len, of nfs Q R f] by auto
qed
} note main = this
from firstStep[OF qrstep_iff_rqrstep_or_nrqrstep Fun(2)]
show ?case
proof
assume steps: "(Fun f ts ⋅ σ, s) ∈ (nrqrstep nfs Q R)⇧*"
show ?thesis
proof (rule main[OF steps])
fix u
assume sub: "s ⊳ u"
then have "s ⊵ u" by auto
show "u ∈ NF_terms Q"
by (rule NF_subterm[OF Fun(3)], insert sub, auto)
qed
next
assume steps: "(Fun f ts ⋅ σ, s) ∈ (nrqrstep nfs Q R)⇧* O rqrstep nfs Q R O ?QR⇧*"
then obtain u v where one: "(Fun f ts ⋅ σ, u) ∈ (nrqrstep nfs Q R)⇧*"
and two: "(u,v) ∈ rqrstep nfs Q R"
and three: "(v,s) ∈ ?QR⇧*" by auto
{
fix u'
assume "u ⊳ u'"
then have "u' ∈ NF_terms Q" using two[unfolded rqrstep_def] by auto
}
from main[OF one this]
have first: "∀ x ∈ vars_term (Fun f ts). (σ x, τ x) ∈ ?QR'⇧* ∧ (b x ⟶ τ x ∈ NF_terms Q)"
and steps: "(Fun f ts ⋅ τ, u) ∈ ?QR⇧*" by blast+
from two have "(u,v) ∈ ?QR" unfolding qrstep_iff_rqrstep_or_nrqrstep by auto
with three have steps2: "(u,s) ∈ ?QR⇧*" by auto
show ?thesis
by (intro conjI, rule first, insert steps steps2, auto)
qed
qed
lemma normalize_subst_qrsteps_inn:
fixes Q R R' σ nfs
defines τ: "τ ≡ λ x. some_NF (qrstep nfs Q R') (σ x)"
assumes UNF: "UNF (qrstep nfs Q R')"
and R': "⋀ x u. x ∈ vars_term t ⟹ (σ x,u) ∈ (qrstep nfs Q R)⇧* ⟹ (σ x,u) ∈ (qrstep nfs Q R')⇧*"
and steps: "(t ⋅ σ,s) ∈ (qrstep nfs Q R)⇧*"
and s: "s ∈ NF_terms Q"
and inn: "NF_terms Q ⊆ NF_trs R'"
shows "(∀x ∈ vars_term t. (σ x, τ x) ∈ (qrstep nfs Q R')⇧* ∧ τ x ∈ NF_terms Q) ∧ (t ⋅ τ, s) ∈ (qrstep nfs Q R)⇧*"
using normalize_subst_qrsteps_inn_partial[OF UNF R' steps s inn, of "λ _. True", unfolded if_True]
unfolding τ by blast
lemma Tinf_imp_SN_nr_first_root_step_rel:
assumes Tinf: "t ∈ Tinf (relto (qrstep nfs Q R) (qrstep nfs Q' S))"
shows "SN_on (relto (nrqrstep nfs Q R) (nrqrstep nfs Q' S)) {t} ∧ (∃ s u. (t,s) ∈ (nrqrstep nfs Q R ∪ nrqrstep nfs Q' S)⇧* ∧ (s,u) ∈ rqrstep nfs Q R ∪ rqrstep nfs Q' S ∧ ¬ SN_on (relto (qrstep nfs Q R) (qrstep nfs Q' S)) {u})"
proof -
let ?R = "qrstep nfs Q R"
let ?S = "qrstep nfs Q' S"
let ?rel = "relto ?R ?S"
let ?nR = "nrqrstep nfs Q R"
let ?nS = "nrqrstep nfs Q' S"
let ?nrel = "relto ?nR ?nS"
let ?rR = "rqrstep nfs Q R"
let ?rS = "rqrstep nfs Q' S"
let ?N = "?nR ∪ ?nS"
let ?RO = "?rR ∪ ?rS"
from Tinf[unfolded Tinf_def] have notSN: "¬ SN_on ?rel {t}" and min: "⋀ s. s ⊲ t ⟹ SN_on ?rel {s}" by auto
from this[unfolded SN_rel_on_def[symmetric] SN_rel_on_conv]
have nSN: "¬ SN_rel_on_alt ?R ?S {t}" and min2: "⋀ s. s ⊲ t ⟹ SN_rel_on_alt ?R ?S {s}" by auto
from nSN[unfolded SN_rel_on_alt_def] obtain ts where start: "ts 0 = t" and steps: "⋀ i. (ts i, ts (Suc i)) ∈ ?R ∪ ?S" and inf: "INFM i. (ts i, ts (Suc i)) ∈ ?R" by auto
show ?thesis
proof (cases "SN_on ?nrel {t}")
case True
from True[unfolded SN_rel_on_def[symmetric] SN_rel_on_conv]
have "SN_rel_on_alt ?nR ?nS {ts 0}" unfolding start .
note SN = this[unfolded SN_rel_on_alt_def, rule_format, of ts]
let ?P = "λ i. (ts i, ts (Suc i)) ∈ ?RO"
have "∃ i. ?P i"
proof (rule ccontr)
assume nthesis: "¬ ?thesis"
then have "⋀ i. (ts i, ts (Suc i)) ∈ ?N" using steps[unfolded qrstep_iff_rqrstep_or_nrqrstep] by auto
with SN have "¬ (INFM i. (ts i, ts (Suc i)) ∈ ?nR)" by auto
then show False
proof (elim notE, unfold INFM_nat_le, intro allI)
fix m
from inf[unfolded INFM_nat_le] obtain n where n: "n ≥ m" and step: "(ts n, ts (Suc n)) ∈ ?R" by auto
from step nthesis have "(ts n, ts (Suc n)) ∈ ?nR" unfolding qrstep_iff_rqrstep_or_nrqrstep by auto
then show "∃ n ≥ m. (ts n, ts (Suc n)) ∈ ?nR" using n by auto
qed
qed
then obtain i where step: "?P i" by auto
from LeastI[of ?P, OF step] have step: "?P (LEAST i. ?P i)" .
obtain i where i: "i = (LEAST i. ?P i)" by auto
from step have step: "?P i" unfolding i .
{
fix j
assume "j < i"
from not_less_Least[OF this[unfolded i]] have "¬ ?P j" .
with steps[of j] have "(ts j, ts (Suc j)) ∈ ?N"
unfolding qrstep_iff_rqrstep_or_nrqrstep by auto
} note nsteps = this
show ?thesis
proof -
have "(ts 0, ts i) ∈ ?N⇧*" unfolding rtrancl_fun_conv
by (rule exI[of _ ts], rule exI[of _ i], insert nsteps, auto)
moreover
let ?ss = "shift ts (Suc i)"
have "¬ SN_on (relto ?R ?S) {ts (Suc i)}"
unfolding SN_rel_on_def[symmetric]
unfolding SN_rel_on_conv SN_rel_on_alt_def
unfolding not_all not_imp not_not
proof (rule exI[of _ ?ss], intro conjI allI)
fix j
show "(?ss j, ?ss (Suc j)) ∈ ?R ∪ ?S" using steps[of "j + Suc i"] by auto
next
show "?ss 0 ∈ {ts (Suc i)}" by simp
next
show "INFM j. (?ss j, ?ss (Suc j)) ∈ ?R"
unfolding INFM_nat_le
proof (rule allI)
fix m
from inf[unfolded INFM_nat_le, rule_format, of "m + Suc i"]
obtain n where n: "n ≥ m + Suc i" and step: "(ts n, ts (Suc n)) ∈ ?R" by auto
show "∃ n ≥ m. (?ss n, ?ss (Suc n)) ∈ ?R"
by (rule exI[of _ "n - Suc i"], insert n step, auto)
qed
qed
ultimately show ?thesis
using True step start by blast
qed
next
case False
from this[unfolded SN_rel_on_def[symmetric] SN_rel_on_conv]
have nSN: "¬ SN_rel_on_alt ?nR ?nS {t}" .
from nSN[unfolded SN_rel_on_alt_def] obtain ts where start: "ts 0 = t" and nsteps: "⋀ i. (ts i, ts (Suc i)) ∈ ?N" and inf: "INFM i. (ts i, ts (Suc i)) ∈ ?nR" by auto
obtain f ss where init: "ts 0 = Fun f ss"
using nrqrstep_imp_arg_qrstep[of "ts 0" "ts (Suc 0)"] nsteps[of 0]
by (cases "ts 0", auto)
let ?n = "length ss"
obtain n where n: "n = ?n" by auto
{
fix i
have "∃ ssi. ts i = Fun f ssi ∧ length ssi = n"
proof (induct i)
case 0
then show ?case unfolding init n by auto
next
case (Suc i)
from Suc obtain ssi where tsi: "ts i = Fun f ssi" and n: "length ssi = n" by auto
from nrqrstep_preserves_root[of "ts i" "ts (Suc i)"] nsteps[of i]
have "root (ts (Suc i)) = root (ts i)" by auto
then show ?case unfolding tsi root.simps n by (cases "ts (Suc i)", auto)
qed
}
from choice[OF allI[OF this]] obtain sss where ts: "⋀ i. ts i = Fun f (sss i)" and len: "⋀ i. length (sss i) = n" by force
let ?strict = "λ i. ∃ j < n. (sss i ! j, sss (Suc i) ! j) ∈ ?R"
have inf: "INFM i. ?strict i"
unfolding INFM_nat_le
proof (intro allI)
fix i
from inf[unfolded INFM_nat_le, rule_format, of i] obtain k where
k: "k ≥ i" and step: "(ts k, ts (Suc k)) ∈ ?nR" by auto
show "∃ k ≥ i. ?strict k"
by (rule exI, rule conjI[OF k],
insert nrqrstep_imp_arg_qrstep[OF step] ts len, auto)
qed
let ?idx = "λ i. if ?strict i then (SOME j. j < n ∧ (sss i ! j, sss (Suc i) ! j) ∈ ?R)
else 0"
obtain idx where idx: "idx = ?idx" by auto
{
fix i
assume stri: "?strict i"
then have idxi: "idx i = (SOME j. j < n ∧ (sss i ! j, sss (Suc i) ! j) ∈ ?R)" unfolding idx by simp
from someI_ex[OF stri] have "idx i < n ∧ (sss i ! idx i, sss (Suc i) ! idx i) ∈ ?R" unfolding idxi .
} note idx_strict = this
{
fix i
have "idx i ≤ n" using idx_strict[of i] by (cases "?strict i", auto simp: idx)
} note idx_n = this
{
fix X
have "finite (idx ` X)"
proof (rule finite_subset)
show "idx ` X ⊆ { i . i ≤ n}" using idx_n by auto
next
have id: "{i. i ≤ n} = set [0 ..< Suc n]" by auto
show "finite {i. i ≤ n}" unfolding id by (rule finite_set)
qed
} note fin = this
note pigeon = pigeonhole_infinite[OF inf[unfolded INFM_iff_infinite] fin]
then obtain j where "infinite { i ∈ {i. ?strict i}. idx i = j}" by auto
then have inf: "INFM i. ?strict i ∧ idx i = j" unfolding INFM_iff_infinite by simp
note inf = inf[unfolded INFM_nat_le, rule_format]
{
from inf[of 0] obtain k where stri: "?strict k" and idx: "idx k = j" by auto
from idx_strict[OF stri] idx have "j < n" by auto
} note jn = this
with n have "ss ! j ∈ set ss" by auto
with init have "ss ! j ⊲ ts 0" by auto
from min[unfolded start[symmetric], OF this] have SN: "SN_on ?rel {ss ! j}" by auto
let ?ss = "λ i. sss i ! j"
let ?RS = "?R ∪ ?S"
from SN have SN: "SN_on ?rel {?ss 0}" using ts[of 0] init by simp
{
fix i
have "(?ss i, ?ss (Suc i)) ∈ ?RS^="
proof (cases "(ts i, ts (Suc i)) ∈ ?nS")
case True
from nrqrstep_imp_arg_qrsteps[OF True, of j]
show ?thesis unfolding ts by simp
next
case False
with nsteps[of i]
have "(ts i, ts (Suc i)) ∈ ?nR" by auto
from nrqrstep_imp_arg_qrsteps[OF this, of j]
show ?thesis unfolding ts by auto
qed
} note j_steps = this
let ?Rel = "?RS⇧* O ?R O ?RS⇧*"
{
fix i
have "(?ss i, ?ss (Suc i)) ∈ ?RS⇧* ∪ ?Rel"
by (rule set_mp[OF _ j_steps[of i]], regexp)
} note jsteps = this
from SN_on_trancl[OF SN, unfolded relto_trancl_conv]
have SN: "SN_on ?Rel {?ss 0}" .
have compat: "?RS⇧* O ?Rel ⊆ ?Rel" by regexp
from non_strict_ending[of ?ss "?RS⇧*" ?Rel, OF allI[OF jsteps] compat SN]
obtain k where k: "⋀ l. l ≥ k ⟹ (?ss l, ?ss (Suc l)) ∉ ?Rel" by auto
from inf[of k] obtain l where lk: "l ≥ k" and strict: "?strict l" and lj: "idx l = j" by auto
from k[OF lk] have no_step: "(?ss l, ?ss (Suc l)) ∉ ?R" by auto
with idx_strict[OF strict] lj have False by auto
then show ?thesis by auto
qed
qed
lemma nrqrstep_empty[simp]: "nrqrstep nfs Q {} = {}" unfolding nrqrstep_def by auto
lemma Tinf_imp_SN_nr_first_root_step:
assumes Tinf: "t ∈ Tinf (qrstep nfs Q R)"
shows "SN_on (nrqrstep nfs Q R) {t} ∧ (∃ s u. (t,s) ∈ (nrqrstep nfs Q R)⇧* ∧ (s,u) ∈ rqrstep nfs Q R ∧ ¬ SN_on (qrstep nfs Q R) {u})"
using Tinf_imp_SN_nr_first_root_step_rel[of t nfs Q "{}" Q R]
using Tinf by auto
lemma SN_on_subterms_imp_SN_on_nrqrstep:
fixes R :: "('f, 'v) trs"
assumes "∀s⊲t. SN_on (qrstep nfs Q R) {s}"
shows "SN_on (nrqrstep nfs Q R) {t}"
proof (cases "SN_on (qrstep nfs Q R) {t}")
case True
then show ?thesis unfolding qrstep_iff_rqrstep_or_nrqrstep unfolding SN_defs by auto
next
case False
with assms have "t ∈ Tinf (qrstep nfs Q R)" unfolding Tinf_def by auto
from Tinf_imp_SN_nr_first_root_step[OF this]
show ?thesis by simp
qed
lemma SN_args_imp_SN_rel:
assumes SN: "⋀s. s ∈ set ss ⟹ SN_on (relto (qrstep nfs Q R) (qrstep nfs Q S)) {s}"
and nvar: "∀(l, r)∈R ∪ S. is_Fun l"
and ndef: "¬ defined (applicable_rules Q (R ∪ S)) (f,length ss)"
shows "SN_on (relto (qrstep nfs Q R) (qrstep nfs Q S)) {Fun f ss}"
proof (rule ccontr)
assume nSN: "¬ ?thesis"
let ?RS = "relto (qrstep nfs Q R) (qrstep nfs Q S)"
have "Fun f ss ∈ Tinf ?RS" unfolding Tinf_def
proof (intro CollectI conjI nSN allI impI)
fix s
assume "Fun f ss ⊳ s"
then obtain si where si: "si ∈ set ss" and supteq: "si ⊵ s" by auto
from ctxt_closed_SN_on_subt[OF ctxt.closed_relto[OF ctxt_closed_qrstep ctxt_closed_qrstep] SN[OF si] supteq]
show "SN_on ?RS {s}" .
qed
from Tinf_imp_SN_nr_first_root_step_rel[OF this]
obtain s u where steps: "(Fun f ss, s) ∈ (nrqrstep nfs Q (R ∪ S))⇧*" and su: "(s,u) ∈ rqrstep nfs Q (R ∪ S)"
unfolding nrqrstep_union rqrstep_union by auto
from nrqrsteps_preserve_root[OF steps] obtain ts where
s: "s = Fun f ts" and
len: "length ss = length ts" by (cases s, auto)
note ndef = ndef[unfolded len]
note su = su[unfolded s]
from rqrstepE[OF su] obtain l r σ where lr: "(l,r) ∈ (R ∪ S)" and id: "Fun f ts = l ⋅ σ"
and NF: "∀ u ⊲ l ⋅ σ. u ∈ NF_terms Q" .
from only_applicable_rules[OF NF] have app: "applicable_rule Q (l,r)" .
from nvar lr id obtain ls where l: "l = Fun f ls" and len: "length ts = length ls" by (cases l; force)
note ndef = ndef[unfolded len]
from app lr ndef show False unfolding l unfolding applicable_rules_def defined_def by force
qed
lemma SN_args_imp_SN:
assumes "⋀s. s ∈ set ss ⟹ SN_on (qrstep nfs Q R) {s}"
and "∀(l, r)∈R. is_Fun l"
and "¬ defined (applicable_rules Q R) (f,length ss)"
shows "SN_on (qrstep nfs Q R) {Fun f ss}"
using SN_args_imp_SN_rel[of ss nfs Q "{}" R f] assms by auto
lemma SN_args_imp_SN_rel_rstep:
assumes "⋀s. s ∈ set ss ⟹ SN_on (relto (rstep R) (rstep S)) {s}"
and "∀(l, r)∈R ∪ S. is_Fun l"
and "¬ defined (R ∪ S) (f,length ss)"
shows "SN_on (relto (rstep R) (rstep S)) {Fun f ss}"
using SN_args_imp_SN_rel[of ss False "{}" S R f] assms by auto
lemma SN_args_imp_SN_rstep :
assumes SN: "⋀s. s ∈ set ss ⟹ SN_on (rstep R) {s}"
and nvar: "∀(l, r)∈R. is_Fun l"
and ndef: "¬ defined R (f, length ss)"
shows "SN_on (rstep R) {Fun f ss}"
using SN_args_imp_SN[of ss False "{}" _ f, OF _ nvar] SN ndef by auto
lemma normalize_subst_qrsteps_inn_infinite:
fixes Q R R' σ nfs
defines τ: "τ ≡ λ x. some_NF (qrstep nfs Q R') (σ x)"
assumes UNF: "UNF (qrstep nfs Q R')"
and R': "⋀ x u. x ∈ vars_term t ⟹ (σ x,u) ∈ (qrstep nfs Q R)⇧* ⟹ (σ x,u) ∈ (qrstep nfs Q R')⇧*"
and steps: "¬ SN_on (qrstep nfs Q R) {t ⋅ σ}"
and SN: "⋀ x. x ∈ vars_term t ⟹ SN_on (qrstep nfs Q R) {σ x}"
and inn: "NF_terms Q ⊆ NF_trs R'"
shows "¬ SN_on (qrstep nfs Q R) {t ⋅ τ}"
proof -
let ?R = "qrstep nfs Q R"
let ?R' = "qrstep nfs Q R'"
from not_SN_imp_subt_Tinf[OF steps] obtain s
where subt: "t ⋅ σ ⊵ s" and s_inf: "s ∈ Tinf ?R" by auto
from supteq_imp_subt_at[OF subt] obtain p where p: "p ∈ poss (t ⋅ σ)"
and subt: "s = t ⋅ σ |_ p" by auto
show ?thesis
proof (cases "p ∈ poss t ∧ is_Fun (t |_ p)")
case True
obtain tp where tp: "tp = t |_ p" by auto
with True have p: "p ∈ poss t" and is_fun: "is_Fun tp" by auto
then have s: "s = tp ⋅ σ" by (simp add: subt tp)
from subt_at_imp_supteq[OF p] have subt: "t ⊵ tp" unfolding tp .
from s_inf[unfolded s] have tp_inf: "tp ⋅ σ ∈ Tinf ?R" .
{
fix x
assume "x ∈ vars_term tp"
then have "x ∈ vars_term t" using supteq_imp_vars_term_subset [OF subt] by auto
} note vars = this
let ?n = "nrqrstep nfs Q R"
let ?r = "rqrstep nfs Q R"
from tp_inf[unfolded Tinf_def] have SN: "∀ s ⊲ tp ⋅ σ. SN_on ?R {s}"
and nSN: "¬ SN_on ?R {tp ⋅ σ}" by auto
from SN_on_subterms_imp_SN_on_nrqrstep[OF SN] have SN: "SN_on ?n {tp ⋅ σ}"
by auto
from nSN obtain f where start: "f 0 = tp ⋅ σ"
and steps: "∀ i. (f i, f (Suc i)) ∈ ?R" by auto
from chain_Un_SN_on_imp_first_step[OF steps[unfolded qrstep_iff_rqrstep_or_nrqrstep], OF SN[unfolded start[symmetric]]]
obtain i where root: "(f i, f (Suc i)) ∈ ?r" and nroot: "⋀ j. j < i ⟹ (f j, f (Suc j)) ∈ ?n" by auto
have nroot: "(tp ⋅ σ, f i) ∈ ?n⇧*" unfolding rtrancl_fun_conv
by (intro exI[of _ f] exI[of _ i], unfold start, insert nroot, auto)
from is_fun obtain g ts where is_fun: "tp = Fun g ts" by (cases tp, auto)
note nroot = nroot[unfolded is_fun]
from nrqrsteps_preserve_root[OF nroot] obtain ss where fi: "f i = Fun g ss" and len: "length ss = length ts" by (cases "f i", auto)
note root = root[unfolded fi]
from root[unfolded rqrstep_def] have NF: "⋀ u. u ⊲ Fun g ss ⟹ u ∈ NF_terms Q" by auto
let ?ts = "map (λ t. t ⋅ τ) ts"
let ?lts = "length ?ts"
{
fix i
assume i: "i < ?lts"
from nrqrsteps_imp_arg_qrsteps[OF nroot, of i] i len
have steps: "(ts ! i ⋅ σ, ss ! i) ∈ ?R⇧*" unfolding fi by auto
have NF: "ss ! i ∈ NF_terms Q"
by (rule NF, insert i len, auto)
{
fix x
assume "x ∈ vars_term (ts ! i)"
with i have "x ∈ vars_term (Fun g ts)" by auto
with vars have "x ∈ vars_term t" unfolding is_fun by auto
} note vars = this
from normalize_subst_qrsteps_inn[OF UNF R'[OF vars] steps NF inn]
have "(ts ! i ⋅ τ, ss ! i) ∈ ?R⇧*" unfolding τ ..
then have "(?ts ! i, ss ! i) ∈ ?R⇧*" using i by auto
} note τsteps = this
from len have len: "?lts = length ss" by simp
from args_qrsteps_imp_qrsteps[OF len, of nfs Q R g] τsteps
have tpfi: "(tp ⋅ τ, f i) ∈ ?R⇧*" unfolding is_fun fi by simp
obtain g where g: "g ≡ λ j. f (i + j)" by auto
from steps have "⋀ i. (g i, g (Suc i)) ∈ ?R" unfolding g by auto
then have "¬ SN_on ?R {g 0}" by auto
then have nSN: "¬ SN_on ?R {f i}" unfolding g by auto
with steps_preserve_SN_on[OF tpfi]
have "¬ SN_on ?R {tp ⋅ τ}" by auto
with ctxt_closed_SN_on_subt[OF ctxt_closed_qrstep _ supteq_subst[OF subt], of nfs Q R τ]
show ?thesis by auto
next
case False
from pos_into_subst[OF refl p False]
obtain q q' x where pq: "p = q @ q'" and q: "q ∈ poss t" and t: "t |_ q = Var x" by auto
from subteq_Var_imp_in_vars_term [OF subt_at_imp_supteq [OF q, unfolded t]]
have x: "x ∈ vars_term t" .
have "s = σ x |_ q' ∧ q' ∈ poss (σ x)"
using p
unfolding poss_append_poss subt pq
and subt_at_append [OF poss_imp_subst_poss [OF q]]
and subt_at_subst [OF q] t by simp
then have s: "σ x ⊵ s" using subt_at_imp_supteq by auto
from ctxt_closed_SN_on_subt[OF ctxt_closed_qrstep SN[OF x] s]
have "SN_on ?R {s}" by auto
with s_inf[unfolded Tinf_def] show ?thesis by auto
qed
qed
lemma qrstep_r_p_s_conv:
fixes s t
assumes step: "(s, t) ∈ qrstep_r_p_s nfs Q R lr p σ"
defines [simp]: "C ≡ ctxt_of_pos_term p s"
shows "p ∈ poss s" and "p ∈ poss t" and "s = C⟨fst lr ⋅ σ⟩" and "t = C⟨snd lr ⋅ σ⟩" and "NF_subst nfs lr σ Q" and "ctxt_of_pos_term p t = C"
proof -
from step have p_in_s: "p ∈ poss s" unfolding qrstep_r_p_s_def by simp
have p_in_t: "p ∈ poss t" using qrstep_r_p_s_imp_poss[OF step] by simp
have C: "C = ctxt_of_pos_term p t" using ctxt_of_pos_term_qrstep_below[OF step] by simp
from p_in_s show "p ∈ poss s".
show "p ∈ poss t" using qrstep_r_p_s_imp_poss[OF step] by simp
from step show "s = C⟨fst lr ⋅ σ⟩" unfolding qrstep_r_p_s_def using ctxt_supt_id[OF p_in_s] by simp
from C show "t = C⟨snd lr ⋅ σ⟩" using step unfolding qrstep_r_p_s_def using ctxt_supt_id[OF p_in_t] by simp
from step show "NF_subst nfs lr σ Q" unfolding qrstep_r_p_s_def by simp
from C show "ctxt_of_pos_term p t = C" by simp
qed
lemma qrstep_r_p_s_redex_reduct:
assumes step: "(s,t) ∈ qrstep_r_p_s nfs Q R lr p σ"
shows "t|_p = snd lr ⋅ σ"
using qrstep_r_p_s_conv[OF step]
by (metis replace_at_subt_at)
lemma qrstep_r_p_s_imp_nrqrstep:
assumes step: "(s, t) ∈ qrstep_r_p_s nfs Q R lr p σ" and ne: "p ≠ []"
shows "(s, t) ∈ nrqrstep nfs Q R"
proof -
from step[unfolded qrstep_r_p_s_def]
have NF: "∀ u ⊲ fst lr ⋅ σ. u ∈ NF_terms Q"
and p: "p ∈ poss s"
and lr: "lr ∈ R"
and s: "s |_ p = fst lr ⋅ σ"
and t: "t = replace_at s p (snd lr ⋅ σ)"
and nfs: "NF_subst nfs lr σ Q" by auto
show ?thesis
proof (rule nrqrstepI[OF NF _ _ _ t])
show "(fst lr, snd lr) ∈ R" using lr by simp
next
from ne obtain i q where ne: "p = (i # q)" by (cases p, auto)
with p show "ctxt_of_pos_term p s ≠ □" by (cases s, auto)
qed (insert ctxt_supt_id[OF p, unfolded s] nfs, auto)
qed
lemma qrsteps_imp_qrsteps_r_p_s:
assumes "(s, t) ∈ (qrstep nfs Q R)⇧*"
shows "∃ n ts lr p σ. ts 0 = s ∧ ts n = t ∧ (∀ i < n. (ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) (p i) (σ i))"
proof -
from assms[unfolded qrsteps_rules_conv]
obtain n ts lr where
first: "ts 0 = s"
and last: "ts n = t"
and steps: "∀ i < n. (ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i} ∧ lr i ∈ R" by auto
let ?ts = "λ i. (ts i, ts (Suc i))"
{
fix i
assume "i < n"
from steps[rule_format, OF this]
have "?ts i ∈ qrstep nfs Q (R ∩ {lr i})" by auto
from this[unfolded qrstep_qrstep_r_p_s_conv] obtain lr' p σ where "?ts i ∈ qrstep_r_p_s nfs Q (R ∩ {lr i}) lr' p σ" by auto
then have "∃ p σ. ?ts i ∈ qrstep_r_p_s nfs Q R (lr i) p σ" unfolding qrstep_r_p_s_def by auto
}
then have "∀ i. ∃ p σ. i < n ⟶ ?ts i ∈ qrstep_r_p_s nfs Q R (lr i) p σ" by simp
from choice[OF this] obtain p where "∀ i. ∃ σ. i < n ⟶ ?ts i ∈ qrstep_r_p_s nfs Q R (lr i) (p i) σ" by auto
from choice[OF this] obtain σ where steps: "⋀ i. i < n ⟹ ?ts i ∈ qrstep_r_p_s nfs Q R (lr i) (p i) (σ i)" by auto
show ?thesis
proof (intro exI conjI)
show "∀ i < n. ?ts i ∈ qrstep_r_p_s nfs Q R (lr i) (p i) (σ i)" using steps by simp
qed (insert first last, auto)
qed
lemma qrsteps_r_p_s_imp_qrsteps:
assumes first: "ts 0 = s"
and last: "ts n = t"
and steps: "⋀ i. i < n ⟹ (ts i, ts (Suc i)) ∈ qrstep_r_p_s nfs Q R (lr i) (p i) (σ i)"
shows "(s, t) ∈ (qrstep nfs Q R)⇧*"
unfolding qrsteps_rules_conv
proof (intro exI[of _ n] exI[of _ ts] exI[of _ lr] conjI first last allI, intro allI impI)
fix i
assume i: "i < n"
show "(ts i, ts (Suc i)) ∈ qrstep nfs Q {lr i} ∧ lr i ∈ R" using steps[OF i] unfolding qrstep_qrstep_r_p_s_conv
unfolding qrstep_r_p_s_def by blast
qed
lemma qrstep_r_p_s_imp_applicable_rule: "(s,t) ∈ qrstep_r_p_s nfs Q R lr p σ ⟹ applicable_rule Q lr"
using only_applicable_rules[of "fst lr" σ Q]
unfolding qrstep_r_p_s_def
by (cases lr, simp)
lemma SN_on_qrstep_r_p_s_imp_wf_rule:
assumes SN: "SN_on (qrstep nfs Q R) {t}"
and step: "(t, s) ∈ qrstep_r_p_s nfs Q R lr p σ"
and nfs: "¬ nfs"
shows "vars_term (snd lr) ⊆ vars_term (fst lr) ∧ is_Fun (fst lr)"
proof -
obtain l r where lr: "lr = (l,r)" by force
from qrstep_r_p_s_imp_applicable_rule[OF step] have u: "applicable_rule Q lr" .
from step[unfolded lr qrstep_r_p_s_def] have p: "p ∈ poss t" and t: "t |_ p = l ⋅ σ" and mem: "(l,r) ∈ R" and NF: "∀ u ⊲ l ⋅ σ. u ∈ NF_terms Q" by auto
from SN_on_imp_wwf_rule[OF SN ctxt_supt_id[OF p, unfolded t, symmetric] mem NF nfs]
have "wwf_rule Q (l,r)" .
then show ?thesis using u unfolding lr wwf_rule_def by auto
qed
lemma SN_on_Var_gen:
assumes "Ball (fst ` R) is_Fun" shows "SN_on (qrstep nfs Q R) {Var x}" (is "SN_on _ {?x}")
proof -
let ?qr = "qrstep nfs Q R"
show "SN_on ?qr {?x}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain A where "A 0 = ?x" and rsteps: "chain ?qr A"
unfolding SN_on_def by best
then have "(?x,A 1) ∈ ?qr" using spec[OF rsteps, of 0] by auto
then obtain l r C σ where "(l,r) ∈ R" and x: "Var x = C⟨l ⋅ σ⟩" by auto
with assms obtain f ls where "l = Fun f ls" by force
with x obtain ls where "Var x = C⟨Fun f ls⟩" by auto
then show False by (cases C, auto)
qed
qed
lemma SN_on_Var:
assumes "wwf_qtrs Q R" shows "SN_on (qrstep nfs Q R) {Var x}" (is "SN_on _ {?x}")
by (rule SN_on_Var_gen, insert wwf_qtrs_imp_left_fun[OF assms], force)
lemma wwf_qtrs_imp_nfs_switch_r_p_s: assumes wwf: "wwf_qtrs Q R"
shows "qrstep_r_p_s nfs Q R = qrstep_r_p_s nfs' Q R"
proof -
{
fix nfs nfs' lr p σ s t
assume step: "(s,t) ∈ qrstep_r_p_s nfs Q R lr p σ"
obtain l r where lr: "lr = (l,r)" by force
from step[unfolded qrstep_r_p_s_def lr] have *: "(∀u⊲l ⋅ σ. u ∈ NF_terms Q)"
"p ∈ poss s" "(l,r) ∈ R" "s |_ p = l ⋅ σ" "t = (ctxt_of_pos_term p s)⟨r ⋅ σ⟩" and NF: "NF_subst nfs (l,r) σ Q" by auto
have "applicable_rule Q (l,r)" using only_applicable_rules * by auto
with wwf[unfolded wwf_qtrs_def] * have l: "is_Fun l" and rl: "vars_term r ⊆ vars_term l" by auto
have NF: "NF_subst nfs' (l,r) σ Q"
unfolding NF_subst_def
proof (intro impI subsetI)
fix u
assume u: "u ∈ σ ` vars_rule (l,r)"
then obtain x where u: "u = σ x" and x: "x ∈ vars_rule (l,r)" by auto
from x rl have x: "x ∈ vars_term l" by (cases "x ∈ vars_term l", auto simp: vars_rule_def)
then have "Var x ⊴ l" by auto
with l have "Var x ⊲ l" by auto
from supt_subst[OF this, of σ] *
show "u ∈ NF_terms Q" unfolding u by auto
qed
with * have "(s,t) ∈ qrstep_r_p_s nfs' Q R lr p σ" unfolding lr qrstep_r_p_s_def by auto
} note main = this
from main[of _ _ nfs _ _ _ nfs'] main[of _ _ nfs' _ _ _ nfs] show ?thesis
by (intro ext, auto)
qed
lemma wwf_qtrs_imp_nfs_switch: assumes wwf: "wwf_qtrs Q R"
shows "qrstep nfs Q R = qrstep nfs' Q R"
using
qrstep_qrstep_r_p_s_conv[of _ _ nfs Q R]
qrstep_qrstep_r_p_s_conv[of _ _ nfs' Q R]
wwf_qtrs_imp_nfs_switch_r_p_s[OF wwf, of nfs nfs'] by auto
lemma wwf_qtrs_imp_nfs_False_switch: assumes "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q R"
shows "qrstep nfs Q R = qrstep False Q R"
proof (cases "nfs ∧ Q ≠ {}")
case True
from wwf_qtrs_imp_nfs_switch[OF assms] True show ?thesis by auto
next
case False
show ?thesis
proof (cases nfs)
case True
with False have "Q = {}" by auto
then show ?thesis by simp
qed simp
qed
lemma rqrstep_rename_vars: assumes R: "⋀ st. st ∈ R ⟹ ∃ st'. st' ∈ R' ∧ st =⇩v st'"
shows "rqrstep nfs Q R ⊆ rqrstep nfs Q R'"
proof
fix x y
assume "(x,y) ∈ rqrstep nfs Q R"
from rqrstepE[OF this]
obtain l r σ where NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q" and x: "x = l ⋅ σ" and y: "y = r ⋅ σ" and lr: "(l,r) ∈ R"
and nfs: "NF_subst nfs (l,r) σ Q" .
from R[OF lr] obtain l' r' where lr': "(l',r') ∈ R'" and eq: "(l,r) =⇩v (l',r')" by auto
from eq_rule_mod_varsE[OF eq]
obtain σ1 σ2 where 1: "l = l' ⋅ σ1" "r = r' ⋅ σ1" and 2: "l' = l ⋅ σ2" "r' = r ⋅ σ2" by auto
from x y have xy: "x = l' ⋅ (σ1 ∘⇩s σ)" "y = r' ⋅ (σ1 ∘⇩s σ)" unfolding 1 by auto
show "(x,y) ∈ rqrstep nfs Q R'"
proof (rule rqrstepI[OF _ lr' xy])
show "∀u⊲l' ⋅ σ1 ∘⇩s σ. u ∈ NF_terms Q" using NF[unfolded 1] by simp
show "NF_subst nfs (l', r') (σ1 ∘⇩s σ) Q"
proof
fix x
assume nfs and x: "x ∈ vars_term l' ∨ x ∈ vars_term r'"
have "l' ⋅ σ1 ⋅ σ2 = l'" "r' ⋅ σ1 ⋅ σ2 = r'" unfolding 1[symmetric] 2[symmetric] by auto
then have l': "l' ⋅ (σ1 ∘⇩s σ2) = l' ⋅ Var" and r': "r' ⋅ (σ1 ∘⇩s σ2) = r' ⋅ Var" by auto
from term_subst_eq_rev[OF l'] term_subst_eq_rev[OF r'] x have "(σ1 ∘⇩s σ2) x = Var x" by blast
then have id: "σ1 x ⋅ σ2 = Var x" unfolding subst_compose_def by auto
then obtain y where x1: "σ1 x = Var y" by (cases "σ1 x", auto)
from x
have y: "y ∈ vars_term l ∨ y ∈ vars_term r" unfolding 1 using x1 unfolding vars_term_subst by force
then have y: "y ∈ vars_rule (l,r)" unfolding vars_rule_def by simp
from nfs[unfolded NF_subst_def] ‹nfs› y have "σ y ∈ NF_terms Q" by auto
then show "(σ1 ∘⇩s σ) x ∈ NF_terms Q" unfolding subst_compose_def x1 by simp
qed
qed
qed
lemma qrstep_rename_vars: assumes R: "⋀ st. st ∈ R ⟹ ∃ st'. st' ∈ R' ∧ st =⇩v st'"
shows "qrstep nfs Q R ⊆ qrstep nfs Q R'"
proof
fix s t
assume "(s,t) ∈ qrstep nfs Q R"
from qrstepE[OF this] obtain C σ l r where
"∀u⊲l ⋅ σ. u ∈ NF_terms Q" "(l, r) ∈ R" and st: "s = C⟨l ⋅ σ⟩" "t = C⟨r ⋅ σ⟩" and "NF_subst nfs (l, r) σ Q" .
then have "(l ⋅ σ, r ⋅ σ) ∈ rqrstep nfs Q R" by auto
from set_mp[OF rqrstep_rename_vars[OF R] this] have "(l ⋅ σ, r ⋅ σ) ∈ rqrstep nfs Q R'" .
then have "(l ⋅ σ, r ⋅ σ) ∈ qrstep nfs Q R'" unfolding qrstep_iff_rqrstep_or_nrqrstep ..
with st show "(s,t) ∈ qrstep nfs Q R'" by auto
qed
lemma NF_subst_qrstep: assumes "⋀ fn . fn ∈ funas_term t ⟹ ¬ defined (applicable_rules Q R) fn"
and varsNF: "⋀ x. x ∈ vars_term t ⟹ σ x ∈ NF (qrstep nfs Q R)"
and var_cond: "∀(l, r) ∈ R. is_Fun l"
shows "(t ⋅ σ) ∈ NF (qrstep nfs Q R)"
proof
fix s
show "(t ⋅ σ, s) ∉ qrstep nfs Q R"
proof
assume "(t ⋅ σ, s) ∈ qrstep nfs Q R"
from qrstepE[OF this]
obtain C σ' l r where nf: "∀u⊲l ⋅ σ'. u ∈ NF_terms Q"
and lr: "(l, r) ∈ R" and t: "t ⋅ σ = C⟨l ⋅ σ'⟩" and nfs: "NF_subst nfs (l, r) σ' Q" .
from var_cond lr
obtain f ls where l: "l = Fun f ls" by (cases l, auto)
let ?f = "(f,length ls)"
from l lr only_applicable_rules[OF nf] have "defined (applicable_rules Q R) ?f"
unfolding applicable_rules_def defined_def by force
with assms have f: "?f ∉ funas_term t" by auto
with varsNF t
show False
proof (induct t arbitrary: C)
case (Var x)
from Var(1)[of x] Var(2) have NF: "C⟨l ⋅ σ'⟩ ∈ NF (qrstep nfs Q R)" by auto
with qrstepI[OF nf lr refl refl nfs, of C] show False by auto
next
case (Fun g ts)
from Fun(3-4) arg_cong[OF Fun(3), of root, unfolded l, simplified] l obtain bef D aft where
C: "C = More g bef D aft" and len: "length ts = Suc (length bef + length aft)" by (cases C, auto)
from Fun(3)[unfolded C] have id: "map (λt. t ⋅ σ) ts = bef @ D⟨l ⋅ σ'⟩ # aft" by auto
let ?i = "length bef"
let ?t = "ts ! ?i"
from len have mem: "?t ∈ set ts" by auto
from len arg_cong[OF id, of "λ ts. ts ! ?i"] have idt: "?t ⋅ σ = D ⟨l ⋅ σ' ⟩" by simp
show False
by (rule Fun(1)[OF mem Fun(2) idt], insert Fun(4) mem, auto)
qed
qed
qed
lemma NF_subst_from_NF_args:
assumes wf: "Q ≠ {} ⟹ nfs ⟹ wf_rule (s,t)"
and NF: "set (args (s ⋅ σ)) ⊆ NF_terms Q"
shows "NF_subst nfs (s, t) σ Q"
proof (cases "Q = {} ∨ ¬ nfs")
case False
with wf obtain f ss where s: "s = Fun f ss" and vars: "vars_term s ⊇ vars_term t"
unfolding wf_rule_def by (cases s, auto)
show ?thesis
proof
fix x
assume "x ∈ vars_term s ∨ x ∈ vars_term t"
with vars have "x ∈ vars_term s" by auto
with s obtain si where si: "si ∈ set ss" and "x ∈ vars_term si" by auto
then have "si ⊵ Var x" by auto
then have sub: "si ⋅ σ ⊵ σ x" by auto
from si NF s have "si ⋅ σ ∈ NF_terms Q" by auto
from NF_subterm[OF this sub] show "σ x ∈ NF_terms Q" .
qed
qed auto
end