Theory Typed_Model

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

section ‹The Typed Model›
theory Typed_Model
imports Lazy_Intruder
begin

text ‹Term types›
type_synonym ('f,'v) term_type = "('f,'v) term"

text ‹Constructors for term types›
abbreviation (input) TAtom::"'v ⇒ ('f,'v) term_type" where
  "TAtom a ≡ Var a"

abbreviation (input) TComp::"['f, ('f,'v) term_type list] ⇒ ('f,'v) term_type" where
  "TComp f ts ≡ Fun f ts"


text ‹
  The typed model extends the intruder model with a typing function ‹Γ› that assigns types to terms.
›
locale typed_model = intruder_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)"
  +
  fixes Γ::"('fun,'var) term ⇒ ('fun,'atom::finite) term_type"
  assumes const_type: "⋀c. arity c = 0 ⟹ ∃a. ∀ts. Γ (Fun c ts) = TAtom a"
    and fun_type: "⋀f ts. arity f > 0 ⟹ Γ (Fun f ts) = TComp f (map Γ ts)"
    and Γ_wf: "⋀x f ts. TComp f ts ⊑ Γ (Var x) ⟹ arity f > 0"
              "⋀x. wftrm (Γ (Var x))"
begin


subsection ‹Definitions›
text ‹The set of atomic types›
abbreviation "𝔗a ≡ UNIV::('atom set)"

text ‹Well-typed substitutions›
definition wtsubst where
  "wtsubst σ ≡ (∀v. Γ (Var v) = Γ (σ v))"

text ‹The set of sub-message patterns (SMP)›
inductive_set SMP::"('fun,'var) terms ⇒ ('fun,'var) terms" for M where
  MP[intro]: "t ∈ M ⟹ t ∈ SMP M"
| Subterm[intro]: "⟦t ∈ SMP M; t' ⊑ t⟧ ⟹ t' ∈ SMP M"
| Substitution[intro]: "⟦t ∈ SMP M; wtsubst δ; wftrms (subst_range δ)⟧ ⟹ (t ⋅ δ) ∈ SMP M"
| Ana[intro]: "⟦t ∈ SMP M; Ana t = (K,T); k ∈ set K⟧ ⟹ k ∈ SMP M"

text ‹
  Type-flaw resistance for sets:
  Unifiable sub-message patterns must have the same type (unless they are variables)
›
definition tfrset where
  "tfrset M ≡ (∀s ∈ SMP M - (Var`𝒱). ∀t ∈ SMP M - (Var`𝒱). (∃δ. Unifier δ s t) ⟶ Γ s = Γ t)"

text ‹
  Type-flaw resistance for strand steps:
  - The terms in a satisfiable equality step must have the same types
  - Inequality steps must satisfy the conditions of the "inequality lemma"›
fun tfrstp where
  "tfrstp (Equality a t t') = ((∃δ. Unifier δ t t') ⟶ Γ t = Γ t')"
| "tfrstp (Inequality X F) = (
      (∀x ∈ fvpairs F - set X. ∃a. Γ (Var x) = TAtom a) ∨
      (∀f T. Fun f T ∈ subtermsset (trmspairs F) ⟶ T = [] ∨ (∃s ∈ set T. s ∉ Var ` set X)))"
| "tfrstp _ = True"

text ‹
  Type-flaw resistance for strands:
  - The set of terms in strands must be type-flaw resistant
  - The steps of strands must be type-flaw resistant
›
definition tfrst where
  "tfrst S ≡ tfrset (trmsst S) ∧ list_all tfrstp S"


subsection ‹Small Lemmata›
lemma tfrstp_list_all_alt_def:
  "list_all tfrstp S ⟷
    ((∀a t t'. Equality a t t' ∈ set S ∧ (∃δ. Unifier δ t t') ⟶ Γ t = Γ t') ∧
    (∀X F. Inequality X F ∈ set S ⟶ 
      (∀x ∈ fvpairs F - set X. ∃a. Γ (Var x) = TAtom a)
    ∨ (∀f T. Fun f T ∈ subtermsset (trmspairs F) ⟶ T = [] ∨ (∃s ∈ set T. s ∉ Var ` set X))))"
  (is "?P S ⟷ ?Q S")
proof
  show "?P S ⟹ ?Q S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp

  show "?Q S ⟹ ?P S"
  proof (induction S)
    case (Cons x S) thus ?case by (cases x) auto
  qed simp
qed

lemma Γ_wf'': "TComp f T ⊑ Γ t ⟹ arity f > 0"
proof (induction t)
  case (Var x) thus ?case using Γ_wf(1)[of f T x] by blast
next
  case (Fun g S) thus ?case
    using fun_type[of g S] const_type[of g] by (cases "arity g") auto
qed

lemma Γ_wf': "wftrm t ⟹ wftrm (Γ t)"
proof (induction t)
  case (Fun f T)
  hence *: "arity f = length T" "⋀t. t ∈ set T ⟹ wftrm (Γ t)" unfolding wftrm_def by auto
  { assume "arity f = 0" hence ?case using const_type[of f] by auto }
  moreover
  { assume "arity f > 0" hence ?case using fun_type[of f] * by force }
  ultimately show ?case by auto 
qed (metis Γ_wf(2))

lemma fun_type_inv: assumes "Γ t = TComp f T" shows "arity f > 0"
using Γ_wf''(1)[of f T t] assms by simp_all

lemma fun_type_inv_wf: assumes "Γ t = TComp f T" "wftrm t" shows "arity f = length T"
using Γ_wf'[OF assms(2)] assms(1) unfolding wftrm_def by auto

lemma const_type_inv: "Γ (Fun c X) = TAtom a ⟹ arity c = 0"
by (rule ccontr, simp add: fun_type)

