Theory Proof_Terms

section‹Proof Terms›

theory Proof_Terms
  imports 
    First_Order_Terms.Matching
    First_Order_Rewriting.Multistep
    Proof_Term_Utils
begin

subsection‹Definitions›

text‹A rewrite rule consists of a pair of terms representing its left-hand side and right-hand side. 
We associate a rule symbol with each rewrite rule. ›
datatype ('f, 'v) prule = 
  Rule (lhs: "('f, 'v) term") (rhs: "('f, 'v) term") ("_ → _" [51, 51] 52)

text‹Translate between @{type prule} defined here and @{type rule} as defined in IsaFoR.›
abbreviation to_rule :: "('f, 'v) prule ⇒ ('f, 'v) rule" 
  where "to_rule r ≡ (lhs r, rhs r)"

text‹Proof terms are terms built from variables, function symbols, and rules.›
type_synonym
  ('f, 'v) pterm = "(('f, 'v) prule + 'f, 'v) term"
type_synonym
  ('f, 'v) pterm_ctxt = "(('f, 'v) prule + 'f, 'v) ctxt"

text‹We provides an easier notation for proof terms (avoiding @{term Inl} and @{term Inr}).›
abbreviation Prule :: "('f, 'v) prule ⇒ ('f, 'v) pterm list ⇒ ('f, 'v) pterm" 
  where "Prule α As ≡ Fun (Inl α) As"
abbreviation Pfun :: "'f  ⇒ ('f, 'v) pterm list ⇒ ('f, 'v) pterm" 
  where "Pfun f As ≡ Fun (Inr f) As"

text‹Also for contexts.›
abbreviation Crule :: "('f, 'v) prule ⇒ ('f, 'v) pterm list ⇒ ('f, 'v) pterm_ctxt ⇒ ('f, 'v) pterm list ⇒('f, 'v) pterm_ctxt" 
  where "Crule α As1 C As2 ≡ More (Inl α) As1 C As2"
abbreviation Cfun :: "'f  ⇒ ('f, 'v) pterm list ⇒ ('f, 'v) pterm_ctxt ⇒ ('f, 'v) pterm list ⇒('f, 'v) pterm_ctxt" 
  where "Cfun f As1 C As2 ≡ More (Inr f) As1 C As2"

text ‹Case analysis on proof terms.›
lemma pterm_cases [case_names Var Pfun Prule, cases type: pterm]:
  "(⋀x. A = Var x ⟹ P) ⟹ (⋀f As. A = Pfun f As ⟹ P) ⟹ (⋀α As. A = Prule α As ⟹ P) ⟹ P"
proof (cases A)
  case (Fun x21 x22)
  show "⋀x21 x22. (⋀x. A = Var x ⟹ P) ⟹ (⋀f As. A = Pfun f As ⟹ P) ⟹ (⋀α As. A = Prule α As ⟹ P) ⟹ A = Fun x21 x22 ⟹ P" 
   using sum.exhaust by auto 
qed

text ‹Induction scheme for proof terms.› 
lemma
  fixes P :: "('f, 'v) pterm ⇒ bool"
  assumes "⋀x. P (Var x)" 
  and "⋀f As. (⋀a. a ∈ set As ⟹ P a) ⟹ P (Pfun f As)"
  and "⋀α As. (⋀a. a ∈ set As ⟹ P a) ⟹ P (Prule α As)"
  shows pterm_induct [case_names Var Pfun Prule, induct type: "pterm"]: "P A"
  using assms proof(induct A)
  case (Fun f ts)
  then show ?case by(cases f) auto
qed simp

text ‹Induction scheme for contexts of proof terms.› 
lemma
  fixes P :: "('f, 'v) pterm_ctxt ⇒ bool"
  assumes "P □" 
  and "⋀f ss1 C ss2. P C ⟹ P (Cfun f ss1 C ss2)"
  and "⋀α ss1 C ss2. P C ⟹ P (Crule α ss1 C ss2)"
  shows pterm_ctxt_induct [case_names Hole Cfun Crule, induct type: "pterm_ctxt"]: "P C"
  using assms proof(induct C)
  case (More f ss1 C ss2)
  then show ?case by(cases f) auto
qed

text ‹Obtain the distinct variables occurring on the left-hand side of a rule in the order they appear.›
abbreviation var_rule :: "('f, 'v) prule ⇒ 'v list" where "var_rule α ≡ vars_distinct (lhs α)"

abbreviation lhs_subst :: "('g, 'v) term list ⇒ ('f, 'v) prule ⇒ ('g, 'v) subst " ("⟨_⟩⇩_" [0,99])
  where "lhs_subst As α ≡ mk_subst Var (zip (var_rule α) As)"

text‹A proof term using only function symbols and variables is an empty step.›
fun is_empty_step :: "('f, 'v) pterm ⇒ bool" where
  "is_empty_step (Var x) = True"
| "is_empty_step (Pfun f As) = list_all is_empty_step As"
| "is_empty_step (Prule α As) = False"

fun is_Prule :: "('f, 'v) pterm ⇒ bool" where
  "is_Prule (Prule _ _) = True"
| "is_Prule _ = False"

text‹Source and target›
fun source :: "('f, 'v) pterm ⇒ ('f, 'v) term" where
  "source (Var x) = Var x"
| "source (Pfun f As) = Fun f (map source As)"
| "source (Prule α As) = lhs α ⋅ ⟨map source As⟩⇩α" 

fun target :: "('f, 'v) pterm ⇒ ('f, 'v) term" where
  "target (Var x) = Var x"
| "target (Pfun f As) = Fun f (map target As)"
| "target (Prule α As) = rhs α ⋅ ⟨map target As⟩⇩α" 

text‹Source also works for proof term contexts in left-linear TRSs.›
fun source_ctxt :: "('f, 'v) pterm_ctxt ⇒ ('f, 'v) ctxt" where
  "source_ctxt □ = □"
