theory Semantic_Labeling
imports
QTRS.Q_Restricted_Rewriting
TA.DP_Transformation
begin
type_synonym ('v, 'c) assign = "'v ⇒ 'c"
type_synonym ('f, 'c) inter = "'f ⇒ 'c list ⇒ 'c"
type_synonym ('f, 'l) labels = "'f ⇒ nat ⇒ 'l ⇒ bool"
type_synonym ('f, 'c, 'l) label = "'f ⇒ 'c list ⇒ 'l"
type_synonym ('f, 'l, 'lf) lcompose = "'f ⇒ nat ⇒ 'l ⇒ 'lf"
type_synonym ('lf, 'f, 'l) ldecompose = "'lf ⇒ ('f × 'l)"
fun eval_lab :: "('f,'c)inter ⇒ ('f,'c,'l)label ⇒ ('f,'l,'lf)lcompose ⇒ ('v,'c)assign ⇒ ('f,'v)term ⇒ ('c × ('lf,'v)term)"
where "eval_lab I L LC α (Var x) = (α x, Var x)"
| "eval_lab I L LC α (Fun f ts) =
(let clts = map (eval_lab I L LC α) ts;
cs = map fst clts;
c = I f cs;
lts = map snd clts in
(c, Fun (LC f (length ts) (L f cs)) lts))"
fun lab_root :: "('f,'c)inter ⇒ ('f,'c,'l)label ⇒ ('f,'c,'l)label ⇒ ('f,'l,'lf)lcompose ⇒ ('v,'c)assign ⇒ ('f,'v)term ⇒ ('lf,'v)term"
where "lab_root I L L' LC α (Fun f ts) =
(let clts = map (eval_lab I L LC α) ts;
cs = map fst clts;
lts = map snd clts in
(Fun (LC f (length ts) (L' f cs)) lts))"
| "lab_root _ _ _ _ _ (Var x) = (Var x)"
fun lab_root_all :: "('f,'c)inter ⇒ ('f,'c,'l)label ⇒ ('f,'c,'l)label ⇒ ('f,'l,'lf)lcompose ⇒ ('f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool) ⇒ ('v,'c)assign ⇒ ('f,'v)term ⇒ ('lf,'v)terms"
where "lab_root_all I L L' LC lge α (Fun f ts) =
(let clts = map (eval_lab I L LC α) ts;
cs = map fst clts;
lts = map snd clts;
l = L' f cs in
{(Fun (LC f (length ts) ls) lts) | ls. lge f (length ts) l ls})"
| "lab_root_all _ _ _ _ _ _ (Var x) = {(Var x)}"
abbreviation eval where "eval I L LC α t ≡ fst (eval_lab I L LC α t)"
abbreviation lab where "lab I L LC α t ≡ snd (eval_lab I L LC α t)"
definition wf_assign where "wf_assign C α ≡ ∀ x. α x ∈ C"
definition lab_rule where "lab_rule I L LC C lr ≡ {(lab I L LC α (fst lr), lab I L LC α (snd lr)) | α . wf_assign C α}"
definition lab_lhs where "lab_lhs I L LC C l ≡ {lab I L LC α l | α . wf_assign C α}"
definition lab_root_rule where "lab_root_rule I L L' LC C lr ≡ {(lab_root I L L' LC α (fst lr), lab_root I L L' LC α (snd lr)) | α . wf_assign C α}"
definition lab_root_all_rule where "lab_root_all_rule I L L' LC lge C rule ≡ {(lab_root I L L' LC α (fst rule), lr) | α lr. wf_assign C α ∧ lr ∈ lab_root_all I L L' LC lge α (snd rule)}"
abbreviation lab_trs where "lab_trs I L LC C R ≡ ⋃(lab_rule I L LC C ` R)"
abbreviation lab_lhss where "lab_lhss I L LC C Q ≡ ⋃(lab_lhs I L LC C ` Q)"
abbreviation lab_lhss_all where "lab_lhss_all LD Q ≡ { lt. map_funs_term (λ fl. fst (LD fl)) lt ∈ Q}"
abbreviation lab_root_trs where "lab_root_trs I L L' LC C R ≡ ⋃(lab_root_rule I L L' LC C ` R)"
abbreviation lab_root_all_trs where "lab_root_all_trs I L L' LC lge C R ≡ ⋃(lab_root_all_rule I L L' LC lge C ` R)"
definition wf_inter where "wf_inter I C ≡ ∀ f cs. set cs ⊆ C ⟶ I f cs ∈ C"
definition wf_label where "wf_label L LS C ≡ ∀ f cs. set cs ⊆ C ⟶ LS f (length cs) (L f cs)"
abbreviation qmodel_rule where "qmodel_rule I L LC C cge l r ≡ ∀ α. wf_assign C α ⟶ cge (eval I L LC α l) (eval I L LC α r)"
definition qmodel where "qmodel I L LC C cge R ≡ ∀ (l,r) ∈ R. qmodel_rule I L LC C cge l r"
definition cge_wm: "cge_wm I C cge ≡ ∀ f bef c d aft. (set ([c,d] @ bef @ aft) ⊆ C ∧ cge c d ⟶ cge (I f (bef @ c # aft)) (I f (bef @ d # aft)))"
definition lge_wm: "lge_wm I L C cge lge ≡ ∀ f bef c d aft. (set ([c,d] @ bef @ aft) ⊆ C ∧ cge c d ⟶ lge f (Suc (length bef + length aft)) (L f (bef @ c # aft)) (L f (bef @ d # aft)))"
definition
decr_of_ord :: "('f ⇒ nat ⇒ 'l rel) ⇒ ('f,'l,'lf)lcompose ⇒ ('f,'l)labels ⇒ ('lf, 'v) trs"
where
"decr_of_ord gr LC LS ≡ {(Fun (LC f (length ts) l) ts, Fun (LC f (length ts) l') ts) | f l l' ts. LS f (length ts) l ∧ LS f (length ts) l' ∧ (l,l') ∈ gr f (length ts)}"
definition lge_to_lgr :: "('f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool) ⇒ ('f,'l)labels ⇒ 'f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool"
where "lge_to_lgr lge LS f n ≡ let LSfn = LS f n; lgefn = lge f n in (λ l l'. l ≠ l' ∧ LSfn l ∧ LSfn l' ∧ lgefn l l')"
definition lge_to_lgr_rel :: "('f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool) ⇒ ('f,'l)labels ⇒ 'f ⇒ nat ⇒ 'l rel"
where "lge_to_lgr_rel lge LS f n ≡ {(l,l')| l l'. lge_to_lgr lge LS f n l l'}"
locale sl_interpr =
fixes C :: "'c set"
and c :: "'c"
and I :: "('f,'c)inter"
and cge :: "'c ⇒ 'c ⇒ bool"
and lge :: "'f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool"
and L :: "('f,'c,'l)label"
and LC :: "('f,'l,'lf)lcompose"
and LD :: "('lf,'f,'l)ldecompose"
and LS :: "('f,'l)labels"
assumes c: "c ∈ C"
and wf_I: "wf_inter I C"
and wf_L: "wf_label L LS C"
and wm_cge: "cge_wm I C cge"
and wm_lge: "lge_wm I L C cge lge"
and gr_SN: "⋀ f n. SN (lge_to_lgr_rel lge LS f n)"
and LD_LC: "⋀ f n l. LD (LC f n l) = (f,l)"
and lge_trans: "⋀ f n x y z. ⟦lge f n x y; lge f n y z⟧ ⟹ lge f n x z"
locale sl_interpr_root = sl_interpr C c I cge lge L LC LD LS
for C c I cge lge L and LC :: "('f,'l,'lf)lcompose" and LD LS +
fixes
L' :: "('f,'c,'l)label"
and LS' :: "('f,'l)labels"
assumes
wf_L': "wf_label L' LS' C"
and wm_lge': "lge_wm I L' C cge lge"
and lge_refl: "⋀ f n x. LS' f n x ⟹ lge f n x x"
and gr'_SN: "⋀ f n. SN (lge_to_lgr_rel lge (λ f n x. LS f n x ∨ LS' f n x) f n)"
context sl_interpr
begin
abbreviation gr where "gr ≡ lge_to_lgr_rel lge LS"
abbreviation Eval where "Eval ≡ eval I L LC"
abbreviation Lab where "Lab ≡ lab I L LC"
abbreviation Lab_trs :: "('f,'v)trs ⇒ ('lf,'v)trs" where "Lab_trs ≡ lab_trs I L LC C"
abbreviation Lab_lhss :: "('f,'v)terms ⇒ ('lf,'v)terms" where "Lab_lhss ≡ lab_lhss I L LC C"
abbreviation Lab_lhss_all :: "('f,'v)terms ⇒ ('lf,'v)terms" where "Lab_lhss_all ≡ lab_lhss_all LD"
abbreviation wf_ass where "wf_ass ≡ wf_assign C"
definition subst_ass where "subst_ass α σ ≡ λ x. Eval α (σ x)"
definition lab_subst where "lab_subst α σ ≡ (λx. Lab α (σ x))"
abbreviation Decr :: "('lf,'v)trs" where "Decr ≡ decr_of_ord gr LC LS"
definition default_ass where "default_ass x = c"
abbreviation LAB where "LAB t ≡ Lab default_ass t"
abbreviation UNLAB where "UNLAB fl ≡ fst (LD fl)"
end
context sl_interpr_root
begin
abbreviation LS_both where "LS_both ≡ (λ f n x. LS f n x ∨ LS' f n x)"
abbreviation gr_root where "gr_root ≡ lge_to_lgr_rel lge LS'"
abbreviation gr_both where "gr_both ≡ lge_to_lgr_rel lge LS_both"
abbreviation Lab_root where "Lab_root ≡ lab_root I L L' LC"
abbreviation Lab_root_all where "Lab_root_all ≡ lab_root_all I L L' LC lge"
abbreviation Lab_root_trs :: "('f,'v)trs ⇒ ('lf,'v)trs" where "Lab_root_trs ≡ lab_root_trs I L L' LC C"
abbreviation Lab_root_all_trs :: "('f,'v)trs ⇒ ('lf,'v)trs" where "Lab_root_all_trs ≡ lab_root_all_trs I L L' LC lge C"
abbreviation Decr_root :: "('lf,'v)trs" where "Decr_root ≡ decr_of_ord gr_root LC LS'"
abbreviation Decr_both :: "('lf,'v)trs" where "Decr_both ≡ decr_of_ord gr_both LC LS_both"
abbreviation LAB_root where "LAB_root t ≡ Lab_root default_ass t"
end
context sl_interpr
begin
lemma Decr_SN_generic: assumes grSN: "⋀ f n. SN (lge_to_lgr_rel lge LSg f n)"
shows "SN (rstep (decr_of_ord (lge_to_lgr_rel lge LSg) LC LSg))" (is "SN (rstep ?Decr)")
proof -
let ?gr = "lge_to_lgr_rel lge LSg"
let ?id = "id :: 'lf ⇒ 'lf"
let ?nfs = "False"
let ?m = "False"
show ?thesis
proof(rule ccontr)
assume nSN: "¬ ?thesis"
hence nSN: "¬ SN (qrstep ?nfs {} ?Decr)" by auto
have wf_trs: "wf_trs ?Decr" unfolding decr_of_ord_def wf_trs_def by auto
hence wf_trs: "wf_qtrs ?nfs {} ?Decr" unfolding wf_qtrs_def wwf_qtrs_def wf_trs_def by auto
from not_SN_imp_ichain[OF this nSN]
obtain s t σ where ichain: "ichain (initial_dpp ?id ?nfs ?m {} ?Decr) s t σ" by blast
note ichain = ichain[unfolded initial_dpp.simps applicable_rules_empty]
have DP: "DP ?id ?Decr ⊆ {(Fun ((LC f (length ts) l)) ts, Fun ((LC f (length ts) l')) ts) | f l l' (ts :: ('lf,'a)term list). (l,l') ∈ ?gr f (length ts)}" (is "_ ⊆ ?DP")
proof -
{
fix f l l' ts h and us :: "('lf,'a) term list"
assume gr: "(l,l') ∈ ?gr f (length ts)" and right: "Fun (LC f (length ts) l') ts ⊵ Fun h us" and left: "¬ (Fun (LC f (length ts) l) ts ⊳ Fun h us)"
let ?n = "length ts"
have "(sharp_term id (Fun (LC f ?n l) ts), sharp_term id (Fun h us)) ∈ ?DP"
proof (cases "Fun h us = Fun (LC f ?n l') ts")
case True
with gr show ?thesis by auto
next
case False
with right have "Fun (LC f ?n l') ts ⊳ Fun h us" by auto
hence "Fun (LC f ?n l) ts ⊳ Fun h us"
proof (cases, (auto)[1])
case (subt s)
thus ?thesis ..
qed
with left show ?thesis by blast
qed
}
thus ?thesis unfolding DP_on_def decr_of_ord_def by blast
qed
from ichain DP have DP: "⋀ i. (s i, t i) ∈ ?DP" by (simp add: ichain.simps) blast
obtain l where l: "l = (λ t :: ('lf,'a)term. case t of Fun lf _ ⇒ snd (LD lf))" by auto
obtain n where n: "n = (λ i. num_args (s i))" by auto
obtain f where f: "f = (λ i. case (s i) of Fun lf _ ⇒ fst (LD lf))" by auto
{
fix i :: nat
from DP[of i] obtain fi li li' usi where si: "s i = Fun ((LC fi (length usi) li')) usi" and ti: "t i = Fun ((LC fi (length usi) li)) usi" by blast
let ?n = "length usi"
from DP[of i] obtain f' ll l' where "LC fi (length usi) li' = LC f' (length usi) l' ∧ LC fi (length usi) li = LC f' (length usi) ll ∧ (l', ll) ∈ ?gr f' (length usi)" unfolding si ti by auto
hence id: "LD (LC fi (length usi) li') = LD (LC f' (length usi) l') ∧ LD (LC fi (length usi) li) = LD (LC f' (length usi) ll)" and gr: "(l', ll) ∈ ?gr f' (length usi)" by auto
from id[unfolded LD_LC] gr have labels: "(li',li) ∈ ?gr fi ?n" by simp
have lti: "l (t i) = li" unfolding l ti using LD_LC by simp
have lsi: "l (s i) = li'" unfolding l si using LD_LC by simp
from ichain have "(t i ⋅ σ i, s (Suc i) ⋅ (σ (Suc i))) ∈ (rstep ?Decr)^*" by (simp add: ichain.simps)
hence steps: "(Fun ((LC fi ?n li)) (map (λ u. u ⋅ σ i) usi), s (Suc i) ⋅ σ (Suc i)) ∈ (rstep ?Decr)^*" unfolding ti by simp
have nvar: "∀ lr ∈ ?Decr. ∀ x. fst lr ≠ Var x" unfolding decr_of_ord_def map_funs_trs.simps by auto
obtain t where t: "s (Suc i) ⋅ σ (Suc i) = t" by auto
obtain ts where ts: "map (λ u. u ⋅ σ i) usi = ts" and lts: "length usi = length ts" by auto
from steps have "∃ ssi li'. s (Suc i) ⋅ σ (Suc i) = Fun ((LC fi ?n li')) ssi ∧ length ssi = ?n ∧ (li,li') ∈ (?gr fi ?n)^*"
unfolding t ts lts
proof (induct)
case base
show ?case by auto
next
case (step u s)
from step(3) obtain vs li' where u: "u = Fun (LC fi (length ts) li') vs" and len: "length vs = length ts" and li': "(li,li') ∈ (?gr fi (length ts))^*" by auto
from step(2) obtain C l r σ where ul: "u = C⟨l ⋅ σ⟩" and sr: "s = C⟨r ⋅ σ⟩" and lr: "(l,r) ∈ ?Decr" by auto
show ?case
proof (cases C)
case (More g bef D aft)
let ?ts = "(bef @ D⟨r⋅σ⟩ # aft)"
from u[unfolded ul] len have "s = Fun (LC fi (length ts) li') ?ts" and "length ?ts = length ts" unfolding sr More by auto
with li' show ?thesis by auto
next
case Hole
hence ul: "u = l ⋅ σ" and sr: "s = r ⋅ σ" using ul sr by auto
from lr[unfolded decr_of_ord_def] obtain f l1 l2 ls where l: "l = Fun (LC f (length ls) l1) ls" and r: "r = Fun (LC f (length ls) l2) ls" and l1l2: "(l1,l2) ∈ ?gr f (length ls)"
by auto
from ul[unfolded u l] len have len: "length ls = length ts" and f: "LC fi (length ts) li' = LC f (length ts) l1" (is "?l = ?l1") by auto
hence "LD ?l = LD ?l1" by auto
from this[unfolded LD_LC] have f: "f = fi" and l1: "l1 = li'" by auto
from li' l1l2[unfolded len f l1] have "(li,l2) ∈ (?gr fi (length ts))^*" by auto
with sr[unfolded r f len] len show ?thesis by auto
qed
qed
then obtain ssi li'' where "s (Suc i) ⋅ σ (Suc i) = Fun ((LC fi ?n li'')) ssi" and "length ssi = ?n" and li'': "(li,li'') ∈ (?gr fi ?n)^*" by auto
with DP[of "Suc i"] obtain ssi where ssi: "s (Suc i) = Fun ((LC fi ?n li'')) ssi" and len: "length ssi = ?n" by auto
have lssi: "l (s (Suc i)) = li''" unfolding l ssi using LD_LC by simp
from labels li'' have "(l (s i), l (s (Suc i))) ∈ (?gr (f i) (n i))^+" and "n (Suc i) = n i" and "f (Suc i) = f i" unfolding lsi lssi lti n f
unfolding si ssi by (auto simp: len LD_LC)
} note main = this
{
fix i
have "n i = n 0 ∧ f i = f 0"
by (induct i, auto simp: main)
with main(1)[of i] have "(l (s i), l (s (Suc i))) ∈ (?gr (f 0) (n 0))^+" by simp
}
with SN_imp_SN_trancl[OF grSN[of "f 0" "n 0"]] show False unfolding SN_defs by force
qed
qed
lemma Decr_SN: "SN (rstep Decr)"
by (rule Decr_SN_generic, rule gr_SN)
lemma wf_default_ass: "wf_ass default_ass"
unfolding default_ass_def wf_assign_def using c by auto
lemma eval_subst[simp] :
"Eval α (t ⋅ σ) = Eval (subst_ass α σ) t"
proof (induct t, simp add: subst_ass_def)
case (Fun f ts)
let ?beta = "subst_ass α σ"
have evalInd: "map (λ x. Eval α (x ⋅ σ)) ts = map (Eval ?beta) ts" using Fun by auto
have "Eval α (Fun f ts ⋅ σ) = Eval α (Fun f (map (λ t. t ⋅ σ) ts))" by simp
also have "… = Eval ?beta (Fun f ts)" by (simp add: Let_def o_def evalInd)
finally show ?case .
qed
lemma lab_subst[simp] :
"Lab α (t ⋅ σ) = Lab (subst_ass α σ) t ⋅ lab_subst α σ"
by (induct t, simp add: lab_subst_def, simp add: Let_def o_def)
end
context sl_interpr_root
begin
lemma Decr_both: "Decr ∪ Decr_root ⊆ Decr_both"
proof -
{
fix l r f n
assume "(l,r) ∈ gr f n"
hence "(l,r) ∈ gr_both f n" unfolding lge_to_lgr_rel_def lge_to_lgr_def
by (auto simp: Let_def)
} note subset = this
{
fix l r f n
assume "(l,r) ∈ gr_root f n"
hence "(l,r) ∈ gr_both f n" unfolding lge_to_lgr_rel_def lge_to_lgr_def
by (auto simp: Let_def)
} note subset_root = this
show "Decr ∪ Decr_root ⊆ Decr_both" (is "?DD ⊆ _")
proof
fix s t
assume "(s,t) ∈ ?DD"
thus "(s,t) ∈ Decr_both"
proof
assume "(s,t) ∈ Decr"
thus ?thesis unfolding decr_of_ord_def using subset by blast
next
assume "(s,t) ∈ Decr_root"
thus ?thesis unfolding decr_of_ord_def using subset_root by blast
qed
qed
qed
lemma Decr_SN_both: "SN (rstep Decr_both)"
by (rule Decr_SN_generic[OF gr'_SN] )
lemma Decr_SN_both_2: "SN (rstep (Decr ∪ Decr_root))"
by (rule SN_subset[OF Decr_SN_both rstep_mono[OF Decr_both]])
lemma lab_root_subst[simp]:
"is_Fun t ⟹ Lab_root α (t ⋅ σ) = Lab_root (subst_ass α σ) t ⋅ lab_subst α σ"
by (cases t, auto simp add: o_def)
end
context sl_interpr
begin
lemma wf_term[simp]: assumes "wf_ass α"
shows "Eval α t ∈ C"
proof (induct t)
case (Var x)
with assms show ?case by (auto simp: wf_assign_def)
next
case (Fun f ts)
let ?cs = "map (Eval α) ts"
let ?c = "I f ?cs"
from Fun have "set ?cs ⊆ C" by auto
with wf_I have "?c ∈ C" unfolding wf_inter_def by (best)
thus ?case by (simp add: Let_def o_def)
qed
lemma wf_ass_subst_ass[simp]: assumes "wf_ass α"
shows "wf_ass (subst_ass α σ)"
using assms unfolding subst_ass_def by (simp add: wf_assign_def)
lemma quasi_sem_rewrite: assumes step: "(s,t) ∈ qrstep nfs Q R"
and qmodel: "qmodel I L LC C cge R"
and wfass: "wf_ass α"
shows "cge (Eval α s) (Eval α t)"
using step
proof
fix l r C' σ assume in_R: "(l, r) ∈ R" and s: "s = C'⟨l⋅σ⟩" and t: "t = C'⟨r⋅σ⟩"
let ?beta = "subst_ass α σ"
have wfbeta: "wf_ass ?beta" using wfass by auto
have "Eval α (l⋅σ) = Eval ?beta l" by simp
also have "cge … (Eval ?beta r)" using in_R wfbeta qmodel by (auto simp: qmodel_def)
also have "… = Eval α (r⋅σ)" by simp
finally have root: "cge (Eval α (l⋅σ)) (Eval α (r⋅σ))" .
have "Eval α s = Eval α (C'⟨l⋅σ⟩)" by (simp add: s)
also have "cge … (Eval α (C'⟨r⋅σ⟩))"
proof (induct C', simp add: root[simplified])
case (More f bef D aft)
show ?case
proof (simp add: Let_def, rule wm_cge[unfolded cge_wm, THEN spec, THEN spec, THEN spec, THEN spec, THEN spec, THEN mp],
rule conjI[OF _ More], rule subsetI)
fix x
assume "x ∈ set ([Eval α D⟨l ⋅ σ⟩, Eval α D⟨r ⋅ σ⟩] @ map (fst ∘ eval_lab I L LC α) bef @ map (fst ∘ eval_lab I L LC α) aft)"
hence "x ∈ { Eval α u | u. True}" by auto
with wf_term[OF wfass] show "x ∈ C" by blast
qed
qed
also have "… = Eval α t" by (simp add: t)
finally show ?thesis .
qed
lemma UNLAB_lab: "map_funs_term UNLAB (Lab α t) = t"
proof (induct t)
case (Var x) thus ?case by auto
next
case (Fun f ts)
thus ?case
unfolding eval_lab.simps Let_def snd_conv term.simps
LD_LC fst_conv
by (induct ts, auto)
qed
lemma Lab_lhss_subset: "Lab_lhss Q ⊆ Lab_lhss_all Q"
proof
fix t
assume "t ∈ Lab_lhss Q"
then obtain α q where q: "q ∈ Q" and "wf_assign C α" and t: "t = Lab α q"
by (force simp: lab_lhs_def)
show "t ∈ Lab_lhss_all Q" unfolding t using q
by (auto simp: UNLAB_lab)
qed
lemma gr_irreflexive: "(l,l) ∉ gr f n"
using SN_on_irrefl[OF gr_SN[of f n]] by blast
lemma lab_nf:
assumes nf: "s ∈ NF_terms Q"
shows "Lab α s ∈ NF_terms (Lab_lhss_all Q)"
proof(rule, rule)
fix t
assume "(Lab α s, t) ∈ rstep (Id_on (Lab_lhss_all Q))"
from rstep_imp_map_rstep[OF this, of UNLAB, unfolded UNLAB_lab]
have step: "(s, map_funs_term UNLAB t) ∈ rstep (map_funs_trs UNLAB (Id_on (Lab_lhss_all Q)))" (is "?p ∈ rstep ?Q") .
have subset: "?Q ⊆ Id_on Q"
proof -
{
fix l r
assume "(l,r) ∈ ?Q"
then obtain q where "q ∈ Lab_lhss_all Q" and "l = map_funs_term UNLAB q" and "r = map_funs_term UNLAB q"
by (force simp: map_funs_trs.simps)
hence "(l,r) ∈ Id_on Q" by auto
}
thus ?thesis by auto
qed
from rstep_mono[OF subset] step
have "(s, map_funs_term UNLAB t) ∈ rstep (Id_on Q)" by auto
with nf show False
by auto
qed
lemma vars_term_lab[simp]: "vars_term (Lab α t) = vars_term t"
by (induct t, auto simp: Let_def)
lemma lab_nf_subst: assumes "NF_subst nfs (l,r) σ Q"
shows "NF_subst nfs (Lab α l, Lab β r) (lab_subst γ σ) (Lab_lhss_all Q)"
proof
let ?l = "Lab α l"
let ?r = "Lab β r"
let ?σ = "lab_subst γ σ"
fix x
assume nfs and "x ∈ vars_term ?l ∨ x ∈ vars_term ?r"
hence x: "x ∈ vars_rule (l,r)" by (auto simp: vars_rule_def)
show "?σ x ∈ NF_terms (Lab_lhss_all Q)" unfolding lab_subst_def
by (rule lab_nf, insert assms[unfolded NF_subst_def] ‹nfs› x, auto)
qed
lemma lab_rqrstep: assumes step: "(s,t) ∈ rqrstep nfs Q R"
and wfass: "wf_ass α"
shows "(Lab α s, Lab α t) ∈ rqrstep nfs (Lab_lhss_all Q) (Lab_trs R)"
using step
proof
fix l r σ
assume rule: "(l,r) ∈ R" and s: "s = l ⋅ σ" and t: "t = r ⋅ σ"
and nfs: "NF_subst nfs (l,r) σ Q"
and NF: "∀u⊲l ⋅ σ. u ∈ NF_terms Q"
let ?beta = "subst_ass α σ"
let ?delt = "lab_subst α σ"
let ?Q = "Lab_lhss_all Q"
have wfbeta: "wf_ass ?beta" using wfass by auto
from rule wfbeta
have mem: "(Lab ?beta l, Lab ?beta r) ∈ (Lab_trs R)" by (simp add: lab_rule_def, force)
have id: "Lab ?beta l ⋅ ?delt = Lab α (l ⋅ σ)" by simp
note conv = NF_rstep_supt_args_conv
show ?thesis unfolding s t
proof (rule rqrstepI[OF _ mem lab_subst lab_subst lab_nf_subst[OF nfs]])
show "∀ u ⊲ Lab ?beta l ⋅ ?delt. u ∈ NF_terms ?Q" unfolding id conv
proof
fix u
assume u: "u ∈ set (args (Lab α (l ⋅ σ)))"
then obtain f ls where ls: "l ⋅ σ = Fun f ls" by (cases "l ⋅ σ", auto)
from u ls obtain v where u: "u = Lab α v" and v: "v ∈ set ls"
by (auto simp: Let_def)
from NF[unfolded conv ls] v have "v ∈ NF_terms Q" by auto
from lab_nf[OF this]
show "u ∈ NF_terms ?Q" unfolding u .
qed
qed
qed
fun lge_term :: "('lf,'v)term ⇒ ('lf,'v)term ⇒ bool"
where "lge_term (Var x) (Var y) = (x = y)"
| "lge_term (Fun f ts) (Fun g ss) = (length ts = length ss ∧ (∀ i < length ss. lge_term (ts ! i) (ss ! i))
∧ (∃ h lf lg. f = LC h (length ss) lf ∧ g = LC h (length ss) lg ∧ (lf = lg ∨ Ball {lf,lg} (LS h (length ss)) ∧ lge h (length ss) lf lg)))"
| "lge_term _ _ = False"
lemma lge_term_decr:
assumes D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and ge: "lge_term u (Lab α s)"
and NF: "∀ t ⊲ s. t ∈ NF_terms Q"
shows "(u,Lab α s) ∈ (qrstep nfs (Lab_lhss_all Q) D)^*" (is "_ ∈ ?D^*")
using ge NF
proof (induct s arbitrary: u)
case (Var x)
thus ?case by (cases u, auto)
next
case (Fun f ss)
let ?Q = "Lab_lhss_all Q"
from Fun(2) obtain g us where u: "u = Fun g us" by (cases u, auto simp: Let_def)
note Fun = Fun[unfolded u]
have id: "Lab α (Fun f ss) = Fun (LC f (length ss) (L f (map (Eval α) ss))) (map (Lab α) ss)"
(is "_ = Fun ?g ?ss")
by (simp add: Let_def o_def)
from Fun(2)[unfolded id] obtain h lg1 lg2 where len: "length ss = length us" and g: "g = LC h (length ss) lg1" and h: "?g = LC h (length ss) lg2" and disj: "lg1 = lg2 ∨ Ball {lg1,lg2} (LS h (length ss)) ∧ lge h (length ss) lg1 lg2" by auto
from h have "LD ?g = LD (LC h (length ss) lg2)" by simp
from this[unfolded LD_LC] have h: "h = f" and lg2: "L f (map (Eval α) ss) = lg2" by auto
{
fix i
assume i: "i < length ss"
from i have mem: "ss ! i ∈ set ss" by auto
from i Fun(2)[unfolded id] have ge: "lge_term (us ! i) (Lab α (ss ! i))" by auto
have NF1: "∀ t ⊲ ss ! i. t ∈ NF_terms Q" using mem Fun(3) by auto
from Fun(3)[unfolded NF_rstep_supt_args_conv] mem have "ss ! i ∈ NF_terms Q" by simp
from lab_nf[OF this] have NF2: "Lab α (ss ! i) ∈ NF_terms ?Q" .
from Fun(1)[OF mem ge NF1] have "(us ! i, Lab α (ss ! i)) ∈ ?D^*" by auto
note this and NF2
} note args = this
have one: "(Fun g us, Fun g ?ss) ∈ ?D^*"
by (rule args_qrsteps_imp_qrsteps, insert len args(1), auto)
from disj[unfolded h] have "lg1 = lg2 ∨ Ball {lg1, lg2} (LS f (length ss)) ∧ lge f (length ss) lg1 lg2 ∧ lg1 ≠ lg2"
(is "_ ∨ ?two") by blast
thus ?case
proof
assume eq: "lg1 = lg2"
show ?case using one unfolding u g eq id h lg2 .
next
assume ?two
hence "(lg1,lg2) ∈ gr f (length ss)"
unfolding lge_to_lgr_rel_def lge_to_lgr_def Let_def h by auto
hence mem: "(Fun g ?ss, Fun ?g ?ss) ∈ Decr" using ‹?two› unfolding g lg2 decr_of_ord_def h by auto
with D have mem: "(Fun g ?ss, Fun ?g ?ss) ∈ (subst.closure D ∩ Decr)^*" by auto
hence "(Fun g ?ss, Fun ?g ?ss) ∈ ?D^* ∩ { (Fun h1 ?ss, Fun h2 ?ss) | h1 h2. True }"
proof (induct)
case base thus ?case by auto
next
case (step y z)
from step(3)
obtain gg where y: "y = Fun gg ?ss" by auto
note step = step[unfolded y]
from step(3) have steps: "(Fun g ?ss, Fun gg ?ss) ∈ ?D^*" by auto
from step(2)[unfolded decr_of_ord_def] obtain ggg where z: "z = Fun ggg ?ss" by auto
from step(2) have "(Fun gg ?ss, z) ∈ subst.closure D" by auto
then obtain l r σ where lr: "(l,r) ∈ D" and id: "l ⋅ σ = Fun gg ?ss" "z = r ⋅ σ"
by (auto elim: subst.closure.cases)
have D: "?D = qrstep False (Lab_lhss_all Q) D"
by (rule wwf_qtrs_imp_nfs_False_switch[OF wf_trs_imp_wwf_qtrs[OF wf]]) auto
have "(Fun gg ?ss, z) ∈ ?D" unfolding D
proof (rule qrstepI[OF _ lr, of σ _ _ □])
show "∀u⊲ l ⋅ σ. u ∈ NF_terms (Lab_lhss_all Q)"
unfolding id NF_rstep_supt_args_conv set_conv_nth using args(2) by auto
qed (auto simp: id)
with steps have steps: "(Fun g ?ss, z) ∈ ?D^*" by auto
thus ?case unfolding z by auto
qed
with one show ?case unfolding id u by auto
qed
qed
lemma lge_term_refl: "lge_term (Lab α t) (Lab α t)"
proof (induct t)
case (Var x) thus ?case by simp
next
case (Fun f ts)
show ?case
by (unfold lge_term.simps eval_lab.simps map_map o_def snd_conv Let_def length_map, intro conjI,
simp, simp add: Fun,
intro exI conjI, rule refl, rule refl, simp)
qed
lemma quasi_lab_rewrite:
assumes D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and step: "(s,t) ∈ qrstep nfs Q R"
and qmodel: "qmodel I L LC C cge R"
and wfass: "wf_ass α"
and ge: "lge_term u (Lab α s)"
shows "∃ v s'. (u,s') ∈ (qrstep nfs (Lab_lhss_all Q) D)^* ∧ (s',v) ∈ qrstep nfs (Lab_lhss_all Q) (Lab_trs R) ∧ lge_term v (Lab α t)"
using step ge
proof (induct)
case (IH C' σ l r)
let ?Q = "Lab_lhss_all Q"
let ?De = "qrstep nfs ?Q D"
let ?R = "qrstep nfs ?Q (Lab_trs R)"
from IH(4)
show "∃ v s'. (u, s') ∈ ?De^* ∧ (s',v) ∈ ?R ∧ lge_term v (Lab α C'⟨r ⋅ σ⟩)"
proof (induct C' arbitrary: u)
case (Hole u)
from rqrstepI[OF IH(1) IH(2) refl refl IH(3)]
have step: "(l ⋅ σ, r ⋅ σ) ∈ rqrstep nfs Q R" .
from lab_rqrstep[OF this wfass] have "(Lab α (l ⋅ σ), Lab α (r ⋅ σ)) ∈ rqrstep nfs ?Q (Lab_trs R)" .
hence step: "(Lab α (l ⋅ σ), Lab α (r ⋅ σ)) ∈ ?R" unfolding qrstep_iff_rqrstep_or_nrqrstep by auto
have steps: "(u,Lab α (l ⋅ σ)) ∈ ?De^*"
by (rule lge_term_decr[OF D wf], insert Hole IH(1), auto)
show ?case
by (rule exI[of _ "Lab α (r ⋅ σ)"], rule exI[of _ "Lab α (l ⋅ σ)"], intro conjI, rule steps, rule step,
unfold ctxt_apply_term.simps, rule lge_term_refl)
next
case (More f ss D ts u)
let ?n = "Suc (length ss + length ts)"
let ?ll = "L f (map (Eval α) (ss @ D⟨l ⋅ σ⟩ # ts))"
let ?lr = "L f (map (Eval α) (ss @ D⟨r ⋅ σ⟩ # ts))"
let ?D = "More (LC f ?n ?ll) (map (Lab α) ss) □ (map (Lab α) ts)"
let ?E = "More (LC f ?n ?lr) (map (Lab α) ss) □ (map (Lab α) ts)"
from IH(2) have "(D⟨l ⋅ σ⟩, D⟨r ⋅ σ⟩) ∈ qrstep False {} R" using ctxt.closure.intros by auto
hence cge: "cge (Eval α D⟨l ⋅ σ⟩) (Eval α D⟨r ⋅ σ⟩)" using qmodel wfass by (rule quasi_sem_rewrite)
let ?l = "?D⟨Lab α D⟨l ⋅ σ⟩⟩"
let ?r = "?E⟨Lab α D⟨r ⋅ σ⟩⟩"
have id: "Lab α (More f ss D ts)⟨l ⋅ σ⟩ = ?l" "Lab α (More f ss D ts)⟨r ⋅ σ⟩ = ?r"
by (auto simp: Let_def o_def)
{
fix c
assume "c ∈ set ([Eval α D⟨l ⋅ σ⟩, Eval α D⟨r ⋅ σ⟩] @ map (Eval α) ss @ map (Eval α) ts)"
hence "c ∈ { Eval α u | u. True}" by auto
with wf_term[OF wfass] have "c ∈ C" by blast
} note inC = this
have lge: "lge f ?n ?ll ?lr"
by (simp, rule wm_lge[unfolded lge_wm, THEN spec, THEN spec[of _ "map (Eval α) ss"], THEN spec, THEN spec,
THEN spec[of _ "map (Eval α) ts"], THEN mp, simplified length_map], rule conjI[OF _ cge], rule subsetI, rule inC, simp)
from More(2) id have ge: "lge_term u (?D⟨Lab α D⟨ l ⋅ σ⟩⟩)" by simp
then obtain g us where u: "u = Fun g us" and len: "length us = ?n" by (cases u, auto)
let ?m = "length ss"
from ge[unfolded u, simplified]
obtain h lg1 lg2 where ge: "∀ i < ?n. lge_term (us ! i) (map (Lab α) (ss @ D⟨l⋅σ⟩ # ts) ! i)" and g: "g = LC h ?n lg1" and h: "LC f ?n ?ll = LC h ?n lg2" and disj: "lg1 = lg2 ∨ Ball {lg1,lg2} (LS h ?n) ∧ lge h ?n lg1 lg2" by auto
from h have "LD (LC f ?n ?ll) = LD (LC h ?n lg2)" by simp
from this[unfolded LD_LC] have h: "h = f" and lg2: "?ll = lg2" by auto
from ge[THEN spec[of _ "length ss"]] have "lge_term (us ! ?m) (Lab α D⟨l⋅σ⟩)" by (auto simp: nth_append)
from More(1)[OF this] obtain v s' where steps: "(us ! ?m, s') ∈ ?De^*" and step: "(s',v) ∈ ?R" and lge2: "lge_term v (Lab α D⟨r ⋅ σ⟩)" by auto
let ?list = "λ u. (take ?m us @ u # drop (Suc ?m) us)"
let ?C = "λ u. Fun g (?list u)"
have steps: "(?C (us ! ?m), ?C s') ∈ ?De^*"
by (rule ctxt_closed_one[OF _ steps], blast)
have "?m < length us" using len by simp
from id_take_nth_drop[OF this] have "?C (us ! ?m) = Fun g us" by simp
with steps have steps: "(Fun g us, ?C s') ∈ ?De^*" by simp
have step: "(?C s',?C v) ∈ ?R"
by (rule ctxt_closed_one[OF _ step], blast)
show ?case
proof (intro exI conjI, unfold u, rule steps, rule step, unfold id(2))
let ?lisl = "?list v"
let ?lisr = "map (Lab α) ss @ Lab α D⟨r⋅σ⟩ # map (Lab α) ts"
from len have leng: "length ?lisr = ?n" by simp
show "lge_term (Fun g (take ?m us @ v # drop (Suc ?m) us)) ?r"
unfolding ctxt_apply_term.simps lge_term.simps
proof (intro conjI, simp add: len)
let ?p = "λ i. lge_term (?lisl ! i) (?lisr ! i)"
show "∀ i < length ?lisr. ?p i"
proof (intro allI impI)
fix i
assume i: "i < length ?lisr"
with len have i': "i < length us" by auto
show "?p i"
proof (cases "i < ?m")
case True
with ge[THEN spec[of _ i]]
show "?p i"
by (auto simp: i' nth_append)
next
case False note oFalse = this
show "?p i"
proof (cases "i = ?m")
case True
with i' lge2 show ?thesis
by (auto simp: i' nth_append)
next
case False
from oFalse have "i = i - ?m + ?m" by simp
then obtain j where "i = j + ?m" by simp
with False obtain j where id: "i = ?m + Suc j" by (cases j, auto)
from i id have j: "j < length ts" by auto
from j len have min: "min (length us) ?m = ?m" by simp
show "?p i"
using ge[THEN spec[of _ i]] i i' unfolding len[symmetric]
by (auto simp: id nth_append min)
qed
qed
qed
next
obtain n where n: "?n = n" by auto
obtain ll where ll: "?ll = ll" by auto
obtain lr where lr: "?lr = lr" by auto
have "LS f ?n ?ll"
by (simp, rule wf_L[unfolded wf_label_def, THEN spec, THEN spec[of _ "map (Eval α) (ss @ D⟨l ⋅ σ⟩ # ts)"], THEN mp, simplified], auto simp: inC)
hence llLS: "LS f n ll" using ll n by auto
have "LS f ?n ?lr"
by (simp, rule wf_L[unfolded wf_label_def, THEN spec, THEN spec[of _ "map (Eval α) (ss @ D⟨r ⋅ σ⟩ # ts)"], THEN mp, simplified], auto simp: inC)
hence lrLS: "LS f n lr" using lr n by auto
show "∃ h lf lg.
g = LC h (length ?lisr) lf ∧
LC f ?n ?lr = LC h (length ?lisr) lg ∧
(lf = lg ∨ Ball {lf,lg} (LS h (length ?lisr)) ∧ lge h (length ?lisr) lf lg)"
unfolding leng n g h
proof (intro exI conjI, rule refl, rule refl, insert disj[unfolded lg2[symmetric]] lge, unfold leng n h ll lr)
assume one: "lg1 = ll ∨ Ball {lg1,ll} (LS f n) ∧ lge f n lg1 ll"
and two: "lge f n ll lr"
from one
show "lg1 = lr ∨ Ball {lg1,lr} (LS f n) ∧ lge f n lg1 lr"
proof
assume "lg1 = ll"
with two llLS lrLS show ?thesis by auto
next
assume "Ball {lg1,ll} (LS f n) ∧ lge f n lg1 ll"
with lge_trans[OF _ two, of lg1] lrLS show ?thesis by auto
qed
qed
qed
qed
qed
qed
lemma quasi_lab_rewrites:
assumes D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and step: "(s,t) ∈ (qrstep nfs Q R)^*"
and qmodel: "qmodel I L LC C cge R"
and wfass: "wf_ass α"
and ge: "lge_term u (Lab α s)"
shows "∃ v. (u,v) ∈ (qrstep nfs (Lab_lhss_all Q) (Lab_trs R ∪ D))^* ∧ lge_term v (Lab α t)"
using step
proof (induct)
case base
show ?case
by (rule exI[of _ u], rule conjI[OF _ ge], auto)
next
case (step t w)
let ?Q = "(Lab_lhss_all Q)"
let ?R = "qrstep nfs ?Q (Lab_trs R ∪ D)"
from step(3) obtain v where steps: "(u,v) ∈ ?R^*" and lge: "lge_term v (Lab α t)" by auto
from quasi_lab_rewrite[OF D wf step(2) qmodel wfass lge] obtain x y where
more_steps: "(v,x) ∈ (qrstep nfs ?Q D)^*" "(x,y) ∈ qrstep nfs ?Q (Lab_trs R)" and ge: "lge_term y (Lab α w)"
by auto
from steps more_steps have steps: "(u,y) ∈ ?R^* O (qrstep nfs ?Q D)^* O qrstep nfs ?Q (Lab_trs R)" by auto
have steps: "(u,y) ∈ ?R^*"
by (rule set_mp[OF _ steps], unfold qrstep_union, regexp)
with ge show ?case by auto
qed
lemma quasi_lab_relstep:
assumes D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and step: "(s,t) ∈ rel_qrstep (nfs,Q,R,S)"
and qmodel_R: "qmodel I L LC C cge R"
and qmodel_S: "qmodel I L LC C cge S"
and wfass: "wf_ass α"
and ge: "lge_term x (Lab α s)"
shows "∃ v. (x,v) ∈ rel_qrstep (nfs,Lab_lhss_all Q,Lab_trs R, Lab_trs S ∪ D) ∧ lge_term v (Lab α t)"
proof -
let ?Q = "Lab_lhss_all Q"
let ?R = "Lab_trs R"
let ?D = "D"
let ?S = "Lab_trs S"
from step
obtain u v where steps: "(s,u) ∈ (qrstep nfs Q S)^*" "(u,v) ∈ qrstep nfs Q R" "(v,t) ∈ (qrstep nfs Q S)^*"
by auto
from quasi_lab_rewrites[OF D wf steps(1) qmodel_S wfass ge]
obtain u1 where step1: "(x,u1) ∈ (qrstep nfs ?Q (?S ∪ ?D))^*" and ge: "lge_term u1 (Lab α u)"
by auto
from quasi_lab_rewrite[OF D wf steps(2) qmodel_R wfass ge]
obtain v1 v2 where step2: "(u1,v1) ∈ (qrstep nfs ?Q ?D)^*" "(v1,v2) ∈ qrstep nfs ?Q ?R" and ge: "lge_term v2 (Lab α v)"
by auto
from quasi_lab_rewrites[OF D wf steps(3) qmodel_S wfass ge]
obtain t1 where step3: "(v2,t1) ∈ (qrstep nfs ?Q (?S ∪ ?D))^*" and ge: "lge_term t1 (Lab α t)"
by auto
from step1 step2 step3
have step: "(x,t1) ∈ (qrstep nfs ?Q (?S ∪ ?D))^* O (qrstep nfs ?Q ?D)^* O qrstep nfs ?Q ?R O (qrstep nfs ?Q (?S ∪ ?D))^*" by auto
have "(x,t1) ∈ rel_qrstep (nfs, ?Q,?R, ?S ∪ ?D)"
by (rule set_mp[OF _ step], unfold qrstep_union split, regexp)
with ge show ?thesis by auto
qed
end
context
begin
qualified fun aux where
"aux R 0 z = z"
| "aux R (Suc n) z = (SOME lt. R (aux R n z,lt,Suc n))"
end
context sl_interpr
begin
lemma quasi_rel_SN_lab_imp_rel_SN:
assumes D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and LQ: "NF_terms LQ ⊇ NF_terms (Lab_lhss_all Q)"
and SN: "SN_qrel (nfs, LQ,Lab_trs R,Lab_trs S ∪ D)"
and qmodel_R: "qmodel I L LC C cge R"
and qmodel_S: "qmodel I L LC C cge S"
shows "SN_qrel (nfs,Q,R,S)"
unfolding SN_qrel_def split_conv SN_rel_defs
proof
fix f
assume "∀ i. (f i, f (Suc i)) ∈ relto (qrstep nfs Q R) (qrstep nfs Q S)"
hence steps: "⋀ i. (f i, f (Suc i)) ∈ rel_qrstep (nfs,Q,R,S)" by auto
let ?R = "rel_qrstep (nfs,Lab_lhss_all Q, Lab_trs R, Lab_trs S ∪ D)"
obtain g where g: "g = (λi. Semantic_Labeling.aux (λ (r,lt,n). (r,lt) ∈ ?R ∧ lge_term lt (LAB (f n))) i (LAB (f 0)))" by auto
note main = someI_ex[OF quasi_lab_relstep[OF D wf steps qmodel_R qmodel_S wf_default_ass]]
{
fix i
have "(g i, g (Suc i)) ∈ ?R ∧ lge_term (g i) (LAB (f i))" (is "?p i")
proof (induct i)
case 0
from main[of _ 0, OF _ _ lge_term_refl]
show "?p 0" by (auto simp: lge_term_refl g)
next
case (Suc i)
hence ge: "lge_term (g i) (LAB (f i))" by auto
from main[OF _ _ ge]
have ge: "lge_term (g (Suc i)) (LAB (f (Suc i)))" by (auto simp: g)
from main[OF _ _ ge] ge
show ?case by (auto simp: g)
qed
hence "(g i, g (Suc i)) ∈ ?R" by simp
} note steps = this
from steps have "¬ SN ?R" unfolding SN_defs by auto
with SN_subset[OF _ rel_qrstep_mono[OF subset_refl subset_refl LQ]] SN[unfolded SN_qrel_def SN_rel_defs]
show False by auto
qed
abbreviation F_all :: "'lf sig"
where "F_all ≡ {(LC f n l,n) | l f n. LS f n l}"
lemma wf_lab: assumes wf: "wf_ass α"
shows "funas_term (Lab α t) ⊆ F_all"
proof (induct t)
case (Var x)
thus ?case by auto
next
case (Fun f ts)
let ?n = "length ts"
have C: "set (map (Eval α) ts) ⊆ C"
using wf_term[OF wf] by auto
have L: "LS f ?n (L f (map (Eval α) ts))"
using wf_L[unfolded wf_label_def, THEN spec, THEN spec, THEN mp[OF _ C]] by auto
show ?case unfolding eval_lab.simps Let_def o_def snd_conv map_map
using L Fun by force
qed
end
lemma lab_trs_union: "lab_trs I L LC cge (R ∪ S) = lab_trs I L LC cge R ∪ lab_trs I L LC cge S" by auto
context sl_interpr_root
begin
fun lge_term_root :: "('lf,'v)term ⇒ ('lf,'v)term ⇒ bool"
where "lge_term_root (Fun f ts) (Fun g ss) = (length ts = length ss ∧ (∀ i < length ss. lge_term (ts ! i) (ss ! i))
∧ (∃ h lf lg. f = LC h (length ss) lf ∧ g = LC h (length ss) lg ∧ (lf = lg ∨ Ball {lf,lg} (LS' h (length ss)) ∧ lge h (length ss) lf lg)))"
| "lge_term_root (Var x) (Var y) = (x = y)"
| "lge_term_root _ _ = False"
lemma lge_term_root_refl: "lge_term_root (Lab_root α t) (Lab_root α t)"
proof (induct t)
case (Var x) thus ?case by simp
next
case (Fun f ts)
show ?case
by (unfold lge_term_root.simps lab_root.simps map_map o_def snd_conv Let_def length_map, intro conjI,
simp, simp add: lge_term_refl,
intro exI conjI, rule refl, rule refl, simp)
qed
lemma quasi_lab_root_rewrite:
assumes D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and step: "(s,t) ∈ nrqrstep nfs Q R"
and qmodel: "qmodel I L LC C cge R"
and wfass: "wf_ass α"
and ge: "lge_term_root u (Lab_root α s)"
shows "∃ v s'. (u,s') ∈ (nrqrstep nfs (Lab_lhss_all Q) D)^* ∧ (s',v) ∈ nrqrstep nfs (Lab_lhss_all Q) (Lab_trs R) ∧ lge_term_root v (Lab_root α t)"
proof -
let ?Q = "Lab_lhss_all Q"
let ?De = "qrstep nfs ?Q D"
let ?nDe = "nrqrstep nfs ?Q D"
let ?R = "qrstep nfs ?Q (Lab_trs R)"
let ?nR = "nrqrstep nfs ?Q (Lab_trs R)"
from step[unfolded nrqrstep_def]
obtain C' l r σ where lr: "(l,r) ∈ R" and "C' ≠ □" and s: "s = C'⟨l ⋅ σ⟩" and t: "t = C'⟨r ⋅ σ⟩" and
NF: "∀ u ⊲ l ⋅ σ. u ∈ NF_terms Q" and nfs: "NF_subst nfs (l,r) σ Q" by auto
then obtain f D bef aft where C': "C' = More f bef D aft" by (cases C', auto)
let ?si = "D⟨l⋅σ⟩"
let ?ti = "D⟨r⋅σ⟩"
let ?C = "λ t. Fun f (bef @ t # aft)"
from lr NF nfs have step: "(?si, ?ti) ∈ qrstep nfs Q R" by auto
from quasi_sem_rewrite[OF step qmodel wfass]
have cge: "cge (Eval α ?si) (Eval α ?ti)" .
let ?n = "Suc (length bef + length aft)"
let ?m = "length bef"
let ?ls = "λ t. map (Lab α) bef @ Lab α t # map (Lab α) aft"
let ?lsi = "?ls ?si"
let ?lti = "?ls ?ti"
let ?L' = "L' f (map (Eval α) (bef @ D⟨l ⋅ σ⟩ # aft))"
let ?L'' = "L' f (map (Eval α) (bef @ D⟨r ⋅ σ⟩ # aft))"
from C' s t have s: "s = ?C ?si" and t: "t = ?C ?ti" by auto
from ge[unfolded s] obtain g us where u: "u = Fun g us" by (cases u, auto)
from ge[unfolded s u lab_root.simps Let_def lge_term_root.simps map_map o_def]
obtain h lf lg where len: "length us = ?n" and args: "⋀ i. i < ?n ⟹ lge_term (us ! i) (?lsi ! i)"
and g: "g = LC h ?n lf" and id: "LC f ?n ?L' = LC h ?n lg" and disj: "lf = lg ∨ Ball {lf,lg} (LS' h ?n) ∧ lge h ?n lf lg"
by auto
from id have "LD (LC f ?n ?L') = LD (LC h ?n lg)" by auto
from this[unfolded LD_LC] have h: "h = f" and lg: "lg = ?L'" by auto
from args[of ?m] have lge_term: "lge_term (us ! ?m) (Lab α ?si)" by (auto simp: nth_append)
from quasi_lab_rewrite[OF D wf step qmodel wfass lge_term] obtain v s'
where steps: "(us ! ?m, s') ∈ ?De^*" and step: "(s',v) ∈ ?R" and ge: "lge_term v (Lab α D⟨r ⋅ σ⟩)" by auto
let ?lis = "λ t. (take ?m us @ t # drop (Suc ?m) us)"
let ?D = "λ f t. Fun f (?lis t)"
have us: "take ?m us @ us ! ?m # drop (Suc ?m) us = us" (is "?us = us")
by (rule id_take_nth_drop[symmetric], insert len, auto)
hence gus: "Fun g us = Fun g ?us" by simp
from len have m: "?m < length us" by auto
have gus: "Fun g us = Fun g (?lis (us ! ?m))" using id_take_nth_drop[OF m]
by simp
show ?thesis
proof (rule exI[of _ "?D g v"], rule exI[of _ "?D g s'"], unfold u, intro conjI)
show "(?D g s', ?D g v) ∈ ?nR"
by (rule qrstep_imp_ctxt_nrqrstep[OF step])
next
show "(Fun g us, ?D g s') ∈ ?nDe^*"
unfolding gus
by (rule qrsteps_imp_ctxt_nrqrsteps[OF steps])
next
let ?lt = "map (Lab α) (bef @ D⟨r ⋅ σ⟩ # aft)"
have ex: "∃ h lf lg. g = LC h ?n lf ∧ LC f ?n ?L'' = LC h ?n lg ∧ (lf = lg ∨ Ball {lf,lg} (LS' h ?n) ∧ lge h ?n lf lg)"
proof (intro exI conjI, unfold g h, rule refl, rule refl)
{
fix c
assume "c ∈ set ([Eval α ?si, Eval α ?ti] @ map (Eval α) bef @ map (Eval α) aft)"
hence "c ∈ { Eval α u | u. True}" by auto
with wf_term[OF wfass] have "c ∈ C" by blast
} note inC = this
have lge: "lge f ?n ?L' ?L''"
by (simp, rule wm_lge'[unfolded lge_wm, THEN spec, THEN spec[of _ "map (Eval α) bef"], THEN spec, THEN spec,
THEN spec[of _ "map (Eval α) aft"], THEN mp, simplified length_map], rule conjI[OF _ cge], rule subsetI, rule inC, simp)
have L': "LS' f ?n ?L'"
by (simp, rule wf_L'[unfolded wf_label_def, THEN spec, THEN spec[of _ "map (Eval α) (bef @ ?si # aft)"], THEN mp, simplified], auto simp: inC)
have L'': "LS' f ?n ?L''"
by (simp, rule wf_L'[unfolded wf_label_def, THEN spec, THEN spec[of _ "map (Eval α) (bef @ ?ti # aft)"], THEN mp, simplified], auto simp: inC)
show "lf = ?L'' ∨ Ball {lf, ?L''} (LS' f ?n) ∧ lge f ?n lf ?L''"
using disj
proof
assume "lf = lg"
with lg lge L' L'' show ?thesis by auto
next
assume "Ball {lf,lg} (LS' h ?n) ∧ lge h ?n lf lg"
hence lf: "LS' f ?n lf" and ge2: "lge f ?n lf lg" unfolding h by auto
from lge_trans[OF ge2[unfolded lg] lge] L'' lf
show ?thesis by blast
qed
qed
show "lge_term_root (?D g v) (Lab_root α t)"
unfolding t lab_root.simps Let_def map_map o_def lge_term_root.simps
proof (intro conjI, simp add: len, intro allI impI)
fix i
assume i: "i < length ?lt"
show "lge_term (?lis v ! i) (?lt ! i)"
proof (cases "i = ?m")
case True
hence id: "?lis v ! i = v" "?lt ! i = Lab α D⟨r⋅σ⟩" by (auto simp: len nth_append)
show ?thesis unfolding id by (rule ge)
next
case False
have id: "?lis v ! i = us ! i"
by (rule nth_append_take_drop_is_nth_conv, insert False i len, auto)
obtain j where j: "j = i - ?m - 1" by auto
have "i > ?m ⟹ i - ?m = Suc j" unfolding j by auto
hence id2: "?lt ! i = ?lsi ! i" using False by (cases "i > ?m", auto simp: nth_append)
from args[of i] i len have "lge_term (us ! i) (?lsi ! i)" by auto
thus ?thesis unfolding id id2 .
qed
qed (insert ex, auto)
qed
qed
lemma quasi_lab_root_rewrites:
assumes D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and step: "(s,t) ∈ (nrqrstep nfs Q R)^*"
and qmodel: "qmodel I L LC C cge R"
and wfass: "wf_ass α"
and ge: "lge_term_root u (Lab_root α s)"
shows "∃ v . (u,v) ∈ (nrqrstep nfs (Lab_lhss_all Q) (Lab_trs R ∪ D))^* ∧ lge_term_root v (Lab_root α t)"
using step
proof (induct)
case base
show ?case
by (rule exI[of _ u], rule conjI[OF _ ge], auto)
next
case (step t w)
let ?Q = "(Lab_lhss_all Q)"
let ?R = "qrstep nfs ?Q (Lab_trs R ∪ D)"
let ?nR = "nrqrstep nfs ?Q (Lab_trs R ∪ D)"
from step(3) obtain v where steps: "(u,v) ∈ ?nR^*" and lge: "lge_term_root v (Lab_root α t)" by auto
from quasi_lab_root_rewrite[OF D wf step(2) qmodel wfass lge] obtain x y where
more_steps: "(v,x) ∈ (nrqrstep nfs ?Q D)^*" "(x,y) ∈ nrqrstep nfs ?Q (Lab_trs R)" and ge: "lge_term_root y (Lab_root α w)"
by auto
from steps more_steps have steps: "(u,y) ∈ ?nR^* O (nrqrstep nfs ?Q D)^* O nrqrstep nfs ?Q (Lab_trs R)" by auto
have steps: "(u,y) ∈ ?nR^*"
by (rule set_mp[OF _ steps], unfold nrqrstep_union, regexp)
with ge show ?case by auto
qed
lemma lge_term_root_decr:
assumes D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and ge: "lge_term_root u (Lab_root α s)"
and NF: "s ∈ NF_terms Q"
shows "(u,Lab_root α s) ∈ (nrqrstep nfs (Lab_lhss_all Q) D)^* O Decr_root^=" (is "_ ∈ ?D^* O _")
proof (cases s)
case (Var x)
thus ?thesis using ge by (cases u, auto)
next
case (Fun f ss)
let ?Q = "Lab_lhss_all Q"
let ?D' = "qrstep nfs ?Q D"
from ge Fun obtain g us where u: "u = Fun g us" by (cases u, auto simp: Let_def)
note ge = ge[unfolded u lab_root.simps Let_def map_map o_def]
have id: "Lab_root α s = Fun (LC f (length ss) (L' f (map (Eval α) ss))) (map (Lab α) ss)"
(is "_ = Fun ?g ?ss")
by (simp add: Fun Let_def o_def)
note ge = ge[unfolded id]
from ge obtain h lg1 lg2 where len: "length ss = length us" and g: "g = LC h (length ss) lg1" and h: "?g = LC h (length ss) lg2" and disj: "lg1 = lg2 ∨ Ball {lg1,lg2} (LS' h (length ss)) ∧ lge h (length ss) lg1 lg2" by auto
from h have "LD ?g = LD (LC h (length ss) lg2)" by simp
from this[unfolded LD_LC] have h: "h = f" and lg2: "L' f (map (Eval α) ss) = lg2" by auto
{
fix i
assume i: "i < length ss"
from i have mem: "ss ! i ∈ set ss" by auto
from i ge have ge: "lge_term (us ! i) (Lab α (ss ! i))" by auto
have NF1: "∀ t ⊲ ss ! i. t ∈ NF_terms Q"
proof (intro impI allI)
fix t
assume "ss ! i ⊳ t"
with mem have "t ⊲ s" unfolding Fun by auto
with NF_imp_subt_NF[OF NF]
show "t ∈ NF_terms Q" by auto
qed
from lge_term_decr[OF D wf ge NF1] i
have "(us ! i, ?ss ! i) ∈ ?D'^*" by auto
} note args = this
have one: "(Fun g us, Fun g ?ss) ∈ ?D^*"
by (rule args_steps_imp_steps_gen[OF _ _ args],
rule qrsteps_imp_ctxt_nrqrsteps, insert len, auto)
from disj[unfolded h] have "lg1 = lg2 ∨ Ball {lg1, lg2} (LS' f (length ss)) ∧ lge f (length ss) lg1 lg2 ∧ lg1 ≠ lg2"
(is "_ ∨ ?two") by blast
thus ?thesis
proof
assume eq: "lg1 = lg2"
show ?thesis using one unfolding u g eq id h lg2 by auto
next
assume ?two
hence "(lg1,lg2) ∈ gr_root f (length ss)"
unfolding lge_to_lgr_rel_def lge_to_lgr_def Let_def h by auto
hence mem: "(Fun g ?ss, Fun ?g ?ss) ∈ Decr_root" using ‹?two› unfolding g lg2 decr_of_ord_def h by auto
with one show ?thesis unfolding id u by auto
qed
qed
lemma quasi_lab_root_rewrites_qnf:
assumes D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and step: "(s,t) ∈ (nrqrstep nfs Q R)^*"
and qmodel: "qmodel I L LC C cge R"
and wfass: "wf_ass α"
and NF: "t ∈ NF_terms Q"
shows "(Lab_root α s, Lab_root α t) ∈ (nrqrstep nfs (Lab_lhss_all Q) (Lab_trs R ∪ D))^* O Decr_root^="
proof -
let ?Q = "Lab_lhss_all Q"
let ?D = "nrqrstep nfs ?Q D"
let ?RD = "nrqrstep nfs ?Q (Lab_trs R ∪ D)"
from quasi_lab_root_rewrites[OF D wf step qmodel wfass lge_term_root_refl]
obtain v where steps: "(Lab_root α s, v) ∈ ?RD^*" and ge: "lge_term_root v (Lab_root α t)" by auto
from lge_term_root_decr[OF D wf ge NF]
have "(v,Lab_root α t) ∈ ?D^* O Decr_root^=" .
with steps have steps: "(Lab_root α s, Lab_root α t) ∈ ?RD^* O ?D^* O Decr_root^=" by auto
show ?thesis
by (rule set_mp[OF _ steps], unfold nrqrstep_union, regexp)
qed
lemma nrqrstep_Decr_root: "(nrqrstep nfs Q R O Decr_root^=) = (Decr_root^= O nrqrstep nfs Q R)" (is "(?N O ?D^=) = _")
proof -
obtain D where D: "?D^= = D" by auto
obtain N where N: "?N = N" by auto
{
fix s t
assume "(s,t) ∈ ?N O ?D^="
then obtain u where su: "(s,u) ∈ ?N" and ut: "(u,t) ∈ ?D^=" by auto
have "(s,t) ∈ ?D^= O ?N"
proof (cases "u = t")
case True
with su show ?thesis by auto
next
case False
with ut have ut: "(u,t) ∈ ?D" by auto
from su show ?thesis
proof
fix l r C σ
assume nf: "∀ u ⊲ l⋅σ. u ∈ NF_terms Q" and lr: "(l,r) ∈ R"
and C: "C ≠ □" and s: "s = C⟨l⋅σ⟩" and u: "u = 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)
let ?args = "λ t. bef @ D⟨t⟩ # aft"
let ?n = "λ t. length (?args t)"
let ?ts = "?args (r ⋅ σ)"
let ?ss = "?args (l ⋅ σ)"
let ?nts = "?n (r ⋅ σ)"
from ut[unfolded decr_of_ord_def]
obtain g l1 l2 ts where u2: "u = Fun (LC g (length ts) l1) ts" and
t: "t = Fun (LC g (length ts) l2) ts" and
l1: "LS' g (length ts) l1" and
l2: "LS' g (length ts) l2" and
gr: "(l1,l2) ∈ gr_root g (length ts)"
by blast
let ?f1 = "LC g (length ts) l1"
let ?f2 = "LC g (length ts) l2"
from u u2 C have f: "f = ?f1" and ts: "ts = ?ts" by auto
let ?u = "Fun ?f2 ?ss"
have "(s,?u) ∈ ?D" unfolding s C f decr_of_ord_def
using l1 l2 gr
unfolding ts by auto
moreover have "(?u,t) ∈ ?N"
unfolding t ts
proof (rule nrqrstepI[OF nf lr _ _ _ nfs])
have "More ?f2 bef D aft ≠ □" by simp
qed auto
ultimately show ?thesis by auto
qed
qed
}
moreover
{
fix s t
assume "(s,t) ∈ ?D^= O ?N"
then obtain u where su: "(s,u) ∈ ?D^=" and ut: "(u,t) ∈ ?N" by auto
have "(s,t) ∈ ?N O ?D^="
proof (cases "s = u")
case True
with ut show ?thesis by auto
next
case False
with su have su: "(s,u) ∈ ?D" by auto
from ut show ?thesis
proof
fix l r C σ
assume nf: "∀ u ⊲ l⋅σ. u ∈ NF_terms Q" and lr: "(l,r) ∈ R"
and C: "C ≠ □" and u: "u = 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)
let ?args = "λ t. bef @ D⟨t⟩ # aft"
let ?n = "λ t. length (?args t)"
let ?ts = "?args (l ⋅ σ)"
let ?ss = "?args (r ⋅ σ)"
let ?nts = "?n (r ⋅ σ)"
from su[unfolded decr_of_ord_def]
obtain g l1 l2 ts where u2: "u = Fun (LC g (length ts) l2) ts" and
s: "s = Fun (LC g (length ts) l1) ts" and
l1: "LS' g (length ts) l1" and
l2: "LS' g (length ts) l2" and
gr: "(l1,l2) ∈ gr_root g (length ts)"
by blast
let ?f1 = "LC g (length ts) l1"
let ?f2 = "LC g (length ts) l2"
from u u2 C have f: "f = ?f2" and ts: "ts = ?ts" by auto
let ?u = "Fun ?f1 ?ss"
have "(?u,t) ∈ ?D" unfolding t C f decr_of_ord_def
using l1 l2 gr
unfolding ts by auto
moreover have "(s,?u) ∈ ?N"
unfolding s ts
proof (rule nrqrstepI[OF nf lr _ _ _ nfs])
have "More ?f1 bef D aft ≠ □" by simp
qed auto
ultimately show ?thesis by auto
qed
qed
}
ultimately show ?thesis unfolding D N by blast
qed
lemma nrqrsteps_Decr_root:
"((nrqrstep nfs Q R)^* O Decr_root^=) = (Decr_root^= O (nrqrstep nfs Q R)^*)" (is "(?N^* O ?D) = _")
proof -
{
fix n
have "(?N^^n O ?D) = (?D O ?N^^n)"
proof (induct n)
case 0
show ?case by simp
next
case (Suc n)
have "?N^^(Suc n) O ?D = ?N^^n O ?N O ?D"
by auto
also have "... = (?N^^n O ?D) O ?N" unfolding nrqrstep_Decr_root
by blast
also have "... = ?D O (?N^^n O ?N)" unfolding Suc by blast
finally show ?case by auto
qed
} note n = this
thus ?thesis unfolding rtrancl_is_UN_relpow by (auto simp: relcomp.simps, blast+)
qed
lemma quasi_lab_root_steps_qnf:
assumes nvar: "∀(l,r) ∈ (R ∪ S). is_Fun l"
and ndef: "¬ defined (applicable_rules Q (R ∪ S)) (the (root s))"
and D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and steps: "(s,t) ∈ (qrstep nfs Q (R ∪ S))^*"
and qmodel_R: "qmodel I L LC C cge R"
and qmodel_S: "qmodel I L LC C cge S"
and nf: "t ∈ NF_terms Q"
and wfass: "wf_ass α"
shows "(Lab_root α s,Lab_root α t) ∈ Decr_root^= O
(qrstep nfs (Lab_lhss_all Q) (Lab_trs R ∪ Lab_trs S ∪ D))^*"
(is "?st ∈ _")
proof -
let ?Q = "Lab_lhss_all Q"
let ?R = "Lab_trs R"
let ?RS = "Lab_trs R ∪ Lab_trs S"
let ?D = "D"
let ?QD = "nrqrstep nfs ?Q D"
let ?All = "nrqrstep nfs ?Q (?RS ∪ D)"
let ?Lab = "Lab_root α"
from qrsteps_imp_nrqrsteps[OF nvar ndef steps]
have st: "(s,t) ∈ (nrqrstep nfs Q (R ∪ S))^*" .
from qmodel_R qmodel_S have qmodel: "qmodel I L LC C cge (R ∪ S)"
unfolding qmodel_def by auto
from quasi_lab_root_rewrites[OF D wf st qmodel wfass lge_term_root_refl]
obtain t' where st: "(?Lab s, t') ∈ ?All^*"
and t': "lge_term_root t' (?Lab t)" unfolding lab_trs_union by auto
from lge_term_root_decr[OF D wf t' nf]
have tt: "(t', ?Lab t) ∈ ?QD^* O Decr_root^=" by auto
from st tt
have st: "?st ∈ ?All^* O ?QD^* O Decr_root^=" by blast
have st: "?st ∈ ?All^* O Decr_root^="
by (rule set_mp[OF _ st], unfold nrqrstep_union, regexp)
from this[simplified nrqrsteps_Decr_root O_assoc[symmetric]]
have st: "?st ∈ Decr_root^= O ?All^*"
by (simp add: O_assoc)
have "?All ⊆ qrstep nfs ?Q (?RS ∪ D)"
unfolding qrstep_iff_rqrstep_or_nrqrstep by auto
from rtrancl_mono[OF this] st
show ?thesis by blast
qed
lemma quasi_lab_root_relto_qnf:
assumes nvar: "∀(l,r) ∈ (R ∪ S). is_Fun l"
and ndef: "¬ defined (applicable_rules Q (R ∪ S)) (the (root s))"
and D: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and steps: "(s,t) ∈ (qrstep nfs Q (R ∪ S))^* O qrstep nfs Q R O (qrstep nfs Q (R ∪ S))^*"
and qmodel_R: "qmodel I L LC C cge R"
and qmodel_S: "qmodel I L LC C cge S"
and nf: "t ∈ NF_terms Q"
and wfass: "wf_ass α"
shows "(Lab_root α s,Lab_root α t) ∈ Decr_root^= O
(qrstep nfs (Lab_lhss_all Q) (Lab_trs R ∪ Lab_trs S ∪ D))^* O
(qrstep nfs (Lab_lhss_all Q) (Lab_trs R)) O
(qrstep nfs (Lab_lhss_all Q) (Lab_trs R ∪ Lab_trs S ∪ D))^*"
(is "?st ∈ _")
proof -
let ?Q = "Lab_lhss_all Q"
let ?R = "Lab_trs R"
let ?RS = "Lab_trs R ∪ Lab_trs S"
let ?D = "D"
let ?QD = "nrqrstep nfs ?Q D"
let ?QR = "nrqrstep nfs ?Q ?R"
let ?All = "nrqrstep nfs ?Q (?RS ∪ D)"
let ?Lab = "Lab_root α"
from steps
obtain u v where steps: "(s,u) ∈ (qrstep nfs Q (R ∪ S))^*" "(u,v) ∈ qrstep nfs Q R" "(v,t) ∈ (qrstep nfs Q (R ∪ S))^*"
by auto
from qrsteps_imp_nrqrsteps[OF nvar ndef steps(1)]
have su: "(s,u) ∈ (nrqrstep nfs Q (R ∪ S))^*" .
note ndef = ndef[unfolded nrqrsteps_num_args[OF su] nrqrsteps_preserve_root[OF su]]
have uv: "(u,v) ∈ nrqrstep nfs Q R"
by (rule qrstep_imp_nrqrstep[OF _ _ steps(2)], insert nvar ndef, auto simp: applicable_rules_union defined_def)
note ndef = ndef[unfolded nrqrstep_num_args[OF uv] nrqrstep_preserves_root[OF uv]]
from qrsteps_imp_nrqrsteps[OF nvar ndef steps(3)]
have vt: "(v,t) ∈ (nrqrstep nfs Q (R ∪ S))^*" .
from qmodel_R qmodel_S have qmodel: "qmodel I L LC C cge (R ∪ S)"
unfolding qmodel_def by auto
note rewrs = quasi_lab_root_rewrites[OF D wf _ qmodel wfass]
from rewrs[OF _ _ su lge_term_root_refl]
obtain u' where su: "(?Lab s, u') ∈ ?All^*"
and u': "lge_term_root u' (?Lab u)" unfolding lab_trs_union by auto
from quasi_lab_root_rewrite[OF D wf uv qmodel_R wfass u']
obtain u'' v' where uu: "(u',u'') ∈ ?QD^*" and
uv: "(u'',v') ∈ ?QR"
and v': "lge_term_root v' (?Lab v)" by auto
from rewrs[OF _ _ vt v'] obtain t' where
vt: "(v',t') ∈ ?All^*" and
t': "lge_term_root t' (?Lab t)" by auto
from lge_term_root_decr[OF D wf t' nf]
have tt: "(t', ?Lab t) ∈ ?QD^* O Decr_root^=" by auto
from su uu uv vt tt
have st: "?st ∈ ?All^* O ?QD^* O ?QR O ?All^* O ?QD^* O Decr_root^=" by blast
have st: "?st ∈ ?All^* O ?QR O ?All^* O Decr_root^="
by (rule set_mp[OF _ st], unfold nrqrstep_union, regexp)
from this[simplified nrqrsteps_Decr_root nrqrstep_Decr_root O_assoc[symmetric]]
have st: "?st ∈ Decr_root^= O ?All^* O ?QR O ?All^*"
by (simp add: O_assoc)
hence "?st ∈ Decr_root^= O (relto (?QR) (?All))" .
thus ?thesis
using relto_mono[of ?QR "qrstep nfs ?Q ?R" ?All "qrstep nfs ?Q (?RS ∪ D)"]
unfolding qrstep_iff_rqrstep_or_nrqrstep by blast
qed
lemma UNLAB_lab_root: "map_funs_term UNLAB (Lab_root α t) = t"
proof (cases t)
case (Var x) thus ?thesis by auto
next
case (Fun f ts)
show ?thesis unfolding Fun lab_root.simps Let_def term.simps map_map o_def
LD_LC fst_conv using UNLAB_lab[of α]
by (induct ts, auto)
qed
lemma quasi_lab_root_all_merge:
assumes steps: "(Lab_root α (t ⋅ σ),v) ∈ Decr_root^= O Rel"
and tv: "is_Fun t"
and st: "(s,t) ∈ P"
and wfass: "wf_ass α"
shows "∃ lt. (Lab_root (subst_ass α σ) s,lt) ∈ Lab_root_all_trs P ∧
(lt ⋅ lab_subst α σ, v) ∈ Rel ∧ map_funs_term UNLAB (lt ⋅ lab_subst α σ) = t ⋅ σ
∧ ⋃(funas_term ` set (args (lt ⋅ lab_subst α σ))) ⊆ F_all
∧ map_funs_term UNLAB lt = t"
proof -
let ?L = "Lab_root α"
let ?a = "subst_ass α σ"
let ?σ = "lab_subst α σ"
let ?L' = "Lab_root ?a"
let ?D = "Decr_root^="
let ?P = "Lab_root_all_trs P"
let ?m = "map_funs_term UNLAB"
let ?w = "λt. ⋃(funas_term ` set (args t)) ⊆ F_all"
from steps obtain lu where tu: "(?L (t ⋅ σ), lu) ∈ ?D" and uv: "(lu,v) ∈ Rel" by auto
from tv obtain f ts where t: "t = Fun f ts" by force
then obtain tss where tsig: "t ⋅ σ = Fun f tss" and tss: "tss = map (λ t. t ⋅ σ) ts" by auto
let ?ls = "?L' s"
let ?cs = "map (Eval α) tss"
let ?cs' = "map (Eval ?a) ts"
let ?ltss = "map (Lab α) tss"
let ?n = "length tss"
let ?f = "LC f ?n (L' f ?cs)"
let ?lts = "Fun ?f ?ltss"
have ltsig: "?L (t ⋅ σ) = ?lts" unfolding tsig by (auto simp: o_def)
have ltsig': "?L (t ⋅ σ) = ?L' t ⋅ ?σ" unfolding lab_root_subst[OF tv] ..
have wfa: "wf_ass ?a" by (rule wf_ass_subst_ass[OF wfass])
have cs': "set ?cs' ⊆ C"
using wf_term[OF wfa] by auto
have L': "LS' f (length ts) (L' f ?cs')"
by (rule wf_L'[unfolded wf_label_def, THEN spec[of _ f], THEN spec[of _ ?cs'], THEN mp, unfolded length_map], rule cs')
have wftss:"⋀ t. t ∈ set (map (Lab α) tss) ⟹ funas_term t ⊆ F_all"
using wf_lab[OF wfass] by force
show ?thesis
proof (cases "?L (t ⋅ σ) = lu")
assume id: "?L (t ⋅ σ) = lu"
have rel: "(?L' t ⋅ ?σ,v) ∈ Rel"
using uv unfolding ltsig'[symmetric] id by auto
have P: "(?L' s, ?L' t) ∈ ?P"
proof(rule, rule, rule refl, rule st, unfold lab_root_all_rule_def, rule,
intro exI conjI, unfold fst_conv snd_conv, rule refl, rule wfa)
show "?L' t ∈ Lab_root_all ?a t"
unfolding t
by (simp add: o_def, intro exI conjI, rule refl, rule lge_refl, rule L')
qed
show "∃ lt. (?L' s, lt) ∈ ?P ∧ (lt ⋅ ?σ,v) ∈ Rel ∧ ?m (lt ⋅ ?σ) = t ⋅ σ ∧ ?w (lt ⋅ ?σ) ∧ ?m lt = t"
by (intro exI conjI, rule P, rule rel,
unfold ltsig'[symmetric], rule UNLAB_lab_root,
unfold ltsig, insert wftss, force, rule UNLAB_lab_root)
next
assume "?L (t ⋅ σ) ≠ lu"
with tu have "(?L (t ⋅ σ), lu) ∈ Decr_root" by simp
from this[unfolded ltsig decr_of_ord_def]
obtain g l l'
where f: "?f = LC g (length ?ltss) l" and lu: "lu = Fun (LC g (length ?ltss) l') ?ltss" and inLS: "LS' g (length ?ltss) l" "LS' g (length ?ltss) l'"
and gr: "(l,l') ∈ gr_root g (length ?ltss)" by auto
from arg_cong[OF f, of LD, unfolded LD_LC]
have gf: "g = f" and l: "l = L' f ?cs" by auto
have L't: "?L' t = Fun ?f (map (Lab ?a) ts)" unfolding t lab_root.simps Let_def map_map o_def tss by simp
note L't = L't[unfolded f gf tss length_map]
hence L't: "?L' t = Fun (LC f (length ts) l) (map (Lab ?a) ts)"
unfolding l tss .
let ?t = "Fun (LC f (length ts) l') (map (Lab ?a) ts)"
have tu: "?t ⋅ ?σ = lu" unfolding lu tss gf by auto
show "∃ lt. (?L' s, lt) ∈ ?P ∧ (lt ⋅ ?σ,v) ∈ Rel ∧ ?m (lt ⋅ ?σ) = t ⋅ σ ∧ ?w (lt ⋅ ?σ) ∧ ?m lt = t"
proof (rule exI[of _ ?t], intro conjI)
show "(?t ⋅ ?σ,v) ∈ Rel" unfolding tu by (rule uv)
next
show "(?L' s, ?t) ∈ ?P"
proof (rule, rule, rule refl, rule st,
unfold lab_root_all_rule_def, rule,
intro exI conjI, unfold fst_conv snd_conv, rule refl, rule wfa)
show "?t ∈ Lab_root_all ?a t"
unfolding t lab_root_all.simps Let_def
proof (rule, intro exI conjI, unfold map_map o_def, rule refl)
have id: "L' f ?cs' = l" unfolding l tss map_map o_def by auto
show "lge f (length ts) (L' f ?cs') l'" unfolding id
using gr[unfolded gf tss length_map]
unfolding lge_to_lgr_rel_def lge_to_lgr_def Let_def by auto
qed
qed
next
show "?w (?t ⋅ ?σ)"
unfolding tu lu using wftss by force
next
show "?m (?t ⋅ ?σ) = t ⋅ σ"
unfolding tu lu term.simps map_map t tss LD_LC gf fst_conv o_def UNLAB_lab
by auto
next
show "?m ?t = t "
unfolding tu lu term.simps map_map t tss LD_LC gf fst_conv o_def UNLAB_lab
by auto
qed
qed
qed
lemma lab_nf_root:
assumes nf: "s ∈ NF_terms Q"
shows "Lab_root α s ∈ NF_terms (Lab_lhss_all Q)"
proof(rule, rule)
fix t
assume "(Lab_root α s, t) ∈ rstep (Id_on (Lab_lhss_all Q))"
from rstep_imp_map_rstep[OF this, of UNLAB, unfolded UNLAB_lab_root]
have step: "(s, map_funs_term UNLAB t) ∈ rstep (map_funs_trs UNLAB (Id_on (Lab_lhss_all Q)))" (is "?p ∈ rstep ?Q") .
have subset: "?Q ⊆ Id_on Q"
proof -
{
fix l r
assume "(l,r) ∈ ?Q"
then obtain q where "q ∈ Lab_lhss_all Q" and "l = map_funs_term UNLAB q" and "r = map_funs_term UNLAB q"
by (force simp: map_funs_trs.simps)
hence "(l,r) ∈ Id_on Q" by auto
}
thus ?thesis by auto
qed
from rstep_mono[OF subset] step
have "(s, map_funs_term UNLAB t) ∈ rstep (Id_on Q)" by auto
with nf show False
by auto
qed
end
text ‹towards minimality›
context sl_interpr
begin
lemma lab_subst_inj: assumes inj: "⋀ f. inj (L f)"
and x: "x ∈ vars_term t"
and nv: "is_Fun t"
and diff: "α x ≠ α' x"
shows "Lab α t ⋅ σ ≠ Lab α' t ⋅ σ'"
using nv x
proof (induct t)
case (Var y)
thus ?case by auto
next
case (Fun f ts) note oFun = this
from Fun(3) obtain t where t: "t ∈ set ts" and x: "x ∈ vars_term t"
by auto
from t obtain i where i: "i < length ts" and ti: "ts ! i = t"
unfolding set_conv_nth by auto
from id_take_nth_drop[OF i] ti have ts: "Fun f ts = Fun f (take i ts @ t # drop (Suc i) ts)"
by auto
show ?case
proof (cases t)
case (Fun g ss)
hence "is_Fun t" by auto
from oFun(1)[OF t this x]
show ?thesis unfolding ts
by (auto simp: Let_def)
next
case (Var y)
with x have t: "t = Var x" by auto
from i have i: "min (length ts) i = i"
"Suc (i + (length ts - Suc i)) = length ts" by auto
show ?thesis
proof (rule ccontr)
assume eq: "¬ ?thesis"
let ?n = "length ts"
let ?bef = "take i ts"
let ?aft = "drop (Suc i) ts"
from eq have "LC f ?n (L f (map (Eval α) ?bef @ α x # map (Eval α) ?aft)) =
LC f ?n (L f (map (Eval α') ?bef @ α' x # map (Eval α') ?aft))"
(is "LC f ?n ?l = LC f ?n ?r")
by (auto simp: ts t Let_def o_def i)
hence "LD (LC f ?n ?l) = LD (LC f ?n ?r)" by auto
from this[unfolded LD_LC] have eq: "?l = ?r" by simp
with inj[unfolded inj_on_def, THEN bspec, THEN bspec, THEN mp[OF _ eq]] have "α x = α' x" by auto
with diff show False by auto
qed
qed
qed
fun eval_lab_ctxt :: "('v,'c)assign ⇒ 'c ⇒ ('f,'v)ctxt ⇒ ('c × ('lf,'v)ctxt)"
where "eval_lab_ctxt α d Hole = (d, Hole)"
| "eval_lab_ctxt α d (More f bef C' aft) =
(let clbef = map (eval_lab I L LC α) bef;
claft = map (eval_lab I L LC α) aft;
cl = eval_lab_ctxt α d C';
cs = map fst (clbef) @ fst cl # map fst claft;
c = I f cs;
lbef = map snd clbef;
laft = map snd claft in
(c, More (LC f (Suc (length bef + length aft)) (L f cs)) lbef (snd cl) laft))"
lemma eval_ctxt: "Eval α (D⟨t⟩) = fst (eval_lab_ctxt α (Eval α t) D)"
by (induct D, auto simp: Let_def)
lemma lab_ctxt: "Lab α (D⟨t⟩) = (snd (eval_lab_ctxt α (Eval α t) D))⟨Lab α t⟩"
by (induct D, auto simp: Let_def o_def eval_ctxt)
lemma lab_UNLAB:
assumes t: "Lab α t = u"
shows "Lab α (map_funs_term UNLAB u) = u"
proof -
from t have "Lab α (map_funs_term UNLAB (Lab α t)) = Lab α (map_funs_term UNLAB u)"
by simp
from this[unfolded UNLAB_lab, unfolded t] show ?thesis ..
qed
lemma lab_ctxt_split:
assumes "Lab α t = D⟨u⟩"
shows "Lab α (map_funs_term UNLAB u) = u ∧ snd (eval_lab_ctxt α (Eval α (map_funs_term UNLAB u)) (map_funs_ctxt UNLAB D)) = D"
using assms
proof (induct D arbitrary: t)
case Hole
hence "Lab α t = u" by simp
from lab_UNLAB[OF this]
show ?case by simp
next
case (More f bef D aft)
from More(2) obtain g ts where t: "t = Fun g ts" by (cases t, auto)
note More = More[unfolded t]
from More(2)
have f: "f = LC g (length ts) (L g (map (Eval α) ts))"
and ts: "map (Lab α) ts = bef @ D⟨u⟩ # aft" (is "?ts = ?bua")
by (auto simp: Let_def o_def)
from arg_cong[OF ts,of length]
have len: "length ts = Suc (length bef + length aft)" by auto
note ts' = ts[unfolded list_eq_iff_nth_eq, THEN conjunct2, THEN spec, THEN mp, unfolded length_map]
let ?m = "length bef"
from len have m: "?m < length ts" by auto
from arg_cong[OF ts, of "λ x. x ! ?m"] m
have tu: "Lab α (ts ! ?m) = D⟨u⟩" by auto
from More(1)[OF this] have one: "Lab α (map_funs_term UNLAB u) = u"
and two: "snd (eval_lab_ctxt α (Eval α (map_funs_term UNLAB u)) (map_funs_ctxt UNLAB D)) = D" by auto
let ?map = "map (λ x. Lab α (map_funs_term UNLAB x))"
have bef: "?map bef = bef"
proof (rule nth_equalityI, simp, unfold length_map, intro allI impI)
fix i
assume i: "i < ?m"
with len have i': "i < length ts" by auto
have "?map bef ! i = Lab α (map_funs_term UNLAB (bef ! i))" using i by auto
also have "... = bef ! i"
proof (rule lab_UNLAB)
show "Lab α (ts ! i) = bef ! i"
using ts'[OF i'] i' i
by (auto simp: nth_append)
qed
finally show "?map bef ! i = bef ! i" .
qed
have aft: "?map aft = aft"
proof (rule nth_equalityI, simp, unfold length_map, intro allI impI)
fix i
assume i: "i < length aft"
let ?i = "Suc (?m + i)"
from i len have i': "?i < length ts" by auto
have "?map aft ! i = Lab α (map_funs_term UNLAB (aft ! i))" using i by auto
also have "... = aft ! i"
proof (rule lab_UNLAB)
show "Lab α (ts ! ?i) = aft ! i"
using ts'[OF i'] i' i
by (auto simp: nth_append)
qed
finally show "?map aft ! i = aft ! i" .
qed
show ?case
proof (rule conjI[OF one], simp add: Let_def o_def two bef aft)
let ?n = "Suc (?m + length aft)"
let ?ma = "map (λ x. Eval α (map_funs_term UNLAB x))"
let ?ctxt = "eval_lab_ctxt α (Eval α (map_funs_term UNLAB u)) (map_funs_ctxt UNLAB D)"
let ?cs = "?ma bef @ fst ?ctxt # ?ma aft"
have ld_f: "LD f = (UNLAB f, snd (LD f))" by simp
with arg_cong[OF f, of LD, unfolded LD_LC] have
g: "UNLAB f = g" and Lg: "L g (map (Eval α) ts) = snd (LD f)" by auto
show "LC (UNLAB f) ?n (L (UNLAB f) ?cs) = f" unfolding g
unfolding f len
proof (rule arg_cong[where f = "LC g ?n"], rule arg_cong[where f = "L g"])
{
fix i
assume i: "i < ?n"
hence i': "i < length (bef @ D⟨u⟩ # aft)" by simp
from ts have ts': "map (Eval α) (map (map_funs_term UNLAB) ?ts) ! i
= map (Eval α) (map (map_funs_term UNLAB) ?bua) ! i" (is "?l = ?r") by simp from i have "map (Eval α) ts ! i = ?l" using len
by (simp add: UNLAB_lab)
also have "... = Eval α (map_funs_term UNLAB (?bua ! i))" unfolding ts'
unfolding map_map
unfolding nth_map[OF i'] by (simp add: o_def)
also have "... = ?cs ! i"
proof (cases "i < ?m")
case True
thus ?thesis
by (auto simp: nth_append)
next
case False
show ?thesis
proof (cases "i - ?m")
case (Suc j)
with i have "j < length aft" by auto
with Suc show ?thesis using False
by (auto simp: nth_append)
next
case 0
with False have i: "i = ?m" by simp
show ?thesis unfolding i
by (simp add: nth_append eval_ctxt)
qed
qed
finally
have "?cs ! i = map (Eval α) ts ! i" by simp
} note main = this
show "?cs = map (Eval α) ts"
by (rule nth_equalityI, insert main len, auto)
qed
qed
qed
lemma lab_nf_rev:
assumes nf: "Lab α s ∈ NF_terms (Lab_lhss Q)" and wf: "wf_ass α"
shows "s ∈ NF_terms Q"
unfolding NF_ctxt_subst
proof(rule,rule)
assume "∃ C q σ. s = C⟨q ⋅ σ⟩ ∧ q ∈ Q"
then obtain C q σ where s: "s = C⟨q⋅σ⟩" and q: "q ∈ Q" by auto
let ?σ = "lab_subst α σ"
let ?q = "Lab (subst_ass α σ) q"
let ?Q = "Lab_lhss Q"
obtain D where D: "Lab α s = D⟨?q⋅?σ⟩" unfolding s
unfolding lab_ctxt by auto
have q: "?q ∈ ?Q"
by (auto simp: lab_lhs_def, rule bexI[OF _ q], rule exI[of _ "subst_ass α σ"], auto simp: wf)
have "Lab α s ∉ NF_terms ?Q"
unfolding D NF_ctxt_subst
using q by auto
thus False using nf by auto
qed
end
lemma eval_lab_independent:
fixes t::"('f,'v)term" and I::"('f,'c)inter"
assumes "∀x∈vars_term t. α x = β x"
shows "eval_lab I L LC α t = eval_lab I L LC β t"
using assms
proof (induct t, simp)
case (Fun f ts)
hence map: "map (eval_lab I L LC α) ts = map (eval_lab I L LC β) ts" by auto
thus ?case by (auto simp: Let_def map)
qed
lemma lab_root_independent:
fixes t::"('f,'v)term" and I::"('f,'c)inter"
assumes vars: "∀x∈vars_term t. α x = β x"
shows "lab_root I L L' LC α t = lab_root I L L' LC β t"
proof (cases t, simp)
case (Fun f ts)
from vars[unfolded Fun] have vars: "⋀ t . t ∈ set ts ⟹ (∀ x ∈ vars_term t. α x = β x)" by auto
from eval_lab_independent[OF vars]
have map: "map (eval_lab I L LC α) ts = map (eval_lab I L LC β) ts" by auto
show ?thesis unfolding Fun by (auto simp: Let_def map)
qed
context sl_interpr
begin
lemma inj_step: assumes inj: "⋀ f. inj (L f)"
and step: "(Lab α t,u) ∈ qrstep nfs (Lab_lhss Q) (Lab_trs R)"
and wwf: "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q R"
and SN: "¬ SN_on (qrstep nfs Q R) {t} ⟹ wwf_qtrs Q R"
and model: "qmodel I L LC C cge R"
and cge: "cge = (op =)"
and wf: "wf_ass α"
shows "∃ s. (t,s) ∈ qrstep nfs Q R ∧ u = Lab α s"
proof -
from wwf_qtrs_imp_nfs_False_switch[OF wwf] have switch: "qrstep nfs Q R = qrstep False Q R" by blast
from step obtain C σ ll lr where id: "Lab α t = C⟨ll⋅σ⟩" "u = C⟨lr⋅σ⟩" and llr: "(ll,lr) ∈ Lab_trs R" and NF: "∀ u ⊲ ll ⋅ σ. u ∈ NF_terms (Lab_lhss Q)" by (induct, auto)
from llr obtain l r β where lr: "(l,r) ∈ R" and llr: "ll = Lab β l" "lr = Lab β r" and beta: "wf_ass β" by (force simp: lab_rule_def)
note id1 = lab_ctxt_split[OF id(1), unfolded llr]
let ?C = "snd (eval_lab_ctxt α (Eval α (map_funs_term UNLAB (Lab β l ⋅ σ))) (map_funs_ctxt UNLAB C))"
let ?σ = "map_funs_subst UNLAB σ"
have nf: "∀ u ⊲ l ⋅ ?σ. u ∈ NF_terms Q"
proof (intro allI impI)
fix u
assume u: "l ⋅ ?σ ⊳ u"
then obtain D where D: "D ≠ □" and u: "l ⋅ ?σ = D⟨u⟩" by (rule supt_ctxtE)
show "u ∈ NF_terms Q"
proof (rule lab_nf_rev, rule NF[THEN spec, THEN mp], unfold llr)
let ?D = "snd (eval_lab_ctxt α (Eval α u) D)"
show "Lab β l ⋅ σ ⊳ Lab α u"
proof (rule ctxt_supt)
have "Lab β l ⋅ σ = Lab α (l ⋅ ?σ)"
using id1 by (auto simp: UNLAB_lab)
also have "... = Lab α (D⟨u⟩)" unfolding u ..
also have "... = ?D⟨Lab α u⟩" (is "_ = ?r") unfolding lab_ctxt ..
finally show "Lab β l ⋅ σ = ?r" .
next
from D show "?D ≠ □" by (cases D, auto simp: Let_def)
qed
next
show "wf_ass α" by (rule wf)
qed
qed
have "(map_funs_term UNLAB (Lab α t), map_funs_term UNLAB u) ∈ qrstep nfs Q R" unfolding switch
proof (rule qrstepI[OF _ lr], unfold id llr map_funs_term_ctxt_distrib map_funs_subst_distrib UNLAB_lab)
show "(map_funs_ctxt UNLAB C)⟨l ⋅ ?σ⟩ = (map_funs_ctxt UNLAB C)⟨l ⋅ ?σ⟩" ..
next
show "∀u⊲l ⋅ map_funs_subst UNLAB σ. u ∈ NF_terms Q" by (rule nf)
qed auto
hence step: "(t, map_funs_term UNLAB u) ∈ qrstep nfs Q R" unfolding UNLAB_lab .
have wwf: "wwf_rule Q (l,r)"
proof (cases "wwf_qtrs Q R")
case True
with lr show ?thesis unfolding wwf_qtrs_def wwf_rule_def by auto
next
case False
from False SN have "SN_on (qrstep nfs Q R) {t}" by auto
hence SN: "SN_on (qrstep False Q R) {t}" unfolding switch by auto
show ?thesis
by (rule SN_on_imp_wwf_rule[OF SN _ lr nf, unfolded arg_cong[OF id(1), of "map_funs_term UNLAB", unfolded UNLAB_lab]], unfold llr, auto simp: UNLAB_lab)
qed
show ?thesis
proof (intro exI conjI, rule step, unfold id llr)
show "C⟨Lab β r ⋅ σ⟩ = Lab α (map_funs_term UNLAB C⟨Lab β r ⋅ σ⟩)"
proof -
let ?D = "snd (eval_lab_ctxt α (Eval α (map_funs_term UNLAB (Lab β r ⋅ σ))) (map_funs_ctxt UNLAB C))"
from model[unfolded qmodel_def, THEN bspec[OF _ lr], unfolded split cge]
have eval: "⋀ α. wf_ass α ⟹ Eval α l = Eval α r" by simp
have CD: "?C = ?D"
by (rule arg_cong[where f = "λx. snd (eval_lab_ctxt α x (map_funs_ctxt UNLAB C))"], unfold map_funs_subst_distrib eval_subst UNLAB_lab, rule eval, simp add: wf)
have "Lab α (map_funs_term UNLAB C⟨Lab β r ⋅ σ⟩) = Lab α ((map_funs_ctxt UNLAB C) ⟨r ⋅ ?σ⟩)"
unfolding map_funs_term_ctxt_distrib map_funs_subst_distrib UNLAB_lab by simp
also have "... = ?D⟨Lab α (r ⋅ ?σ)⟩" unfolding lab_ctxt
unfolding map_funs_subst_distrib UNLAB_lab ..
also have "... = ?C⟨Lab α (r ⋅ ?σ)⟩" unfolding CD ..
also have "... = C⟨Lab α (r ⋅ ?σ)⟩" using id1 by simp
also have "... = C⟨Lab β r ⋅ σ⟩"
unfolding ctxt_eq lab_subst
proof -
let ?α = "subst_ass α ?σ"
let ?τ = "lab_subst α ?σ"
from id1 have idl: "Lab ?α l ⋅ ?τ = Lab β l ⋅ σ"
by (simp add: UNLAB_lab)
from wwf[unfolded wwf_rule_def, THEN mp[OF _ only_applicable_rules[OF nf]]]
have nvar: "is_Fun l" and rl: "vars_term r ⊆ vars_term l" by auto
{
fix x
assume x: "x ∈ vars_term l"
have "?α x = β x"
using lab_subst_inj[OF inj x nvar, of ?α β ?τ σ] idl
by auto
} note alpha_beta = this
hence abl: "∀ x ∈ vars_term l. ?α x = β x" by auto
hence abr: "∀ x ∈ vars_term r. ?α x = β x" using rl by auto
from eval_lab_independent[OF abl, of I L LC]
have l: "Lab ?α l = Lab β l" by simp
from eval_lab_independent[OF abr, of I L LC]
have r: "Lab ?α r = Lab β r" by simp
show "Lab ?α r ⋅ ?τ = Lab β r ⋅ σ" unfolding r
by (rule vars_term_subset_subst_eq [OF _ idl [unfolded l]], unfold vars_term_lab,
rule rl)
qed
finally show ?thesis by simp
qed
qed
qed
lemma SN_inj:
assumes inj: "⋀ f. inj (L f)"
and wwf: "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q R"
and SN: "SN_on (qrstep nfs Q R) {t}"
and model: "qmodel I L LC C cge R"
and cge: "cge = (op =)"
and wf: "wf_ass α"
and LQ: "NF_terms (Lab_lhss Q) ⊇ NF_terms LQ"
shows "SN_on (qrstep nfs LQ (Lab_trs R)) {Lab α t}"
proof -
let ?QR = "qrstep nfs (Lab_lhss Q) (Lab_trs R)"
{
fix f
assume f0: "f 0 = Lab α t" and "∀ i. (f i, f (Suc i)) ∈ ?QR"
hence steps: "⋀ i. (f i, f (Suc i)) ∈ ?QR" by auto
note main = inj_step[OF inj _ wwf _ model cge wf]
obtain g where g: "g = (λ n. Semantic_Labeling.aux (λ (pt,t,i). ((pt,t) ∈ qrstep nfs Q R ∧ f i = Lab α t)) n t)" by auto
{
fix i
have "(i > 0 ⟶ (g (i - 1), g i) ∈ qrstep nfs Q R) ∧ Lab α (g i) = f i ∧ SN_on (qrstep nfs Q R) {g i}"
proof (induct i)
case 0
show ?case by (auto simp: f0 g SN)
next
case (Suc i)
hence id: "f i = Lab α (g i)" and SN: "SN_on (qrstep nfs Q R) {g i}" by auto
from someI_ex[OF main[OF steps[of i, unfolded id] ]] SN
have gsi: "(g i, g (Suc i)) ∈ qrstep nfs Q R" and fsi: "f (Suc i) = Lab α (g (Suc i))"
unfolding g aux.simps by auto
from step_preserves_SN_on[OF gsi SN] gsi fsi
show ?case by auto
qed
hence "i > 0 ⟶ (g (i - 1), g i) ∈ qrstep nfs Q R" by simp
}
hence "⋀ i. (g i, g (Suc i)) ∈ qrstep nfs Q R" by force
hence "¬ SN_on (qrstep nfs Q R) {g 0}" by auto
with SN have False unfolding g by auto
}
hence SN: "SN_on ?QR {Lab α t}" unfolding SN_on_def by blast
show ?thesis
by (rule SN_on_subset1[OF SN qrstep_mono[OF _ LQ]], auto)
qed
end
context sl_interpr
begin
definition Lab_all_trs :: "('f,'v)trs ⇒ ('lf,'v)trs"
where "Lab_all_trs R ≡ {(l,r) | l r. funas_term r ⊆ F_all ∧ (map_funs_term UNLAB l, map_funs_term UNLAB r) ∈ R}"
definition Lab_lhss_more :: "('f,'v)terms ⇒ ('lf,'v)terms"
where "Lab_lhss_more Q ≡ { l. funas_term l ⊆ F_all ∧ map_funs_term UNLAB l ∈ Q}"
lemma Lab_lhss_more: "Lab_lhss Q ⊆ Lab_lhss_more Q" "Lab_lhss_more Q ⊆ Lab_lhss_all Q"
proof -
show "Lab_lhss Q ⊆ Lab_lhss_more Q"
proof
fix x
assume "x ∈ Lab_lhss Q"
then obtain q where q: "q ∈ Q" and x: "x ∈ lab_lhs I L LC C q" by auto
then obtain a where x: "x = Lab a q" and a: "wf_ass a" unfolding lab_lhs_def by auto
show "x ∈ Lab_lhss_more Q" unfolding x Lab_lhss_more_def using wf_lab[OF a, of q] UNLAB_lab[of a q] q by auto
qed
next
show "Lab_lhss_more Q ⊆ Lab_lhss_all Q" unfolding Lab_lhss_more_def by auto
qed
lemma NF_unlab: assumes NF: "s ∈ NF_terms LQ"
and wf: "funas_term s ⊆ F_all"
and LQ: "NF_terms (Lab_lhss_more Q) ⊇ NF_terms LQ"
and Q: "⋀ q. q ∈ Q ⟹ linear_term q"
shows "map_funs_term UNLAB s ∈ NF_terms Q"
proof -
let ?m = "map_funs_term UNLAB"
let ?LQ = "Lab_lhss_more Q"
from LQ NF have NF: "s ∈ NF_terms ?LQ" by auto
show ?thesis
proof (rule ccontr)
assume "?m s ∉ NF_terms Q"
thus False
proof (rule not_NF_termsE)
fix q C σ
assume q: "q ∈ Q" and m: "?m s = C⟨q ⋅ σ⟩"
from Q[OF q] have lin: "linear_term q" by auto
from map_funs_term_ctxt_decomp[OF m] obtain D u where C: "C = map_funs_ctxt UNLAB D"
and qσ: "?m u = q ⋅ σ" and s: "s = D⟨u⟩" by auto
from map_funs_subst_split[OF qσ lin]
obtain t τ where u: "u = t ⋅ τ" and qt: "q = ?m t" and vars: "⋀ x. x ∈ vars_term q ⟹ ?m (τ x) = σ x" by auto
note NF = NF[unfolded s u]
note wf = wf[unfolded s u]
from wf q qt
have "t ∈ ?LQ" unfolding funas_term_ctxt_apply funas_term_subst unfolding Lab_lhss_more_def by auto
with NF show False by auto
qed
qed
qed
lemma wf_Lab_all_trs: assumes "(l,r) ∈ Lab_all_trs R"
shows "funas_term r ⊆ F_all"
using assms
unfolding Lab_all_trs_def by auto
lemma wf_Decr:
assumes wf: "funas_term lt ⊆ F_all"
and d: "(lt,ls) ∈ qrstep nfs Q Decr"
shows "funas_term ls ⊆ F_all"
using d
proof
fix C σ l r
assume d: "(l,r) ∈ Decr" and lt: "lt = C⟨l⋅σ⟩" and ls: "ls = C⟨r ⋅ σ⟩"
from d[unfolded decr_of_ord_def] obtain f l1 l2 ts where
l: "l = Fun (LC f (length ts) l1) ts" and r: "r = Fun (LC f (length ts) l2) ts"
and l2: "LS f (length ts) l2" by auto
hence vars: "vars_term l = vars_term r" by auto
show ?thesis using wf unfolding ls lt unfolding funas_term_ctxt_apply funas_term_subst vars
unfolding l r using l2 by auto
qed
lemma wf_Decr_args:
assumes wf: "⋃(funas_term ` set (args lt)) ⊆ F_all"
and d: "(lt,ls) ∈ qrstep nfs Q Decr"
shows "⋃(funas_term ` set (args ls)) ⊆ F_all"
using d
proof
fix C σ l r
assume d: "(l,r) ∈ Decr" and lt: "lt = C⟨l⋅σ⟩" and ls: "ls = C⟨r ⋅ σ⟩"
and NF: "∀ u ⊲ l⋅σ. u ∈ NF_terms Q"
from d[unfolded decr_of_ord_def] obtain f l1 l2 ts where
l: "l = Fun (LC f (length ts) l1) ts" and r: "r = Fun (LC f (length ts) l2) ts"
and l2: "LS f (length ts) l2" by auto
hence vars: "vars_term l = vars_term r" by auto
show "⋃(funas_term ` set (args ls)) ⊆ F_all"
proof (cases C)
case Hole
show ?thesis using wf unfolding ls lt Hole l r by auto
next
case (More g bef D aft)
from wf have "funas_term (D⟨l⋅σ⟩) ⊆ F_all" unfolding lt More by auto
hence "funas_term (D⟨r⋅σ⟩) ⊆ F_all" unfolding funas_term_ctxt_apply funas_term_subst vars
unfolding l r using l2 by auto
thus ?thesis using wf unfolding ls lt More by auto
qed
qed
lemma step_imp_UNLAB_step: assumes LR: "LR ⊆ Lab_all_trs R"
and lin: "⋀ q. q ∈ Q ⟹ linear_term q"
and wfs: "⋃(funas_term ` set (args s)) ⊆ F_all"
and wf: "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q R"
and SN: "¬ SN_on (qrstep nfs Q R) {map_funs_term UNLAB s} ⟹ wwf_qtrs Q R"
and LQ: "NF_terms (Lab_lhss_more Q) ⊇ NF_terms LQ"
and step: "(s,t) ∈ qrstep nfs LQ LR"
shows "(map_funs_term UNLAB s, map_funs_term UNLAB t) ∈ qrstep nfs Q R ∧ ⋃(funas_term ` set (args t)) ⊆ F_all ∧ (funas_term s ⊆ F_all ⟶ funas_term t ⊆ F_all)"
proof -
from wwf_qtrs_imp_nfs_False_switch[OF wf] have switch: "qrstep nfs Q R = qrstep False Q R" by blast
let ?Q = "Lab_lhss_more Q"
let ?m = "map_funs_term UNLAB"
from qrstep_mono[OF LR LQ] step
have "(s,t) ∈ qrstep nfs ?Q (Lab_all_trs R)" by auto
from this[unfolded qrstep_rule_conv[where R = "Lab_all_trs R"]]
obtain l r where lr: "(l,r) ∈ Lab_all_trs R" and step: "(s,t) ∈ qrstep nfs ?Q {(l,r)}" by auto
from step obtain C σ where s: "s = C⟨l⋅σ⟩" and t: "t = C⟨r⋅σ⟩" and NF: "∀ u ⊲ l ⋅ σ. u ∈ NF_terms ?Q"
and nfs: "NF_subst nfs (l,r) σ ?Q" by auto
have mlr: "(?m l, ?m r) ∈ R" "(?m l, ?m r) ∈ {(?m l, ?m r)}" using lr[unfolded Lab_all_trs_def] by auto
have mnf: "∀u⊲map_funs_term UNLAB l ⋅ map_funs_subst UNLAB σ. u ∈ NF_terms Q" unfolding map_funs_subst_distrib[symmetric]
proof (intro allI impI)
fix u
assume "?m (l ⋅ σ) ⊳ u"
thus "u ∈ NF_terms Q"
proof
fix D
assume D: "D ≠ □" and mls: "?m (l ⋅ σ) = D⟨u⟩"
from map_funs_term_ctxt_decomp[OF mls] obtain E v where DE: "D = map_funs_ctxt UNLAB E"
and u: "u = ?m v" and lσ: "l ⋅ σ = E⟨v⟩" by auto
from D DE have E: "E ≠ □" by (cases E, auto)
obtain CE where CE: "CE = C ∘⇩c E" by auto
have sCEv: "s = CE⟨v⟩" unfolding CE s lσ by auto
obtain f bef E' aft where CE: "CE = More f bef E' aft"
using E unfolding CE by (cases C, cases E, auto)
have "E'⟨v⟩ ∈ set (args s)" unfolding sCEv CE by auto
hence "funas_term (E'⟨v⟩) ⊆ F_all" using wfs by blast
hence vwf: "funas_term v ⊆ F_all" by auto
show "u ∈ NF_terms Q"
unfolding u
proof (rule NF_unlab[OF _ vwf subset_refl lin])
show "v ∈ NF_terms ?Q"
using NF[unfolded lσ] E by auto
qed
qed
qed
have ustep: "(?m s, ?m t) ∈ qrstep False Q ({(?m l, ?m r)})" unfolding s t map_funs_term_ctxt_distrib map_funs_subst_distrib
by (rule qrstepI[OF mnf mlr(2) refl refl], simp)
have "wf_rule (?m l, ?m r)"
proof (cases "SN_on (qrstep nfs Q R) {?m s}")
case True
from SN_on_imp_qrstep_wf_rules[OF SN_on_subset1[OF True[unfolded switch] qrstep_mono] ustep]
have "(?m s, ?m t) ∈ qrstep False Q (wf_rules {(?m l, ?m r)})"
using mlr by auto
hence "wf_rules {(?m l, ?m r)} ≠ {}" by auto
thus "wf_rule (?m l, ?m r)" unfolding wf_rules_def by auto
next
case False
from SN[OF this] have "wwf_qtrs Q R" by auto
from this[unfolded wwf_qtrs_wwf_rules] mlr(1) have "wwf_rule Q (?m l,?m r)" by auto
moreover have "applicable_rule Q (?m l, ?m r)"
by (rule only_applicable_rules[OF mnf])
ultimately show ?thesis unfolding wwf_rule_def wf_rule_def by blast
qed
hence vars: "vars_term r ⊆ vars_term l" and nvar: "is_Fun l"
unfolding wf_rule_def snd_conv fst_conv using vars_term_map_funs_term
by auto
{
assume wfs: "funas_term s ⊆ F_all"
have wf: "funas_term t ⊆ F_all"
by (rule qrstep_preserves_funas_terms[OF wf_Lab_all_trs[OF lr] wfs step vars])
} note wfst = this
from nvar obtain f ls where l: "l = Fun f ls" by (cases l, auto)
have wfr: "funas_term r ⊆ F_all" using lr LR unfolding Lab_all_trs_def by auto
{
fix x
assume "x ∈ vars_term r"
with vars have x: "x ∈ vars_term l" by auto
have "funas_term (σ x) ⊆ F_all"
proof (cases C)
case (More f bef D aft)
from s[unfolded More] have "D⟨l⋅σ⟩ ∈ set (args s)" by auto
with wfs have "funas_term (D⟨l⋅σ⟩) ⊆ F_all" by blast
thus ?thesis using x unfolding funas_term_ctxt_apply funas_term_subst by force
next
case Hole
from x obtain l' where l': "l' ∈ set ls" and x: "x ∈ vars_term l'" unfolding l by auto
from s[unfolded Hole] l l' have "l' ⋅ σ ∈ set (args s)" by auto
hence "funas_term (l' ⋅ σ) ⊆ F_all" using wfs by auto
with x show ?thesis unfolding funas_term_subst by auto
qed
}
with wfr
have wfrσ: "funas_term (r ⋅ σ) ⊆ F_all"
unfolding funas_term_subst by blast
have wft: "⋃(funas_term ` set (args t)) ⊆ F_all"
proof (cases C)
case Hole
show ?thesis unfolding t Hole using wfrσ funas_term_args by force
next
case (More f bef D aft)
{
fix u
assume "u ∈ set (args (More f bef D aft)⟨r ⋅ σ⟩)"
hence "u ∈ set bef ∪ set aft ∨ u = D⟨r⋅σ⟩" by auto
hence "funas_term u ⊆ F_all"
proof
assume u: "u = D⟨r ⋅ σ⟩"
from wfs[unfolded s More] have "funas_term (D⟨l⋅σ⟩) ⊆ F_all" by auto
thus ?thesis using wfrσ unfolding u by auto
next
assume "u ∈ set bef ∪ set aft"
with wfs[unfolded s More] show ?thesis by auto
qed
}
thus ?thesis unfolding t More by blast
qed
have "(?m s, ?m t) ∈ qrstep False Q R"
using set_mp[OF qrstep_mono[OF _ subset_refl] ustep, of R] mlr(1) by auto
with wft wfst show ?thesis unfolding switch by auto
qed
lemma Decr_UNLAB: "map_funs_trs UNLAB Decr ⊆ Id"
unfolding map_funs_trs.simps decr_of_ord_def using LD_LC by auto
lemma map_funs_term_Decr:
assumes step: "(s,t) ∈ qrstep nfs Q Decr"
shows "map_funs_term UNLAB s = map_funs_term UNLAB t"
proof -
from qrstep_imp_map_rstep[OF step, of UNLAB]
rstep_mono[OF Decr_UNLAB] rstep_id
show ?thesis by auto
qed
lemma SN_on_UNLAB_imp_SN_on: assumes LR: "LR ⊆ Lab_all_trs R"
and lin: "⋀ q. q ∈ Q ⟹ linear_term q"
and wfs: "⋃(funas_term ` set (args s)) ⊆ F_all"
and wwf: "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q R"
and SN: "SN_on (qrstep nfs Q R) {map_funs_term UNLAB s}"
and LQ: "NF_terms (Lab_lhss_more Q) ⊇ NF_terms LQ"
shows "SN_on (qrstep nfs LQ (LR ∪ Decr)) {s}"
proof
fix f
assume f: "f 0 ∈ {s}" and steps: "∀ i. (f i, f (Suc i)) ∈ qrstep nfs LQ (LR ∪ Decr)"
let ?r = "qrstep nfs Q R"
let ?B = "qrstep nfs LQ LR ∪ qrstep nfs LQ Decr"
let ?R = "qrstep nfs LQ LR"
let ?D = "qrstep nfs LQ Decr"
let ?m = "λi. map_funs_term UNLAB (f i)"
let ?w = "λt. ⋃(funas_term ` set (args t)) ⊆ F_all"
let ?SN = "λx. SN_on ?r {x}"
let ?f = "λ i. (f i, f (Suc i))"
from steps have steps: "⋀ i. ?f i ∈ ?B" unfolding qrstep_union by auto
show False
proof (cases "∀ i. (∃ j ≥ i. ?f j ∈ ?R)")
case False
then obtain i where n: "⋀ j. j ≥ i ⟹ ?f j ∉ ?R" by auto
obtain g where g: "g = (λ j. f (j + i))" by auto
{
fix j
have "(g j, g (Suc j)) ∈ ?D" using steps[of "j + i"] n[of "j + i"]
unfolding g by auto
}
hence "¬ SN ?D" unfolding SN_defs by blast
with SN_subset[OF Decr_SN, of "qrstep nfs LQ Decr"] show False by auto
next
case True
let ?p = "λ i. ?f i ∈ ?R"
{
fix i
have "?w (f i) ∧ ?SN (?m i) ∧ (i > 0 ⟶ ((?p (i - 1) ⟶ (?m (i - 1), ?m i) ∈ ?r)) ∧ (¬ ?p (i - 1) ⟶ ?m i = ?m (i - 1)))"
proof (induct i)
case 0
show ?case unfolding singletonD[OF f] using wfs SN by auto
next
case (Suc i)
hence wf: "?w (f i)" and SN: "?SN (?m i)" by auto
show ?case
proof (cases "?p i")
case True
from step_imp_UNLAB_step[OF LR lin wf wwf _ LQ True]
show ?thesis using step_preserves_SN_on[OF _ SN] True SN by auto
next
case False
with steps[of i] have step: "?f i ∈ ?D" by auto
from wf_Decr_args[OF wf step] have wf: "?w (f (Suc i))" by auto
from map_funs_term_Decr[OF step] have "?m i = ?m (Suc i)" .
thus ?thesis using wf SN False by auto
qed
qed
} note main = this
{
fix i
assume "?p i"
with main[of "Suc i"] have "(?m i, ?m (Suc i)) ∈ ?r" by simp
} note p = this
{
fix i
assume "¬ ?p i"
with main[of "Suc i"] have "?m (Suc i) = ?m i" by simp
} note np = this
obtain p where p': "p = ?p" by auto
from p p' have p: "⋀ i. p i ⟹ (?m i, ?m (Suc i)) ∈ ?r" by auto
from np p' have np: "⋀ i. ¬ p i ⟹ ?m (Suc i) = ?m i" by auto
interpret infinitely_many p unfolding p'
by (unfold_locales, unfold INFM_nat_le, rule True)
obtain g where g: "g = (λ i. ?m (index i))" by auto
{
fix i
from p[OF index_p, of i]
have "(g i, ?m (Suc (index i))) ∈ ?r" unfolding g by auto
also have "?m (Suc (index i)) = g (Suc i)"
proof -
let ?i = "Suc (index i)"
{
fix k
assume "?i + k ≤ index (Suc i)"
hence "?m (?i + k) = ?m ?i"
proof (induct k)
case 0 thus ?case by simp
next
case (Suc k)
with np[OF index_not_p_between[of i "?i + k"]]
show ?case by auto
qed
} note eq = this
let ?k = "index (Suc i) - ?i"
from index_ordered[of i] have "?i ≤ index (Suc i)" by auto
hence id: "?i + ?k = index (Suc i)" by auto
hence "?i + ?k ≤ index (Suc i)" by auto
from eq[OF this] show ?thesis unfolding id g ..
qed
finally have "(g i, g (Suc i)) ∈ ?r" .
}
hence "¬ SN_on ?r {g 0}" unfolding SN_defs by auto
with main[of "index 0"] show False unfolding g by auto
qed
qed
end
context sl_interpr_root
begin
lemma SN_inj_root: assumes inj: "⋀ f. inj (L f)"
and wwf: "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q R"
and SN: "SN_on (qrstep nfs Q R) {t}"
and ndef: "¬ defined (applicable_rules Q R) (the (root t))"
and model: "qmodel I L LC C cge R"
and cge: "cge = (op =)"
and wf: "wf_ass α"
and LQ: "NF_terms (Lab_lhss Q) ⊇ NF_terms LQ"
and nvar: "⋀ l r. (l,r) ∈ R ⟹ is_Fun l"
shows "SN_on (qrstep nfs LQ (Lab_trs R)) {Lab_root α t}"
proof (rule SN_on_subset1[OF _ qrstep_mono[OF subset_refl LQ]])
from nvar have nvar: "∀ (l,r) ∈ R. is_Fun l" by auto
{
fix l r
assume lr: "(l,r) ∈ Lab_trs R" and v: "is_Var l"
from lr obtain ll rr where "(l,r) ∈ lab_rule I L LC C (ll,rr)"
and llrr: "(ll,rr) ∈ R" by auto
then obtain α where l: "l = Lab α ll" unfolding lab_rule_def by auto
from nvar llrr v have False unfolding l by (cases ll, auto simp: Let_def)
}
hence nvarL: "∀ (l,r) ∈ Lab_trs R. is_Fun l" by auto
let ?LQ = "Lab_lhss Q"
let ?QR = "qrstep nfs ?LQ (Lab_trs R)"
show "SN_on ?QR {Lab_root α t}"
proof (cases t)
case (Var x)
show ?thesis
proof
fix f
assume z: "f 0 ∈ {Lab_root α t}" and steps: "∀ i. (f i, f (Suc i)) ∈ ?QR"
from steps[THEN spec[of _ 0]] singletonD[OF z] Var have "(Var x, f (Suc 0)) ∈ ?QR" by simp
thus False
proof
fix D σ l r
assume lr: "(l,r) ∈ Lab_trs R" and "Var x = D⟨l⋅σ⟩"
then obtain y where l: "l = Var y" by (cases D, simp, cases l, auto)
from nvarL l lr show False by force
qed
qed
next
case (Fun f ts)
show ?thesis unfolding Fun lab_root.simps Let_def
proof (rule SN_args_imp_SN[OF _ nvarL], unfold map_map o_def)
fix lt
assume "lt ∈ set (map (Lab α) ts)"
then obtain t where t: "t ∈ set ts" and lt: "lt = Lab α t" by auto
show "SN_on ?QR {lt}" unfolding lt
by (rule SN_inj[OF inj wwf SN_imp_SN_arg_gen[OF ctxt_closed_qrstep SN[unfolded Fun] t] model cge wf subset_refl])
next
let ?n = "length ts"
let ?f = "LC f ?n (L' f (map (Eval α) ts))"
let ?m = "length (map (Lab α) ts)"
let ?U = "applicable_rules ?LQ (Lab_trs R)"
let ?d = "defined ?U (?f,?m)"
show "¬ ?d"
proof
assume "?d"
from this[unfolded defined_def]
obtain l r where lr: "(l,r) ∈ ?U" and l: "root l = Some (?f, ?n)" by auto
then obtain ls where l: "l = Fun ?f ls" and ls: "length ls = ?n" by (cases l, auto)
from lr[unfolded applicable_rules_def] have lr: "(l,r) ∈ Lab_trs R"
and u: "applicable_rule ?LQ (l,r)" by auto
from u[unfolded applicable_rule_def] have
NF: "⋀ s. l ⊳ s ⟹ s ∈ NF_terms (Lab_lhss Q)" by auto
from lr obtain ll rr where "(l,r) ∈ lab_rule I L LC C (ll,rr)"
and llrr: "(ll,rr) ∈ R" by auto
then obtain α where l': "l = Lab α ll" and r: "r = Lab α rr"
and wf_a: "wf_ass α"
unfolding lab_rule_def by auto
have u: "applicable_rule Q (ll,rr)"
unfolding applicable_rule_def fst_conv
proof (intro allI impI)
fix s
assume supt: "ll ⊳ s"
show "s ∈ NF_terms Q"
proof (rule lab_nf_rev[OF _ wf_a])
from supt obtain D where llD: "ll = D⟨s⟩" and D: "D ≠ □" by auto
show "Lab α s ∈ NF_terms (Lab_lhss Q)"
by (rule NF[unfolded l' llD lab_ctxt, OF nectxt_imp_supt_ctxt],
insert D, cases D, auto simp: Let_def)
qed
qed
with llrr have u: "(ll,rr) ∈ applicable_rules Q R"
unfolding applicable_rules_def by auto
from ndef[unfolded Fun] have ndef: "¬ defined (applicable_rules Q R) (f, ?n)" by auto
from l[unfolded l'] obtain g lls where ll: "ll = Fun g lls" by (cases ll, auto simp: Let_def)
let ?g = "LC g (length lls) (L g (map (Eval α) lls))"
from l[unfolded l' ll] have gf: "?g = ?f" and lls: "length lls = length ls"
by (auto simp: Let_def o_def)
from arg_cong[OF gf, of LD, unfolded LD_LC] have gf: "g = f" by auto
have "defined (applicable_rules Q R) (g, length lls)"
unfolding defined_def using u unfolding ll by auto
with ndef show False unfolding gf lls ls ..
qed
qed
qed
qed
end
context sl_interpr
begin
lemma model_rewrite:
fixes R :: "('f,'v)trs"
assumes model: "qmodel I L LC C cge R"
and decr: "Decr = ({} :: ('lf,'v)trs)" (is "?D = {}")
and step: "(s,t) ∈ qrstep nfs Q R"
and LQ: "NF_terms LQ ⊇ NF_terms (Lab_lhss_all Q)"
shows "(LAB s, LAB t) ∈ qrstep nfs LQ (Lab_trs R)"
proof -
from quasi_lab_rewrite[OF _ _ step model wf_default_ass lge_term_refl, of ?D,
unfolded qrstep_empty_r decr wf_trs_def]
obtain v where step: "(LAB s, v) ∈ qrstep nfs (Lab_lhss_all Q) (Lab_trs R)" and lge: "lge_term v (LAB t)" by auto
{
fix s t :: "('lf,'v)term"
assume "lge_term s t"
hence "s = t"
proof (induct s arbitrary: t)
case (Var x)
thus ?case by (cases t, auto)
next
case (Fun f ss t)
from Fun(2) obtain g ts where t: "t = Fun g ts" by (cases t, auto simp: Let_def)
note Fun = Fun[unfolded t]
have ssts: "ss = ts"
by (rule nth_equalityI, insert Fun, auto)
from Fun(2)[simplified]
obtain h lf lg where f: "f = LC h (length ts) lf" and
g: "g = LC h (length ts) lg" and
disj: "lf = lg ∨ Ball {lf,lg} (LS h (length ts)) ∧ lge h (length ts) lf lg" (is "?id ∨ ?cond") by auto
from disj have "?id ∨ lf ≠ lg ∧ ?cond" by blast
hence fg: "f = g"
proof
assume "lf = lg"
thus ?thesis unfolding f g by auto
next
assume cond: "lf ≠ lg ∧ ?cond"
hence "(lf,lg) ∈ gr h (length ts)"
unfolding lge_to_lgr_rel_def lge_to_lgr_def
by (auto simp: Let_def)
with cond decr show ?thesis unfolding decr_of_ord_def by auto
qed
show ?case unfolding t fg ssts ..
qed
}
from step[unfolded this[OF lge]]
qrstep_mono[OF subset_refl LQ]
show ?thesis by blast
qed
end
hide_const Semantic_Labeling.aux
locale sl_interpr_same = sl_interpr C c I cge lge L LC LD LS
for
C :: "'c set"
and c :: "'c"
and I :: "('f,'c)inter"
and cge :: "'c ⇒ 'c ⇒ bool"
and lge :: "'f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool"
and L :: "('f,'c,'l)label"
and LC :: "('f,'l,'f)lcompose"
and LD :: "('f,'f,'l)ldecompose"
and LS :: "('f,'l)labels"
begin
lemma sl_model_finite: fixes R :: "('f,'v)trs"
assumes inj: "⋀ f. inj (L f)"
and wwf: "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q (R ∪ Rw)"
and model_R: "qmodel I L LC C cge R"
and model_Rw: "qmodel I L LC C cge Rw"
and cge: "cge = (op =)"
and decr: "Decr = ({} :: ('f,'v)trs)"
and LQ1: "NF_terms (Lab_lhss Q) ⊇ NF_terms LQ"
and LQ2: "NF_terms LQ ⊇ NF_terms (Lab_lhss_all Q)"
and fin: "finite_dpp (nfs,m,Lab_trs P, Lab_trs Pw, LQ, Lab_trs R, Lab_trs Rw)"
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)"
proof -
let ?P = "Lab_trs P"
let ?Pw = "Lab_trs Pw"
let ?R = "Lab_trs R"
let ?Rw = "Lab_trs Rw"
let ?Q = "LQ"
let ?subst_closure' = "rqrstep nfs ?Q"
let ?subst_closure = "rqrstep nfs Q"
let ?M = "{(s, t). m ⟶ SN_on (qrstep nfs ?Q (?R ∪ ?Rw)) {t}}"
let ?N = "{(s,t). s ∈ NF_terms ?Q}"
let ?P' = "?subst_closure' ?P ∩ ?N ∩ ?M"
let ?Pw' = "?subst_closure' ?Pw ∩ ?N ∩ ?M"
let ?R' ="qrstep nfs ?Q ?R"
let ?Rw' ="qrstep nfs ?Q ?Rw"
let ?A = "?P' ∪ ?Pw' ∪ ?R' ∪ ?Rw'"
note NF_anti = LQ2
show ?thesis
proof (rule finite_dpp_map_min[OF fin, where I = "λ _. True"])
fix t
assume SN: "m ⟶ SN_on (qrstep nfs Q (R ∪ Rw)) {t}"
show "m ⟶ SN_on (qrstep nfs ?Q (?R ∪ ?Rw)) {LAB t}"
proof
assume m
with SN have SN: "SN_on (qrstep nfs Q (R ∪ Rw)) {t}" by blast
show "SN_on (qrstep nfs ?Q (?R ∪ ?Rw)) {LAB t}"
unfolding lab_trs_union[symmetric]
by (rule SN_inj[OF inj wwf SN _ cge wf_default_ass LQ1],
insert model_R model_Rw, auto simp: qmodel_def)
qed
next
fix s t
assume "(s,t) ∈ qrstep nfs Q Rw"
from model_rewrite[OF model_Rw decr this LQ2]
show "(LAB s, LAB t)
∈ ?A^* ∧ True" by auto
next
fix s t
assume "(s,t) ∈ qrstep nfs Q R"
from model_rewrite[OF model_R decr this LQ2]
show "(LAB s, LAB t) ∈ ?A^* O (?P' ∪ ?R') O ?A^* ∧ True"
by auto
next
fix s t
assume "(s,t) ∈ ?subst_closure P ∩ {(s,t). s ∈ NF_terms Q}" and SN: "m ⟶ SN_on (qrstep nfs ?Q (?R ∪ ?Rw)) {LAB t}"
hence step: "(s,t) ∈ ?subst_closure P" and nf: "s ∈ NF_terms Q" by auto
from lab_nf[OF nf] have "LAB s ∈ NF_terms (Lab_lhss_all Q)" by auto
with NF_anti
have N: "(LAB s, LAB t) ∈ ?N" by auto
from lab_rqrstep[OF step wf_default_ass] rqrstep_mono[OF subset_refl NF_anti]
have "(LAB s, LAB t) ∈ rqrstep nfs LQ (Lab_trs P)" by blast
with N SN show "(LAB s, LAB t) ∈ ?A^* O ?P' O ?A^* ∧ True" by auto
next
fix s t
assume "(s,t) ∈ ?subst_closure Pw ∩ {(s,t). s ∈ NF_terms Q}" and SN: "m ⟶ SN_on (qrstep nfs ?Q (?R ∪ ?Rw)) {LAB t}"
hence step: "(s,t) ∈ ?subst_closure Pw" and nf: "s ∈ NF_terms Q" by auto
from lab_nf[OF nf] have "LAB s ∈ NF_terms (Lab_lhss_all Q)" by auto
with NF_anti
have N: "(LAB s, LAB t) ∈ ?N" by auto
from lab_rqrstep[OF step wf_default_ass] rqrstep_mono[OF subset_refl NF_anti]
have "(LAB s, LAB t) ∈ rqrstep nfs LQ (Lab_trs Pw)" by blast
with N SN show "(LAB s, LAB t) ∈ ?A^* O (?P' ∪ ?Pw') O ?A^* ∧ True" by auto
qed
qed
end
locale sl_interpr_root_same = sl_interpr_root C c I cge lge L LC LD LS L' LS'
for C :: "'c set"
and c :: "'c"
and I :: "('f,'c)inter"
and cge :: "'c ⇒ 'c ⇒ bool"
and lge :: "'f ⇒ nat ⇒ 'l ⇒ 'l ⇒ bool"
and L :: "('f,'c,'l)label"
and LC :: "('f,'l,'f)lcompose"
and LD :: "('f,'f,'l)ldecompose"
and LS :: "('f,'l)labels"
and L' :: "('f,'c,'l)label"
and LS' :: "('f,'l)labels"
begin
lemma sl_model_root_finite: fixes R :: "('f,'v)trs"
assumes inj: "⋀ f. inj (L f)"
and wwf: "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q (R ∪ Rw)"
and model_R: "qmodel I L LC C cge R"
and model_Rw: "qmodel I L LC C cge Rw"
and cge: "cge = (op =)"
and decr: "Decr = ({} :: ('f,'v)trs)"
and decr_root: "Decr_root = ({} :: ('f,'v)trs)"
and LQ1: "NF_terms (Lab_lhss Q) ⊇ NF_terms LQ"
and LQ2: "NF_terms LQ ⊇ NF_terms (Lab_lhss_all Q)"
and nvarP: "∀ (s,t) ∈ P ∪ Pw. is_Fun s ∧ is_Fun t"
and ndefP: "∀ (s,t) ∈ P ∪ Pw. ¬ defined (applicable_rules Q (R ∪ Rw)) (the (root t))"
and nvar: "∀ (s,t) ∈ R ∪ Rw. is_Fun s"
and fin: "finite_dpp (nfs,m,Lab_root_trs P, Lab_root_trs Pw, LQ, Lab_trs R, Lab_trs Rw)"
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)"
proof -
let ?E = "{} :: ('f,'v)trs"
from decr have decr: "Decr ⊆ (subst.closure ?E ∩ Decr)^+" by auto
from decr_root have decr_root: "⋀ D :: ('f,'v)trs. Decr_root^= O D = D" by auto
let ?P = "Lab_root_trs P"
let ?Pw = "Lab_root_trs Pw"
let ?R = "Lab_trs R"
let ?Rw = "Lab_trs Rw"
let ?Q = "LQ"
let ?R' ="qrstep nfs ?Q ?R"
let ?Rw' ="qrstep nfs ?Q (?R ∪ ?Rw)"
let ?dpp = "(nfs,m,P,Pw,Q,R,Rw)"
note mono2 = qrstep_mono[OF _ LQ2]
have wftrs: "wf_trs {}" unfolding wf_trs_def by auto
show ?thesis
unfolding finite_dpp_def
proof (clarify)
fix s t σ
assume "min_ichain ?dpp s t σ"
hence ichain: "ichain ?dpp s t σ" and SN: "⋀ i. m ⟹ SN_on (qrstep nfs Q (R ∪ Rw)) {t i ⋅ σ i}" by (auto simp: minimal_cond_def)
let ?steps = "λ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (qrstep nfs Q (R ∪ Rw))^* O qrstep nfs Q R O (qrstep nfs Q (R ∪ Rw))^*"
from ichain[unfolded ichain.simps]
have PPw: "⋀ i. (s i, t i) ∈ P ∪ Pw"
and steps: "⋀ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (qrstep nfs Q (R ∪ Rw))^*"
and NF: "⋀ i. s i ⋅ σ i ∈ NF_terms Q"
and nfs: "⋀ i. NF_subst nfs (s i, t i) (σ i) Q"
and inf: "(INFM i. (s i, t i) ∈ P) ∨ (INFM i. ?steps i)"
by auto
let ?l = "LAB_root"
let ?ts = "λ i. ?l (t i ⋅ σ i)"
let ?ss = "λ i. ?l (s i ⋅ σ i)"
let ?a = "subst_ass default_ass"
let ?t = "λ i. Lab_root (?a (σ i)) (t i)"
let ?s = "λ i. Lab_root (?a (σ i)) (s i)"
let ?σ = "λ i. lab_subst default_ass (σ i)"
let ?p = "λ i. (?t i ⋅ ?σ i, ?s (Suc i) ⋅ ?σ (Suc i))"
from model_R model_Rw have model: "qmodel I L LC C cge (R ∪ Rw)"
unfolding qmodel_def by auto
{
fix i
note wf_ass_subst_ass[OF wf_default_ass, of "σ i"]
} note wf_ass = this
{
fix i
from nvarP PPw[of i] have nvarPi: "is_Fun (t i)" "is_Fun (s i)" by auto
from nvarP PPw[of "Suc i"] have nvarPsi: "is_Fun (s (Suc i))" by auto
have tsi: "?t i ⋅ ?σ i = ?ts i" unfolding lab_root_subst[OF nvarPi(1)] ..
have ssi: "?s i ⋅ ?σ i = ?ss i" unfolding lab_root_subst[OF nvarPi(2)] ..
have sssi: "?s (Suc i) ⋅ ?σ (Suc i) = ?ss (Suc i)" unfolding lab_root_subst[OF nvarPsi] ..
from nvarPi obtain f ts where ti: "t i = Fun f ts" by force
from nvarPi obtain g ss where si: "s i = Fun g ss" by force
from ndefP PPw[of i] have ndef: "¬ defined (applicable_rules Q (R ∪ Rw)) (f, length ts)" using ti by force
from ndef have ndef: "¬ defined (applicable_rules Q (R ∪ Rw)) (the (root (t i ⋅ σ i)))" unfolding ti by auto
from wf_ass[of i] PPw[of i] have PPw: "(?s i, ?t i) ∈ ?P ∪ ?Pw" by (force simp: lab_root_rule_def)
have steps: "?p i ∈
?Rw'^*" unfolding tsi sssi
by (rule set_mp[OF _ quasi_lab_root_steps_qnf[OF nvar ndef decr wftrs steps[of i] model_R model_Rw NF wf_default_ass, unfolded decr_root]],
rule rtrancl_mono[OF mono2], auto)
from set_mp[OF LQ2 lab_nf_root[OF NF[of i], of default_ass]]
have NF: "?s i ⋅ ?σ i ∈ NF_terms ?Q" unfolding ssi .
from SN_inj_root[OF inj wwf SN[of i] ndef model cge wf_default_ass LQ1 ]
have SN: "m ⟹ SN_on ?Rw' {?t i ⋅ ?σ i}" unfolding lab_trs_union tsi using nvar by auto
let ?aa = "?a (σ i)"
from lab_nf_subst[OF nfs[of i]]
have "NF_subst nfs (Lab ?aa (s i), Lab ?aa (t i)) (?σ i) (Lab_lhss_all Q)" .
hence "NF_subst nfs (?s i, ?t i) (?σ i) (Lab_lhss_all Q)"
unfolding NF_subst_def ti si vars_rule_def by (auto simp: Let_def)
with LQ2
have nfs: "NF_subst nfs (?s i, ?t i) (?σ i) LQ" unfolding NF_subst_def by auto
note PPw steps NF SN tsi sssi ndef nfs
}
note main = this
from main(4) have min: "m ⟹ minimal_cond nfs ?Q (?R ∪ ?Rw) ?s ?t ?σ"
unfolding minimal_cond_def by auto
let ?dpp = "(nfs,m,?P,?Pw,?Q,?R,?Rw)"
have ichain: "ichain ?dpp ?s ?t ?σ"
unfolding ichain.simps
proof (intro conjI allI)
fix i
show "(?s i, ?t i) ∈ ?P ∪ ?Pw" using main(1) by auto
show "?s i ⋅ ?σ i ∈ NF_terms ?Q" using main(3) by auto
show "?p i ∈ ?Rw'^*" using main(2) by auto
show "NF_subst nfs (?s i, ?t i) (?σ i) LQ" using main(8) .
let ?lsteps = "λ i. ?p i ∈ ?Rw'^* O ?R' O ?Rw'^*"
show "(INFM i. (?s i, ?t i) ∈ ?P) ∨ (INFM i. ?lsteps i)"
unfolding INFM_disj_distrib[symmetric]
unfolding INFM_nat_le
proof (intro allI)
fix n
from inf[unfolded INFM_disj_distrib[symmetric], unfolded INFM_nat_le]
obtain m where m: "m ≥ n" and disj: "(s m, t m) ∈ P ∨ ?steps m" by blast
show "∃ m ≥ n. (?s m, ?t m) ∈ ?P ∨ ?lsteps m"
proof (intro exI conjI, rule m)
from disj show "(?s m, ?t m) ∈ ?P ∨ ?lsteps m"
proof
assume "(s m, t m) ∈ P"
thus ?thesis
using wf_ass[of m] by (force simp: lab_root_rule_def)
next
assume "?steps m"
from set_mp[OF relto_mono[OF mono2[OF subset_refl] mono2[OF subset_refl]]
quasi_lab_root_relto_qnf[OF nvar main(7) decr wftrs this model_R model_Rw NF wf_default_ass, unfolded decr_root]]
show ?thesis
unfolding main(5) main(6)
by simp
qed
qed
qed
qed
with min have "min_ichain ?dpp ?s ?t ?σ" by simp
with fin show False unfolding finite_dpp_def by auto
qed
qed
lemma sl_qmodel_root_finite: fixes R D :: "('f,'v)trs"
assumes model_R: "qmodel I L LC C cge R"
and model_Rw: "qmodel I L LC C cge Rw"
and D1: "Decr ⊆ (subst.closure D ∩ Decr)^+"
and wf: "nfs ⟹ Q ≠ {} ⟹ wf_trs D"
and wwf: "nfs ⟹ Q ≠ {} ⟹ wwf_qtrs Q (R ∪ Rw)"
and D2: "D ⊆ Decr"
and LQ1: "NF_terms (Lab_lhss_more Q) ⊇ NF_terms LQ"
and LQ2: "NF_terms LQ ⊇ NF_terms (Lab_lhss_all Q)"
and Q: "⋀q. q ∈ Q ⟹ linear_term q"
and LR: "Lab_trs R ⊆ LR"
and LRw: "Lab_trs Rw ⊆ LR ∪ LRw"
and LRRw: "LR ∪ LRw ⊆ Lab_all_trs (R ∪ Rw)"
and nvarP: "∀ (s,t) ∈ P ∪ Pw. is_Fun s ∧ is_Fun t"
and ndefP: "∀ (s,t) ∈ P ∪ Pw. ¬ defined (applicable_rules Q (R ∪ Rw)) (the (root t))"
and nvar: "∀ (l,r) ∈ R ∪ Rw. is_Fun l"
and fin: "finite_dpp (nfs,m,Lab_root_all_trs P, Lab_root_all_trs Pw, LQ, LR, LRw ∪ D)"
shows "finite_dpp (nfs,m,P,Pw,Q,R,Rw)"
proof -
let ?r = "qrstep nfs Q R"
let ?rw = "qrstep nfs Q (R ∪ Rw)"
let ?rws = "?rw^*"
let ?rrw = "?rws O ?r O ?rws"
let ?D = "Decr_root :: ('f,'v)trs"
let ?P = "Lab_root_all_trs P"
let ?Pw = "Lab_root_all_trs Pw"
let ?R = "Lab_trs R"
let ?Rw = "Lab_trs Rw"
let ?Q = "LQ"
let ?R' ="qrstep nfs ?Q ?R"
let ?Rw' ="qrstep nfs ?Q (?R ∪ ?Rw ∪ D)"
let ?Rws = "?Rw'^*"
let ?RRw = "?Rws O ?R' O ?Rws"
let ?dpp = "(nfs,m,P,Pw,Q,R,Rw)"
note mono2 = qrstep_mono[OF subset_refl LQ2]
show ?thesis
unfolding finite_dpp_def
proof (clarify)
fix s t σ
assume "min_ichain ?dpp s t σ"
hence ichain: "ichain ?dpp s t σ" and SN: "⋀ i. m ⟹ SN_on (qrstep nfs Q (R ∪ Rw)) {t i ⋅ σ i}" by (auto simp: minimal_cond_def)
let ?steps = "λ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (qrstep nfs Q (R ∪ Rw))^* O qrstep nfs Q R O (qrstep nfs Q (R ∪ Rw))^*"
from ichain[unfolded ichain.simps]
have PPw: "⋀ i. (s i, t i) ∈ P ∪ Pw"
and steps: "⋀ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i)) ∈ (qrstep nfs Q (R ∪ Rw))^*"
and NF: "⋀ i. s i ⋅ σ i ∈ NF_terms Q"
and nfs: "⋀ i. NF_subst nfs (s i, t i) (σ i) Q"
and inf: "(INFM i. (s i, t i) ∈ P) ∨ (INFM i. ?steps i)"
by auto
let ?l = "LAB_root"
let ?ts = "λ i. ?l (t i ⋅ σ i)"
let ?ss = "λ i. ?l (s i ⋅ σ i)"
let ?a = "subst_ass default_ass"
let ?s = "λ i. Lab_root (?a (σ i)) (s i)"
let ?σ = "λ i. lab_subst default_ass (σ i)"
let ?p' = "λ i. (t i ⋅ σ i, s (Suc i) ⋅ σ (Suc i))"
let ?p = "λ i. (?l (t i ⋅ σ i), ?l (s (Suc i) ⋅ σ (Suc i)))"
let ?Pc = "λ i. if (s i,t i) ∈ P then ?P else ?Pw"
let ?pc = "λ i. if (s i,t i) ∈ P then P else Pw"
let ?Rc = "λ i. if ?p' i ∈ ?rrw then ?RRw else ?Rws"
let ?w = "λ t. ⋃(funas_term ` set (args t)) ⊆ F_all"
let ?m = "map_funs_term UNLAB"
let ?mu = "λ i u. ?m (u ⋅ ?σ i) = t i ⋅ σ i"
let ?muu = "λ i u. ?m (u ) = t i"
have rrws: "?RRw ⊆ ?Rws" unfolding qrstep_union by regexp
let ?prop = "λ i P R lt. (?s i,lt) ∈ P ∧ (lt ⋅ ?σ i,
?s (Suc i) ⋅ ?σ (Suc i)) ∈ R ∧ ?mu i lt ∧ ?w (lt ⋅ ?σ i) ∧ ?muu i lt"
let ?t' = "λ i. SOME lt. ?prop i (?Pc i) (?Rc i) lt"
obtain t' where t': "t' = ?t'" by auto
let ?p'' = "λ i. (t' i ⋅ ?σ i, ?s (Suc i) ⋅ ?σ (Suc i))"
from model_R model_Rw have model: "qmodel I L LC C cge (R ∪ Rw)"
unfolding qmodel_def by auto
{
fix i
note wf_ass_subst_ass[OF wf_default_ass, of "σ i"]
} note wf_ass = this
{
fix i
from nvarP PPw[of i] have nvarPi: "is_Fun (t i)" "is_Fun (s i)" by auto
from nvarP PPw[of "Suc i"] have nvarPsi: "is_Fun (s (Suc i))" by auto
have ssi: "?s i ⋅ ?σ i = ?ss i" unfolding lab_root_subst[OF nvarPi(2)] ..
have sssi: "?ss (Suc i) = ?s (Suc i) ⋅ ?σ (Suc i)" unfolding lab_root_subst[OF nvarPsi] ..
from nvarPi obtain f ts where ti: "t i = Fun f ts" by force
from nvarPi obtain g ss where si: "s i = Fun g ss" by force
from ndefP PPw[of i] have ndef: "¬ defined (applicable_rules Q (R ∪ Rw)) (f, length ts)" using ti by force
from ndef have ndef: "¬ defined (applicable_rules Q (R ∪ Rw)) (the (root (t i ⋅ σ i)))" unfolding ti by auto
have steps: "?p i ∈ ?D^= O ?Rc i"
proof (cases "?p' i ∈ ?rrw")
case False
hence id: "?Rc i = ?Rws" by simp
show ?thesis unfolding id
by (rule set_mp[OF _ quasi_lab_root_steps_qnf[OF nvar ndef D1 wf steps[of i] model_R model_Rw NF wf_default_ass]], insert rtrancl_mono[OF mono2], auto)
next
case True
hence id: "?Rc i = ?RRw" by auto
from quasi_lab_root_relto_qnf[OF nvar ndef D1 wf True model_R model_Rw NF wf_default_ass]
obtain v where "(?ts i, v) ∈ Decr_root^=" and "(v, ?ss (Suc i)) ∈ relto (qrstep nfs (Lab_lhss_all Q) ?R ) (qrstep nfs (Lab_lhss_all Q) (?R ∪ ?Rw ∪ D))"
by auto
with set_mp[OF relto_mono[OF mono2 mono2], of "(v, ?ss (Suc i))" nfs "?R ∪ ?Rw ∪ D" nfs ?R]
show ?thesis unfolding id by blast
qed
have pc: "(s i, t i) ∈ ?pc i" using PPw[of i] by auto
note steps = quasi_lab_root_all_merge[OF steps nvarPi(1) pc wf_default_ass]
have pc: "Lab_root_all_trs (?pc i) = ?Pc i" by simp
note steps = steps[unfolded pc sssi]
from someI_ex[OF steps]
have t': "?prop i (?Pc i) (?Rc i) (t' i)" unfolding t' .
from set_mp[OF LQ2 lab_nf_root[OF NF[of i], of default_ass]]
have NF: "?s i ⋅ ?σ i ∈ NF_terms ?Q" unfolding ssi .
obtain lu u where lu: "lu = t' i ⋅ ?σ i" and u: "u = t i ⋅ σ i" by auto
with t' SN[of i] have wf: "?w lu" and mu: "u = ?m lu" and SN: "m ⟹ SN_on ?rw {?m lu}" by auto
from SN_on_UNLAB_imp_SN_on[OF LRRw Q wf wwf SN LQ1]
have SN: "m ⟹ SN_on (qrstep nfs LQ (LR ∪ LRw ∪ Decr)) {lu}" .
have SN: "m ⟹ SN_on (qrstep nfs LQ (LR ∪ LRw ∪ D)) {lu}"
by (rule SN_on_subset1[OF SN qrstep_mono], insert D2, auto)
let ?aa = "?a (σ i)"
from t' have tim: "t i = map_funs_term UNLAB (t' i)" by simp
have varsti: "vars_term (t' i) = vars_term (t i)" unfolding tim by simp
from lab_nf_subst[OF nfs[of i]] have "NF_subst nfs (Lab ?aa (s i), Lab ?aa (t i)) (?σ i) (Lab_lhss_all Q)" .
hence "NF_subst nfs (Lab ?aa (s i), Lab ?aa (t i)) (?σ i) LQ"
using LQ2 unfolding NF_subst_def by auto
hence nfs: "NF_subst nfs (?s i, t' i) (?σ i) LQ" using varsti
unfolding si ti NF_subst_def vars_rule_def by (auto simp: Let_def)
note t' NF SN[unfolded lu] nfs
}
note main = this
have id: "?R ∪ (?Rw ∪ D) = ?R ∪ ?Rw ∪ D" by auto
let ?dpp = "(nfs,m,?P,?Pw,?Q,?R,?Rw ∪ D)"
have ichain: "ichain ?dpp ?s t' ?σ"
unfolding ichain.simps id
proof (intro conjI allI)
fix i
show "(?s i, t' i) ∈ ?P ∪ ?Pw"
using main(1)[of i] by (cases "(s i, t i) ∈ P", auto)
show "?s i ⋅ ?σ i ∈ NF_terms ?Q" using main(2) by auto
show "?p'' i ∈ ?Rws" using main(1)[of i] rrws
by (cases "?p' i ∈ ?rrw", auto)
show "NF_subst nfs (?s i, t' i) (?σ i) LQ" using main[of i] by simp
let ?lsteps = "λ i. ?p'' i ∈ ?RRw"
show "(INFM i. (?s i, t' i) ∈ ?P) ∨ (INFM i. ?lsteps i)"
unfolding INFM_disj_distrib[symmetric]
unfolding INFM_nat_le
proof (intro allI)
fix n
from inf[unfolded INFM_disj_distrib[symmetric], unfolded INFM_nat_le]
obtain m where m: "m ≥ n" and disj: "(s m, t m) ∈ P ∨ ?p' m ∈ ?rrw" by blast
show "∃ m ≥ n. (?s m, t' m) ∈ ?P ∨ ?lsteps m"
proof (intro exI conjI, rule m)
from disj show "(?s m, t' m) ∈ ?P ∨ ?lsteps m"
proof
assume "(s m, t m) ∈ P"
thus ?thesis using main(1)[of m] by auto
next
assume "?p' m ∈ ?rrw"
thus ?thesis using main(1)[of m] by auto
qed
qed
qed
qed
let ?dpp = "(nfs,m,?P,?Pw, ?Q, LR, LRw ∪ D)"
have ichain: "ichain ?dpp ?s t' ?σ"
by (rule ichain_mono[OF ichain _ _ _ LR], insert LRw LR, auto)
from main(3) have min_cond: "m ⟹ minimal_cond nfs ?Q (LR ∪ (LRw ∪ D)) ?s t' ?σ"
unfolding minimal_cond_def Un_assoc ..
from ichain min_cond have "min_ichain ?dpp ?s t' ?σ" by simp
with fin show False unfolding finite_dpp_def by auto
qed
qed
end
sublocale sl_interpr_root_same ⊆ sl_interpr_same ..
end