Theory Typing_Result

(*  Title:      Typing_Result.thy
    Author:     Andreas Viktor Hess, DTU
    SPDX-License-Identifier: BSD-3-Clause
*)

section ‹The Typing Result›

theory Typing_Result
imports Typed_Model
begin

subsection ‹Locale Setup›
locale typing_result = typed_model arity public Ana Γ
  for arity::"'fun ⇒ nat"
    and public::"'fun ⇒ bool"
    and Ana::"('fun,'var) term ⇒ (('fun,'var) term list × ('fun,'var) term list)"
    and Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
  +
  assumes infinite_typed_consts: "⋀a. infinite {c. Γ (Fun c []) = TAtom a ∧ public c}"
    and no_private_funs[simp]: "⋀f. arity f > 0 ⟹ public f"
begin

subsubsection ‹Minor Lemmata›

lemma fun_type_inv': assumes "Γ t = TComp f T" shows "arity f > 0" "public f"
using assms fun_type_inv by simp_all

lemma infinite_public_consts[simp]: "infinite {c. public c ∧ arity c = 0}"
proof -
  fix a::'atom
  define A where "A ≡ {c. Γ (Fun c []) = TAtom a ∧ public c}"
  define B where "B ≡ {c. public c ∧ arity c = 0}"

  have "arity c = 0" when c: "c ∈ A" for c
    using c const_type_inv unfolding A_def by blast
  hence "A ⊆ B" unfolding A_def B_def by blast
  hence "infinite B"
    using infinite_typed_consts[of a, unfolded A_def[symmetric]]
    by (metis infinite_super)
  thus ?thesis unfolding B_def by blast
qed

lemma infinite_fun_syms[simp]:
  "infinite {c. public c ∧ arity c > 0} ⟹ infinite Σf"
  "infinite 𝒞" "infinite 𝒞pub" "infinite (UNIV::'fun set)"
by (metis Σf_unfold finite_Collect_conjI,
    metis infinite_public_consts finite_Collect_conjI,
    use infinite_public_consts 𝒞pub_unfold in ‹force simp add: Collect_conj_eq›,
    metis UNIV_I finite_subset subsetI infinite_public_consts(1))

lemma id_univ_proper_subset[simp]: "Σf ⊂ UNIV" "(∃f. arity f > 0) ⟹ 𝒞 ⊂ UNIV"
by (metis finite.emptyI inf_top.right_neutral top.not_eq_extremum disjoint_fun_syms
          infinite_fun_syms(2) inf_commute)
   (metis top.not_eq_extremum UNIV_I const_arity_eq_zero less_irrefl)

lemma exists_fun_notin_funs_term: "∃f::'fun. f ∉ funs_term t"
by (metis UNIV_eq_I finite_fun_symbols infinite_fun_syms(4))

lemma exists_fun_notin_funs_terms:
  assumes "finite M" shows "∃f::'fun. f ∉ ⋃(funs_term ` M)"
by (metis assms finite_fun_symbols infinite_fun_syms(4) ex_new_if_finite finite_UN)

lemma exists_notin_funsst: "∃f. f ∉ funsst (S::('fun,'var) strand)"
by (metis UNIV_eq_I finite_funsst infinite_fun_syms(4))

lemma infinite_typed_consts': "infinite {c. Γ (Fun c []) = TAtom a ∧ public c ∧ arity c = 0}"
proof -
  { fix c assume "Γ (Fun c []) = TAtom a" "public c"
    hence "arity c = 0" using const_type[of c] fun_type[of c "[]"] by auto
  } hence "{c. Γ (Fun c []) = TAtom a ∧ public c ∧ arity c = 0} =
           {c. Γ (Fun c []) = TAtom a ∧ public c}"
    by auto
  thus "infinite {c. Γ (Fun c []) = TAtom a ∧ public c ∧ arity c = 0}"
    using infinite_typed_consts[of a] by metis
qed

lemma atypes_inhabited: "∃c. Γ (Fun c []) = TAtom a ∧ wftrm (Fun c []) ∧ public c ∧ arity c = 0"
proof -
  obtain c where "Γ (Fun c []) = TAtom a" "public c" "arity c = 0"
    using infinite_typed_consts'(1)[of a] not_finite_existsD by blast
  thus ?thesis using const_type_inv[OF ‹Γ (Fun c []) = TAtom a›] unfolding wftrm_def by auto
qed

lemma atype_ground_term_ex: "∃t. fv t = {} ∧ Γ t = TAtom a ∧ wftrm t"
using atypes_inhabited[of a] by force

lemma type_ground_inhabited: "∃t'. fv t' = {} ∧ Γ t = Γ t'"
proof -
  { fix τ::"('fun, 'atom) term_type" assume "⋀f T. Fun f T ⊑ τ ⟹ 0 < arity f"
    hence "∃t'. fv t' = {} ∧ τ = Γ t'"
    proof (induction τ)
      case (Fun f T)
      hence "arity f > 0" by auto
    
      from Fun.IH Fun.prems(1) have "∃Y. map Γ Y = T ∧ (∀x ∈ set Y. fv x = {})"
      proof (induction T)
        case (Cons x X)
        hence "⋀g Y. Fun g Y ⊑ Fun f X ⟹ 0 < arity g" by auto
        hence "∃Y. map Γ Y = X ∧ (∀x∈set Y. fv x = {})" using Cons by auto
        moreover have "∃t'. fv t' = {} ∧ x = Γ t'" using Cons by auto
        ultimately obtain y Y where
            "fv y = {}" "Γ y = x" "map Γ Y = X" "∀x∈set Y. fv x = {}" 
          using Cons by moura
        hence "map Γ (y#Y) = x#X ∧ (∀x∈set (y#Y). fv x = {})" by auto
        thus ?case by meson 
      qed simp
      then obtain Y where "map Γ Y = T" "∀x ∈ set Y. fv x = {}" by metis
      hence "fv (Fun f Y) = {}" "Γ (Fun f Y) = TComp f T" using fun_type[OF ‹arity f > 0›] by auto
      thus ?case by (metis exI[of "λt. fv t = {} ∧ Γ t = TComp f T" "Fun f Y"])
    qed (metis atype_ground_term_ex)
  }
  thus ?thesis by (metis Γ_wf'')
qed

lemma type_wfttype_inhabited:
  assumes "⋀f T. Fun f T ⊑ τ ⟹ 0 < arity f" "wftrm τ"
  shows "∃t. Γ t = τ ∧ wftrm t"
using assms
proof (induction τ)
  case (Fun f Y)
  have IH: "∃t. Γ t = y ∧ wftrm t" when y: "y ∈ set Y " for y
  proof -
    have "wftrm y"
      using Fun y unfolding wftrm_def
      by (metis Fun_param_is_subterm term.le_less_trans) 
    moreover have "Fun g Z ⊑ y ⟹ 0 < arity g" for g Z
      using Fun y by auto
    ultimately show ?thesis using Fun.IH[OF y] by auto
  qed

  from Fun have "arity f = length Y" "arity f > 0" unfolding wftrm_def by force+
  moreover from IH have "∃X. map Γ X = Y ∧ (∀x ∈ set X. wftrm x)"
    by (induct Y, simp_all, metis list.simps(9) set_ConsD)
  ultimately show ?case by (metis fun_type length_map wf_trmI)
qed (use atypes_inhabited wftrm_def in blast)

lemma type_pgwt_inhabited: "wftrm t ⟹ ∃t'. Γ t = Γ t' ∧ public_ground_wf_term t'"
proof -
  assume "wftrm t"
  { fix τ assume "Γ t = τ"
    hence "∃t'. Γ t = Γ t' ∧ public_ground_wf_term t'" using ‹wftrm t›
    proof (induction τ arbitrary: t)
      case (Var a t)
      then obtain c where "Γ t = Γ (Fun c [])" "arity c = 0" "public c"
        using const_type_inv[of _ "[]" a] infinite_typed_consts(1)[of a]  not_finite_existsD
        by force
      thus ?case using PGWT[OF ‹public c›, of "[]"] by auto
    next
      case (Fun f Y t)
      have *: "arity f > 0" "public f" "arity f = length Y"
        using fun_type_inv[OF ‹Γ t = TComp f Y›] fun_type_inv_wf[OF ‹Γ t = TComp f Y› ‹wftrm t›]
        by auto
      have "⋀y. y ∈ set Y ⟹ ∃t'. y = Γ t' ∧ public_ground_wf_term t'"
        using Fun.prems(1) Fun.IH Γ_wf''[of _ _ t] Γ_wf'[OF ‹wftrm t›] type_wfttype_inhabited
        by (metis Fun_param_is_subterm term.order_trans wf_trm_subtermeq) 
      hence "∃X. map Γ X = Y ∧ (∀x ∈ set X. public_ground_wf_term x)"
        by (induct Y, simp_all, metis list.simps(9) set_ConsD)
      then obtain X where X: "map Γ X = Y" "⋀x. x ∈ set X ⟹ public_ground_wf_term x" by moura
      hence "arity f = length X" using *(3) by auto
      have "Γ t = Γ (Fun f X)" "public_ground_wf_term (Fun f X)"
        using fun_type[OF *(1), of X] Fun.prems(1) X(1) apply simp
        using PGWT[OF *(2) ‹arity f = length X› X(2)] by metis
      thus ?case by metis
    qed
  }
  thus ?thesis using ‹wftrm t› by auto