lemma const_type_inv_wf: assumes "Γ (Fun c X) = TAtom a" and "wftrm (Fun c X)" shows "X = []"
by (metis assms const_type_inv length_0_conv subtermeqI' wftrm_def)

lemma const_type': "∀c ∈ 𝒞. ∃a ∈ 𝔗a. ∀X. Γ (Fun c X) = TAtom a" using const_type by simp
lemma fun_type': "∀f ∈ Σf. ∀X. Γ (Fun f X) = TComp f (map Γ X)" using fun_type by simp

lemma fun_type_id_eq: "Γ (Fun f X) = TComp g Y ⟹ f = g"
by (metis const_type fun_type neq0_conv "term.inject"(2) "term.simps"(4))

lemma fun_type_length_eq: "Γ (Fun f X) = TComp g Y ⟹ length X = length Y"
by (metis fun_type fun_type_id_eq fun_type_inv(1) length_map term.inject(2))

lemma pgwt_type_map: 
  assumes "public_ground_wf_term t"
  shows "Γ t = TAtom a ⟹ ∃f. t = Fun f []" "Γ t = TComp g Y ⟹ ∃X. t = Fun g X ∧ map Γ X = Y"
proof -
  let ?A = "Γ t = TAtom a ⟶ (∃f. t = Fun f [])"
  let ?B = "Γ t = TComp g Y ⟶ (∃X. t = Fun g X ∧ map Γ X = Y)"
  have "?A ∧ ?B"
  proof (cases "Γ t")
    case (Var a)
    obtain f X where "t = Fun f X" "arity f = length X"
      using pgwt_fun[OF assms(1)] pgwt_arity[OF assms(1)] by fastforce+
    thus ?thesis using const_type_inv ‹Γ t = TAtom a› by auto
  next
    case (Fun g Y)
    obtain f X where *: "t = Fun f X" using pgwt_fun[OF assms(1)] by force
    hence "f = g" "map Γ X = Y"
      using fun_type_id_eq ‹Γ t = TComp g Y› fun_type[OF fun_type_inv(1)[OF ‹Γ t = TComp g Y›]]
      by fastforce+
    thus ?thesis using *(1) ‹Γ t = TComp g Y› by auto 
  qed
  thus "Γ t = TAtom a ⟹ ∃f. t = Fun f []" "Γ t = TComp g Y ⟹ ∃X. t = Fun g X ∧ map Γ X = Y"
    by auto
qed 

lemma wt_subst_Var[simp]: "wtsubst Var" by (metis wtsubst_def)

lemma wt_subst_trm: "(⋀v. v ∈ fv t ⟹ Γ (Var v) = Γ (θ v)) ⟹ Γ t = Γ (t ⋅ θ)"
proof (induction t)
  case (Fun f X)
  hence *: "⋀x. x ∈ set X ⟹ Γ x = Γ (x ⋅ θ)" by auto
  show ?case
  proof (cases "f ∈ Σf")
    case True
    hence "∀X. Γ (Fun f X) = TComp f (map Γ X)" using fun_type' by auto
    thus ?thesis using * by auto
  next
    case False
    hence "∃a ∈ 𝔗a. ∀X. Γ (Fun f X) = TAtom a" using const_type' by auto
    thus ?thesis by auto
  qed
qed auto

lemma wt_subst_trm': "⟦wtsubst σ; Γ s = Γ t⟧ ⟹ Γ (s ⋅ σ) = Γ (t ⋅ σ)"
by (metis wt_subst_trm wtsubst_def)

lemma wt_subst_trm'': "wtsubst σ ⟹ Γ t = Γ (t ⋅ σ)"
by (metis wt_subst_trm wtsubst_def)

lemma wt_subst_compose:
  assumes "wtsubst θ" "wtsubst δ" shows "wtsubst (θ ∘s δ)"
proof -
  have "⋀v. Γ (θ v) = Γ (θ v ⋅ δ)" using wt_subst_trm ‹wtsubst δ› unfolding wtsubst_def by metis
  moreover have "⋀v. Γ (Var v) = Γ (θ v)" using ‹wtsubst θ› unfolding wtsubst_def by metis
  ultimately have "⋀v. Γ (Var v) = Γ (θ v ⋅ δ)" by metis
  thus ?thesis unfolding wtsubst_def subst_compose_def by metis
qed

lemma wt_subst_TAtom_Var_cases:
  assumes θ: "wtsubst θ" "wftrms (subst_range θ)"
  and x: "Γ (Var x) = TAtom a"
  shows "(∃y. θ x = Var y) ∨ (∃c. θ x = Fun c [])"
proof (cases "(∃y. θ x = Var y)")
  case False
  then obtain c T where c: "θ x = Fun c T"
    by (cases "θ x") simp_all
  hence "wftrm (Fun c T)"
    using θ(2) by fastforce
  hence "T = []"
    using const_type_inv_wf[of c T a] x c wt_subst_trm''[OF θ(1), of "Var x"]
    by fastforce
  thus ?thesis
    using c by blast
qed simp

lemma wt_subst_TAtom_fv:
  assumes θ: "wtsubst θ" "∀x. wftrm (θ x)"
  and "∀x ∈ fv t - X. ∃a. Γ (Var x) = TAtom a"
  shows "∀x ∈ fv (t ⋅ θ) - fvset (θ ` X). ∃a. Γ (Var x) = TAtom a"
using assms(3)
proof (induction t)
  case (Var x) thus ?case
  proof (cases "x ∈ X")
    case False
    with Var obtain a where "Γ (Var x) = TAtom a" by moura
    hence *: "Γ (θ x) = TAtom a" "wftrm (θ x)" using θ unfolding wtsubst_def by auto
    show ?thesis
    proof (cases "θ x")
      case (Var y) thus ?thesis using * by auto
    next
      case (Fun f T)
      hence "T = []" using * const_type_inv[of f T a] unfolding wftrm_def by auto
      thus ?thesis using Fun by auto
    qed
  qed auto
qed fastforce

lemma wt_subst_TAtom_subterms_subst:
  assumes "wtsubst θ" "∀x ∈ fv t. ∃a. Γ (Var x) = TAtom a" "wftrms (θ ` fv t)"
  shows "subterms (t ⋅ θ) = subterms t ⋅set θ"
using assms(2,3)
proof (induction t)
  case (Var x)
  obtain a where a: "Γ (Var x) = TAtom a" using Var.prems(1) by moura
  hence "Γ (θ x) = TAtom a" using wt_subst_trm''[OF assms(1), of "Var x"] by simp
  hence "(∃y. θ x = Var y) ∨ (∃c. θ x = Fun c [])"
    using const_type_inv_wf Var.prems(2) by (cases "θ x") auto
  thus ?case by auto
next
  case (Fun f T)
  have "subterms (t ⋅ θ) = subterms t ⋅set θ" when "t ∈ set T" for t
    using that Fun.prems(1,2) Fun.IH[OF that]
    by auto
  thus ?case by auto
qed

lemma wt_subst_TAtom_subterms_set_subst: 
  assumes "wtsubst θ" "∀x ∈ fvset M. ∃a. Γ (Var x) = TAtom a" "wftrms (θ ` fvset M)"
  shows "subtermsset (M ⋅set θ) = subtermsset M ⋅set θ"
proof
  show "subtermsset (M ⋅set θ) ⊆ subtermsset M ⋅set θ"
  proof
    fix t assume "t ∈ subtermsset (M ⋅set θ)"
    then obtain s where s: "s ∈ M" "t ∈ subterms (s ⋅ θ)" by auto
    thus "t ∈ subtermsset M ⋅set θ"
      using assms(2,3) wt_subst_TAtom_subterms_subst[OF assms(1), of s]
      by auto
  qed

  show "subtermsset M ⋅set θ ⊆ subtermsset (M ⋅set θ)"
  proof
    fix t assume "t ∈ subtermsset M ⋅set θ"
    then obtain s where s: "s ∈ M" "t ∈ subterms s ⋅set θ" by auto
    thus "t ∈ subtermsset (M ⋅set θ)"
      using assms(2,3) wt_subst_TAtom_subterms_subst[OF assms(1), of s]
      by auto
  qed
qed

lemma wt_subst_subst_upd:
  assumes "wtsubst θ"
    and "Γ (Var x) = Γ t"
  shows "wtsubst (θ(x := t))"
using assms unfolding wtsubst_def
by (metis fun_upd_other fun_upd_same)

lemma wt_subst_const_fv_type_eq:
  assumes "∀x ∈ fv t. ∃a. Γ (Var x) = TAtom a"
    and δ: "wtsubst δ" "wftrms (subst_range δ)"
  shows "∀x ∈ fv (t ⋅ δ). ∃y ∈ fv t. Γ (Var x) = Γ (Var y)"
using assms(1)
proof (induction t)
  case (Var x)
  then obtain a where a: "Γ (Var x) = TAtom a" by moura
  show ?case
  proof (cases "δ x")
    case (Fun f T)
    hence "wftrm (Fun f T)" "Γ (Fun f T) = TAtom a"
      using a wt_subst_trm''[OF δ(1), of "Var x"] δ(2) by fastforce+
    thus ?thesis using const_type_inv_wf Fun by fastforce
  qed (use a wt_subst_trm''[OF δ(1), of "Var x"] in simp)
qed fastforce

lemma TComp_term_cases:
  assumes "wftrm t" "Γ t = TComp f T"
  shows "(∃v. t = Var v) ∨ (∃T'. t = Fun f T' ∧ T = map Γ T' ∧ T' ≠ [])"
proof (cases "∃v. t = Var v")
  case False
  then obtain T' where T': "t = Fun f T'" "T = map Γ T'"
    using assms fun_type[OF fun_type_inv(1)[OF assms(2)]] fun_type_id_eq
    by (cases t) force+
  thus ?thesis using assms fun_type_inv(1) fun_type_inv_wf by fastforce
qed metis

lemma TAtom_term_cases:
  assumes "wftrm t" "Γ t = TAtom τ"
  shows "(∃v. t = Var v) ∨ (∃f. t = Fun f [])"
using assms const_type_inv unfolding wftrm_def by (cases t) auto

lemma subtermeq_imp_subtermtypeeq:
  assumes "wftrm t" "s ⊑ t"
  shows "Γ s ⊑ Γ t"
using assms(2,1)
proof (induction t)
  case (Fun f T) thus ?case
  proof (cases "s = Fun f T")
    case False
    then obtain x where x: "x ∈ set T" "s ⊑ x" using Fun.prems(1) by auto
    hence "wftrm x" using wf_trm_subtermeq[OF Fun.prems(2)] Fun_param_is_subterm[of _ T f] by auto
    hence "Γ s ⊑ Γ x" using Fun.IH[OF x] by simp
    moreover have "arity f > 0" using x fun_type_inv_wf Fun.prems
      by (metis length_pos_if_in_set term.order_refl wftrm_def)
    ultimately show ?thesis using x Fun.prems fun_type[of f T] by auto
  qed simp
qed simp

lemma subterm_funs_term_in_type:
  assumes "wftrm t" "Fun f T ⊑ t" "Γ (Fun f T) = TComp f (map Γ T)"
  shows "f ∈ funs_term (Γ t)"
using assms(2,1,3)
proof (induction t)
  case (Fun f' T')
  hence [simp]: "wftrm (Fun f T)" by (metis wf_trm_subtermeq)
  { fix a assume τ: "Γ (Fun f' T') = TAtom a"
    hence "Fun f T = Fun f' T'" using Fun TAtom_term_cases subtermeq_Var_const by metis
    hence False using Fun.prems(3) τ by simp
  }
  moreover
  { fix g S assume τ: "Γ (Fun f' T') = TComp g S"
    hence "g = f'" "S = map Γ T'"
      using Fun.prems(2) fun_type_id_eq[OF τ] fun_type[OF fun_type_inv(1)[OF τ]]
      by auto
    hence τ': "Γ (Fun f' T') = TComp f' (map Γ T')" using τ by auto
    hence "g ∈ funs_term (Γ (Fun f' T'))" using τ by auto
    moreover {
      assume "Fun f T ≠ Fun f' T'"
      then obtain x where "x ∈ set T'" "Fun f T ⊑ x" using Fun.prems(1) by auto
      hence "f ∈ funs_term (Γ x)"
        using Fun.IH[OF _ _ _ Fun.prems(3), of x] wf_trm_subtermeq[OF ‹wftrm (Fun f' T')›, of x]
        by force
      moreover have "Γ x ∈ set (map Γ T')" using τ' ‹x ∈ set T'› by auto
      ultimately have "f ∈ funs_term (Γ (Fun f' T'))" using τ' by auto
    }
    ultimately have ?case by (cases "Fun f T = Fun f' T'") (auto simp add: ‹g = f'›)
  }
  ultimately show ?case by (cases "Γ (Fun f' T')") auto
qed simp

lemma wt_subst_fv_termtype_subterm:
  assumes "x ∈ fv (θ y)"
    and "wtsubst θ"
    and "wftrm (θ y)"
  shows "Γ (Var x) ⊑ Γ (Var y)"
using subtermeq_imp_subtermtypeeq[OF assms(3) var_is_subterm[OF assms(1)]]
      wt_subst_trm''[OF assms(2), of "Var y"]
by auto

lemma wt_subst_fvset_termtype_subterm:
  assumes "x ∈ fvset (θ ` Y)"
    and "wtsubst θ"
    and "wftrms (subst_range θ)"
  shows "∃y ∈ Y. Γ (Var x) ⊑ Γ (Var y)"
using wt_subst_fv_termtype_subterm[OF _ assms(2), of x] assms(1,3)
by fastforce

lemma funs_term_type_iff:
  assumes t: "wftrm t"
    and f: "arity f > 0"
  shows "f ∈ funs_term (Γ t) ⟷ (f ∈ funs_term t ∨ (∃x ∈ fv t. f ∈ funs_term (Γ (Var x))))"
    (is "?P t ⟷ ?Q t")
using t
proof (induction t)
  case (Fun g T)
  hence IH: "?P s ⟷ ?Q s" when "s ∈ set T" for s
    using that wf_trm_subterm[OF _ Fun_param_is_subterm]
    by blast
  have 0: "arity g = length T" using Fun.prems unfolding wftrm_def by auto
  show ?case
  proof (cases "f = g")
    case True thus ?thesis using fun_type[OF f] by simp
  next
    case False
    have "?P (Fun g T) ⟷ (∃s ∈ set T. ?P s)"
    proof
      assume *: "?P (Fun g T)"
      hence "Γ (Fun g T) = TComp g (map Γ T)"
        using const_type[of g] fun_type[of g] by force
      thus "∃s ∈ set T. ?P s" using False * by force
    next
      assume *: "∃s ∈ set T. ?P s"
      hence "Γ (Fun g T) = TComp g (map Γ T)"
        using 0 const_type[of g] fun_type[of g] by force
      thus "?P (Fun g T)" using False * by force
    qed
    thus ?thesis using False f IH by auto
  qed
qed simp

lemma funs_term_type_iff':
  assumes M: "wftrms M"
    and f: "arity f > 0"
  shows "f ∈ ⋃(funs_term ` Γ ` M) ⟷
        (f ∈ ⋃(funs_term ` M) ∨ (∃x ∈ fvset M. f ∈ funs_term (Γ (Var x))))" (is "?A ⟷ ?B")
proof
  assume ?A
  then obtain t where "t ∈ M" "wftrm t" "f ∈ funs_term (Γ t)" using M by moura
  thus ?B using funs_term_type_iff[OF _ f, of t] by auto
next
  assume ?B
  then obtain t where "t ∈ M" "wftrm t" "f ∈ funs_term t ∨ (∃x ∈ fv t. f ∈ funs_term (Γ (Var x)))"
    using M by auto
  thus ?A using funs_term_type_iff[OF _ f, of t] by blast
qed

lemma Ana_subterm_type:
  assumes "Ana t = (K,M)"
    and "wftrm t"
    and "m ∈ set M"
  shows "Γ m ⊑ Γ t"
proof -
  have "m ⊑ t" using Ana_subterm[OF assms(1)] assms(3) by auto
  thus ?thesis using subtermeq_imp_subtermtypeeq[OF assms(2)] by simp
qed

lemma wf_trm_TAtom_subterms:
  assumes "wftrm t" "Γ t = TAtom τ"
  shows "subterms t = {t}"
using assms const_type_inv unfolding wftrm_def by (cases t) force+

lemma wf_trm_TComp_subterm:
  assumes "wftrm s" "t ⊏ s"
  obtains f T where "Γ s = TComp f T"
proof (cases s)
  case (Var x) thus ?thesis using ‹t ⊏ s› by simp
next
  case (Fun g S)
  hence "length S > 0" using assms Fun_subterm_inside_params[of t g S] by auto
  hence "arity g > 0" by (metis ‹wftrm s› ‹s = Fun g S› term.order_refl wftrm_def) 
  thus ?thesis using fun_type ‹s = Fun g S› that by auto
qed

lemma SMP_empty[simp]: "SMP {} = {}"
proof (rule ccontr)
  assume "SMP {} ≠ {}"
  then obtain t where "t ∈ SMP {}" by auto
  thus False by (induct t rule: SMP.induct) auto
qed

lemma SMP_I:
  assumes "s ∈ M" "wtsubst δ" "t ⊑ s ⋅ δ" "⋀v. wftrm (δ v)"
  shows "t ∈ SMP M"
using SMP.Substitution[OF SMP.MP[OF assms(1)] assms(2)] SMP.Subterm[of "s ⋅ δ" M t] assms(3,4)
by (cases "t = s ⋅ δ") simp_all

lemma SMP_wf_trm:
  assumes "t ∈ SMP M" "wftrms M"
  shows "wftrm t"
using assms(1)
by (induct t rule: SMP.induct)
   (use assms(2) in blast,
    use wf_trm_subtermeq in blast,
    use wf_trm_subst in blast,
    use Ana_keys_wf' in blast)

lemma SMP_ikI[intro]: "t ∈ ikst S ⟹ t ∈ SMP (trmsst S)" by force

lemma MP_setI[intro]: "x ∈ set S ⟹ trmsstp x ⊆ trmsst S" by force

lemma SMP_setI[intro]: "x ∈ set S ⟹ trmsstp x ⊆ SMP (trmsst S)" by force

lemma SMP_subset_I:
  assumes M: "∀t ∈ M. ∃s δ. s ∈ N ∧ wtsubst δ ∧ wftrms (subst_range δ) ∧ t = s ⋅ δ"
  shows "SMP M ⊆ SMP N"
proof
  fix t show "t ∈ SMP M ⟹ t ∈ SMP N"
  proof (induction t rule: SMP.induct)
    case (MP t)
    then obtain s δ where s: "s ∈ N" "wtsubst δ" "wftrms (subst_range δ)" "t = s ⋅ δ"
      using M by moura
    show ?case using SMP_I[OF s(1,2), of "s ⋅ δ"] s(3,4) wf_trm_subst_range_iff by fast
  qed (auto intro!: SMP.Substitution[of _ N])
qed

lemma SMP_union: "SMP (A ∪ B) = SMP A ∪ SMP B"
proof
  show "SMP (A ∪ B) ⊆ SMP A ∪ SMP B"
  proof
    fix t assume "t ∈ SMP (A ∪ B)"
    thus "t ∈ SMP A ∪ SMP B" by (induct rule: SMP.induct) blast+
  qed

  { fix t assume "t ∈ SMP A" hence "t ∈ SMP (A ∪ B)" by (induct rule: SMP.induct) blast+ }
  moreover { fix t assume "t ∈ SMP B" hence "t ∈ SMP (A ∪ B)" by (induct rule: SMP.induct) blast+ }
  ultimately show "SMP A ∪ SMP B ⊆ SMP (A ∪ B)" by blast
qed

lemma SMP_append[simp]: "SMP (trmsst (S@S')) = SMP (trmsst S) ∪ SMP (trmsst S')" (is "?A = ?B")
using SMP_union by simp

lemma SMP_mono: "A ⊆ B ⟹ SMP A ⊆ SMP B"
proof -
  assume "A ⊆ B"
  then obtain C where "B = A ∪ C" by moura
  thus "SMP A ⊆ SMP B" by (simp add: SMP_union)
qed

lemma SMP_Union: "SMP (⋃m ∈ M. f m) = (⋃m ∈ M. SMP (f m))"
proof
  show "SMP (⋃m∈M. f m) ⊆ (⋃m∈M. SMP (f m))"
  proof
    fix t assume "t ∈ SMP (⋃m∈M. f m)"
    thus "t ∈ (⋃m∈M. SMP (f m))" by (induct t rule: SMP.induct) force+
  qed
  show "(⋃m∈M. SMP (f m)) ⊆ SMP (⋃m∈M. f m)"
  proof
    fix t assume "t ∈ (⋃m∈M. SMP (f m))"
    then obtain m where "m ∈ M" "t ∈ SMP (f m)" by moura
    thus "t ∈ SMP (⋃m∈M. f m)" using SMP_mono[of "f m" "⋃m∈M. f m"] by auto
  qed
qed

lemma SMP_singleton_ex:
  "t ∈ SMP M ⟹ (∃m ∈ M. t ∈ SMP {m})"
  "m ∈ M ⟹ t ∈ SMP {m} ⟹ t ∈ SMP M"
using SMP_Union[of "λt. {t}" M] by auto

lemma SMP_Cons: "SMP (trmsst (x#S)) = SMP (trmsst [x]) ∪ SMP (trmsst S)"
using SMP_append[of "[x]" S] by auto

lemma SMP_Nil[simp]: "SMP (trmsst []) = {}" 
proof -
  { fix t assume "t ∈ SMP (trmsst [])" hence False by induct auto }
  thus ?thesis by blast
qed

lemma SMP_subset_union_eq: assumes "M ⊆ SMP N" shows "SMP N = SMP (M ∪ N)"
proof -
  { fix t assume "t ∈ SMP (M ∪ N)" hence "t ∈ SMP N"
      using assms by (induction rule: SMP.induct) blast+
  }
  thus ?thesis using SMP_union by auto
qed

lemma SMP_subterms_subset: "subtermsset M ⊆ SMP M"
proof
  fix t assume "t ∈ subtermsset M"
  then obtain m where "m ∈ M" "t ⊑ m" by auto
  thus "t ∈ SMP M" using SMP_I[of _ _ Var] by auto
qed

lemma SMP_SMP_subset: "N ⊆ SMP M ⟹ SMP N ⊆ SMP M"
by (metis SMP_mono SMP_subset_union_eq Un_commute Un_upper2)

lemma wt_subst_rm_vars: "wtsubst δ ⟹ wtsubst (rm_vars X δ)"
using rm_vars_dom unfolding wtsubst_def by auto

lemma wt_subst_SMP_subset:
  assumes "trmsst S ⊆ SMP S'" "wtsubst δ" "wftrms (subst_range δ)"
  shows "trmsst (S ⋅st δ) ⊆ SMP S'"
proof
  fix t assume *: "t ∈ trmsst (S ⋅st δ)"
  show "t ∈ SMP S'" using trm_strand_subst_cong(2)[OF *]
  proof
    assume "∃t'. t = t' ⋅ δ ∧ t' ∈ trmsst S"
    thus "t ∈ SMP S'" using assms SMP.Substitution by auto
  next
    assume "∃X F. Inequality X F ∈ set S ∧ (∃t'∈trmspairs F. t = t' ⋅ rm_vars (set X) δ)"
    then obtain X F t' where **:
        "Inequality X F ∈ set S" "t'∈trmspairs F" "t = t' ⋅ rm_vars (set X) δ"
      by force
    then obtain s where s: "s ∈ trmsstp (Inequality X F)" "t = s ⋅ rm_vars (set X) δ" by moura
    hence "s ∈ SMP (trmsst S)" using **(1) by force
    hence "t ∈ SMP (trmsst S)"
      using SMP.Substitution[OF _ wt_subst_rm_vars[OF assms(2)] wf_trms_subst_rm_vars'[OF assms(3)]]
      unfolding s(2) by blast
    thus "t ∈ SMP S'" by (metis SMP_union SMP_subset_union_eq UnCI assms(1))
  qed
qed

lemma MP_subset_SMP: "⋃(trmsstp ` set S) ⊆ SMP (trmsst S)" "trmsst S ⊆ SMP (trmsst S)" "M ⊆ SMP M"
by auto

lemma SMP_fun_map_snd_subset: "SMP (trmsst (map Send1 X)) ⊆ SMP (trmsst [Send1 (Fun f X)])"
proof
  fix t assume "t ∈ SMP (trmsst (map Send1 X))" thus "t ∈ SMP (trmsst [Send1 (Fun f X)])"
  proof (induction t rule: SMP.induct)
    case (MP t)
    hence "t ∈ set X" by auto
    hence "t ⊏ Fun f X" by (metis subtermI')
    thus ?case using SMP.Subterm[of "Fun f X" "trmsst [Send1 (Fun f X)]" t] using SMP.MP by auto
  qed blast+
qed

lemma SMP_wt_subst_subset:
  assumes "t ∈ SMP (M ⋅set ℐ)" "wtsubst ℐ" "wftrms (subst_range ℐ)"
  shows "t ∈ SMP M"
using assms wf_trm_subst_range_iff[of ℐ] by (induct t rule: SMP.induct) blast+

lemma SMP_wt_instances_subset:
  assumes "∀t ∈ M. ∃s ∈ N. ∃δ. t = s ⋅ δ ∧ wtsubst δ ∧ wftrms (subst_range δ)"
    and "t ∈ SMP M"
  shows "t ∈ SMP N"
proof -
  obtain m where m: "m ∈ M" "t ∈ SMP {m}" using SMP_singleton_ex(1)[OF assms(2)] by blast
  then obtain n δ where n: "n ∈ N" "m = n ⋅ δ" "wtsubst δ" "wftrms (subst_range δ)"
    using assms(1) by fast

  have "t ∈ SMP (N ⋅set δ)" using n(1,2) SMP_singleton_ex(2)[of m "N ⋅set δ", OF _ m(2)] by fast
  thus ?thesis using SMP_wt_subst_subset[OF _ n(3,4)] by blast
qed

lemma SMP_consts:
  assumes "∀t ∈ M. ∃c. t = Fun c []"
    and "∀t ∈ M. Ana t = ([], [])"
  shows "SMP M = M"
proof
  show "SMP M ⊆ M"
  proof
    fix t show "t ∈ SMP M ⟹ t ∈ M"
      apply (induction t rule: SMP.induct)
      by (use assms in auto)
  qed
qed auto

lemma SMP_subterms_eq:
  "SMP (subtermsset M) = SMP M"
proof
  show "SMP M ⊆ SMP (subtermsset M)" using SMP_mono[of M "subtermsset M"] by blast
  show "SMP (subtermsset M) ⊆ SMP M"
  proof
    fix t show "t ∈ SMP (subtermsset M) ⟹ t ∈ SMP M" by (induction t rule: SMP.induct) blast+
  qed
qed

lemma SMP_funs_term:
  assumes t: "t ∈ SMP M" "f ∈ funs_term t ∨ (∃x ∈ fv t. f ∈ funs_term (Γ (Var x)))"
    and f: "arity f > 0"
    and M: "wftrms M"
    and Ana_f: "⋀s K T. Ana s = (K,T) ⟹ f ∈ ⋃(funs_term ` set K) ⟹ f ∈ funs_term s"
  shows "f ∈ ⋃(funs_term ` M) ∨ (∃x ∈ fvset M. f ∈ funs_term (Γ (Var x)))"
using t
proof (induction t rule: SMP.induct)
  case (Subterm t t')
  thus ?case by (metis UN_I vars_iff_subtermeq funs_term_subterms_eq(1) term.order_trans)
next
  case (Substitution t δ)
  show ?case
    using M SMP_wf_trm[OF Substitution.hyps(1)] wf_trm_subst[of δ t, OF Substitution.hyps(3)]
          funs_term_type_iff[OF _ f] wt_subst_trm''[OF Substitution.hyps(2), of t]
          Substitution.prems Substitution.IH
    by metis
next
  case (Ana t K T t')
  thus ?case
    using Ana_f[OF Ana.hyps(2)] Ana_keys_fv[OF Ana.hyps(2)]
    by fastforce
qed auto

lemma id_type_eq:
  assumes "Γ (Fun f X) = Γ (Fun g Y)"
  shows "f ∈ 𝒞 ⟹ g ∈ 𝒞" "f ∈ Σf ⟹ g ∈ Σf"
using assms const_type' fun_type' id_union_univ(1)
by (metis UNIV_I UnE "term.distinct"(1))+

lemma fun_type_arg_cong:
  assumes "f ∈ Σf" "g ∈ Σf" "Γ (Fun f (x#X)) = Γ (Fun g (y#Y))"
  shows "Γ x = Γ y" "Γ (Fun f X) = Γ (Fun g Y)"
using assms fun_type' by auto

lemma fun_type_arg_cong':
  assumes "f ∈ Σf" "g ∈ Σf" "Γ (Fun f (X@x#X')) = Γ (Fun g (Y@y#Y'))" "length X = length Y"
  shows "Γ x = Γ y"
using assms
proof (induction X arbitrary: Y)
  case Nil thus ?case using fun_type_arg_cong(1)[of f g x X' y Y'] by auto
next
  case (Cons x' X Y'')
  then obtain y' Y where "Y'' = y'#Y" by (metis length_Suc_conv)
  hence "Γ (Fun f (X@x#X')) = Γ (Fun g (Y@y#Y'))" "length X = length Y"
    using Cons.prems(3,4) fun_type_arg_cong(2)[OF Cons.prems(1,2), of x' "X@x#X'"] by auto
  thus ?thesis using Cons.IH[OF Cons.prems(1,2)] by auto
qed

lemma fun_type_param_idx: "Γ (Fun f T) = Fun g S ⟹ i < length T ⟹ Γ (T ! i) = S ! i"
by (metis fun_type fun_type_id_eq fun_type_inv(1) nth_map term.inject(2))

lemma fun_type_param_ex:
  assumes "Γ (Fun f T) = Fun g (map Γ S)" "t ∈ set S"
  shows "∃s ∈ set T. Γ s = Γ t"
using fun_type_length_eq[OF assms(1)] length_map[of Γ S] assms(2)
      fun_type_param_idx[OF assms(1)] nth_map in_set_conv_nth
by metis

lemma tfr_stp_all_split:
  "list_all tfrstp (x#S) ⟹ list_all tfrstp [x]"
  "list_all tfrstp (x#S) ⟹ list_all tfrstp S"
  "list_all tfrstp (S@S') ⟹ list_all tfrstp S"
  "list_all tfrstp (S@S') ⟹ list_all tfrstp S'"
  "list_all tfrstp (S@x#S') ⟹ list_all tfrstp (S@S')"
by fastforce+

lemma tfr_stp_all_append:
  assumes "list_all tfrstp S" "list_all tfrstp S'"
  shows "list_all tfrstp (S@S')"
using assms by fastforce

lemma tfr_stp_all_wt_subst_apply:
  assumes "list_all tfrstp S"
    and θ: "wtsubst θ" "wftrms (subst_range θ)"
           "bvarsst S ∩ range_vars θ = {}"
  shows "list_all tfrstp (S ⋅st θ)"
using assms(1,4)
proof (induction S)
  case (Cons x S)
  hence IH: "list_all tfrstp (S ⋅st θ)"
    using tfr_stp_all_split(2)[of x S]
    unfolding range_vars_alt_def by fastforce
  thus ?case
  proof (cases x)
    case (Equality a t t')
    hence "(∃δ. Unifier δ t t') ⟶ Γ t = Γ t'" using Cons.prems by auto
    hence "(∃δ. Unifier δ (t ⋅ θ) (t' ⋅ θ)) ⟶ Γ (t ⋅ θ) = Γ (t' ⋅ θ)"
      by (metis Unifier_comp' wt_subst_trm'[OF assms(2)])
    moreover have "(x#S) ⋅st θ = Equality a (t ⋅ θ) (t' ⋅ θ)#(S ⋅st θ)"
      using ‹x = Equality a t t'› by auto
    ultimately show ?thesis using IH by auto
  next
    case (Inequality X F)
    let ?σ = "rm_vars (set X) θ"
    let ?G = "F ⋅pairs ?σ"

    let ?P = "λF X. ∀x ∈ fvpairs F - set X. ∃a. Γ (Var x) = TAtom a"
    let ?Q = "λF X.
      ∀f T. Fun f T ∈ subtermsset (trmspairs F) ⟶ T = [] ∨ (∃s ∈ set T. s ∉ Var ` set X)"

    have 0: "set X ∩ range_vars ?σ = {}"
      using Cons.prems(2) Inequality rm_vars_img_subset[of "set X"]
      by (auto simp add: subst_domain_def range_vars_alt_def)

    have 1: "?P F X ∨ ?Q F X" using Inequality Cons.prems by simp

    have 2: "fvset (?σ ` set X) = set X" by auto

    have "?P ?G X" when "?P F X" using that
    proof (induction F)
      case (Cons g G)
      obtain t t' where g: "g = (t,t')" by (metis surj_pair)
      
      have "∀x ∈ (fv (t ⋅ ?σ) ∪ fv (t' ⋅ ?σ)) - set X. ∃a. Γ (Var x) = Var a"
      proof -
        have *: "∀x ∈ fv t - set X. ∃a. Γ (Var x) = Var a"
               "∀x ∈ fv t' - set X. ∃a. Γ (Var x) = Var a"
          using g Cons.prems by simp_all

        have **: "∀x. wftrm (?σ x)"
          using θ(2) wf_trm_subst_range_iff[of θ] wf_trm_subst_rm_vars'[of θ _ "set X"] by simp

        show ?thesis
          using wt_subst_TAtom_fv[OF wt_subst_rm_vars[OF θ(1)] ** *(1)]
                wt_subst_TAtom_fv[OF wt_subst_rm_vars[OF θ(1)] ** *(2)]
                wt_subst_trm'[OF wt_subst_rm_vars[OF θ(1), of "set X"]] 2
          by blast
      qed
      moreover have "∀x∈fvpairs (G ⋅pairs ?σ) - set X. ∃a. Γ (Var x) = Var a"
        using Cons by auto
      ultimately show ?case using g by (auto simp add: subst_apply_pairs_def)
    qed (simp add: subst_apply_pairs_def)
    hence "?P ?G X ∨ ?Q ?G X"
      using 1 ineq_subterm_inj_cond_subst[OF 0, of "trmspairs F"] trmspairs_subst[of F ?σ]
      by presburger
    moreover have "(x#S) ⋅st θ = Inequality X (F ⋅pairs ?σ)#(S ⋅st θ)"
      using ‹x = Inequality X F› by auto
    ultimately show ?thesis using IH by simp
  qed auto
qed simp

lemma tfr_stp_all_same_type:
  "list_all tfrstp (S@Equality a t t'#S') ⟹ Unifier δ t t' ⟹ Γ t = Γ t'"
by force+

lemma tfr_subset:
  "⋀A B. tfrset (A ∪ B) ⟹ tfrset A"
  "⋀A B. tfrset B ⟹ A ⊆ B ⟹ tfrset A"
  "⋀A B. tfrset B ⟹ SMP A ⊆ SMP B ⟹ tfrset A"
proof -
  show 1: "tfrset (A ∪ B) ⟹ tfrset A" for A B
    using SMP_union[of A B] unfolding tfrset_def by simp

  fix A B assume B: "tfrset B"

  show "A ⊆ B ⟹ tfrset A"
  proof -
    assume "A ⊆ B"
    then obtain C where "B = A ∪ C" by moura
    thus ?thesis using B 1 by blast
  qed

  show "SMP A ⊆ SMP B ⟹ tfrset A"
  proof -
    assume "SMP A ⊆ SMP B"
    then obtain C where "SMP B = SMP A ∪ C" by moura
    thus ?thesis using B unfolding tfrset_def by blast
  qed
qed

lemma tfr_empty[simp]: "tfrset {}"
unfolding tfrset_def by simp

lemma tfr_consts_mono:
  assumes "∀t ∈ M. ∃c. t = Fun c []"
    and "∀t ∈ M. Ana t = ([], [])"
    and "tfrset N"
  shows "tfrset (N ∪ M)"
proof -
  { fix s t
    assume *: "s ∈ SMP (N ∪ M) - range Var" "t ∈ SMP (N ∪ M) - range Var" "∃δ. Unifier δ s t"
    hence **: "is_Fun s" "is_Fun t" "s ∈ SMP N ∨ s ∈ M" "t ∈ SMP N ∨ t ∈ M"
      using assms(3) SMP_consts[OF assms(1,2)] SMP_union[of N M] by auto
    moreover have "Γ s = Γ t" when "s ∈ SMP N" "t ∈ SMP N"
      using that assms(3) *(3) **(1,2) unfolding tfrset_def by blast
    moreover have "Γ s = Γ t" when st: "s ∈ M" "t ∈ M"
    proof -
      obtain c d where "s = Fun c []" "t = Fun d []" using st assms(1) by moura
      hence "s = t" using *(3) by fast
      thus ?thesis by metis
    qed
    moreover have "Γ s = Γ t" when st: "s ∈ SMP N" "t ∈ M"
    proof -
      obtain c where "t = Fun c []" using st assms(1) by moura
      hence "s = t" using *(3) **(1,2) by auto
      thus ?thesis by metis
    qed
    moreover have "Γ s = Γ t" when st: "s ∈ M" "t ∈ SMP N"
    proof -
      obtain c where "s = Fun c []" using st assms(1) by moura
      hence "s = t" using *(3) **(1,2) by auto
      thus ?thesis by metis
    qed
    ultimately have "Γ s = Γ t" by metis
  } thus ?thesis by (metis tfrset_def)
qed

lemma dualst_tfrstp: "list_all tfrstp S ⟹ list_all tfrstp (dualst S)"
proof (induction S)
  case (Cons x S)
  have "list_all tfrstp S" using Cons.prems by simp
  hence IH: "list_all tfrstp (dualst S)" using Cons.IH by metis
  from Cons show ?case
  proof (cases x)
    case (Equality a t t')
    hence "(∃δ. Unifier δ t t') ⟹ Γ t = Γ t'" using Cons by auto
    thus ?thesis using Equality IH by fastforce
  next
    case (Inequality X F)
    have "set (dualst (x#S)) = insert x (set (dualst S))" using Inequality by auto
    moreover have "(∀x ∈ fvpairs F - set X. ∃a. Γ (Var x) = Var a) ∨
            (∀f T. Fun f T ∈ subtermsset (trmspairs F) ⟶ T = [] ∨ (∃s ∈ set T. s ∉ Var ` set X))" 
      using Cons.prems Inequality by auto
    ultimately show ?thesis using Inequality IH by auto
  qed auto
qed simp

lemma subst_var_inv_wt:
  assumes "wtsubst δ"
  shows "wtsubst (subst_var_inv δ X)"
using assms f_inv_into_f[of _ δ X]
unfolding wtsubst_def subst_var_inv_def
by presburger

lemma subst_var_inv_wf_trms:
  "wftrms (subst_range (subst_var_inv δ X))"
using f_inv_into_f[of _ δ X]
unfolding wtsubst_def subst_var_inv_def
by auto

lemma unify_list_wt_if_same_type:
  assumes "Unification.unify E B = Some U" "∀(s,t) ∈ set E. wftrm s ∧ wftrm t ∧ Γ s = Γ t"
  and "∀(v,t) ∈ set B. Γ (Var v) = Γ t"
  shows "∀(v,t) ∈ set U. Γ (Var v) = Γ t"
using assms
proof (induction E B arbitrary: U rule: Unification.unify.induct)
  case (2 f X g Y E B U)
  hence "wftrm (Fun f X)" "wftrm (Fun g Y)" "Γ (Fun f X) = Γ (Fun g Y)" by auto

  from "2.prems"(1) obtain E' where *: "decompose (Fun f X) (Fun g Y) = Some E'"
    and [simp]: "f = g" "length X = length Y" "E' = zip X Y"
    and **: "Unification.unify (E'@E) B = Some U"
    by (auto split: option.splits)
  
  have "∀(s,t) ∈ set E'. wftrm s ∧ wftrm t ∧ Γ s = Γ t"
  proof -
    { fix s t assume "(s,t) ∈ set E'"
      then obtain X' X'' Y' Y'' where "X = X'@s#X''" "Y = Y'@t#Y''" "length X' = length Y'"
        using zip_arg_subterm_split[of s t X Y] ‹E' = zip X Y› by metis
      hence "Γ (Fun f (X'@s#X'')) = Γ (Fun g (Y'@t#Y''))" by (metis ‹Γ (Fun f X) = Γ (Fun g Y)›)
      
      from ‹E' = zip X Y› have "∀(s,t) ∈ set E'. s ⊏ Fun f X ∧ t ⊏ Fun g Y"
        using zip_arg_subterm[of _ _ X Y] by blast
      with ‹(s,t) ∈ set E'› have "wftrm s" "wftrm t"
        using wf_trm_subterm ‹wftrm (Fun f X)› ‹wftrm (Fun g Y)› by (blast,blast)
      moreover have "f ∈ Σf"
      proof (rule ccontr)
        assume "f ∉ Σf"
        hence "f ∈ 𝒞" "arity f = 0" using const_arity_eq_zero[of f] by simp_all
        thus False using ‹wftrm (Fun f X)› * ‹(s,t) ∈ set E'› unfolding wftrm_def by auto
      qed
      hence "Γ s = Γ t"
        using fun_type_arg_cong' ‹f ∈ Σf› ‹Γ (Fun f (X'@s#X'')) = Γ (Fun g (Y'@t#Y''))›
              ‹length X' = length Y'› ‹f = g›
        by metis
      ultimately have "wftrm s" "wftrm t" "Γ s = Γ t" by metis+
    }
    thus ?thesis by blast
  qed
  moreover have "∀(s,t) ∈ set E. wftrm s ∧ wftrm t ∧ Γ s = Γ t" using "2.prems"(2) by auto
  ultimately show ?case using "2.IH"[OF * ** _ "2.prems"(3)] by fastforce
next
  case (3 v t E B U)
  hence "Γ (Var v) = Γ t" "wftrm t" by auto
  hence "wtsubst (subst v t)"
      and *: "∀(v, t) ∈ set ((v,t)#B). Γ (Var v) = Γ t"
             "⋀t t'. (t,t') ∈ set E ⟹ Γ t = Γ t'"
    using "3.prems"(2,3) unfolding wtsubst_def subst_def by auto

  show ?case
  proof (cases "t = Var v")
    assume "t = Var v" thus ?case using 3 by auto
  next
    assume "t ≠ Var v"
    hence "v ∉ fv t" using "3.prems"(1) by auto
    hence **: "Unification.unify (subst_list (subst v t) E) ((v, t)#B) = Some U"
      using Unification.unify.simps(3)[of v t E B] "3.prems"(1) ‹t ≠ Var v› by auto
    
    have "∀(s, t) ∈ set (subst_list (subst v t) E). wftrm s ∧ wftrm t"
      using wf_trm_subst_singleton[OF _ ‹wftrm t›] "3.prems"(2)
      unfolding subst_list_def subst_def by auto
    moreover have "∀(s, t) ∈ set (subst_list (subst v t) E). Γ s = Γ t"
      using *(2)[THEN wt_subst_trm'[OF ‹wtsubst (subst v t)›]] by (simp add: subst_list_def)
    ultimately show ?thesis using "3.IH"(2)[OF ‹t ≠ Var v› ‹v ∉ fv t› ** _ *(1)] by auto
  qed
next
  case (4 f X v E B U)
  hence "Γ (Var v) = Γ (Fun f X)" "wftrm (Fun f X)" by auto
  hence "wtsubst (subst v (Fun f X))"
      and *: "∀(v, t) ∈ set ((v,(Fun f X))#B). Γ (Var v) = Γ t"
             "⋀t t'. (t,t') ∈ set E ⟹ Γ t = Γ t'"
    using "4.prems"(2,3) unfolding wtsubst_def subst_def by auto

  have "v ∉ fv (Fun f X)" using "4.prems"(1) by force
  hence **: "Unification.unify (subst_list (subst v (Fun f X)) E) ((v, (Fun f X))#B) = Some U"
    using Unification.unify.simps(3)[of v "Fun f X" E B] "4.prems"(1) by auto
  
  have "∀(s, t) ∈ set (subst_list (subst v (Fun f X)) E). wftrm s ∧ wftrm t"
    using wf_trm_subst_singleton[OF _ ‹wftrm (Fun f X)›] "4.prems"(2)
    unfolding subst_list_def subst_def by auto
  moreover have "∀(s, t) ∈ set (subst_list (subst v (Fun f X)) E). Γ s = Γ t"
    using *(2)[THEN wt_subst_trm'[OF ‹wtsubst (subst v (Fun f X))›]] by (simp add: subst_list_def)
  ultimately show ?case using "4.IH"[OF ‹v ∉ fv (Fun f X)› ** _ *(1)] by auto
qed auto

lemma mgu_wt_if_same_type:
  assumes "mgu s t = Some σ" "wftrm s" "wftrm t" "Γ s = Γ t"
  shows "wtsubst σ"
proof -
  let ?fv_disj = "λv t S. ¬(∃(v',t') ∈ S - {(v,t)}. (insert v (fv t)) ∩ (insert v' (fv t')) ≠ {})"

  from assms(1) obtain σ' where "Unification.unify [(s,t)] [] = Some σ'" "subst_of σ' = σ"
    by (auto simp: mgu_def split: option.splits)
  hence "∀(v,t) ∈ set σ'. Γ (Var v) = Γ t" "distinct (map fst σ')"
    using assms(2,3,4) unify_list_wt_if_same_type unify_list_distinct[of "[(s,t)]"] by auto
  thus "wtsubst σ" using ‹subst_of σ' = σ› unfolding wtsubst_def
  proof (induction σ' arbitrary: σ rule: List.rev_induct)
    case (snoc tt σ' σ)
    then obtain v t where tt: "tt = (v,t)" by (metis surj_pair)
    hence σ: "σ = subst v t ∘s subst_of σ'" using snoc.prems(3) by simp
    
    have "∀(v,t) ∈ set σ'. Γ (Var v) = Γ t" "distinct (map fst σ')" using snoc.prems(1,2) by auto
    then obtain σ'' where σ'': "subst_of σ' = σ''" "∀v. Γ (Var v) = Γ (σ'' v)" by (metis snoc.IH)
    hence "Γ t = Γ (t ⋅ σ'')" for t using wt_subst_trm by blast
    hence "Γ (Var v) = Γ (σ'' v)" "Γ t = Γ (t ⋅ σ'')" using σ''(2) by auto
    moreover have "Γ (Var v) = Γ t" using snoc.prems(1) tt by simp
    moreover have σ2: "σ = Var(v := t) ∘s σ'' " using σ σ''(1) unfolding subst_def by simp
    ultimately have "Γ (Var v) = Γ (σ v)" unfolding subst_compose_def by simp

    have "subst_domain (subst v t) ⊆ {v}" unfolding subst_def by (auto simp add: subst_domain_def)
    hence *: "subst_domain σ ⊆ insert v (subst_domain σ'')"
      using tt σ σ''(1) snoc.prems(2) subst_domain_compose[of _ σ'']
      by (auto simp add: subst_domain_def)
    
    have "v ∉ set (map fst σ')" using tt snoc.prems(2) by auto
    hence "v ∉ subst_domain σ''" using σ''(1) subst_of_dom_subset[of σ'] by auto

    { fix w assume "w ∈ subst_domain σ''"
      hence "σ w = σ'' w" using σ2 σ''(1) ‹v ∉ subst_domain σ''› unfolding subst_compose_def by auto
      hence "Γ (Var w) = Γ (σ w)" using σ''(2) by simp
    }
    thus ?case using ‹Γ (Var v) = Γ (σ v)› * by force
  qed simp
qed

lemma wt_Unifier_if_Unifier:
  assumes s_t: "wftrm s" "wftrm t" "Γ s = Γ t"
    and δ: "Unifier δ s t"
  shows "∃θ. Unifier θ s t ∧ wtsubst θ ∧ wftrms (subst_range θ)"
using mgu_always_unifies[OF δ] mgu_gives_MGU[THEN MGU_is_Unifier[of s _ t]]
      mgu_wt_if_same_type[OF _ s_t] mgu_wf_trm[OF _ s_t(1,2)] wf_trm_subst_range_iff
by fast

end


subsection ‹Automatically Proving Type-Flaw Resistance›
subsubsection ‹Definitions: Variable Renaming›
abbreviation "max_var t ≡ Max (insert 0 (snd ` fv t))"
abbreviation "max_var_set X ≡ Max (insert 0 (snd ` X))"

definition "var_rename n v ≡ Var (fst v, snd v + Suc n)"
definition "var_rename_inv n v ≡ Var (fst v, snd v - Suc n)"


subsubsection ‹Definitions: Computing a Finite Representation of the Sub-Message Patterns›
text ‹A sufficient requirement for a term to be a well-typed instance of another term›
definition is_wt_instance_of_cond where
  "is_wt_instance_of_cond Γ t s ≡ (
    Γ t = Γ s ∧ (case mgu t s of
      None ⇒ False
    | Some δ ⇒ inj_on δ (fv t) ∧ (∀x ∈ fv t. is_Var (δ x))))"

definition has_all_wt_instances_of where
  "has_all_wt_instances_of Γ N M ≡ ∀t ∈ N. ∃s ∈ M. is_wt_instance_of_cond Γ t s"

text ‹This function computes a finite representation of the set of sub-message patterns›
definition SMP0 where
  "SMP0 Ana Γ M ≡ let
      f = λt. Fun (the_Fun (Γ t)) (map Var (zip (args (Γ t)) [0..<length (args (Γ t))]));
      g = λM'. map f (filter (λt. is_Var t ∧ is_Fun (Γ t)) M')@
               concat (map (fst ∘ Ana) M')@concat (map subterms_list M');
      h = remdups ∘ g
    in while (λA. set (h A) ≠ set A) h M"

text ‹These definitions are useful to refine an SMP representation set›
fun generalize_term where
  "generalize_term _ _ n (Var x) = (Var x, n)"
| "generalize_term Γ p n (Fun f T) = (let τ = Γ (Fun f T)
    in if p τ then (Var (τ, n), Suc n)
       else let (T',n') = foldr (λt (S,m). let (t',m') = generalize_term Γ p m t in (t'#S,m'))
                                T ([],n)
            in (Fun f T', n'))"

definition generalize_terms where
  "generalize_terms Γ p ≡ map (fst ∘ generalize_term Γ p 0)"

definition remove_superfluous_terms where
  "remove_superfluous_terms Γ T ≡
    let
      f = λS t R. ∃s ∈ set S - R. s ≠ t ∧ is_wt_instance_of_cond Γ t s;
      g = λS t (U,R). if f S t R then (U, insert t R) else (t#U, R);
      h = λS. remdups (fst (foldr (g S) S ([],{})))
    in while (λS. h S ≠ S) h T"


subsubsection ‹Definitions: Checking Type-Flaw Resistance›
definition is_TComp_var_instance_closed where
  "is_TComp_var_instance_closed Γ M ≡ ∀x ∈ fvset M. is_Fun (Γ (Var x)) ⟶
      (∃t ∈ M. is_Fun t ∧ Γ t = Γ (Var x) ∧ list_all is_Var (args t) ∧ distinct (args t))"

definition finite_SMP_representation where
  "finite_SMP_representation arity Ana Γ M ≡
    (M = {} ∨ card M > 0) ∧
    wftrms' arity M ∧
    has_all_wt_instances_of Γ (subtermsset M) M ∧
    has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M ∧
    is_TComp_var_instance_closed Γ M"

definition comp_tfrset where
  "comp_tfrset arity Ana Γ M ≡
    finite_SMP_representation arity Ana Γ M ∧
    (let δ = var_rename (max_var_set (fvset M))
     in ∀s ∈ M. ∀t ∈ M. is_Fun s ∧ is_Fun t ∧ Γ s ≠ Γ t ⟶ mgu s (t ⋅ δ) = None)"

fun comp_tfrstp where
  "comp_tfrstp Γ (⟨_: t ≐ t'⟩st) = (mgu t t' ≠ None ⟶ Γ t = Γ t')"
| "comp_tfrstp Γ (∀X⟨∨≠: F⟩st) = (
    (∀x ∈ fvpairs F - set X. is_Var (Γ (Var x))) ∨
    (∀u ∈ subtermsset (trmspairs F).
      is_Fun u ⟶ (args u = [] ∨ (∃s ∈ set (args u). s ∉ Var ` set X))))"
| "comp_tfrstp _ _ = True"

definition comp_tfrst where
  "comp_tfrst arity Ana Γ M S ≡
    list_all (comp_tfrstp Γ) S ∧
    list_all (wftrm' arity) (trms_listst S) ∧
    has_all_wt_instances_of Γ (trmsst S) M ∧
    comp_tfrset arity Ana Γ M"


subsubsection ‹Small Lemmata›
lemma max_var_set_mono:
  assumes "finite N"
    and "M ⊆ N"
  shows "max_var_set M ≤ max_var_set N"
by (meson assms Max.subset_imp finite.insertI finite_imageI image_mono insert_mono insert_not_empty) 

lemma less_Suc_max_var_set:
  assumes z: "z ∈ X"
    and X: "finite X"
  shows "snd z < Suc (max_var_set X)"
proof -
  have "snd z ∈ snd ` X" using z by simp
  hence "snd z ≤ Max (insert 0 (snd ` X))" using X by simp
  thus ?thesis using X by simp
qed

lemma (in typed_model) finite_SMP_representationD:
  assumes "finite_SMP_representation arity Ana Γ M"
  shows "wftrms M"
    and "has_all_wt_instances_of Γ (subtermsset M) M"
    and "has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
    and "is_TComp_var_instance_closed Γ M"
    and "finite M"
using assms wftrms_code[of M] unfolding finite_SMP_representation_def list_all_iff card_gt_0_iff
by blast+

lemma (in typed_model) is_wt_instance_of_condD:
  assumes t_instance_s: "is_wt_instance_of_cond Γ t s"
  obtains δ where
    "Γ t = Γ s" "mgu t s = Some δ"
    "inj_on δ (fv t)" "δ ` (fv t) ⊆ range Var"
using t_instance_s unfolding is_wt_instance_of_cond_def Let_def by (cases "mgu t s") fastforce+

lemma (in typed_model) is_wt_instance_of_condD':
  assumes t_wf_trm: "wftrm t"
    and s_wf_trm: "wftrm s"
    and t_instance_s: "is_wt_instance_of_cond Γ t s"
  shows "∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ t = s ⋅ δ"
proof -
  obtain δ where s:
      "Γ t = Γ s" "mgu t s = Some δ"
      "inj_on δ (fv t)" "δ ` (fv t) ⊆ range Var"
    by (metis is_wt_instance_of_condD[OF t_instance_s])

  have 0: "wftrm t" "wftrm s" using s(1) t_wf_trm s_wf_trm by auto

  note 1 = mgu_wt_if_same_type[OF s(2) 0 s(1)]

  note 2 = conjunct1[OF mgu_gives_MGU[OF s(2)]]

  show ?thesis
    using s(1) inj_var_ran_unifiable_has_subst_match[OF 2 s(3,4)]
          wt_subst_compose[OF 1 subst_var_inv_wt[OF 1, of "fv t"]]
          wf_trms_subst_compose[OF mgu_wf_trms[OF s(2) 0] subst_var_inv_wf_trms[of δ "fv t"]]
    by auto
qed

lemma (in typed_model) is_wt_instance_of_condD'':
  assumes s_wf_trm: "wftrm s"
    and t_instance_s: "is_wt_instance_of_cond Γ t s"
    and t_var: "t = Var x"
  shows "∃y. s = Var y ∧ Γ (Var y) = Γ (Var x)"
proof -
  obtain δ where δ: "wtsubst δ" and s: "Var x = s ⋅ δ"
    using is_wt_instance_of_condD'[OF _ s_wf_trm t_instance_s] t_var by auto
  obtain y where y: "s = Var y" using s by (cases s) auto
  show ?thesis using wt_subst_trm''[OF δ] s y by metis
qed

lemma (in typed_model) has_all_wt_instances_ofD:
  assumes N_instance_M: "has_all_wt_instances_of Γ N M"
    and t_in_N: "t ∈ N"
  obtains s δ where
    "s ∈ M" "Γ t = Γ s" "mgu t s = Some δ"
    "inj_on δ (fv t)" "δ ` (fv t) ⊆ range Var"
by (metis t_in_N N_instance_M is_wt_instance_of_condD has_all_wt_instances_of_def)

lemma (in typed_model) has_all_wt_instances_ofD':
  assumes N_wf_trms: "wftrms N"
    and M_wf_trms: "wftrms M"
    and N_instance_M: "has_all_wt_instances_of Γ N M"
    and t_in_N: "t ∈ N"
  shows "∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ t ∈ M ⋅set δ"
using assms is_wt_instance_of_condD' unfolding has_all_wt_instances_of_def by fast

lemma (in typed_model) has_all_wt_instances_ofD'':
  assumes N_wf_trms: "wftrms N"
    and M_wf_trms: "wftrms M"
    and N_instance_M: "has_all_wt_instances_of Γ N M"
    and t_in_N: "Var x ∈ N"
  shows "∃y. Var y ∈ M ∧ Γ (Var y) = Γ (Var x)"
using assms is_wt_instance_of_condD'' unfolding has_all_wt_instances_of_def by fast
  
lemma (in typed_model) has_all_instances_of_if_subset:
  assumes "N ⊆ M"
  shows "has_all_wt_instances_of Γ N M"
unfolding has_all_wt_instances_of_def
proof
  fix t assume t: "t ∈ N"
  hence "is_wt_instance_of_cond Γ t t"
    using inj_onI[of "fv t"] mgu_same_empty[of t]
    unfolding is_wt_instance_of_cond_def by force
  thus "∃s ∈ M. is_wt_instance_of_cond Γ t s" using t assms by blast
qed

lemma (in typed_model) SMP_I':
  assumes N_wf_trms: "wftrms N"
    and M_wf_trms: "wftrms M"
    and N_instance_M: "has_all_wt_instances_of Γ N M"
    and t_in_N: "t ∈ N"
  shows "t ∈ SMP M"
using has_all_wt_instances_ofD'[OF N_wf_trms M_wf_trms N_instance_M t_in_N]
      SMP.Substitution[OF SMP.MP[of _ M]]
by blast


subsubsection ‹Lemma: Proving Type-Flaw Resistance›
locale typed_model' = typed_model arity public Ana Γ
  for arity::"'fun ⇒ nat"
    and public::"'fun ⇒ bool"
    and Ana::"('fun,(('fun,'atom::finite) term_type × nat)) term
              ⇒ (('fun,(('fun,'atom) term_type × nat)) term list
                 × ('fun,(('fun,'atom) term_type × nat)) term list)"
    and Γ::"('fun,(('fun,'atom) term_type × nat)) term ⇒ ('fun,'atom) term_type"
  +
  assumes Γ_Var_fst: "⋀τ n m. Γ (Var (τ,n)) = Γ (Var (τ,m))"
    and Ana_const: "⋀c T. arity c = 0 ⟹ Ana (Fun c T) = ([],[])"
    and Ana_subst'_or_Ana_keys_subterm:
      "(∀f T δ K R. Ana (Fun f T) = (K,R) ⟶ Ana (Fun f T ⋅ δ) = (K ⋅list δ,R ⋅list δ)) ∨
       (∀t K R k. Ana t = (K,R) ⟶ k ∈ set K ⟶ k ⊏ t)"
begin

lemma var_rename_inv_comp: "t ⋅ (var_rename n ∘s var_rename_inv n) = t"
proof (induction t)
  case (Fun f T)
  hence "map (λt. t ⋅ var_rename n ∘s var_rename_inv n) T = T" by (simp add: map_idI) 
  thus ?case by (metis eval_term.simps(2)) 
qed (simp add: var_rename_def var_rename_inv_def subst_compose)

lemma var_rename_fv_disjoint:
  "fv s ∩ fv (t ⋅ var_rename (max_var s)) = {}"
proof -
  have 1: "∀v ∈ fv s. snd v ≤ max_var s" by simp
  have 2: "∀v ∈ fv (t ⋅ var_rename n). snd v > n" for n unfolding var_rename_def by (induct t) auto
  show ?thesis using 1 2 by force
qed

lemma var_rename_fv_set_disjoint:
  assumes "finite M" "s ∈ M"
  shows "fv s ∩ fv (t ⋅ var_rename (max_var_set (fvset M))) = {}"
proof -
  have 1: "∀v ∈ fv s. snd v ≤ max_var_set (fvset M)" using assms
  proof (induction M rule: finite_induct)
    case (insert t M) thus ?case
    proof (cases "t = s")
      case False
      hence "∀v ∈ fv s. snd v ≤ max_var_set (fvset M)" using insert by simp
      moreover have "max_var_set (fvset M) ≤ max_var_set (fvset (insert t M))"
        using insert.hyps(1) insert.prems
        by force
      ultimately show ?thesis by auto
    qed simp
  qed simp

  have 2: "∀v ∈ fv (t ⋅ var_rename n). snd v > n" for n unfolding var_rename_def by (induct t) auto

  show ?thesis using 1 2 by force
qed

lemma var_rename_fv_set_disjoint':
  assumes "finite M"
  shows "fvset M ∩ fvset (N ⋅set var_rename (max_var_set (fvset M))) = {}"
using var_rename_fv_set_disjoint[OF assms] by auto

lemma var_rename_is_renaming[simp]:
  "subst_range (var_rename n) ⊆ range Var"
  "subst_range (var_rename_inv n) ⊆ range Var"
unfolding var_rename_def var_rename_inv_def by auto

lemma var_rename_wt[simp]:
  "wtsubst (var_rename n)"
  "wtsubst (var_rename_inv n)"
by (auto simp add: var_rename_def var_rename_inv_def wtsubst_def Γ_Var_fst)

lemma var_rename_wt':
  assumes "wtsubst δ" "s = m ⋅ δ"
  shows "wtsubst (var_rename_inv n ∘s δ)" "s = m ⋅ var_rename n ⋅ var_rename_inv n ∘s δ"
using assms(2) wt_subst_compose[OF var_rename_wt(2)[of n] assms(1)] var_rename_inv_comp[of m n]
by force+

lemma var_rename_wftrms_range[simp]:
  "wftrms (subst_range (var_rename n))"
  "wftrms (subst_range (var_rename_inv n))"
using var_rename_is_renaming by fastforce+

lemma Fun_range_case:
  "(∀f T. Fun f T ∈ M ⟶ P f T) ⟷ (∀u ∈ M. case u of Fun f T ⇒ P f T | _ ⇒ True)"
  "(∀f T. Fun f T ∈ M ⟶ P f T) ⟷ (∀u ∈ M. is_Fun u ⟶ P (the_Fun u) (args u))"
by (auto split: "term.splits")

lemma is_TComp_var_instance_closedD:
  assumes x: "∃y ∈ fvset M. Γ (Var x) = Γ (Var y)" "Γ (Var x) = TComp f T"
    and closed: "is_TComp_var_instance_closed Γ M"
  shows "∃g U. Fun g U ∈ M ∧ Γ (Fun g U) = Γ (Var x) ∧ (∀u ∈ set U. is_Var u) ∧ distinct U"
using assms unfolding is_TComp_var_instance_closed_def list_all_iff list_ex_iff by fastforce

lemma is_TComp_var_instance_closedD':
  assumes "∃y ∈ fvset M. Γ (Var x) = Γ (Var y)" "TComp f T ⊑ Γ (Var x)"
    and closed: "is_TComp_var_instance_closed Γ M"
    and wf: "wftrms M"
  shows "∃g U. Fun g U ∈ M ∧ Γ (Fun g U) = TComp f T ∧ (∀u ∈ set U. is_Var u) ∧ distinct U"
using assms(1,2)
proof (induction "Γ (Var x)" arbitrary: x)
  case (Fun g U)
  note IH = Fun.hyps(1)
  have g: "arity g > 0" using Fun.hyps(2) fun_type_inv[of "Var x"] Γ_Var_fst by simp_all
  then obtain V where V:
      "Fun g V ∈ M" "Γ (Fun g V) = Γ (Var x)" "∀v ∈ set V. ∃x. v = Var x"
      "distinct V" "length U = length V"
    using is_TComp_var_instance_closedD[OF Fun.prems(1) Fun.hyps(2)[symmetric] closed(1)]
    by (metis Fun.hyps(2) fun_type_id_eq fun_type_length_eq is_VarE)
  hence U: "U = map Γ V" using fun_type[OF g(1), of V] Fun.hyps(2) by simp
  hence 1: "Γ v ∈ set U" when v: "v ∈ set V" for v using v by simp

  have 2: "∃y ∈ fvset M. Γ (Var z) = Γ (Var y)" when z: "Var z ∈ set V" for z
    using V(1) fv_subset_subterms Fun_param_in_subterms[OF z] by fastforce

  show ?case
  proof (cases "TComp f T = Γ (Var x)")
    case False
    then obtain u where u: "u ∈ set U" "TComp f T ⊑ u"
      using Fun.prems(2) Fun.hyps(2) by moura
    then obtain y where y: "Var y ∈ set V" "Γ (Var y) = u" using U V(3) Γ_Var_fst by auto
    show ?thesis using IH[OF _ 2[OF y(1)]] u y(2) by metis
  qed (use V in fastforce)
qed simp

lemma TComp_var_instance_wt_subst_exists:
  assumes gT: "Γ (Fun g T) = TComp g (map Γ U)" "wftrm (Fun g T)"
    and U: "∀u ∈ set U. ∃y. u = Var y" "distinct U"
  shows "∃θ. wtsubst θ ∧ wftrms (subst_range θ) ∧ Fun g T = Fun g U ⋅ θ"
proof -
  define the_i where "the_i ≡ λy. THE x. x < length U ∧ U ! x = Var y"
  define θ where θ: "θ ≡ λy. if Var y ∈ set U then T ! the_i y else Var y"

  have g: "arity g > 0" using gT(1,2) fun_type_inv(1) by blast

  have UT: "length U = length T" using fun_type_length_eq gT(1) by fastforce

  have 1: "the_i y < length U ∧ U ! the_i y = Var y" when y: "Var y ∈ set U" for y
    using theI'[OF distinct_Ex1[OF U(2) y]] unfolding the_i_def by simp

  have 2: "wtsubst θ"
    using θ 1 gT(1) fun_type[OF g] UT
    unfolding wtsubst_def
    by (metis (no_types, lifting) nth_map term.inject(2))

  have "∀i<length T. U ! i ⋅ θ = T ! i"
    using θ 1 U(1) UT distinct_Ex1[OF U(2)] in_set_conv_nth
    by (metis (no_types, lifting) eval_term.simps(1))
  hence "T = map (λt. t ⋅ θ) U" by (simp add: UT nth_equalityI)
  hence 3: "Fun g T = Fun g U ⋅ θ" by simp

  have "subst_range θ ⊆ set T" using θ 1 U(1) UT by (auto simp add: subst_domain_def)
  hence 4: "wftrms (subst_range θ)" using gT(2) wf_trm_param by auto

  show ?thesis by (metis 2 3 4)
qed

lemma TComp_var_instance_closed_has_Var:
  assumes closed: "is_TComp_var_instance_closed Γ M"
    and wf_M: "wftrms M"
    and wf_δx: "wftrm (δ x)"
    and y_ex: "∃y ∈ fvset M. Γ (Var x) = Γ (Var y)"
    and t: "t ⊑ δ x"
    and δ_wt: "wtsubst δ"
  shows "∃y ∈ fvset M. Γ (Var y) = Γ t"
proof (cases "Γ (Var x)")
  case (Var a)
  hence "t = δ x"
    using t wf_δx δ_wt
    by (metis (full_types) const_type_inv_wf fun_if_subterm subtermeq_Var_const(2) wtsubst_def)
  thus ?thesis using y_ex wt_subst_trm''[OF δ_wt, of "Var x"] by fastforce
next
  case (Fun f T)
  hence Γ_δx: "Γ (δ x) = TComp f T" using wt_subst_trm''[OF δ_wt, of "Var x"] by auto

  show ?thesis
  proof (cases "t = δ x")
    case False
    hence t_subt_δx: "t ⊏ δ x" using t(1) Γ_δx by fastforce

    obtain T' where T': "δ x = Fun f T'" using Γ_δx t_subt_δx fun_type_id_eq by (cases "δ x") auto
    
    obtain g S where gS: "Fun g S ⊑ δ x" "t ∈ set S" using Fun_ex_if_subterm[OF t_subt_δx] by blast
  
    have gS_wf: "wftrm (Fun g S)" by (rule wf_trm_subtermeq[OF wf_δx gS(1)])
    hence "arity g > 0" using gS(2) by (metis length_pos_if_in_set wf_trm_arity) 
    hence gS_Γ: "Γ (Fun g S) = TComp g (map Γ S)" using fun_type by blast
  
    obtain h U where hU:
        "Fun h U ∈ M" "Γ (Fun h U) = Fun g (map Γ S)" "∀u ∈ set U. is_Var u"
      using is_TComp_var_instance_closedD'[OF y_ex _ closed wf_M]
            subtermeq_imp_subtermtypeeq[OF wf_δx] gS Γ_δx Fun gS_Γ
      by metis
  
    obtain y where y: "Var y ∈ set U" "Γ (Var y) = Γ t"
      using hU(3) fun_type_param_ex[OF hU(2) gS(2)] by fast
  
    have "y ∈ fvset M" using hU(1) y(1) by force
    thus ?thesis using y(2) closed by metis
  qed (metis y_ex Fun Γ_δx)
qed

lemma TComp_var_instance_closed_has_Fun:
  assumes closed: "is_TComp_var_instance_closed Γ M"
    and wf_M: "wftrms M"
    and wf_δx: "wftrm (δ x)"
    and y_ex: "∃y ∈ fvset M. Γ (Var x) = Γ (Var y)"
    and t: "t ⊑ δ x"
    and δ_wt: "wtsubst δ"
    and t_Γ: "Γ t = TComp g T"
    and t_fun: "is_Fun t"
  shows "∃m ∈ M. ∃θ. wtsubst θ ∧ wftrms (subst_range θ) ∧ t = m ⋅ θ ∧ is_Fun m"
proof -
  obtain T'' where T'': "t = Fun g T''" using t_Γ t_fun fun_type_id_eq by blast

  have g: "arity g > 0" using t_Γ fun_type_inv[of t] by simp_all

  have "TComp g T ⊑ Γ (Var x)" using δ_wt t t_Γ
    by (metis wf_δx subtermeq_imp_subtermtypeeq wtsubst_def) 
  then obtain U where U:
      "Fun g U ∈ M" "Γ (Fun g U) = TComp g T" "∀u ∈ set U. ∃y. u = Var y"
      "distinct U" "length T'' = length U"
    using is_TComp_var_instance_closedD'[OF y_ex _ closed wf_M]
    by (metis t_Γ T'' fun_type_id_eq fun_type_length_eq is_VarE)
  hence UT': "T = map Γ U" using fun_type[OF g, of U] by simp

  show ?thesis
    using TComp_var_instance_wt_subst_exists UT' T'' U(1,3,4) t t_Γ wf_δx wf_trm_subtermeq
    by (metis term.disc(2))
qed

lemma TComp_var_and_subterm_instance_closed_has_subterms_instances:
  assumes M_var_inst_cl: "is_TComp_var_instance_closed Γ M"
    and M_subterms_cl: "has_all_wt_instances_of Γ (subtermsset M) M"
    and M_wf: "wftrms M"
    and t: "t ⊑set M"
    and s: "s ⊑ t ⋅ δ"
    and δ: "wtsubst δ" "wftrms (subst_range δ)"
  shows "∃m ∈ M. ∃θ. wtsubst θ ∧ wftrms (subst_range θ) ∧ s = m ⋅ θ"
using subterm_subst_unfold[OF s]
proof
  assume "∃s'. s' ⊑ t ∧ s = s' ⋅ δ"
  then obtain s' where s': "s' ⊑ t" "s = s' ⋅ δ" by blast
  then obtain θ where θ: "wtsubst θ" "wftrms (subst_range θ)" "s' ∈ M ⋅set θ"
    using t has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]
          term.order_trans[of s' t]
    by blast
  then obtain m where m: "m ∈ M" "s' = m ⋅ θ" by blast

  have "s = m ⋅ (θ ∘s δ)" using s'(2) m(2) by simp
  thus ?thesis
    using m(1) wt_subst_compose[OF θ(1) δ(1)] wf_trms_subst_compose[OF θ(2) δ(2)] by blast
next
  assume "∃x ∈ fv t. s ⊏ δ x"
  then obtain x where x: "x ∈ fv t" "s ⊏ δ x" "s ⊑ δ x" by blast

  note 0 = TComp_var_instance_closed_has_Var[OF M_var_inst_cl M_wf]
  note 1 = has_all_wt_instances_ofD''[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]

  have δx_wf: "wftrm (δ x)" and s_wf_trm: "wftrm s"
    using δ(2) wf_trm_subterm[OF _ x(2)] by fastforce+

  have x_fv_ex: "∃y ∈ fvset M. Γ (Var x) = Γ (Var y)"
    using x(1) s fv_subset_subterms[OF t] by auto

  obtain y where y: "y ∈ fvset M" "Γ (Var y) = Γ s"
    using 0[of δ x s, OF δx_wf x_fv_ex x(3) δ(1)] by metis
  then obtain z where z: "Var z ∈ M" "Γ (Var z) = Γ s"
    using 1[of y] vars_iff_subtermeq_set[of y M] by metis

  define θ where "θ ≡ Var(z := s)::('fun, ('fun, 'atom) term × nat) subst"

  have "wtsubst θ" "wftrms (subst_range θ)" "s = Var z ⋅ θ"
    using z(2) s_wf_trm unfolding θ_def wtsubst_def by force+
  thus ?thesis using z(1) by blast
qed

context
begin
private lemma SMP_D_aux1:
  assumes "t ∈ SMP M"
    and closed: "has_all_wt_instances_of Γ (subtermsset M) M"
                "is_TComp_var_instance_closed Γ M"
    and wf_M: "wftrms M"
  shows "∀x ∈ fv t. ∃y ∈ fvset M. Γ (Var y) = Γ (Var x)"
using assms(1)
proof (induction t rule: SMP.induct)
  case (MP t) show ?case
  proof
    fix x assume x: "x ∈ fv t"
    hence "Var x ∈ subtermsset M" using MP.hyps vars_iff_subtermeq by fastforce
    then obtain δ s where δ: "wtsubst δ" "wftrms (subst_range δ)"
        and s: "s ∈ M" "Var x = s ⋅ δ"
      using has_all_wt_instances_ofD'[OF wf_trms_subterms[OF wf_M] wf_M closed(1)] by blast
    then obtain y where y: "s = Var y" by (cases s) auto
    thus "∃y ∈ fvset M. Γ (Var y) = Γ (Var x)"
      using s wt_subst_trm''[OF δ(1), of "Var y"] by force
  qed
next
  case (Subterm t t')
  hence "fv t' ⊆ fv t" using subtermeq_vars_subset by auto
  thus ?case using Subterm.IH by auto
next
  case (Substitution t δ)
  note IH = Substitution.IH
  show ?case
  proof
    fix x assume x: "x ∈ fv (t ⋅ δ)"
    then obtain y where y: "y ∈ fv t" "Γ (Var x) ⊑ Γ (Var y)"
      using Substitution.hyps(2,3)
      by (metis subst_apply_img_var subtermeqI' subtermeq_imp_subtermtypeeq
                vars_iff_subtermeq wtsubst_def wf_trm_subst_rangeD)
    let ?P = "λx. ∃y ∈ fvset M. Γ (Var y) = Γ (Var x)"
    show "?P x" using y IH
    proof (induction "Γ (Var y)" arbitrary: y t)
      case (Var a)
      hence "Γ (Var x) = Γ (Var y)" by auto
      thus ?case using Var(2,4) by auto
    next
      case (Fun f T)
      obtain z where z: "∃w ∈ fvset M. Γ (Var z) = Γ (Var w)" "Γ (Var z) = Γ (Var y)"
        using Fun.prems(1,3) by blast
      show ?case
      proof (cases "Γ (Var x) = Γ (Var y)")
        case True thus ?thesis using Fun.prems by auto
      next
        case False
        then obtain τ where τ: "τ ∈ set T" "Γ (Var x) ⊑ τ" using Fun.prems(2) Fun.hyps(2) by auto
        then obtain U where U:
            "Fun f U ∈ M" "Γ (Fun f U) = Γ (Var z)" "∀u ∈ set U. ∃v. u = Var v" "distinct U"
          using is_TComp_var_instance_closedD'[OF z(1) _ closed(2) wf_M] Fun.hyps(2) z(2)
          by (metis fun_type_id_eq subtermeqI' is_VarE)
        hence 1: "∀x ∈ fv (Fun f U). ∃y ∈ fvset M. Γ (Var y) = Γ (Var x)" by force

        have "arity f > 0" using U(2) z(2) Fun.hyps(2) fun_type_inv(1) by metis
        hence "Γ (Fun f U) = TComp f (map Γ U)" using fun_type by auto
        then obtain u where u: "Var u ∈ set U" "Γ (Var u) = τ"
          using τ(1) U(2,3) z(2) Fun.hyps(2) by auto
        show ?thesis
          using Fun.hyps(1)[of u "Fun f U"] u τ 1
          by force
      qed
    qed
  qed
next
  case (Ana t K T k)
  have "fv k ⊆ fv t" using Ana_keys_fv[OF Ana.hyps(2)] Ana.hyps(3) by auto
  thus ?case using Ana.IH by auto
qed

private lemma SMP_D_aux2:
  fixes t::"('fun, ('fun, 'atom) term × nat) term"
  assumes t_SMP: "t ∈ SMP M"
    and t_Var: "∃x. t = Var x"
    and M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
  shows "∃m ∈ M. ∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ t = m ⋅ δ"
proof -
  have M_wf: "wftrms M" 
      and M_var_inst_cl: "is_TComp_var_instance_closed Γ M"
      and M_subterms_cl: "has_all_wt_instances_of Γ (subtermsset M) M"
      and M_Ana_cl: "has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
    using finite_SMP_representationD[OF M_SMP_repr] by blast+

  have M_Ana_wf: "wftrms (⋃ ((set ∘ fst ∘ Ana) ` M))"
  proof
    fix k assume "k ∈ ⋃((set ∘ fst ∘ Ana) ` M)"
    then obtain m where m: "m ∈ M" "k ∈ set (fst (Ana m))" by force
    thus "wftrm k" using M_wf Ana_keys_wf'[of m "fst (Ana m)" _ k] surjective_pairing by blast
  qed

  note 0 = has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]
  note 1 = has_all_wt_instances_ofD'[OF M_Ana_wf M_wf M_Ana_cl]

  obtain x y where x: "t = Var x" and y: "y ∈ fvset M" "Γ (Var y) = Γ (Var x)"
    using t_Var SMP_D_aux1[OF t_SMP M_subterms_cl M_var_inst_cl M_wf] by fastforce
  then obtain m δ where m: "m ∈ M" "m ⋅ δ = Var y" and δ: "wtsubst δ"
    using 0[of "Var y"] vars_iff_subtermeq_set[of y M] by fastforce
  obtain z where z: "m = Var z" using m(2) by (cases m) auto

  define θ where "θ ≡ Var(z := Var x)::('fun, ('fun, 'atom) term × nat) subst"

  have "Γ (Var z) = Γ (Var x)" using y(2) m(2) z wt_subst_trm''[OF δ, of m] by argo
  hence "wtsubst θ" "wftrms (subst_range θ)" unfolding θ_def wtsubst_def by force+
  moreover have "t = m ⋅ θ" using x z unfolding θ_def by simp
  ultimately show ?thesis using m(1) by blast
qed

private lemma SMP_D_aux3:
  assumes hyps: "t' ⊑ t" and wf_t: "wftrm t" and prems: "is_Fun t'"
    and IH:
      "((∃f. t = Fun f []) ∧ (∃m ∈ M. ∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ t = m ⋅ δ)) ∨
       (∃m ∈ M. ∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ t = m ⋅ δ ∧ is_Fun m)"
    and M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
  shows "((∃f. t' = Fun f []) ∧ (∃m ∈ M. ∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ t' = m ⋅ δ)) ∨
         (∃m ∈ M. ∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ t' = m ⋅ δ ∧ is_Fun m)"
proof (cases "∃f. t = Fun f [] ∨ t' = Fun f []")
  case True
  have M_wf: "wftrms M" 
    and M_var_inst_cl: "is_TComp_var_instance_closed Γ M"
    and M_subterms_cl: "has_all_wt_instances_of Γ (subtermsset M) M"
    and M_Ana_cl: "has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
  using finite_SMP_representationD[OF M_SMP_repr] by blast+

  note 0 = has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl]
  note 1 = TComp_var_instance_closed_has_Fun[OF M_var_inst_cl M_wf]
  note 2 = TComp_var_and_subterm_instance_closed_has_subterms_instances[
            OF M_var_inst_cl M_subterms_cl M_wf]

  have wf_t': "wftrm t'" using hyps wf_t wf_trm_subterm by blast

  obtain c where "t = Fun c [] ∨ t' = Fun c []" using True by moura
  thus ?thesis
  proof
    assume c: "t' = Fun c []"
    show ?thesis
    proof (cases "∃f. t = Fun f []")
      case True
      hence "t = t'" using c hyps by force
      thus ?thesis using IH by fast
    next
      case False
      note F = this
      then obtain m δ where m: "m ∈ M" "t = m ⋅ δ"
          and δ: "wtsubst δ" "wftrms (subst_range δ)"
        using IH by blast

      show ?thesis using subterm_subst_unfold[OF hyps[unfolded m(2)]]
      proof
        assume "∃m'. m' ⊑ m ∧ t' = m' ⋅ δ"
        then obtain m' where m': "m' ⊑ m" "t' = m' ⋅ δ" by moura
        obtain n θ where n: "n ∈ M" "m' = n ⋅ θ" and θ: "wtsubst θ" "wftrms (subst_range θ)"
          using 0[of m'] m(1) m'(1) by blast
        have "t' = n ⋅ (θ ∘s δ)" using m'(2) n(2) by auto
        thus ?thesis
          using c n(1) wt_subst_compose[OF θ(1) δ(1)] wf_trms_subst_compose[OF θ(2) δ(2)] by blast
      next
        assume "∃x ∈ fv m. t' ⊏ δ x"
        then obtain x where x: "x ∈ fv m" "t' ⊏ δ x" "t' ⊑ δ x" by moura
        have δx_wf: "wftrm (δ x)" using δ(2) by fastforce
        
        have x_fv_ex: "∃y ∈ fvset M. Γ (Var x) = Γ (Var y)" using x m by auto

        show ?thesis
        proof (cases "Γ t'")
          case (Var a)
          show ?thesis
            using c m 2[OF _ hyps[unfolded m(2)] δ]
            by fast
        next
          case (Fun g S)
          show ?thesis
            using c 1[of δ x t', OF δx_wf x_fv_ex x(3) δ(1) Fun]
            by blast
        qed
      qed
    qed
  qed (use IH hyps in simp)
next
  case False
  note F = False
  then obtain m δ where m:
      "m ∈ M" "wtsubst δ" "t = m ⋅ δ" "is_Fun m" "wftrms (subst_range δ)"
    using IH by moura
  obtain f T where fT: "t' = Fun f T" "arity f > 0" "Γ t' = TComp f (map Γ T)"
    using F prems fun_type wf_trm_subtermeq[OF wf_t hyps]
    by (metis is_FunE length_greater_0_conv subtermeqI' wftrm_def)

  have closed: "has_all_wt_instances_of Γ (subtermsset M) M"
               "is_TComp_var_instance_closed Γ M"
    using M_SMP_repr unfolding finite_SMP_representation_def by metis+

  have M_wf: "wftrms M" 
    using finite_SMP_representationD[OF M_SMP_repr] by blast

  show ?thesis
  proof (cases "∃x ∈ fv m. t' ⊑ δ x")
    case True
    then obtain x where x: "x ∈ fv m" "t' ⊑ δ x" by moura
    have 1: "x ∈ fvset M" using m(1) x(1) by auto
    have 2: "is_Fun (δ x)" using prems x(2) by auto
    have 3: "wftrm (δ x)" using m(5) by (simp add: wf_trm_subst_rangeD)
    have "¬(∃f. δ x = Fun f [])" using F x(2) by auto
    hence "∃f T. Γ (Var x) = TComp f T" using 2 3 m(2)
      by (metis (no_types) fun_type is_FunE length_greater_0_conv subtermeqI' wftrm_def wtsubst_def)
    moreover have "∃f T. Γ t' = Fun f T"
      using False prems wf_trm_subtermeq[OF wf_t hyps]
      by (metis (no_types) fun_type is_FunE length_greater_0_conv subtermeqI' wftrm_def)
    ultimately show ?thesis
      using TComp_var_instance_closed_has_Fun 1 x(2) m(2) prems closed 3 M_wf
      by metis
  next
    case False
    then obtain m' where m': "m' ⊑ m" "t' = m' ⋅ δ" "is_Fun m'"
      using hyps m(3) subterm_subst_not_img_subterm
      by blast
    then obtain θ m'' where θ: "wtsubst θ" "wftrms (subst_range θ)" "m'' ∈ M" "m' = m'' ⋅ θ"
      using m(1) has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf closed(1)] by blast
    hence t'_m'': "t' = m'' ⋅ θ ∘s δ" using m'(2) by fastforce

    note θδ = wt_subst_compose[OF θ(1) m(2)] wf_trms_subst_compose[OF θ(2) m(5)]

    show ?thesis
    proof (cases "is_Fun m''")
      case True thus ?thesis using θ(3,4) m'(2,3) m(4) fT t'_m'' θδ by blast
    next
      case False
      then obtain x where x: "m'' = Var x" by moura
      hence "∃y ∈ fvset M. Γ (Var x) = Γ (Var y)" "t' ⊑ (θ ∘s δ) x"
            "Γ (Var x) = Fun f (map Γ T)" "wftrm ((θ ∘s δ) x)"
        using θδ t'_m'' θ(3) fv_subset[OF θ(3)] fT(3) eval_term.simps(1)[of _ "θ ∘s δ"]
              wt_subst_trm''[OF θδ(1), of "Var x"]
           by force+
      thus ?thesis
        using x TComp_var_instance_closed_has_Fun[
                of M "θ ∘s δ" x t' f "map Γ T", OF closed(2) M_wf _ _ _ θδ(1) fT(3) prems]
        by blast
    qed
  qed
qed

lemma SMP_D:
  assumes "t ∈ SMP M" "is_Fun t"
    and M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
  shows "((∃f. t = Fun f []) ∧ (∃m ∈ M. ∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ t = m ⋅ δ)) ∨
         (∃m ∈ M. ∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ t = m ⋅ δ ∧ is_Fun m)"
proof -
  have wf_M: "wftrms M"
      and closed: "has_all_wt_instances_of Γ (subtermsset M) M"
                  "has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
                  "is_TComp_var_instance_closed Γ M"
    using finite_SMP_representationD[OF M_SMP_repr] by blast+

  show ?thesis using assms(1,2)
  proof (induction t rule: SMP.induct)
    case (MP t)
    moreover have "wtsubst Var" "wftrms (subst_range Var)" "t = t ⋅ Var" by simp_all
    ultimately show ?case by blast 
  next
    case (Subterm t t')
    hence t_fun: "is_Fun t" by auto
    note * = Subterm.hyps(2) SMP_wf_trm[OF Subterm.hyps(1) wf_M(1)]
             Subterm.prems Subterm.IH[OF t_fun] M_SMP_repr
    show ?case by (rule SMP_D_aux3[OF *])
  next
    case (Substitution t δ)
    have wf: "wftrm t" by (metis Substitution.hyps(1) wf_M(1) SMP_wf_trm)
    hence wf': "wftrm (t ⋅ δ)" using Substitution.hyps(3) wf_trm_subst by blast
    show ?case
    proof (cases "Γ t")
      case (Var a)
      hence 1: "Γ (t ⋅ δ) = TAtom a" using Substitution.hyps(2) by (metis wt_subst_trm'') 
      then obtain c where c: "t ⋅ δ = Fun c []"
        using TAtom_term_cases[OF wf' 1] Substitution.prems by fastforce
      hence "(∃x. t = Var x) ∨ t = t ⋅ δ" by (cases t) auto
      thus ?thesis
      proof
        assume t_Var: "∃x. t = Var x"
        then obtain x where x: "t = Var x" "δ x = Fun c []" "Γ (Var x) = TAtom a"
          using c 1 wt_subst_trm''[OF Substitution.hyps(2), of t] by force
        
        obtain m θ where m: "m ∈ M" "t = m ⋅ θ" and θ: "wtsubst θ" "wftrms (subst_range θ)"
          using SMP_D_aux2[OF Substitution.hyps(1) t_Var M_SMP_repr] by moura

        have "m ⋅ (θ ∘s δ) = Fun c []" using c m(2) by auto
        thus ?thesis
          using c m(1) wt_subst_compose[OF θ(1) Substitution.hyps(2)]
                wf_trms_subst_compose[OF θ(2) Substitution.hyps(3)]
          by metis
      qed (use c Substitution.IH in auto)
    next
      case (Fun f T)
      hence 1: "Γ (t ⋅ δ) = TComp f T" using Substitution.hyps(2) by (metis wt_subst_trm'')
      have 2: "¬(∃f. t = Fun f [])" using Fun TComp_term_cases[OF wf] by auto
      obtain T'' where T'': "t ⋅ δ = Fun f T''"
        using 1 2 fun_type_id_eq Fun Substitution.prems
        by fastforce
      have f: "arity f > 0" using fun_type_inv[OF 1] by metis
  
      show ?thesis
      proof (cases t)
        case (Fun g U)
        then obtain m θ where m:
            "m ∈ M" "wtsubst θ" "t = m ⋅ θ" "is_Fun m" "wftrms (subst_range θ)"
          using Substitution.IH Fun 2 by moura
        have "wtsubst (θ ∘s δ)" "t ⋅ δ = m ⋅ (θ ∘s δ)" "wftrms (subst_range (θ ∘s δ))"
          using wt_subst_compose[OF m(2) Substitution.hyps(2)] m(3)
                wf_trms_subst_compose[OF m(5) Substitution.hyps(3)]
          by auto
        thus ?thesis using m(1,4) by metis
      next
        case (Var x)
        then obtain y where y: "y ∈ fvset M" "Γ (Var y) = Γ (Var x)"
          using SMP_D_aux1[OF Substitution.hyps(1) closed(1,3) wf_M] Fun
          by moura
        hence 3: "Γ (Var y) = TComp f T" using Var Fun Γ_Var_fst by simp
        
        obtain h V where V:
            "Fun h V ∈ M" "Γ (Fun h V) = Γ (Var y)" "∀u ∈ set V. ∃z. u = Var z" "distinct V"
          by (metis is_VarE is_TComp_var_instance_closedD[OF _ 3 closed(3)] y(1))
        moreover have "length T'' = length V" using 3 V(2) fun_type_length_eq 1 T'' by metis
        ultimately have TV: "T = map Γ V"
          by (metis fun_type[OF f(1)] 3 fun_type_id_eq term.inject(2))
  
        obtain θ where θ: "wtsubst θ" "wftrms (subst_range θ)" "t ⋅ δ = Fun h V ⋅ θ"
          using TComp_var_instance_wt_subst_exists 1 3 T'' TV V(2,3,4) wf'
          by (metis fun_type_id_eq)
  
        have 9: "Γ (Fun h V) = Γ (δ x)" using y(2) Substitution.hyps(2) V(2) 1 3 Var by auto
  
        show ?thesis using Var θ 9 V(1) by force
      qed
    qed
  next
    case (Ana t K T k)
    have 1: "is_Fun t" using Ana.hyps(2,3) by auto
    then obtain f U where U: "t = Fun f U" by moura
  
    have 2: "fv k ⊆ fv t" using Ana_keys_fv[OF Ana.hyps(2)] Ana.hyps(3) by auto
  
    have wf_t: "wftrm t"
      using SMP_wf_trm[OF Ana.hyps(1)] wftrm_code wf_M
      by auto
    hence wf_k: "wftrm k"
      using Ana_keys_wf'[OF Ana.hyps(2)] wftrm_code Ana.hyps(3)
      by auto
  
    have wf_M_keys: "wftrms (⋃((set ∘ fst ∘ Ana) ` M))"
    proof
      fix t assume "t ∈ (⋃((set ∘ fst ∘ Ana) ` M))"
      then obtain s where s: "s ∈ M" "t ∈ (set ∘ fst ∘ Ana) s" by blast
      obtain K R where KR: "Ana s = (K,R)" by (metis surj_pair)
      hence "t ∈ set K" using s(2) by simp
      thus "wftrm t" using Ana_keys_wf'[OF KR] wf_M s(1) by blast
    qed
  
    show ?case using Ana_subst'_or_Ana_keys_subterm
    proof
      assume "∀t K T k. Ana t = (K, T) ⟶ k ∈ set K ⟶ k ⊏ t"
      hence *: "k ⊑ t" using Ana.hyps(2,3) by auto
      show ?thesis by (rule SMP_D_aux3[OF * wf_t Ana.prems Ana.IH[OF 1] M_SMP_repr])
    next
      assume Ana_subst':
          "∀f T δ K M. Ana (Fun f T) = (K, M) ⟶ Ana (Fun f T ⋅ δ) = (K ⋅list δ, M ⋅list δ)"
  
      have "arity f > 0" using Ana_const[of f U] U Ana.hyps(2,3) by fastforce
      hence "U ≠ []" using wf_t U unfolding wftrm_def by force
      then obtain m δ where m: "m ∈ M" "wtsubst δ" "wftrms (subst_range δ)" "t = m ⋅ δ" "is_Fun m"
        using Ana.IH[OF 1] U by auto
      hence "Ana (t ⋅ δ) = (K ⋅list δ,T ⋅list δ)" using Ana_subst' U Ana.hyps(2) by auto
      obtain Km Tm where Ana_m: "Ana m = (Km,Tm)" by moura
      hence "Ana (m ⋅ δ) = (Km ⋅list δ,Tm ⋅list δ)"
        using Ana_subst' U m(4) is_FunE[OF m(5)] Ana.hyps(2)
        by metis
      then obtain km where km: "km ∈ set Km" "k = km ⋅ δ" using Ana.hyps(2,3) m(4) by auto
      then obtain θ km' where θ: "wtsubst θ" "wftrms (subst_range θ)"
          and km': "km' ∈ M" "km = km' ⋅ θ"
        using Ana_m m(1) has_all_wt_instances_ofD'[OF wf_M_keys wf_M closed(2), of km] by force
  
      have kθδ: "k = km' ⋅ θ ∘s δ" "wtsubst (θ ∘s δ)" "wftrms (subst_range (θ ∘s δ))"
        using km(2) km' wt_subst_compose[OF θ(1) m(2)] wf_trms_subst_compose[OF θ(2) m(3)]
        by auto
  
      show ?case
      proof (cases "is_Fun km'")
        case True thus ?thesis using kθδ km'(1) by blast
      next
        case False
        note F = False
        then obtain x where x: "km' = Var x" by auto
        hence 3: "x ∈ fvset M" using fv_subset[OF km'(1)] by auto
        obtain kf kT where kf: "k = Fun kf kT" using Ana.prems by auto
        show ?thesis
        proof (cases "kT = []")
          case True thus ?thesis using kθδ(1) kθδ(2) kθδ(3) kf km'(1) by blast
        next
          case False
          hence 4: "arity kf > 0" using wf_k kf TAtom_term_cases const_type by fastforce
          then obtain kT' where kT': "Γ k = TComp kf kT'" by (simp add: fun_type kf) 
          then obtain V where V:
              "Fun kf V ∈ M" "Γ (Fun kf V) = Γ (Var x)" "∀u ∈ set V. ∃v. u = Var v"
              "distinct V" "is_Fun (Fun kf V)"
            using is_TComp_var_instance_closedD[OF _ _ closed(3), of x]
                  x m(2) kθδ(1) 3 wt_subst_trm''[OF kθδ(2)]
            by (metis fun_type_id_eq term.disc(2) is_VarE)
          have 5: "kT' = map Γ V"
            using fun_type[OF 4] x kT' kθδ m(2) V(2)
            by (metis term.inject(2) wt_subst_trm'')
          thus ?thesis
            using TComp_var_instance_wt_subst_exists wf_k kf 4 V(3,4) kT' V(1,5)
            by metis
        qed
      qed
    qed
  qed
qed

lemma SMP_D':
  fixes M
  defines "δ ≡ var_rename (max_var_set (fvset M))"
  assumes M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
    and s: "s ∈ SMP M" "is_Fun s" "∄f. s = Fun f []"
    and t: "t ∈ SMP M" "is_Fun t" "∄f. t = Fun f []"
  obtains σ s0 θ t0
  where "wtsubst σ" "wftrms (subst_range σ)" "s0 ∈ M" "is_Fun s0" "s = s0 ⋅ σ" "Γ s = Γ s0"
    and "wtsubst θ" "wftrms (subst_range θ)" "t0 ∈ M" "is_Fun t0" "t = t0 ⋅ δ ⋅ θ" "Γ t = Γ t0"
proof -
  obtain σ s0 where
      s0: "wtsubst σ" "wftrms (subst_range σ)" "s0 ∈ M" "s = s0 ⋅ σ" "is_Fun s0"
    using s(3) SMP_D[OF s(1,2) M_SMP_repr] unfolding δ_def by metis

  obtain θ t0 where t0:
      "wtsubst θ" "wftrms (subst_range θ)" "t0 ∈ M" "t = t0 ⋅ δ ⋅ θ" "is_Fun t0"
    using t(3) SMP_D[OF t(1,2) M_SMP_repr] var_rename_wt'[of _ t]
          wf_trms_subst_compose_Var_range(1)[OF _ var_rename_is_renaming(2)]
    unfolding δ_def by metis

  have "Γ s = Γ s0" "Γ t = Γ (t0 ⋅ δ)" "Γ (t0 ⋅ δ) = Γ t0"
    using s0 t0 wt_subst_trm'' by (metis, metis, metis δ_def var_rename_wt(1))
  thus ?thesis using s0 t0 that by simp
qed

lemma SMP_D'':
  fixes t::"('fun, ('fun, 'atom) term × nat) term"
  assumes t_SMP: "t ∈ SMP M"
    and M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
  shows "∃m ∈ M. ∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ t = m ⋅ δ"
proof (cases "(∃x. t = Var x) ∨ (∃c. t = Fun c [])")
  case True
  have M_wf: "wftrms M" 
      and M_var_inst_cl: "is_TComp_var_instance_closed Γ M"
      and M_subterms_cl: "has_all_wt_instances_of Γ (subtermsset M) M"
      and M_Ana_cl: "has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
    using finite_SMP_representationD[OF M_SMP_repr] by blast+

  have M_Ana_wf: "wftrms (⋃ ((set ∘ fst ∘ Ana) ` M))"
  proof
    fix k assume "k ∈ ⋃((set ∘ fst ∘ Ana) ` M)"
    then obtain m where m: "m ∈ M" "k ∈ set (fst (Ana m))" by force
    thus "wftrm k" using M_wf Ana_keys_wf'[of m "fst (Ana m)" _ k] surjective_pairing by blast
  qed

  show ?thesis using True
  proof
    assume "∃x. t = Var x"
    then obtain x y where x: "t = Var x" and y: "y ∈ fvset M" "Γ (Var y) = Γ (Var x)"
      using SMP_D_aux1[OF t_SMP M_subterms_cl M_var_inst_cl M_wf] by fastforce
    then obtain m δ where m: "m ∈ M" "m ⋅ δ = Var y" and δ: "wtsubst δ"
      using has_all_wt_instances_ofD'[OF wf_trms_subterms[OF M_wf] M_wf M_subterms_cl, of "Var y"]
            vars_iff_subtermeq_set[of y M]
      by fastforce

    obtain z where z: "m = Var z" using m(2) by (cases m) auto

    define θ where "θ ≡ Var(z := Var x)::('fun, ('fun, 'atom) term × nat) subst"

    have "Γ (Var z) = Γ (Var x)" using y(2) m(2) z wt_subst_trm''[OF δ, of m] by argo
    hence "wtsubst θ" "wftrms (subst_range θ)" unfolding θ_def wtsubst_def by force+
    moreover have "t = m ⋅ θ" using x z unfolding θ_def by simp
    ultimately show ?thesis using m(1) by blast
  qed (use SMP_D[OF t_SMP _ M_SMP_repr] in blast)
qed (use SMP_D[OF t_SMP _ M_SMP_repr] in blast)
end

lemma tfrset_if_comp_tfrset:
  assumes "comp_tfrset arity Ana Γ M"
  shows "tfrset M"
proof -
  let ?δ = "var_rename (max_var_set (fvset M))"
  have M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
    by (metis comp_tfrset_def assms)

  have M_finite: "finite M"
    using assms card_gt_0_iff unfolding comp_tfrset_def finite_SMP_representation_def by blast

  show ?thesis
  proof (unfold tfrset_def; intro ballI impI)
    fix s t assume "s ∈ SMP M - Var`𝒱" "t ∈ SMP M - Var`𝒱"
    hence st: "s ∈ SMP M" "is_Fun s" "t ∈ SMP M" "is_Fun t" by auto
    have "¬(∃δ. Unifier δ s t)" when st_type_neq: "Γ s ≠ Γ t"
    proof (cases "∃f. s = Fun f [] ∨ t = Fun f []")
      case False
      then obtain σ s0 θ t0 where
            s0: "s0 ∈ M" "is_Fun s0" "s = s0 ⋅ σ" "Γ s = Γ s0"
        and t0: "t0 ∈ M" "is_Fun t0" "t = t0 ⋅ ?δ ⋅ θ" "Γ t = Γ t0"
        using SMP_D'[OF M_SMP_repr st(1,2) _ st(3,4)] by metis
      hence "¬(∃δ. Unifier δ s0 (t0 ⋅ ?δ))"
        using assms mgu_None_is_subst_neq st_type_neq wt_subst_trm''[OF var_rename_wt(1)]
        unfolding comp_tfrset_def Let_def by metis
      thus ?thesis
        using vars_term_disjoint_imp_unifier[OF var_rename_fv_set_disjoint[OF M_finite]] s0(1) t0(1)
        unfolding s0(3) t0(3) by (metis (no_types, opaque_lifting) subst_subst_compose)
    qed (use st_type_neq st(2,4) in auto)
    thus "Γ s = Γ t" when "∃δ. Unifier δ s t" by (metis that)
  qed
qed

lemma tfrset_if_comp_tfrset':
  assumes "let N = SMP0 Ana Γ M in set M ⊆ set N ∧ comp_tfrset arity Ana Γ (set N)"
  shows "tfrset (set M)"
by (rule tfr_subset(2)[
          OF tfrset_if_comp_tfrset[OF conjunct2[OF assms[unfolded Let_def]]]
             conjunct1[OF assms[unfolded Let_def]]])

lemma tfrstp_is_comp_tfrstp: "tfrstp a = comp_tfrstp Γ a"
proof (cases a)
  case (Equality ac t t')
  thus ?thesis
    using mgu_always_unifies[of t _ t'] mgu_gives_MGU[of t t']
    by auto
next
  case (Inequality X F)
  thus ?thesis
    using tfrstp.simps(2)[of X F]
          comp_tfrstp.simps(2)[of Γ X F]
          Fun_range_case(2)[of "subtermsset (trmspairs F)"] 
    unfolding is_Var_def
    by auto
qed auto

lemma tfrst_if_comp_tfrst:
  assumes "comp_tfrst arity Ana Γ M S"
  shows "tfrst S"
unfolding tfrst_def
proof
  have comp_tfrset_M: "comp_tfrset arity Ana Γ M"
    using assms unfolding comp_tfrst_def by blast
  
  have wftrms_M: "wftrms M"
      and wftrms_S: "wftrms (trmsst S)"
      and S_trms_instance_M: "has_all_wt_instances_of Γ (trmsst S) M"
    using assms wftrm_code wftrms_code trms_listst_is_trmsst
    unfolding comp_tfrst_def comp_tfrset_def finite_SMP_representation_def list_all_iff
    by blast+

  show "tfrset (trmsst S)"
    using tfr_subset(3)[OF tfrset_if_comp_tfrset[OF comp_tfrset_M] SMP_SMP_subset]
          SMP_I'[OF wftrms_S wftrms_M S_trms_instance_M]
    by blast

  have "list_all (comp_tfrstp Γ) S" by (metis assms comp_tfrst_def)
  thus "list_all tfrstp S" by (induct S) (simp_all add: tfrstp_is_comp_tfrstp)
qed

lemma tfrst_if_comp_tfrst':
  assumes "comp_tfrst arity Ana Γ (set (SMP0 Ana Γ (trms_listst S))) S"
  shows "tfrst S"
by (rule tfrst_if_comp_tfrst[OF assms])



subsubsection ‹Lemmata for Checking Ground SMP (GSMP) Disjointness›
context
begin
private lemma ground_SMP_disjointI_aux1:
  fixes M::"('fun, ('fun, 'atom) term × nat) term set"
  assumes f_def: "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ wtsubst δ ∧ wftrms (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
    and g_def: "g ≡ λM. {t ∈ M. fv t = {}}"
  shows "f (SMP M) = g (SMP M)"
proof
  have "t ∈ f (SMP M)" when t: "t ∈ SMP M" "fv t = {}" for t
  proof -
    define δ where "δ ≡ Var::('fun, ('fun, 'atom) term × nat) subst"
    have "wtsubst δ" "wftrms (subst_range δ)" "t = t ⋅ δ"
      using subst_apply_term_empty[of t] that(2) wt_subst_Var wf_trm_subst_range_Var
      unfolding δ_def by auto
    thus ?thesis using SMP.Substitution[OF t(1), of δ] t(2) unfolding f_def by fastforce
  qed
  thus "g (SMP M) ⊆ f (SMP M)" unfolding g_def by blast
qed (use f_def g_def in blast)

private lemma ground_SMP_disjointI_aux2:
  fixes M::"('fun, ('fun, 'atom) term × nat) term set"
  assumes f_def: "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ wtsubst δ ∧ wftrms (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
    and M_SMP_repr: "finite_SMP_representation arity Ana Γ M"
  shows "f M = f (SMP M)"
proof
  have M_wf: "wftrms M" 
      and M_var_inst_cl: "is_TComp_var_instance_closed Γ M"
      and M_subterms_cl: "has_all_wt_instances_of Γ (subtermsset M) M"
      and M_Ana_cl: "has_all_wt_instances_of Γ (⋃((set ∘ fst ∘ Ana) ` M)) M"
    using finite_SMP_representationD[OF M_SMP_repr] by blast+

  show "f (SMP M) ⊆ f M"
  proof
    fix t assume "t ∈ f (SMP M)"
    then obtain s δ where s: "t = s ⋅ δ" "s ∈ SMP M" "fv (s ⋅ δ) = {}"
        and δ: "wtsubst δ" "wftrms (subst_range δ)"
      unfolding f_def by blast

    have t_wf: "wftrm t" using SMP_wf_trm[OF s(2) M_wf] s(1) wf_trm_subst[OF δ(2)] by blast 

    obtain m θ where m: "m ∈ M" "s = m ⋅ θ" and θ: "wtsubst θ" "wftrms (subst_range θ)"
      using SMP_D''[OF s(2) M_SMP_repr] by blast

    have "t = m ⋅ (θ ∘s δ)" "fv (m ⋅ (θ ∘s δ)) = {}" using s(1,3) m(2) by simp_all
    thus "t ∈ f M"
      using m(1) wt_subst_compose[OF θ(1) δ(1)] wf_trms_subst_compose[OF θ(2) δ(2)]
      unfolding f_def by blast
  qed
qed (auto simp add: f_def)

private lemma ground_SMP_disjointI_aux3:
  fixes A B C::"('fun, ('fun, 'atom) term × nat) term set"
  defines "P ≡ λt s. ∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ Unifier δ t s"
  assumes f_def: "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ wtsubst δ ∧ wftrms (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
    and Q_def: "Q ≡ λt. intruder_synth' public arity {} t"
    and R_def: "R ≡ λt. ∃u ∈ C. is_wt_instance_of_cond Γ t u"
    and AB: "wftrms A" "wftrms B" "fvset A ∩ fvset B = {}"
    and C: "wftrms C"
    and ABC: "∀t ∈ A. ∀s ∈ B. P t s ⟶ Q t ∨ R t"
  shows "f A ∩ f B ⊆ f C ∪ {m. {} ⊢c m}"
proof
  fix t assume "t ∈ f A ∩ f B"
  then obtain ta tb δa δb where
          ta: "t = ta ⋅ δa" "ta ∈ A" "wtsubst δa" "wftrms (subst_range δa)" "fv (ta ⋅ δa) = {}"
      and tb: "t = tb ⋅ δb" "tb ∈ B" "wtsubst δb" "wftrms (subst_range δb)" "fv (tb ⋅ δb) = {}"
    unfolding f_def by blast

  have ta_tb_wf: "wftrm ta" "wftrm tb" "fv ta ∩ fv tb = {}" "Γ ta = Γ tb"
    using ta(1,2) tb(1,2) AB fv_subset_subterms
          wt_subst_trm''[OF ta(3), of ta] wt_subst_trm''[OF tb(3), of tb]
    by (fast, fast, blast, simp)

  obtain θ where θ: "Unifier θ ta tb" "wtsubst θ" "wftrms (subst_range θ)"
    using vars_term_disjoint_imp_unifier[OF ta_tb_wf(3), of δa δb]
          ta(1) tb(1) wt_Unifier_if_Unifier[OF ta_tb_wf(1,2,4)]
    by blast
  hence "Q ta ∨ R ta" using ABC ta(2) tb(2) unfolding P_def by blast+
  thus "t ∈ f C ∪ {m. {} ⊢c m}"
  proof
    show "Q ta ⟹ ?thesis"
      using ta(1) pgwt_ground[of ta] pgwt_is_empty_synth[of ta] subst_ground_ident[of ta δa]
      unfolding Q_def f_def intruder_synth_code[symmetric] by simp
  next
    assume "R ta"
    then obtain ua σa where ua: "ta = ua ⋅ σa" "ua ∈ C" "wtsubst σa" "wftrms (subst_range σa)"
      using θ ABC ta_tb_wf(1,2) ta(2) tb(2) C is_wt_instance_of_condD'
      unfolding P_def R_def by metis
  
    have "t = ua ⋅ (σa ∘s δa)" "fv t = {}"
      using ua(1) ta(1,5) tb(1,5) by auto
    thus ?thesis
      using ua(2) wt_subst_compose[OF ua(3) ta(3)] wf_trms_subst_compose[OF ua(4) ta(4)]
      unfolding f_def by blast
  qed
qed

lemma ground_SMP_disjointI:
  fixes A B::"('fun, ('fun, 'atom) term × nat) term set" and C
  defines "f ≡ λM. {t ⋅ δ | t δ. t ∈ M ∧ wtsubst δ ∧ wftrms (subst_range δ) ∧ fv (t ⋅ δ) = {}}"
    and "g ≡ λM. {t ∈ M. fv t = {}}"
    and "Q ≡ λt. intruder_synth' public arity {} t"
    and "R ≡ λt. ∃u ∈ C. is_wt_instance_of_cond Γ t u"
  assumes AB_fv_disj: "fvset A ∩ fvset B = {}"
    and A_SMP_repr: "finite_SMP_representation arity Ana Γ A"
    and B_SMP_repr: "finite_SMP_representation arity Ana Γ B"
    and C_wf: "wftrms C"
    and ABC: "∀t ∈ A. ∀s ∈ B. Γ t = Γ s ∧ mgu t s ≠ None ⟶ Q t ∨ R t"
  shows "g (SMP A) ∩ g (SMP B) ⊆ f C ∪ {m. {} ⊢c m}"
proof -
  have AB_wf: "wftrms A" "wftrms B"
    using A_SMP_repr B_SMP_repr finite_SMP_representationD(1)
    by (blast, blast)

  let ?P = "λt s. ∃δ. wtsubst δ ∧ wftrms (subst_range δ) ∧ Unifier δ t s"
  have ABC': "∀t ∈ A. ∀s ∈ B. ?P t s ⟶ Q t ∨ R t"
    by (metis (no_types) ABC mgu_None_is_subst_neq wt_subst_trm'')

  show ?thesis
    using ground_SMP_disjointI_aux1[OF f_def g_def, of A]
          ground_SMP_disjointI_aux1[OF f_def g_def, of B]
          ground_SMP_disjointI_aux2[OF f_def A_SMP_repr]
          ground_SMP_disjointI_aux2[OF f_def B_SMP_repr]
          ground_SMP_disjointI_aux3[OF f_def Q_def R_def AB_wf AB_fv_disj C_wf ABC']
    by argo
qed

end

end

end