Theory Labels_and_Overlaps
section‹Labels and Overlaps›
theory Labels_and_Overlaps
imports
Orthogonal_PT
Well_Quasi_Orders.Almost_Full_Relations
begin
subsection‹Labeled Proof Terms›
text‹The idea is to label function symbols in the source of a proof term that are affected by
a rule symbol @{term α} with @{term α} and the distance from the root to @{term α}.
Therefore, a label is a pair consisting of a rule symbol and a natural number, or it can be
@{term None}.
A labeled term is a term, where each function symbol additionally has a label associated with it.›
type_synonym
('f, 'v) label = "(('f, 'v) prule × nat) option"
type_synonym
('f, 'v) term_lab = "('f × ('f, 'v) label, 'v) term"
fun label_term :: "('f, 'v) prule ⇒ nat ⇒ ('f, 'v) term ⇒ ('f, 'v) term_lab"
where
"label_term α i (Var x) = Var x"
| "label_term α i (Fun f ts) = Fun (f, Some (α, i)) (map (label_term α (i+1)) ts)"
abbreviation labeled_lhs :: "('f, 'v) prule ⇒ ('f, 'v) term_lab"
where "labeled_lhs α ≡ label_term α 0 (lhs α)"
fun labeled_source :: "('f, 'v) pterm ⇒ ('f, 'v) term_lab"
where
"labeled_source (Var x) = Var x"
| "labeled_source (Pfun f As) = Fun (f, None) (map labeled_source As)"
| "labeled_source (Prule α As) = (labeled_lhs α) ⋅ ⟨map labeled_source As⟩⇩α"
fun term_lab_to_term :: "('f, 'v) term_lab ⇒ ('f, 'v) term"
where
"term_lab_to_term (Var x) = Var x"
| "term_lab_to_term (Fun f ts) = Fun (fst f) (map term_lab_to_term ts)"
fun term_to_term_lab :: "('f, 'v) term ⇒ ('f, 'v) term_lab"
where
"term_to_term_lab (Var x) = Var x"
| "term_to_term_lab (Fun f ts) = Fun (f, None) (map term_to_term_lab ts)"
fun get_label :: "('f, 'v) term_lab ⇒ ('f, 'v) label"
where
"get_label (Var x) = None"
| "get_label (Fun f ts) = snd f"
fun labelposs :: "('f, 'v) term_lab ⇒ pos set"
where
"labelposs (Var x) = {}"
| "labelposs (Fun (f, None) ts) = (⋃i<length ts. {i # p | p. p ∈ labelposs (ts ! i)})"
| "labelposs (Fun (f, Some l) ts) = {[]} ∪ (⋃i<length ts. {i # p | p. p ∈ labelposs (ts ! i)})"
abbreviation possL :: "('f, 'v) pterm ⇒ pos set"
where "possL A ≡ labelposs (labeled_source A)"
lemma labelposs_term_to_term_lab: "labelposs (term_to_term_lab t) = {}"
by(induct t) simp_all
lemma term_lab_to_term_lab[simp]: "term_lab_to_term (term_to_term_lab t) = t"
proof(induct t)
case (Fun f ts)
then show ?case
unfolding term_lab_to_term.simps term_to_term_lab.simps fst_conv by (simp add: map_nth_eq_conv)
qed simp
lemma term_lab_to_term_subt_at:
assumes "p ∈ poss t"
shows "term_lab_to_term t |_p = term_lab_to_term (t|_p)"
using assms proof(induct p arbitrary:t)
case (Cons i p)
from args_poss[OF Cons(2)] obtain f ts where f:"t = Fun f ts" and
p:"p ∈ poss (ts ! i)" and i:"i < length ts" by blast
from Cons(1)[OF p] i show ?case
unfolding f term_lab_to_term.simps by simp
qed simp
lemma vars_term_labeled_lhs: "vars_term (label_term α i t) = vars_term t"
by (induct t arbitrary:i) simp_all
lemma vars_term_list_labeled_lhs: "vars_term_list (label_term α i t) = vars_term_list t"
proof (induct t arbitrary:i)
case (Fun f ts)
show ?case unfolding label_term.simps vars_term_list.simps using Fun
by (metis (mono_tags, lifting) length_map map_nth_eq_conv nth_mem)
qed (simp add: vars_term_list.simps(1))
lemma var_poss_list_labeled_lhs: "var_poss_list (label_term α i t) = var_poss_list t"
proof (induct t arbitrary:i)
case (Fun f ts)
then have ts:"map (var_poss_list ∘ label_term α (i + 1)) ts = map var_poss_list ts"
by auto
then show ?case
unfolding label_term.simps var_poss_list.simps map_map ts by simp
qed (simp add: poss_list.simps(1))
lemma var_labeled_lhs[simp]: "vars_distinct (label_term α i t) = vars_distinct t"
by (simp add: vars_term_list_labeled_lhs)
lemma labelposs_subt_at:
assumes "q ∈ poss t" "p ∈ labelposs (t|_q)"
shows "q@p ∈ labelposs t"
using assms proof(induct t arbitrary:q)
case (Fun f ts)
then show ?case proof(cases q)
case (Cons i q')
with Fun(2) have i:"i < length ts" and q':"q' ∈ poss (ts!i)"
by simp+
with Fun(3) have "p ∈ labelposs ((ts!i)|_q')"
unfolding Cons by simp
with Fun(1) i q' have IH:"q'@p ∈ labelposs (ts!i)"
using nth_mem by blast
obtain f' lab where f:"f = (f', lab)"
by fastforce
then show ?thesis proof(cases lab)
case None
show ?thesis
unfolding f Cons None labelposs.simps using i IH by simp
next
case (Some a)
then show ?thesis
unfolding f Cons Some labelposs.simps using i IH by simp
qed
qed simp
qed simp
lemma var_label_term:
assumes "p ∈ poss t" and "t|_p = Var x"
shows "label_term α n t |_p = Var x"
using assms proof(induct t arbitrary:p n)
case (Fun f ts)
then obtain i p' where p':"i < length ts" "p = i#p'" "p' ∈ poss (ts!i)"
by auto
then show ?case
unfolding label_term.simps p'(2) subt_at.simps using Fun(1,3) p'(2) by force
qed simp
lemma get_label_label_term:
assumes "p ∈ fun_poss t"
shows "get_label (label_term α n t|_p) = Some (α, n + size p)"
using assms proof(induct t arbitrary: n p)
case (Fun f ts)
show ?case proof(cases p)
case (Cons i p')
with Fun(2) have i:"i < length ts" and p':"p' ∈ fun_poss (ts!i)" by simp+
with Fun(1) have "get_label (label_term α (n+1) (ts!i) |_ p') = Some (α, n + 1 + size p')" by simp
then show ?thesis unfolding Cons label_term.simps subt_at.simps using i by auto
qed simp
qed simp
lemma linear_label_term:
assumes "linear_term t"
shows "linear_term (label_term α n t)"
using assms proof(induct t arbitrary:n)
case (Fun f ts)
from Fun(2) have "(is_partition (map vars_term ts))"
by simp
then have "is_partition (map vars_term (map (label_term α (Suc n)) ts))"
by (metis (mono_tags, lifting) length_map map_nth_eq_conv vars_term_labeled_lhs)
moreover {fix t assume t:"t ∈ set ts"
with Fun(2) have "linear_term t"
by simp
with Fun(1) have "linear_term (label_term α (Suc n) t)"
using t by blast
}
ultimately show ?case unfolding label_term.simps by simp
qed simp
lemma var_term_lab_to_term:
assumes "p ∈ poss t" and "t|_p = Var x"
shows "term_lab_to_term t |_p = Var x"
using assms proof(induct t arbitrary:p)
case (Fun f ts)
then obtain i p' where p':"i < length ts" "p = i#p'" "p' ∈ poss (ts!i)"
by auto
then show ?case
unfolding term_lab_to_term.simps p'(2) subt_at.simps using Fun(1,3) p'(2) by force
qed simp
lemma poss_term_lab_to_term[simp]: "poss t = poss (term_lab_to_term t)"
by(induct t) auto
lemma fun_poss_term_lab_to_term[simp]: "fun_poss t = fun_poss (term_lab_to_term t)"
by(induct t) auto
lemma vars_term_list_term_lab_to_term: "vars_term_list t = vars_term_list (term_lab_to_term t)"
proof(induct t)
case (Var x)
then show ?case
by (simp add: vars_term_list.simps(1))
next
case (Fun f ts)
then show ?case unfolding vars_term_list.simps term_lab_to_term.simps
by (smt (verit, best) length_map map_eq_conv' nth_map nth_mem)
qed
lemma vars_term_list_term_to_term_lab: "vars_term_list (term_to_term_lab t) = vars_term_list t"
proof(induct t)
case (Var x)
then show ?case
by (simp add: vars_term_list.simps(1))
next
case (Fun f ts)
then show ?case unfolding vars_term_list.simps term_to_term_lab.simps
by (metis (mono_tags, lifting) length_map map_nth_eq_conv nth_mem)
qed
lemma linear_term_to_term_lab:
assumes "linear_term t"
shows "linear_term (term_to_term_lab t)"
using assms proof(induct t)
case (Fun f ts)
then show ?case unfolding term_to_term_lab.simps linear_term.simps
by (smt (verit, best) imageE length_map list.set_map map_nth_eq_conv set_vars_term_list vars_term_list_term_to_term_lab)
qed simp
lemma var_poss_list_term_lab_to_term: "var_poss_list t = var_poss_list (term_lab_to_term t)"
proof(induct t)
case (Var x)
then show ?case
by (simp add: poss_list.simps(1))
next
case (Fun f ts)
then have *:"(map var_poss_list ts) = (map var_poss_list (map term_lab_to_term ts))"
by auto
then show ?case unfolding term_lab_to_term.simps var_poss_list.simps length_map *
by blast
qed
lemma label_poss_labeled_lhs:
assumes "p ∈ fun_poss (label_term α n t)"
shows "p ∈ labelposs (label_term α n t)"
using assms proof(induct t arbitrary:p n)
case (Fun f ts)
then show ?case proof(cases p)
case (Cons i p')
from Fun(2) have i:"i < length ts"
unfolding Cons by simp
with Fun(2) have "p' ∈ fun_poss (label_term α (n+1) (ts!i))"
unfolding Cons by auto
with i have "p' ∈ labelposs (label_term α (n+1) (ts!i))"
using Fun(1) by simp
with i show ?thesis
unfolding Cons label_term.simps labelposs.simps by simp
qed simp
qed simp
lemma labeled_var:
assumes "source A = Var x"
shows "labeled_source A = Var x"
using assms proof(induct A)
case (Prule α As)
then show ?case proof(cases "As = []")
case True
from Prule(2) have "lhs α = Var x"
unfolding source.simps True list.map by simp
with True show ?thesis
by simp
next
case False
then obtain a as where as:"As = a # as"
using list.exhaust by blast
from Prule(2) obtain y where y:"lhs α = Var y"
using is_Var_def by fastforce
from Prule(2) have "source a = Var x"
unfolding source.simps y as single_var by simp
with Prule(1) as have "labeled_source a = Var x"
by simp
then show ?thesis
unfolding labeled_source.simps as y single_var by simp
qed
qed simp_all
lemma labelposs_subs_fun_poss: "labelposs t ⊆ fun_poss t"
proof(induct t)
case (Fun fl ts)
then show ?case proof(cases "snd fl")
case None
then obtain f where f:"fl = (f, None)"
by (metis prod.collapse)
then have "labelposs (Fun fl ts) = (⋃i<length ts. {i # p |p. p ∈ labelposs (ts ! i)})"
by simp
also have "... ⊆ (⋃i<length ts. {i # p |p. p ∈ fun_poss (ts ! i)})" using Fun
by (smt SUP_mono basic_trans_rules(31) lessThan_iff mem_Collect_eq nth_mem subsetI)
finally show ?thesis
by auto
next
case (Some l)
then obtain f where f:"fl = (f, Some l)"
by (metis prod.collapse)
then have "labelposs (Fun fl ts) = {[]} ∪ (⋃i<length ts. {i # p |p. p ∈ labelposs (ts ! i)})"
by simp
also have "... ⊆ {[]} ∪ (⋃i<length ts. {i # p |p. p ∈ fun_poss (ts ! i)})" using Fun
by (smt SUP_mono basic_trans_rules(31) lessThan_iff mem_Collect_eq nth_mem subsetI sup_mono)
finally show ?thesis
by auto
qed
qed simp
lemma labelposs_subs_poss[simp]: "labelposs t ⊆ poss t"
using labelposs_subs_fun_poss fun_poss_imp_poss by blast
lemma get_label_imp_labelposs:
assumes "p ∈ poss t" and "get_label (t|_p) ≠ None"
shows "p ∈ labelposs t"
using assms proof(induct p arbitrary:t)
case Nil
then show ?case unfolding subt_at.simps
by (smt UnCI get_label.elims insert_iff labelposs.elims prod.sel(2) term.distinct(1) term.inject(2))
next
case (Cons i p)
then obtain f ts where t:"t = Fun f ts" and "p ∈ poss (ts ! i)" and i:"i < length ts"
using args_poss by blast
with Cons(1,3) have "p ∈ labelposs (ts!i)"
by simp
with i have p:"i # p ∈ (⋃i<length ts. {i # p |p. p ∈ labelposs (ts ! i)})"
by blast
then show ?case proof(cases "snd f")
case None
with p show ?thesis unfolding t using labelposs.simps(2)
by (metis (mono_tags, lifting) prod.collapse)
next
case (Some a)
with p show ?thesis unfolding t using labelposs.simps(3)
by (smt UN_iff Un_iff mem_Collect_eq prod.collapse)
qed
qed
lemma labelposs_obtain_label:
assumes "p ∈ labelposs t"
shows "∃α m. get_label (t|_p) = Some(α, m)"
using assms proof(induct t arbitrary: p)
case (Fun fl ts)
then show ?case proof(cases p)
case Nil
{fix f assume f:"fl = (f, None)"
from Fun(2) have False unfolding Nil f labelposs.simps(2)
by blast
}
with Nil show ?thesis
by (metis eq_snd_iff get_label.simps(2) option.exhaust subt_at.simps(1))
next
case (Cons i q)
with Fun(2) have iq:"i # q ∈ labelposs (Fun fl ts)"
by simp
then have i:"i < length ts"
using labelposs_subs_poss by fastforce
with iq have "i # q ∈ {i # p |p. p ∈ labelposs (ts ! i)}" proof(cases "snd fl")
case (Some a)
then obtain f α n where f:"fl = (f, Some (α, n))"
by (metis eq_snd_iff)
from iq show ?thesis unfolding f labelposs.simps
by blast
qed (smt UN_iff labelposs.simps(2) list.inject mem_Collect_eq prod.collapse)
with i Fun(1) Cons show ?thesis
by simp
qed
qed simp
lemma possL_obtain_label:
assumes "p ∈ possL A"
shows "∃α m. get_label ((labeled_source A)|_p) = Some(α, m)"
using assms labelposs_obtain_label by blast
lemma labeled_source_apply_subst:
assumes "A ∈ wf_pterm R"
shows "labeled_source (A ⋅ σ) = (labeled_source A) ⋅ (labeled_source ∘ σ)"
using assms proof(induct A)
case (3 α As)
have id:"∀ x ∈ vars_term (labeled_lhs α). (⟨map (labeled_source ∘ (λt. t ⋅ σ)) As⟩⇩α) x = (⟨map labeled_source As⟩⇩α ∘⇩s (labeled_source ∘ σ)) x"
proof-
have vars:"vars_term (labeled_lhs α) = set (var_rule α)" using vars_term_labeled_lhs by simp
{ fix i assume i:"i < length (var_rule α)"
with 3 have "(⟨map (labeled_source ∘ (λt. t ⋅ σ)) As⟩⇩α) ((var_rule α)!i) = labeled_source ((As!i) ⋅ σ)"
by (simp add: mk_subst_distinct)
also have "... = labeled_source (As!i) ⋅ (labeled_source ∘ σ)"
using 3 i by (metis nth_mem)
also have "... = (⟨map labeled_source As⟩⇩α ∘⇩s (labeled_source ∘ σ)) ((var_rule α)!i)"
using 3 i unfolding subst_compose_def by (simp add: mk_subst_distinct)
finally have "(⟨map (labeled_source ∘ (λt. t ⋅ σ)) As⟩⇩α) ((var_rule α)!i) = (⟨map labeled_source As⟩⇩α ∘⇩s (labeled_source ∘ σ)) ((var_rule α)!i)" .
} with vars show ?thesis by (metis in_set_idx)
qed
have "labeled_source ((Prule α As) ⋅ σ) = (labeled_lhs α) ⋅ ⟨map (labeled_source ∘ (λt. t ⋅ σ)) As⟩⇩α"
unfolding eval_term.simps(2) by simp
also have "... = (labeled_lhs α) ⋅ (⟨map labeled_source As⟩⇩α ∘⇩s (labeled_source ∘ σ))"
using id by (meson term_subst_eq)
also have "... = (labeled_source (Prule α As)) ⋅ (labeled_source ∘ σ)" by simp
finally show ?case .
qed simp_all
lemma labelposs_apply_subst:
"labelposs (s ⋅ σ) = labelposs s ∪ {p@q| p q x. p ∈ var_poss s ∧ s|_p = Var x ∧ q ∈ labelposs (σ x)}"
proof(induct s)
case (Fun f ts)
obtain f' l where f:"f = (f', l)" by fastforce
let ?lp1="⋃i<length ts. {i # p |p. p ∈ labelposs (ts ! i)}"
let ?lp2="⋃i<length ts. {i#(p@q)| p q x. p ∈ var_poss (ts!i) ∧ (ts!i)|_p = Var x ∧ q ∈ labelposs (σ x)}"
{fix i assume i:"i < length ts"
with Fun have "{i # p |p. p ∈ labelposs (ts ! i ⋅ σ)} = {i # p| p. p ∈ labelposs (ts!i) ∪ {p@q| p q x. p ∈ var_poss (ts!i) ∧ (ts!i)|_p = Var x ∧ q ∈ labelposs (σ x)}}"
by auto
then have "{i # p |p. p ∈ labelposs (map (λs. s ⋅ σ) ts ! i)} = {i # p| p. p ∈ labelposs (ts!i)} ∪ {i#(p@q)| p q x. p ∈ var_poss (ts!i) ∧ (ts!i)|_p = Var x ∧ q ∈ labelposs (σ x)}"
unfolding Un_iff using i by auto
}note IH=this
{fix i assume i:"i < length ts"
let ?l="{i#(p@q)| p q x. p ∈ var_poss (ts!i) ∧ (ts!i)|_p = Var x ∧ q ∈ labelposs (σ x)}"
let ?r="{p@q| p q x. p ∈ {i # p |p. p ∈ var_poss (ts ! i)} ∧ (Fun f ts)|_p = Var x ∧ q ∈ labelposs (σ x)}"
have "?l = ?r" proof
show "?l ⊆ ?r"
by (smt (verit, ccfv_SIG) Collect_mono_iff Cons_eq_appendI mem_Collect_eq subt_at.simps(2))
show "?r ⊆ ?l"
by (smt (verit, best) Collect_mono_iff Cons_eq_appendI mem_Collect_eq subt_at.simps(2))
qed
}
then have lp2:"{p@q| p q x. p ∈ var_poss (Fun f ts) ∧ (Fun f ts)|_p = Var x ∧ q ∈ labelposs (σ x)} = ?lp2"
unfolding var_poss.simps by auto
show ?case proof(cases l)
case None
have "labelposs (Fun f ts ⋅ σ) = ?lp1 ∪ ?lp2"
unfolding eval_term.simps f None labelposs.simps length_map using IH by auto
moreover have "labelposs (Fun f ts) = ?lp1"
unfolding f None by simp
ultimately show ?thesis using lp2 by simp
next
case (Some a)
have "labelposs (Fun f ts ⋅ σ) = {[]} ∪ ?lp1 ∪ ?lp2"
unfolding eval_term.simps f Some labelposs.simps length_map using IH by auto
moreover have "labelposs (Fun f ts) = {[]} ∪ ?lp1"
unfolding f Some by simp
ultimately show ?thesis using lp2 by simp
qed
qed simp
lemma possL_apply_subst:
assumes "A ⋅ σ ∈ wf_pterm R"
shows "possL (A ⋅ σ) = possL A ∪ {p@q| p q x. p ∈ var_poss (labeled_source A) ∧ (labeled_source A)|_p = Var x ∧ q ∈ possL (σ x)}"
proof-
from assms have *:"labeled_source (A ⋅ σ) = labeled_source A ⋅ (labeled_source ∘ σ)"
using labeled_source_apply_subst subst_imp_well_def by blast
then show ?thesis unfolding * labelposs_apply_subst
by auto
qed
lemma label_term_to_term[simp]: "term_lab_to_term (label_term α n t) = t"
by(induct t arbitrary:α n)(simp_all add: map_nth_eq_conv)
lemma fun_poss_label_term: "p ∈ fun_poss (label_term β n t) ⟷ p ∈ fun_poss t"
proof
{assume "p ∈ fun_poss (label_term β n t)"
then show "p ∈ fun_poss t" proof(induct t arbitrary:n p)
case (Fun f ts)
then show ?case by(cases p) auto
qed simp
}
{assume "p ∈ fun_poss t"
then show "p ∈ fun_poss (label_term β n t)" proof(induct t arbitrary:n p)
case (Fun f ts)
then show ?case by(cases p) auto
qed simp
}
qed
lemma term_lab_to_term_subst: "term_lab_to_term (t ⋅ σ) = term_lab_to_term t ⋅ (term_lab_to_term ∘ σ)"
proof(induct t)
case (Fun f As)
then show ?case unfolding eval_term.simps(2) term_lab_to_term.simps
by fastforce
qed simp
lemma labeled_source_to_term[simp]: "term_lab_to_term (labeled_source A) = source A"
proof(induct A)
case (Prule α As)
have "term_lab_to_term ∘ ⟨map labeled_source As⟩⇩α = ⟨map (term_lab_to_term ∘ labeled_source) As⟩⇩α"
by simp
also have " ... = ⟨map source As⟩⇩α" using Prule
by (metis (mono_tags, lifting) comp_apply map_eq_conv)
finally show ?case unfolding labeled_source.simps source.simps
by (simp add: term_lab_to_term_subst)
qed simp_all
lemma possL_subset_poss_source: "possL A ⊆ poss (source A)"
using poss_term_lab_to_term labeled_source_to_term labelposs_subs_poss
by metis
lemma labeled_source_pos:
assumes "p ∈ poss s" and "term_lab_to_term t = s"
shows "term_lab_to_term (t|_p) = s|_p"
using assms proof(induct p arbitrary:s t)
case (Cons i p)
from Cons(2) obtain f ss where s:"s = Fun f ss"
using args_poss by blast
with Cons(2) have p:"p ∈ poss (ss!i)"
by force
from Cons(3) s obtain label ts where t:"t = Fun (f, label) ts"
by (metis args_poss local.Cons(2) poss_term_lab_to_term prod.collapse term.inject(2) term_lab_to_term.simps(2))
with Cons(2,3) s have "term_lab_to_term (ts!i) = ss!i"
by auto
with Cons(1) p show ?case unfolding s t
by simp
qed simp
lemma get_label_at_fun_poss_subst:
assumes "p ∈ fun_poss t"
shows "get_label ((t ⋅ σ)|_p) = get_label (t|_p)"
using assms fun_poss_fun_conv fun_poss_imp_poss by fastforce
lemma labeled_source_simple_pterm:"possL (to_pterm t) = {}"
by(induct t) simp_all
lemma label_term_increase:
assumes "s = (label_term α n t) ⋅ σ" and "p ∈ fun_poss t"
shows "get_label (s|_p) = Some (α, n + length p)"
using assms proof(induct p arbitrary: s t n)
case Nil
then obtain f ts where "t = Fun f ts"
by (metis fun_poss_list.simps(1) in_set_simps(3) is_FunE is_Var_def set_fun_poss_list)
with Nil(1) show ?case
by simp
next
case (Cons i p)
then obtain f ts where f:"t = Fun f ts" and i:"i<length ts"
by (meson args_poss fun_poss_imp_poss)
with Cons(3) have p:"p ∈ fun_poss (ts!i)"
by auto
let ?s' = "(label_term α (n+1) (ts!i)) ⋅ σ"
from Cons(1) p have "get_label (?s'|_ p) = Some (α, n + 1 + length p)"
by blast
with i show ?case unfolding Cons(2) f
by simp
qed
text‹The number attached to a labeled function symbol cannot exceed the depth of that function symbol.›
lemma label_term_max_value:
assumes "p ∈ poss (labeled_source A)" and "get_label ((labeled_source A)|_p) = Some (α, n)"
and "A ∈ wf_pterm R"
shows "n ≤ length p"
using assms proof(induct A arbitrary: p)
case (Pfun f As)
then show ?case proof(cases p)
case (Cons i q)
with Pfun(2) have i:"i < length As" by simp
with Pfun(3) have lab:"get_label (labeled_source (As!i) |_ q) = Some (α, n)"
unfolding Cons by simp
with Pfun(2) i have "q ∈ poss (labeled_source (As!i))"
unfolding Cons by auto
with Pfun(1,4) Cons i lab show ?thesis
using nth_mem fun_well_arg by fastforce
qed simp
next
case (Prule β As)
from Prule(2) consider "p ∈ fun_poss (labeled_lhs β)" | "(∃p1 p2 x. p = p1@p2
∧ p1 ∈ poss (labeled_lhs β) ∧ (labeled_lhs β)|_p1 = Var x
∧ p2 ∈ poss ((⟨map labeled_source As⟩⇩β) x)
∧ (labeled_source (Prule β As))|_p = ((⟨map labeled_source As⟩⇩β) x)|_p2)"
unfolding labeled_source.simps by (meson poss_is_Fun_fun_poss poss_subst_choice)
then show ?case proof(cases)
case 1
then have "p ∈ fun_poss (lhs β)"
by (simp add: fun_poss_label_term)
then have "get_label ((labeled_source (Prule β As))|_p) = Some (β, length p)"
unfolding labeled_source.simps by (simp add: label_term_increase)
with Prule(3) show ?thesis by auto
next
case 2
then obtain p1 p2 x where p1p2:"p = p1 @ p2" and x:"p1 ∈ poss (labeled_lhs β) ∧ labeled_lhs β |_ p1 = Var x"
and p2:"p2 ∈ poss ((⟨map labeled_source As⟩⇩β) x)"
and lab:"labeled_source (Prule β As) |_ p = (⟨map labeled_source As⟩⇩β) x |_ p2"
by blast
from Prule(4) have l:"length As = length (var_rule β)"
using wf_pterm.simps by fastforce
from x have "x ∈ vars_term (lhs β)"
by (metis subt_at_imp_supteq subteq_Var_imp_in_vars_term vars_term_labeled_lhs)
with x obtain i where i:"i < length (var_rule β) ∧ (var_rule β)!i = x"
by (metis in_set_conv_nth set_vars_term_list vars_term_list_vars_distinct)
with l have *:"(⟨map labeled_source As⟩⇩β) x = labeled_source (As!i)"
by (metis (no_types, lifting) length_map lhs_subst_var_i nth_map)
with Prule(3) lab have "get_label ((labeled_source (As!i))|_p2) = Some (α, n)"
by simp
with Prule(1,4) p2 * i l have "n ≤ length p2"
by (metis fun_well_arg nth_mem)
with * p1p2 lab i l show ?thesis by force
qed
qed simp
text‹The labels decrease when moving up towards the root from a labeled function symbol.›
lemma label_decrease:
assumes "p@q ∈ poss (labeled_source A)"
and "get_label ((labeled_source A)|_(p@q)) = Some (α, length q + n)"
and "A ∈ wf_pterm R"
shows "get_label ((labeled_source A)|_p) = Some (α, n)"
using assms proof(induct A arbitrary: p q)
case (Pfun f As)
then show ?case proof(cases p)
case Nil
from Pfun(2,3) obtain i q' where iq':"q = i#q'" and i:"i < length As" and q':"q' ∈ poss (labeled_source (As!i))"
unfolding Nil by auto
with Pfun(2,3) have "get_label (labeled_source (As!i) |_ (q')) = Some (α, length q + n)"
unfolding Nil by auto
with iq' q' have False
using label_term_max_value Pfun(4) i fun_well_arg by (metis le_imp_less_Suc length_nth_simps(2) not_add_less1 nth_mem)
then show ?thesis by simp
next
case (Cons i p')
with Pfun(2) have ip':"p = i#p'" and i:"i < length As"
by auto
with Pfun(2) have p':"p'@q ∈ poss (labeled_source (As!i))"
by simp
from Pfun(3) i ip' have "get_label (labeled_source (As!i) |_ (p'@q)) = Some (α, length q + n)"
by simp
with Pfun(1,4) p' i have "get_label ((labeled_source (As!i))|_p') = Some (α, n)"
by (metis fun_well_arg nth_mem)
then show ?thesis
using i ip' by fastforce
qed
next
case (Prule β As)
from Prule(2) consider "p@q ∈ fun_poss (labeled_lhs β)" | "(∃p1 p2 x. p@q = p1@p2
∧ p1 ∈ poss (labeled_lhs β) ∧ (labeled_lhs β)|_p1 = Var x
∧ p2 ∈ poss ((⟨map labeled_source As⟩⇩β) x)
∧ (labeled_source (Prule β As))|_(p@q) = ((⟨map labeled_source As⟩⇩β) x)|_p2)"
unfolding labeled_source.simps by (meson poss_is_Fun_fun_poss poss_subst_choice)
then show ?case proof(cases)
case 1
then have lab:"get_label ((labeled_source (Prule β As))|_(p@q)) = Some (β, length p + length q)"
by (simp add: fun_poss_label_term label_term_increase)
from 1 have "p ∈ fun_poss (labeled_lhs β)" proof(cases q)
case (Cons a list)
then show ?thesis
using 1 fun_poss_append_poss fun_poss_imp_poss by blast
qed simp
with Prule(3) lab show ?thesis
by (simp add: fun_poss_label_term label_term_increase)
next
case 2
then obtain p1 p2 x where p1p2:"p@q = p1 @ p2" and x:"p1 ∈ poss (labeled_lhs β) ∧ labeled_lhs β |_ p1 = Var x"
and p2:"p2 ∈ poss ((⟨map labeled_source As⟩⇩β) x)"
and lab:"labeled_source (Prule β As) |_(p@q) = (⟨map labeled_source As⟩⇩β) x |_ p2"
by blast
from Prule(4) have l:"length As = length (var_rule β)"
using wf_pterm.simps by fastforce
from x have "x ∈ vars_term (lhs β)"
by (metis subt_at_imp_supteq subteq_Var_imp_in_vars_term vars_term_labeled_lhs)
then obtain i where i:"i < length (var_rule β) ∧ (var_rule β)!i = x"
by (metis in_set_idx set_vars_term_list vars_term_list_vars_distinct)
with l have *:"(⟨map labeled_source As⟩⇩β) x = labeled_source (As!i)"
by (metis (no_types, lifting) length_map lhs_subst_var_i nth_map)
with Prule(3) lab have as_i:"get_label ((labeled_source (As!i))|_p2) = Some (α, length q + n)"
by simp
have p1_above_p:"p1 ≤⇩p p" proof(rule ccontr)
assume "¬ p1 ≤⇩p p"
with p1p2 have "length p < length p1"
by (metis less_eq_pos_simps(1) pos_cases pos_less_eq_append_not_parallel prefix_smaller)
with p1p2 have le:"length p2 < length q"
using length_append by (metis add.commute less_add_eq_less)
with as_i Prule(4) * i l p2 have "length q + n ≤ length p2"
by (metis fun_well_arg label_term_max_value nth_mem)
with le show False by linarith
qed
let ?p'="the (remove_prefix p1 p)"
from p1_above_p p1p2 have p2':"p2 = ?p' @ q"
by (metis append_assoc pos_diff_def prefix_pos_diff same_append_eq)
then have lab':"labeled_source (Prule β As) |_(p1@?p') = (⟨map labeled_source As⟩⇩β) x |_?p'"
using x p1p2 Prule(2) unfolding labeled_source.simps
by (metis (mono_tags, lifting) labeled_source.simps(3) poss_append_poss eval_term.simps(1) subt_at_subst subterm_poss_conv)
from p2' Prule(1,4) p2 * i l as_i have "get_label ((labeled_source (As!i))|_?p') = Some (α, n)"
by (metis fun_well_arg nth_mem)
with lab' * show ?thesis
by (metis p1_above_p pos_diff_def prefix_pos_diff)
qed
qed simp
text‹If a function symbol is labeled with @{term "(α, n)"}, then the function symbol @{term n}
positions above it is labeled with @{term "(α, 0)"}.›
lemma obtain_label_root:
assumes "p ∈ poss (labeled_source A)"
and "get_label ((labeled_source A)|_p) = Some (α, n)"
and "A ∈ wf_pterm R"
shows "get_label ((labeled_source A)|_(take (length p - n) p)) = Some (α, 0) ∧ take (length p - n) p ∈ poss (labeled_source A)"
proof-
from assms have n:"n ≤ length p"
using label_term_max_value by blast
with assms show ?thesis
by (metis (no_types, lifting) add.right_neutral append_take_drop_id diff_diff_cancel label_decrease length_drop poss_append_poss)
qed
lemma label_ctxt_apply_term:
assumes "get_label (labeled_source A |_ p) = l" "q ∈ poss s"
shows "get_label (labeled_source ((ctxt_of_pos_term q (to_pterm s)) ⟨A⟩) |_ (q@p)) = l"
using assms(2) proof(induct s arbitrary:q)
case (Var x)
then have q:"q = []" by simp
from assms(1) show ?case unfolding q by simp
next
case (Fun f ts)
then show ?case proof(cases q)
case Nil
from assms(1) show ?thesis unfolding Nil by simp
next
case (Cons i q')
with Fun(2) have i:"i < length ts" and q':"q' ∈ poss (ts!i)" by auto
with Fun(1) have "get_label (labeled_source (ctxt_of_pos_term q' (to_pterm (ts!i)))⟨A⟩ |_ (q' @ p)) = l" by simp
then show ?thesis
unfolding to_pterm.simps Cons ctxt_of_pos_term.simps labeled_source.simps append_Cons intp_actxt.simps subt_at.simps
by (metis (no_types, lifting) Cons_nth_drop_Suc append_take_drop_id i length_append length_map less_imp_le_nat list.size(4) nth_append_take nth_map)
qed
qed
lemma single_redex_at_p_label:
assumes "p ∈ poss s" and "is_Fun (lhs α)"
shows "get_label (labeled_source (ll_single_redex s p α) |_p) = Some(α, 0)"
proof-
from assms(2) obtain f ts where f:"lhs α = Fun f ts"
by blast
have "get_label (labeled_source (Prule α (map (to_pterm ∘ (λpi. s |_ (p @ pi))) (var_poss_list (lhs α))))) = Some (α, 0)"
unfolding f labeled_source.simps label_term.simps eval_term.simps get_label.simps by simp
then show ?thesis
unfolding ll_single_redex_def using label_ctxt_apply_term[where p="[]"] assms(1)
by (smt (verit) self_append_conv subt_at.simps(1))
qed
text‹Whenever a function symbol at position @{term p} has label @{term "(α, 0)"} or no label in
@{term "labeled_source A"}, then we know that there exists a position @{term q} in @{term A} such
that @{term "A|_q = α(As)"} for appropriate @{term As}.
Moreover, taking the source of the context at position @{term q} must be the same as first computing
the source of @{term A} and then taking the context at @{term p}.›
context left_lin
begin
lemma poss_labeled_source:
assumes "p ∈ poss (labeled_source A)"
and "get_label ((labeled_source A)|_p) = Some (α, 0)"
and "A ∈ wf_pterm R"
shows "∃q ∈ poss A. ctxt_of_pos_term p (source A) = source_ctxt (ctxt_of_pos_term q A) ∧
A|_q = Prule α (map (λi. A|_(q@[i])) [0..<length (var_rule α)])"
using assms proof(induct A arbitrary:p)
case (Var x)
then have "p = []" by simp
with Var(2) have False unfolding labeled_source.simps by simp
then show ?case by blast
next
case (Pfun f As)
then show ?case proof(cases p)
case (Cons i p')
with Pfun(2) have ip':"p = i#p'" and i:"i < length As"
by auto
with Pfun(2) have p':"p' ∈ poss (labeled_source (As!i))"
by simp
from Pfun(3) i ip' have "get_label (labeled_source (As!i) |_ p') = Some (α, 0)"
by simp
with Pfun(1,4) p' i obtain q where q:"q ∈ poss (As!i)" and "ctxt_of_pos_term p' (source (As!i)) = source_ctxt (ctxt_of_pos_term q (As!i))"
and prule:"(As!i)|_q = Prule α (map (λj. (As!i)|_(q@[j])) [0..<length (var_rule α)])"
using nth_mem by blast
then have "ctxt_of_pos_term p (source (Pfun f As)) = source_ctxt (ctxt_of_pos_term (i#q) (Pfun f As))"
unfolding ip' using i by(simp add: take_map drop_map)
then show ?thesis
using q(1) i prule by fastforce
qed simp
next
case (Prule β As)
have l:"length As = length (var_rule β)"
using Prule(4) using wf_pterm.simps by fastforce
from Prule(2) consider "p ∈ fun_poss (labeled_lhs β)" | "(∃p1 p2 x. p = p1@p2
∧ p1 ∈ poss (labeled_lhs β) ∧ (labeled_lhs β)|_p1 = Var x
∧ p2 ∈ poss ((⟨map labeled_source As⟩⇩β) x)
∧ (labeled_source (Prule β As))|_p = ((⟨map labeled_source As⟩⇩β) x)|_p2)"
unfolding labeled_source.simps by (meson poss_is_Fun_fun_poss poss_subst_choice)
then show ?case proof(cases)
case 1
then have "p ∈ fun_poss (lhs β)"
by (simp add: fun_poss_label_term)
then have "get_label ((labeled_source (Prule β As))|_p) = Some (β, length p)"
unfolding labeled_source.simps by (simp add: label_term_increase)
with Prule(3) have p:"p = []" and α:"α = β" by simp+
have "As = (map (λi. Prule β As |_ ([i])) [0..<length As])"
by (simp add: map_nth)
then have "As = (map (λi. Prule β As |_ ([] @ [i])) [0..<length (var_rule α)])"
unfolding α using l by force
then show ?thesis unfolding p α by auto
next
case 2
then obtain p1 p2 x where p1p2:"p = p1 @ p2" and x:"p1 ∈ poss (labeled_lhs β) ∧ labeled_lhs β |_ p1 = Var x"
and p2:"p2 ∈ poss ((⟨map labeled_source As⟩⇩β) x)"
and lab:"labeled_source (Prule β As) |_ p = (⟨map labeled_source As⟩⇩β) x |_ p2"
by blast
from Prule(4) have l:"length As = length (var_rule β)"
using wf_pterm.simps by fastforce
from Prule(4) have "to_rule β ∈ R"
using wf_pterm.cases by force
with left_lin have lin:"linear_term (lhs β)"
using left_linear_trs_def by fastforce
from x have p1:"p1 ∈ poss (lhs β)" by simp
then have p1':"p1 ∈ poss ((lhs β) ⋅ ⟨map source As⟩⇩β)" by simp
from p1 x have x':"lhs β |_ p1 = Var x"
by (metis label_term_to_term labeled_source_pos term_lab_to_term.simps(1))
from p1 x' obtain i where i:"i < length (vars_term_list (lhs β))" "var_poss_list (lhs β) ! i = p1" "vars_term_list (lhs β) ! i = x"
by (metis in_set_idx length_var_poss_list term.inject(1) var_poss_iff var_poss_list_sound vars_term_list_var_poss_list)
with lin have i':"i < length (var_rule β) ∧ (var_rule β)!i = x"
by (metis linear_term_var_vars_term_list)
with l have *:"(⟨map labeled_source As⟩⇩β) x = labeled_source (As!i)"
by (metis (no_types, lifting) length_map lhs_subst_var_i nth_map)
with Prule(3) lab have "get_label ((labeled_source (As!i))|_p2) = Some (α, 0)"
by simp
with Prule(1,4) p2 * i' l obtain q where q:"q∈poss (As!i)" "ctxt_of_pos_term p2 (source (As!i)) = source_ctxt (ctxt_of_pos_term q (As!i))"
"(As!i) |_ q = Prule α (map (λj. (As!i) |_ (q @ [j])) [0..<length (var_rule α)])"
by (smt (verit, ccfv_SIG) fun_well_arg map_eq_conv nth_mem)
have p1'':"(var_poss_list (lhs β) ! length (take i As)) = p1"
using i l by (metis id_take_nth_drop length_take length_var_poss_list lin linear_term_var_vars_term_list nth_append_length)
have x_sub:"Var x ⋅ ⟨map source As⟩⇩β = source (As!i)"
by (metis (no_types, lifting) i' l length_map lhs_subst_var_i nth_map eval_term.simps(1))
have "ctxt_of_pos_term p (source (Prule β As)) = source_ctxt (ctxt_of_pos_term (i#q) (Prule β As))" proof-
{fix y assume "y ∈ vars_term (lhs β)" "y ≠ vars_term_list (lhs β) ! i"
then obtain j where j:"j < length (var_rule β)" "y = (var_rule β) ! j" "j ≠ i"
by (metis in_set_conv_nth lin linear_term_var_vars_term_list set_vars_term_list)
have x:"(vars_term_list (lhs β) ! length (take i As)) = x"
by (metis i' id_take_nth_drop l length_take lin linear_term_var_vars_term_list nth_append_length)
from j have "(⟨map source (take i As @ Var x # drop (Suc i) As)⟩⇩β) y = source (As!j)"
using apply_lhs_subst_var_rule l
by (smt (verit, best) Cons_nth_drop_Suc append_Cons_nth_not_middle append_take_drop_id i' length_append length_map length_nth_simps(2) lin linear_term_var_vars_term_list nth_map x)
then have "(⟨map source (take i As @ Var (vars_term_list (lhs β) ! length (take i As)) # drop (Suc i) As)⟩⇩β) y = (⟨map source As⟩⇩β) y"
unfolding x by (metis (no_types, lifting) j(1,2) l length_map lhs_subst_var_i nth_map)
}
then have *:"ctxt_of_pos_term p1 (lhs β) ⋅⇩c ⟨map source As⟩⇩β =
ctxt_of_pos_term p1 (lhs β ⋅ ⟨map source (take i As @ Var (vars_term_list (lhs β) ! length (take i As)) # drop (Suc i) As)⟩⇩β)"
using i
unfolding ctxt_of_pos_term_subst[OF p1, symmetric]
apply (intro ctxt_of_pos_term_hole_subst[OF lin, of i])
subgoal by (metis length_var_poss_list)
by auto
then show ?thesis
unfolding source.simps p1p2 ctxt_of_pos_term_append[OF p1'] ctxt_of_pos_term_subst[OF p1] subt_at_subst[OF p1] x' ctxt_of_pos_term.simps source_ctxt.simps Let_def x_sub q(2) * p1''
by simp
qed
moreover from q(3) have "Prule β As |_ (i#q) = Prule α (map (λj. Prule β As |_ ((i#q) @ [j])) [0..<length (var_rule α)])"
by simp
ultimately show ?thesis
using i' q(1) l by (metis poss_Cons_poss term.sel(4))
qed
qed
lemma poss_labeled_source_None:
assumes "p ∈ poss (labeled_source A)"
and "get_label ((labeled_source A)|_p) = None"
and "A ∈ wf_pterm R"
shows "∃q ∈ poss A. ctxt_of_pos_term p (source A) = source_ctxt (ctxt_of_pos_term q A)"
using assms proof(induct A arbitrary:p)
case (Pfun f As)
then show ?case proof(cases p)
case (Cons i p')
with Pfun(2) have ip':"p = i#p'" and i:"i < length As"
by auto
with Pfun(2) have p':"p' ∈ poss (labeled_source (As!i))"
by simp
from Pfun(3) have "get_label (labeled_source (As ! i) |_ p') = None"
unfolding ip' labeled_source.simps using i by simp
with Pfun(1,4) p' i obtain q where q:"q ∈ poss (As!i)" and "ctxt_of_pos_term p' (source (As!i)) = source_ctxt (ctxt_of_pos_term q (As!i))"
using nth_mem by blast
then have "ctxt_of_pos_term p (source (Pfun f As)) = source_ctxt (ctxt_of_pos_term (i#q) (Pfun f As))"
unfolding ip' using i by(simp add: take_map drop_map)
then show ?thesis
using q(1) i by fastforce
qed simp
next
case (Prule β As)
have l:"length As = length (var_rule β)"
using Prule(4) using wf_pterm.simps by fastforce
from Prule(2) consider "p ∈ fun_poss (labeled_lhs β)" | "(∃p1 p2 x. p = p1@p2
∧ p1 ∈ poss (labeled_lhs β) ∧ (labeled_lhs β)|_p1 = Var x
∧ p2 ∈ poss ((⟨map labeled_source As⟩⇩β) x)
∧ (labeled_source (Prule β As))|_p = ((⟨map labeled_source As⟩⇩β) x)|_p2)"
unfolding labeled_source.simps by (meson poss_is_Fun_fun_poss poss_subst_choice)
then show ?case proof(cases)
case 1
then have "p ∈ fun_poss (lhs β)"
by (simp add: fun_poss_label_term)
then have "get_label ((labeled_source (Prule β As))|_p) = Some (β, length p)"
unfolding labeled_source.simps by (simp add: label_term_increase)
then show ?thesis
using Prule(3) by simp
next
case 2
then obtain p1 p2 x where p1p2:"p = p1 @ p2" and x:"p1 ∈ poss (labeled_lhs β) ∧ labeled_lhs β |_ p1 = Var x"
and p2:"p2 ∈ poss ((⟨map labeled_source As⟩⇩β) x)"
and lab:"labeled_source (Prule β As) |_ p = (⟨map labeled_source As⟩⇩β) x |_ p2"
by blast
from Prule(4) have l:"length As = length (var_rule β)"
using wf_pterm.simps by fastforce
from Prule(4) have "to_rule β ∈ R"
using wf_pterm.cases by force
with left_lin have lin:"linear_term (lhs β)"
using left_linear_trs_def by fastforce
from x have p1:"p1 ∈ poss (lhs β)" by simp
then have p1':"p1 ∈ poss ((lhs β) ⋅ ⟨map source As⟩⇩β)" by simp
from p1 x have x':"lhs β |_ p1 = Var x"
by (metis label_term_to_term labeled_source_pos term_lab_to_term.simps(1))
from p1 x' obtain i where i:"i < length (vars_term_list (lhs β))" "var_poss_list (lhs β) ! i = p1" "vars_term_list (lhs β) ! i = x"
by (metis in_set_idx length_var_poss_list term.inject(1) var_poss_iff var_poss_list_sound vars_term_list_var_poss_list)
with lin have i':"i < length (var_rule β) ∧ (var_rule β)!i = x"
by (metis linear_term_var_vars_term_list)
with l have *:"(⟨map labeled_source As⟩⇩β) x = labeled_source (As!i)"
by (metis (no_types, lifting) length_map lhs_subst_var_i nth_map)
with Prule(3) lab have "get_label ((labeled_source (As!i))|_p2) = None"
by simp
with Prule(1,4) p2 * i' l obtain q where q:"q∈poss (As!i)" "ctxt_of_pos_term p2 (source (As!i)) = source_ctxt (ctxt_of_pos_term q (As!i))"
by (smt (verit, ccfv_SIG) fun_well_arg map_eq_conv nth_mem)
have p1'':"(var_poss_list (lhs β) ! length (take i As)) = p1"
using i l by (metis id_take_nth_drop length_take length_var_poss_list lin linear_term_var_vars_term_list nth_append_length)
have x_sub:"Var x ⋅ ⟨map source As⟩⇩β = source (As!i)"
by (metis (no_types, lifting) i' l length_map lhs_subst_var_i nth_map eval_term.simps(1))
have "ctxt_of_pos_term p (source (Prule β As)) = source_ctxt (ctxt_of_pos_term (i#q) (Prule β As))" proof-
{fix y assume "y ∈ vars_term (lhs β)" "y ≠ vars_term_list (lhs β) ! i"
then obtain j where j:"j < length (var_rule β)" "y = (var_rule β) ! j" "j ≠ i"
by (metis in_set_conv_nth lin linear_term_var_vars_term_list set_vars_term_list)
have x:"(vars_term_list (lhs β) ! length (take i As)) = x"
by (metis i' id_take_nth_drop l length_take lin linear_term_var_vars_term_list nth_append_length)
from j have "(⟨map source (take i As @ Var x # drop (Suc i) As)⟩⇩β) y = source (As!j)"
using apply_lhs_subst_var_rule l
by (smt (verit, best) Cons_nth_drop_Suc append_Cons_nth_not_middle append_take_drop_id i' length_append length_map length_nth_simps(2) lin linear_term_var_vars_term_list nth_map x)
then have "(⟨map source (take i As @ Var (vars_term_list (lhs β) ! length (take i As)) # drop (Suc i) As)⟩⇩β) y = (⟨map source As⟩⇩β) y"
unfolding x by (metis (no_types, lifting) j(1,2) l length_map lhs_subst_var_i nth_map)
}
then have *:"ctxt_of_pos_term p1 (lhs β) ⋅⇩c ⟨map source As⟩⇩β =
ctxt_of_pos_term p1 (lhs β ⋅ ⟨map source (take i As @ Var (vars_term_list (lhs β) ! length (take i As)) # drop (Suc i) As)⟩⇩β)"
using i
unfolding ctxt_of_pos_term_subst[OF p1, symmetric]
apply (intro ctxt_of_pos_term_hole_subst[OF lin, of i])
subgoal by (metis length_var_poss_list)
by auto
then show ?thesis
unfolding source.simps p1p2 ctxt_of_pos_term_append[OF p1'] ctxt_of_pos_term_subst[OF p1] subt_at_subst[OF p1] x' ctxt_of_pos_term.simps source_ctxt.simps Let_def x_sub q(2) * p1''
by simp
qed
then show ?thesis
using i' q(1) l by (metis poss_Cons_poss term.sel(4))
qed
qed simp
end
text‹If we know that some part of a term does not contain labels (i.e., is coming from a simple
proof term @{term t}) then we know that the label originates below some variable position of @{term t}.›
lemma labeled_source_to_pterm_subst:
assumes p_pos:"p ∈ possL (to_pterm t ⋅ σ)" and well:"∀x ∈ vars_term t. σ x ∈ wf_pterm R"
shows "∃p1 p2 x γ. p1 ∈ poss t ∧ t|_p1 = Var x ∧ p1@p2 ≤⇩p p
∧ p2 ∈ possL (σ x) ∧ get_label ((labeled_source (σ x))|_p2) = Some (γ, 0) "
proof-
{assume p:"p ∈ fun_poss (labeled_source (to_pterm t))"
then have "get_label ((labeled_source (to_pterm t))|_p) = None"
using labeled_source_simple_pterm by (metis empty_iff fun_poss_imp_poss get_label_imp_labelposs)
moreover have "get_label ((labeled_source ((to_pterm t) ⋅ σ))|_p) = get_label ((labeled_source (to_pterm t))|_p)"
by (metis get_label_at_fun_poss_subst labeled_source_apply_subst p to_pterm_wf_pterm)
ultimately have False using p_pos possL_obtain_label by fastforce
}
with p_pos obtain p1 r x where p:"p = p1@r" and p1:"p1 ∈ poss t" and t:"(labeled_source (to_pterm t))|_p1 = Var x"
by (smt (z3) labeled_source_apply_subst labeled_source_to_term possL_subset_poss_source poss_subst_apply_term poss_term_lab_to_term source_to_pterm subset_eq to_pterm_wf_pterm)
then have x:"t|_p1 = Var x"
by (metis labeled_source_pos labeled_source_to_term source_to_pterm term_lab_to_term.simps(1))
from p_pos have r_pos:"r ∈ poss (labeled_source (σ x))"
unfolding p using p1 t labeled_source_apply_subst
by (smt (z3) comp_apply labeled_source_to_term labelposs_subs_poss less_eq_pos_def less_eq_pos_simps(1) p poss_append_poss poss_term_lab_to_term source_to_pterm subset_eq eval_term.simps(1) subt_at_subst to_pterm_wf_pterm)
from p_pos obtain γ n where lab:"get_label ((labeled_source (σ x))|_r) = Some (γ, n)"
unfolding p labeled_source_apply_subst[OF to_pterm_wf_pterm] using t p1 p
by (smt (verit, ccfv_SIG) comp_apply fun_poss_imp_poss labeled_source_to_term labelposs_obtain_label labelposs_subs_fun_poss poss_term_lab_to_term source_to_pterm subset_eq eval_term.simps(1) subt_at_subst subterm_poss_conv)
let ?p2="take (length r - n) r"
have "?p2 ≤⇩p r" by (metis append_take_drop_id less_eq_pos_simps(1))
then have "p1@?p2 ≤⇩p p" unfolding p by simp
moreover have "get_label ((labeled_source (σ x))|_?p2) = Some (γ, 0) ∧ ?p2 ∈ poss (labeled_source (σ x))"
using obtain_label_root[OF r_pos lab] well p1 x by (metis in_mono term.set_intros(3) vars_term_subt_at)
moreover then have "?p2 ∈ possL (σ x)" using get_label_imp_labelposs by blast
ultimately show ?thesis using p1 x by blast
qed
lemma labelposs_subst:
assumes "p ∈ labelposs (t ⋅ σ)"
shows "p ∈ labelposs t ∨ (∃p1 p2 x. p = p1@p2 ∧ p1 ∈ poss t ∧ t|_p1 = Var x ∧ p2 ∈ labelposs (σ x))"
using assms proof(induct t arbitrary:p)
case (Fun fl ts)
then show ?case proof(cases p)
case Nil
from Fun(2) obtain f l where "fl = (f, Some l)"
unfolding eval_term.simps Nil by (metis get_label.simps(2) labelposs_obtain_label subt_at.simps(1) surjective_pairing)
then show ?thesis
unfolding Nil by simp
next
case (Cons i p')
from Fun(2) have i:"i < length ts"
unfolding Cons eval_term.simps using labelposs_subs_poss by fastforce
with Fun(2) have "p' ∈ labelposs (ts!i ⋅ σ)"
unfolding Cons eval_term.simps by (metis (no_types, lifting) get_label_imp_labelposs labelposs_obtain_label labelposs_subs_poss nth_map option.simps(3) poss_Cons_poss subset_eq subt_at.simps(2) term.sel(4))
with Fun(1) i consider "p' ∈ labelposs (ts!i)" | "(∃p1 p2 x. p' = p1 @ p2 ∧ p1 ∈ poss (ts!i) ∧ (ts!i) |_ p1 = Var x ∧ p2 ∈ labelposs (σ x))"
by (meson nth_mem)
then show ?thesis proof(cases)
case 1
with i show ?thesis unfolding Cons
by (metis (no_types, lifting) get_label_imp_labelposs labelposs_obtain_label labelposs_subs_poss option.simps(3) poss_Cons_poss subsetD subt_at.simps(2) term.sel(4))
next
case 2
then obtain p1 p2 x where p':"p' = p1 @ p2" and p1:"p1 ∈ poss (ts ! i)" "ts ! i |_ p1 = Var x" and "p2 ∈ labelposs (σ x)"
by blast
with i show ?thesis unfolding Cons
by (metis append_Cons poss_Cons_poss subt_at.simps(2) term.sel(4))
qed
qed
qed simp
lemma set_labelposs_subst:
"labelposs (t ⋅ σ) = labelposs t ∪ (⋃i< length (vars_term_list t). {(var_poss_list t!i)@q | q. q ∈ labelposs (σ (vars_term_list t ! i))})" (is "?ps = ?qs")
proof
{fix p assume "p ∈ ?ps"
then consider "p ∈ labelposs t" | "(∃p1 p2 x. p = p1@p2 ∧ p1 ∈ poss t ∧ t|_p1 = Var x ∧ p2 ∈ labelposs (σ x))"
using labelposs_subst by blast
then have "p ∈ ?qs" proof(cases)
case 2
then obtain p1 p2 x where "p = p1@p2 ∧ p1 ∈ poss t ∧ t|_p1 = Var x ∧ p2 ∈ labelposs (σ x)"
by blast
moreover then obtain i where i:"i < length (vars_term_list t)" "vars_term_list t ! i = x" "var_poss_list t ! i = p1"
by (metis in_set_idx length_var_poss_list term.inject(1) var_poss_iff var_poss_list_sound vars_term_list_var_poss_list)
ultimately have "p ∈ {var_poss_list t ! i @ q |q. q ∈ labelposs (σ (vars_term_list t ! i))}"
by blast
with i(1) show ?thesis
by blast
qed simp
}
then show "?ps ⊆ ?qs"
by blast
{fix q assume "q ∈ ?qs"
then consider "q ∈ labelposs t" | "q ∈ (⋃i< length (vars_term_list t). {(var_poss_list t!i)@q | q. q ∈ labelposs (σ (vars_term_list t ! i))})"
by blast
then have "q ∈ ?ps" proof(cases)
case 1
then show ?thesis proof(induct t arbitrary:q)
case (Fun f ts)
then show ?case proof(cases q)
case Nil
with Fun(2) obtain f' lab where f':"f = (f', Some lab)"
by (metis get_label.simps(2) labelposs_obtain_label prod.exhaust_sel subt_at.simps(1))
show ?thesis unfolding Nil f' by simp
next
case (Cons i q')
obtain f' lab where f':"f = (f', lab)"
by fastforce
show ?thesis proof(cases lab)
case None
from Fun(2) have i:"i < length ts"
unfolding f' Cons None labelposs.simps by simp
from Fun(2) have "q' ∈ labelposs (ts!i)"
unfolding f' Cons None by simp
with Fun(1) i have "q' ∈ labelposs (ts!i ⋅ σ)"
by simp
with i show ?thesis
unfolding f' Cons None eval_term.simps labelposs.simps by simp
next
case (Some a)
from Fun(2) have i:"i < length ts"
unfolding f' Cons Some labelposs.simps by simp
from Fun(2) have "q' ∈ labelposs (ts!i)"
unfolding f' Cons Some by simp
with Fun(1) i have "q' ∈ labelposs (ts!i ⋅ σ)"
by simp
with i show ?thesis
unfolding f' Cons Some eval_term.simps labelposs.simps by simp
qed
qed
qed simp
next
case 2
then show ?thesis proof(induct t arbitrary:q)
case (Var x)
have "var_poss_list (Var x) = [[]]"
unfolding poss_list.simps var_poss.simps by simp
with Var show ?case unfolding vars_term_list.simps
by (smt (verit, ccfv_SIG) One_nat_def UN_iff bot_nat_0.not_eq_extremum length_0_conv length_nth_simps(2) lessThan_iff mem_Collect_eq not_less_eq nth_Cons_0 self_append_conv2 eval_term.simps(1))
next
case (Fun fl ts)
from Fun(2) obtain i q' where q:"q = var_poss_list (Fun fl ts) ! i @ q'" "q' ∈ labelposs (σ (vars_term_list (Fun fl ts) ! i))" and i:"i < length (vars_term_list (Fun fl ts))"
by blast
then have i':"i < length (var_poss_list (Fun fl ts))"
by (metis length_var_poss_list)
then obtain j r where j:"j < length ts" "var_poss_list (Fun fl ts) ! i = j#r"
unfolding var_poss_list.simps by (smt (z3) add.left_neutral diff_zero length_map length_upt length_zip map_nth_eq_conv min.idem nth_concat_split nth_upt nth_zip prod.simps(2))
with i obtain x where x:"Fun fl ts |_(j#r) = Var x"
by (metis vars_term_list_var_poss_list)
from j i' have "j#r ∈ var_poss (Fun fl ts)"
by (metis nth_mem var_poss_list_sound)
then have "r ∈ var_poss (ts!j)"
by simp
then obtain i' where r:"i'<length (var_poss_list (ts!j))" "r = var_poss_list (ts!j) ! i'"
by (metis in_set_conv_nth var_poss_list_sound)
moreover then have "(vars_term_list (Fun fl ts) ! i) = (vars_term_list (ts!j) ! i')"
using x by (metis i j(2) length_var_poss_list subt_at.simps(2) term.inject(1) vars_term_list_var_poss_list)
ultimately have "r@q' ∈ (⋃i<length (vars_term_list (ts!j)). {var_poss_list (ts!j) ! i @ q |q. q ∈ labelposs (σ (vars_term_list (ts!j) ! i))})"
using q(2) unfolding length_var_poss_list by auto
with Fun(1) j(1) have r_pos:"r@q' ∈ labelposs ((ts!j) ⋅ σ)"
using nth_mem by blast
obtain f lab where f:"fl = (f, lab)"
using surjective_pairing by blast
then show ?case proof(cases lab)
case None
from r_pos have "j#r@q' ∈ labelposs (Fun fl ts ⋅ σ)"
unfolding eval_term.simps f None labelposs.simps length_map using j(1) by simp
then show ?thesis unfolding q j(2) by simp
next
case (Some a)
from r_pos have "j#r@q' ∈ labelposs (Fun fl ts ⋅ σ)"
unfolding eval_term.simps f Some labelposs.simps length_map using j(1) by simp
then show ?thesis unfolding q j(2) by simp
qed
qed
qed
}
then show "?qs ⊆ ?ps"
by blast
qed
text‹The labeled positions in a proof term @{term "Prule α As"} are the function positions of
@{term "lhs α"} together with all labeled positions in the arguments @{term As}.›
lemma possl_rule:
assumes "length As = length (var_rule α)" "linear_term (lhs α)"
shows "possL (Prule α As) = fun_poss (lhs α) ∪ (⋃i< (length As). {(var_poss_list (lhs α)!i)@q | q. q ∈ possL(As!i)})"
proof-
from assms(1,2) have l:"length (vars_term_list (labeled_lhs α)) = length As"
by (metis linear_term_var_vars_term_list vars_term_list_labeled_lhs)
have "labelposs (labeled_lhs α) = fun_poss (lhs α)"
by (metis fun_poss_term_lab_to_term label_poss_labeled_lhs label_term_to_term labelposs_subs_fun_poss subsetI subset_antisym)
moreover from assms(1,2) have "i < length As ⟹ (⟨map labeled_source As⟩⇩α) (vars_term_list (labeled_lhs α) ! i) = labeled_source (As!i)" for i
using lhs_subst_var_i linear_term_var_vars_term_list by (smt (verit, best) length_map nth_map vars_term_list_labeled_lhs)
ultimately show ?thesis using set_labelposs_subst[of "labeled_lhs α"] unfolding l var_poss_list_labeled_lhs by force
qed
lemma labelposs_subs_fun_poss_source:
assumes "p ∈ possL A"
shows "p ∈ fun_poss (source A)"
proof-
have "p ∈ fun_poss (labeled_source A)"
using assms labelposs_subs_fun_poss by blast
then show ?thesis using fun_poss_term_lab_to_term
by auto
qed
text‹The labeled source of a context (obtained from some proof term @{term A}) applied to some proof
term @{term B} is the labeled source of the context applied to the labeled source of the proof term
@{term B}.›
context left_lin
begin
lemma label_source_ctxt:
assumes "A ∈ wf_pterm R"
and "ctxt_of_pos_term p (source A) = source_ctxt (ctxt_of_pos_term p' A)"
and "p ∈ poss (source A)" and "p' ∈ poss A"
shows "labeled_source (ctxt_of_pos_term p' A)⟨B⟩ = (ctxt_of_pos_term p (labeled_source A))⟨labeled_source B⟩"
using assms proof(induct p' arbitrary:p A)
case Nil
then have p:"p = []"
using hole_pos_ctxt_of_pos_term by force
then show ?case by simp
next
case (Cons i p')
then obtain fl As where a:"A = Fun fl As" and i:"i < length As" and p':"p' ∈ poss (As!i)"
by (meson args_poss)
then show ?case proof(cases fl)
case (Inl α)
from Cons(2) have l:"length As = length (var_rule α)"
unfolding a Inl using wf_pterm.cases by auto
have "to_rule α ∈ R"
using Cons(2) unfolding a Inl using wf_pterm.cases by force
with left_lin have lin:"linear_term (lhs α)"
using left_linear_trs_def by fastforce
let ?p1="var_poss_list (lhs α) ! i"
from i l lin have p1:"(lhs α)|_?p1 = Var (var_rule α ! i)"
by (metis linear_term_var_vars_term_list vars_term_list_var_poss_list)
from i l have p1_pos:"?p1 ∈ poss (lhs α)"
by (metis comp_apply length_remdups_leq length_rev length_var_poss_list nth_mem order_less_le_trans var_poss_imp_poss var_poss_list_sound)
let ?p2="hole_pos (source_ctxt (ctxt_of_pos_term p' (As ! i)))"
have "hole_pos (source_ctxt (ctxt_of_pos_term (i # p') A)) = ?p1@?p2"
unfolding a Inl source.simps ctxt_of_pos_term.simps source_ctxt.simps Let_def hole_pos_ctxt_compose using p1_pos Cons(5) a by force
with Cons(3) have p:"p = ?p1@?p2"
by (metis Cons.prems(3) hole_pos_ctxt_of_pos_term)
have at_p1:"(source A)|_?p1 = source (As!i)"
unfolding a Inl source.simps using p1
by (smt (verit, best) Inl i l length_map lhs_subst_var_i nth_map p1_pos eval_term.simps(1) subt_at_subst)
with Cons(4) have p2_pos:"?p2 ∈ poss (source (As!i))"
unfolding p by simp
from at_p1 have *:"ctxt_of_pos_term p (source A) = (ctxt_of_pos_term ?p1 (source A) ∘⇩c (ctxt_of_pos_term ?p2 (source (As ! i))))"
unfolding p using ctxt_of_pos_term_append using Cons.prems(3) p by fastforce
from Cons(3) have "ctxt_of_pos_term ?p2 (source (As!i)) = source_ctxt (ctxt_of_pos_term p' (As!i))"
unfolding * unfolding a Inl source.simps ctxt_of_pos_term.simps source_ctxt.simps Let_def using ctxt_comp_equals Cons(5) p1_pos
by (smt (verit, ccfv_SIG) a ctxt_of_pos_term.simps(2) hole_pos.simps(2) hole_pos_ctxt_of_pos_term list.inject poss_imp_subst_poss)
with Cons(1,2) i p2_pos p' a Inl have IH:"labeled_source (ctxt_of_pos_term p' (As!i))⟨B⟩ = (ctxt_of_pos_term ?p2 (labeled_source (As!i)))⟨labeled_source B⟩"
by (meson fun_well_arg nth_mem)
then have list_IH:"map labeled_source (take i As @ (ctxt_of_pos_term p' (As ! i))⟨B⟩ # drop (Suc i) As) =
map labeled_source (take i As) @ (ctxt_of_pos_term ?p2 (labeled_source (As ! i)))⟨labeled_source B⟩ # map labeled_source (drop (Suc i) As)"
using i by fastforce
from lin have lin':"linear_term (labeled_lhs α)"
using linear_label_term by blast
from p1_pos have p1_pos:"?p1 ∈ poss (labeled_lhs α)"
by simp
from p1 have x:"labeled_lhs α |_ var_poss_list (lhs α) ! i = Var (var_rule α ! i)"
by (metis label_term_to_term p1_pos poss_term_lab_to_term var_label_term)
have "(⟨map labeled_source As⟩⇩α)((var_rule α ! i) := (ctxt_of_pos_term ?p2 ((⟨map labeled_source As⟩⇩α) (var_rule α ! i)))⟨labeled_source B⟩)
= ⟨(take i (map labeled_source As)) @ (ctxt_of_pos_term ?p2 (labeled_source (As!i)))⟨labeled_source B⟩ # (drop (Suc i) (map labeled_source As))⟩⇩α"
using i by (smt (verit, best) Cons.prems(4) a ctxt_of_pos_term.simps(2) hole_pos.simps(2) hole_pos_ctxt_of_pos_term id_take_nth_drop l length_map lhs_subst_upd lhs_subst_var_i list.inject nth_map take_map)
then show ?thesis unfolding a Inl ctxt_of_pos_term.simps labeled_source.simps intp_actxt.simps p list_IH
using replace_at_append_subst[OF lin' p1_pos x] by (smt (verit) drop_map take_map)
next
case (Inr f)
from Cons(3,4,5) obtain p2 where p:"p = i#p2" and p2:"p2 ∈ poss (source (As!i))" and ctxt:"ctxt_of_pos_term p2 (source (As!i)) = source_ctxt (ctxt_of_pos_term p' (As!i))"
unfolding a Inr source.simps ctxt_of_pos_term.simps source_ctxt.simps by (smt (verit, best) Cons.prems(2) Cons.prems(3) Inr a actxt.inject ctxt_of_pos_term.simps(2) i nth_map source_poss)
from Cons(1,2) ctxt p2 p' have IH:"labeled_source (ctxt_of_pos_term p' (As!i))⟨B⟩ = (ctxt_of_pos_term p2 (labeled_source (As!i)))⟨labeled_source B⟩"
using a i nth_mem by blast
then have list_IH:"map labeled_source (take i As @ (ctxt_of_pos_term p' (As ! i))⟨B⟩ # drop (Suc i) As) =
map labeled_source (take i As) @ (ctxt_of_pos_term p2 (labeled_source (As ! i)))⟨labeled_source B⟩ # map labeled_source (drop (Suc i) As)"
using i by fastforce
show ?thesis unfolding a Inr ctxt_of_pos_term.simps p labeled_source.simps intp_actxt.simps list_IH
by (simp add: drop_map i take_map)
qed
qed
end
lemma labeled_ctxt_above:
assumes "p ∈ poss A" and "r ∈ poss A" and "¬ p ≤⇩p r"
shows "get_label ((ctxt_of_pos_term p A)⟨labeled_source B⟩ |_r) = get_label (A |_r)"
using assms proof(induct A arbitrary:r p)
case (Fun f As)
then have "p ≠ []"
by blast
with Fun(2) obtain i p' where i:"i < length As" and p':"p' ∈ poss (As!i)" and p:"p = i#p'"
by auto
from Fun(4) consider "r <⇩p p" | "r ⊥ p"
using parallel_pos by fastforce
then show ?case proof(cases)
case 1
then show ?thesis proof(cases r)
case Nil
show ?thesis unfolding p Nil by simp
next
case (Cons j r')
from 1 have j:"j = i"
unfolding p Cons by simp
with Fun(1) have "get_label ((ctxt_of_pos_term p' (As!i))⟨labeled_source B⟩ |_ r') = get_label ((As!i) |_ r')"
using i p' Fun(3,4) unfolding Cons j p by simp
then show ?thesis
unfolding Cons p subt_at.simps ctxt_of_pos_term.simps intp_actxt.simps by (metis i j nat_less_le nth_append_take)
qed
next
case 2
then obtain j r' where r:"r = j#r'"
unfolding p by (metis parallel_pos.elims(2))
then show ?thesis proof(cases "i = j")
case True
from Fun(1) 2 i have "get_label ((ctxt_of_pos_term p' (As!i))⟨labeled_source B⟩ |_ r') = get_label ((As!i) |_ r')"
using Fun.prems(2) Fun.prems(3) True p p' r by force
then show ?thesis using p r True
by (metis "2" Fun.prems(1) Fun.prems(2) parallel_pos parallel_replace_at_subt_at)
next
case False
then show ?thesis
unfolding p r subt_at.simps ctxt_of_pos_term.simps intp_actxt.simps by (metis i nth_list_update upd_conv_take_nth_drop)
qed
qed
qed simp
text‹The labeled positions of a context (obtained from some proof term @{term A}) applied to some
proof term @{term B} are the labeled positions of the context together with the labeled positions of
the proof term @{term B}.›
context left_lin
begin
lemma label_ctxt:
assumes "A ∈ wf_pterm R"
and "ctxt_of_pos_term p (source A) = source_ctxt (ctxt_of_pos_term p' A)"
and "p ∈ poss (source A)" and "p' ∈ poss A"
shows "possL (ctxt_of_pos_term p' A)⟨B⟩ = {q. q ∈ possL A ∧ ¬p ≤⇩p q} ∪ {p@q| q. q ∈ possL B}"
using assms proof(induct p' arbitrary:p A)
case Nil
then have p:"p = []"
using hole_pos_ctxt_of_pos_term by force
then have "{q ∈ possL A. ¬ p ≤⇩p q} = {}"
by simp
then show ?case
unfolding Nil ctxt_of_pos_term.simps p by simp
next
case (Cons i p')
then obtain fl As where a:"A = Fun fl As" and i:"i < length As" and p':"p' ∈ poss (As!i)"
by (meson args_poss)
then show ?case proof(cases fl)
case (Inl α)
from Cons(2) have l:"length As = length (var_rule α)"
unfolding a Inl using wf_pterm.cases by auto
have "to_rule α ∈ R"
using Cons(2) unfolding a Inl using wf_pterm.cases by force
with left_lin have lin:"linear_term (lhs α)"
using left_linear_trs_def by fastforce
let ?p1="var_poss_list (lhs α) ! i"
from i l lin have p1:"(lhs α)|_?p1 = Var (var_rule α ! i)"
by (metis linear_term_var_vars_term_list vars_term_list_var_poss_list)
from i l have p1_pos:"?p1 ∈ poss (lhs α)"
by (metis comp_apply length_remdups_leq length_rev length_var_poss_list nth_mem order_less_le_trans var_poss_imp_poss var_poss_list_sound)
let ?p2="hole_pos (source_ctxt (ctxt_of_pos_term p' (As ! i)))"
have "hole_pos (source_ctxt (ctxt_of_pos_term (i # p') A)) = ?p1@?p2"
unfolding a Inl source.simps ctxt_of_pos_term.simps source_ctxt.simps Let_def hole_pos_ctxt_compose using p1_pos Cons(5) a by force
with Cons(3) have p:"p = ?p1@?p2"
by (metis Cons.prems(3) hole_pos_ctxt_of_pos_term)
have at_p1:"(source A)|_?p1 = source (As!i)"
unfolding a Inl source.simps using p1
by (smt (verit, best) Inl i l length_map lhs_subst_var_i nth_map p1_pos eval_term.simps(1) subt_at_subst)
with Cons(4) have p2_pos:"?p2 ∈ poss (source (As!i))"
unfolding p by simp
from at_p1 have *:"ctxt_of_pos_term p (source A) = (ctxt_of_pos_term ?p1 (source A) ∘⇩c (ctxt_of_pos_term ?p2 (source (As ! i))))"
unfolding p using ctxt_of_pos_term_append using Cons.prems(3) p by fastforce
from Cons(3) have "ctxt_of_pos_term ?p2 (source (As!i)) = source_ctxt (ctxt_of_pos_term p' (As!i))"
unfolding * unfolding a Inl source.simps ctxt_of_pos_term.simps source_ctxt.simps Let_def using ctxt_comp_equals Cons(5) p1_pos
by (smt (verit, ccfv_SIG) a ctxt_of_pos_term.simps(2) hole_pos.simps(2) hole_pos_ctxt_of_pos_term list.inject poss_imp_subst_poss)
with Cons(1,2) i p2_pos p' a Inl have IH:"possL (ctxt_of_pos_term p' (As!i))⟨B⟩ = {q ∈ possL (As!i). ¬ ?p2 ≤⇩p q} ∪ {?p2 @ q |q. q ∈ possL B}"
by (meson fun_well_arg nth_mem)
let ?a1="fun_poss (lhs α)"
let ?a2="(⋃j ∈ {k. k < length As ∧ k ≠ i}. {(var_poss_list (lhs α)!j)@q | q. q ∈ possL(As!j)})"
let ?a3="{?p1@q | q. q ∈ possL (As!i) ∧ ¬ ?p2 ≤⇩p q}"
let ?a4="{?p1 @ ?p2 @ q |q. q ∈ possL B}"
let ?b1="{q ∈ possL A. ¬ p ≤⇩p q}"
have "?a1 ∪ ?a2 ∪ ?a3 = ?b1" proof
{fix x assume x:"x ∈ ?a1"
then have "¬ ?p1 ≤⇩p x"
by (metis append.right_neutral fun_poss_append_poss fun_poss_fun_conv fun_poss_imp_poss p1 prefix_pos_diff term.distinct(1))
then have "¬ p ≤⇩p x"
unfolding p using less_eq_pos_simps(1) order_pos.order.trans by blast
with x have "x ∈ ?b1"
unfolding a Inl using possl_rule l lin by auto
} moreover {fix x assume "x ∈ ?a2"
then obtain j q where j:"j < length As" "j ≠ i" and q:"q ∈ possL (As ! j)" and x:"x = var_poss_list (lhs α) ! j @ q"
by blast
from j have j':"j < length (var_poss_list (lhs α))"
using l lin by (metis length_var_poss_list linear_term_var_vars_term_list)
with j(2) have "?p1 ≠ (var_poss_list (lhs α)) !j"
by (metis (mono_tags, lifting) distinct_remdups distinct_rev i j(1) l lin linear_term_var_vars_term_list nth_eq_iff_index_eq o_apply term.inject(1) vars_term_list_var_poss_list)
with j' have "?p1 ⊥ var_poss_list (lhs α) ! j"
using var_poss_parallel by (metis nth_mem p1 p1_pos var_poss_iff var_poss_list_sound)
then have "¬ p ≤⇩p x"
unfolding p x using less_eq_pos_simps(1) order_pos.order_trans pos_less_eq_append_not_parallel by blast
then have "x ∈ ?b1"
unfolding a Inl possl_rule[OF l lin] x using j(1) q by blast
} moreover {fix x assume "x ∈ ?a3"
then obtain q where x:"x = ?p1@q" "q ∈ possL (As ! i)" "¬ ?p2 ≤⇩p q"
by blast
from x(3) have "¬ p ≤⇩p x"
unfolding p x(1) using less_eq_pos_simps(2) by blast
with x(2) have "x ∈ ?b1"
unfolding a Inl possl_rule[OF l lin] x(1) using i by auto
}
ultimately show "?a1 ∪ ?a2 ∪ ?a3 ⊆ ?b1" by blast
{fix x assume b1:"x ∈ ?b1"
then consider "x ∈ fun_poss (lhs α)" | "x ∈ (⋃i<length As. {var_poss_list (lhs α) ! i @ q |q. q ∈ possL (As ! i)})"
unfolding a Inl possl_rule[OF l lin] by blast
then have "x ∈ ?a1 ∪ ?a2 ∪ ?a3" proof(cases)
case 2
then obtain j q where j:"j < length As" and x:"x = var_poss_list (lhs α) ! j @ q" and q:"q ∈ possL (As!j)"
by blast
then show ?thesis proof(cases "j = i")
case True
from b1 have "¬ ?p2 ≤⇩p q"
unfolding p x True using less_eq_pos_simps(2) by blast
then show ?thesis using j x q by auto
qed auto
qed simp
}
then show "?b1 ⊆ ?a1 ∪ ?a2 ∪ ?a3" by blast
qed
moreover have "possL (ctxt_of_pos_term (i # p') A)⟨B⟩ = ?a1 ∪ ?a2 ∪ ?a3 ∪ ?a4" proof-
from l i have l':"length (take i As @ (ctxt_of_pos_term p' (As ! i))⟨B⟩ # drop (Suc i) As) = length (var_rule α)"
by simp
have set:"{j. j < length As} = {j. j < length As ∧ j ≠ i} ∪ {i}"
using i Collect_disj_eq by auto
let ?args="(take i As @ (ctxt_of_pos_term p' (As ! i))⟨B⟩ # drop (Suc i) As)"
{fix j assume "j < length As ∧ j ≠ i"
with i have "?args ! j = As!j"
by (meson nat_less_le nth_append_take_drop_is_nth_conv)
} moreover have "?args!i = (ctxt_of_pos_term p' (As ! i))⟨B⟩" using i
by (simp add: nth_append_take)
moreover from set have "(⋃j<length As. {var_poss_list (lhs α) ! j @ q |q. q ∈ possL (?args ! j)}) =
(⋃j ∈ {j. j < length As ∧ j ≠ i}. {var_poss_list (lhs α) ! j @ q |q. q ∈ possL (?args ! j)}) ∪ {?p1 @ q |q. q ∈ possL (?args!i)}"
by force
ultimately have "(⋃j<length As. {var_poss_list (lhs α) ! j @ q |q. q ∈ possL (?args ! j)}) =
(⋃j ∈ {j. j < length As ∧ j ≠ i}. {var_poss_list (lhs α) ! j @ q |q. q ∈ possL (As ! j)}) ∪ {?p1 @ q |q. q ∈ possL (ctxt_of_pos_term p' (As ! i))⟨B⟩}"
by simp
moreover have "possL (ctxt_of_pos_term (i # p') A)⟨B⟩ = fun_poss (lhs α) ∪
(⋃j<length As. {var_poss_list (lhs α) ! j @ q |q. q ∈ possL (?args ! j)})"
unfolding a Inl ctxt_of_pos_term.simps intp_actxt.simps using possl_rule[OF l' lin] i by force
ultimately show ?thesis unfolding IH by auto
qed
ultimately show ?thesis using p by force
next
case (Inr f)
from Cons(3,4,5) obtain p2 where p:"p = i#p2" and "p2 ∈ poss (source (As!i))" and ctxt:"ctxt_of_pos_term p2 (source (As!i)) = source_ctxt (ctxt_of_pos_term p' (As!i))"
unfolding a Inr source.simps ctxt_of_pos_term.simps source_ctxt.simps by (smt (verit, best) Cons.prems(2) Cons.prems(3) Inr a actxt.inject ctxt_of_pos_term.simps(2) i nth_map source_poss)
with Cons(1,2) i p' have IH:"possL (ctxt_of_pos_term p' (As!i))⟨B⟩ = {q ∈ possL (As!i). ¬ p2 ≤⇩p q} ∪ {p2 @ q |q. q ∈ possL B}"
unfolding a Inr by (meson fun_well_arg nth_mem)
let ?a2="(⋃j ∈ {k. k < length As ∧ k ≠ i}. {j # q | q. q ∈ possL(As!j)})"
let ?a3="{i#q | q. q ∈ possL (As!i) ∧ ¬ p2 ≤⇩p q}"
let ?a4="{i # p2 @ q |q. q ∈ possL B}"
let ?b1="{q ∈ possL A. ¬ p ≤⇩p q}"
have "?a2 ∪ ?a3 = ?b1" proof
{fix x assume "x ∈ ?a2"
then obtain j q where j:"j < length As" "j ≠ i" and q:"q ∈ possL (As ! j)" and x:"x = j # q"
by blast
from j q have "j#q ∈ possL A"
unfolding a Inr by simp
then have "x ∈ ?b1"
unfolding x p using j(2) by simp
} moreover {fix x assume "x ∈ ?a3"
then obtain q where x:"x = i#q" "q ∈ possL (As ! i)" "¬ p2 ≤⇩p q"
by blast
from x(3) have "¬ p ≤⇩p x"
unfolding p x(1) using less_eq_pos_simps(2) by simp
with x(2) have "x ∈ ?b1"
unfolding a Inr x(1) using i by auto
}
ultimately show "?a2 ∪ ?a3 ⊆ ?b1" by blast
{fix x assume b1:"x ∈ ?b1"
then have "x ∈ possL A"
by simp
then obtain j q where j:"j < length As" and x:"x = j # q" and q:"q ∈ possL (As!j)"
unfolding a Inr labeled_source.simps labelposs.simps length_map by force
then have "x ∈ ?a2 ∪ ?a3" proof(cases "j = i")
case True
with b1 have "¬ p2 ≤⇩p q"
unfolding p x using less_eq_pos_simps(2) by simp
then show ?thesis using j x q b1 by auto
qed simp
}
then show "?b1 ⊆ ?a2 ∪ ?a3" by blast
qed
moreover have "possL (ctxt_of_pos_term (i # p') A)⟨B⟩ = ?a2 ∪ ?a3 ∪ ?a4" proof-
have l:"length (take i As @ (ctxt_of_pos_term p' (As ! i))⟨B⟩ # drop (Suc i) As) = length As"
using i by simp
{fix j assume "j < length As"
then have "(map labeled_source (take i As @ (ctxt_of_pos_term p' (As ! i))⟨B⟩ # drop (Suc i) As) ! j) = labeled_source ((take i As @ (ctxt_of_pos_term p' (As ! i))⟨B⟩ # drop (Suc i) As) ! j)"
using nth_map l by metis
}note map_lab=this
have set:"{j. j < length As} = {j. j < length As ∧ j ≠ i} ∪ {i}"
using i Collect_disj_eq by auto
let ?args="(take i As @ (ctxt_of_pos_term p' (As ! i))⟨B⟩ # drop (Suc i) As)"
{fix j assume "j < length As ∧ j ≠ i"
with i have "?args ! j = As!j"
by (meson nat_less_le nth_append_take_drop_is_nth_conv)
} moreover have "?args!i = (ctxt_of_pos_term p' (As ! i))⟨B⟩" using i
by (simp add: nth_append_take)
moreover from set have "(⋃j<length As. {j # q |q. q ∈ possL (?args ! j)}) =
(⋃j ∈ {j. j < length As ∧ j ≠ i}. {j # q |q. q ∈ possL (?args ! j)}) ∪ {i # q |q. q ∈ possL (?args!i)}"
by force
ultimately have "(⋃j<length As. {j # q |q. q ∈ possL (?args ! j)}) =
(⋃j ∈ {j. j < length As ∧ j ≠ i}. {j # q |q. q ∈ possL (As ! j)}) ∪ {i # q |q. q ∈ possL (ctxt_of_pos_term p' (As ! i))⟨B⟩}"
by simp
moreover have "possL (ctxt_of_pos_term (i # p') A)⟨B⟩ = (⋃j<length As. {j # q |q. q ∈ possL (?args ! j)})"
unfolding a Inr ctxt_of_pos_term.simps intp_actxt.simps labeled_source.simps labelposs.simps length_map l using map_lab by force
ultimately show ?thesis unfolding IH by auto
qed
ultimately show ?thesis using p by force
qed
qed
lemma single_redex_possL:
assumes "to_rule α ∈ R" "p ∈ poss s"
shows "possL (ll_single_redex s p α) = {p @ q |q. q ∈ fun_poss (lhs α)}"
proof-
let ?Δ="ll_single_redex s p α"
have *:"possL (Prule α (map (to_pterm ∘ (λpi. s|_(p@pi))) (var_poss_list (lhs α)))) = labelposs (labeled_lhs α)"
proof-
{fix x
have "labelposs ((⟨map labeled_source (map (to_pterm ∘ (λpi. s |_ (p @ pi))) (var_poss_list (lhs α)))⟩⇩α) x) = {}"
by (smt (verit) comp_apply labeled_source_simple_pterm labelposs.simps(1) length_map lhs_subst_not_var_i lhs_subst_var_i map_nth_eq_conv)
}
then show ?thesis unfolding labeled_source.simps labelposs_apply_subst by blast
qed
have "possL ?Δ = {q ∈ possL (to_pterm s). ¬ p ≤⇩p q} ∪ {p @ q |q. q ∈ possL (Prule α (map (to_pterm ∘ (λpi. s|_(p@pi))) (var_poss_list (lhs α))))}"
using label_ctxt assms by (simp add: ll_single_redex_def p_in_poss_to_pterm source_ctxt_to_pterm)
also have "...= {p @ q |q. q ∈ possL (Prule α (map (to_pterm ∘ (λpi. s|_(p@pi))) (var_poss_list (lhs α))))}"
using labeled_source_simple_pterm by auto
also have "...= {p @ q |q. q ∈ labelposs (labeled_lhs α)}"
unfolding * by simp
finally show ?thesis
using label_poss_labeled_lhs labelposs_subs_fun_poss by fastforce
qed
end
lemma labeled_poss_in_lhs:
assumes p_pos:"p ∈ poss (source (Prule α As))" and well:"Prule α As ∈ wf_pterm R"
and "get_label ((labeled_source (Prule α As))|_p) = Some (α, length p)" "is_Fun (lhs α)"
shows "p ∈ fun_poss (lhs α)"
proof-
from p_pos consider "p ∈ fun_poss (lhs α)" | "∃p1 p2 x. p = p1 @ p2 ∧ p1 ∈ poss (lhs α) ∧ (lhs α)|_p1 = Var x ∧ p2 ∈ poss ((⟨map source As⟩⇩α) x)"
unfolding source.simps using poss_subst_apply_term by metis
then show ?thesis proof(cases)
case 2
then obtain p1 p2 x where p:"p = p1 @ p2" and p1:"p1 ∈ poss (lhs α)" "(lhs α)|_p1 = Var x" and p2:"p2 ∈ poss ((⟨map source As⟩⇩α) x)"
by blast
then obtain i where i:"i < length (var_rule α)" "var_rule α!i = x"
by (metis in_set_conv_nth set_vars_term_list subt_at_imp_supteq subteq_Var_imp_in_vars_term vars_term_list_vars_distinct)
from p1 have p1_pos':"p1 ∈ poss (labeled_lhs α)"
by simp
from p1 have p1_pos:"p1 ∈ poss (labeled_lhs α ⋅ ⟨map labeled_source As⟩⇩α)"
by (metis labeled_source.simps(3) labeled_source_to_term p p_pos poss_append_poss poss_term_lab_to_term)
from p1 have x:"labeled_lhs α |_p1 = Var x"
by (metis fun_poss_term_lab_to_term label_term_to_term labeled_source_pos poss_simps(4) poss_term_lab_to_term term.sel(1) term_lab_to_term.simps(1) var_poss_iff)
from well have l:"length As = length (var_rule α)"
using wf_pterm.cases by auto
with well i have asi:"As!i ∈ wf_pterm R"
by (metis fun_well_arg nth_mem)
from l have lab:"labeled_source (Prule α As) |_p = labeled_source (As!i) |_p2"
unfolding p labeled_source.simps subt_at_append[OF p1_pos] subt_at_subst[OF p1_pos'] x using i
by (metis (no_types, lifting) length_map lhs_subst_var_i nth_map eval_term.simps(1))
moreover from assms(4) p1 have "length p2 < length p"
unfolding p by auto
moreover from p2 have "p2 ∈ poss (labeled_source (As!i))"
using l i by (metis (no_types, lifting) labeled_source_to_term length_map lhs_subst_var_i nth_map poss_term_lab_to_term)
ultimately have False using assms(3) asi by (simp add: label_term_max_value leD)
then show ?thesis by simp
qed simp
qed
context left_lin_no_var_lhs
begin
lemma get_label_Prule:
assumes "Prule α As ∈ wf_pterm R" and "p ∈ poss (source (Prule α As))" and "get_label (labeled_source (Prule α As) |_ p) = Some (β, 0)"
shows "(p = [] ∧ α = β) ∨
(∃ p1 p2 i. p = p1@p2 ∧ i < length As ∧ var_poss_list (lhs α)!i = p1 ∧
p2 ∈ poss (source (As!i)) ∧ get_label (labeled_source (As!i)|_p2) = Some (β, 0))"
proof-
from assms(1) have α:"to_rule α ∈ R"
using wf_pterm.simps by fastforce
with no_var_lhs obtain f ts where lhs:"lhs α = Fun f ts" by fastforce
from assms(1) have l1:"length (var_rule α) = length As"
using wf_pterm.cases by force
then have l2:"length (var_poss_list (lhs α)) = length As"
using left_lin.length_var_rule[OF left_lin_axioms α] by (simp add: length_var_poss_list)
from left_lin have var_rule:"var_rule α = vars_term_list (lhs α)"
using α left_linear_trs_def linear_term_var_vars_term_list by fastforce
then show ?thesis proof(cases "p=[]")
case True
from assms(3) have "β = α" unfolding True labeled_source.simps lhs label_term.simps eval_term.simps subt_at.simps by simp
then show ?thesis unfolding True by simp
next
case False
from assms(3) have possL:"p ∈ possL (Prule α As)"
by (metis assms(2) get_label_imp_labelposs labeled_source_to_term option.distinct(1) poss_term_lab_to_term)
{assume "p ∈ fun_poss (lhs α)"
then have "get_label (labeled_source (Prule α As) |_ p) = Some (α, length p)"
unfolding labeled_source.simps lhs using label_term_increase by (metis add_0)
with assms(3) False have False by simp
}
with assms(2) obtain p1 p2 x where p:"p = p1@p2" and p1:"p1 ∈ poss (lhs α)" "lhs α |_ p1 = Var x" and p2:"p2 ∈ poss ((⟨map source As⟩⇩α) x)"
unfolding source.simps using poss_subst_apply_term[of p "lhs α"] by metis
then have "p1 ∈ var_poss (lhs α)" using var_poss_iff by blast
with p1 obtain i where i:"i < length As" "vars_term_list (lhs α) !i = x" "var_poss_list (lhs α) ! i = p1"
using l2 by (metis in_set_conv_nth length_var_poss_list term.inject(1) var_poss_list_sound vars_term_list_var_poss_list)
with p2 l1 have p2_poss:"p2 ∈ poss (source (As!i))"
by (smt (verit, del_insts) α case_prodD left_lin left_linear_trs_def length_map lhs_subst_var_i linear_term_var_vars_term_list nth_map)
from p1 have "labeled_source (Prule α As) |_ p = ((⟨map labeled_source As⟩⇩α) x)|_p2"
unfolding labeled_source.simps p by (smt (verit) assms(2) eval_term.simps(1) label_term_to_term labeled_source.simps(3) labeled_source_to_term p poss_term_lab_to_term subt_at_subst subterm_poss_conv var_label_term)
moreover from var_rule have "map (⟨map labeled_source As⟩⇩α) (vars_term_list (lhs α)) = map labeled_source As"
by (metis apply_lhs_subst_var_rule l1 length_map)
ultimately have "labeled_source (Prule α As) |_ p = (labeled_source (As!i))|_p2"
using i by (metis map_nth_conv)
with assms(3) have "get_label (labeled_source (As ! i) |_ p2) = Some (β, 0)" by force
with p2_poss i p show ?thesis by blast
qed
qed
end
text‹If the labeled source of a proof term @{term A} has the shape @{term "t ⋅ σ"} where all
function symbols in @{term t} are unlabeled, then @{term A} matches @{term t} with some substitution
@{term τ}.›
context no_var_lhs
begin
lemma pterm_source_substitution:
assumes "A ∈ wf_pterm R"
and "source A = t ⋅ σ" and "linear_term t"
and "∀p ∈ fun_poss t. p ∉ possL A"
shows "A = (to_pterm t) ⋅ (mk_subst Var (match_substs (to_pterm t) A))"
using assms proof(induct A arbitrary:t σ)
case (1 x)
from 1(1) obtain y where y:"t = Var y"
using subst_apply_eq_Var by (metis source.simps(1))
have match:"match_substs (Var y) (Var x) = [(y, Var x)]"
unfolding match_substs_def vars_term_list.simps poss_list.simps by simp
show ?case unfolding y to_pterm.simps match
by simp
next
case (2 As f)
show ?case proof(cases t)
case (Var x)
have match:"match_substs (Var x) (Pfun f As) = [(x, Pfun f As)]"
unfolding match_substs_def vars_term_list.simps poss_list.simps by simp
then show ?thesis unfolding Var to_pterm.simps match by simp
next
case (Fun g ts)
from 2(2) have f:"f = g"
unfolding Fun by simp
from 2(2) have l:"length ts = length As"
unfolding Fun eval_term.simps using map_eq_imp_length_eq by fastforce
{fix i assume i:"i < length As"
from 2(2) i have "source (As!i) = (ts!i) ⋅ σ"
unfolding Fun f by (smt (verit, best) eval_term.simps(2) l nth_map source.simps(2) term.sel(4))
moreover from 2(3) i l have lin_tsi:"linear_term (ts!i)"
unfolding Fun by simp
moreover have "(∀p∈fun_poss (ts!i). p ∉ possL (As!i))" proof
fix p assume "p ∈ fun_poss (ts!i)"
then have "i#p ∈ fun_poss (Fun f ts)"
using i l by simp
with 2(4) have "i#p ∉ possL (Pfun f As)"
unfolding Fun f by fastforce
then show "p ∉ possL (As!i)"
using i unfolding labeled_source.simps labelposs.simps by simp
qed
ultimately have IH:"As!i = to_pterm (ts!i) ⋅ mk_subst Var (match_substs (to_pterm (ts!i)) (As!i))"
using 2(1) i nth_mem by blast
have "As!i = to_pterm (ts!i) ⋅ mk_subst Var (match_substs (to_pterm t) (Pfun g As))" proof-
{fix x assume "x ∈ vars_term (to_pterm (ts!i))"
then obtain j where j:"vars_term_list (ts!i) !j = x" "j < length (vars_term_list (ts!i))"
by (metis in_set_conv_nth set_vars_term_list vars_to_pterm)
then have j':"j < length (map ((|_) (As ! i)) (var_poss_list (to_pterm (ts ! i))))"
by (metis length_map length_var_poss_list var_poss_list_to_pterm)
let ?qj="var_poss_list (to_pterm (ts!i)) !j"
have map_j:"(map ((|_) (As ! i)) (var_poss_list (to_pterm (ts ! i))))!j = (As!i)|_?qj"
using j' by simp
have "distinct (vars_term_list (ts!i))"
using lin_tsi by (metis distinct_remdups distinct_rev linear_term_var_vars_term_list o_apply)
then have dist1:"distinct (map fst (match_substs (to_pterm (ts!i)) (As!i)))"
unfolding match_substs_def by (metis length_map length_var_poss_list map_fst_zip vars_to_pterm)
have "distinct (vars_term_list t)"
by (metis "2.prems"(2) distinct_remdups distinct_rev linear_term_var_vars_term_list o_apply)
then have dist2:"distinct (map fst (match_substs (to_pterm t) (Pfun g As)))"
unfolding match_substs_def by (metis length_map length_var_poss_list map_fst_zip vars_to_pterm)
have "(x, (As!i)|_?qj) ∈ set (match_substs (to_pterm (ts!i)) (As!i))"
unfolding match_substs_def using map_j j j' by (metis (no_types, lifting) in_set_conv_nth length_zip min_less_iff_conj nth_zip vars_to_pterm)
then have sub1:"mk_subst Var (match_substs (to_pterm (ts!i)) (As!i)) x = As!i |_ ?qj"
using dist1 map_of_eq_Some_iff unfolding mk_subst_def by simp
let ?j'="(sum_list (map (length ∘ vars_term_list) (take i ts)) + j)"
have x2:"vars_term_list t ! ?j' = x"
unfolding Fun vars_term_list.simps using j(1) by (smt (verit, best) concat_nth i j(2) l length_map map_map nth_map take_map)
have lj':"?j' < length (vars_term_list (to_pterm t))" unfolding vars_to_pterm unfolding Fun to_pterm.simps vars_term_list.simps
using i j(2) l concat_nth_length by (metis List.map.compositionality length_map nth_map take_map)
then have j'_var_poss:"?j' < length (var_poss_list (to_pterm t))"
by (metis length_var_poss_list)
then have lj'':"?j' < length (map ((|_) (Pfun g As)) (var_poss_list (to_pterm t)))"
by (metis length_map length_var_poss_list)
have "var_poss_list (to_pterm t) ! ?j' = i#?qj"
proof-
have l_zip:"i < length (zip [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts)))"
by (simp add: i l)
have zip:"zip [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts)) ! i = (i, var_poss_list (to_pterm (ts ! i)))"
using nth_zip by (simp add: i l)
have map2:"map2 (λi. map ((#) i)) [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts)) ! i ! j = i#?qj"
unfolding nth_map[OF l_zip] zip using j' by auto
from l_zip have i'':"i < length (map2 (λx. map ((#) x)) [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts)))"
by simp
have j'':"j < length (map2 (λx. map ((#) x)) [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts)) ! i)"
unfolding nth_map[OF l_zip] zip using j(2) by (metis case_prod_conv length_map length_var_poss_list vars_to_pterm)
{fix k assume k:"k < length ts"
then have zip:"zip [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts)) ! k = (k, var_poss_list (to_pterm (ts ! k)))"
using nth_zip by simp
then have "map2 (λx. map ((#) x)) [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts)) ! k =
map ((#) k) (var_poss_list (to_pterm (ts ! k)))"
using k by simp
then have "length ((map2 (λx. map ((#) x)) [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts)))!k) =
length (vars_term_list (ts!k))"
using length_var_poss_list vars_to_pterm by (metis length_map)
with k have "(map length (map2 (λx. map ((#) x)) [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts))))!k =
(map (length ∘ vars_term_list) ts) ! k" by simp
}
moreover have "length (map length (map2 (λx. map ((#) x)) [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts)))) = length ts"
by simp
ultimately have "(map length (map2 (λx. map ((#) x)) [0..<length (map to_pterm ts)] (map var_poss_list (map to_pterm ts)))) =
(map (length ∘ vars_term_list) ts)" by (simp add: map_nth_eq_conv)
then show ?thesis
unfolding Fun to_pterm.simps var_poss_list.simps using concat_nth[OF i'' j''] unfolding map2 take_map[symmetric] by simp
qed
with lj'' have "(map ((|_) (Pfun g As)) (var_poss_list (to_pterm t)))!?j' = Pfun g As |_ (i#?qj)"
by force
with x2 have "(x, Pfun g As |_(i#?qj)) ∈ set (match_substs (to_pterm t) (Pfun g As))"
unfolding match_substs_def using lj' lj'' by (metis (no_types, lifting) in_set_conv_nth length_zip min_less_iff_conj nth_zip vars_to_pterm)
then have sub2:"mk_subst Var (match_substs (to_pterm t) (Pfun g As)) x = Pfun g As |_ (i#?qj)"
using dist2 map_of_eq_Some_iff unfolding mk_subst_def by simp
from sub1 sub2 have "mk_subst Var (match_substs (to_pterm (ts!i)) (As!i)) x = mk_subst Var (match_substs (to_pterm t) (Pfun g As)) x"
by simp
}
then show ?thesis using IH
using term_subst_eq by force
qed
}
then show ?thesis
unfolding Fun f eval_term.simps to_pterm.simps using l by (metis (mono_tags, lifting) length_map map_nth_eq_conv)
qed
next
case (3 α As)
show ?case proof(cases t)
case (Var x)
have match:"match_substs (Var x) (Prule α As) = [(x, Prule α As)]"
unfolding match_substs_def vars_term_list.simps poss_list.simps by simp
then show ?thesis unfolding Var to_pterm.simps match by simp
next
case (Fun g ts)
from 3(1) no_var_lhs obtain f ss where lhsa:"lhs α = Fun f ss"
by blast
have "[] ∈ possL (Prule α As)"
unfolding labeled_source.simps lhsa label_term.simps labelposs.simps eval_term.simps by simp
with 3(6) have False unfolding Fun by simp
then show ?thesis by simp
qed
qed
lemma unlabeled_source_to_pterm:
assumes "labeled_source A = s ⋅ τ"
and "linear_term s" and "A ∈ wf_pterm R"
and "labelposs s = {}"
shows "∃As. A = to_pterm (term_lab_to_term s) ⋅ (mk_subst Var (zip (vars_term_list s) As)) ∧ length (vars_term_list s) = length As"
using assms proof(induct s arbitrary:A)
case (Var x)
let ?As ="[A]"
have "A = to_pterm (term_lab_to_term (Var x)) ⋅ mk_subst Var (zip (vars_term_list (Var x)) ?As)"
unfolding term_lab_to_term.simps to_pterm.simps vars_term_list.simps zip_Cons_Cons zip_Nil mk_subst_def by simp
then show ?case
by (smt (verit) length_nth_simps(1) list.size(4) vars_term_list.simps(1))
next
case (Fun fl ts)
from Fun(5) obtain f where f:"fl = (f, None)"
by (metis empty_iff empty_pos_in_poss get_label.simps(2) get_label_imp_labelposs prod.exhaust_sel subt_at.simps(1))
with Fun(2) have "∃As. A = Pfun f As ∧ length As = length ts" proof(cases A)
case (Pfun g As)
from Fun(2) show ?thesis
unfolding Pfun f labeled_source.simps using map_eq_imp_length_eq by auto
next
case (Prule α As)
from Fun(4) no_var_lhs obtain g ss where lhs:"lhs α = Fun g ss"
by (metis Inl_inject Prule case_prodD is_FunE is_Prule.simps(1) is_Prule.simps(3) term.distinct(1) term.sel(2) wf_pterm.simps)
from Fun(2) show ?thesis
unfolding Prule f lhs labeled_source.simps by force
qed simp
then obtain As where as:"A = Pfun f As" and l:"length As = length ts"
by blast
{fix i assume i:"i < length ts"
with Fun(2) have "labeled_source (As!i) = (ts!i) ⋅ τ"
unfolding as by (smt (verit, best) eval_term.simps(2) l labeled_source.simps(2) nth_map term.inject(2))
moreover from i Fun(3) have "linear_term (ts!i)"
by simp
moreover from i Fun(4) have "As!i ∈ wf_pterm R"
unfolding as by (metis l fun_well_arg nth_mem)
moreover from i Fun(5) have "labelposs (ts!i) = {}"
unfolding f labelposs.simps by blast
ultimately have "∃As'. (As!i) = to_pterm (term_lab_to_term (ts!i)) ⋅ mk_subst Var (zip (vars_term_list (ts!i)) As') ∧ length (vars_term_list (ts!i)) = length As'"
using Fun(1) i by force
}
then obtain As' where l'':"length As' = length ts"
and IH:"(∀i < length ts. (As!i) = to_pterm (term_lab_to_term (ts!i)) ⋅ mk_subst Var (zip (vars_term_list (ts!i)) (As'!i)) ∧ length (vars_term_list (ts!i)) = length (As'!i))"
using Ex_list_of_length_P[where P="λAs' i. As ! i = to_pterm (term_lab_to_term (ts ! i)) ⋅ mk_subst Var (zip (vars_term_list (ts ! i)) As') ∧ length (vars_term_list (ts!i)) = length As'"] l by blast
then have l':"length As' = length (map to_pterm (map term_lab_to_term ts))"
by simp
have vars_list:"map vars_term_list (map to_pterm (map term_lab_to_term ts)) = map vars_term_list ts"
by (smt (verit, best) length_map map_nth_eq_conv vars_term_list_term_lab_to_term vars_to_pterm)
have "map vars_term (map to_pterm (map term_lab_to_term ts)) = map vars_term ts"
using vars_term_list_term_lab_to_term by (smt (verit, ccfv_threshold) length_map map_nth_eq_conv set_vars_term_list vars_to_pterm)
then have part:"is_partition (map vars_term (map to_pterm (map term_lab_to_term ts)))"
using Fun(3) by (metis linear_term.simps(2))
have *:"∀i < length ts. to_pterm (term_lab_to_term (ts!i)) ⋅ mk_subst Var (concat (map2 zip (map vars_term_list (map to_pterm (map term_lab_to_term ts))) As')) = As!i"
using mk_subst_partition_special[OF l' part] unfolding length_map using nth_map IH
by (smt (verit, best) length_map vars_term_list_term_lab_to_term vars_to_pterm)
from IH have "∀i < length ts. length (vars_term_list (to_pterm (term_lab_to_term (ts! i)))) = length (As' ! i)"
by (metis vars_term_list_term_lab_to_term vars_to_pterm)
then have ls:"∀i < length ts. length (map vars_term_list (map to_pterm (map term_lab_to_term ts)) ! i) = length (As' ! i)"
using nth_map by simp
then have cc:"concat (map2 zip (map vars_term_list (map to_pterm (map term_lab_to_term ts))) As') = zip (concat (map vars_term_list ts)) (concat As')"
unfolding vars_list using concat_map2_zip by (metis l' length_map)
have "A = to_pterm (term_lab_to_term (Fun fl ts)) ⋅ mk_subst Var (zip (vars_term_list (Fun fl ts)) (concat As'))"
unfolding f term_lab_to_term.simps to_pterm.simps fst_conv eval_term.simps as vars_term_list.simps cc[symmetric] using * by (simp add: l list_eq_iff_nth_eq)
moreover have "length (vars_term_list (Fun fl ts)) = length (concat As')"
unfolding vars_term_list.simps
using l'' ls by (metis eq_length_concat_nth length_map vars_list)
ultimately show ?case by auto
qed
end
lemma labels_intersect_label_term:
assumes "term_lab_to_term A = t ⋅ (term_lab_to_term ∘ σ)"
and "linear_term t"
and "labelposs A ∩ labelposs ((label_term α n t) ⋅ σ) = {}"
shows "∃As. A = term_to_term_lab t ⋅ (mk_subst Var (zip (vars_term_list t) As)) ∧ length As = length (vars_term_list t)"
using assms proof(induct t arbitrary:A n)
case (Var x)
have "A = mk_subst Var (zip [x] [A]) x"
unfolding mk_subst_def by simp
then show ?case unfolding term_to_term_lab.simps eval_term.simps vars_term_list.simps by fastforce
next
case (Fun f ts)
from Fun(2) obtain lab ss where a:"A = Fun (f, lab) ss"
using term_lab_to_term.simps by (smt (verit, ccfv_threshold) eroot.cases fst_conv old.prod.exhaust eval_term.simps(2) term.distinct(1) term.sel(2))
from Fun(4) have lab:"lab = None"
unfolding a using insertCI by auto
from Fun(2) have l:"length ts = length ss"
unfolding a by (metis length_map eval_term.simps(2) term.sel(4) term_lab_to_term.simps(2))
{fix i assume i:"i < length ts"
with Fun(2) have "term_lab_to_term (ss!i) = ts!i ⋅ (term_lab_to_term ∘ σ)"
unfolding a term_lab_to_term.simps eval_term.simps fst_conv by (metis l nth_map term.inject(2))
moreover from i Fun(3) have "linear_term (ts!i)"
by simp
moreover have "labelposs (ss!i) ∩ labelposs (label_term α (n+1) (ts!i) ⋅ σ) = {}"
proof-
{fix q assume q1:"q ∈ labelposs (ss!i)" and q2:"q ∈ labelposs (label_term α (n+1) (ts!i) ⋅ σ)"
from q1 i l have "i#q ∈ labelposs A"
unfolding a lab label_term.simps labelposs.simps by simp
moreover from q2 i have "i#q ∈ labelposs ((label_term α n (Fun f ts)) ⋅ σ)"
unfolding label_term.simps eval_term.simps labelposs.simps length_map by simp
ultimately have False
using Fun(4) by blast
}
then show ?thesis
by blast
qed
ultimately have "∃As. ss!i = term_to_term_lab (ts!i) ⋅ (mk_subst Var (zip (vars_term_list (ts!i)) As)) ∧ length As = length (vars_term_list (ts!i))"
using Fun(1) i nth_mem by blast
}
then obtain Ass where l':"length Ass = length ts"
and IH:"(∀i < length ts. (ss!i) = (term_to_term_lab (ts!i)) ⋅ mk_subst Var (zip (vars_term_list (ts!i)) (Ass!i)) ∧ length (Ass!i) = length (vars_term_list (ts!i)))"
using Ex_list_of_length_P[where P="λAss i. ss ! i = (term_to_term_lab (ts ! i)) ⋅ mk_subst Var (zip (vars_term_list (ts ! i)) Ass) ∧ length Ass = length (vars_term_list (ts!i))"] l by blast
let ?As="concat Ass"
from l' have l'':"length Ass = length (map term_to_term_lab ts)"
by simp
have vars_list:"map vars_term_list (map term_to_term_lab ts) = map vars_term_list ts"
using vars_term_list_term_to_term_lab by auto
have "map vars_term (map term_to_term_lab ts) = map vars_term ts"
using vars_term_list_term_to_term_lab by (smt (verit, ccfv_threshold) length_map map_nth_eq_conv set_vars_term_list vars_to_pterm)
then have part:"is_partition (map vars_term (map term_to_term_lab ts))"
using Fun(3) by (metis linear_term.simps(2))
have *:"∀i < length ts. (term_to_term_lab (ts!i)) ⋅ mk_subst Var (concat (map2 zip (map vars_term_list (map term_to_term_lab ts)) Ass)) = ss!i"
using mk_subst_partition_special[OF l'' part] unfolding length_map using nth_map IH
by (smt (verit, best) length_map vars_term_list_term_to_term_lab vars_to_pterm)
from IH have "∀i < length ts. length (vars_term_list (term_to_term_lab (ts! i))) = length (Ass ! i)"
by (metis vars_term_list_term_to_term_lab)
then have ls:"∀i < length ts. length (map vars_term_list (map term_to_term_lab ts) ! i) = length (Ass ! i)"
using nth_map by simp
then have cc:"concat (map2 zip (map vars_term_list (map term_to_term_lab ts)) Ass) = zip (concat (map vars_term_list ts)) (concat Ass)"
unfolding vars_list using concat_map2_zip by (metis l' length_map)
have "A = term_to_term_lab (Fun f ts) ⋅ mk_subst Var (zip (vars_term_list (Fun f ts)) ?As)"
unfolding term_to_term_lab.simps eval_term.simps vars_term_list.simps a lab cc[symmetric] using * by (simp add: l list_eq_iff_nth_eq)
moreover from IH l' have l'':"length ?As = length (vars_term_list (Fun f ts))"
unfolding vars_term_list.simps by (simp add: eq_length_concat_nth)
ultimately show ?case
by blast
qed
lemma labeled_wf_pterm_rule_in_TRS:
assumes "A ∈ wf_pterm R" and "p ∈ poss (labeled_source A)"
and "get_label (labeled_source A |_ p) = Some (α, n)"
shows "to_rule α ∈ R"
using assms proof(induct A arbitrary: p n)
case (2 ts f)
from 2(2,3) obtain i p' where p:"p = i#p'" "i < length ts" "p' ∈ poss (labeled_source (ts!i))" "get_label (labeled_source (ts!i) |_ p') = Some (α, n)"
unfolding labeled_source.simps get_label.simps by auto
with 2(1) show ?case
using nth_mem by blast
next
case (3 β As)
from 3(4) consider "p ∈ fun_poss (labeled_lhs β)" | "(∃p1 p2 x. p = p1@p2
∧ p1 ∈ poss (labeled_lhs β) ∧ (labeled_lhs β)|_p1 = Var x
∧ p2 ∈ poss ((⟨map labeled_source As⟩⇩β) x)
∧ (labeled_source (Prule β As))|_p = ((⟨map labeled_source As⟩⇩β) x)|_p2)"
unfolding labeled_source.simps by (meson poss_is_Fun_fun_poss poss_subst_choice)
then show ?case proof(cases)
case 1
then have "p ∈ fun_poss (lhs β)"
by (simp add: fun_poss_label_term)
then have "get_label ((labeled_source (Prule β As))|_p) = Some (β, length p)"
unfolding labeled_source.simps by (simp add: label_term_increase)
with 3(1,5) show ?thesis by auto
next
case 2
then obtain p1 p2 x where p1p2:"p = p1 @ p2" and x:"p1 ∈ poss (labeled_lhs β) ∧ labeled_lhs β |_ p1 = Var x"
and p2:"p2 ∈ poss ((⟨map labeled_source As⟩⇩β) x)"
and lab:"labeled_source (Prule β As) |_ p = (⟨map labeled_source As⟩⇩β) x |_ p2"
by blast
from x have "x ∈ vars_term (lhs β)"
by (metis subt_at_imp_supteq subteq_Var_imp_in_vars_term vars_term_labeled_lhs)
with x obtain i where i:"i < length (var_rule β) ∧ (var_rule β)!i = x"
by (metis in_set_conv_nth set_vars_term_list vars_term_list_vars_distinct)
with 3(2) have *:"(⟨map labeled_source As⟩⇩β) x = labeled_source (As!i)"
by (metis (no_types, lifting) length_map lhs_subst_var_i nth_map)
with 3(5) lab have "get_label ((labeled_source (As!i))|_p2) = Some (α, n)"
by simp
with 3(3) p2 i 3(2) * show ?thesis by force
qed
qed simp
context no_var_lhs
begin
lemma unlabeled_above_p:
assumes "A ∈ wf_pterm R"
and "p ∈ poss (source A)"
and "∀ r. r <⇩p p ⟶ r ∉ possL A"
shows "p ∈ poss A ∧ labeled_source A|_p = labeled_source (A|_p)"
using assms proof(induct p arbitrary: A)
case (Cons i p)
from Cons(3) obtain f ts where f:"source A = Fun f ts" and i:"i < length ts" and p:"p ∈ poss (ts!i)"
using args_poss by blast
from Cons(4) have "[] ∉ possL A"
by (simp add: order_pos.less_le)
then have no_lab:"get_label (labeled_source A) = None"
by (metis empty_pos_in_poss get_label_imp_labelposs subt_at.simps(1))
from Cons(3) obtain f' As where a:"A = Fun f' As"
by (metis Cons_poss_Var eroot.cases source.simps(1))
then have f':"f' = Inr f" proof(cases A)
case (Pfun g Bs)
then show ?thesis using f Pfun a by simp
next
case (Prule α Bs)
with Cons(2) obtain g ss where g:"lhs α = Fun g ss"
using no_var_lhs by (metis Inl_inject case_prodD is_Prule.simps(1) is_Prule.simps(3) term.collapse(2) term.distinct(1) term.sel(2) wf_pterm.simps)
then show ?thesis using no_lab unfolding Prule by simp
qed simp
from i a have i':"i < length As"
using f f' by force
from Cons(3) have "p ∈ poss (source (As!i))"
unfolding a f' by auto
moreover
{fix r assume "r ∈ poss (source (As!i))" and le:"r <⇩p p"
then have "i#r ∈ poss (labeled_source A)"
unfolding a f' using i' by simp
moreover from le have "i#r <⇩p i#p"
by simp
ultimately have "i#r ∉ possL A"
using Cons(4) by blast
then have "r ∉ possL (As!i)"
unfolding a f' labeled_source.simps using i' by force
}
ultimately have "p ∈ poss (As!i) ∧ labeled_source (As!i) |_ p = labeled_source ((As!i) |_ p)"
using Cons(1,2) i' unfolding a f' by (meson fun_well_arg nth_mem possL_subset_poss_source subsetD)
with i' a f' show ?case
by simp
qed simp
end
lemma (in single_redex) labeled_source_at_pq:"labeled_source (A|_q) = (labeled_source A)|_p"
using a pq q p a_well proof(induct q arbitrary:p A)
case Nil
then have "p = []"
by (simp add: subt_at_ctxt_of_pos_term subt_at_id_imp_eps)
then show ?case
by simp
next
case (Cons i q)
from Cons(4) obtain fs Bs where a:"A = Fun fs Bs" and i:"i < length Bs" and q:"q ∈ poss (Bs!i)"
using args_poss by blast
let ?As = "map (λj. (Bs!i) |_ (q @ [j])) [0..<length (var_rule α)]"
have "(map (λia. A |_ ((i # q) @ [ia])) [0..<length (var_rule α)]) = ?As"
unfolding a by simp
with a i q Cons(2,4) have bsi:"Bs!i = (ctxt_of_pos_term q (Bs!i))⟨Prule α ?As⟩"
by (metis ctxt_supt_id subt_at.simps(2) subt_at_ctxt_of_pos_term)
from Cons(6) have bi_well:"Bs ! i ∈ wf_pterm R"
unfolding a by (meson fun_well_arg i nth_mem)
show ?case proof(cases fs)
case (Inl β)
from Cons(6) have lin:"linear_term (lhs β)"
unfolding a Inl using left_lin left_linear_trs_def term.inject(2) wf_pterm.cases by fastforce
from Cons(6) have is_Fun:"is_Fun (lhs β)"
unfolding a Inl using no_var_lhs using wf_pterm.cases by auto
from Cons(6) have l_bs:"length Bs = length (var_rule β)"
unfolding a Inl using wf_pterm.cases by auto
obtain p1 p2 where p:"p = p1@p2" and p1:"p1 = var_poss_list (lhs β) ! i" and p2:"p2 ∈ poss (source (Bs!i))"
using ctxt_rule_obtain_pos Cons(4,5,3) lin l_bs unfolding a Inl by metis
have ctxt:"ctxt_of_pos_term p2 (source (Bs ! i)) = source_ctxt (ctxt_of_pos_term q (Bs ! i))"
proof-
from p1 have p1_pos:"p1 ∈ poss (lhs β)"
using i l_bs lin by (metis length_var_poss_list linear_term_var_vars_term_list nth_mem var_poss_imp_poss var_poss_list_sound)
from p1_pos have p1':"p1 ∈ poss (lhs β ⋅ ⟨map source Bs⟩⇩β)"
by simp
from p1 have p1'':"var_poss_list (lhs β) ! length (take i Bs) = p1"
using i by force
have *:"lhs β ⋅ ⟨map source Bs⟩⇩β |_ p1 = source (Bs!i)"
unfolding p1 using l_bs i
by (smt (verit) length_map lhs_subst_var_i lin linear_term_var_vars_term_list nth_map p1 p1_pos eval_term.simps(1) subt_at_subst vars_term_list_var_poss_list)
from Cons(3) show ?thesis
unfolding a Inl p source.simps ctxt_of_pos_term.simps source_ctxt.simps Let_def ctxt_of_pos_term_append[OF p1'] * p1''
using ctxt_comp_equals[OF p1'] p1_pos using poss_imp_subst_poss by blast
qed
from Cons(1)[OF bsi ctxt q p2 bi_well] have IH:" labeled_source (Bs ! i |_ q) = labeled_source (Bs ! i) |_ p2"
by presburger
from p1 have "p1 = var_poss_list (labeled_lhs β) ! i"
by (simp add: var_poss_list_labeled_lhs)
moreover then have "(labeled_lhs β)|_p1 = Var (vars_term_list (lhs β)!i)"
by (metis i l_bs lin linear_term_var_vars_term_list vars_term_list_labeled_lhs vars_term_list_var_poss_list)
ultimately show ?thesis
unfolding a Inl using i IH unfolding subt_at.simps p labeled_source.simps
by (smt (verit, ccfv_threshold) apply_lhs_subst_var_rule filter_cong l_bs length_map length_var_poss_list lin linear_term_var_vars_term_list map_nth_conv nth_mem poss_imp_subst_poss eval_term.simps(1) subt_at_append subt_at_subst var_poss_imp_poss var_poss_list_sound vars_term_list_labeled_lhs)
next
case (Inr f)
from Cons(3,5) obtain p' where p:"p = i#p'" and p':"p' ∈ poss (source (Bs!i))"
by (metis Cons.prems(3) Inr a source_poss)
from Cons(3) have ctxt:"ctxt_of_pos_term p' (source (Bs ! i)) = source_ctxt (ctxt_of_pos_term q (Bs ! i))"
unfolding a Inr p by (simp add: i)
from Cons(1)[OF bsi ctxt q p' bi_well] have IH:"labeled_source (Bs ! i |_ q) = labeled_source (Bs ! i) |_ p'"
by presburger
then show ?thesis
unfolding a Inr p using i by simp
qed
qed
context left_lin
begin
lemma single_redex_label:
assumes "Δ = ll_single_redex s p α" "p ∈ poss s" "q ∈ poss (source Δ)" "to_rule α ∈ R"
and "get_label (labeled_source Δ |_q) = Some (β, n)"
shows "α = β ∧ (∃q'. q = p@q' ∧ length q' = n ∧ q' ∈ fun_poss (lhs α))"
proof-
from assms have wf:"Δ ∈ wf_pterm R"
using single_redex_wf_pterm left_lin left_linear_trs_def by fastforce
from assms have "q ∈ possL Δ"
using get_label_imp_labelposs by force
then obtain q' where q:"q = p@q'" and q':"q' ∈ fun_poss (lhs α)"
unfolding assms(1) using single_redex_possL[OF assms(4,2)] by auto
from assms have "labeled_source Δ = (ctxt_of_pos_term p (labeled_source (to_pterm s)))⟨labeled_source (Prule α (map (to_pterm ∘ (λpi. s|_(p@pi))) (var_poss_list (lhs α))))⟩"
using label_source_ctxt by (simp add: ll_single_redex_def p_in_poss_to_pterm source_ctxt_to_pterm)
then have "labeled_source Δ |_q = labeled_source (Prule α (map (to_pterm ∘ (λpi. s|_(p@pi))) (var_poss_list (lhs α)))) |_q'"
unfolding q using assms(2) by (metis hole_pos_ctxt_of_pos_term hole_pos_poss labeled_source_to_term poss_term_lab_to_term replace_at_subt_at source_to_pterm subt_at_append)
then have "get_label (labeled_source Δ |_q) = get_label (labeled_lhs α|_q')"
using get_label_at_fun_poss_subst q' by force
also have "... = Some (α, size q')"
using get_label_label_term q' by fastforce
finally show ?thesis using assms q q' by force
qed
end
subsection‹Measuring Overlap›
abbreviation measure_ov :: "('f, 'v) pterm ⇒ ('f, 'v) pterm ⇒ nat"
where "measure_ov A B ≡ card ((possL A) ∩ (possL B))"
lemma finite_labelposs: "finite (labelposs A)"
by (meson finite_fun_poss labelposs_subs_fun_poss rev_finite_subset)
lemma finite_possL: "finite (possL A)"
by (simp add: finite_labelposs)
lemma measure_ov_symm: "measure_ov A B = measure_ov B A"
by (simp add: Int_commute)
lemma measure_lhs_subst:
assumes l:"length As = length Bs"
shows "card ((labelposs ((label_term α j t) ⋅ ⟨map labeled_source As⟩⇩α)) ∩
(labelposs (labeled_source (to_pterm t) ⋅ ⟨map labeled_source Bs⟩⇩α)))
= (∑x←vars_term_list t. measure_ov ((⟨As⟩⇩α) x) ((⟨Bs⟩⇩α) x))"
using assms proof(induct t arbitrary:j)
case (Var x)
show ?case proof(cases "∃i < length As. i < length (var_rule α) ∧ x = (var_rule α)!i")
case True
then obtain i where i:"x = (var_rule α)!i" and il:"i < length As" and il2:"i < length (var_rule α)" by auto
then have a:"(⟨map labeled_source As⟩⇩α) x = labeled_source (As!i)"
using lhs_subst_var_i by (metis (no_types, lifting) length_map nth_map)
from i il il2 l have b:"(⟨map labeled_source Bs⟩⇩α) x = labeled_source (Bs!i)"
using lhs_subst_var_i by (metis (no_types, lifting) length_map nth_map)
from i show ?thesis unfolding vars_term_list.simps sum_list_elem
unfolding to_pterm.simps label_term.simps labeled_source.simps eval_term.simps
unfolding a b using lhs_subst_var_i l il il2 by metis
next
case False
then have a:"(⟨map labeled_source As⟩⇩α) x = Var x"
using lhs_subst_not_var_i by (metis length_map)
from False l have b:"(⟨map labeled_source Bs⟩⇩α) x = Var x"
using lhs_subst_not_var_i by (metis length_map)
from False l have "possL ((⟨As⟩⇩α) x) ∩ possL ((⟨Bs⟩⇩α) x) = {}"
unfolding term.set(3) using lhs_subst_not_var_i
by (metis inf.idem labeled_source.simps(1) labelposs.simps(1))
then show ?thesis unfolding label_term.simps to_pterm.simps labeled_source.simps eval_term.simps a b
by auto
qed
next
case (Fun f ts)
let ?as="(map (λt. t ⋅ ⟨map labeled_source As⟩⇩α) (map (label_term α (j + 1)) ts))"
let ?bs="(map (λt. t ⋅ ⟨map labeled_source Bs⟩⇩α) (map labeled_source (map to_pterm ts)))"
let ?f="(λi. ({i # p |p. p ∈ labelposs (?as ! i)} ∩ {i # p |p. p ∈ labelposs (?bs ! i)}))"
have "{[]} ∩ (⋃i<length ts. {i # p |p. p ∈ labelposs (map (λt. t ⋅ ⟨map labeled_source Bs⟩⇩α) (map labeled_source (map to_pterm ts)) ! i)}) = {}"
by blast
then have *:"labelposs (label_term α j (Fun f ts) ⋅ ⟨map labeled_source As⟩⇩α) ∩ labelposs (labeled_source (to_pterm (Fun f ts)) ⋅ ⟨map labeled_source Bs⟩⇩α)
= (⋃i<length ts. (?f i))"
unfolding label_term.simps to_pterm.simps labeled_source.simps eval_term.simps labelposs.simps by auto
have "is_partition (map ?f [0..<length ts])" proof-
{fix i j assume j:"j < length ts" and i:"i < j"
have "?f i ∩ ?f j = {}" unfolding Int_def using i
by fastforce
}
then show ?thesis unfolding is_partition_def by auto
qed
moreover have "∀i<length ts. finite (?f i)" by (simp add: finite_labelposs)
ultimately have **:"card (⋃i<length ts. (?f i)) = (∑i<length ts. card (?f i))"
unfolding * using card_Union_Sum by blast
{fix i assume i:"i < length ts"
have "?f i = {i # p |p. p ∈ labelposs (?as ! i) ∩ labelposs (?bs ! i)}"
unfolding Int_def by blast
then have "card (?f i) = card (labelposs (?as ! i) ∩ labelposs (?bs ! i))"
unfolding Setcompr_eq_image using card_image by (metis (no_types, lifting) inj_on_Cons1)
with Fun i have "card (?f i) = (∑x←vars_term_list (ts!i). measure_ov ((⟨As⟩⇩α) x) ((⟨Bs⟩⇩α) x))"
by simp
}
then show ?case unfolding vars_term_list.simps * **
by (simp add: sum_sum_concat)
qed
lemma measure_lhs_args_zero:
assumes l:"length As = length Bs"
and empty:"∀ i < length As. measure_ov (As!i) (Bs!i) = 0"
shows "measure_ov (Prule α As) ((to_pterm (lhs α)) ⋅ ⟨Bs⟩⇩α) = 0"
proof-
let ?xs="vars_term_list (lhs α)"
have sum:"measure_ov (Prule α As) ((to_pterm (lhs α)) ⋅ ⟨Bs⟩⇩α)
= (∑x←vars_term_list (lhs α). measure_ov ((⟨As⟩⇩α) x) ((⟨Bs⟩⇩α) x))"
using labeled_source_apply_subst measure_lhs_subst[OF l]
by (metis (mono_tags, lifting) fun_mk_subst labeled_source.simps(1) labeled_source.simps(3) to_pterm_wf_pterm)
{fix i assume i:"i < length ?xs"
have "measure_ov ((⟨As⟩⇩α) (?xs ! i)) ((⟨Bs⟩⇩α) (?xs ! i)) = 0"
proof(cases "(∃j<length As. j < length (var_rule α) ∧ (?xs!i) = var_rule α ! j)")
case True
then obtain j where j:"j < length As" "j < length (var_rule α)" and ij:"?xs!i = (var_rule α)!j"
by blast
then show ?thesis
unfolding ij using empty by (metis j l lhs_subst_var_i)
next
case False
then have "(⟨As⟩⇩α) (?xs!i) = Var (?xs!i)"
using lhs_subst_not_var_i by metis
moreover have "(⟨Bs⟩⇩α) (?xs!i) = Var (?xs!i)"
using l False lhs_subst_not_var_i by metis
ultimately show ?thesis by simp
qed}
then show ?thesis
using sum by (simp add: sum_list_zero)
qed
lemma measure_zero_subt_at:
assumes "term_lab_to_term A = term_lab_to_term B"
and "labelposs A ∩ labelposs B = {}"
and "p ∈ poss A"
shows "labelposs (A|_p) ∩ labelposs (B|_p) = {}"
using assms proof(induct p arbitrary: A B)
case (Cons i p)
from Cons(4) obtain f a ts where a:"A = Fun (f, a) ts" and i:"i < length ts" and p:"p ∈ poss (ts!i)"
using args_poss by (metis old.prod.exhaust)
with Cons(2) obtain b ss where b:"B = Fun (f, b) ss"
by (metis (no_types, opaque_lifting) Cons.prems(3) Term.term.simps(2) args_poss old.prod.exhaust poss_term_lab_to_term prod.sel(1) term_lab_to_term.simps(2))
have ts:"(⋃i<length ts. {i # p | p. p ∈ labelposs (ts ! i)}) ⊆ labelposs A" unfolding a by(cases a) auto
have ss:"(⋃i<length ss. {i # p | p. p ∈ labelposs (ss ! i)}) ⊆ labelposs B" unfolding b by(cases b) auto
from ss ts b i Cons(2,3,4) have "labelposs (ts!i) ∩ labelposs (ss!i) = {}" by auto
with Cons(1,2) p i show ?case
unfolding a b by (simp add: map_eq_conv')
qed simp
lemma empty_step_imp_measure_zero:
assumes "is_empty_step A"
shows "measure_ov A B = 0"
by (metis assms card_eq_0_iff inf_bot_left labeled_source_simple_pterm source_empty_step)
lemma measure_ov_to_pterm:
shows "measure_ov A (to_pterm t) = 0"
by (simp add: labeled_source_simple_pterm)
lemma measure_zero_imp_orthogonal:
assumes R:"left_lin_no_var_lhs R" and S:"left_lin_no_var_lhs S"
and "co_initial A B" "A ∈ wf_pterm R" "B ∈ wf_pterm S"
and "measure_ov A B = 0"
shows "A ⊥⇩p B"
using assms(3-) proof(induct A arbitrary:B rule:subterm_induct)
case (subterm A)
then show ?case proof(cases A)
case (Var x)
with subterm show ?thesis proof(cases B)
case (Prule α Bs)
from subterm(2) Var obtain y where y:"lhs α = Var y"
unfolding Prule by (metis source.simps(1) source.simps(3) subst_apply_eq_Var)
from subterm(4) Prule S have "is_Fun (lhs α)"
unfolding left_lin_no_var_lhs_def no_var_lhs_def
by (metis Inl_inject case_prodD is_FunI is_Prule.simps(1) is_Prule.simps(3) is_VarI term.inject(2) wf_pterm.simps)
with y show ?thesis by simp
qed (simp_all add: orthogonal.intros(1))
next
case (Pfun f As)
note A=this
with subterm show ?thesis proof(cases B)
case (Pfun g Bs)
from subterm(2) have f:"f = g"
unfolding Pfun A by simp
from subterm(2) have l:"length As = length Bs"
unfolding A Pfun using map_eq_imp_length_eq by auto
{fix i assume i:"i < length As"
then have "As!i ⊲ A"
unfolding A by simp
moreover from i subterm(2) l have "co_initial (As!i) (Bs!i)"
by (metis (mono_tags, lifting) A Pfun nth_map source.simps(2) term.inject(2))
moreover from i subterm(3) have "As!i ∈ wf_pterm R"
using A by auto
moreover from i subterm(4) l have "Bs!i ∈ wf_pterm S"
using Pfun by auto
moreover have "measure_ov (As!i) (Bs!i) = 0" proof-
{fix p assume a:"p ∈ possL (As!i)" and b:"p ∈ possL (Bs!i)"
with i have "i#p ∈ possL A"
unfolding A labeled_source.simps labelposs.simps by simp
moreover from b i l have "i#p ∈ possL B"
unfolding Pfun labeled_source.simps labelposs.simps by simp
ultimately have False using subterm(4)
by (metis card_gt_0_iff disjoint_iff finite_Int finite_possL less_numeral_extra(3) subterm.prems(4))
}
then show ?thesis
by (metis card.empty disjoint_iff)
qed
ultimately have "As!i ⊥⇩p Bs!i"
using subterm(1) by blast
}
then show ?thesis
unfolding A Pfun f using l by auto
next
case (Prule β Bs)
from subterm(4) S have lin:"linear_term (lhs β)"
unfolding Prule left_lin_no_var_lhs_def left_lin_def left_linear_trs_def using wf_pterm.cases by fastforce
have isfun:"is_Fun (lhs β)"
using subterm(4) S no_var_lhs.lhs_is_Fun unfolding Prule left_lin_no_var_lhs_def by blast
have "(lhs β) ⋅ (term_lab_to_term ∘ (⟨map labeled_source Bs⟩⇩β)) = lhs β ⋅ ⟨map source Bs⟩⇩β"
by (metis label_term_to_term labeled_source.simps(3) labeled_source_to_term source.simps(3) term_lab_to_term_subst)
with subterm(2) have co_init:"term_lab_to_term (labeled_source A) = lhs β ⋅ (term_lab_to_term ∘ ⟨map labeled_source Bs⟩⇩β)"
unfolding Prule by simp
from subterm(5) have "possL A ∩ possL B = {}"
by (simp add: finite_possL)
then obtain τ where "labeled_source A = term_to_term_lab (lhs β) ⋅ τ"
unfolding labeled_source.simps(3) Prule using labels_intersect_label_term[OF co_init lin] by blast
moreover have "labelposs (term_to_term_lab (lhs β)) = {}"
using labelposs_term_to_term_lab by blast
moreover from lin have "linear_term (term_to_term_lab (lhs β))"
using linear_term_to_term_lab by blast
moreover have "term_lab_to_term (term_to_term_lab (lhs β)) = lhs β"
by simp
ultimately obtain σ where sigma:"A = to_pterm (lhs β) ⋅ σ"
using no_var_lhs.unlabeled_source_to_pterm subterm(3) R unfolding left_lin_no_var_lhs_def by metis
let ?As="map σ (var_rule β)"
from sigma have a:"A = (to_pterm (lhs β)) ⋅ ⟨?As⟩⇩β"
by (smt (verit, best) apply_lhs_subst_var_rule comp_apply length_map map_eq_conv set_remdups set_rev set_vars_term_list term_subst_eq vars_to_pterm)
{fix i assume i:"i < length (var_rule β)"
let ?xi="var_rule β!i"
from i obtain i' where i':"i' < length (vars_term_list (lhs β))" "?xi = vars_term_list (lhs β)!i'"
by (metis comp_apply in_set_conv_nth set_remdups set_rev)
have l:"length Bs = length (var_rule β)"
using subterm(4) unfolding Prule using wf_pterm.cases by force
from i have asi:"?As!i = σ ?xi"
by simp
then have "?As!i ⊲ A"
using a sigma subst_image_subterm i' by (metis is_FunE isfun nth_mem set_vars_term_list to_pterm.simps(2) vars_to_pterm)
moreover from i subterm(2) have "co_initial (?As!i) (Bs!i)"
unfolding a Prule source.simps source_apply_subst[OF to_pterm_wf_pterm[of "lhs β"]] source_to_pterm using l
by (smt (verit, best) apply_lhs_subst_var_rule comp_def i'(1) i'(2) length_map nth_map nth_mem set_vars_term_list term_subst_eq_conv)
moreover have "measure_ov (?As!i) (Bs!i) = 0" proof-
{fix p assume p:"p ∈ possL (?As!i)"
let ?pi="var_poss_list (labeled_source (to_pterm (lhs β)))!i'"
have pi:"?pi=var_poss_list (labeled_lhs β) !i'"
by (simp add: var_poss_list_term_lab_to_term)
have xi:"?xi=vars_term_list (labeled_lhs β) !i'"
by (metis i'(2) vars_term_list_labeled_lhs)
have xi':"?xi=vars_term_list (labeled_source (to_pterm (lhs β))) ! i'"
using vars_term_list_term_lab_to_term i'(2) by (metis labeled_source_to_term source_to_pterm)
have i'l:"i' < length (vars_term_list (labeled_lhs β))"
by (simp add: i'(1) vars_term_list_labeled_lhs)
have i'l':"i' < length (vars_term_list (labeled_source (to_pterm (lhs β))))"
by (simp add: i'(1) vars_term_list_term_lab_to_term)
have "(labeled_source (to_pterm (lhs β))) |_?pi = Var ?xi"
using i' using i'l' vars_term_list_var_poss_list xi' by auto
moreover have "possL A = labelposs ((labeled_source (to_pterm (lhs β))) ⋅ (labeled_source ∘ σ))"
using labeled_source_apply_subst to_pterm_wf_pterm unfolding sigma by metis
with p have "?pi@p ∈ possL A"
unfolding set_labelposs_subst asi xi' using i'l' by fastforce
with subterm(5) have "?pi@p ∉ possL B"
by (meson card_eq_0_iff disjoint_iff finite_Int finite_labelposs)
moreover {assume "p ∈ possL (Bs!i)"
then have "?pi@p ∈ {?pi @ q |q. q ∈ labelposs ((⟨map labeled_source Bs⟩⇩β) ?xi)}"
by (smt (verit) Inl_inject Inr_Inl_False Prule apply_lhs_subst_var_rule i length_map map_nth_conv mem_Collect_eq subterm.prems(3) term.distinct(1) term.inject(2) wf_pterm.cases)
then have "?pi@p ∈ possL B"
unfolding Prule labeled_source.simps set_labelposs_subst xi pi using i'l by blast
}
ultimately have "p ∉ possL (Bs!i)"
by blast
}
then have "possL (?As!i) ∩ possL (Bs!i) = {}"
by blast
then show ?thesis by simp
qed
ultimately have "?As!i ⊥⇩p Bs!i"
using subterm(1,3,4) i unfolding a Prule
by (smt (verit, best) Inr_Inl_False Term.term.simps(4) length_map lhs_subst_args_wf_pterm nth_mem sum.inject(1) term.inject(2) wf_pterm.simps)
}
then show ?thesis unfolding a Prule using orthogonal.intros(4)[of ?As Bs]
by (smt (verit, best) Prule Term.term.simps(4) in_set_zip length_map old.sum.inject(1) prod.case_eq_if subterm.prems(3) sum.distinct(1) term.inject(2) wf_pterm.cases)
qed simp
next
case (Prule α As)
then have A:"A = Prule α As"
by simp
from Prule subterm(3) R have lin:"linear_term (lhs α)"
unfolding left_lin_no_var_lhs_def left_lin_def left_linear_trs_def
using wf_pterm.simps by fastforce
obtain f ts where f:"lhs α = Fun f ts"
using subterm(3) R no_var_lhs.lhs_is_Fun unfolding left_lin_no_var_lhs_def Prule by blast
show ?thesis proof(cases B)
case (Var x)
then show ?thesis
by (metis source.simps(1) source_orthogonal subterm.prems(1) to_pterm.simps(1))
next
case (Pfun g Bs)
have "(lhs α) ⋅ (term_lab_to_term ∘ (⟨map labeled_source As⟩⇩α)) = lhs α ⋅ ⟨map source As⟩⇩α"
by (metis label_term_to_term labeled_source.simps(3) labeled_source_to_term source.simps(3) term_lab_to_term_subst)
with subterm(2) have co_init:"term_lab_to_term (labeled_source B) = lhs α ⋅ (term_lab_to_term ∘ ⟨map labeled_source As⟩⇩α)"
unfolding Prule by simp
from subterm(5) have "possL A ∩ possL B = {}"
by (simp add: finite_possL)
then obtain τ where "labeled_source B = term_to_term_lab (lhs α) ⋅ τ"
unfolding labeled_source.simps(3) Prule using labels_intersect_label_term[OF co_init lin] by blast
moreover have "labelposs (term_to_term_lab (lhs α)) = {}"
using labelposs_term_to_term_lab by blast
moreover from lin have "linear_term (term_to_term_lab (lhs α))"
using linear_term_to_term_lab by auto
moreover have "term_lab_to_term (term_to_term_lab (lhs α)) = lhs α"
by simp
ultimately obtain σ where sigma:"B = to_pterm (lhs α) ⋅ σ"
using no_var_lhs.unlabeled_source_to_pterm S subterm(4) unfolding left_lin_no_var_lhs_def by metis
let ?Bs="map σ (var_rule α)"
from sigma have b:"B = (to_pterm (lhs α)) ⋅ ⟨?Bs⟩⇩α"
by (smt (verit, best) apply_lhs_subst_var_rule comp_apply length_map map_eq_conv set_remdups set_rev set_vars_term_list term_subst_eq vars_to_pterm)
{fix i assume i:"i < length (var_rule α)"
let ?xi="var_rule α!i"
from i obtain i' where i':"i' < length (vars_term_list (lhs α))" "?xi = vars_term_list (lhs α)!i'"
by (metis comp_apply in_set_conv_nth set_remdups set_rev)
from i have asi:"?Bs!i = σ ?xi"
by simp
moreover have l:"length As = length (var_rule α)"
using subterm(3) unfolding A using wf_pterm.cases by force
then have "As!i ⊲ A"
using i unfolding A by simp
moreover from i subterm(2) have "co_initial (As!i) (?Bs!i)"
unfolding b Prule source.simps source_apply_subst[OF to_pterm_wf_pterm[of "lhs α"]] source_to_pterm using l
by (smt (verit, best) apply_lhs_subst_var_rule comp_def i'(1) i'(2) length_map nth_map nth_mem set_vars_term_list term_subst_eq_conv)
moreover have "measure_ov (As!i) (?Bs!i) = 0" proof-
{fix p assume p:"p ∈ possL (?Bs!i)"
let ?pi="var_poss_list (labeled_source (to_pterm (lhs α)))!i'"
have pi:"?pi=var_poss_list (labeled_lhs α) !i'"
by (simp add: var_poss_list_term_lab_to_term)
have xi:"?xi=vars_term_list (labeled_lhs α) !i'"
by (metis i'(2) vars_term_list_labeled_lhs)
have xi':"?xi=vars_term_list (labeled_source (to_pterm (lhs α))) ! i'"
using vars_term_list_term_lab_to_term i'(2) by (metis labeled_source_to_term source_to_pterm)
have i'l:"i' < length (vars_term_list (labeled_lhs α))"
by (simp add: i'(1) vars_term_list_labeled_lhs)
have i'l':"i' < length (vars_term_list (labeled_source (to_pterm (lhs α))))"
by (simp add: i'(1) vars_term_list_term_lab_to_term)
have "(labeled_source (to_pterm (lhs α))) |_?pi = Var ?xi"
using i' using i'l' vars_term_list_var_poss_list xi' by auto
moreover have "possL B = labelposs ((labeled_source (to_pterm (lhs α))) ⋅ (labeled_source ∘ σ))"
using labeled_source_apply_subst to_pterm_wf_pterm unfolding sigma by metis
with p have "?pi@p ∈ possL B"
unfolding set_labelposs_subst asi xi' using i'l' by fastforce
with subterm(5) have "?pi@p ∉ possL A"
by (meson card_eq_0_iff disjoint_iff finite_Int finite_labelposs)
moreover {assume "p ∈ possL (As!i)"
then have "?pi@p ∈ {?pi @ q |q. q ∈ labelposs ((⟨map labeled_source As⟩⇩α) ?xi)}"
by (smt (verit) Inl_inject Inr_Inl_False Prule apply_lhs_subst_var_rule i length_map map_nth_conv mem_Collect_eq subterm.prems(2) term.distinct(1) term.inject(2) wf_pterm.cases)
then have "?pi@p ∈ possL A"
unfolding Prule labeled_source.simps set_labelposs_subst xi pi using i'l by blast
}
ultimately have "p ∉ possL (As!i)"
by blast
}
then have "possL (As!i) ∩ possL (?Bs!i) = {}"
by blast
then show ?thesis by simp
qed
ultimately have "As!i ⊥⇩p ?Bs!i"
using subterm(1,3,4) i unfolding b Prule
by (smt (verit, best) Inr_Inl_False Term.term.simps(4) length_map lhs_subst_args_wf_pterm nth_mem sum.inject(1) term.inject(2) wf_pterm.simps)
}
then show ?thesis unfolding b Prule using orthogonal.intros(3)[of As ?Bs]
by (smt (verit, best) Prule Term.term.simps(4) in_set_zip length_map old.sum.inject(1) prod.case_eq_if subterm.prems(2) sum.distinct(1) term.inject(2) wf_pterm.cases)
next
case (Prule β Bs)
from subterm(4) S obtain g ss where g:"lhs β = Fun g ss"
unfolding Prule left_lin_no_var_lhs_def using no_var_lhs.lhs_is_Fun by blast
have "[] ∈ possL A"
unfolding A f labeled_source.simps label_term.simps eval_term.simps labelposs.simps by blast
moreover have "[] ∈ possL B"
unfolding Prule g labeled_source.simps label_term.simps eval_term.simps labelposs.simps by blast
ultimately show ?thesis
using subterm(5) by (simp add: disjoint_iff finite_labelposs)
qed
qed
qed
subsection‹Collecting Overlapping Positions›
abbreviation overlaps_pos :: "('f, 'v) term_lab ⇒ ('f, 'v) term_lab ⇒ (pos × pos) set"
where "overlaps_pos A B ≡ Set.filter (λ(p,q). get_label (A|_p) ≠ None ∧ get_label (B|_q) ≠ None ∧
snd (the (get_label (A|_p))) = 0 ∧ snd (the (get_label (B|_q))) = 0 ∧
(p <⇩p q ∧ get_label (A|_q) ≠ None ∧ fst (the (get_label (A|_q))) = fst (the (get_label (A|_p))) ∧ snd (the (get_label (A|_q))) = length (the (remove_prefix p q)) ∨
(q ≤⇩p p ∧ get_label (B|_p) ≠ None ∧ fst (the (get_label (B|_q))) = fst (the (get_label (B|_p))) ∧ snd (the (get_label (B|_p))) = length (the (remove_prefix q p)))))
(fun_poss A × fun_poss B)"
lemma overlaps_pos_symmetric:
assumes "(p,q) ∈ overlaps_pos A B"
shows "(q,p) ∈ overlaps_pos B A"
using SigmaI assms less_pos_def by auto
lemma overlaps_pos_intro:
assumes "q@q' ∈ fun_poss A" and "q ∈ fun_poss B"
and "get_label (A|_(q@q')) = Some (γ, 0)"
and "get_label (B|_q) = Some (β, 0)"
and "get_label (B|_(q@q')) = Some (β, length q')"
shows "(q@q', q) ∈ overlaps_pos A B"
using assms by force
text‹Define the partial order on overlaps›
definition less_eq_overlap :: "pos × pos ⇒ pos × pos ⇒ bool" (infix "≤⇩o" 50)
where "p ≤⇩o q ⟷ (fst p ≤⇩p fst q) ∧ (snd p ≤⇩p snd q)"
definition less_overlap :: "pos × pos ⇒ pos × pos ⇒ bool" (infix "<⇩o" 50)
where "p <⇩o q ⟷ p ≤⇩o q ∧ p ≠ q "