| "source_ctxt (Cfun f As1 C As2) = More f (map source As1) (source_ctxt C) (map source As2)"
| "source_ctxt (Crule α As1 C As2) = 
  (let ctxt_pos = (var_poss_list (lhs α))!(length As1);
       placeholder = Var ((vars_term_list (lhs α)) ! (length As1)) in 
   ctxt_of_pos_term (ctxt_pos) (lhs α ⋅ ⟨map source (As1 @ ((placeholder # As2)))⟩⇩α)) ∘⇩c (source_ctxt C)" 

abbreviation "co_initial A B ≡ (source A = source B)" 

text ‹Transform simple terms to proof terms.›
fun to_pterm :: "('f, 'v) term ⇒ ('f, 'v) pterm" where 
  "to_pterm (Var x) = Var x"
| "to_pterm (Fun f ts) = Pfun f (map to_pterm ts)"

text‹Also for contexts.›
fun to_pterm_ctxt :: "('f, 'v) ctxt ⇒ ('f, 'v) pterm_ctxt" where
  "to_pterm_ctxt □ = □"
| "to_pterm_ctxt (More f ss1 C ss2) = Cfun f (map to_pterm ss1) (to_pterm_ctxt C) (map to_pterm ss2)"

subsection‹Frequently Used Locales/Contexts›
text‹Often certain properties about proof terms only hold when the underlying TRS
does not contain variable left-hand sides and/or variables on the right 
are a subset of the variables on the left and/or the TRS is left-linear.›
locale left_lin =
  fixes R :: "('f, 'v) trs"
  assumes left_lin:"left_linear_trs R" 

locale no_var_lhs =
  fixes R :: "('f, 'v) trs"
  assumes no_var_lhs:"Ball R (λ(l, r). is_Fun l)"

locale var_rhs_subset_lhs =
  fixes R :: "('f, 'v) trs"
  assumes varcond:"Ball R (λ(l, r). vars_term r ⊆ vars_term l)"

locale wf_trs = no_var_lhs + var_rhs_subset_lhs
locale left_lin_no_var_lhs = left_lin + no_var_lhs
locale left_lin_wf_trs = left_lin + wf_trs

context wf_trs
begin
lemma wf_trs_alt:
  shows "Trs.wf_trs R" 
  unfolding wf_trs_def' using no_var_lhs varcond by auto 
end

context left_lin
begin
lemma length_var_rule:
  assumes "to_rule α ∈ R" 
  shows "length (var_rule α) = length (vars_term_list (lhs α))" 
  using assms
  by (metis case_prodD left_lin left_linear_trs_def linear_term_var_vars_term_list) 
end

subsection‹Proof Term Predicates›
text ‹The number of arguments of a well-defined proof term over a TRS @{term R} using a rule symbol 
@{term α} corresponds to the number of variables in @{term "lhs α"}. Also the rewrite rule for 
@{term α} must belong to the TRS @{term R}.›
inductive_set wf_pterm :: "('f, 'v) trs ⇒ ('f, 'v) pterm set"
  for R where
 [simp]: "Var x ∈ wf_pterm R"
|[intro]: "∀t ∈ set ts. t ∈ wf_pterm R ⟹  Pfun f ts ∈ wf_pterm R"
|[intro]: "(lhs α, rhs α) ∈ R ⟹ length As = length (var_rule α) ⟹ 
                ∀a ∈ set As. a ∈ wf_pterm R ⟹ Prule α As ∈ wf_pterm R"

inductive_set wf_pterm_ctxt :: "('f, 'v) trs ⇒ ('f, 'v) pterm_ctxt set"
  for R where
 [simp]: "□ ∈ wf_pterm_ctxt R"
|[intro]: "∀s ∈ (set ss1) ∪ (set ss2). s ∈ wf_pterm R ⟹ C ∈ wf_pterm_ctxt R ⟹ 
           Cfun f ss1 C ss2 ∈ wf_pterm_ctxt R"
|[intro]: "(lhs α, rhs α) ∈ R ⟹ (length ss1) + (length ss2) + 1 = length (var_rule α) ⟹ 
           ∀s ∈ (set ss1) ∪ (set ss2). s ∈ wf_pterm R ⟹ C ∈ wf_pterm_ctxt R ⟹
           Crule α ss1 C ss2 ∈ wf_pterm_ctxt R"

lemma fun_well_arg[intro]: 
  assumes "Fun f As ∈ wf_pterm R" "a ∈ set As"
  shows "a ∈ wf_pterm R" 
  using assms wf_pterm.cases by auto

lemma trs_well_ctxt_arg[intro]:
  assumes "More f ss1 C ss2 ∈ wf_pterm_ctxt R" "s ∈ (set ss1) ∪ (set ss2)"
  shows "s ∈ wf_pterm R"
  using assms wf_pterm_ctxt.cases  by blast 

lemma trs_well_ctxt_C[intro]:
  assumes "More f ss1 C ss2 ∈ wf_pterm_ctxt R"
  shows "C ∈ wf_pterm_ctxt R"
  using assms wf_pterm_ctxt.cases by auto

context no_var_lhs
begin
lemma lhs_is_Fun:
  assumes "Prule α Bs ∈ wf_pterm R"
  shows "is_Fun (lhs α)"
  by (metis Inl_inject assms case_prodD is_FunI is_Prule.simps(1) is_Prule.simps(3) is_VarI 
      no_var_lhs.no_var_lhs no_var_lhs_axioms term.inject(2) wf_pterm.simps)
end

lemma lhs_subst_var_well_def:
  assumes "∀i < length As. As!i ∈ wf_pterm R" 
  shows "(⟨As⟩⇩α) x ∈ wf_pterm R"
proof (cases "map_of (zip (var_rule α) As) x")
  case None
  then show ?thesis unfolding mk_subst_def by simp
next
  case (Some a)
  then have "a ∈ set As"
    by (meson in_set_zipE map_of_SomeD) 
  with assms Some show ?thesis 
    unfolding mk_subst_def using in_set_idx by force
qed

lemma lhs_subst_well_def:
  assumes "∀i < length As. As!i ∈ wf_pterm R" "B ∈ wf_pterm R"
  shows "B ⋅ (⟨As⟩⇩α) ∈ wf_pterm R"
  using assms proof(induction B arbitrary: As)
  case (Var x)
  then show ?case using lhs_subst_var_well_def by simp
next
  case (Pfun f Bs)
  from Pfun(3) have "∀b ∈ set Bs. b ∈ wf_pterm R" 
    by blast 
  with Pfun show ?case by fastforce 
next
  case (Prule β Bs)
  from Prule(3) have "∀b ∈ set Bs. b ∈ wf_pterm R" 
    by blast
  moreover have "length (map (λt. t ⋅ ⟨As⟩⇩α) Bs) = length (var_rule β)"
    using Prule(3) wf_pterm.simps by fastforce 
  moreover from Prule(3) have "to_rule β ∈ R"
    using Inl_inject sum.distinct(1) wf_pterm.cases by force 
  ultimately show ?case unfolding eval_term.simps(2) using Prule
    by (simp add: wf_pterm.intros(3)) 
qed

lemma subt_at_is_wf_pterm:
  assumes "p ∈ poss A" and "A ∈ wf_pterm R"
  shows "A|_p ∈ wf_pterm R"
  using assms proof(induct p arbitrary:A)
  case (Cons i p)
  then obtain f As where a:"A = Fun f As" and i:"i < length As" and p:"p ∈ poss (As!i)"
    using args_poss by blast 
  with Cons(3) have "As!i ∈ wf_pterm R"
    using nth_mem by blast 
  with Cons.hyps p a show ?case by simp
qed simp

lemma ctxt_of_pos_term_well:
  assumes "p ∈ poss A" and "A ∈ wf_pterm R"
  shows "ctxt_of_pos_term p A ∈ wf_pterm_ctxt R"
  using assms proof(induct p arbitrary:A)
  case (Cons i p)
  then obtain fs As where a:"A = Fun fs As" and i:"i < length As" and p:"p ∈ poss (As!i)"
    using args_poss by blast 
  with Cons(3) have as:"∀j < length As. As!j ∈ wf_pterm R"
    using nth_mem by blast
  with Cons.hyps p i have IH:"ctxt_of_pos_term p (As!i) ∈ wf_pterm_ctxt R"
    by blast 
  then show ?case proof(cases fs)
    case (Inl α)
    from Cons(3) have "to_rule α ∈ R" unfolding a Inl
      using wf_pterm.cases by auto  
    moreover from Cons(3) i have "length (take i As) + length (drop (Suc i) As) + 1 = length (var_rule α)" 
      unfolding a Inl using wf_pterm.cases by force 
    ultimately show ?thesis 
      unfolding a ctxt_of_pos_term.simps Inl using as IH wf_pterm_ctxt.intros(3)
      by (metis (no_types, opaque_lifting) UnE in_set_conv_nth in_set_dropD in_set_takeD)
  next
    case (Inr f)
    show ?thesis 
      unfolding a ctxt_of_pos_term.simps Inr using as IH wf_pterm_ctxt.intros(2)
      by (metis Cons.prems(2) UnE a fun_well_arg in_set_dropD in_set_takeD) 
  qed 
qed simp

text‹Every normal term is a well-defined proof term.›
lemma to_pterm_wf_pterm[simp]: "to_pterm t ∈ wf_pterm R"
  by (induction t) (simp_all add: wf_pterm.intros(2,3))

lemma to_pterm_trs_ctxt:
  assumes "p ∈ poss (to_pterm s)"
  shows "ctxt_of_pos_term p (to_pterm s) ∈ wf_pterm_ctxt R"
  by (simp add: assms ctxt_of_pos_term_well)

lemma to_pterm_ctxt_wf_pterm_ctxt:
  shows "to_pterm_ctxt C ∈ wf_pterm_ctxt R"
proof(induct C)
  case (More f xs C ys)
  then show ?case unfolding to_pterm_ctxt.simps
    by (metis Un_iff fun_well_arg to_pterm.simps(2) to_pterm_wf_pterm wf_pterm_ctxt.intros(2))
qed simp

lemma ctxt_wf_pterm:
  assumes "A ∈ wf_pterm R" and "p ∈ poss A"
    and "B ∈ wf_pterm R"
  shows "(ctxt_of_pos_term p A)⟨B⟩ ∈ wf_pterm R"
  using assms proof(induct p arbitrary:A)
  case (Cons i p)
  from Cons(3) obtain f As where A:"A = Fun f As" "i < length As" "p ∈ poss (As!i)"
    using args_poss by blast 
  moreover with Cons(2) have "As!i ∈ wf_pterm R"
    using nth_mem by blast 
  ultimately have IH:"(ctxt_of_pos_term p (As!i))⟨B⟩ ∈ wf_pterm R" 
    using Cons.hyps assms(3) by presburger
  from Cons(2) have as:"∀a ∈ set As. a ∈ wf_pterm R" 
    unfolding A by auto
  show ?case proof(cases f)
    case (Inl α)
    from Cons(2) have alpha:"to_rule α ∈ R" 
      unfolding A Inl using wf_pterm.simps by fastforce
    moreover from Cons(2) have "length As = length (var_rule α)" 
      unfolding A Inl using wf_pterm.simps by fastforce
    ultimately show ?thesis 
      unfolding Inl A ctxt_of_pos_term.simps intp_actxt.simps using wf_pterm.intros(3)[OF alpha] IH as A(2)
      by (smt (verit, ccfv_SIG) id_take_nth_drop in_set_conv_nth le_simps(1) length_append list.size(4) nth_append_take nth_append_take_drop_is_nth_conv)   
  next
  case (Inr b)
  show ?thesis unfolding Inr A ctxt_of_pos_term.simps intp_actxt.simps using wf_pterm.intros(2) IH as A(2)
    by (smt (verit, ccfv_SIG) Cons_nth_drop_Suc append_take_drop_id in_set_conv_nth length_append length_nth_simps(2) less_imp_le_nat nth_append_take nth_append_take_drop_is_nth_conv)
  qed 
qed simp

subsection‹'Normal' Terms vs. Proof Terms›

lemma to_pterm_empty: "is_empty_step (to_pterm t)"
proof (induction t)
  case (Fun f ts)
  then have "list_all is_empty_step (map to_pterm ts)" using list_all_iff by force 
  then show ?case by simp
qed simp

text‹Variables remain unchanged.›
lemma vars_to_pterm: "vars_term_list (to_pterm t) = vars_term_list t" 
proof(induction t)
  case (Fun f ts)
  then have *:"map vars_term_list ts = map (vars_term_list ∘ to_pterm) ts" by simp
  show ?case by (simp add: "*" vars_term_list.simps(2)) 
qed (simp add: vars_term_list.simps(1))

lemma poss_list_to_pterm: "poss_list t = poss_list (to_pterm t)"
proof(induction t)
  case (Fun f ts)
  then have *:"map poss_list ts = map (poss_list ∘ to_pterm) ts" by simp
  show ?case by (simp add: "*" poss_list.simps(2)) 
qed (simp add: poss_list.simps(1))

lemma p_in_poss_to_pterm:
  assumes "p ∈ poss t"
  shows "p ∈ poss (to_pterm t)"
  using assms poss_list_to_pterm by (metis poss_list_sound)

lemma var_poss_to_pterm: "var_poss t = var_poss (to_pterm t)" 
proof(induction t)
  case (Fun f ts)
  then have *:"map var_poss ts = map (var_poss ∘ to_pterm) ts" by simp
  then show ?case unfolding var_poss.simps to_pterm.simps
    by auto
qed simp

lemma var_poss_list_to_pterm: "var_poss_list (to_pterm t) = var_poss_list t"
proof(induct t)
  case (Fun f ts)
  then show ?case unfolding var_poss_list.simps to_pterm.simps
    by (metis (no_types, lifting) length_map map_nth_eq_conv nth_mem)
qed simp

text‹@{const to_pterm} distributes over application of substitution.›
lemma to_pterm_subst: 
"to_pterm (t ⋅ σ) = (to_pterm t) ⋅ (to_pterm ∘ σ)"
  by (induct t, auto)

text‹@{const to_pterm} distributes over context.›
lemma to_pterm_ctxt_of_pos_apply_term:
  assumes "p ∈ poss s"
  shows "to_pterm ((ctxt_of_pos_term p s) ⟨t⟩) = (ctxt_of_pos_term p (to_pterm s))⟨to_pterm t⟩"
  using assms proof(induct p arbitrary:s)
  case (Cons i p)
  then obtain f ss where s:"s = Fun f ss" and i:"i < length ss" and p:"p ∈ poss (ss!i)"
    using args_poss by blast
  then show ?case unfolding s to_pterm.simps ctxt_of_pos_term.simps intp_actxt.simps using Cons(1)
    by (simp add: drop_map take_map)
qed simp

text‹Linear terms become linear proof terms.›
lemma to_pterm_linear:
  assumes "linear_term t"
  shows "linear_term (to_pterm t)"
  using assms proof(induction t)
  case (Fun f ts)
  have *:"map vars_term ts = map vars_term (map to_pterm ts)"
    by (metis (mono_tags, lifting) length_map map_nth_eq_conv set_vars_term_list vars_to_pterm)
  with Fun show ?case  by auto
qed simp

lemma lhs_subst_trivial: 
  shows "match (to_pterm (lhs α) ⋅ ⟨As⟩⇩α) (to_pterm (lhs α)) = Some ⟨As⟩⇩α"
  using match_trivial
  by (smt comp_def mem_Collect_eq mk_subst_not_mem set_remdups set_rev set_vars_term_list subsetI subst_domain_def vars_to_pterm)

lemma to_pterm_ctxt_apply_term:
  "to_pterm C⟨t⟩ = (to_pterm_ctxt C) ⟨to_pterm t⟩"
  by(induct C) simp_all


subsection‹Substitutions›
lemma fun_mk_subst[simp]:
  assumes "∀x. f (Var x) = Var x"
  shows "f ∘ (mk_subst Var (zip vs ts)) = mk_subst Var (zip vs (map f ts))"
proof-
  have "∀a. f (case map_of (zip vs ts) a of None ⇒ Var a | Some t ⇒ t)
          = (case map_of (zip vs ts) a of None ⇒ Var a | Some t ⇒ f t)" 
    using assms by (simp add: option.case_eq_if) 
  moreover have "∀a. (case map_of (zip vs (map f ts)) a of None ⇒ Var a | Some x ⇒ x) 
                   = (case (map_of (zip vs ts)) a of None ⇒ Var a | Some t ⇒ f t)" 
    by (simp add:zip_map2 map_of_map option.case_eq_if option.map_sel)
  ultimately show ?thesis unfolding mk_subst_def unfolding comp_def by auto
qed

lemma apply_lhs_subst_var_rule:
  assumes "length ts = length (var_rule α)"
  shows "map (⟨ts⟩⇩α) (var_rule α) = ts"
  using assms by (simp add: mk_subst_distinct map_nth_eq_conv)

lemma match_lhs_subst:
  assumes "match B (to_pterm (lhs α)) = Some σ"
  shows "∃Bs. length Bs = length (var_rule α) ∧ 
         B = (to_pterm (lhs α)) ⋅ ⟨Bs⟩⇩α ∧ 
        (∀x ∈ set (var_rule α). σ x = (⟨Bs⟩⇩α) x)" 
proof-
  obtain Bs where Bs:"length Bs = length (var_rule α)" 
      "∀i < length (var_rule α). Bs!i = σ ((var_rule α)!i)"
    using length_map nth_map by blast
  then have 2:"(∀x ∈ set (var_rule α). σ x = (⟨Bs⟩⇩α) x)"
    by (smt apply_lhs_subst_var_rule in_set_idx nth_map)
  have v:"vars_term (to_pterm (lhs α)) = set (var_rule α)"
    by (metis comp_apply set_remdups set_rev set_vars_term_list vars_to_pterm) 
  from assms have "B = (to_pterm (lhs α)) ⋅ σ"
    using match_matches by blast 
  also have "… = (to_pterm (lhs α)) ⋅ ⟨Bs⟩⇩α"
    by (intro term_subst_eq, insert 2 v, auto) 
  finally show ?thesis using Bs 2 by auto 
qed

lemma apply_subst_wf_pterm:
  assumes "A ∈ wf_pterm R"
    and "∀x ∈ vars_term A. σ x ∈ wf_pterm R"
  shows "A ⋅ σ ∈ wf_pterm R"
  using assms proof(induct A)
  case (2 ts f)
  {fix t assume t:"t ∈ set ts"
    with 2(2) have "(∀x∈vars_term t. σ x ∈ wf_pterm R)"
      by (meson term.set_intros(4)) 
    with t 2(1) have "t ⋅ σ ∈ wf_pterm R"
      by blast
  }
  then show ?case unfolding eval_term.simps by (simp add: wf_pterm.intros(2))
next
  case (3 α As)
  {fix a assume a:"a ∈ set As"
    with 3(4) have "(∀x∈vars_term a. σ x ∈ wf_pterm R)"
      by (meson term.set_intros(4)) 
    with a 3(3) have "a ⋅ σ ∈ wf_pterm R"
      by blast
  }
  with 3(1,2) show ?case unfolding eval_term.simps by (simp add: wf_pterm.intros(3))
qed simp

lemma subst_well_def:
  assumes "B ∈ wf_pterm R" "A ⋅ σ = B" "x ∈ vars_term A"
  shows "σ x ∈ wf_pterm R"
  using assms by (metis (no_types, lifting) poss_imp_subst_poss eval_term.simps(1) subt_at_is_wf_pterm subt_at_subst vars_term_poss_subt_at)

lemma lhs_subst_args_wf_pterm:
  assumes "to_pterm (lhs α) ⋅ ⟨As⟩⇩α ∈ wf_pterm R" and "length As = length (var_rule α)"
  shows "∀a ∈ set As. a ∈ wf_pterm R"
proof-
 from assms have "map (⟨As⟩⇩α) (var_rule α) = As"
    using apply_lhs_subst_var_rule by blast 
  with assms show ?thesis
    by (smt comp_apply in_set_idx map_nth_eq_conv nth_mem set_remdups set_rev set_vars_term_list subst_well_def vars_to_pterm) 
qed
 
lemma match_well_def:
  assumes "B ∈ wf_pterm R" "match B A = Some σ"
  shows "∀i < length (vars_distinct A). σ ((vars_distinct A) ! i) ∈ wf_pterm R"
  using assms subst_well_def match_matches
  by (smt comp_apply nth_mem set_remdups set_rev set_vars_term_list)

lemma subst_imp_well_def:
  assumes "A ⋅ σ ∈ wf_pterm R"
  shows "A ∈ wf_pterm R"
  using assms proof(induct A)
  case (Pfun f As)
  {fix i assume i:"i < length As"
    with Pfun(2) have "(As!i) ⋅ σ ∈ wf_pterm R" 
      by auto
    with Pfun(1) i have "As!i ∈ wf_pterm R"
      by simp 
  }
  then show ?case using wf_pterm.intros(2)
    by (metis in_set_idx)
next
  case (Prule α As)
  {fix i assume i:"i < length As"
    with Prule(2) have "(As!i) ⋅ σ ∈ wf_pterm R" 
      by auto
    with Prule(1) i have "As!i ∈ wf_pterm R"
      by simp 
  }
  moreover from Prule(2) have "to_rule α ∈ R" "length As = length (var_rule α)"
    using wf_pterm.cases by force+
  ultimately show ?case using wf_pterm.intros(3) Prule(2) 
    by (metis in_set_idx)
qed simp

lemma lhs_subst_var_i:
  assumes "x = (var_rule α)!i" and "i < length (var_rule α)" and "i < length As"
  shows "(⟨As⟩⇩α) x = As!i"
  using assms mk_subst_distinct distinct_remdups by (metis comp_apply distinct_rev)

lemma lhs_subst_not_var_i:
  assumes "¬(∃i < length As. i < length (var_rule α) ∧ x = (var_rule α)!i)"
  shows "(⟨As⟩⇩α) x = Var x"
  using assms proof(rule contrapos_np)
  {assume "(⟨As⟩⇩α) x ≠ Var x"
    then obtain i where "i < length (zip (var_rule α) As)" and "(var_rule α)!i = x" 
      unfolding mk_subst_def by (smt assms imageE in_set_zip map_of_eq_None_iff option.case_eq_if) 
    then show "∃i<length As. i < length (var_rule α) ∧ x = var_rule α ! i"
      by auto 
  }
qed

lemma lhs_subst_upd:
  assumes "length ss1 < length (var_rule α)"
  shows "((⟨ss1 @ t # ss2⟩⇩α) ((var_rule α)!(length ss1) := s)) = ⟨ss1 @ s # ss2⟩⇩α"
proof
  fix x
  show "((⟨ss1 @ t # ss2⟩⇩α)(var_rule α ! length ss1 := s)) x = (⟨ss1 @ s # ss2⟩⇩α) x" proof(cases "x = (var_rule α)!(length ss1)")
    case True
    with assms have "((⟨ss1 @ t # ss2⟩⇩α)(var_rule α ! length ss1 := s)) x = s"
      by simp  
    moreover from assms have "(⟨ss1 @ s # ss2⟩⇩α) x = s" unfolding True
      by (smt (verit, del_insts) add.commute add_Suc_right le_add_same_cancel2 le_imp_less_Suc length_append length_nth_simps(2) lhs_subst_var_i nth_append_length zero_order(1)) 
    ultimately show ?thesis by simp
  next
    case False
    then show ?thesis
      by (smt (verit, del_insts) append_Cons_nth_not_middle fun_upd_apply length_append length_nth_simps(2) lhs_subst_not_var_i lhs_subst_var_i) 
  qed
qed

lemma eval_lhs_subst:
  assumes l:"length (var_rule α) = length As" 
  shows "(to_pterm (lhs α)) ⋅ ⟨As⟩⇩α ⋅ σ = (to_pterm (lhs α)) ⋅ ⟨map (λa. a ⋅ σ) As⟩⇩α" 
proof-
  {fix x assume "x ∈ vars_term (to_pterm (lhs α))" 
    then obtain i where i:"i < length (var_rule α)" "(var_rule α) !i = x"
      using vars_to_pterm by (metis in_set_conv_nth set_vars_term_list vars_term_list_vars_distinct) 
    with l have "(⟨As⟩⇩α) x = As!i"
      by (metis lhs_subst_var_i) 
    then have 1:"(⟨As⟩⇩α ∘⇩s σ) x = As!i ⋅ σ"
      unfolding subst_compose_def by simp
    from i l have "(⟨map (λa. a ⋅ σ) As⟩⇩α) x = map (λa. a ⋅ σ) As ! i" 
      using lhs_subst_var_i by (metis length_map) 
    with 1 i l have "(⟨As⟩⇩α ∘⇩s σ) x = (⟨map (λa. a ⋅ σ) As⟩⇩α) x" by simp
  }
  then show ?thesis
    by (smt (verit, ccfv_SIG) eval_same_vars_cong subst_subst_compose) 
qed

lemma var_rule_pos_subst:
  assumes "i < length (var_rule α)" "length ss = length (var_rule α)" 
    and "p ∈ poss (lhs α)" "Var ((var_rule α)!i) = (lhs α)|_p" 
  shows "lhs α ⋅ ⟨ss⟩⇩α |_ (p@q) = (ss!i)|_q"
proof-
  from assms(1,2) have "(⟨ss⟩⇩α) ((var_rule α)!i) = ss!i"
    using lhs_subst_var_i by force 
  with assms(3,4) show ?thesis by auto
qed

lemma lhs_subst_var_rule:
  assumes "vars_term t ⊆ vars_term (lhs α)" 
  shows "t ⋅ ⟨map σ (var_rule α)⟩⇩α = t ⋅ σ"
  using assms by (smt (verit, ccfv_SIG) apply_lhs_subst_var_rule comp_apply length_map map_eq_conv set_remdups set_rev set_vars_term_list subsetD term_subst_eq_conv)

subsection‹Contexts›
lemma match_lhs_context:
  assumes "i < length (vars_term_list t) ∧ p = (var_poss_list t)!i"
    and "linear_term t"
    and "match (((ctxt_of_pos_term p (t ⋅ σ)))⟨B⟩) t = Some τ"
shows "map τ (vars_term_list t) = (map σ (vars_term_list t))[i := B] "
proof-
  from assms have "(ctxt_of_pos_term p (t ⋅ σ))⟨B⟩ = t ⋅ (σ(vars_term_list t!i := B))"
    using ctxt_apply_term_subst by blast
  with assms(3) have *:"(∀x∈vars_term t. (σ(vars_term_list t!i := B)) x = τ x)" 
    using match_complete' by (metis option.inject)
  from assms(2) have "distinct (vars_term_list t)"
    by (metis distinct_remdups distinct_rev linear_term_var_vars_term_list o_apply) 
  with * assms(1) show ?thesis
    by (smt (verit, ccfv_threshold) fun_upd_other fun_upd_same length_list_update length_map map_nth_eq_conv nth_eq_iff_index_eq nth_list_update nth_mem set_vars_term_list)
qed

lemma ctxt_lhs_subst:
  assumes i:"i < length (var_poss_list (lhs α))" and l:"length As = length (var_rule α)"
    and p1:"p1 = var_poss_list (lhs α) ! i" and lin:"linear_term (lhs α)" 
    and "p2 ∈ poss (As!i)"
  shows "(ctxt_of_pos_term (p1 @ p2) (to_pterm (lhs α) ⋅ ⟨As⟩⇩α))⟨A⟩ = 
         (to_pterm (lhs α)) ⋅ ⟨take i As @ (ctxt_of_pos_term p2 (As!i))⟨A⟩ # drop (Suc i) As⟩⇩α"
proof-
  have l2:"length (var_poss_list (lhs α)) = length (var_rule α)" 
    using lin by (metis length_var_poss_list linear_term_var_vars_term_list) 
  from p1 i have p1_pos:"p1 ∈ poss (to_pterm (lhs α))"
    by (metis nth_mem var_poss_imp_poss var_poss_list_sound var_poss_to_pterm) 
  have sub:"(to_pterm (lhs α))|_p1 = Var (vars_term_list (lhs α)!i)"
    by (metis i length_var_poss_list p1 var_poss_list_to_pterm vars_term_list_var_poss_list vars_to_pterm)
  have **: "(to_pterm (lhs α) ⋅ ⟨As⟩⇩α)|_p1 = As!i" 
    unfolding subt_at_subst[OF p1_pos] sub eval_term.simps using i l l2 by (metis lhs_subst_var_i lin linear_term_var_vars_term_list) 
  then have *:"(ctxt_of_pos_term (p1 @ p2) (to_pterm (lhs α) ⋅ ⟨As⟩⇩α)) = ((ctxt_of_pos_term p1 (to_pterm (lhs α))) ⋅⇩c ⟨As⟩⇩α) ∘⇩c (ctxt_of_pos_term p2 (As!i))"
    using ctxt_of_pos_term_append ctxt_of_pos_term_subst by (metis p1_pos poss_imp_subst_poss) 
  show ?thesis
    by (smt (verit, ccfv_threshold) * ** ctxt_ctxt_compose
        ctxt_subst_apply lhs_subst_upd append_Cons_nth_not_middle 
        i id_take_nth_drop l l2 less_imp_le_nat lin linear_term_var_vars_term_list 
        nth_append_take p1_pos sub to_pterm_linear
        ctxt_of_pos_term_append ctxt_supt_id eval_term.simps(1) poss_imp_subst_poss
        replace_at_append_subst subt_at_subst)
qed

lemma ctxt_rule_obtain_pos:
  assumes iq:"i#q ∈ poss (Prule α As)"
    and p_pos:"p ∈ poss (source (Prule α As))"
    and ctxt:"source_ctxt (ctxt_of_pos_term (i#q) (Prule α As)) = ctxt_of_pos_term p (source (Prule α As))"
    and lin:"linear_term (lhs α)"
    and l:"length As = length (var_rule α)" 
  shows "∃p1 p2. p = p1@p2 ∧ p1 = var_poss_list (lhs α)!i ∧ p2 ∈ poss (source (As!i))" 
proof-
  from iq have i:"i < length As"
    by simp 
  let ?p1="var_poss_list (lhs α)!i"
  have p1:"(var_poss_list (lhs α) ! length (take i As)) = ?p1"
    using i by fastforce 
  have p1_pos:"?p1 ∈ poss (lhs α)"
    by (metis i l length_var_poss_list lin linear_term_var_vars_term_list nth_mem var_poss_imp_poss var_poss_list_sound)
  then have *:"source_ctxt (ctxt_of_pos_term (i # q) (Prule α As)) = ((ctxt_of_pos_term ?p1 (lhs α)) ⋅⇩c ⟨map source (take i As @ Var (vars_term_list (lhs α) ! length (take i As)) # drop (Suc i) As)⟩⇩α) ∘⇩c
    source_ctxt (ctxt_of_pos_term q (As ! i))" 
    unfolding ctxt_of_pos_term.simps source_ctxt.simps Let_def p1 by (simp add: ctxt_of_pos_term_subst)
  from ctxt have "?p1  ≤⇩p p" 
    unfolding * using p1_pos p_pos unfolding source.simps using ctxt_subst_comp_pos by blast
  then obtain p2 where p:"p = ?p1@p2"
    using less_eq_pos_def by force 
  have "(lhs α)|_?p1 = Var (vars_term_list (lhs α) !i)"
    by (metis i l lin linear_term_var_vars_term_list vars_term_list_var_poss_list) 
  moreover have "Var (vars_term_list (lhs α) !i) ⋅ ⟨map source As⟩⇩α = source (As!i)"
    unfolding eval_term.simps using lhs_subst_var_i i l by (smt (verit, best) length_map lin linear_term_var_vars_term_list nth_map) 
  ultimately have "p2 ∈ poss (source (As!i))" 
    using p_pos unfolding p using p1_pos by auto 
  with p show ?thesis by simp
qed

subsection‹Source and Target›
lemma source_empty_step:
  assumes "is_empty_step t"
  shows "to_pterm (source t) = t"
using assms by (induction t) (simp_all add: list_all_length map_nth_eq_conv)

lemma empty_coinitial:
  shows "co_initial A t ⟹ is_empty_step t ⟹ to_pterm (source A) = t"
  by (simp add: source_empty_step)

lemma source_to_pterm[simp]: "source (to_pterm t) = t"
  by (induction t) (simp_all add: map_nth_eq_conv)
  
lemma target_to_pterm[simp]: "target (to_pterm t) = t"
  by (induction t) (simp_all add: map_nth_eq_conv)

lemma vars_term_source:
  assumes "A ∈ wf_pterm R"
  shows "vars_term A = vars_term (source A)"
  using assms proof(induct A)
  case (3 α As)
  show ?case proof
    {fix x assume "x ∈ vars_term (Prule α As)"
      then obtain i where i:"i < length As" "x ∈ vars_term (As!i)"
        by (metis term.sel(4) var_imp_var_of_arg) 
      from i(1) 3(2) obtain j where j:"j < length (vars_term_list (lhs α))" "vars_term_list (lhs α)!j = var_rule α !i"
        by (metis comp_apply in_set_idx nth_mem set_remdups set_rev)
      let ?p="(var_poss_list (lhs α)!j)"
      from j have p:"?p ∈ poss (lhs α)"
        by (metis in_set_conv_nth length_var_poss_list var_poss_imp_poss var_poss_list_sound) 
      with 3(2) i(1) j have "source (Prule α As) |_ ?p = source (As!i)" 
        using mk_subst_distinct unfolding source.simps
        by (smt (verit, best) comp_apply distinct_remdups distinct_rev filter_cong length_map map_nth_conv mk_subst_same eval_term.simps(1) subt_at_subst vars_term_list_var_poss_list)  
      with 3(3) have "x ∈ vars_term (source (Prule α As))"
        unfolding source.simps using vars_term_subt_at p
        by (smt (verit, ccfv_SIG) i nth_mem poss_imp_subst_poss subsetD)
    } 
    then show "vars_term (Prule α As) ⊆ vars_term (source (Prule α As))"
      by blast 
    {fix x assume "x ∈ vars_term (source (Prule α As))"
      then obtain y where y:"y ∈ vars_term (lhs α)"  "x ∈ vars_term ((⟨map source As⟩⇩α) y)"
        using vars_term_subst by force 
      then obtain i where i:"i < length (var_rule α)" "y = var_rule α!i"
        by (metis in_set_idx set_vars_term_list vars_term_list_vars_distinct) 
      with y(2) 3(2) have "x ∈ vars_term (source (As!i))"
        by (simp add: mk_subst_distinct) 
      with 3 i(1) have "x ∈ vars_term (Prule α As)"
        by (metis nth_mem term.set_intros(4))
    }
    then show "vars_term (source (Prule α As)) ⊆ vars_term (Prule α As)" 
      by blast
  qed
qed auto

context var_rhs_subset_lhs
begin
lemma vars_term_target:
  assumes "A ∈ wf_pterm R"
  shows "vars_term (target A) ⊆ vars_term A"
  using assms proof(induct A)
  case (3 α As)
  show ?case proof
  fix x assume "x ∈ vars_term (target (Prule α As))"
    then obtain y where y:"y ∈ vars_term (rhs α)"  "x ∈ vars_term ((⟨map target As⟩⇩α) y)"
      using vars_term_subst by force 
    then have "y ∈ vars_term (lhs α)"
      using "3.hyps"(1) varcond by auto 
    then obtain i where i:"i < length (var_rule α)" "y = var_rule α!i"
      by (metis in_set_idx set_vars_term_list vars_term_list_vars_distinct) 
    with y(2) 3(2) have "x ∈ vars_term (target (As!i))"
      by (simp add: mk_subst_distinct) 
    with 3 i(1) show "x ∈ vars_term (Prule α As)"
      by fastforce
  qed
qed auto
end

lemma linear_source_imp_linear_pterm:
  assumes "A ∈ wf_pterm R" "linear_term (source A)" 
  shows "linear_term A" 
  using assms proof(induct A)
  case (2 As f)
  then show ?case unfolding source.simps linear_term.simps using vars_term_source
    by (smt (verit, ccfv_SIG) in_set_idx length_map map_equality_iff nth_map nth_mem)
next
  case (3 α As)
  {fix a assume a:"a ∈ set As"
    with 3(2) obtain i where i:"i < length (var_rule α)" "As!i = a"
      by (metis in_set_idx) 
    let ?x="var_rule α ! i"
    from i have "?x ∈ vars_term (lhs α)"
      by (metis comp_apply nth_mem set_remdups set_rev set_vars_term_list)
    then obtain p where "p ∈ poss (lhs α)" "lhs α |_p = Var ?x"
      by (meson vars_term_poss_subt_at) 
    then have "source (Prule α As) ⊵ source a" 
      unfolding source.simps using lhs_subst_var_i[of ?x α i As] i 3(2)
      by (smt (verit, best) ‹var_rule α ! i ∈ vars_term (lhs α)› apply_lhs_subst_var_rule eval_term.simps(1) length_map map_nth_conv supteq_subst vars_term_supteq)
    then have "linear_term (source a)" 
      using 3(4) by (metis subt_at_linear supteq_imp_subt_at) 
    with 3(3) a have "linear_term a" by simp
  }
  moreover have "is_partition (map vars_term As)" proof-
    {fix i j assume i:"i < length As" and j:"j < length As" and ij:"i ≠ j"
      let ?x="var_rule α ! i" and ?y="var_rule α ! j" 
      from i j ij 3(2) have xy:"?x ≠ ?y"
        by (simp add: nth_eq_iff_index_eq) 
      from i 3(2) have "?x ∈ vars_term (lhs α)"
        by (metis comp_apply nth_mem set_remdups set_rev set_vars_term_list)
      then obtain p where p:"p ∈ poss (lhs α)" "lhs α |_p = Var ?x"
        by (meson vars_term_poss_subt_at) 
      from j 3(2) have "?y ∈ vars_term (lhs α)"
        by (metis comp_apply nth_mem set_remdups set_rev set_vars_term_list)
      then obtain q where q:"q ∈ poss (lhs α)" "lhs α |_q = Var ?y"
        by (meson vars_term_poss_subt_at) 
      from xy p q have "p ⊥ q"
        using less_eq_pos_def parallel_pos by auto 
      moreover have "source (Prule α As) |_p = source (As!i)" 
        unfolding source.simps by (metis (mono_tags, lifting) "3.hyps"(2) eval_term.simps(1) i length_map lhs_subst_var_i nth_map p subt_at_subst) 
      moreover have "source (Prule α As) |_q = source (As!j)" 
        unfolding source.simps by (metis (mono_tags, lifting) "3.hyps"(2) eval_term.simps(1) j length_map lhs_subst_var_i nth_map q subt_at_subst) 
      ultimately have "vars_term (source (As!i)) ∩ vars_term (source (As!j)) = {}" 
        using 3(4) by (metis linear_subterms_disjoint_vars p(1) poss_imp_subst_poss q(1) source.simps(3)) 
      then have "vars_term (As!i) ∩ vars_term (As!j) = {}"
        using vars_term_source 3(3) i j using nth_mem by blast
    }
    then show ?thesis 
      unfolding is_partition_alt is_partition_alt_def by simp
    qed
  ultimately show ?case unfolding source.simps linear_term.simps by simp
qed simp

context var_rhs_subset_lhs
begin
lemma target_apply_subst:
  assumes "A ∈ wf_pterm R"
  shows "target (A ⋅ σ) = (target A) ⋅ (target ∘ σ)"
using assms(1) proof(induct A)
  case (2 ts f)
  then have "(map target (map (λt. t ⋅ σ) ts)) = (map (λt. t ⋅ (target ∘ σ)) (map target ts))"
    unfolding map_map o_def by auto
  then show ?case unfolding eval_term.simps target.simps by simp
next
  case (3 α As)
  have id:"∀ x ∈ vars_term (rhs α). (⟨map (target ∘ (λt. t ⋅ σ)) As⟩⇩α) x = (⟨map target As⟩⇩α ∘⇩s (target ∘ σ)) x"
    proof-
      have vars:"vars_term (rhs α) ⊆ set (var_rule α)" 
        using 3(1) varcond by auto
    { fix i assume i:"i < length (var_rule α)"
      with 3 have "(⟨map (target ∘ (λt. t ⋅ σ)) As⟩⇩α) ((var_rule α)!i) = target ((As!i) ⋅ σ)" 
        by (simp add: mk_subst_distinct)
      also have "... = target (As!i) ⋅ (target ∘ σ)" 
        using 3 i by (metis nth_mem) 
      also have "... = (⟨map target As⟩⇩α ∘⇩s (target ∘ σ)) ((var_rule α)!i)" 
        using 3 i unfolding subst_compose_def by (simp add: mk_subst_distinct)
      finally have "(⟨map (target ∘ (λt. t ⋅ σ)) As⟩⇩α) ((var_rule α)!i) = (⟨map target As⟩⇩α ∘⇩s (target ∘ σ)) ((var_rule α)!i)" .
    } with vars show ?thesis by (smt (z3) in_mono in_set_conv_nth) 
    qed
  have "target ((Prule α As) ⋅ σ) = (rhs α) ⋅ ⟨map (target ∘ (λt. t ⋅ σ)) As⟩⇩α" 
    unfolding eval_term.simps(2) by simp
  also have "... = (rhs α) ⋅ (⟨map target As⟩⇩α ∘⇩s (target ∘ σ))" 
    using id by (meson term_subst_eq)
  also have "... = (target (Prule α As)) ⋅ (target ∘ σ)" by simp
  finally show ?case .
qed simp
end

context var_rhs_subset_lhs
begin
lemma tgt_subst_simp:
assumes "A ∈ wf_pterm R"
  shows "target (A ⋅ σ) = target ((to_pterm (target A)) ⋅ σ)"
  by (metis assms target_apply_subst target_to_pterm to_pterm_wf_pterm)
end

lemma target_empty_apply_subst:
  assumes "is_empty_step t"
  shows "target (t ⋅ σ) = (target t) ⋅ (target ∘ σ)"
using assms proof(induction t)
  case (Var x)
  then show ?case by (metis comp_apply eval_term.simps(1) target.simps(1))
next
  case (Pfun f As)
  from Pfun(2) have "∀a ∈ set As. is_empty_step a"
    by (simp add: Ball_set_list_all) 
  with Pfun(1) show ?case by simp
next
  case (Prule α As)
  then show ?case
    using is_empty_step.simps(3) by blast
qed

lemma source_ctxt_comp:"source_ctxt (C1 ∘⇩c C2) = source_ctxt C1 ∘⇩c source_ctxt C2"
  by(induct C1) (simp_all add:ctxt_monoid_mult.mult_assoc)

lemma context_source: "source (A⟨B⟩) = source (A⟨to_pterm (source B)⟩)" 
proof(induct A rule:actxt.induct)
  case (More f ss1 A ss2)
  then show ?case by(cases f) simp_all
qed simp

lemma context_target: "target (A⟨B⟩) = target (A⟨to_pterm (target B)⟩)" 
proof(induct A rule:actxt.induct)
  case (More f ss1 A ss2)
  then show ?case by(cases f) simp_all
qed simp

lemma source_to_pterm_ctxt:
  "source ((to_pterm_ctxt C)⟨A⟩) = C⟨source A⟩"
  by (metis context_source source_to_pterm to_pterm_ctxt_apply_term)   

lemma target_to_pterm_ctxt:
  "target ((to_pterm_ctxt C)⟨A⟩) = C⟨target A⟩"   
  by (metis context_target target_to_pterm to_pterm_ctxt_apply_term)   

lemma source_ctxt_to_pterm: 
  assumes "p ∈ poss s"
  shows "source_ctxt (ctxt_of_pos_term p (to_pterm s)) = ctxt_of_pos_term p s" 
using assms proof(induct p arbitrary:s)
  case (Cons i p)
  then obtain f ss where s:"s = Fun f ss" and "i < length ss" and "p ∈ poss (ss!i)"
    using args_poss by blast 
  then show ?case 
    unfolding s to_pterm.simps ctxt_of_pos_term.simps source_ctxt.simps using Cons(1)
    by (smt (verit, best) drop_map nth_map source.simps(2) source_to_pterm take_map term.inject(2) to_pterm.simps(2))
qed simp

lemma to_pterm_ctxt_at_pos:
  assumes "p ∈ poss s"
  shows  "ctxt_of_pos_term p (to_pterm s) = to_pterm_ctxt (ctxt_of_pos_term p s)"
using assms proof(induct p arbitrary:s)
  case (Cons i p)
  then obtain f ss where s:"s = Fun f ss"
    using args_poss by blast 
  with Cons show ?case
    using drop_map s take_map by force
qed simp

lemma to_pterm_ctxt_hole_pos: "hole_pos C = hole_pos (to_pterm_ctxt C)"
  by(induct C) simp_all

lemma source_to_pterm_ctxt':
  assumes "q ∈ poss s"
  shows "source_ctxt (to_pterm_ctxt (ctxt_of_pos_term q s)) = ctxt_of_pos_term q s"
using assms proof(induct q arbitrary: s)
  case (Cons i q)
  then obtain f ss where s:"s = Fun f ss" and i:"i < length ss"
    by (meson args_poss) 
  with Cons have IH:"source_ctxt (to_pterm_ctxt (ctxt_of_pos_term q (ss!i))) = ctxt_of_pos_term q (ss!i)"
    by auto
  with i show ?case unfolding s ctxt_of_pos_term.simps to_pterm_ctxt.simps source_ctxt.simps
    using source_to_pterm by (metis source.simps(2) term.sel(4) to_pterm.simps(2)) 
qed simp

lemma to_pterm_ctxt_comp: "to_pterm_ctxt (C ∘⇩c D) = to_pterm_ctxt C ∘⇩c to_pterm_ctxt D"
  by(induct C) simp_all

lemma source_apply_subst: 
  assumes "A ∈ wf_pterm R"
  shows "source (A ⋅ σ) = (source A) ⋅ (source ∘ σ)"
using assms proof(induct A)
  case (3 α As)
  have id:"∀ x ∈ vars_term (lhs α). (⟨map (source ∘ (λt. t ⋅ σ)) As⟩⇩α) x = (⟨map source As⟩⇩α ∘⇩s (source ∘ σ)) x"
    proof-
      have vars:"vars_term (lhs α) = set (var_rule α)" by simp
    { fix i assume i:"i < length (var_rule α)"
      with 3 have "(⟨map (source ∘ (λt. t ⋅ σ)) As⟩⇩α) ((var_rule α)!i) = source ((As!i) ⋅ σ)" 
        by (simp add: mk_subst_distinct)
      also have "... = source (As!i) ⋅ (source ∘ σ)" 
        using 3 i by (metis nth_mem) 
      also have "... = (⟨map source As⟩⇩α ∘⇩s (source ∘ σ)) ((var_rule α)!i)" 
        using 3 i unfolding subst_compose_def by (simp add: mk_subst_distinct)
      finally have "(⟨map (source ∘ (λt. t ⋅ σ)) As⟩⇩α) ((var_rule α)!i) = (⟨map source As⟩⇩α ∘⇩s (source ∘ σ)) ((var_rule α)!i)" .
    } with vars show ?thesis by (metis in_set_idx) 
  qed
  have "source ((Prule α As) ⋅ σ) = (lhs α) ⋅ ⟨map (source ∘ (λt. t ⋅ σ)) As⟩⇩α" 
    unfolding eval_term.simps(2) by simp
  also have "... = (lhs α) ⋅ (⟨map source As⟩⇩α ∘⇩s (source ∘ σ))" 
    using id by (meson term_subst_eq)
  also have "... = (source (Prule α As)) ⋅ (source ∘ σ)" by simp
  finally show ?case .
qed simp_all

lemma ctxt_of_pos_term_at_var_subst: 
  assumes "linear_term t"
    and "p ∈ poss t" and "t|_p = Var x"
    and "∀y ∈ vars_term t. y ≠ x ⟶ τ y = σ y"
  shows "ctxt_of_pos_term p (t ⋅ τ) = ctxt_of_pos_term p (t ⋅ σ)"
  using assms proof(induct t arbitrary:p)
  case (Fun f ts)
  from Fun(3,4) obtain i p' where p:"p = i#p'" and i:"i < length ts" and p':"p' ∈ poss (ts!i)"
    by auto 
  with Fun(4) have x:"ts!i |_p' = Var x" 
    by simp
  {fix j assume j:"j < length ts" "j ≠ i"
    from Fun(2) have "x ∉ vars_term (ts!j)"
      by (metis i j p' subset_eq term.set_intros(3) var_in_linear_args vars_term_subt_at x)  
    with Fun(5) j have "ts!j ⋅ τ = ts!j ⋅ σ"
      by (metis (no_types, lifting) nth_mem term.set_intros(4) term_subst_eq)
    then have "(map (λt. t ⋅ τ) ts)!j = (map (λt. t ⋅ σ) ts)!j"
      by (simp add: j) 
  }note args=this
  from args have args1:"take i (map (λt. t ⋅ τ) ts) = take i (map (λt. t ⋅ σ) ts)"
     using nth_take_lemma[of i "(map (λt. t ⋅ τ) ts)" "(map (λt. t ⋅ σ) ts)"] i by simp 
  from args have args2:"drop (Suc i) (map (λt. t ⋅ τ) ts) = drop (Suc i) (map (λt. t ⋅ σ) ts)"
     using nth_drop_equal[of "(map (λt. t ⋅ τ) ts)" "(map (λt. t ⋅ σ) ts)" "Suc i"] i by simp 
  from Fun(1,2,5) i have IH:"ctxt_of_pos_term p' ((ts!i) ⋅ τ) = ctxt_of_pos_term p' ((ts!i) ⋅ σ)"
    by (simp add: p' x)
  with args1 args2 show ?case 
    unfolding p eval_term.simps ctxt_of_pos_term.simps by (simp add: i)
qed simp

context left_lin
begin

lemma source_ctxt_apply_subst: 
  assumes "C ∈ wf_pterm_ctxt R"
  shows "source_ctxt (C ⋅⇩c σ) = (source_ctxt C) ⋅⇩c (source ∘ σ)"
using assms proof(induct C)
  case (2 ss1 ss2 C f)
  then show ?case 
    unfolding source_ctxt.simps actxt.simps 2 using source_apply_subst by auto
next
  case (3 α ss1 ss2 C)
  let ?p="(var_poss_list (lhs α) ! length ss1)"
  let ?x="(vars_term_list (lhs α) ! length ss1)"
  have var_at_p:"(lhs α)|_?p = Var ?x"
    by (metis "3.hyps"(2) add_lessD1 length_remdups_leq length_rev less_add_one o_apply order_less_le_trans vars_term_list_var_poss_list) 
  from 3(2) have pos1:"?p ∈ poss (lhs α)"
    by (metis add_lessD1 comp_apply length_remdups_leq length_rev length_var_poss_list less_add_one nth_mem order_less_le_trans var_poss_imp_poss var_poss_list_sound) 
  then have pos:"?p ∈ poss (lhs α ⋅ ⟨map source (ss1 @ Var (vars_term_list (lhs α) ! length ss1) # ss2)⟩⇩α)"
    using poss_imp_subst_poss by blast 
  have lin:"linear_term (lhs α)" 
    using 3(1) left_lin using left_linear_trs_def by fastforce 
  {fix y assume "y ∈ vars_term (lhs α)" and x:"y ≠ ?x"
    then obtain i where i:"i < length (var_rule α)" "var_rule α ! i = y"
      by (metis in_set_idx lin linear_term_var_vars_term_list set_vars_term_list) 
    with x consider "i < length ss1" | "i > length ss1 ∧ i < length (var_rule α)"
      using lin linear_term_var_vars_term_list nat_neq_iff by fastforce
    then have "(⟨map source (map (λt. t ⋅ σ) ss1 @ Var ?x # map (λt. t ⋅ σ) ss2)⟩⇩α) y = ((⟨map source (ss1 @ Var ?x # ss2)⟩⇩α) y) ⋅ (source ∘ σ)"
    proof(cases)
      case 1
      with i have "(⟨map source (map (λt. t ⋅ σ) ss1 @ Var ?x # map (λt. t ⋅ σ) ss2)⟩⇩α) y = source ((ss1!i) ⋅ σ)"
        by (smt (z3) "3.hyps"(2) One_nat_def add.right_neutral add_Suc_right append_Cons_nth_left comp_apply distinct_remdups distinct_rev length_append length_map length_nth_simps(2) map_nth_eq_conv mk_subst_same) 
      moreover from i 1 have "(⟨map source (ss1 @ Var ?x # ss2)⟩⇩α) y = source (ss1!i)"
        by (smt (verit, ccfv_threshold) "3.hyps"(2) One_nat_def ab_semigroup_add_class.add_ac(1) append_Cons_nth_left comp_apply distinct_remdups distinct_rev length_append length_map list.size(4) map_nth_eq_conv mk_subst_distinct) 
      moreover have "ss1!i ∈ wf_pterm R" 
        using 3(3) 1 by (meson UnCI nth_mem) 
      ultimately show ?thesis 
        using source_apply_subst by auto
    next
      case 2
      let ?i="i - ((length ss1)+1)"
      have i':"?i < length ss2" 
        using 3(2) 2 by (simp add: less_diff_conv2) 
      have i1:"(map source (map (λt. t ⋅ σ) ss1 @ Var ?x # map (λt. t ⋅ σ) ss2))!i = source ((ss2!?i) ⋅ σ)" proof-
        have i'':"i = length (map source (map (λt. t ⋅ σ) ss1 @ [Var ?x])) + ?i" 
          unfolding length_append length_map using "2" by force 
        show ?thesis unfolding map_append list.map 
          using i' i'' nth_append_length_plus[of "(map source (map (λt. t ⋅ σ) ss1 @ [Var (vars_term_list (lhs α) ! length ss1)]))" "map source (map (λt. t ⋅ σ) ss2)"]
          by (smt (verit, del_insts) Cons_eq_appendI append_Nil append_assoc length_map list.simps(9) map_append nth_map) 
      qed
      have i2:"map source (ss1 @ Var ?x # ss2) ! i = source (ss2!?i)" proof-
        have i'':"i = length (map source (ss1 @ [Var ?x])) + ?i" 
          unfolding length_append length_map using "2" by force 
        show ?thesis unfolding map_append list.map 
          using i' i'' nth_append_length_plus[of "(map source (ss1 @ [Var (vars_term_list (lhs α) ! length ss1)]))" "map source ss2"]
          by (smt (verit, del_insts) append.left_neutral append_Cons append_assoc length_map list.simps(9) map_append nth_map) 
      qed
      from i1 2 have "(⟨map source (map (λt. t ⋅ σ) ss1 @ Var ?x # map (λt. t ⋅ σ) ss2)⟩⇩α) y = source ((ss2!?i) ⋅ σ)"
        by (smt (verit, ccfv_threshold) "3.hyps"(2) One_nat_def ab_semigroup_add_class.add_ac(1) comp_def distinct_remdups distinct_rev i(2) length_append length_map list.size(4) mk_subst_distinct) 
      moreover from i2 2 have "(⟨map source (ss1 @ Var ?x # ss2)⟩⇩α) y = source (ss2!?i)"
        by (metis (no_types, opaque_lifting) "3.hyps"(2) One_nat_def add.right_neutral add_Suc_right comp_apply distinct_remdups distinct_rev i(2) length_append length_map length_nth_simps(2) mk_subst_distinct)
      moreover have "ss2!?i ∈ wf_pterm R" 
        using 3(3) 2 ‹?i < length ss2›  by (metis UnCI nth_mem) 
      ultimately show ?thesis 
        using source_apply_subst by auto
    qed
  }
  then have "ctxt_of_pos_term ?p (lhs α ⋅ ⟨map source (map (λt. t ⋅ σ) ss1 @ Var ?x # map (λt. t ⋅ σ) ss2)⟩⇩α) = 
             ctxt_of_pos_term ?p (lhs α ⋅ ⟨map source (ss1 @ Var ?x # ss2)⟩⇩α ⋅ (source ∘ σ))"
    using ctxt_of_pos_term_at_var_subst[OF lin pos1 var_at_p] unfolding subst_subst by (smt (verit) subst_compose)
  then show ?case unfolding source_ctxt.simps actxt.simps Let_def 3 subst_compose_ctxt_compose_distrib length_map ctxt_of_pos_term_subst[OF pos, symmetric] 
    by presburger
qed simp

text‹Needs left-linearity to avoid multihole contexts.›
lemma source_ctxt_apply_term: 
  assumes "C ∈ wf_pterm_ctxt R"
  shows "source (C⟨A⟩) = (source_ctxt C)⟨source A⟩"
using assms proof(induct C)
  case (3 α ss1 ss2 C)
  from 3(1) left_lin have lin:"linear_term (lhs α)"
    using left_linear_trs_def by fastforce 
  from 3(2) have len:"length ss1 < length (vars_term_list (lhs α))"
    by (metis add_lessD1 less_add_one lin linear_term_var_vars_term_list)  
  have "(source_ctxt (Crule α ss1 C ss2))⟨source A⟩ = 
      lhs α ⋅ ⟨(map source ss1) @ (source_ctxt C)⟨source A⟩ # (map source ss2)⟩⇩α"
    unfolding source_ctxt.simps Let_def intp_actxt.simps source.simps ctxt_ctxt_compose
    using ctxt_apply_term_subst[OF lin len] lhs_subst_upd
    by (smt (verit) len length_map lin linear_term_var_vars_term_list list.simps(9) map_append) 
  with 3(5) show ?case by simp 
qed simp_all
end

lemma rewrite_tgt:
  assumes rstep:"(t,v) ∈ (rstep R)⇧*"
  shows "(target (C ⟨(to_pterm t) ⋅ σ⟩), target (C ⟨(to_pterm v) ⋅ σ⟩)) ∈ (rstep R)⇧*"
proof(induct C)
  case Hole
  then show ?case
    by (simp add: local.rstep rsteps_closed_subst target_empty_apply_subst to_pterm_empty) 
next
  case (Cfun f ss1 C ss2)
  then show ?case by (simp add: ctxt_closed_one ctxt_closed_rsteps)
next
  case (Crule α ss1 C ss2)
  {fix x assume "x ∈ vars_term (rhs α)"
    from Crule have "((⟨map target (ss1 @ C⟨to_pterm t ⋅ σ⟩ # ss2)⟩⇩α) x, (⟨map target (ss1 @ C⟨to_pterm v ⋅ σ⟩ # ss2)⟩⇩α) x) ∈ (rstep R)⇧*"
    proof(cases "x ∈ vars_term (lhs α)")
      case True
      then obtain i where "i < length (vars_distinct (lhs α))" "x = vars_distinct (lhs α)!i"
        by (metis in_set_idx set_vars_term_list vars_term_list_vars_distinct)
      then show ?thesis using Crule
        by (smt (z3) append_Cons_nth_not_middle length_append length_map length_nth_simps(2) lhs_subst_not_var_i lhs_subst_var_i map_nth_eq_conv nth_append_length rtrancl.simps) 
    next
      case False
      then show ?thesis
        by (simp add: mk_subst_not_mem)
    qed
  }
  then show ?case by (simp add: subst_rsteps_imp_rsteps)
qed

subsection‹Additional Results›

lemma length_args_well_Prule:
  assumes "Prule α As ∈ wf_pterm R" "Prule α Bs ∈ wf_pterm S"
  shows "length As = length Bs"
proof-
  from assms(1) have "length As = length (var_rule α)" using wf_pterm.simps by fastforce
  moreover from assms(2) have "length Bs = length (var_rule α)" using wf_pterm.simps by fastforce
  ultimately show ?thesis by simp
qed

lemma co_initial_Var:
  assumes "co_initial (Var x) B"
  shows "B = Var x ∨ (∃α b' y. B = Prule α b' ∧ lhs α = Var y)"
proof-
  {assume "B ≠ Var x"
    with assms obtain α b' where "B = Prule α b'"
      by (metis is_empty_step.elims(3) source.elims source_empty_step term.distinct(1))
    moreover with assms have "∃ y. lhs α = Var y"
      by (metis source.simps(1) source.simps(3) subst_apply_eq_Var) 
    ultimately have "(∃α b' y. B = Prule α b' ∧ lhs α = Var y)"
      by blast 
  }
  then show ?thesis
    by blast
qed

lemma source_poss:
  assumes p:"p ∈ poss (source (Pfun f As))" and iq:"i#q ∈ poss (Pfun f As)"
    and ctxt:"source_ctxt (ctxt_of_pos_term (i#q) (Pfun f As)) = ctxt_of_pos_term p (source (Pfun f As))"
  shows "∃p'. p = i#p' ∧ p' ∈ poss (source (As!i))"
proof-
  obtain p' where "hole_pos (source_ctxt (ctxt_of_pos_term (i#q) (Pfun f As))) = i#p'" 
                  "p' = hole_pos (source_ctxt (ctxt_of_pos_term q (As ! i)))"
    unfolding ctxt_of_pos_term.simps source_ctxt.simps take_map drop_map using iq by auto 
  with ctxt have "p = i#p'"
    by (metis hole_pos_ctxt_of_pos_term p) 
  with p show ?thesis
    by auto 
qed

lemma simple_pterm_match:
  assumes "source A = t ⋅ σ"
    and "linear_term t"
    and "A ⋅ τ1 = to_pterm t ⋅ τ2"
  shows "matches A (to_pterm t)" 
  using assms proof(induct t arbitrary: A)
  case (Var x)
  then show ?case
    using matches_iff by force
next
  case (Fun f ts)
  from Fun(2,4) show ?case proof(cases A)
    case (Pfun g As)
    with Fun(2) have f:"f = g" by simp
    from Fun(2) have l:"length ts = length As" 
      unfolding Pfun source.simps f eval_term.simps by (simp add: map_equality_iff) 
    {fix i assume i:"i < length ts" 
      with Fun(2) have "source (As ! i) = ts ! i ⋅ σ" 
        unfolding Pfun source.simps f eval_term.simps by (simp add: map_equality_iff)
      moreover from i Fun(4) have "As ! i ⋅ τ1 = to_pterm (ts ! i) ⋅ τ2" 
        unfolding Pfun f to_pterm.simps eval_term.simps using l map_nth_conv by fastforce 
      ultimately have "matches (As!i) (to_pterm (ts!i))" 
        using Fun(1)[of "ts!i" "As!i"] l i Fun(3) by force
      then have "∃σ. As!i = (to_pterm (ts!i)) ⋅ σ"
        by (metis matches_iff) 
    }note IH=this
    from Fun(3) have lin:"linear_term (to_pterm (Fun f ts))"
      using to_pterm_linear by blast 
    from linear_term_obtain_subst[OF lin[unfolded to_pterm.simps]] show ?thesis 
      unfolding Pfun f by (smt (verit, del_insts) IH l length_map matches_iff nth_map to_pterm.simps(2)) 
  qed simp_all
qed

subsection ‹Proof Terms Represent Multi-Steps›

context var_rhs_subset_lhs
begin
lemma mstep_to_pterm:
  assumes "(s, t) ∈ mstep R"
  shows "∃A. A ∈ wf_pterm R ∧ source A = s ∧ target A = t"
  using assms(1) proof(induct)
  case (Var x)
  then show ?case
    by (meson source.simps(1) target.simps(1) wf_pterm.intros(1))
next
  case (args f n ss ts)
  then have "∀i∈set [0..<n]. ∃a. a ∈ wf_pterm R ∧ source a = ss ! i ∧ target a = ts ! i"
    by simp 
  then obtain As where as:"length As = n ∧ (∀i < n. (As!i) ∈ wf_pterm R ∧ source (As!i) = ss ! i ∧ target (As!i) = ts ! i)"  
    using obtain_list_with_property[where P="λa i. a ∈ wf_pterm R ∧ source a = ss!i ∧ target a = ts!i" and xs="[0..<n]"]
    by (metis add.left_neutral diff_zero length_upt nth_upt set_upt)      
  with args(1) have "source (Pfun f As) = Fun f ss" 
    unfolding source.simps by (simp add: map_nth_eq_conv) 
  moreover from as args(2) have "target (Pfun f As) = Fun f ts" 
    unfolding target.simps by (simp add: map_nth_eq_conv) 
  ultimately show ?case 
    using as by (metis in_set_idx wf_pterm.intros(2))
next
  case (rule l r σ τ)
  let ?α ="(l → r)"
  have "set (vars_distinct l) = vars_term l"
    by simp
  with rule(2) obtain As where as:"length As = length (vars_distinct l) ∧ 
     (∀i < length (vars_distinct l). (As!i) ∈ wf_pterm R ∧ 
     source (As!i) = σ ((vars_distinct l) ! i) ∧ target (As!i) = τ ((vars_distinct l) ! i))"  
    using obtain_list_with_property[where P="λa x. a ∈ wf_pterm R ∧ source a = σ x ∧ target a = τ x"] by blast
  with rule(1) have well:"Prule ?α As ∈ wf_pterm R"
    by (metis in_set_idx prule.sel(1) prule.sel(2) wf_pterm.simps) 
  from as have "∀x ∈ vars_term l. (⟨map source As⟩⇩?α) x = σ x"
    by (smt (z3) apply_lhs_subst_var_rule in_set_idx length_map map_nth_conv prule.sel(1) set_vars_term_list vars_term_list_vars_distinct)
  then have s:"source (Prule ?α As) = l ⋅ σ"
    by (simp add: term_subst_eq_conv) 
  from as varcond have "∀x ∈ vars_term r. (⟨map target As⟩⇩?α) x = τ x"
    by (smt (verit, best) apply_lhs_subst_var_rule fst_conv in_set_conv_nth length_map nth_map prule.sel(1) 
        rule.hyps(1) set_vars_term_list snd_conv split_beta subsetD vars_term_list_vars_distinct) 
  then have "target (Prule ?α As) = r ⋅ τ" 
    by (simp add: term_subst_eq_conv) 
  with well s show ?case 
    by blast
qed
end

lemma pterm_to_mstep:
  assumes "A ∈ wf_pterm R"
  shows "(source A, target A) ∈ mstep R "
  using assms proof(induct)
  case (2 As f)
  then show ?case
    by (simp add: mstep.args)
next
  case (3 α As)
  then have "∀x∈vars_term (lhs α). ((⟨map source As⟩⇩α) x, (⟨map target As⟩⇩α) x) ∈ mstep R"
    by (smt (verit, best) apply_lhs_subst_var_rule comp_def in_set_idx length_map map_nth_conv nth_mem set_remdups set_rev set_vars_term_list) 
  with 3(1) show ?case
    by (simp add: mstep.rule)
qed simp

lemma co_init_prule: 
  assumes "co_initial (Prule α As) (Prule α Bs)"
    and "Prule α As ∈ wf_pterm R" and "Prule α Bs ∈ wf_pterm R"
  shows "∀i<length As. co_initial (As!i) (Bs!i)"
proof-
  from assms have l1:"length As = length (var_rule α)"
    using wf_pterm.simps by fastforce 
  from assms have l2:"length Bs = length (var_rule α)"
    using wf_pterm.simps by fastforce 
  {fix i assume i:"i < length As" and co:"¬ (co_initial (As!i) (Bs!i))"
    then have "(⟨map source As⟩⇩α) ((var_rule α)!i) ≠ (⟨map source Bs⟩⇩α) ((var_rule α)!i)"
      by (metis l1 l2 length_map lhs_subst_var_i nth_map) 
    with assms(1) have False unfolding source.simps
      by (smt (z3) comp_apply i l1 nth_mem set_remdups set_rev set_vars_term_list term_subst_eq_rev) 
  } then show ?thesis
    by blast 
qed

section‹Operations on Proof Terms›
text‹The operations residual, deletion, and join on proof terms all fulfill 
@{text "A ⋆ (source A) = A"} which implies several useful results.›

locale op_proof_term = left_lin_no_var_lhs +
  fixes f :: "(('a, 'b) prule + 'a, 'b) Term.term ⇒ (('a, 'b) prule + 'a, 'b) Term.term ⇒ (('a, 'b) prule + 'a, 'b) Term.term option"
  assumes f_src:" A ∈ wf_pterm R ⟹ f A (to_pterm (source A)) = Some A"
  and f_pfun:"f (Pfun g As)(Pfun g Bs) = (if length As = length Bs then
                                         (case those (map2 f As Bs) of
                                          Some xs ⇒ Some (Pfun g xs)
                                         | None ⇒ None) else None)"
  and f_prule:"f (Prule α As) (Pfun g Bs) = (case match (Pfun g Bs)  (to_pterm (lhs α)) of
                          None ⇒ None
                          | Some σ ⇒
                            (case those (map2 f As (map σ (var_rule α))) of
                              Some xs ⇒ Some (Prule α xs)
                          | None ⇒ None))"
begin

notation
  f  ("'(⋆')") and
  f  ("(_ ⋆ _)"  [51, 51] 50)

lemma apply_f_ctxt: 
  assumes "C ∈ wf_pterm_ctxt R"
    and "A ⋆ B = Some D"
  shows "C⟨A⟩ ⋆ (to_pterm_ctxt (source_ctxt C))⟨B⟩ = Some (C⟨D⟩)"
  using assms proof(induct C rule:pterm_ctxt_induct)
  case (Cfun f ss1 C ss2)
   have l:"length ((map (to_pterm ∘ source) ss1) @ (to_pterm_ctxt (source_ctxt C))⟨A⟩ # (map (to_pterm ∘ source) ss2))
          = length (ss1 @ C⟨B⟩ # ss2)" by auto
   from Cfun(2) have well1:"∀i < length ss1. (ss1!i) ∈ wf_pterm R" by auto
   from Cfun(2) have well2:"∀i < length ss2. (ss2!i) ∈ wf_pterm R" by auto
   from Cfun have fC:"C⟨A⟩ ⋆ (to_pterm_ctxt (source_ctxt C))⟨B⟩ = Some (C⟨D⟩)" 
     by auto
   from well1 have f1:"∀i < length ss1. ((map2 (⋆) ss1 (map (to_pterm ∘ source) ss1))!i = Some (ss1!i))"
     using f_src to_pterm_empty by fastforce 
   from well2 have f2:"∀i < length ss2. ((map2 (⋆) ss2 (map (to_pterm ∘ source) ss2))!i = Some (ss2!i))"
     using f_src to_pterm_empty by fastforce 
   {fix i assume i:"i < (length ss1) + (length ss2) +1"
     have "(map2 (⋆) (ss1 @ (C⟨A⟩ # ss2))  
           (map (to_pterm ∘ source) ss1 @ ((to_pterm_ctxt (source_ctxt C))⟨B⟩ # map (to_pterm ∘ source) ss2)))!i 
           = Some ((ss1 @ C⟨D⟩ # ss2)!i)"
     proof-
       consider "i < length ss1" | "i = length ss1" | "i > length ss1"
         using nat_neq_iff by blast 
       then show ?thesis proof(cases)
         case 1
         then show ?thesis using f1
           by (simp add: append_Cons_nth_left)
       next
         case 2
         then show ?thesis using fC 
           by (simp add: append_Cons_nth_middle)
       next
         case 3
         with i have l:"(map (to_pterm ∘ source) ss1 @ (to_pterm_ctxt (source_ctxt C))⟨B⟩ # map (to_pterm ∘ source) ss2)!i
                     = (map (to_pterm ∘ source) ss2)!(i-(length ss1 + 1))"
           by (metis add.commute length_map less_SucI not_less_eq nth_append_Cons plus_1_eq_Suc)
         from 3 i have r:"(ss1 @ (C⟨to_pterm (source B)⟩ # ss2))!i = ss2!(i-(length ss1 + 1))"
           by (metis add.commute less_SucI not_less_eq nth_append_Cons plus_1_eq_Suc) 
         from l r 3 show ?thesis using f2
           by (smt One_nat_def add.right_neutral add_Suc add_Suc_right add_diff_inverse_nat add_less_cancel_left append_Cons_nth_right i length_append length_map length_zip list.size(4) min_less_iff_conj not_less_eq nth_map nth_zip)
       qed
     qed
   }
   with l have "those ((map2 (⋆) (ss1 @ (C⟨A⟩ # ss2))  
              (map (to_pterm ∘ source) ss1 @ ((to_pterm_ctxt (source_ctxt C))⟨B⟩ # map (to_pterm ∘ source) ss2))))
            = Some (ss1 @ C⟨D⟩ # ss2)" by (simp add: those_some)
   with l show ?case using f_pfun by simp 
 next
   case (Crule α ss1 C ss2)
   from Crule(2) have alpha:"to_rule α ∈ R"
     using wf_pterm_ctxt.cases by auto 
   then have linear:"linear_term (lhs α)"
     using left_lin left_linear_trs_def by fastforce
   then have linear':"linear_term (to_pterm (lhs α))"
     using to_pterm_linear by blast
   have l1:"length ((map (to_pterm ∘ source) ss1) @ (to_pterm_ctxt (source_ctxt C))⟨A⟩ # (map (to_pterm ∘ source) ss2))
          = length (ss1 @ C⟨B⟩ # ss2)" by auto
   from Crule(2) have l2:"length (ss1 @ C⟨B⟩ # ss2) = length (var_rule α)"
     using wf_pterm_ctxt.simps by fastforce
   from Crule(2) have well1:"∀i < length ss1. (ss1!i) ∈ wf_pterm R" by auto
   from Crule(2) have well2:"∀i < length ss2. (ss2!i) ∈ wf_pterm R" by auto
   from Crule have fC:"C⟨A⟩ ⋆ (to_pterm_ctxt (source_ctxt C))⟨B⟩ = Some (C⟨D⟩)" 
     by auto
   from well1 have f1:"∀i < length ss1. ((map2 (⋆) ss1 (map (to_pterm ∘ source) ss1))!i = Some (ss1!i))"
     using f_src to_pterm_empty by fastforce 
   from well2 have f2:"∀i < length ss2. ((map2 (⋆) ss2 (map (to_pterm ∘ source) ss2))!i = Some (ss2!i))"
     using f_src to_pterm_empty by fastforce 
   {fix i assume i:"i < (length ss1) + (length ss2) +1"
     have "(map2 (⋆) (ss1 @ (C⟨A⟩ # ss2)) (map (to_pterm ∘ source) ss1 @ ((to_pterm_ctxt (source_ctxt C))⟨B⟩ # 
           (map (to_pterm ∘ source) ss2))) )!i = Some ((ss1 @ C⟨D⟩ # ss2)!i)"
     proof-
       consider "i < length ss1" | "i = length ss1" | "i > length ss1"
         using nat_neq_iff by blast 
       then show ?thesis proof(cases)
         case 1
         then show ?thesis using f1
           by (simp add: append_Cons_nth_left)
       next
         case 2
         then show ?thesis using fC
           by (simp add: append_Cons_nth_middle)
       next
         case 3
         with i have l:"(map (to_pterm ∘ source) ss1 @ (to_pterm_ctxt (source_ctxt C))⟨B⟩ # map (to_pterm ∘ source) ss2)!i
                     = (map (to_pterm ∘ source) ss2)!(i-(length ss1 + 1))"
           by (metis add.commute length_map less_SucI not_less_eq nth_append_Cons plus_1_eq_Suc)
         from 3 i have r:"(ss1 @ (C⟨to_pterm (source B)⟩ # ss2))!i = ss2!(i-(length ss1 + 1))"
           by (metis add.commute less_SucI not_less_eq nth_append_Cons plus_1_eq_Suc) 
         from l r 3 show ?thesis using f2
           by (smt One_nat_def add.right_neutral add_Suc add_Suc_right add_diff_inverse_nat add_less_cancel_left append_Cons_nth_right i length_append length_map length_zip list.size(4) min_less_iff_conj not_less_eq nth_map nth_zip)
       qed
     qed
   }
   with l1 have IH:"those (map2 (⋆) (ss1 @ (C⟨A⟩ # ss2)) (map (to_pterm ∘ source) ss1 @ ((to_pterm_ctxt (source_ctxt C))⟨B⟩ # 
                         (map (to_pterm ∘ source) ss2))) ) = Some (ss1 @ C⟨D⟩ # ss2)" by (simp add: those_some)
   let ?p = "(var_poss_list (lhs α) ! length ss1)"
   let ?x = "vars_term_list (lhs α) ! length ss1"
   let ?σ = "⟨map source (ss1 @ Var (vars_term_list (lhs α) ! length ss1) # ss2)⟩⇩α"
   from l2 linear have l3:"length ss1 < length (var_poss_list (lhs α))"
     by (metis (no_types, lifting) add_Suc_right append_Cons_nth_left le_imp_less_Suc length_append length_var_poss_list linear_term_var_vars_term_list linorder_neqE_nat list.size(3) list.size(4) not_add_less1 nth_equalityI self_append_conv zero_order(1))
   then have "?p ∈ poss (lhs α)"
     using nth_mem var_poss_imp_poss var_poss_list_sound by blast
   then have ctxt:"(to_pterm_ctxt (source_ctxt (Crule α ss1 C ss2)))⟨B⟩ =
      (ctxt_of_pos_term ?p (to_pterm (lhs α) ⋅ (to_pterm ∘ ?σ)))⟨(to_pterm_ctxt (source_ctxt C))⟨B⟩⟩"
     unfolding source_ctxt.simps intp_actxt.simps Let_def ctxt_ctxt_compose to_pterm_ctxt_comp 
     using to_pterm_ctxt_at_pos[where ?p="?p" and ?s="lhs α ⋅ ?σ"] by (simp add: to_pterm_subst)
   from l3 have l4:"length ss1 < length (vars_term_list (to_pterm (lhs α)))"
     by (metis length_var_poss_list vars_to_pterm) 
   have "(to_pterm_ctxt (source_ctxt (Crule α ss1 C ss2)))⟨B⟩ = 
               to_pterm (lhs α) ⋅ ((to_pterm ∘ ?σ)(?x := (to_pterm_ctxt (source_ctxt C))⟨B⟩))"
     unfolding ctxt using ctxt_apply_term_subst[where ?p="?p" and ?t="to_pterm (lhs α)" and ?i="length ss1" and ?s="(to_pterm_ctxt (source_ctxt C))⟨B⟩" and ?σ="(to_pterm ∘ ?σ)"]
       linear' l4  var_poss_list_to_pterm vars_to_pterm by metis 
   then obtain τ where τ:"match (to_pterm_ctxt (source_ctxt (Crule α ss1 C ss2)))⟨B⟩ (to_pterm (lhs α)) = Some τ" 
     unfolding ctxt using ctxt_apply_term_subst linear' match_complete' option.distinct(1) by force 
   have varr:"(var_rule α) = vars_term_list (to_pterm (lhs α))" 
     using linear linear_term_var_vars_term_list unfolding vars_to_pterm by force
   have "(map (to_pterm ∘ ?σ) (vars_term_list (to_pterm (lhs α)))) = map (to_pterm ∘ source) (ss1 @ Var (vars_term_list (lhs α) ! length ss1) # ss2)"
     using apply_lhs_subst_var_rule l2 unfolding varr[symmetric] by force
   then have "(map (to_pterm ∘ ?σ) (vars_term_list (to_pterm (lhs α))))[length ss1 := (to_pterm_ctxt (source_ctxt C))⟨B⟩] = 
              (map (to_pterm ∘ source) ss1 @ (to_pterm_ctxt (source_ctxt C))⟨B⟩ # (map (to_pterm ∘ source) ss2))"
     by (metis (no_types, lifting) length_map list.simps(9) list_update_length map_append) 
   with τ have map_tau:"map τ (var_rule α) = (map (to_pterm ∘ source) ss1 @ (to_pterm_ctxt (source_ctxt C))⟨B⟩ #
                                   (map (to_pterm ∘ source) ss2))"  
     using match_lhs_context[where ?t="to_pterm (lhs α)" and ?τ=τ and ?σ="(to_pterm ∘ ?σ)"] 
       l4 var_poss_list_to_pterm linear' ctxt varr by metis
   from alpha no_var_lhs obtain f ts where f:"lhs α = Fun f ts"
     by blast
   have "[] ∉ var_poss (lhs α)" 
     unfolding f var_poss.simps by force 
   then obtain i q where iq:"?p = i # q" using l3
     by (metis in_set_conv_nth subt_at.elims var_poss_list_sound)
   then obtain ts' where root_not_rule:"(to_pterm_ctxt (source_ctxt (Crule α ss1 C ss2)))⟨B⟩ = Pfun f ts'"
     unfolding ctxt iq unfolding f by simp
   then show ?case 
     using τ f_prule map_tau IH by force
 qed simp

end

end