qed

end

subsection ‹The Typing Result for the Composition-Only Intruder›
context typing_result
begin

subsubsection ‹Well-typedness and Type-Flaw Resistance Preservation›
context
begin

private lemma LI_preserves_tfr_stp_all_single:
  assumes "(S,θ) ↝ (S',θ')" "wfconstr S θ" "wtsubst θ"
  and "list_all tfrstp S" "tfrset (trmsst S)" "wftrms (trmsst S)"
  shows "list_all tfrstp S'"
using assms
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' θ)
  hence "list_all tfrstp S" "list_all tfrstp S'" by simp_all
  moreover have "list_all tfrstp (map Send1 X)" by (induct X) auto
  ultimately show ?case by simp
next
  case (Unify S f Y δ X S' θ)
  hence "list_all tfrstp (S@S')" by simp

  have "fvst (S@Send1 (Fun f X)#S') ∩ bvarsst (S@S') = {}"
    using Unify.prems(1) by (auto simp add: wfconstr_def)
  moreover have "fv (Fun f X) ⊆ fvst (S@Send1 (Fun f X)#S')" by auto
  moreover have "fv (Fun f Y) ⊆ fvst (S@Send1 (Fun f X)#S')"
    using Unify.hyps(2) fv_subset_if_in_strand_ik'[of "Fun f Y" S] by force
  ultimately have bvars_disj:
      "bvarsst (S@S') ∩ fv (Fun f X) = {}" "bvarsst (S@S') ∩ fv (Fun f Y) = {}"
    by blast+

  have "wftrm (Fun f X)" using Unify.prems(5) by simp
  moreover have "wftrm (Fun f Y)"
  proof -
    obtain x where "x ∈ set S" "Fun f Y ∈ subtermsset (trmsstp x)" "wftrms (trmsstp x)"
      using Unify.hyps(2) Unify.prems(5) by force+
    thus ?thesis using wf_trm_subterm by auto
  qed
  moreover have
      "Fun f X ∈ SMP (trmsst (S@Send1 (Fun f X)#S'))"
      "Fun f Y ∈ SMP (trmsst (S@Send1 (Fun f X)#S'))"
    using SMP_append[of S "Send1 (Fun f X)#S'"] SMP_Cons[of "Send1 (Fun f X)" S']
          SMP_ikI[OF Unify.hyps(2)]
    by auto
  hence "Γ (Fun f X) = Γ (Fun f Y)"
    using Unify.prems(4) mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]
    unfolding tfrset_def by blast
  ultimately have "wtsubst δ" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis
  moreover have "wftrms (subst_range δ)"
    using mgu_wf_trm[OF Unify.hyps(3)[symmetric] ‹wftrm (Fun f X)› ‹wftrm (Fun f Y)›]
    by (metis wf_trm_subst_range_iff)
  moreover have "bvarsst (S@S') ∩ range_vars δ = {}"
    using mgu_vars_bounded[OF Unify.hyps(3)[symmetric]] bvars_disj by fast
  ultimately show ?case using tfr_stp_all_wt_subst_apply[OF ‹list_all tfrstp (S@S')›] by metis
next
  case (Equality S δ t t' a S' θ)
  have "list_all tfrstp (S@S')" "Γ t = Γ t'"
    using tfr_stp_all_same_type[of S a t t' S']
          tfr_stp_all_split(5)[of S _ S']
          MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
          Equality.prems(3)
    by blast+
  moreover have "wftrm t" "wftrm t'" using Equality.prems(5) by auto
  ultimately have "wtsubst δ"
    using mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric]]
    by metis
  moreover have "wftrms (subst_range δ)"
    using mgu_wf_trm[OF Equality.hyps(2)[symmetric] ‹wftrm t› ‹wftrm t'›]
    by (metis wf_trm_subst_range_iff)
  moreover have "fvst (S@Equality a t t'#S') ∩ bvarsst (S@Equality a t t'#S') = {}"
    using Equality.prems(1) by (auto simp add: wfconstr_def)
  hence "bvarsst (S@S') ∩ fv t = {}" "bvarsst (S@S') ∩ fv t' = {}" by auto
  hence "bvarsst (S@S') ∩ range_vars δ = {}"
    using mgu_vars_bounded[OF Equality.hyps(2)[symmetric]] by fast
  ultimately show ?case using tfr_stp_all_wt_subst_apply[OF ‹list_all tfrstp (S@S')›] by metis
qed

private lemma LI_in_SMP_subset_single:
  assumes "(S,θ) ↝ (S',θ')" "wfconstr S θ" "wtsubst θ"
          "tfrset (trmsst S)" "wftrms (trmsst S)" "list_all tfrstp S"
  and "trmsst S ⊆ SMP M"
  shows "trmsst S' ⊆ SMP M"
using assms
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' θ)
  hence "SMP (trmsst [Send1 (Fun f X)]) ⊆ SMP M"
  proof -
    have "SMP (trmsst [Send1 (Fun f X)]) ⊆ SMP (trmsst (S@Send1 (Fun f X)#S'))"
      using trmsst_append SMP_mono by auto
    thus ?thesis
      using SMP_union[of "trmsst (S@Send1 (Fun f X)#S')" M]
            SMP_subset_union_eq[OF Compose.prems(6)]
      by auto
  qed
  thus ?case using Compose.prems(6) by auto
next
  case (Unify S f Y δ X S' θ)
  have "Fun f X ∈ SMP (trmsst (S@Send1 (Fun f X)#S'))" by auto
  moreover have "MGU δ (Fun f X) (Fun f Y)"
    by (metis mgu_gives_MGU[OF Unify.hyps(3)[symmetric]])
  moreover have
        "⋀x. x ∈ set S ⟹ wftrms (trmsstp x)" "wftrm (Fun f X)"
    using Unify.prems(4) by force+
  moreover have "Fun f Y ∈ SMP (trmsst (S@Send1 (Fun f X)#S'))"
    by (meson SMP_ikI Unify.hyps(2) contra_subsetD ik_append_subset(1))
  ultimately have "wftrm (Fun f Y)" "Γ (Fun f X) = Γ (Fun f Y)"
    using ikst_subterm_exD[OF ‹Fun f Y ∈ ikst S›] ‹tfrset (trmsst (S@Send1 (Fun f X)#S'))›
    unfolding tfrset_def by (metis (full_types) SMP_wf_trm Unify.prems(4), blast)
  hence "wtsubst δ" by (metis mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric] ‹wftrm (Fun f X)›])
  moreover have "wftrms (subst_range δ)"
    using mgu_wf_trm[OF Unify.hyps(3)[symmetric] ‹wftrm (Fun f X)› ‹wftrm (Fun f Y)›] by simp
  ultimately have "trmsst ((S@Send1 (Fun f X)#S') ⋅st δ) ⊆ SMP M"
    using SMP.Substitution Unify.prems(6) wt_subst_SMP_subset by metis
  thus ?case by auto
next
  case (Equality S δ t t' a S' θ)
  hence "Γ t = Γ t'"
    using tfr_stp_all_same_type MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
    by metis
  moreover have "t ∈ SMP (trmsst (S@Equality a t t'#S'))" "t' ∈ SMP (trmsst (S@Equality a t t'#S'))"
    using Equality.prems(1) by auto
  moreover have "MGU δ t t'" using mgu_gives_MGU[OF Equality.hyps(2)[symmetric]] by metis
  moreover have "⋀x. x ∈ set S ⟹ wftrms (trmsstp x)" "wftrm t" "wftrm t'"
    using Equality.prems(4) by force+
  ultimately have "wtsubst δ" by (metis mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric] ‹wftrm t›])
  moreover have "wftrms (subst_range δ)"
    using mgu_wf_trm[OF Equality.hyps(2)[symmetric] ‹wftrm t› ‹wftrm t'›] by simp
  ultimately have "trmsst ((S@Equality a t t'#S') ⋅st δ) ⊆ SMP M"
    using SMP.Substitution Equality.prems wt_subst_SMP_subset by metis
  thus ?case by auto
qed

private lemma LI_preserves_tfr_single:
  assumes "(S,θ) ↝ (S',θ')" "wfconstr S θ" "wtsubst θ" "wftrms (subst_range θ)"
          "tfrset (trmsst S)" "wftrms (trmsst S)"
          "list_all tfrstp S"
  shows "tfrset (trmsst S') ∧ wftrms (trmsst S')"
using assms
proof (induction rule: LI_rel.induct)
  case (Compose S X f S' θ)
  let ?SMPmap = "SMP (trmsst (S@map Send1 X@S')) - (Var`𝒱)"
  have "?SMPmap ⊆ SMP (trmsst (S@Send1 (Fun f X)#S')) - (Var`𝒱)"
    using SMP_fun_map_snd_subset[of X f]
          SMP_append[of "map Send1 X" S'] SMP_Cons[of "Send1 (Fun f X)" S']
          SMP_append[of S "Send1 (Fun f X)#S'"] SMP_append[of S "map Send1 X@S'"]
    by auto
  hence "∀s ∈ ?SMPmap. ∀t ∈ ?SMPmap. (∃δ. Unifier δ s t) ⟶ Γ s = Γ t"
    using Compose unfolding tfrset_def by (meson subsetCE)
  thus ?case
    using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Compose[OF Compose.hyps]], of S']
          Compose.prems(5)
    unfolding tfrset_def by blast
next
  case (Unify S f Y δ X S' θ)
  let ?SMPδ = "SMP (trmsst (S@S' ⋅st δ)) - (Var`𝒱)"

  have "SMP (trmsst (S@S' ⋅st δ)) ⊆ SMP (trmsst (S@Send1 (Fun f X)#S'))"
  proof
    fix s assume "s ∈ SMP (trmsst (S@S' ⋅st δ))" thus "s ∈ SMP (trmsst (S@Send1 (Fun f X)#S'))"
      using LI_in_SMP_subset_single[
              OF LI_rel.Unify[OF Unify.hyps] Unify.prems(1,2,4,5,6)
                 MP_subset_SMP(2)[of "S@Send1 (Fun f X)#S'"]]
      by (metis SMP_union SMP_subset_union_eq Un_iff)
  qed
  hence "∀s ∈ ?SMPδ. ∀t ∈ ?SMPδ. (∃δ. Unifier δ s t) ⟶ Γ s = Γ t"
    using Unify.prems(4) unfolding tfrset_def by (meson Diff_iff subsetCE)
  thus ?case
    using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Unify[OF Unify.hyps]], of S']
          Unify.prems(5)
    unfolding tfrset_def by blast
next
  case (Equality S δ t t' a S' θ)
  let ?SMPδ = "SMP (trmsst (S@S' ⋅st δ)) - (Var`𝒱)"

  have "SMP (trmsst (S@S' ⋅st δ)) ⊆ SMP (trmsst (S@Equality a t t'#S'))"
  proof
    fix s assume "s ∈ SMP (trmsst (S@S' ⋅st δ))" thus "s ∈ SMP (trmsst (S@Equality a t t'#S'))"
      using LI_in_SMP_subset_single[
              OF LI_rel.Equality[OF Equality.hyps] Equality.prems(1,2,4,5,6)
                 MP_subset_SMP(2)[of "S@Equality a t t'#S'"]]
      by (metis SMP_union SMP_subset_union_eq Un_iff)
  qed
  hence "∀s ∈ ?SMPδ. ∀t ∈ ?SMPδ. (∃δ. Unifier δ s t) ⟶ Γ s = Γ t"
    using Equality.prems unfolding tfrset_def by (meson Diff_iff subsetCE)
  thus ?case
    using LI_preserves_trm_wf[OF r_into_rtrancl[OF LI_rel.Equality[OF Equality.hyps]], of _ S']
          Equality.prems
    unfolding tfrset_def by blast
qed

private lemma LI_preserves_welltypedness_single:
  assumes "(S,θ) ↝ (S',θ')" "wfconstr S θ" "wtsubst θ" "wftrms (subst_range θ)"
  and "tfrset (trmsst S)" "wftrms (trmsst S)" "list_all tfrstp S"
  shows "wtsubst θ' ∧ wftrms (subst_range θ')"
using assms
proof (induction rule: LI_rel.induct)
  case (Unify S f Y δ X S' θ)
  have "wftrm (Fun f X)" using Unify.prems(5) unfolding tfrset_def by simp
  moreover have "wftrm (Fun f Y)"
  proof -
    obtain x where "x ∈ set S" "Fun f Y ∈ subtermsset (trmsstp x)" "wftrms (trmsstp x)"
      using Unify.hyps(2) Unify.prems(5) unfolding tfrset_def by force
    thus ?thesis using wf_trm_subterm by auto
  qed
  moreover have
      "Fun f X ∈ SMP (trmsst (S@Send1 (Fun f X)#S'))" "Fun f Y ∈ SMP (trmsst (S@Send1 (Fun f X)#S'))"
    using SMP_append[of S "Send1 (Fun f X)#S'"] SMP_Cons[of "Send1 (Fun f X)" S']
          SMP_ikI[OF Unify.hyps(2)]
    by auto
  hence "Γ (Fun f X) = Γ (Fun f Y)"
    using Unify.prems(4) mgu_gives_MGU[OF Unify.hyps(3)[symmetric]]
    unfolding tfrset_def by blast
  ultimately have "wtsubst δ" using mgu_wt_if_same_type[OF Unify.hyps(3)[symmetric]] by metis

  have "wftrms (subst_range δ)"
    by (meson mgu_wf_trm[OF Unify.hyps(3)[symmetric] ‹wftrm (Fun f X)› ‹wftrm (Fun f Y)›]
              wf_trm_subst_range_iff)
  hence "wftrms (subst_range (θ ∘s δ))"
    using wf_trm_subst_range_iff wf_trm_subst ‹wftrms (subst_range θ)›
    unfolding subst_compose_def
    by (metis (no_types, lifting))
  thus ?case by (metis wt_subst_compose[OF ‹wtsubst θ› ‹wtsubst δ›])
next
  case (Equality S δ t t' a S' θ)
  have "wftrm t" "wftrm t'" using Equality.prems(5) by simp_all
  moreover have "Γ t = Γ t'"
    using ‹list_all tfrstp (S@Equality a t t'#S')›
          MGU_is_Unifier[OF mgu_gives_MGU[OF Equality.hyps(2)[symmetric]]]
    by auto
  ultimately have "wtsubst δ" using mgu_wt_if_same_type[OF Equality.hyps(2)[symmetric]] by metis

  have "wftrms (subst_range δ)"
    by (meson mgu_wf_trm[OF Equality.hyps(2)[symmetric] ‹wftrm t› ‹wftrm t'›] wf_trm_subst_range_iff)
  hence "wftrms (subst_range (θ ∘s δ))"
    using wf_trm_subst_range_iff wf_trm_subst ‹wftrms (subst_range θ)›
    unfolding subst_compose_def
    by (metis (no_types, lifting))
  thus ?case by (metis wt_subst_compose[OF ‹wtsubst θ› ‹wtsubst δ›])
qed metis

lemma LI_preserves_welltypedness:
  assumes "(S,θ) ↝* (S',θ')" "wfconstr S θ" "wtsubst θ" "wftrms (subst_range θ)"
    and "tfrset (trmsst S)" "wftrms (trmsst S)" "list_all tfrstp S"
  shows "wtsubst θ'" (is "?A θ'")
    and "wftrms (subst_range θ')" (is "?B θ'")
proof -
  have "?A θ' ∧ ?B θ'" using assms
  proof (induction S θ rule: converse_rtrancl_induct2)
    case (step S1 θ1 S2 θ2)
    hence "?A θ2 ∧ ?B θ2" using LI_preserves_welltypedness_single by presburger
    moreover have "wfconstr S2 θ2"
      by (fact LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] step.prems(1)])
    moreover have "tfrset (trmsst S2)" "wftrms (trmsst S2)"
      using LI_preserves_tfr_single[OF step.hyps(1)] step.prems by presburger+
    moreover have "list_all tfrstp S2"
      using LI_preserves_tfr_stp_all_single[OF step.hyps(1)] step.prems by fastforce
    ultimately show ?case using step.IH by presburger
  qed simp
  thus "?A θ'" "?B θ'" by simp_all
qed

lemma LI_preserves_tfr:
  assumes "(S,θ) ↝* (S',θ')" "wfconstr S θ" "wtsubst θ" "wftrms (subst_range θ)"
    and "tfrset (trmsst S)" "wftrms (trmsst S)" "list_all tfrstp S"
  shows "tfrset (trmsst S')" (is "?A S'")
    and "wftrms (trmsst S')" (is "?B S'")
    and "list_all tfrstp S'" (is "?C S'")
proof -
  have "?A S' ∧ ?B S' ∧ ?C S'" using assms
  proof (induction S θ rule: converse_rtrancl_induct2)
    case (step S1 θ1 S2 θ2)
    have "wfconstr S2 θ2" "tfrset (trmsst S2)" "wftrms (trmsst S2)" "list_all tfrstp S2"
      using LI_preserves_wellformedness[OF r_into_rtrancl[OF step.hyps(1)] step.prems(1)]
            LI_preserves_tfr_single[OF step.hyps(1) step.prems(1,2)]
            LI_preserves_tfr_stp_all_single[OF step.hyps(1) step.prems(1,2)]
            step.prems(3,4,5,6)
      by metis+
    moreover have "wtsubst θ2" "wftrms (subst_range θ2)"
      using LI_preserves_welltypedness[OF r_into_rtrancl[OF step.hyps(1)] step.prems]
      by simp_all
    ultimately show ?case using step.IH by presburger
  qed blast
  thus "?A S'" "?B S'" "?C S'" by simp_all
qed

lemma LI_preproc_preserves_tfr:
  assumes "tfrst S"
  shows "tfrst (LI_preproc S)"
unfolding tfrst_def
proof
  have S: "tfrset (trmsst S)" "list_all tfrstp S" using assms unfolding tfrst_def by metis+

  show "tfrset (trmsst (LI_preproc S))" by (metis S(1) LI_preproc_trms_eq)

  show "list_all tfrstp (LI_preproc S)" using S(2)
  proof (induction S)
    case (Cons x S)
    have IH: "list_all tfrstp (LI_preproc S)" using Cons by simp
    have x: "tfrstp x" using Cons.prems by simp

    show ?case using x IH unfolding list_all_iff by (cases x) auto
  qed simp
qed
end

subsubsection ‹Simple Constraints are Well-typed Satisfiable›
text ‹Proving the existence of a well-typed interpretation›
context
begin

lemma wt_interpretation_exists: 
  obtains ℐ::"('fun,'var) subst"
  where "interpretationsubst ℐ" "wtsubst ℐ" "subst_range ℐ ⊆ public_ground_wf_terms"
proof
  define ℐ where "ℐ = (λx. (SOME t. Γ (Var x) = Γ t ∧ public_ground_wf_term t))"

  { fix x t assume "ℐ x = t"
    hence "Γ (Var x) = Γ t ∧ public_ground_wf_term t"
      using someI_ex[of "λt. Γ (Var x) = Γ t ∧ public_ground_wf_term t",
                     OF type_pgwt_inhabited[of "Var x"]]
      unfolding ℐ_def wftrm_def by simp
  } hence props: "ℐ v = t ⟹ Γ (Var v) = Γ t ∧ public_ground_wf_term t" for v t by metis

  have "ℐ v ≠ Var v" for v using props pgwt_ground by fastforce
  hence "subst_domain ℐ = UNIV" by auto
  moreover have "ground (subst_range ℐ)" by (simp add: props pgwt_ground)
  ultimately show "interpretationsubst ℐ" by metis
  show "wtsubst ℐ" unfolding wtsubst_def using props by simp
  show "subst_range ℐ ⊆ public_ground_wf_terms" by (auto simp add: props)
qed

lemma wt_grounding_subst_exists:
  "∃θ. wtsubst θ ∧ wftrms (subst_range θ) ∧ fv (t ⋅ θ) = {}"
proof -
  obtain θ where θ: "interpretationsubst θ" "wtsubst θ" "subst_range θ ⊆ public_ground_wf_terms"
    using wt_interpretation_exists by blast
  show ?thesis using pgwt_wellformed interpretation_grounds[OF θ(1)] θ(2,3) by blast
qed

private fun fresh_pgwt::"'fun set ⇒ ('fun,'atom) term_type ⇒ ('fun,'var) term"  where
  "fresh_pgwt S (TAtom a) =
    Fun (SOME c. c ∉ S ∧ Γ (Fun c []) = TAtom a ∧ public c) []"
| "fresh_pgwt S (TComp f T) = Fun f (map (fresh_pgwt S) T)"

private lemma fresh_pgwt_same_type:
  assumes "finite S" "wftrm t"
  shows "Γ (fresh_pgwt S (Γ t)) = Γ t"
proof -
  let ?P = "λτ::('fun,'atom) term_type. wftrm τ ∧ (∀f T. TComp f T ⊑ τ ⟶ 0 < arity f)"
  { fix τ assume "?P τ" hence "Γ (fresh_pgwt S τ) = τ"
    proof (induction τ)
      case (Var a)
      let ?P = "λc. c ∉ S ∧ Γ (Fun c []) = Var a ∧ public c"
      let ?Q = "λc. Γ (Fun c []) = Var a ∧ public c"
      have " {c. ?Q c} - S = {c. ?P c}" by auto
      hence "infinite {c. ?P c}"
        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
        by metis
      hence "∃c. ?P c" using not_finite_existsD by blast
      thus ?case using someI_ex[of ?P] by auto
    next
      case (Fun f T)
      have f: "0 < arity f" using Fun.prems fun_type_inv by auto
      have "⋀t. t ∈ set T ⟹ ?P t"
        using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
        by metis
      hence "⋀t. t ∈ set T ⟹ Γ (fresh_pgwt S t) = t" using Fun.prems Fun.IH by auto
      hence "map Γ (map (fresh_pgwt S) T) = T"  by (induct T) auto
      thus ?case using fun_type[OF f] by simp
    qed
  } thus ?thesis using assms(1) Γ_wf'[OF assms(2)] Γ_wf'' by auto
qed

private lemma fresh_pgwt_empty_synth:
  assumes "finite S" "wftrm t"
  shows "{} ⊢c fresh_pgwt S (Γ t)"
proof -
  let ?P = "λτ::('fun,'atom) term_type. wftrm τ ∧ (∀f T. TComp f T ⊑ τ ⟶ 0 < arity f)"
  { fix τ assume "?P τ" hence "{} ⊢c fresh_pgwt S τ"
    proof (induction τ)
      case (Var a)
      let ?P = "λc. c ∉ S ∧ Γ (Fun c []) = Var a ∧ public c"
      let ?Q = "λc. Γ (Fun c []) = Var a ∧ public c"
      have " {c. ?Q c} - S = {c. ?P c}" by auto
      hence "infinite {c. ?P c}"
        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
        by metis
      hence "∃c. ?P c" using not_finite_existsD by blast
      thus ?case
        using someI_ex[of ?P] intruder_synth.ComposeC[of "[]" _ "{}"] const_type_inv
        by auto
    next
      case (Fun f T)
      have f: "0 < arity f" "length T = arity f" "public f" 
        using Fun.prems fun_type_inv unfolding wftrm_def by auto
      have "⋀t. t ∈ set T ⟹ ?P t"
        using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
        by metis
      hence "⋀t. t ∈ set T ⟹ {} ⊢c fresh_pgwt S t" using Fun.prems Fun.IH by auto
      moreover have "length (map (fresh_pgwt S) T) = arity f" using f(2) by auto
      ultimately show ?case using intruder_synth.ComposeC[of "map (fresh_pgwt S) T" f] f by auto
    qed
  } thus ?thesis using assms(1) Γ_wf'[OF assms(2)] Γ_wf'' by auto
qed

private lemma fresh_pgwt_has_fresh_const:
  assumes "finite S" "wftrm t"
  obtains c where "Fun c [] ⊑ fresh_pgwt S (Γ t)" "c ∉ S"
proof -
  let ?P = "λτ::('fun,'atom) term_type. wftrm τ ∧ (∀f T. TComp f T ⊑ τ ⟶ 0 < arity f)"
  { fix τ assume "?P τ" hence "∃c. Fun c [] ⊑ fresh_pgwt S τ ∧ c ∉ S"
    proof (induction τ)
      case (Var a)
      let ?P = "λc. c ∉ S ∧ Γ (Fun c []) = Var a ∧ public c"
      let ?Q = "λc. Γ (Fun c []) = Var a ∧ public c"
      have " {c. ?Q c} - S = {c. ?P c}" by auto
      hence "infinite {c. ?P c}"
        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
        by metis
      hence "∃c. ?P c" using not_finite_existsD by blast
      thus ?case using someI_ex[of ?P] by auto
    next
      case (Fun f T)
      have f: "0 < arity f" "length T = arity f" "public f" "T ≠ []"
        using Fun.prems fun_type_inv unfolding wftrm_def by auto
      obtain t' where t': "t' ∈ set T" by (meson all_not_in_conv f(4) set_empty) 
      have "⋀t. t ∈ set T ⟹ ?P t"
        using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
        by metis
      hence "⋀t. t ∈ set T ⟹ ∃c. Fun c [] ⊑ fresh_pgwt S t ∧ c ∉ S"
        using Fun.prems Fun.IH by auto
      then obtain c where c: "Fun c [] ⊑ fresh_pgwt S t'" "c ∉ S" using t' by metis
      thus ?case using t' by auto
    qed
  } thus ?thesis using that assms Γ_wf'[OF assms(2)] Γ_wf'' by blast 
qed

private lemma fresh_pgwt_subterm_fresh:
  assumes "finite S" "wftrm t" "wftrm s" "funs_term s ⊆ S"
  shows "s ∉ subterms (fresh_pgwt S (Γ t))"
proof -
  let ?P = "λτ::('fun,'atom) term_type. wftrm τ ∧ (∀f T. TComp f T ⊑ τ ⟶ 0 < arity f)"
  { fix τ assume "?P τ" hence "s ∉ subterms (fresh_pgwt S τ)"
    proof (induction τ)
      case (Var a)
      let ?P = "λc. c ∉ S ∧ Γ (Fun c []) = Var a ∧ public c"
      let ?Q = "λc. Γ (Fun c []) = Var a ∧ public c"
      have " {c. ?Q c} - S = {c. ?P c}" by auto
      hence "infinite {c. ?P c}"
        using Diff_infinite_finite[OF assms(1) infinite_typed_consts[of a]] 
        by metis
      hence "∃c. ?P c" using not_finite_existsD by blast
      thus ?case using someI_ex[of ?P] assms(4) by auto
    next
      case (Fun f T)
      have f: "0 < arity f" "length T = arity f" "public f" 
        using Fun.prems fun_type_inv unfolding wftrm_def by auto
      have "⋀t. t ∈ set T ⟹ ?P t"
        using Fun.prems wf_trm_subtermeq term.le_less_trans Fun_param_is_subterm
        by metis
      hence "⋀t. t ∈ set T ⟹ s ∉ subterms (fresh_pgwt S t)" using Fun.prems Fun.IH by auto
      moreover have "s ≠ fresh_pgwt S (Fun f T)"
      proof -
        obtain c where c: "Fun c [] ⊑ fresh_pgwt S (Fun f T)" "c ∉ S"
          using fresh_pgwt_has_fresh_const[OF assms(1)] type_wfttype_inhabited Fun.prems
          by metis
        hence "¬Fun c [] ⊑ s" using assms(4) subtermeq_imp_funs_term_subset by force
        thus ?thesis using c(1) by auto
      qed
      ultimately show ?case by auto
    qed
  } thus ?thesis using assms(1) Γ_wf'[OF assms(2)] Γ_wf'' by auto
qed

private lemma wt_fresh_pgwt_term_exists:
  assumes "finite T" "wftrm s" "wftrms T"
  obtains t where "Γ t = Γ s" "{} ⊢c t" "∀s ∈ T. ∀u ∈ subterms s. u ∉ subterms t"
proof -
  have finite_S: "finite (⋃(funs_term ` T))" using assms(1) by auto

  have 1: "Γ (fresh_pgwt (⋃(funs_term ` T)) (Γ s)) = Γ s"
    using fresh_pgwt_same_type[OF finite_S assms(2)] by auto

  have 2: "{} ⊢c fresh_pgwt (⋃(funs_term ` T)) (Γ s)"
    using fresh_pgwt_empty_synth[OF finite_S assms(2)] by auto

  have 3: "∀v ∈ T. ∀u ∈ subterms v. u ∉ subterms (fresh_pgwt (⋃(funs_term ` T)) (Γ s))"
    using fresh_pgwt_subterm_fresh[OF finite_S assms(2)] assms(3)
          wf_trm_subtermeq subtermeq_imp_funs_term_subset
    by force

  show ?thesis by (rule that[OF 1 2 3])
qed

lemma wt_bij_finite_subst_exists:
  assumes "finite (S::'var set)" "finite (T::('fun,'var) terms)" "wftrms T"
  shows "∃σ::('fun,'var) subst.
              subst_domain σ = S
            ∧ bij_betw σ (subst_domain σ) (subst_range σ)
            ∧ subtermsset (subst_range σ) ⊆ {t. {} ⊢c t} - T
            ∧ (∀s ∈ subst_range σ. ∀u ∈ subst_range σ. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u)
            ∧ wtsubst σ
            ∧ wftrms (subst_range σ)"
using assms
proof (induction rule: finite_induct)
  case empty
  have "subst_domain Var = {}"
       "bij_betw Var (subst_domain Var) (subst_range Var)"
       "subtermsset (subst_range Var) ⊆ {t. {} ⊢c t} - T"
       "∀s ∈ subst_range Var. ∀u ∈ subst_range Var. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u"
       "wtsubst Var"
       "wftrms (subst_range Var)"
    unfolding bij_betw_def
    by auto
  thus ?case by (force simp add: subst_domain_def)
next
  case (insert x S)
  then obtain σ where σ:
      "subst_domain σ = S" "bij_betw σ (subst_domain σ) (subst_range σ)"
      "subtermsset (subst_range σ) ⊆ {t. {} ⊢c t} - T"
      "∀s ∈ subst_range σ. ∀u ∈ subst_range σ. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u"
      "wtsubst σ" "wftrms (subst_range σ)"
    by (auto simp del: subst_range.simps)

  have *: "finite (T ∪ subst_range σ)"
    using insert.prems(1) insert.hyps(1) σ(1) by simp
  have **: "wftrm (Var x)" by simp
  have ***: "wftrms (T ∪ subst_range σ)" using assms(3) σ(6) by blast
  obtain t where t:
      "Γ t = Γ (Var x)" "{} ⊢c t"
      "∀s ∈ T ∪ subst_range σ. ∀u ∈ subterms s. u ∉ subterms t"
    using wt_fresh_pgwt_term_exists[OF * ** ***] by auto

  obtain θ where θ: "θ ≡ λy. if x = y then t else σ y" by simp

  have t_ground: "fv t = {}" using t(2) pgwt_ground[of t] pgwt_is_empty_synth[of t] by auto
  hence x_dom: "x ∉ subst_domain σ" "x ∈ subst_domain θ" using insert.hyps(2) σ(1) θ by auto
  moreover have "subst_range σ ⊆ subtermsset (subst_range σ)" by auto
  hence ground_imgs: "ground (subst_range σ)"
    using σ(3) pgwt_ground pgwt_is_empty_synth
    by force
  ultimately have x_img: "σ x ∉ subst_range σ"
    using ground_subst_dom_iff_img
    by (auto simp add: subst_domain_def)

  have "ground (insert t (subst_range σ))"
    using ground_imgs x_dom t_ground
    by auto
  have θ_dom: "subst_domain θ = insert x (subst_domain σ)"
    using θ t_ground by (auto simp add: subst_domain_def)
  have θ_img: "subst_range θ = insert t (subst_range σ)"
  proof
    show "subst_range θ ⊆ insert t (subst_range σ)"
    proof
      fix t' assume "t' ∈ subst_range θ"
      then obtain y where "y ∈ subst_domain θ" "t' = θ y" by auto
      thus "t' ∈ insert t (subst_range σ)" using θ by (auto simp add: subst_domain_def)
    qed
    show "insert t (subst_range σ) ⊆ subst_range θ"
    proof
      fix t' assume t': "t' ∈ insert t (subst_range σ)"
      hence "fv t' = {}" using ground_imgs x_img t_ground by auto
      hence "t' ≠ Var x" by auto
      show "t' ∈ subst_range θ"
      proof (cases "t' = t")
        case False
        hence "t' ∈ subst_range σ" using t' by auto
        then obtain y where "σ y ∈ subst_range σ" "t' = σ y" by auto
        hence "y ∈ subst_domain σ" "t' ≠ Var y"
          using ground_subst_dom_iff_img[OF ground_imgs(1)]
          by (auto simp add: subst_domain_def simp del: subst_range.simps)
        hence "x ≠ y" using x_dom by auto
        hence "θ y = σ y" unfolding θ by auto
        thus ?thesis using ‹t' ≠ Var y› ‹t' = σ y› subst_imgI[of θ y] by auto
      qed (metis subst_imgI θ ‹t' ≠ Var x›)
    qed
  qed
  hence θ_ground_img: "ground (subst_range θ)"
    using ground_imgs t_ground
    by auto

  have "subst_domain θ = insert x S" using θ_dom σ(1) by auto
  moreover have "bij_betw θ (subst_domain θ) (subst_range θ)"
  proof (intro bij_betwI')
    fix y z assume *: "y ∈ subst_domain θ" "z ∈ subst_domain θ"
    hence "fv (θ y) = {}" "fv (θ z) = {}" using θ_ground_img by auto
    { assume "θ y = θ z" hence "y = z"
      proof (cases "θ y ∈ subst_range σ ∧ θ z ∈ subst_range σ")
        case True
        hence **: "y ∈ subst_domain σ" "z ∈ subst_domain σ"
          using θ θ_dom True * t(3) by (metis Un_iff term.order_refl insertE)+ 
        hence "y ≠ x" "z ≠ x" using x_dom by auto
        hence "θ y = σ y" "θ z = σ z" using θ by auto
        thus ?thesis using ‹θ y = θ z› σ(2) ** unfolding bij_betw_def inj_on_def by auto
      qed (metis θ * ‹θ y = θ z› θ_dom ground_imgs(1) ground_subst_dom_iff_img insertE)
    }
    thus "(θ y = θ z) = (y = z)" by auto
  next
    fix y assume "y ∈ subst_domain θ" thus "θ y ∈ subst_range θ" by auto
  next
    fix t assume "t ∈ subst_range θ" thus "∃z ∈ subst_domain θ. t = θ z" by auto
  qed
  moreover have "subtermsset (subst_range θ) ⊆ {t. {} ⊢c t}  - T"
  proof -
    { fix s assume "s ⊑ t"
      hence "s ∈ {t. {} ⊢c t}  - T"
        using t(2,3) 
        by (metis Diff_eq_empty_iff Diff_iff Un_upper1 term.order_refl
                  deduct_synth_subterm mem_Collect_eq) 
    } thus ?thesis using σ(3) θ θ_img by auto
  qed
  moreover have "wtsubst θ" using θ t(1) σ(5) unfolding wtsubst_def by auto
  moreover have "wftrms (subst_range θ)"
    using θ σ(6) t(2) pgwt_is_empty_synth pgwt_wellformed
          wf_trm_subst_range_iff[of σ] wf_trm_subst_range_iff[of θ]
    by metis
  moreover have "∀s∈subst_range θ. ∀u∈subst_range θ. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u"
    using σ(4) θ_img t(3) by (auto simp del: subst_range.simps)
  ultimately show ?case by blast
qed

private lemma wt_bij_finite_tatom_subst_exists_single:
  assumes "finite (S::'var set)" "finite (T::('fun,'var) terms)"
  and "⋀x. x ∈ S ⟹ Γ (Var x) = TAtom a"
  shows "∃σ::('fun,'var) subst. subst_domain σ = S
                      ∧ bij_betw σ (subst_domain σ) (subst_range σ)
                      ∧ subst_range σ ⊆ ((λc. Fun c []) `  {c. Γ (Fun c []) = TAtom a ∧
                                                            public c ∧ arity c = 0}) - T
                      ∧ wtsubst σ
                      ∧ wftrms (subst_range σ)"
proof -
  let ?U = "{c. Γ (Fun c []) = TAtom a ∧ public c ∧ arity c = 0}"

  obtain σ where σ:
      "subst_domain σ = S" "bij_betw σ (subst_domain σ) (subst_range σ)"
      "subst_range σ ⊆ ((λc. Fun c []) ` ?U) - T"
    using bij_finite_const_subst_exists'[OF assms(1,2) infinite_typed_consts'[of a]]
    by auto

  { fix x assume "x ∉ subst_domain σ" hence "Γ (Var x) = Γ (σ x)" by auto }
  moreover
  { fix x assume "x ∈ subst_domain σ"
    hence "∃c ∈ ?U. σ x = Fun c [] ∧ arity c = 0" using σ by auto
    hence "Γ (σ x) = TAtom a" "wftrm (σ x)" using assms(3) const_type wf_trmI[of "[]"] by auto
    hence "Γ (Var x) = Γ (σ x)" "wftrm (σ x)" using assms(3) σ(1) by force+
  }
  ultimately have "wtsubst σ" "wftrms (subst_range σ)"
    using wf_trm_subst_range_iff[of σ]
    unfolding wtsubst_def
    by force+
  thus ?thesis using σ by auto
qed

lemma wt_bij_finite_tatom_subst_exists:
  assumes "finite (S::'var set)" "finite (T::('fun,'var) terms)"
  and "⋀x. x ∈ S ⟹ ∃a. Γ (Var x) = TAtom a"
  shows "∃σ::('fun,'var) subst. subst_domain σ = S
                      ∧ bij_betw σ (subst_domain σ) (subst_range σ)
                      ∧ subst_range σ ⊆ ((λc. Fun c []) `  𝒞pub) - T
                      ∧ wtsubst σ
                      ∧ wftrms (subst_range σ)"
using assms
proof (induction rule: finite_induct)
  case empty
  have "subst_domain Var = {}"
       "bij_betw Var (subst_domain Var) (subst_range Var)"
       "subst_range Var ⊆ ((λc. Fun c []) `  𝒞pub) - T"
       "wtsubst Var"
       "wftrms (subst_range Var)"
    unfolding bij_betw_def
    by auto
  thus ?case by (auto simp add: subst_domain_def)
next
  case (insert x S)
  then obtain a where a: "Γ (Var x) = TAtom a" by fastforce

  from insert obtain σ where σ:
      "subst_domain σ = S" "bij_betw σ (subst_domain σ) (subst_range σ)"
      "subst_range σ ⊆ ((λc. Fun c []) `  𝒞pub) - T" "wtsubst σ"
      "wftrms (subst_range σ)"
    by auto

  let ?S' = "{y ∈ S. Γ (Var y) = TAtom a}"
  let ?T' = "T ∪ subst_range σ"

  have *: "finite (insert x ?S')" using insert by simp
  have **: "finite ?T'" using insert.prems(1) insert.hyps(1) σ(1) by simp
  have ***: "⋀y. y ∈ insert x ?S' ⟹ Γ (Var y) = TAtom a" using a by auto

  obtain δ where δ:
      "subst_domain δ = insert x ?S'" "bij_betw δ (subst_domain δ) (subst_range δ)"
      "subst_range δ ⊆ ((λc. Fun c []) `  𝒞pub) - ?T'" "wtsubst δ" "wftrms (subst_range δ)"
    using wt_bij_finite_tatom_subst_exists_single[OF * ** ***] const_type_inv[of _ "[]" a]
    by blast

  obtain θ where θ: "θ ≡ λy. if x = y then δ y else σ y" by simp

  have x_dom: "x ∉ subst_domain σ" "x ∈ subst_domain δ" "x ∈ subst_domain θ"
    using insert.hyps(2) σ(1) δ(1) θ by (auto simp add: subst_domain_def)
  moreover have ground_imgs: "ground (subst_range σ)" "ground (subst_range δ)"
    using pgwt_ground σ(3) δ(3) by auto
  ultimately have x_img: "σ x ∉ subst_range σ" "δ x ∈ subst_range δ"
    using ground_subst_dom_iff_img by (auto simp add: subst_domain_def)

  have "ground (insert (δ x) (subst_range σ))" using ground_imgs x_dom by auto
  have θ_dom: "subst_domain θ = insert x (subst_domain σ)"
    using δ(1) θ by (auto simp add: subst_domain_def)
  have θ_img: "subst_range θ = insert (δ x) (subst_range σ)"
  proof
    show "subst_range θ ⊆ insert (δ x) (subst_range σ)"
    proof
      fix t assume "t ∈ subst_range θ"
      then obtain y where "y ∈ subst_domain θ" "t = θ y" by auto
      thus "t ∈ insert (δ x) (subst_range σ)" using θ by (auto simp add: subst_domain_def)
    qed
    show "insert (δ x) (subst_range σ) ⊆ subst_range θ"
    proof
      fix t assume t: "t ∈ insert (δ x) (subst_range σ)"
      hence "fv t = {}" using ground_imgs x_img(2) by auto
      hence "t ≠ Var x" by auto
      show "t ∈ subst_range θ"
      proof (cases "t = δ x")
        case True thus ?thesis using subst_imgI θ ‹t ≠ Var x› by metis
      next
        case False
        hence "t ∈ subst_range σ" using t by auto
        then obtain y where "σ y ∈ subst_range σ" "t = σ y" by auto
        hence "y ∈ subst_domain σ" "t ≠ Var y"
          using ground_subst_dom_iff_img[OF ground_imgs(1)]
          by (auto simp add: subst_domain_def simp del: subst_range.simps)
        hence "x ≠ y" using x_dom by auto
        hence "θ y = σ y" unfolding θ by auto
        thus ?thesis using ‹t ≠ Var y› ‹t = σ y› subst_imgI[of θ y] by auto
      qed
    qed
  qed
  hence θ_ground_img: "ground (subst_range θ)" using ground_imgs x_img by auto

  have "subst_domain θ = insert x S" using θ_dom σ(1) by auto
  moreover have "bij_betw θ (subst_domain θ) (subst_range θ)"
  proof (intro bij_betwI')
    fix y z assume *: "y ∈ subst_domain θ" "z ∈ subst_domain θ"
    hence "fv (θ y) = {}" "fv (θ z) = {}" using θ_ground_img by auto
    { assume "θ y = θ z" hence "y = z"
      proof (cases "θ y ∈ subst_range σ ∧ θ z ∈ subst_range σ")
        case True
        hence **: "y ∈ subst_domain σ" "z ∈ subst_domain σ"
          using θ θ_dom x_img(2) δ(3) True
          by (metis (no_types) *(1) DiffE Un_upper2 insertE subsetCE,
              metis (no_types) *(2) DiffE Un_upper2 insertE subsetCE)
        hence "y ≠ x" "z ≠ x" using x_dom by auto
        hence "θ y = σ y" "θ z = σ z" using θ by auto
        thus ?thesis using ‹θ y = θ z› σ(2) ** unfolding bij_betw_def inj_on_def by auto
      qed (metis θ * ‹θ y = θ z› θ_dom ground_imgs(1) ground_subst_dom_iff_img insertE)
    }
    thus "(θ y = θ z) = (y = z)" by auto
  next
    fix y assume "y ∈ subst_domain θ" thus "θ y ∈ subst_range θ" by auto
  next
    fix t assume "t ∈ subst_range θ" thus "∃z ∈ subst_domain θ. t = θ z" by auto
  qed
  moreover have "subst_range θ ⊆ (λc. Fun c []) ` 𝒞pub - T"
    using σ(3) δ(3) θ by (auto simp add: subst_domain_def)
  moreover have "wtsubst θ" using σ(4) δ(4) θ unfolding wtsubst_def by auto
  moreover have "wftrms (subst_range θ)"
    using θ σ(5) δ(5) wf_trm_subst_range_iff[of δ]
          wf_trm_subst_range_iff[of σ] wf_trm_subst_range_iff[of θ]
    by presburger
  ultimately show ?case by blast
qed

theorem wt_sat_if_simple:
  assumes "simple S" "wfconstr S θ" "wtsubst θ" "wftrms (subst_range θ)" "wftrms (trmsst S)"
  and ℐ': "∀X F. Inequality X F ∈ set S ⟶ ineq_model ℐ' X F"
         "ground (subst_range ℐ')"
         "subst_domain ℐ' = {x ∈ varsst S. ∃X F. Inequality X F ∈ set S ∧ x ∈ fvpairs F - set X}"
  and tfr_stp_all: "list_all tfrstp S"
  shows "∃ℐ. interpretationsubst ℐ ∧ (ℐ ⊨c ⟨S, θ⟩) ∧ wtsubst ℐ ∧ wftrms (subst_range ℐ)"
proof -
  from ‹wfconstr S θ› have "wfst {} S" "subst_idem θ" and S_θ_disj: "∀v ∈ varsst S. θ v = Var v"
    using subst_idemI[of θ] unfolding wfconstr_def wfsubst_def by force+
  
  obtain ℐ::"('fun,'var) subst"
    where ℐ: "interpretationsubst ℐ" "wtsubst ℐ" "subst_range ℐ ⊆ public_ground_wf_terms"
    using wt_interpretation_exists by blast
  hence ℐ_deduct: "⋀x M. M ⊢c ℐ x" and ℐ_wf_trm: "wftrms (subst_range ℐ)"
    using pgwt_deducible pgwt_wellformed by fastforce+

  let ?P = "λδ X. subst_domain δ = set X ∧ ground (subst_range δ)"
  let ?Sineqsvars = "{x ∈ varsst S. ∃X F. Inequality X F ∈ set S ∧ x ∈ fvpairs F ∧ x ∉ set X}"
  let ?Strms = "subtermsset (trmsst S)"

  have finite_vars: "finite ?Sineqsvars" "finite ?Strms" "wftrms ?Strms"
    using wf_trm_subtermeq assms(5) by fastforce+

  define Q1 where "Q1 = (λ(F::(('fun,'var) term × ('fun,'var) term) list) X.
    ∀x ∈ fvpairs F - set X. ∃a. Γ (Var x) = TAtom a)"

  define Q2 where "Q2 = (λ(F::(('fun,'var) term × ('fun,'var) term) list) X.
    ∀f T. Fun f T ∈ subtermsset (trmspairs F) ⟶ T = [] ∨ (∃s ∈ set T. s ∉ Var ` set X))"

  define Q1' where "Q1' = (λ(t::('fun,'var) term) (t'::('fun,'var) term) X.
    ∀x ∈ (fv t ∪ fv t') - set X. ∃a. Γ (Var x) = TAtom a)"

  define Q2' where "Q2' = (λ(t::('fun,'var) term) (t'::('fun,'var) term) X.
    ∀f T. Fun f T ∈ subterms t ∪ subterms t' ⟶ T = [] ∨ (∃s ∈ set T. s ∉ Var ` set X))"

  have ex_P: "∀X. ∃δ. ?P δ X" using interpretation_subst_exists' by blast

  have tfr_ineq: "∀X F. Inequality X F ∈ set S ⟶ Q1 F X ∨ Q2 F X"
    using tfr_stp_all Q1_def Q2_def tfrstp_list_all_alt_def[of S] by blast

  have S_fv_bvars_disj: "fvst S ∩ bvarsst S = {}" using ‹wfconstr S θ› unfolding wfconstr_def by metis
  hence ineqs_vars_not_bound: "∀X F x. Inequality X F ∈ set S ⟶ x ∈ ?Sineqsvars ⟶ x ∉ set X"
    using strand_fv_bvars_disjoint_unfold by blast

  have θ_vars_S_bvars_disj: "(subst_domain θ ∪ range_vars θ) ∩ set X = {}"
    when "Inequality X F ∈ set S" for F X
    using wf_constr_bvars_disj[OF ‹wfconstr S θ›]
          strand_fv_bvars_disjointD(1)[OF S_fv_bvars_disj that]
    by blast

  obtain σ::"('fun,'var) subst"
    where σ_fv_dom: "subst_domain σ = ?Sineqsvars"
    and σ_subterm_inj: "subterm_inj_on σ (subst_domain σ)"
    and σ_fresh_pub_img: "subtermsset (subst_range σ) ⊆ {t. {} ⊢c t} - ?Strms"
    and σ_wt: "wtsubst σ"
    and σ_wf_trm: "wftrms (subst_range σ)"
    using wt_bij_finite_subst_exists[OF finite_vars]
          subst_inj_on_is_bij_betw subterm_inj_on_alt_def'
    by moura

  have σ_bij_dom_img: "bij_betw σ (subst_domain σ) (subst_range σ)"
    by (metis σ_subterm_inj subst_inj_on_is_bij_betw subterm_inj_on_alt_def)

  have "finite (subst_domain σ)" by(metis σ_fv_dom finite_vars(1))
  hence σ_finite_img: "finite (subst_range σ)" using σ_bij_dom_img bij_betw_finite by blast 
  
  have σ_img_subterms: "∀s ∈ subst_range σ. ∀u ∈ subst_range σ. (∃v. v ⊑ s ∧ v ⊑ u) ⟶ s = u"
    by (metis σ_subterm_inj subterm_inj_on_alt_def')

  have "subst_range σ ⊆ subtermsset (subst_range σ)" by auto
  hence "subst_range σ ⊆ public_ground_wf_terms - ?Strms"
      and σ_pgwt_img:
        "subst_range σ ⊆ public_ground_wf_terms"
        "subtermsset (subst_range σ) ⊆ public_ground_wf_terms"
    using σ_fresh_pub_img pgwt_is_empty_synth by blast+

  have σ_img_ground: "ground (subst_range σ)"
    using σ_pgwt_img pgwt_ground by auto
  hence σ_inj: "inj σ"
    using σ_bij_dom_img subst_inj_is_bij_betw_dom_img_if_ground_img by auto

  have σ_ineqs_fv_dom: "⋀X F. Inequality X F ∈ set S ⟹ fvpairs F - set X ⊆ subst_domain σ"
    using σ_fv_dom by fastforce

  have σ_dom_bvars_disj: "∀X F. Inequality X F ∈ set S ⟶ subst_domain σ ∩ set X = {}"
    using ineqs_vars_not_bound σ_fv_dom by fastforce
  
  have ℐ'1: "∀X F δ. Inequality X F ∈ set S ⟶ fvpairs F - set X ⊆ subst_domain ℐ'"
    using ℐ'(3) ineqs_vars_not_bound by fastforce
  
  have ℐ'2: "∀X F. Inequality X F ∈ set S ⟶ subst_domain ℐ' ∩ set X = {}"
    using ℐ'(3) ineqs_vars_not_bound by blast
  
  have doms_eq: "subst_domain ℐ' = subst_domain σ" using ℐ'(3) σ_fv_dom by simp

  have σ_ineqs_neq: "ineq_model σ X F" when "Inequality X F ∈ set S" for X F
  proof -
    obtain a::"'fun" where a: "a ∉ ⋃(funs_term ` subtermsset (subst_range σ))"
      using exists_fun_notin_funs_terms[OF subterms_union_finite[OF σ_finite_img]]
      by moura
    hence a': "⋀T. Fun a T ∉ subtermsset (subst_range σ)"
              "⋀S. Fun a [] ∈ set (Fun a []#S)" "Fun a [] ∉ Var ` set X"
      by (meson a UN_I term.set_intros(1), auto)

    define t where "t ≡ Fun a (Fun a []#map fst F)"
    define t' where "t' ≡ Fun a (Fun a []#map snd F)"

    note F_in = that

    have t_fv: "fv t ∪ fv t' ⊆ fvpairs F"
      unfolding t_def t'_def by force

    have t_subterms: "subterms t ∪ subterms t' ⊆ subtermsset (trmspairs F) ∪ {t, t', Fun a []}"
      unfolding t_def t'_def by force

    have "t ⋅ δ ⋅ σ ≠ t' ⋅ δ ⋅ σ" when "?P δ X" for δ
    proof -
      have tfr_assms: "Q1 F X ∨ Q2 F X" using tfr_ineq F_in by metis
  
      have "Q1 F X ⟹ ∀x ∈ fvpairs F - set X. ∃c. σ x = Fun c []"
      proof
        fix x assume "Q1 F X" and x: "x ∈ fvpairs F - set X"
        then obtain a where "Γ (Var x) = TAtom a" unfolding Q1_def by moura
        hence a: "Γ (σ x) = TAtom a" using σ_wt unfolding wtsubst_def by simp
        
        have "x ∈ subst_domain σ" using σ_ineqs_fv_dom x F_in by auto
        then obtain f T where fT: "σ x = Fun f T" by (meson σ_img_ground ground_img_obtain_fun)
        hence "T = []" using σ_wf_trm a TAtom_term_cases by fastforce
        thus "∃c. σ x = Fun c []" using fT by metis
      qed
      hence 1: "Q1 F X ⟹ ∀x ∈ (fv t ∪ fv t') - set X. ∃c. σ x = Fun c []"
        using t_fv by auto
  
      have 2: "¬Q1 F X ⟹ Q2 F X" by (metis tfr_assms)
  
      have 3: "subst_domain σ ∩ set X = {}" using σ_dom_bvars_disj F_in by auto

      have 4: "subtermsset (subst_range σ) ∩ (subterms t ∪ subterms t') = {}"
      proof -
        define M1 where "M1 ≡ {t, t', Fun a []}"
        define M2 where "M2 ≡ ?Strms"

        have "subtermsset (trmspairs F) ⊆ M2"
          using F_in unfolding M2_def by force
        moreover have "subterms t ∪ subterms t' ⊆ subtermsset (trmspairs F) ∪ M1"
          using t_subterms unfolding M1_def by blast
        ultimately have *: "subterms t ∪ subterms t' ⊆ M2 ∪ M1"
          by auto

        have "subtermsset (subst_range σ) ∩ M1 = {}"
             "subtermsset (subst_range σ) ∩ M2 = {}"
          using a' σ_fresh_pub_img
          unfolding t_def t'_def M1_def M2_def
          by blast+
        thus ?thesis using * by blast
      qed
  
      have 5: "(fv t ∪ fv t') - subst_domain σ ⊆ set X"
        using σ_ineqs_fv_dom[OF F_in] t_fv
        by auto
  
      have 6: "∀δ. ?P δ X ⟶ t ⋅ δ ⋅ ℐ' ≠ t' ⋅ δ ⋅ ℐ'"
        by (metis t_def t'_def ℐ'(1) F_in ineq_model_singleE ineq_model_single_iff)
  
      have 7: "fv t ∪ fv t' - set X ⊆ subst_domain ℐ'" using ℐ'1 F_in t_fv by force
  
      have 8: "subst_domain ℐ' ∩ set X = {}" using ℐ'2 F_in by auto

      have 9: "Q1' t t' X" when "Q1 F X"
        using that t_fv
        unfolding Q1_def Q1'_def t_def t'_def
        by blast

      have 10: "Q2' t t' X" when "Q2 F X" unfolding Q2'_def
      proof (intro allI impI)
        fix f T assume "Fun f T ∈ subterms t ∪ subterms t'"
        moreover {
          assume "Fun f T ∈ subtermsset (trmspairs F)"
          hence "T = [] ∨ (∃s∈set T. s ∉ Var ` set X)" by (metis Q2_def that)
        } moreover {
          assume "Fun f T = t" hence "T = [] ∨ (∃s∈set T. s ∉ Var ` set X)"
            unfolding t_def using a'(2,3) by simp
        } moreover {
          assume "Fun f T = t'" hence "T = [] ∨ (∃s∈set T. s ∉ Var ` set X)"
            unfolding t'_def using a'(2,3) by simp
        } moreover {
          assume "Fun f T = Fun a []" hence "T = [] ∨ (∃s∈set T. s ∉ Var ` set X)" by simp
        } ultimately show "T = [] ∨ (∃s∈set T. s ∉ Var ` set X)" using t_subterms by blast
      qed

      note 11 = σ_subterm_inj σ_img_ground 3 4 5
  
      note 12 = 6 7 8 ℐ'(2) doms_eq
  
      show "t ⋅ δ ⋅ σ ≠ t' ⋅ δ ⋅ σ"
        using 1 2 9 10 that sat_ineq_subterm_inj_subst[OF 11 _ 12] 
        unfolding Q1'_def Q2'_def by metis
    qed
    thus ?thesis by (metis t_def t'_def ineq_model_singleI ineq_model_single_iff)
  qed

  have σ_ineqs_fv_dom': "fvpairs (F ⋅pairs δ) ⊆ subst_domain σ"
    when "Inequality X F ∈ set S" and "?P δ X" for F δ X
    using σ_ineqs_fv_dom[OF that(1)]
  proof (induction F)
    case (Cons g G)
    obtain t t' where g: "g = (t,t')" by (metis surj_pair)
    hence "fvpairs (g#G ⋅pairs δ)  = fv (t ⋅ δ) ∪ fv (t' ⋅ δ) ∪ fvpairs (G ⋅pairs δ)"
          "fvpairs (g#G) = fv t ∪ fv t' ∪ fvpairs G"
      by (simp_all add: subst_apply_pairs_def)
    moreover have "fv (t ⋅ δ) = fv t - subst_domain δ" "fv (t' ⋅ δ) = fv t' - subst_domain δ"
      using g that(2) by (simp_all add: subst_fv_unfold_ground_img range_vars_alt_def)
    moreover have "fvpairs (G ⋅pairs δ) ⊆ subst_domain σ" using Cons by auto
    ultimately show ?case using Cons.prems that(2) by auto
  qed (simp add: subst_apply_pairs_def)

  have σ_ineqs_ground: "fvpairs ((F ⋅pairs δ) ⋅pairs σ) = {}"
    when "Inequality X F ∈ set S" and "?P δ X" for F δ X
    using σ_ineqs_fv_dom'[OF that]
  proof (induction F)
    case (Cons g G)
    obtain t t' where g: "g = (t,t')" by (metis surj_pair)
    hence "fv (t ⋅ δ) ⊆ subst_domain σ" "fv (t' ⋅ δ) ⊆ subst_domain σ"
      using Cons.prems by (auto simp add: subst_apply_pairs_def)
    hence "fv (t ⋅ δ ⋅ σ) = {}" "fv (t' ⋅ δ ⋅ σ) = {}"
      using subst_fv_dom_ground_if_ground_img[OF _ σ_img_ground] by metis+
    thus ?case using g Cons by (auto simp add: subst_apply_pairs_def)
  qed (simp add: subst_apply_pairs_def)
 
  from σ_pgwt_img σ_ineqs_neq have σ_deduct: "M ⊢c σ x" when "x ∈ subst_domain σ" for x M
    using that pgwt_deducible by fastforce

  { fix M::"('fun,'var) terms"
    have "⟦M; S⟧c (θ ∘s σ ∘s ℐ)"
      using ‹wfst {} S› ‹simple S› S_θ_disj σ_ineqs_neq σ_ineqs_fv_dom' θ_vars_S_bvars_disj
    proof (induction S arbitrary: M rule: wfst_simple_induct)
      case (ConsSnd v S)
      hence S_sat: "⟦M; S⟧c (θ ∘s σ ∘s ℐ)" and "θ v = Var v" by auto
      hence *: "⋀M. M ⊢c Var v ⋅ (θ ∘s σ ∘s ℐ)"
        using ℐ_deduct σ_deduct
        by (metis ideduct_synth_subst_apply subst_apply_term.simps(1)
                  subst_subst_compose trm_subst_ident')

      define M' where "M' ≡ M ∪ (ikst S ⋅set θ ∘s σ ∘s ℐ)"

      have "∀t ∈ set [Var v]. M' ⊢c t ⋅ (θ ∘s σ ∘s ℐ)" using *[of M'] by simp
      thus ?case
        using strand_sem_append(1)[OF S_sat, of "[Send1 (Var v)]", unfolded M'_def[symmetric]]
              strand_sem_c.simps(1)[of M'] strand_sem_c.simps(2)[of M' "[Var v]" "[]"]
        by presburger
    next
      case (ConsIneq X F S)
      have dom_disj: "subst_domain θ ∩ fvpairs F = {}"
        using ConsIneq.prems(1) subst_dom_vars_in_subst
        by force
      hence *: "F ⋅pairs θ = F" by blast

      have **: "ineq_model σ X F" by (meson ConsIneq.prems(2) in_set_conv_decomp)

      have "⋀x. x ∈ varsst S ⟹ x ∈ varsst (S@[Inequality X F])"
           "⋀x. x ∈ set S ⟹ x ∈ set (S@[Inequality X F])" by auto
      hence IH: "⟦M; S⟧c (θ ∘s σ ∘s ℐ)" by (metis ConsIneq.IH ConsIneq.prems(1,2,3,4))

      have "ineq_model (σ ∘s ℐ) X F"
      proof -
        have "fvpairs (F ⋅pairs δ) ⊆ subst_domain σ" when "?P δ X" for δ
          using ConsIneq.prems(3)[OF _ that] by simp
        hence "fvpairs F - set X ⊆ subst_domain σ"
          using fvpairs_subst_subset ex_P
          by (metis Diff_subset_conv Un_commute)
        thus ?thesis by (metis ineq_model_ground_subst[OF _ σ_i